Proof of Theorem poimirlem7
Step | Hyp | Ref
| Expression |
1 | | poimirlem9.1 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ 𝑆) |
2 | | elrabi 3619 |
. . . . . . . . 9
⊢ (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
3 | | poimirlem22.s |
. . . . . . . . 9
⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} |
4 | 2, 3 | eleq2s 2858 |
. . . . . . . 8
⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
5 | 1, 4 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
6 | | xp1st 7849 |
. . . . . . 7
⊢ (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
7 | 5, 6 | syl 17 |
. . . . . 6
⊢ (𝜑 → (1st
‘𝑇) ∈
(((0..^𝐾)
↑m (1...𝑁))
× {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
8 | | xp2nd 7850 |
. . . . . 6
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
9 | 7, 8 | syl 17 |
. . . . 5
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
10 | | fvex 6781 |
. . . . . 6
⊢
(2nd ‘(1st ‘𝑇)) ∈ V |
11 | | f1oeq1 6700 |
. . . . . 6
⊢ (𝑓 = (2nd
‘(1st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))) |
12 | 10, 11 | elab 3610 |
. . . . 5
⊢
((2nd ‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
13 | 9, 12 | sylib 217 |
. . . 4
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
14 | | f1of 6712 |
. . . 4
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑇)):(1...𝑁)⟶(1...𝑁)) |
15 | 13, 14 | syl 17 |
. . 3
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)⟶(1...𝑁)) |
16 | | poimirlem9.2 |
. . . . . . . . 9
⊢ (𝜑 → (2nd
‘𝑇) ∈
(1...(𝑁 −
1))) |
17 | | elfznn 13267 |
. . . . . . . . 9
⊢
((2nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2nd
‘𝑇) ∈
ℕ) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (2nd
‘𝑇) ∈
ℕ) |
19 | 18 | peano2nnd 11973 |
. . . . . . 7
⊢ (𝜑 → ((2nd
‘𝑇) + 1) ∈
ℕ) |
20 | 19 | peano2nnd 11973 |
. . . . . 6
⊢ (𝜑 → (((2nd
‘𝑇) + 1) + 1) ∈
ℕ) |
21 | | nnuz 12603 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
22 | 20, 21 | eleqtrdi 2850 |
. . . . 5
⊢ (𝜑 → (((2nd
‘𝑇) + 1) + 1) ∈
(ℤ≥‘1)) |
23 | | fzss1 13277 |
. . . . 5
⊢
((((2nd ‘𝑇) + 1) + 1) ∈
(ℤ≥‘1) → ((((2nd ‘𝑇) + 1) + 1)...𝑁) ⊆ (1...𝑁)) |
24 | 22, 23 | syl 17 |
. . . 4
⊢ (𝜑 → ((((2nd
‘𝑇) + 1) + 1)...𝑁) ⊆ (1...𝑁)) |
25 | | poimirlem7.3 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ((((2nd ‘𝑇) + 1) + 1)...𝑁)) |
26 | 24, 25 | sseldd 3926 |
. . 3
⊢ (𝜑 → 𝑀 ∈ (1...𝑁)) |
27 | 15, 26 | ffvelrnd 6956 |
. 2
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇))‘𝑀) ∈ (1...𝑁)) |
28 | | xp1st 7849 |
. . . . . . . . . . . . 13
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁))) |
29 | 7, 28 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁))) |
30 | | elmapfn 8627 |
. . . . . . . . . . . 12
⊢
((1st ‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st
‘(1st ‘𝑇)) Fn (1...𝑁)) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (1st
‘(1st ‘𝑇)) Fn (1...𝑁)) |
32 | 31 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) → (1st
‘(1st ‘𝑇)) Fn (1...𝑁)) |
33 | | 1ex 10955 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
V |
34 | | fnconstg 6658 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
V → (((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn
((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1)))) |
35 | 33, 34 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn
((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) |
36 | | c0ex 10953 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
V |
37 | | fnconstg 6658 |
. . . . . . . . . . . . . . 15
⊢ (0 ∈
V → (((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁))) |
38 | 36, 37 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)) |
39 | 35, 38 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn
((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∧ (((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁))) |
40 | | dff1o3 6718 |
. . . . . . . . . . . . . . . . 17
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd
‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun ◡(2nd ‘(1st
‘𝑇)))) |
41 | 40 | simprbi 496 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ◡(2nd ‘(1st
‘𝑇))) |
42 | 13, 41 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Fun ◡(2nd ‘(1st
‘𝑇))) |
43 | | imain 6515 |
. . . . . . . . . . . . . . 15
⊢ (Fun
◡(2nd ‘(1st
‘𝑇)) →
((2nd ‘(1st ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)))) |
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)))) |
45 | 25 | elfzelzd 13239 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈ ℤ) |
46 | 45 | zred 12408 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑀 ∈ ℝ) |
47 | 46 | ltm1d 11890 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑀 − 1) < 𝑀) |
48 | | fzdisj 13265 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 − 1) < 𝑀 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑁)) = ∅) |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑁)) = ∅) |
50 | 49 | imaeq2d 5966 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ((2nd
‘(1st ‘𝑇)) “ ∅)) |
51 | | ima0 5982 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘(1st ‘𝑇)) “ ∅) =
∅ |
52 | 50, 51 | eqtrdi 2795 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ∅) |
53 | 44, 52 | eqtr3d 2781 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁))) = ∅) |
54 | | fnun 6541 |
. . . . . . . . . . . . 13
⊢
((((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn
((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∧ (((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁))) ∧ (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁))) = ∅) → ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})) Fn (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)))) |
55 | 39, 53, 54 | sylancr 586 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})) Fn (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)))) |
56 | 45 | zcnd 12409 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈ ℂ) |
57 | | npcan1 11383 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈ ℂ → ((𝑀 − 1) + 1) = 𝑀) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑀 − 1) + 1) = 𝑀) |
59 | | 1red 10960 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 1 ∈
ℝ) |
60 | 20 | nnred 11971 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (((2nd
‘𝑇) + 1) + 1) ∈
ℝ) |
61 | 19 | nnred 11971 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((2nd
‘𝑇) + 1) ∈
ℝ) |
62 | 19 | nnge1d 12004 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 1 ≤ ((2nd
‘𝑇) +
1)) |
63 | 61 | ltp1d 11888 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((2nd
‘𝑇) + 1) <
(((2nd ‘𝑇)
+ 1) + 1)) |
64 | 59, 61, 60, 62, 63 | lelttrd 11116 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 1 < (((2nd
‘𝑇) + 1) +
1)) |
65 | | elfzle1 13241 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑀 ∈ ((((2nd
‘𝑇) + 1) + 1)...𝑁) → (((2nd
‘𝑇) + 1) + 1) ≤
𝑀) |
66 | 25, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (((2nd
‘𝑇) + 1) + 1) ≤
𝑀) |
67 | 59, 60, 46, 64, 66 | ltletrd 11118 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 1 < 𝑀) |
68 | 59, 46, 67 | ltled 11106 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 1 ≤ 𝑀) |
69 | | elnnz1 12329 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ ℕ ↔ (𝑀 ∈ ℤ ∧ 1 ≤
𝑀)) |
70 | 45, 68, 69 | sylanbrc 582 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈ ℕ) |
71 | 70, 21 | eleqtrdi 2850 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
72 | 58, 71 | eqeltrd 2840 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑀 − 1) + 1) ∈
(ℤ≥‘1)) |
73 | | peano2zm 12346 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈
ℤ) |
74 | 45, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑀 − 1) ∈ ℤ) |
75 | | uzid 12579 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 − 1) ∈ ℤ
→ (𝑀 − 1) ∈
(ℤ≥‘(𝑀 − 1))) |
76 | | peano2uz 12623 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 − 1) ∈
(ℤ≥‘(𝑀 − 1)) → ((𝑀 − 1) + 1) ∈
(ℤ≥‘(𝑀 − 1))) |
77 | 74, 75, 76 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑀 − 1) + 1) ∈
(ℤ≥‘(𝑀 − 1))) |
78 | 58, 77 | eqeltrrd 2841 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘(𝑀 − 1))) |
79 | | uzss 12587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈
(ℤ≥‘(𝑀 − 1)) →
(ℤ≥‘𝑀) ⊆
(ℤ≥‘(𝑀 − 1))) |
80 | 78, 79 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 →
(ℤ≥‘𝑀) ⊆
(ℤ≥‘(𝑀 − 1))) |
81 | | elfzuz3 13235 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈ ((((2nd
‘𝑇) + 1) + 1)...𝑁) → 𝑁 ∈ (ℤ≥‘𝑀)) |
82 | 25, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
83 | 80, 82 | sseldd 3926 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 − 1))) |
84 | | fzsplit2 13263 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑀 − 1) + 1) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 − 1))) → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁))) |
85 | 72, 83, 84 | syl2anc 583 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁))) |
86 | 58 | oveq1d 7283 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝑀 − 1) + 1)...𝑁) = (𝑀...𝑁)) |
87 | 86 | uneq2d 4101 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁)) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))) |
88 | 85, 87 | eqtrd 2779 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))) |
89 | 88 | imaeq2d 5966 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = ((2nd ‘(1st
‘𝑇)) “
((1...(𝑀 − 1)) ∪
(𝑀...𝑁)))) |
90 | | imaundi 6050 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘(1st ‘𝑇)) “ ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁))) |
91 | 89, 90 | eqtrdi 2795 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)))) |
92 | | f1ofo 6719 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁)) |
93 | 13, 92 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁)) |
94 | | foima 6689 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) |
96 | 91, 95 | eqtr3d 2781 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁))) = (1...𝑁)) |
97 | 96 | fneq2d 6523 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})) Fn (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁))) ↔ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})) Fn (1...𝑁))) |
98 | 55, 97 | mpbid 231 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})) Fn (1...𝑁)) |
99 | 98 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) → ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})) Fn (1...𝑁)) |
100 | | ovexd 7303 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) → (1...𝑁) ∈ V) |
101 | | inidm 4157 |
. . . . . . . . . 10
⊢
((1...𝑁) ∩
(1...𝑁)) = (1...𝑁) |
102 | | eqidd 2740 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) = ((1st ‘(1st
‘𝑇))‘𝑛)) |
103 | | imaundi 6050 |
. . . . . . . . . . . . . . . . . 18
⊢
((2nd ‘(1st ‘𝑇)) “ ({𝑀} ∪ ((𝑀 + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ {𝑀}) ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) |
104 | | fzpred 13286 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑀...𝑁) = ({𝑀} ∪ ((𝑀 + 1)...𝑁))) |
105 | 82, 104 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑀...𝑁) = ({𝑀} ∪ ((𝑀 + 1)...𝑁))) |
106 | 105 | imaeq2d 5966 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ ({𝑀} ∪ ((𝑀 + 1)...𝑁)))) |
107 | | f1ofn 6713 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑇)) Fn (1...𝑁)) |
108 | 13, 107 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)) Fn (1...𝑁)) |
109 | | fnsnfv 6841 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((2nd ‘(1st ‘𝑇)) Fn (1...𝑁) ∧ 𝑀 ∈ (1...𝑁)) → {((2nd
‘(1st ‘𝑇))‘𝑀)} = ((2nd ‘(1st
‘𝑇)) “ {𝑀})) |
110 | 108, 26, 109 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → {((2nd
‘(1st ‘𝑇))‘𝑀)} = ((2nd ‘(1st
‘𝑇)) “ {𝑀})) |
111 | 110 | uneq1d 4100 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ({((2nd
‘(1st ‘𝑇))‘𝑀)} ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ {𝑀}) ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
112 | 103, 106,
111 | 3eqtr4a 2805 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)) = ({((2nd
‘(1st ‘𝑇))‘𝑀)} ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
113 | 112 | xpeq1d 5617 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}) = (({((2nd
‘(1st ‘𝑇))‘𝑀)} ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) × {0})) |
114 | | xpundir 5655 |
. . . . . . . . . . . . . . . 16
⊢
(({((2nd ‘(1st ‘𝑇))‘𝑀)} ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) × {0}) = (({((2nd
‘(1st ‘𝑇))‘𝑀)} × {0}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) |
115 | 113, 114 | eqtrdi 2795 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}) = (({((2nd
‘(1st ‘𝑇))‘𝑀)} × {0}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) |
116 | 115 | uneq2d 4101 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(({((2nd ‘(1st ‘𝑇))‘𝑀)} × {0}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))) |
117 | | un12 4105 |
. . . . . . . . . . . . . 14
⊢
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(({((2nd ‘(1st ‘𝑇))‘𝑀)} × {0}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) = (({((2nd
‘(1st ‘𝑇))‘𝑀)} × {0}) ∪ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) |
118 | 116, 117 | eqtrdi 2795 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})) = (({((2nd
‘(1st ‘𝑇))‘𝑀)} × {0}) ∪ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))) |
119 | 118 | fveq1d 6770 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘𝑛) = ((({((2nd
‘(1st ‘𝑇))‘𝑀)} × {0}) ∪ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛)) |
120 | 119 | ad2antrr 722 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘𝑛) = ((({((2nd
‘(1st ‘𝑇))‘𝑀)} × {0}) ∪ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛)) |
121 | | fnconstg 6658 |
. . . . . . . . . . . . . . . . 17
⊢ (0 ∈
V → (((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) |
122 | 36, 121 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) |
123 | 35, 122 | pm3.2i 470 |
. . . . . . . . . . . . . . 15
⊢
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn
((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∧ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) |
124 | | imain 6515 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
◡(2nd ‘(1st
‘𝑇)) →
((2nd ‘(1st ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
125 | 42, 124 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
126 | 74 | zred 12408 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑀 − 1) ∈ ℝ) |
127 | | peano2re 11131 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈
ℝ) |
128 | 46, 127 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑀 + 1) ∈ ℝ) |
129 | 46 | ltp1d 11888 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 < (𝑀 + 1)) |
130 | 126, 46, 128, 47, 129 | lttrd 11119 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑀 − 1) < (𝑀 + 1)) |
131 | | fzdisj 13265 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 − 1) < (𝑀 + 1) → ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁)) = ∅) |
132 | 130, 131 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁)) = ∅) |
133 | 132 | imaeq2d 5966 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁))) = ((2nd
‘(1st ‘𝑇)) “ ∅)) |
134 | 133, 51 | eqtrdi 2795 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁))) = ∅) |
135 | 125, 134 | eqtr3d 2781 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅) |
136 | | fnun 6541 |
. . . . . . . . . . . . . . 15
⊢
((((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn
((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∧ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) ∧ (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅) → ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
137 | 123, 135,
136 | sylancr 586 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
138 | | imaundi 6050 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘(1st ‘𝑇)) “ ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) |
139 | | imadif 6514 |
. . . . . . . . . . . . . . . . . 18
⊢ (Fun
◡(2nd ‘(1st
‘𝑇)) →
((2nd ‘(1st ‘𝑇)) “ ((1...𝑁) ∖ {𝑀})) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) ∖ ((2nd
‘(1st ‘𝑇)) “ {𝑀}))) |
140 | 42, 139 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...𝑁) ∖ {𝑀})) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) ∖ ((2nd
‘(1st ‘𝑇)) “ {𝑀}))) |
141 | | fzsplit 13264 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ (1...𝑁) → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) |
142 | 26, 141 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) |
143 | 142 | difeq1d 4060 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((1...𝑁) ∖ {𝑀}) = (((1...𝑀) ∪ ((𝑀 + 1)...𝑁)) ∖ {𝑀})) |
144 | | difundir 4219 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((1...𝑀) ∪
((𝑀 + 1)...𝑁)) ∖ {𝑀}) = (((1...𝑀) ∖ {𝑀}) ∪ (((𝑀 + 1)...𝑁) ∖ {𝑀})) |
145 | | fzsplit2 13263 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑀 − 1) + 1) ∈
(ℤ≥‘1) ∧ 𝑀 ∈ (ℤ≥‘(𝑀 − 1))) → (1...𝑀) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑀))) |
146 | 72, 78, 145 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (1...𝑀) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑀))) |
147 | 58 | oveq1d 7283 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (((𝑀 − 1) + 1)...𝑀) = (𝑀...𝑀)) |
148 | | fzsn 13280 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀}) |
149 | 45, 148 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝑀...𝑀) = {𝑀}) |
150 | 147, 149 | eqtrd 2779 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (((𝑀 − 1) + 1)...𝑀) = {𝑀}) |
151 | 150 | uneq2d 4101 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑀)) = ((1...(𝑀 − 1)) ∪ {𝑀})) |
152 | 146, 151 | eqtrd 2779 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (1...𝑀) = ((1...(𝑀 − 1)) ∪ {𝑀})) |
153 | 152 | difeq1d 4060 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((1...𝑀) ∖ {𝑀}) = (((1...(𝑀 − 1)) ∪ {𝑀}) ∖ {𝑀})) |
154 | | difun2 4419 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((1...(𝑀 −
1)) ∪ {𝑀}) ∖
{𝑀}) = ((1...(𝑀 − 1)) ∖ {𝑀}) |
155 | 126, 46 | ltnled 11105 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((𝑀 − 1) < 𝑀 ↔ ¬ 𝑀 ≤ (𝑀 − 1))) |
156 | 47, 155 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ¬ 𝑀 ≤ (𝑀 − 1)) |
157 | | elfzle2 13242 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑀 ∈ (1...(𝑀 − 1)) → 𝑀 ≤ (𝑀 − 1)) |
158 | 156, 157 | nsyl 140 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ¬ 𝑀 ∈ (1...(𝑀 − 1))) |
159 | | difsn 4736 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
𝑀 ∈ (1...(𝑀 − 1)) → ((1...(𝑀 − 1)) ∖ {𝑀}) = (1...(𝑀 − 1))) |
160 | 158, 159 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((1...(𝑀 − 1)) ∖ {𝑀}) = (1...(𝑀 − 1))) |
161 | 154, 160 | eqtrid 2791 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (((1...(𝑀 − 1)) ∪ {𝑀}) ∖ {𝑀}) = (1...(𝑀 − 1))) |
162 | 153, 161 | eqtrd 2779 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((1...𝑀) ∖ {𝑀}) = (1...(𝑀 − 1))) |
163 | 46, 128 | ltnled 11105 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀)) |
164 | 129, 163 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ¬ (𝑀 + 1) ≤ 𝑀) |
165 | | elfzle1 13241 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 ∈ ((𝑀 + 1)...𝑁) → (𝑀 + 1) ≤ 𝑀) |
166 | 164, 165 | nsyl 140 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ¬ 𝑀 ∈ ((𝑀 + 1)...𝑁)) |
167 | | difsn 4736 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
𝑀 ∈ ((𝑀 + 1)...𝑁) → (((𝑀 + 1)...𝑁) ∖ {𝑀}) = ((𝑀 + 1)...𝑁)) |
168 | 166, 167 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (((𝑀 + 1)...𝑁) ∖ {𝑀}) = ((𝑀 + 1)...𝑁)) |
169 | 162, 168 | uneq12d 4102 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((1...𝑀) ∖ {𝑀}) ∪ (((𝑀 + 1)...𝑁) ∖ {𝑀})) = ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁))) |
170 | 144, 169 | eqtrid 2791 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((1...𝑀) ∪ ((𝑀 + 1)...𝑁)) ∖ {𝑀}) = ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁))) |
171 | 143, 170 | eqtrd 2779 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((1...𝑁) ∖ {𝑀}) = ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁))) |
172 | 171 | imaeq2d 5966 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...𝑁) ∖ {𝑀})) = ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁)))) |
173 | 110 | eqcomd 2745 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ {𝑀}) = {((2nd
‘(1st ‘𝑇))‘𝑀)}) |
174 | 95, 173 | difeq12d 4062 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) ∖ ((2nd
‘(1st ‘𝑇)) “ {𝑀})) = ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)})) |
175 | 140, 172,
174 | 3eqtr3d 2787 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁))) = ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)})) |
176 | 138, 175 | eqtr3id 2793 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)})) |
177 | 176 | fneq2d 6523 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) ↔ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)}))) |
178 | 137, 177 | mpbid 231 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)})) |
179 | | eldifsn 4725 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)}) ↔ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀))) |
180 | 179 | biimpri 227 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) → 𝑛 ∈ ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)})) |
181 | 180 | ancoms 458 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ≠ ((2nd
‘(1st ‘𝑇))‘𝑀) ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)})) |
182 | | disjdif 4410 |
. . . . . . . . . . . . . 14
⊢
({((2nd ‘(1st ‘𝑇))‘𝑀)} ∩ ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)})) = ∅ |
183 | | fnconstg 6658 |
. . . . . . . . . . . . . . . 16
⊢ (0 ∈
V → ({((2nd ‘(1st ‘𝑇))‘𝑀)} × {0}) Fn {((2nd
‘(1st ‘𝑇))‘𝑀)}) |
184 | 36, 183 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
({((2nd ‘(1st ‘𝑇))‘𝑀)} × {0}) Fn {((2nd
‘(1st ‘𝑇))‘𝑀)} |
185 | | fvun2 6854 |
. . . . . . . . . . . . . . 15
⊢
((({((2nd ‘(1st ‘𝑇))‘𝑀)} × {0}) Fn {((2nd
‘(1st ‘𝑇))‘𝑀)} ∧ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)}) ∧ (({((2nd
‘(1st ‘𝑇))‘𝑀)} ∩ ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)})) = ∅ ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)}))) → ((({((2nd
‘(1st ‘𝑇))‘𝑀)} × {0}) ∪ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)) |
186 | 184, 185 | mp3an1 1446 |
. . . . . . . . . . . . . 14
⊢
((((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)}) ∧ (({((2nd
‘(1st ‘𝑇))‘𝑀)} ∩ ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)})) = ∅ ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)}))) → ((({((2nd
‘(1st ‘𝑇))‘𝑀)} × {0}) ∪ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)) |
187 | 182, 186 | mpanr1 699 |
. . . . . . . . . . . . 13
⊢
((((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)}) ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)})) → ((({((2nd
‘(1st ‘𝑇))‘𝑀)} × {0}) ∪ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)) |
188 | 178, 181,
187 | syl2an 595 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀) ∧ 𝑛 ∈ (1...𝑁))) → ((({((2nd
‘(1st ‘𝑇))‘𝑀)} × {0}) ∪ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)) |
189 | 188 | anassrs 467 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → ((({((2nd
‘(1st ‘𝑇))‘𝑀)} × {0}) ∪ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)) |
190 | 120, 189 | eqtrd 2779 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘𝑛) = (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)) |
191 | 32, 99, 100, 100, 101, 102, 190 | ofval 7535 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛) = (((1st ‘(1st
‘𝑇))‘𝑛) + (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))) |
192 | | fnconstg 6658 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
V → (((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) Fn ((2nd
‘(1st ‘𝑇)) “ (1...𝑀))) |
193 | 33, 192 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) Fn ((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) |
194 | 193, 122 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢
((((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) Fn ((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) ∧ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) |
195 | | imain 6515 |
. . . . . . . . . . . . . . 15
⊢ (Fun
◡(2nd ‘(1st
‘𝑇)) →
((2nd ‘(1st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) ∩ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
196 | 42, 195 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) ∩ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
197 | | fzdisj 13265 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅) |
198 | 129, 197 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅) |
199 | 198 | imaeq2d 5966 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ((2nd
‘(1st ‘𝑇)) “ ∅)) |
200 | 199, 51 | eqtrdi 2795 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ∅) |
201 | 196, 200 | eqtr3d 2781 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) ∩ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅) |
202 | | fnun 6541 |
. . . . . . . . . . . . 13
⊢
((((((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) Fn ((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) ∧ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) ∧ (((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) ∩ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅) → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
203 | 194, 201,
202 | sylancr 586 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
204 | 142 | imaeq2d 5966 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = ((2nd ‘(1st
‘𝑇)) “
((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))) |
205 | | imaundi 6050 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘(1st ‘𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) |
206 | 204, 205 | eqtrdi 2795 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
207 | 206, 95 | eqtr3d 2781 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = (1...𝑁)) |
208 | 207 | fneq2d 6523 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) ↔ ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))) |
209 | 203, 208 | mpbid 231 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
210 | 209 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
211 | | imaundi 6050 |
. . . . . . . . . . . . . . . . . 18
⊢
((2nd ‘(1st ‘𝑇)) “ ((1...(𝑀 − 1)) ∪ {𝑀})) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ {𝑀})) |
212 | 152 | imaeq2d 5966 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) = ((2nd ‘(1st
‘𝑇)) “
((1...(𝑀 − 1)) ∪
{𝑀}))) |
213 | 110 | uneq2d 4101 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ {((2nd
‘(1st ‘𝑇))‘𝑀)}) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ {𝑀}))) |
214 | 211, 212,
213 | 3eqtr4a 2805 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ {((2nd
‘(1st ‘𝑇))‘𝑀)})) |
215 | 214 | xpeq1d 5617 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) = ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ {((2nd
‘(1st ‘𝑇))‘𝑀)}) × {1})) |
216 | | xpundir 5655 |
. . . . . . . . . . . . . . . 16
⊢
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ {((2nd
‘(1st ‘𝑇))‘𝑀)}) × {1}) = ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
({((2nd ‘(1st ‘𝑇))‘𝑀)} × {1})) |
217 | 215, 216 | eqtrdi 2795 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) = ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
({((2nd ‘(1st ‘𝑇))‘𝑀)} × {1}))) |
218 | 217 | uneq1d 4100 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) = (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
({((2nd ‘(1st ‘𝑇))‘𝑀)} × {1})) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) |
219 | | un23 4106 |
. . . . . . . . . . . . . . 15
⊢
(((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
({((2nd ‘(1st ‘𝑇))‘𝑀)} × {1})) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) = (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) ∪ ({((2nd
‘(1st ‘𝑇))‘𝑀)} × {1})) |
220 | 219 | equncomi 4093 |
. . . . . . . . . . . . . 14
⊢
(((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
({((2nd ‘(1st ‘𝑇))‘𝑀)} × {1})) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) = (({((2nd
‘(1st ‘𝑇))‘𝑀)} × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) |
221 | 218, 220 | eqtrdi 2795 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) = (({((2nd
‘(1st ‘𝑇))‘𝑀)} × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))) |
222 | 221 | fveq1d 6770 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛) = ((({((2nd
‘(1st ‘𝑇))‘𝑀)} × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛)) |
223 | 222 | ad2antrr 722 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛) = ((({((2nd
‘(1st ‘𝑇))‘𝑀)} × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛)) |
224 | | fnconstg 6658 |
. . . . . . . . . . . . . . . 16
⊢ (1 ∈
V → ({((2nd ‘(1st ‘𝑇))‘𝑀)} × {1}) Fn {((2nd
‘(1st ‘𝑇))‘𝑀)}) |
225 | 33, 224 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
({((2nd ‘(1st ‘𝑇))‘𝑀)} × {1}) Fn {((2nd
‘(1st ‘𝑇))‘𝑀)} |
226 | | fvun2 6854 |
. . . . . . . . . . . . . . 15
⊢
((({((2nd ‘(1st ‘𝑇))‘𝑀)} × {1}) Fn {((2nd
‘(1st ‘𝑇))‘𝑀)} ∧ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)}) ∧ (({((2nd
‘(1st ‘𝑇))‘𝑀)} ∩ ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)})) = ∅ ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)}))) → ((({((2nd
‘(1st ‘𝑇))‘𝑀)} × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)) |
227 | 225, 226 | mp3an1 1446 |
. . . . . . . . . . . . . 14
⊢
((((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)}) ∧ (({((2nd
‘(1st ‘𝑇))‘𝑀)} ∩ ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)})) = ∅ ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)}))) → ((({((2nd
‘(1st ‘𝑇))‘𝑀)} × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)) |
228 | 182, 227 | mpanr1 699 |
. . . . . . . . . . . . 13
⊢
((((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)}) ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)})) → ((({((2nd
‘(1st ‘𝑇))‘𝑀)} × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)) |
229 | 178, 181,
228 | syl2an 595 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀) ∧ 𝑛 ∈ (1...𝑁))) → ((({((2nd
‘(1st ‘𝑇))‘𝑀)} × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)) |
230 | 229 | anassrs 467 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → ((({((2nd
‘(1st ‘𝑇))‘𝑀)} × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)) |
231 | 223, 230 | eqtrd 2779 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛) = (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)) |
232 | 32, 210, 100, 100, 101, 102, 231 | ofval 7535 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((1st ‘(1st
‘𝑇))‘𝑛) + (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))) |
233 | 191, 232 | eqtr4d 2782 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛) = (((1st ‘(1st
‘𝑇))
∘f + ((((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛)) |
234 | 233 | an32s 648 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) → (((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛) = (((1st ‘(1st
‘𝑇))
∘f + ((((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛)) |
235 | 234 | anasss 466 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀))) → (((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛) = (((1st ‘(1st
‘𝑇))
∘f + ((((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛)) |
236 | | fveq2 6768 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 𝑇 → (2nd ‘𝑡) = (2nd ‘𝑇)) |
237 | 236 | breq2d 5090 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 𝑇 → (𝑦 < (2nd ‘𝑡) ↔ 𝑦 < (2nd ‘𝑇))) |
238 | 237 | ifbid 4487 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑇 → if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1))) |
239 | 238 | csbeq1d 3840 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
240 | | 2fveq3 6773 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 𝑇 → (1st
‘(1st ‘𝑡)) = (1st ‘(1st
‘𝑇))) |
241 | | 2fveq3 6773 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = 𝑇 → (2nd
‘(1st ‘𝑡)) = (2nd ‘(1st
‘𝑇))) |
242 | 241 | imaeq1d 5965 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...𝑗))) |
243 | 242 | xpeq1d 5617 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1})) |
244 | 241 | imaeq1d 5965 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ ((𝑗 + 1)...𝑁))) |
245 | 244 | xpeq1d 5617 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) |
246 | 243, 245 | uneq12d 4102 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 𝑇 → ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) |
247 | 240, 246 | oveq12d 7286 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑇 → ((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
248 | 247 | csbeq2dv 3843 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
249 | 239, 248 | eqtrd 2779 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
250 | 249 | mpteq2dv 5180 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
251 | 250 | eqeq2d 2750 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘f + ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
252 | 251, 3 | elrab2 3628 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ 𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
253 | 252 | simprbi 496 |
. . . . . . . . . 10
⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
254 | 1, 253 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
255 | | breq1 5081 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑀 − 2) → (𝑦 < (2nd ‘𝑇) ↔ (𝑀 − 2) < (2nd
‘𝑇))) |
256 | 255 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 2)) → (𝑦 < (2nd ‘𝑇) ↔ (𝑀 − 2) < (2nd
‘𝑇))) |
257 | | oveq1 7275 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑀 − 2) → (𝑦 + 1) = ((𝑀 − 2) + 1)) |
258 | | sub1m1 12208 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℂ → ((𝑀 − 1) − 1) = (𝑀 − 2)) |
259 | 56, 258 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑀 − 1) − 1) = (𝑀 − 2)) |
260 | 259 | oveq1d 7283 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝑀 − 1) − 1) + 1) = ((𝑀 − 2) +
1)) |
261 | 74 | zcnd 12409 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑀 − 1) ∈ ℂ) |
262 | | npcan1 11383 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 − 1) ∈ ℂ
→ (((𝑀 − 1)
− 1) + 1) = (𝑀
− 1)) |
263 | 261, 262 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝑀 − 1) − 1) + 1) = (𝑀 − 1)) |
264 | 260, 263 | eqtr3d 2781 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑀 − 2) + 1) = (𝑀 − 1)) |
265 | 257, 264 | sylan9eqr 2801 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 2)) → (𝑦 + 1) = (𝑀 − 1)) |
266 | 256, 265 | ifbieq2d 4490 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 2)) → if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) = if((𝑀 − 2) < (2nd
‘𝑇), 𝑦, (𝑀 − 1))) |
267 | 18 | nncnd 11972 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2nd
‘𝑇) ∈
ℂ) |
268 | | add1p1 12207 |
. . . . . . . . . . . . . . . . 17
⊢
((2nd ‘𝑇) ∈ ℂ → (((2nd
‘𝑇) + 1) + 1) =
((2nd ‘𝑇)
+ 2)) |
269 | 267, 268 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((2nd
‘𝑇) + 1) + 1) =
((2nd ‘𝑇)
+ 2)) |
270 | 269, 66 | eqbrtrrd 5102 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2nd
‘𝑇) + 2) ≤ 𝑀) |
271 | 18 | nnred 11971 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2nd
‘𝑇) ∈
ℝ) |
272 | | 2re 12030 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℝ |
273 | | leaddsub 11434 |
. . . . . . . . . . . . . . . . . 18
⊢
(((2nd ‘𝑇) ∈ ℝ ∧ 2 ∈ ℝ
∧ 𝑀 ∈ ℝ)
→ (((2nd ‘𝑇) + 2) ≤ 𝑀 ↔ (2nd ‘𝑇) ≤ (𝑀 − 2))) |
274 | 272, 273 | mp3an2 1447 |
. . . . . . . . . . . . . . . . 17
⊢
(((2nd ‘𝑇) ∈ ℝ ∧ 𝑀 ∈ ℝ) → (((2nd
‘𝑇) + 2) ≤ 𝑀 ↔ (2nd
‘𝑇) ≤ (𝑀 − 2))) |
275 | 271, 46, 274 | syl2anc 583 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((2nd
‘𝑇) + 2) ≤ 𝑀 ↔ (2nd
‘𝑇) ≤ (𝑀 − 2))) |
276 | 59, 46 | posdifd 11545 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (1 < 𝑀 ↔ 0 < (𝑀 − 1))) |
277 | 67, 276 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 0 < (𝑀 − 1)) |
278 | | elnnz 12312 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 − 1) ∈ ℕ
↔ ((𝑀 − 1)
∈ ℤ ∧ 0 < (𝑀 − 1))) |
279 | 74, 277, 278 | sylanbrc 582 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑀 − 1) ∈ ℕ) |
280 | | nnm1nn0 12257 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 − 1) ∈ ℕ
→ ((𝑀 − 1)
− 1) ∈ ℕ0) |
281 | 279, 280 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑀 − 1) − 1) ∈
ℕ0) |
282 | 259, 281 | eqeltrrd 2841 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑀 − 2) ∈
ℕ0) |
283 | 282 | nn0red 12277 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑀 − 2) ∈ ℝ) |
284 | 271, 283 | lenltd 11104 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2nd
‘𝑇) ≤ (𝑀 − 2) ↔ ¬ (𝑀 − 2) < (2nd
‘𝑇))) |
285 | 275, 284 | bitrd 278 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2nd
‘𝑇) + 2) ≤ 𝑀 ↔ ¬ (𝑀 − 2) < (2nd
‘𝑇))) |
286 | 270, 285 | mpbid 231 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ¬ (𝑀 − 2) < (2nd
‘𝑇)) |
287 | 286 | iffalsed 4475 |
. . . . . . . . . . . . 13
⊢ (𝜑 → if((𝑀 − 2) < (2nd
‘𝑇), 𝑦, (𝑀 − 1)) = (𝑀 − 1)) |
288 | 287 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 2)) → if((𝑀 − 2) < (2nd
‘𝑇), 𝑦, (𝑀 − 1)) = (𝑀 − 1)) |
289 | 266, 288 | eqtrd 2779 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 2)) → if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) = (𝑀 − 1)) |
290 | 289 | csbeq1d 3840 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 2)) → ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋(𝑀 − 1) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
291 | | oveq2 7276 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = (𝑀 − 1) → (1...𝑗) = (1...(𝑀 − 1))) |
292 | 291 | imaeq2d 5966 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = (𝑀 − 1) → ((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...(𝑀 −
1)))) |
293 | 292 | xpeq1d 5617 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = (𝑀 − 1) → (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1})) |
294 | 293 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1})) |
295 | | oveq1 7275 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = (𝑀 − 1) → (𝑗 + 1) = ((𝑀 − 1) + 1)) |
296 | 295, 58 | sylan9eqr 2801 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (𝑗 + 1) = 𝑀) |
297 | 296 | oveq1d 7283 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((𝑗 + 1)...𝑁) = (𝑀...𝑁)) |
298 | 297 | imaeq2d 5966 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ (𝑀...𝑁))) |
299 | 298 | xpeq1d 5617 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})) |
300 | 294, 299 | uneq12d 4102 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}))) |
301 | 300 | oveq2d 7284 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))) |
302 | 74, 301 | csbied 3874 |
. . . . . . . . . . 11
⊢ (𝜑 → ⦋(𝑀 − 1) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))) |
303 | 302 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 2)) → ⦋(𝑀 − 1) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))) |
304 | 290, 303 | eqtrd 2779 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 2)) → ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))) |
305 | | poimir.0 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℕ) |
306 | | nnm1nn0 12257 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
307 | 305, 306 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 − 1) ∈
ℕ0) |
308 | 305 | nnred 11971 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℝ) |
309 | 46 | lem1d 11891 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀 − 1) ≤ 𝑀) |
310 | | elfzle2 13242 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ((((2nd
‘𝑇) + 1) + 1)...𝑁) → 𝑀 ≤ 𝑁) |
311 | 25, 310 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ≤ 𝑁) |
312 | 126, 46, 308, 309, 311 | letrd 11115 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀 − 1) ≤ 𝑁) |
313 | 126, 308,
59, 312 | lesub1dd 11574 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑀 − 1) − 1) ≤ (𝑁 − 1)) |
314 | 259, 313 | eqbrtrrd 5102 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 − 2) ≤ (𝑁 − 1)) |
315 | | elfz2nn0 13329 |
. . . . . . . . . 10
⊢ ((𝑀 − 2) ∈ (0...(𝑁 − 1)) ↔ ((𝑀 − 2) ∈
ℕ0 ∧ (𝑁 − 1) ∈ ℕ0 ∧
(𝑀 − 2) ≤ (𝑁 − 1))) |
316 | 282, 307,
314, 315 | syl3anbrc 1341 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 − 2) ∈ (0...(𝑁 − 1))) |
317 | | ovexd 7303 |
. . . . . . . . 9
⊢ (𝜑 → ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}))) ∈ V) |
318 | 254, 304,
316, 317 | fvmptd 6876 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘(𝑀 − 2)) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))) |
319 | 318 | fveq1d 6770 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘(𝑀 − 2))‘𝑛) = (((1st ‘(1st
‘𝑇))
∘f + ((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛)) |
320 | 319 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀))) → ((𝐹‘(𝑀 − 2))‘𝑛) = (((1st ‘(1st
‘𝑇))
∘f + ((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛)) |
321 | | breq1 5081 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑀 − 1) → (𝑦 < (2nd ‘𝑇) ↔ (𝑀 − 1) < (2nd
‘𝑇))) |
322 | 321 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → (𝑦 < (2nd ‘𝑇) ↔ (𝑀 − 1) < (2nd
‘𝑇))) |
323 | | oveq1 7275 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑀 − 1) → (𝑦 + 1) = ((𝑀 − 1) + 1)) |
324 | 323, 58 | sylan9eqr 2801 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → (𝑦 + 1) = 𝑀) |
325 | 322, 324 | ifbieq2d 4490 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) = if((𝑀 − 1) < (2nd
‘𝑇), 𝑦, 𝑀)) |
326 | 61 | lep1d 11889 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2nd
‘𝑇) + 1) ≤
(((2nd ‘𝑇)
+ 1) + 1)) |
327 | 61, 60, 46, 326, 66 | letrd 11115 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2nd
‘𝑇) + 1) ≤ 𝑀) |
328 | | 1re 10959 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℝ |
329 | | leaddsub 11434 |
. . . . . . . . . . . . . . . . . 18
⊢
(((2nd ‘𝑇) ∈ ℝ ∧ 1 ∈ ℝ
∧ 𝑀 ∈ ℝ)
→ (((2nd ‘𝑇) + 1) ≤ 𝑀 ↔ (2nd ‘𝑇) ≤ (𝑀 − 1))) |
330 | 328, 329 | mp3an2 1447 |
. . . . . . . . . . . . . . . . 17
⊢
(((2nd ‘𝑇) ∈ ℝ ∧ 𝑀 ∈ ℝ) → (((2nd
‘𝑇) + 1) ≤ 𝑀 ↔ (2nd
‘𝑇) ≤ (𝑀 − 1))) |
331 | 271, 46, 330 | syl2anc 583 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((2nd
‘𝑇) + 1) ≤ 𝑀 ↔ (2nd
‘𝑇) ≤ (𝑀 − 1))) |
332 | 271, 126 | lenltd 11104 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2nd
‘𝑇) ≤ (𝑀 − 1) ↔ ¬ (𝑀 − 1) < (2nd
‘𝑇))) |
333 | 331, 332 | bitrd 278 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2nd
‘𝑇) + 1) ≤ 𝑀 ↔ ¬ (𝑀 − 1) < (2nd
‘𝑇))) |
334 | 327, 333 | mpbid 231 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ¬ (𝑀 − 1) < (2nd
‘𝑇)) |
335 | 334 | iffalsed 4475 |
. . . . . . . . . . . . 13
⊢ (𝜑 → if((𝑀 − 1) < (2nd
‘𝑇), 𝑦, 𝑀) = 𝑀) |
336 | 335 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → if((𝑀 − 1) < (2nd
‘𝑇), 𝑦, 𝑀) = 𝑀) |
337 | 325, 336 | eqtrd 2779 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) = 𝑀) |
338 | 337 | csbeq1d 3840 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑀 / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
339 | | oveq2 7276 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑀 → (1...𝑗) = (1...𝑀)) |
340 | 339 | imaeq2d 5966 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑀 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...𝑀))) |
341 | 340 | xpeq1d 5617 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑀 → (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1})) |
342 | | oveq1 7275 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑀 → (𝑗 + 1) = (𝑀 + 1)) |
343 | 342 | oveq1d 7283 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑀 → ((𝑗 + 1)...𝑁) = ((𝑀 + 1)...𝑁)) |
344 | 343 | imaeq2d 5966 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑀 → ((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ ((𝑀 + 1)...𝑁))) |
345 | 344 | xpeq1d 5617 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑀 → (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) |
346 | 341, 345 | uneq12d 4102 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑀 → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) |
347 | 346 | oveq2d 7284 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑀 → ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))) |
348 | 347 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 = 𝑀) → ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))) |
349 | 25, 348 | csbied 3874 |
. . . . . . . . . . 11
⊢ (𝜑 → ⦋𝑀 / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))) |
350 | 349 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋𝑀 / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))) |
351 | 338, 350 | eqtrd 2779 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))) |
352 | 279 | nnnn0d 12276 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 − 1) ∈
ℕ0) |
353 | 46, 308, 59, 311 | lesub1dd 11574 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 − 1) ≤ (𝑁 − 1)) |
354 | | elfz2nn0 13329 |
. . . . . . . . . 10
⊢ ((𝑀 − 1) ∈ (0...(𝑁 − 1)) ↔ ((𝑀 − 1) ∈
ℕ0 ∧ (𝑁 − 1) ∈ ℕ0 ∧
(𝑀 − 1) ≤ (𝑁 − 1))) |
355 | 352, 307,
353, 354 | syl3anbrc 1341 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 − 1) ∈ (0...(𝑁 − 1))) |
356 | | ovexd 7303 |
. . . . . . . . 9
⊢ (𝜑 → ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) ∈ V) |
357 | 254, 351,
355, 356 | fvmptd 6876 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘(𝑀 − 1)) = ((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))) |
358 | 357 | fveq1d 6770 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘(𝑀 − 1))‘𝑛) = (((1st ‘(1st
‘𝑇))
∘f + ((((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛)) |
359 | 358 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀))) → ((𝐹‘(𝑀 − 1))‘𝑛) = (((1st ‘(1st
‘𝑇))
∘f + ((((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛)) |
360 | 235, 320,
359 | 3eqtr4d 2789 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀))) → ((𝐹‘(𝑀 − 2))‘𝑛) = ((𝐹‘(𝑀 − 1))‘𝑛)) |
361 | 360 | expr 456 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀) → ((𝐹‘(𝑀 − 2))‘𝑛) = ((𝐹‘(𝑀 − 1))‘𝑛))) |
362 | 361 | necon1d 2966 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛) → 𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑀))) |
363 | | elmapi 8611 |
. . . . . . . . . . 11
⊢
((1st ‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
364 | 29, 363 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
365 | 364, 27 | ffvelrnd 6956 |
. . . . . . . . 9
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) ∈ (0..^𝐾)) |
366 | | elfzonn0 13413 |
. . . . . . . . 9
⊢
(((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) ∈ (0..^𝐾) → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) ∈
ℕ0) |
367 | 365, 366 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) ∈
ℕ0) |
368 | 367 | nn0red 12277 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) ∈ ℝ) |
369 | 368 | ltp1d 11888 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) < (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) + 1)) |
370 | 368, 369 | ltned 11094 |
. . . . . 6
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) ≠ (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) + 1)) |
371 | 318 | fveq1d 6770 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘(𝑀 − 2))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = (((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘((2nd
‘(1st ‘𝑇))‘𝑀))) |
372 | | ovexd 7303 |
. . . . . . . . 9
⊢ (𝜑 → (1...𝑁) ∈ V) |
373 | | eqidd 2740 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((2nd
‘(1st ‘𝑇))‘𝑀) ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = ((1st ‘(1st
‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀))) |
374 | | fzss1 13277 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈
(ℤ≥‘1) → (𝑀...𝑁) ⊆ (1...𝑁)) |
375 | 71, 374 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀...𝑁) ⊆ (1...𝑁)) |
376 | | eluzfz1 13245 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁)) |
377 | 82, 376 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁)) |
378 | | fnfvima 7103 |
. . . . . . . . . . . . 13
⊢
(((2nd ‘(1st ‘𝑇)) Fn (1...𝑁) ∧ (𝑀...𝑁) ⊆ (1...𝑁) ∧ 𝑀 ∈ (𝑀...𝑁)) → ((2nd
‘(1st ‘𝑇))‘𝑀) ∈ ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁))) |
379 | 108, 375,
377, 378 | syl3anc 1369 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇))‘𝑀) ∈ ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁))) |
380 | | fvun2 6854 |
. . . . . . . . . . . . 13
⊢
(((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn
((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∧ (((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)) ∧ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁))) = ∅ ∧ ((2nd
‘(1st ‘𝑇))‘𝑀) ∈ ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)))) → (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = ((((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})‘((2nd
‘(1st ‘𝑇))‘𝑀))) |
381 | 35, 38, 380 | mp3an12 1449 |
. . . . . . . . . . . 12
⊢
(((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁))) = ∅ ∧ ((2nd
‘(1st ‘𝑇))‘𝑀) ∈ ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁))) → (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = ((((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})‘((2nd
‘(1st ‘𝑇))‘𝑀))) |
382 | 53, 379, 381 | syl2anc 583 |
. . . . . . . . . . 11
⊢ (𝜑 → (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = ((((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})‘((2nd
‘(1st ‘𝑇))‘𝑀))) |
383 | 36 | fvconst2 7073 |
. . . . . . . . . . . 12
⊢
(((2nd ‘(1st ‘𝑇))‘𝑀) ∈ ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)) → ((((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})‘((2nd
‘(1st ‘𝑇))‘𝑀)) = 0) |
384 | 379, 383 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})‘((2nd
‘(1st ‘𝑇))‘𝑀)) = 0) |
385 | 382, 384 | eqtrd 2779 |
. . . . . . . . . 10
⊢ (𝜑 → (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = 0) |
386 | 385 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((2nd
‘(1st ‘𝑇))‘𝑀) ∈ (1...𝑁)) → (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = 0) |
387 | 31, 98, 372, 372, 101, 373, 386 | ofval 7535 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((2nd
‘(1st ‘𝑇))‘𝑀) ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) + 0)) |
388 | 27, 387 | mpdan 683 |
. . . . . . 7
⊢ (𝜑 → (((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) + 0)) |
389 | 367 | nn0cnd 12278 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) ∈ ℂ) |
390 | 389 | addid1d 11158 |
. . . . . . 7
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) + 0) = ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀))) |
391 | 371, 388,
390 | 3eqtrd 2783 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘(𝑀 − 2))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = ((1st ‘(1st
‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀))) |
392 | 357 | fveq1d 6770 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘(𝑀 − 1))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = (((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘((2nd
‘(1st ‘𝑇))‘𝑀))) |
393 | | fzss2 13278 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (1...𝑀) ⊆ (1...𝑁)) |
394 | 82, 393 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1...𝑀) ⊆ (1...𝑁)) |
395 | | elfz1end 13268 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ ↔ 𝑀 ∈ (1...𝑀)) |
396 | 70, 395 | sylib 217 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ (1...𝑀)) |
397 | | fnfvima 7103 |
. . . . . . . . . . . . 13
⊢
(((2nd ‘(1st ‘𝑇)) Fn (1...𝑁) ∧ (1...𝑀) ⊆ (1...𝑁) ∧ 𝑀 ∈ (1...𝑀)) → ((2nd
‘(1st ‘𝑇))‘𝑀) ∈ ((2nd
‘(1st ‘𝑇)) “ (1...𝑀))) |
398 | 108, 394,
396, 397 | syl3anc 1369 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇))‘𝑀) ∈ ((2nd
‘(1st ‘𝑇)) “ (1...𝑀))) |
399 | | fvun1 6853 |
. . . . . . . . . . . . 13
⊢
(((((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) Fn ((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) ∧ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) ∧ ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) ∩ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅ ∧ ((2nd
‘(1st ‘𝑇))‘𝑀) ∈ ((2nd
‘(1st ‘𝑇)) “ (1...𝑀)))) → (((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1})‘((2nd
‘(1st ‘𝑇))‘𝑀))) |
400 | 193, 122,
399 | mp3an12 1449 |
. . . . . . . . . . . 12
⊢
(((((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) ∩ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅ ∧ ((2nd
‘(1st ‘𝑇))‘𝑀) ∈ ((2nd
‘(1st ‘𝑇)) “ (1...𝑀))) → (((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1})‘((2nd
‘(1st ‘𝑇))‘𝑀))) |
401 | 201, 398,
400 | syl2anc 583 |
. . . . . . . . . . 11
⊢ (𝜑 → (((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1})‘((2nd
‘(1st ‘𝑇))‘𝑀))) |
402 | 33 | fvconst2 7073 |
. . . . . . . . . . . 12
⊢
(((2nd ‘(1st ‘𝑇))‘𝑀) ∈ ((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1})‘((2nd
‘(1st ‘𝑇))‘𝑀)) = 1) |
403 | 398, 402 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1})‘((2nd
‘(1st ‘𝑇))‘𝑀)) = 1) |
404 | 401, 403 | eqtrd 2779 |
. . . . . . . . . 10
⊢ (𝜑 → (((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = 1) |
405 | 404 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((2nd
‘(1st ‘𝑇))‘𝑀) ∈ (1...𝑁)) → (((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = 1) |
406 | 31, 209, 372, 372, 101, 373, 405 | ofval 7535 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((2nd
‘(1st ‘𝑇))‘𝑀) ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) + 1)) |
407 | 27, 406 | mpdan 683 |
. . . . . . 7
⊢ (𝜑 → (((1st
‘(1st ‘𝑇)) ∘f + ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) + 1)) |
408 | 392, 407 | eqtrd 2779 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘(𝑀 − 1))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) + 1)) |
409 | 370, 391,
408 | 3netr4d 3022 |
. . . . 5
⊢ (𝜑 → ((𝐹‘(𝑀 − 2))‘((2nd
‘(1st ‘𝑇))‘𝑀)) ≠ ((𝐹‘(𝑀 − 1))‘((2nd
‘(1st ‘𝑇))‘𝑀))) |
410 | | fveq2 6768 |
. . . . . 6
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘𝑀) → ((𝐹‘(𝑀 − 2))‘𝑛) = ((𝐹‘(𝑀 − 2))‘((2nd
‘(1st ‘𝑇))‘𝑀))) |
411 | | fveq2 6768 |
. . . . . 6
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘𝑀) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘(𝑀 − 1))‘((2nd
‘(1st ‘𝑇))‘𝑀))) |
412 | 410, 411 | neeq12d 3006 |
. . . . 5
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘𝑀) → (((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛) ↔ ((𝐹‘(𝑀 − 2))‘((2nd
‘(1st ‘𝑇))‘𝑀)) ≠ ((𝐹‘(𝑀 − 1))‘((2nd
‘(1st ‘𝑇))‘𝑀)))) |
413 | 409, 412 | syl5ibrcom 246 |
. . . 4
⊢ (𝜑 → (𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑀) → ((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛))) |
414 | 413 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑀) → ((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛))) |
415 | 362, 414 | impbid 211 |
. 2
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛) ↔ 𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑀))) |
416 | 27, 415 | riota5 7255 |
1
⊢ (𝜑 → (℩𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛)) = ((2nd ‘(1st
‘𝑇))‘𝑀)) |