Step | Hyp | Ref
| Expression |
1 | | poimirlem9.1 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ 𝑆) |
2 | | elrabi 3327 |
. . . . . . . . 9
⊢ (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
3 | | poimirlem22.s |
. . . . . . . . 9
⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} |
4 | 2, 3 | eleq2s 2705 |
. . . . . . . 8
⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
5 | 1, 4 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ ((((0..^𝐾) ↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
6 | | xp1st 7066 |
. . . . . . 7
⊢ (𝑇 ∈ ((((0..^𝐾) ↑_{𝑚}
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1^{st} ‘𝑇) ∈ (((0..^𝐾) ↑_{𝑚}
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
7 | 5, 6 | syl 17 |
. . . . . 6
⊢ (𝜑 → (1^{st}
‘𝑇) ∈
(((0..^𝐾)
↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
8 | | xp2nd 7067 |
. . . . . 6
⊢
((1^{st} ‘𝑇) ∈ (((0..^𝐾) ↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2^{nd}
‘(1^{st} ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
9 | 7, 8 | syl 17 |
. . . . 5
⊢ (𝜑 → (2^{nd}
‘(1^{st} ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
10 | | fvex 6097 |
. . . . . 6
⊢
(2^{nd} ‘(1^{st} ‘𝑇)) ∈ V |
11 | | f1oeq1 6024 |
. . . . . 6
⊢ (𝑓 = (2^{nd}
‘(1^{st} ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))) |
12 | 10, 11 | elab 3318 |
. . . . 5
⊢
((2^{nd} ‘(1^{st} ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
13 | 9, 12 | sylib 206 |
. . . 4
⊢ (𝜑 → (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
14 | | f1of 6034 |
. . . 4
⊢
((2^{nd} ‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)⟶(1...𝑁)) |
15 | 13, 14 | syl 17 |
. . 3
⊢ (𝜑 → (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)⟶(1...𝑁)) |
16 | | poimirlem9.2 |
. . . . . . . . 9
⊢ (𝜑 → (2^{nd}
‘𝑇) ∈
(1...(𝑁 −
1))) |
17 | | elfznn 12198 |
. . . . . . . . 9
⊢
((2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^{nd}
‘𝑇) ∈
ℕ) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (2^{nd}
‘𝑇) ∈
ℕ) |
19 | 18 | nnzd 11315 |
. . . . . . 7
⊢ (𝜑 → (2^{nd}
‘𝑇) ∈
ℤ) |
20 | | peano2zm 11255 |
. . . . . . 7
⊢
((2^{nd} ‘𝑇) ∈ ℤ → ((2^{nd}
‘𝑇) − 1) ∈
ℤ) |
21 | 19, 20 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((2^{nd}
‘𝑇) − 1) ∈
ℤ) |
22 | | poimir.0 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℕ) |
23 | 22 | nnzd 11315 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℤ) |
24 | 21 | zred 11316 |
. . . . . . 7
⊢ (𝜑 → ((2^{nd}
‘𝑇) − 1) ∈
ℝ) |
25 | 18 | nnred 10884 |
. . . . . . 7
⊢ (𝜑 → (2^{nd}
‘𝑇) ∈
ℝ) |
26 | 22 | nnred 10884 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℝ) |
27 | 25 | lem1d 10808 |
. . . . . . 7
⊢ (𝜑 → ((2^{nd}
‘𝑇) − 1) ≤
(2^{nd} ‘𝑇)) |
28 | | nnm1nn0 11183 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ_{0}) |
29 | 22, 28 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 − 1) ∈
ℕ_{0}) |
30 | 29 | nn0red 11201 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 − 1) ∈ ℝ) |
31 | | elfzle2 12173 |
. . . . . . . . 9
⊢
((2^{nd} ‘𝑇) ∈ (1...(𝑁 − 1)) → (2^{nd}
‘𝑇) ≤ (𝑁 − 1)) |
32 | 16, 31 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (2^{nd}
‘𝑇) ≤ (𝑁 − 1)) |
33 | 26 | lem1d 10808 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 − 1) ≤ 𝑁) |
34 | 25, 30, 26, 32, 33 | letrd 10045 |
. . . . . . 7
⊢ (𝜑 → (2^{nd}
‘𝑇) ≤ 𝑁) |
35 | 24, 25, 26, 27, 34 | letrd 10045 |
. . . . . 6
⊢ (𝜑 → ((2^{nd}
‘𝑇) − 1) ≤
𝑁) |
36 | | eluz2 11527 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ_{≥}‘((2^{nd} ‘𝑇) − 1)) ↔ (((2^{nd}
‘𝑇) − 1) ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ ((2^{nd} ‘𝑇) − 1) ≤ 𝑁)) |
37 | 21, 23, 35, 36 | syl3anbrc 1238 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈
(ℤ_{≥}‘((2^{nd} ‘𝑇) − 1))) |
38 | | fzss2 12209 |
. . . . 5
⊢ (𝑁 ∈
(ℤ_{≥}‘((2^{nd} ‘𝑇) − 1)) → (1...((2^{nd}
‘𝑇) − 1))
⊆ (1...𝑁)) |
39 | 37, 38 | syl 17 |
. . . 4
⊢ (𝜑 → (1...((2^{nd}
‘𝑇) − 1))
⊆ (1...𝑁)) |
40 | | poimirlem6.3 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ (1...((2^{nd} ‘𝑇) − 1))) |
41 | 39, 40 | sseldd 3568 |
. . 3
⊢ (𝜑 → 𝑀 ∈ (1...𝑁)) |
42 | 15, 41 | ffvelrnd 6252 |
. 2
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀) ∈ (1...𝑁)) |
43 | | xp1st 7066 |
. . . . . . . . . . . . 13
⊢
((1^{st} ‘𝑇) ∈ (((0..^𝐾) ↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^{st}
‘(1^{st} ‘𝑇)) ∈ ((0..^𝐾) ↑_{𝑚} (1...𝑁))) |
44 | 7, 43 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1^{st}
‘(1^{st} ‘𝑇)) ∈ ((0..^𝐾) ↑_{𝑚} (1...𝑁))) |
45 | | elmapfn 7743 |
. . . . . . . . . . . 12
⊢
((1^{st} ‘(1^{st} ‘𝑇)) ∈ ((0..^𝐾) ↑_{𝑚} (1...𝑁)) → (1^{st}
‘(1^{st} ‘𝑇)) Fn (1...𝑁)) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (1^{st}
‘(1^{st} ‘𝑇)) Fn (1...𝑁)) |
47 | 46 | adantr 479 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ≠ ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀)) → (1^{st}
‘(1^{st} ‘𝑇)) Fn (1...𝑁)) |
48 | | 1ex 9891 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
V |
49 | | fnconstg 5990 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
V → (((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn
((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1)))) |
50 | 48, 49 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn
((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) |
51 | | c0ex 9890 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
V |
52 | | fnconstg 5990 |
. . . . . . . . . . . . . . 15
⊢ (0 ∈
V → (((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0}) Fn ((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁))) |
53 | 51, 52 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0}) Fn ((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) |
54 | 50, 53 | pm3.2i 469 |
. . . . . . . . . . . . 13
⊢
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn
((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∧ (((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0}) Fn ((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁))) |
55 | | dff1o3 6040 |
. . . . . . . . . . . . . . . . 17
⊢
((2^{nd} ‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun ^{◡}(2^{nd} ‘(1^{st}
‘𝑇)))) |
56 | 55 | simprbi 478 |
. . . . . . . . . . . . . . . 16
⊢
((2^{nd} ‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ^{◡}(2^{nd} ‘(1^{st}
‘𝑇))) |
57 | 13, 56 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Fun ^{◡}(2^{nd} ‘(1^{st}
‘𝑇))) |
58 | | imain 5873 |
. . . . . . . . . . . . . . 15
⊢ (Fun
^{◡}(2^{nd} ‘(1^{st}
‘𝑇)) →
((2^{nd} ‘(1^{st} ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)))) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)))) |
60 | | elfznn 12198 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈ (1...((2^{nd}
‘𝑇) − 1))
→ 𝑀 ∈
ℕ) |
61 | 40, 60 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈ ℕ) |
62 | 61 | nnred 10884 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑀 ∈ ℝ) |
63 | 62 | ltm1d 10807 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑀 − 1) < 𝑀) |
64 | | fzdisj 12196 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 − 1) < 𝑀 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑁)) = ∅) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑁)) = ∅) |
66 | 65 | imaeq2d 5371 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ((2^{nd}
‘(1^{st} ‘𝑇)) “ ∅)) |
67 | | ima0 5386 |
. . . . . . . . . . . . . . 15
⊢
((2^{nd} ‘(1^{st} ‘𝑇)) “ ∅) =
∅ |
68 | 66, 67 | syl6eq 2659 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ∅) |
69 | 59, 68 | eqtr3d 2645 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁))) = ∅) |
70 | | fnun 5896 |
. . . . . . . . . . . . 13
⊢
((((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn
((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∧ (((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0}) Fn ((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁))) ∧ (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁))) = ∅) → ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})) Fn (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)))) |
71 | 54, 69, 70 | sylancr 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})) Fn (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)))) |
72 | 61 | nncnd 10885 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈ ℂ) |
73 | | npcan1 10306 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈ ℂ → ((𝑀 − 1) + 1) = 𝑀) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑀 − 1) + 1) = 𝑀) |
75 | | nnuz 11557 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℕ =
(ℤ_{≥}‘1) |
76 | 61, 75 | syl6eleq 2697 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈
(ℤ_{≥}‘1)) |
77 | 74, 76 | eqeltrd 2687 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑀 − 1) + 1) ∈
(ℤ_{≥}‘1)) |
78 | | nnm1nn0 11183 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑀 ∈ ℕ → (𝑀 − 1) ∈
ℕ_{0}) |
79 | 61, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑀 − 1) ∈
ℕ_{0}) |
80 | 79 | nn0zd 11314 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑀 − 1) ∈ ℤ) |
81 | | uzid 11536 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑀 − 1) ∈ ℤ
→ (𝑀 − 1) ∈
(ℤ_{≥}‘(𝑀 − 1))) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑀 − 1) ∈
(ℤ_{≥}‘(𝑀 − 1))) |
83 | | peano2uz 11575 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 − 1) ∈
(ℤ_{≥}‘(𝑀 − 1)) → ((𝑀 − 1) + 1) ∈
(ℤ_{≥}‘(𝑀 − 1))) |
84 | 82, 83 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑀 − 1) + 1) ∈
(ℤ_{≥}‘(𝑀 − 1))) |
85 | 74, 84 | eqeltrrd 2688 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈ (ℤ_{≥}‘(𝑀 − 1))) |
86 | | uzss 11542 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈
(ℤ_{≥}‘(𝑀 − 1)) →
(ℤ_{≥}‘𝑀) ⊆
(ℤ_{≥}‘(𝑀 − 1))) |
87 | 85, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 →
(ℤ_{≥}‘𝑀) ⊆
(ℤ_{≥}‘(𝑀 − 1))) |
88 | 61 | nnzd 11315 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈ ℤ) |
89 | | elfzle2 12173 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑀 ∈ (1...((2^{nd}
‘𝑇) − 1))
→ 𝑀 ≤
((2^{nd} ‘𝑇)
− 1)) |
90 | 40, 89 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑀 ≤ ((2^{nd} ‘𝑇) − 1)) |
91 | 62, 24, 26, 90, 35 | letrd 10045 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ≤ 𝑁) |
92 | | eluz2 11527 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈
(ℤ_{≥}‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |
93 | 88, 23, 91, 92 | syl3anbrc 1238 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ (ℤ_{≥}‘𝑀)) |
94 | 87, 93 | sseldd 3568 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ (ℤ_{≥}‘(𝑀 − 1))) |
95 | | fzsplit2 12194 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑀 − 1) + 1) ∈
(ℤ_{≥}‘1) ∧ 𝑁 ∈ (ℤ_{≥}‘(𝑀 − 1))) → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁))) |
96 | 77, 94, 95 | syl2anc 690 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁))) |
97 | 74 | oveq1d 6541 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝑀 − 1) + 1)...𝑁) = (𝑀...𝑁)) |
98 | 97 | uneq2d 3728 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁)) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))) |
99 | 96, 98 | eqtrd 2643 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))) |
100 | 99 | imaeq2d 5371 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑁)) = ((2^{nd} ‘(1^{st}
‘𝑇)) “
((1...(𝑀 − 1)) ∪
(𝑀...𝑁)))) |
101 | | imaundi 5449 |
. . . . . . . . . . . . . . 15
⊢
((2^{nd} ‘(1^{st} ‘𝑇)) “ ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁))) |
102 | 100, 101 | syl6eq 2659 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑁)) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)))) |
103 | | f1ofo 6041 |
. . . . . . . . . . . . . . . 16
⊢
((2^{nd} ‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–onto→(1...𝑁)) |
104 | 13, 103 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2^{nd}
‘(1^{st} ‘𝑇)):(1...𝑁)–onto→(1...𝑁)) |
105 | | foima 6017 |
. . . . . . . . . . . . . . 15
⊢
((2^{nd} ‘(1^{st} ‘𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) |
107 | 102, 106 | eqtr3d 2645 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁))) = (1...𝑁)) |
108 | 107 | fneq2d 5881 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})) Fn (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁))) ↔ ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})) Fn (1...𝑁))) |
109 | 71, 108 | mpbid 220 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})) Fn (1...𝑁)) |
110 | 109 | adantr 479 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ≠ ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀)) → ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})) Fn (1...𝑁)) |
111 | | ovex 6554 |
. . . . . . . . . . 11
⊢
(1...𝑁) ∈
V |
112 | 111 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ≠ ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀)) → (1...𝑁) ∈ V) |
113 | | inidm 3783 |
. . . . . . . . . 10
⊢
((1...𝑁) ∩
(1...𝑁)) = (1...𝑁) |
114 | | eqidd 2610 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ≠ ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → ((1^{st}
‘(1^{st} ‘𝑇))‘𝑛) = ((1^{st} ‘(1^{st}
‘𝑇))‘𝑛)) |
115 | | imaundi 5449 |
. . . . . . . . . . . . . . . . . 18
⊢
((2^{nd} ‘(1^{st} ‘𝑇)) “ ({𝑀} ∪ ((𝑀 + 1)...𝑁))) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ {𝑀}) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁))) |
116 | | fzpred 12216 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈
(ℤ_{≥}‘𝑀) → (𝑀...𝑁) = ({𝑀} ∪ ((𝑀 + 1)...𝑁))) |
117 | 93, 116 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑀...𝑁) = ({𝑀} ∪ ((𝑀 + 1)...𝑁))) |
118 | 117 | imaeq2d 5371 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) = ((2^{nd} ‘(1^{st}
‘𝑇)) “ ({𝑀} ∪ ((𝑀 + 1)...𝑁)))) |
119 | | f1ofn 6035 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2^{nd} ‘(1^{st} ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^{nd}
‘(1^{st} ‘𝑇)) Fn (1...𝑁)) |
120 | 13, 119 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (2^{nd}
‘(1^{st} ‘𝑇)) Fn (1...𝑁)) |
121 | | fnsnfv 6152 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((2^{nd} ‘(1^{st} ‘𝑇)) Fn (1...𝑁) ∧ 𝑀 ∈ (1...𝑁)) → {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} = ((2^{nd} ‘(1^{st}
‘𝑇)) “ {𝑀})) |
122 | 120, 41, 121 | syl2anc 690 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} = ((2^{nd} ‘(1^{st}
‘𝑇)) “ {𝑀})) |
123 | 122 | uneq1d 3727 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ {𝑀}) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
124 | 115, 118,
123 | 3eqtr4a 2669 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) = ({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
125 | 124 | xpeq1d 5051 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0}) = (({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁))) × {0})) |
126 | | xpundir 5084 |
. . . . . . . . . . . . . . . 16
⊢
(({((2^{nd} ‘(1^{st} ‘𝑇))‘𝑀)} ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁))) × {0}) = (({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} × {0}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) |
127 | 125, 126 | syl6eq 2659 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0}) = (({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} × {0}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) |
128 | 127 | uneq2d 3728 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})) = ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(({((2^{nd} ‘(1^{st} ‘𝑇))‘𝑀)} × {0}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))) |
129 | | un12 3732 |
. . . . . . . . . . . . . 14
⊢
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(({((2^{nd} ‘(1^{st} ‘𝑇))‘𝑀)} × {0}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) = (({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} × {0}) ∪ ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) |
130 | 128, 129 | syl6eq 2659 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})) = (({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} × {0}) ∪ ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))) |
131 | 130 | fveq1d 6089 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘𝑛) = ((({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} × {0}) ∪ ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛)) |
132 | 131 | ad2antrr 757 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ≠ ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘𝑛) = ((({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} × {0}) ∪ ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛)) |
133 | | fnconstg 5990 |
. . . . . . . . . . . . . . . . 17
⊢ (0 ∈
V → (((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁))) |
134 | 51, 133 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) |
135 | 50, 134 | pm3.2i 469 |
. . . . . . . . . . . . . . 15
⊢
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn
((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∧ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁))) |
136 | | imain 5873 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
^{◡}(2^{nd} ‘(1^{st}
‘𝑇)) →
((2^{nd} ‘(1^{st} ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁))) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
137 | 57, 136 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁))) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
138 | 79 | nn0red 11201 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑀 − 1) ∈ ℝ) |
139 | | peano2re 10060 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈
ℝ) |
140 | 62, 139 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑀 + 1) ∈ ℝ) |
141 | 62 | ltp1d 10805 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 < (𝑀 + 1)) |
142 | 138, 62, 140, 63, 141 | lttrd 10049 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑀 − 1) < (𝑀 + 1)) |
143 | | fzdisj 12196 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 − 1) < (𝑀 + 1) → ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁)) = ∅) |
144 | 142, 143 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁)) = ∅) |
145 | 144 | imaeq2d 5371 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁))) = ((2^{nd}
‘(1^{st} ‘𝑇)) “ ∅)) |
146 | 145, 67 | syl6eq 2659 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁))) = ∅) |
147 | 137, 146 | eqtr3d 2645 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅) |
148 | | fnun 5896 |
. . . . . . . . . . . . . . 15
⊢
((((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn
((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∧ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁))) ∧ (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅) → ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
149 | 135, 147,
148 | sylancr 693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
150 | | imaundi 5449 |
. . . . . . . . . . . . . . . 16
⊢
((2^{nd} ‘(1^{st} ‘𝑇)) “ ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁))) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁))) |
151 | | imadif 5872 |
. . . . . . . . . . . . . . . . . 18
⊢ (Fun
^{◡}(2^{nd} ‘(1^{st}
‘𝑇)) →
((2^{nd} ‘(1^{st} ‘𝑇)) “ ((1...𝑁) ∖ {𝑀})) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑁)) ∖ ((2^{nd}
‘(1^{st} ‘𝑇)) “ {𝑀}))) |
152 | 57, 151 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((1...𝑁) ∖ {𝑀})) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑁)) ∖ ((2^{nd}
‘(1^{st} ‘𝑇)) “ {𝑀}))) |
153 | | fzsplit 12195 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ (1...𝑁) → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) |
154 | 41, 153 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) |
155 | 154 | difeq1d 3688 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((1...𝑁) ∖ {𝑀}) = (((1...𝑀) ∪ ((𝑀 + 1)...𝑁)) ∖ {𝑀})) |
156 | | difundir 3838 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((1...𝑀) ∪
((𝑀 + 1)...𝑁)) ∖ {𝑀}) = (((1...𝑀) ∖ {𝑀}) ∪ (((𝑀 + 1)...𝑁) ∖ {𝑀})) |
157 | | fzsplit2 12194 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑀 − 1) + 1) ∈
(ℤ_{≥}‘1) ∧ 𝑀 ∈ (ℤ_{≥}‘(𝑀 − 1))) → (1...𝑀) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑀))) |
158 | 77, 85, 157 | syl2anc 690 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (1...𝑀) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑀))) |
159 | 74 | oveq1d 6541 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (((𝑀 − 1) + 1)...𝑀) = (𝑀...𝑀)) |
160 | | fzsn 12211 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀}) |
161 | 88, 160 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝑀...𝑀) = {𝑀}) |
162 | 159, 161 | eqtrd 2643 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (((𝑀 − 1) + 1)...𝑀) = {𝑀}) |
163 | 162 | uneq2d 3728 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑀)) = ((1...(𝑀 − 1)) ∪ {𝑀})) |
164 | 158, 163 | eqtrd 2643 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (1...𝑀) = ((1...(𝑀 − 1)) ∪ {𝑀})) |
165 | 164 | difeq1d 3688 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((1...𝑀) ∖ {𝑀}) = (((1...(𝑀 − 1)) ∪ {𝑀}) ∖ {𝑀})) |
166 | | difun2 3999 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((1...(𝑀 −
1)) ∪ {𝑀}) ∖
{𝑀}) = ((1...(𝑀 − 1)) ∖ {𝑀}) |
167 | 138, 62 | ltnled 10035 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((𝑀 − 1) < 𝑀 ↔ ¬ 𝑀 ≤ (𝑀 − 1))) |
168 | 63, 167 | mpbid 220 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ¬ 𝑀 ≤ (𝑀 − 1)) |
169 | | elfzle2 12173 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑀 ∈ (1...(𝑀 − 1)) → 𝑀 ≤ (𝑀 − 1)) |
170 | 168, 169 | nsyl 133 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ¬ 𝑀 ∈ (1...(𝑀 − 1))) |
171 | | difsn 4268 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
𝑀 ∈ (1...(𝑀 − 1)) → ((1...(𝑀 − 1)) ∖ {𝑀}) = (1...(𝑀 − 1))) |
172 | 170, 171 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((1...(𝑀 − 1)) ∖ {𝑀}) = (1...(𝑀 − 1))) |
173 | 166, 172 | syl5eq 2655 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (((1...(𝑀 − 1)) ∪ {𝑀}) ∖ {𝑀}) = (1...(𝑀 − 1))) |
174 | 165, 173 | eqtrd 2643 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((1...𝑀) ∖ {𝑀}) = (1...(𝑀 − 1))) |
175 | 62, 140 | ltnled 10035 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀)) |
176 | 141, 175 | mpbid 220 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ¬ (𝑀 + 1) ≤ 𝑀) |
177 | | elfzle1 12172 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 ∈ ((𝑀 + 1)...𝑁) → (𝑀 + 1) ≤ 𝑀) |
178 | 176, 177 | nsyl 133 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ¬ 𝑀 ∈ ((𝑀 + 1)...𝑁)) |
179 | | difsn 4268 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
𝑀 ∈ ((𝑀 + 1)...𝑁) → (((𝑀 + 1)...𝑁) ∖ {𝑀}) = ((𝑀 + 1)...𝑁)) |
180 | 178, 179 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (((𝑀 + 1)...𝑁) ∖ {𝑀}) = ((𝑀 + 1)...𝑁)) |
181 | 174, 180 | uneq12d 3729 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((1...𝑀) ∖ {𝑀}) ∪ (((𝑀 + 1)...𝑁) ∖ {𝑀})) = ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁))) |
182 | 156, 181 | syl5eq 2655 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((1...𝑀) ∪ ((𝑀 + 1)...𝑁)) ∖ {𝑀}) = ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁))) |
183 | 155, 182 | eqtrd 2643 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((1...𝑁) ∖ {𝑀}) = ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁))) |
184 | 183 | imaeq2d 5371 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((1...𝑁) ∖ {𝑀})) = ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁)))) |
185 | 122 | eqcomd 2615 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ {𝑀}) = {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)}) |
186 | 106, 185 | difeq12d 3690 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑁)) ∖ ((2^{nd}
‘(1^{st} ‘𝑇)) “ {𝑀})) = ((1...𝑁) ∖ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)})) |
187 | 152, 184,
186 | 3eqtr3d 2651 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁))) = ((1...𝑁) ∖ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)})) |
188 | 150, 187 | syl5eqr 2657 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ((1...𝑁) ∖ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)})) |
189 | 188 | fneq2d 5881 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁))) ↔ ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)}))) |
190 | 149, 189 | mpbid 220 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)})) |
191 | | eldifsn 4259 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ((1...𝑁) ∖ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)}) ↔ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀))) |
192 | 191 | biimpri 216 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀)) → 𝑛 ∈ ((1...𝑁) ∖ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)})) |
193 | 192 | ancoms 467 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ≠ ((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀) ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ((1...𝑁) ∖ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)})) |
194 | | disjdif 3991 |
. . . . . . . . . . . . . 14
⊢
({((2^{nd} ‘(1^{st} ‘𝑇))‘𝑀)} ∩ ((1...𝑁) ∖ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)})) = ∅ |
195 | | fnconstg 5990 |
. . . . . . . . . . . . . . . 16
⊢ (0 ∈
V → ({((2^{nd} ‘(1^{st} ‘𝑇))‘𝑀)} × {0}) Fn {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)}) |
196 | 51, 195 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
({((2^{nd} ‘(1^{st} ‘𝑇))‘𝑀)} × {0}) Fn {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} |
197 | | fvun2 6164 |
. . . . . . . . . . . . . . 15
⊢
((({((2^{nd} ‘(1^{st} ‘𝑇))‘𝑀)} × {0}) Fn {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} ∧ ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)}) ∧ (({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} ∩ ((1...𝑁) ∖ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)})) = ∅ ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)}))) → ((({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} × {0}) ∪ ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)) |
198 | 196, 197 | mp3an1 1402 |
. . . . . . . . . . . . . 14
⊢
((((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)}) ∧ (({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} ∩ ((1...𝑁) ∖ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)})) = ∅ ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)}))) → ((({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} × {0}) ∪ ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)) |
199 | 194, 198 | mpanr1 714 |
. . . . . . . . . . . . 13
⊢
((((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)}) ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)})) → ((({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} × {0}) ∪ ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)) |
200 | 190, 193,
199 | syl2an 492 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ≠ ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀) ∧ 𝑛 ∈ (1...𝑁))) → ((({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} × {0}) ∪ ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)) |
201 | 200 | anassrs 677 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ≠ ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → ((({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} × {0}) ∪ ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)) |
202 | 132, 201 | eqtrd 2643 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ≠ ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘𝑛) = (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)) |
203 | 47, 110, 112, 112, 113, 114, 202 | ofval 6781 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ≠ ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛) = (((1^{st} ‘(1^{st}
‘𝑇))‘𝑛) + (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))) |
204 | | fnconstg 5990 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
V → (((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) Fn ((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀))) |
205 | 48, 204 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) Fn ((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) |
206 | 205, 134 | pm3.2i 469 |
. . . . . . . . . . . . 13
⊢
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) Fn ((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) ∧ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁))) |
207 | | imain 5873 |
. . . . . . . . . . . . . . 15
⊢ (Fun
^{◡}(2^{nd} ‘(1^{st}
‘𝑇)) →
((2^{nd} ‘(1^{st} ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) ∩ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
208 | 57, 207 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) ∩ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
209 | | fzdisj 12196 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅) |
210 | 141, 209 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅) |
211 | 210 | imaeq2d 5371 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ((2^{nd}
‘(1^{st} ‘𝑇)) “ ∅)) |
212 | 211, 67 | syl6eq 2659 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ∅) |
213 | 208, 212 | eqtr3d 2645 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) ∩ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅) |
214 | | fnun 5896 |
. . . . . . . . . . . . 13
⊢
((((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) Fn ((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) ∧ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁))) ∧ (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) ∩ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅) → ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
215 | 206, 213,
214 | sylancr 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
216 | 154 | imaeq2d 5371 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑁)) = ((2^{nd} ‘(1^{st}
‘𝑇)) “
((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))) |
217 | | imaundi 5449 |
. . . . . . . . . . . . . . 15
⊢
((2^{nd} ‘(1^{st} ‘𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁))) |
218 | 216, 217 | syl6eq 2659 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑁)) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
219 | 218, 106 | eqtr3d 2645 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = (1...𝑁)) |
220 | 219 | fneq2d 5881 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁))) ↔ ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))) |
221 | 215, 220 | mpbid 220 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
222 | 221 | adantr 479 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ≠ ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀)) → ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
223 | | imaundi 5449 |
. . . . . . . . . . . . . . . . . 18
⊢
((2^{nd} ‘(1^{st} ‘𝑇)) “ ((1...(𝑀 − 1)) ∪ {𝑀})) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) “ {𝑀})) |
224 | 164 | imaeq2d 5371 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) = ((2^{nd} ‘(1^{st}
‘𝑇)) “
((1...(𝑀 − 1)) ∪
{𝑀}))) |
225 | 122 | uneq2d 3728 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∪ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)}) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2^{nd}
‘(1^{st} ‘𝑇)) “ {𝑀}))) |
226 | 223, 224,
225 | 3eqtr4a 2669 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∪ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)})) |
227 | 226 | xpeq1d 5051 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) = ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∪ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)}) × {1})) |
228 | | xpundir 5084 |
. . . . . . . . . . . . . . . 16
⊢
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∪ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)}) × {1}) = ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
({((2^{nd} ‘(1^{st} ‘𝑇))‘𝑀)} × {1})) |
229 | 227, 228 | syl6eq 2659 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) = ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
({((2^{nd} ‘(1^{st} ‘𝑇))‘𝑀)} × {1}))) |
230 | 229 | uneq1d 3727 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) = (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
({((2^{nd} ‘(1^{st} ‘𝑇))‘𝑀)} × {1})) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) |
231 | | un23 3733 |
. . . . . . . . . . . . . . 15
⊢
(((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
({((2^{nd} ‘(1^{st} ‘𝑇))‘𝑀)} × {1})) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) = (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) ∪ ({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} × {1})) |
232 | 231 | equncomi 3720 |
. . . . . . . . . . . . . 14
⊢
(((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
({((2^{nd} ‘(1^{st} ‘𝑇))‘𝑀)} × {1})) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) = (({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} × {1}) ∪ ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) |
233 | 230, 232 | syl6eq 2659 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) = (({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} × {1}) ∪ ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))) |
234 | 233 | fveq1d 6089 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛) = ((({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} × {1}) ∪ ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛)) |
235 | 234 | ad2antrr 757 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ≠ ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛) = ((({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} × {1}) ∪ ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛)) |
236 | | fnconstg 5990 |
. . . . . . . . . . . . . . . 16
⊢ (1 ∈
V → ({((2^{nd} ‘(1^{st} ‘𝑇))‘𝑀)} × {1}) Fn {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)}) |
237 | 48, 236 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
({((2^{nd} ‘(1^{st} ‘𝑇))‘𝑀)} × {1}) Fn {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} |
238 | | fvun2 6164 |
. . . . . . . . . . . . . . 15
⊢
((({((2^{nd} ‘(1^{st} ‘𝑇))‘𝑀)} × {1}) Fn {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} ∧ ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)}) ∧ (({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} ∩ ((1...𝑁) ∖ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)})) = ∅ ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)}))) → ((({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} × {1}) ∪ ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)) |
239 | 237, 238 | mp3an1 1402 |
. . . . . . . . . . . . . 14
⊢
((((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)}) ∧ (({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} ∩ ((1...𝑁) ∖ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)})) = ∅ ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)}))) → ((({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} × {1}) ∪ ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)) |
240 | 194, 239 | mpanr1 714 |
. . . . . . . . . . . . 13
⊢
((((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)}) ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)})) → ((({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} × {1}) ∪ ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)) |
241 | 190, 193,
240 | syl2an 492 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ≠ ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀) ∧ 𝑛 ∈ (1...𝑁))) → ((({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} × {1}) ∪ ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)) |
242 | 241 | anassrs 677 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ≠ ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → ((({((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)} × {1}) ∪ ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)) |
243 | 235, 242 | eqtrd 2643 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ≠ ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛) = (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)) |
244 | 47, 222, 112, 112, 113, 114, 243 | ofval 6781 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ≠ ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((1^{st} ‘(1^{st}
‘𝑇))‘𝑛) + (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))) |
245 | 203, 244 | eqtr4d 2646 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ≠ ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛) = (((1^{st} ‘(1^{st}
‘𝑇))
∘_{𝑓} + ((((2^{nd} ‘(1^{st}
‘𝑇)) “
(1...𝑀)) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛)) |
246 | 245 | an32s 841 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑛 ≠ ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀)) → (((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛) = (((1^{st} ‘(1^{st}
‘𝑇))
∘_{𝑓} + ((((2^{nd} ‘(1^{st}
‘𝑇)) “
(1...𝑀)) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛)) |
247 | 246 | anasss 676 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀))) → (((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛) = (((1^{st} ‘(1^{st}
‘𝑇))
∘_{𝑓} + ((((2^{nd} ‘(1^{st}
‘𝑇)) “
(1...𝑀)) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛)) |
248 | | fveq2 6087 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 𝑇 → (2^{nd} ‘𝑡) = (2^{nd} ‘𝑇)) |
249 | 248 | breq2d 4589 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 𝑇 → (𝑦 < (2^{nd} ‘𝑡) ↔ 𝑦 < (2^{nd} ‘𝑇))) |
250 | 249 | ifbid 4057 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑇 → if(𝑦 < (2^{nd} ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2^{nd} ‘𝑇), 𝑦, (𝑦 + 1))) |
251 | 250 | csbeq1d 3505 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^{nd} ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
252 | | fveq2 6087 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 𝑇 → (1^{st} ‘𝑡) = (1^{st} ‘𝑇)) |
253 | 252 | fveq2d 6091 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 𝑇 → (1^{st}
‘(1^{st} ‘𝑡)) = (1^{st} ‘(1^{st}
‘𝑇))) |
254 | 252 | fveq2d 6091 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = 𝑇 → (2^{nd}
‘(1^{st} ‘𝑡)) = (2^{nd} ‘(1^{st}
‘𝑇))) |
255 | 254 | imaeq1d 5370 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑇 → ((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) = ((2^{nd} ‘(1^{st}
‘𝑇)) “
(1...𝑗))) |
256 | 255 | xpeq1d 5051 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 𝑇 → (((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1})) |
257 | 254 | imaeq1d 5370 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑇 → ((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2^{nd} ‘(1^{st}
‘𝑇)) “ ((𝑗 + 1)...𝑁))) |
258 | 257 | xpeq1d 5051 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 𝑇 → (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) |
259 | 256, 258 | uneq12d 3729 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 𝑇 → ((((2^{nd}
‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) |
260 | 253, 259 | oveq12d 6544 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑇 → ((1^{st}
‘(1^{st} ‘𝑡)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
261 | 260 | csbeq2dv 3943 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^{nd} ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
262 | 251, 261 | eqtrd 2643 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2^{nd} ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
263 | 262 | mpteq2dv 4667 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
264 | 263 | eqeq2d 2619 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑡)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
265 | 264, 3 | elrab2 3332 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ 𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑_{𝑚} (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
266 | 265 | simprbi 478 |
. . . . . . . . . 10
⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
267 | 1, 266 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
268 | | breq1 4580 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑀 − 1) → (𝑦 < (2^{nd} ‘𝑇) ↔ (𝑀 − 1) < (2^{nd}
‘𝑇))) |
269 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑀 − 1) → 𝑦 = (𝑀 − 1)) |
270 | 268, 269 | ifbieq1d 4058 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑀 − 1) → if(𝑦 < (2^{nd} ‘𝑇), 𝑦, (𝑦 + 1)) = if((𝑀 − 1) < (2^{nd}
‘𝑇), (𝑀 − 1), (𝑦 + 1))) |
271 | 25 | ltm1d 10807 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2^{nd}
‘𝑇) − 1) <
(2^{nd} ‘𝑇)) |
272 | 62, 24, 25, 90, 271 | lelttrd 10046 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 < (2^{nd} ‘𝑇)) |
273 | 138, 62, 25, 63, 272 | lttrd 10049 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀 − 1) < (2^{nd}
‘𝑇)) |
274 | 273 | iftrued 4043 |
. . . . . . . . . . . 12
⊢ (𝜑 → if((𝑀 − 1) < (2^{nd}
‘𝑇), (𝑀 − 1), (𝑦 + 1)) = (𝑀 − 1)) |
275 | 270, 274 | sylan9eqr 2665 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → if(𝑦 < (2^{nd} ‘𝑇), 𝑦, (𝑦 + 1)) = (𝑀 − 1)) |
276 | 275 | csbeq1d 3505 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋(𝑀 − 1) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
277 | | oveq2 6534 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = (𝑀 − 1) → (1...𝑗) = (1...(𝑀 − 1))) |
278 | 277 | imaeq2d 5371 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = (𝑀 − 1) → ((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑗)) = ((2^{nd} ‘(1^{st}
‘𝑇)) “
(1...(𝑀 −
1)))) |
279 | 278 | xpeq1d 5051 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = (𝑀 − 1) → (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1})) |
280 | 279 | adantl 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1})) |
281 | | oveq1 6533 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = (𝑀 − 1) → (𝑗 + 1) = ((𝑀 − 1) + 1)) |
282 | 281, 74 | sylan9eqr 2665 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (𝑗 + 1) = 𝑀) |
283 | 282 | oveq1d 6541 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((𝑗 + 1)...𝑁) = (𝑀...𝑁)) |
284 | 283 | imaeq2d 5371 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2^{nd} ‘(1^{st}
‘𝑇)) “ (𝑀...𝑁))) |
285 | 284 | xpeq1d 5051 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})) |
286 | 280, 285 | uneq12d 3729 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0}))) |
287 | 286 | oveq2d 6542 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})))) |
288 | 79, 287 | csbied 3525 |
. . . . . . . . . . 11
⊢ (𝜑 → ⦋(𝑀 − 1) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})))) |
289 | 288 | adantr 479 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋(𝑀 − 1) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})))) |
290 | 276, 289 | eqtrd 2643 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})))) |
291 | | 1red 9911 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℝ) |
292 | 62, 26, 291, 91 | lesub1dd 10494 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 − 1) ≤ (𝑁 − 1)) |
293 | | elfz2nn0 12257 |
. . . . . . . . . 10
⊢ ((𝑀 − 1) ∈ (0...(𝑁 − 1)) ↔ ((𝑀 − 1) ∈
ℕ_{0} ∧ (𝑁 − 1) ∈ ℕ_{0} ∧
(𝑀 − 1) ≤ (𝑁 − 1))) |
294 | 79, 29, 292, 293 | syl3anbrc 1238 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 − 1) ∈ (0...(𝑁 − 1))) |
295 | | ovex 6554 |
. . . . . . . . . 10
⊢
((1^{st} ‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0}))) ∈ V |
296 | 295 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0}))) ∈ V) |
297 | 267, 290,
294, 296 | fvmptd 6181 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘(𝑀 − 1)) = ((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})))) |
298 | 297 | fveq1d 6089 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘(𝑀 − 1))‘𝑛) = (((1^{st} ‘(1^{st}
‘𝑇))
∘_{𝑓} + ((((2^{nd} ‘(1^{st}
‘𝑇)) “
(1...(𝑀 − 1)))
× {1}) ∪ (((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛)) |
299 | 298 | adantr 479 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀))) → ((𝐹‘(𝑀 − 1))‘𝑛) = (((1^{st} ‘(1^{st}
‘𝑇))
∘_{𝑓} + ((((2^{nd} ‘(1^{st}
‘𝑇)) “
(1...(𝑀 − 1)))
× {1}) ∪ (((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛)) |
300 | | breq1 4580 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑀 → (𝑦 < (2^{nd} ‘𝑇) ↔ 𝑀 < (2^{nd} ‘𝑇))) |
301 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑀 → 𝑦 = 𝑀) |
302 | 300, 301 | ifbieq1d 4058 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑀 → if(𝑦 < (2^{nd} ‘𝑇), 𝑦, (𝑦 + 1)) = if(𝑀 < (2^{nd} ‘𝑇), 𝑀, (𝑦 + 1))) |
303 | 272 | iftrued 4043 |
. . . . . . . . . . . 12
⊢ (𝜑 → if(𝑀 < (2^{nd} ‘𝑇), 𝑀, (𝑦 + 1)) = 𝑀) |
304 | 302, 303 | sylan9eqr 2665 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 = 𝑀) → if(𝑦 < (2^{nd} ‘𝑇), 𝑦, (𝑦 + 1)) = 𝑀) |
305 | 304 | csbeq1d 3505 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = 𝑀) → ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑀 / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
306 | | oveq2 6534 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑀 → (1...𝑗) = (1...𝑀)) |
307 | 306 | imaeq2d 5371 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑀 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑗)) = ((2^{nd} ‘(1^{st}
‘𝑇)) “
(1...𝑀))) |
308 | 307 | xpeq1d 5051 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑀 → (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1})) |
309 | | oveq1 6533 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑀 → (𝑗 + 1) = (𝑀 + 1)) |
310 | 309 | oveq1d 6541 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑀 → ((𝑗 + 1)...𝑁) = ((𝑀 + 1)...𝑁)) |
311 | 310 | imaeq2d 5371 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑀 → ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2^{nd} ‘(1^{st}
‘𝑇)) “ ((𝑀 + 1)...𝑁))) |
312 | 311 | xpeq1d 5051 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑀 → (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) |
313 | 308, 312 | uneq12d 3729 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑀 → ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) |
314 | 313 | oveq2d 6542 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑀 → ((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))) |
315 | 314 | adantl 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 = 𝑀) → ((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))) |
316 | 40, 315 | csbied 3525 |
. . . . . . . . . . 11
⊢ (𝜑 → ⦋𝑀 / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))) |
317 | 316 | adantr 479 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = 𝑀) → ⦋𝑀 / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))) |
318 | 305, 317 | eqtrd 2643 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = 𝑀) → ⦋if(𝑦 < (2^{nd}
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))) |
319 | 29 | nn0zd 11314 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) |
320 | 25, 26, 291, 34 | lesub1dd 10494 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2^{nd}
‘𝑇) − 1) ≤
(𝑁 −
1)) |
321 | | eluz2 11527 |
. . . . . . . . . . . . 13
⊢ ((𝑁 − 1) ∈
(ℤ_{≥}‘((2^{nd} ‘𝑇) − 1)) ↔ (((2^{nd}
‘𝑇) − 1) ∈
ℤ ∧ (𝑁 − 1)
∈ ℤ ∧ ((2^{nd} ‘𝑇) − 1) ≤ (𝑁 − 1))) |
322 | 21, 319, 320, 321 | syl3anbrc 1238 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 − 1) ∈
(ℤ_{≥}‘((2^{nd} ‘𝑇) − 1))) |
323 | | fzss2 12209 |
. . . . . . . . . . . 12
⊢ ((𝑁 − 1) ∈
(ℤ_{≥}‘((2^{nd} ‘𝑇) − 1)) → (1...((2^{nd}
‘𝑇) − 1))
⊆ (1...(𝑁 −
1))) |
324 | 322, 323 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (1...((2^{nd}
‘𝑇) − 1))
⊆ (1...(𝑁 −
1))) |
325 | | 1eluzge0 11566 |
. . . . . . . . . . . 12
⊢ 1 ∈
(ℤ_{≥}‘0) |
326 | | fzss1 12208 |
. . . . . . . . . . . 12
⊢ (1 ∈
(ℤ_{≥}‘0) → (1...(𝑁 − 1)) ⊆ (0...(𝑁 − 1))) |
327 | 325, 326 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(1...(𝑁 − 1))
⊆ (0...(𝑁 −
1)) |
328 | 324, 327 | syl6ss 3579 |
. . . . . . . . . 10
⊢ (𝜑 → (1...((2^{nd}
‘𝑇) − 1))
⊆ (0...(𝑁 −
1))) |
329 | 328, 40 | sseldd 3568 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ (0...(𝑁 − 1))) |
330 | | ovex 6554 |
. . . . . . . . . 10
⊢
((1^{st} ‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) ∈ V |
331 | 330 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) ∈ V) |
332 | 267, 318,
329, 331 | fvmptd 6181 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝑀) = ((1^{st} ‘(1^{st}
‘𝑇))
∘_{𝑓} + ((((2^{nd} ‘(1^{st}
‘𝑇)) “
(1...𝑀)) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))) |
333 | 332 | fveq1d 6089 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘𝑀)‘𝑛) = (((1^{st} ‘(1^{st}
‘𝑇))
∘_{𝑓} + ((((2^{nd} ‘(1^{st}
‘𝑇)) “
(1...𝑀)) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛)) |
334 | 333 | adantr 479 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀))) → ((𝐹‘𝑀)‘𝑛) = (((1^{st} ‘(1^{st}
‘𝑇))
∘_{𝑓} + ((((2^{nd} ‘(1^{st}
‘𝑇)) “
(1...𝑀)) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛)) |
335 | 247, 299,
334 | 3eqtr4d 2653 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀))) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘𝑀)‘𝑛)) |
336 | 335 | expr 640 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 ≠ ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘𝑀)‘𝑛))) |
337 | 336 | necon1d 2803 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) → 𝑛 = ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀))) |
338 | | elmapi 7742 |
. . . . . . . . . . 11
⊢
((1^{st} ‘(1^{st} ‘𝑇)) ∈ ((0..^𝐾) ↑_{𝑚} (1...𝑁)) → (1^{st}
‘(1^{st} ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
339 | 44, 338 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (1^{st}
‘(1^{st} ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
340 | 339, 42 | ffvelrnd 6252 |
. . . . . . . . 9
⊢ (𝜑 → ((1^{st}
‘(1^{st} ‘𝑇))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) ∈ (0..^𝐾)) |
341 | | elfzonn0 12337 |
. . . . . . . . 9
⊢
(((1^{st} ‘(1^{st} ‘𝑇))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) ∈ (0..^𝐾) → ((1^{st}
‘(1^{st} ‘𝑇))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) ∈
ℕ_{0}) |
342 | 340, 341 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((1^{st}
‘(1^{st} ‘𝑇))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) ∈
ℕ_{0}) |
343 | 342 | nn0red 11201 |
. . . . . . 7
⊢ (𝜑 → ((1^{st}
‘(1^{st} ‘𝑇))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) ∈ ℝ) |
344 | 343 | ltp1d 10805 |
. . . . . . 7
⊢ (𝜑 → ((1^{st}
‘(1^{st} ‘𝑇))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) < (((1^{st}
‘(1^{st} ‘𝑇))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) + 1)) |
345 | 343, 344 | ltned 10024 |
. . . . . 6
⊢ (𝜑 → ((1^{st}
‘(1^{st} ‘𝑇))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) ≠ (((1^{st}
‘(1^{st} ‘𝑇))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) + 1)) |
346 | 297 | fveq1d 6089 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘(𝑀 − 1))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) = (((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀))) |
347 | 111 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (1...𝑁) ∈ V) |
348 | | eqidd 2610 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀) ∈ (1...𝑁)) → ((1^{st}
‘(1^{st} ‘𝑇))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) = ((1^{st} ‘(1^{st}
‘𝑇))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀))) |
349 | | fzss1 12208 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈
(ℤ_{≥}‘1) → (𝑀...𝑁) ⊆ (1...𝑁)) |
350 | 76, 349 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀...𝑁) ⊆ (1...𝑁)) |
351 | | eluzfz1 12176 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ_{≥}‘𝑀) → 𝑀 ∈ (𝑀...𝑁)) |
352 | 93, 351 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁)) |
353 | | fnfvima 6377 |
. . . . . . . . . . . . 13
⊢
(((2^{nd} ‘(1^{st} ‘𝑇)) Fn (1...𝑁) ∧ (𝑀...𝑁) ⊆ (1...𝑁) ∧ 𝑀 ∈ (𝑀...𝑁)) → ((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀) ∈ ((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁))) |
354 | 120, 350,
352, 353 | syl3anc 1317 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀) ∈ ((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁))) |
355 | | fvun2 6164 |
. . . . . . . . . . . . 13
⊢
(((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn
((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∧ (((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0}) Fn ((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) ∧ ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁))) = ∅ ∧ ((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀) ∈ ((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)))) → (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) = ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀))) |
356 | 50, 53, 355 | mp3an12 1405 |
. . . . . . . . . . . 12
⊢
(((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁))) = ∅ ∧ ((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀) ∈ ((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁))) → (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) = ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀))) |
357 | 69, 354, 356 | syl2anc 690 |
. . . . . . . . . . 11
⊢ (𝜑 → (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) = ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀))) |
358 | 51 | fvconst2 6351 |
. . . . . . . . . . . 12
⊢
(((2^{nd} ‘(1^{st} ‘𝑇))‘𝑀) ∈ ((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) → ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) = 0) |
359 | 354, 358 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) = 0) |
360 | 357, 359 | eqtrd 2643 |
. . . . . . . . . 10
⊢ (𝜑 → (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) = 0) |
361 | 360 | adantr 479 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀) ∈ (1...𝑁)) → (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) = 0) |
362 | 46, 109, 347, 347, 113, 348, 361 | ofval 6781 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀) ∈ (1...𝑁)) → (((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) = (((1^{st}
‘(1^{st} ‘𝑇))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) + 0)) |
363 | 42, 362 | mpdan 698 |
. . . . . . 7
⊢ (𝜑 → (((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2^{nd} ‘(1^{st} ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) = (((1^{st}
‘(1^{st} ‘𝑇))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) + 0)) |
364 | 342 | nn0cnd 11202 |
. . . . . . . 8
⊢ (𝜑 → ((1^{st}
‘(1^{st} ‘𝑇))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) ∈ ℂ) |
365 | 364 | addid1d 10087 |
. . . . . . 7
⊢ (𝜑 → (((1^{st}
‘(1^{st} ‘𝑇))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) + 0) = ((1^{st}
‘(1^{st} ‘𝑇))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀))) |
366 | 346, 363,
365 | 3eqtrd 2647 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘(𝑀 − 1))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) = ((1^{st} ‘(1^{st}
‘𝑇))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀))) |
367 | 332 | fveq1d 6089 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘𝑀)‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) = (((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀))) |
368 | | fzss2 12209 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ_{≥}‘𝑀) → (1...𝑀) ⊆ (1...𝑁)) |
369 | 93, 368 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1...𝑀) ⊆ (1...𝑁)) |
370 | | elfz1end 12199 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ ↔ 𝑀 ∈ (1...𝑀)) |
371 | 61, 370 | sylib 206 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ (1...𝑀)) |
372 | | fnfvima 6377 |
. . . . . . . . . . . . 13
⊢
(((2^{nd} ‘(1^{st} ‘𝑇)) Fn (1...𝑁) ∧ (1...𝑀) ⊆ (1...𝑁) ∧ 𝑀 ∈ (1...𝑀)) → ((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀) ∈ ((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀))) |
373 | 120, 369,
371, 372 | syl3anc 1317 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀) ∈ ((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀))) |
374 | | fvun1 6163 |
. . . . . . . . . . . . 13
⊢
(((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) Fn ((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) ∧ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) ∧ ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) ∩ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅ ∧ ((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀) ∈ ((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)))) → (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) = ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1})‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀))) |
375 | 205, 134,
374 | mp3an12 1405 |
. . . . . . . . . . . 12
⊢
(((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑀)) ∩ ((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅ ∧ ((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀) ∈ ((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀))) → (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) = ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1})‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀))) |
376 | 213, 373,
375 | syl2anc 690 |
. . . . . . . . . . 11
⊢ (𝜑 → (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) = ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1})‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀))) |
377 | 48 | fvconst2 6351 |
. . . . . . . . . . . 12
⊢
(((2^{nd} ‘(1^{st} ‘𝑇))‘𝑀) ∈ ((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) → ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1})‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) = 1) |
378 | 373, 377 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1})‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) = 1) |
379 | 376, 378 | eqtrd 2643 |
. . . . . . . . . 10
⊢ (𝜑 → (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) = 1) |
380 | 379 | adantr 479 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀) ∈ (1...𝑁)) → (((((2^{nd}
‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) = 1) |
381 | 46, 221, 347, 347, 113, 348, 380 | ofval 6781 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀) ∈ (1...𝑁)) → (((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) = (((1^{st}
‘(1^{st} ‘𝑇))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) + 1)) |
382 | 42, 381 | mpdan 698 |
. . . . . . 7
⊢ (𝜑 → (((1^{st}
‘(1^{st} ‘𝑇)) ∘_{𝑓} +
((((2^{nd} ‘(1^{st} ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2^{nd}
‘(1^{st} ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) = (((1^{st}
‘(1^{st} ‘𝑇))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) + 1)) |
383 | 367, 382 | eqtrd 2643 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘𝑀)‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) = (((1^{st}
‘(1^{st} ‘𝑇))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) + 1)) |
384 | 345, 366,
383 | 3netr4d 2858 |
. . . . 5
⊢ (𝜑 → ((𝐹‘(𝑀 − 1))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) ≠ ((𝐹‘𝑀)‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀))) |
385 | | fveq2 6087 |
. . . . . 6
⊢ (𝑛 = ((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘(𝑀 − 1))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀))) |
386 | | fveq2 6087 |
. . . . . 6
⊢ (𝑛 = ((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀) → ((𝐹‘𝑀)‘𝑛) = ((𝐹‘𝑀)‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀))) |
387 | 385, 386 | neeq12d 2842 |
. . . . 5
⊢ (𝑛 = ((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀) → (((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ((𝐹‘(𝑀 − 1))‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)) ≠ ((𝐹‘𝑀)‘((2^{nd}
‘(1^{st} ‘𝑇))‘𝑀)))) |
388 | 384, 387 | syl5ibrcom 235 |
. . . 4
⊢ (𝜑 → (𝑛 = ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀) → ((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛))) |
389 | 388 | adantr 479 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 = ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀) → ((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛))) |
390 | 337, 389 | impbid 200 |
. 2
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ 𝑛 = ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀))) |
391 | 42, 390 | riota5 6513 |
1
⊢ (𝜑 → (℩𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛)) = ((2^{nd} ‘(1^{st}
‘𝑇))‘𝑀)) |