Proof of Theorem poimirlem7
Step | Hyp | Ref
| Expression |
1 | | poimirlem9.1 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ 𝑆) |
2 | | elrabi 3328 |
. . . . . . . . 9
⊢ (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 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(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} |
4 | 2, 3 | eleq2s 2706 |
. . . . . . . 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 7089 |
. . . . . . 7
⊢ (𝑇 ∈ ((((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑇) ∈ (((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
7 | 5, 6 | syl 17 |
. . . . . 6
⊢ (𝜑 → (1st
‘𝑇) ∈
(((0..^𝐾)
↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
8 | | xp2nd 7090 |
. . . . . 6
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑𝑚 (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 6113 |
. . . . . 6
⊢
(2nd ‘(1st ‘𝑇)) ∈ V |
11 | | f1oeq1 6040 |
. . . . . 6
⊢ (𝑓 = (2nd
‘(1st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))) |
12 | 10, 11 | elab 3319 |
. . . . 5
⊢
((2nd ‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
13 | 9, 12 | sylib 207 |
. . . 4
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
14 | | f1of 6050 |
. . . 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 12241 |
. . . . . . . . 9
⊢
((2nd ‘𝑇) ∈ (1...(𝑁 − 1)) → (2nd
‘𝑇) ∈
ℕ) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (2nd
‘𝑇) ∈
ℕ) |
19 | 18 | peano2nnd 10914 |
. . . . . . 7
⊢ (𝜑 → ((2nd
‘𝑇) + 1) ∈
ℕ) |
20 | 19 | peano2nnd 10914 |
. . . . . 6
⊢ (𝜑 → (((2nd
‘𝑇) + 1) + 1) ∈
ℕ) |
21 | | nnuz 11599 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
22 | 20, 21 | syl6eleq 2698 |
. . . . 5
⊢ (𝜑 → (((2nd
‘𝑇) + 1) + 1) ∈
(ℤ≥‘1)) |
23 | | fzss1 12251 |
. . . . 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 3569 |
. . 3
⊢ (𝜑 → 𝑀 ∈ (1...𝑁)) |
27 | 15, 26 | ffvelrnd 6268 |
. 2
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇))‘𝑀) ∈ (1...𝑁)) |
28 | | xp1st 7089 |
. . . . . . . . . . . . 13
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁))) |
29 | 7, 28 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁))) |
30 | | elmapfn 7766 |
. . . . . . . . . . . 12
⊢
((1st ‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑𝑚 (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 9914 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
V |
34 | | fnconstg 6006 |
. . . . . . . . . . . . . . 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 9913 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
V |
37 | | fnconstg 6006 |
. . . . . . . . . . . . . . 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 6056 |
. . . . . . . . . . . . . . . . 17
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd
‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun ◡(2nd ‘(1st
‘𝑇)))) |
41 | 40 | simprbi 479 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ◡(2nd ‘(1st
‘𝑇))) |
42 | 13, 41 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Fun ◡(2nd ‘(1st
‘𝑇))) |
43 | | imain 5888 |
. . . . . . . . . . . . . . 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 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈ ((((2nd
‘𝑇) + 1) + 1)...𝑁) → 𝑀 ∈ ℤ) |
46 | 25, 45 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈ ℤ) |
47 | 46 | zred 11358 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑀 ∈ ℝ) |
48 | 47 | ltm1d 10835 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑀 − 1) < 𝑀) |
49 | | fzdisj 12239 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 − 1) < 𝑀 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑁)) = ∅) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑁)) = ∅) |
51 | 50 | imaeq2d 5385 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ((2nd
‘(1st ‘𝑇)) “ ∅)) |
52 | | ima0 5400 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘(1st ‘𝑇)) “ ∅) =
∅ |
53 | 51, 52 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ∅) |
54 | 44, 53 | eqtr3d 2646 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁))) = ∅) |
55 | | fnun 5911 |
. . . . . . . . . . . . 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 ‘𝑇)) “ (𝑀...𝑁)))) |
56 | 39, 54, 55 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})) Fn (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)))) |
57 | 46 | zcnd 11359 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈ ℂ) |
58 | | npcan1 10334 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈ ℂ → ((𝑀 − 1) + 1) = 𝑀) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑀 − 1) + 1) = 𝑀) |
60 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 1 ∈
ℝ) |
61 | 20 | nnred 10912 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (((2nd
‘𝑇) + 1) + 1) ∈
ℝ) |
62 | 19 | nnred 10912 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((2nd
‘𝑇) + 1) ∈
ℝ) |
63 | 19 | nnge1d 10940 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 1 ≤ ((2nd
‘𝑇) +
1)) |
64 | 62 | ltp1d 10833 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((2nd
‘𝑇) + 1) <
(((2nd ‘𝑇)
+ 1) + 1)) |
65 | 60, 62, 61, 63, 64 | lelttrd 10074 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 1 < (((2nd
‘𝑇) + 1) +
1)) |
66 | | elfzle1 12215 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑀 ∈ ((((2nd
‘𝑇) + 1) + 1)...𝑁) → (((2nd
‘𝑇) + 1) + 1) ≤
𝑀) |
67 | 25, 66 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (((2nd
‘𝑇) + 1) + 1) ≤
𝑀) |
68 | 60, 61, 47, 65, 67 | ltletrd 10076 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 1 < 𝑀) |
69 | 60, 47, 68 | ltled 10064 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 1 ≤ 𝑀) |
70 | | elnnz1 11280 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ ℕ ↔ (𝑀 ∈ ℤ ∧ 1 ≤
𝑀)) |
71 | 46, 69, 70 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈ ℕ) |
72 | 71, 21 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
73 | 59, 72 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑀 − 1) + 1) ∈
(ℤ≥‘1)) |
74 | | peano2zm 11297 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈
ℤ) |
75 | 46, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑀 − 1) ∈ ℤ) |
76 | | uzid 11578 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 − 1) ∈ ℤ
→ (𝑀 − 1) ∈
(ℤ≥‘(𝑀 − 1))) |
77 | | peano2uz 11617 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 − 1) ∈
(ℤ≥‘(𝑀 − 1)) → ((𝑀 − 1) + 1) ∈
(ℤ≥‘(𝑀 − 1))) |
78 | 75, 76, 77 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑀 − 1) + 1) ∈
(ℤ≥‘(𝑀 − 1))) |
79 | 59, 78 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘(𝑀 − 1))) |
80 | | uzss 11584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈
(ℤ≥‘(𝑀 − 1)) →
(ℤ≥‘𝑀) ⊆
(ℤ≥‘(𝑀 − 1))) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 →
(ℤ≥‘𝑀) ⊆
(ℤ≥‘(𝑀 − 1))) |
82 | | elfzuz3 12210 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈ ((((2nd
‘𝑇) + 1) + 1)...𝑁) → 𝑁 ∈ (ℤ≥‘𝑀)) |
83 | 25, 82 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
84 | 81, 83 | sseldd 3569 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 − 1))) |
85 | | fzsplit2 12237 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑀 − 1) + 1) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 − 1))) → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁))) |
86 | 73, 84, 85 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁))) |
87 | 59 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝑀 − 1) + 1)...𝑁) = (𝑀...𝑁)) |
88 | 87 | uneq2d 3729 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁)) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))) |
89 | 86, 88 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))) |
90 | 89 | imaeq2d 5385 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = ((2nd ‘(1st
‘𝑇)) “
((1...(𝑀 − 1)) ∪
(𝑀...𝑁)))) |
91 | | imaundi 5464 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘(1st ‘𝑇)) “ ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁))) |
92 | 90, 91 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)))) |
93 | | f1ofo 6057 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁)) |
94 | 13, 93 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁)) |
95 | | foima 6033 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) |
97 | 92, 96 | eqtr3d 2646 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁))) = (1...𝑁)) |
98 | 97 | fneq2d 5896 |
. . . . . . . . . . . 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...𝑁))) |
99 | 56, 98 | mpbid 221 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})) Fn (1...𝑁)) |
100 | 99 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) → ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})) Fn (1...𝑁)) |
101 | | ovex 6577 |
. . . . . . . . . . 11
⊢
(1...𝑁) ∈
V |
102 | 101 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) → (1...𝑁) ∈ V) |
103 | | inidm 3784 |
. . . . . . . . . 10
⊢
((1...𝑁) ∩
(1...𝑁)) = (1...𝑁) |
104 | | eqidd 2611 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) = ((1st ‘(1st
‘𝑇))‘𝑛)) |
105 | | imaundi 5464 |
. . . . . . . . . . . . . . . . . 18
⊢
((2nd ‘(1st ‘𝑇)) “ ({𝑀} ∪ ((𝑀 + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ {𝑀}) ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) |
106 | | fzpred 12259 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑀...𝑁) = ({𝑀} ∪ ((𝑀 + 1)...𝑁))) |
107 | 83, 106 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑀...𝑁) = ({𝑀} ∪ ((𝑀 + 1)...𝑁))) |
108 | 107 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ ({𝑀} ∪ ((𝑀 + 1)...𝑁)))) |
109 | | f1ofn 6051 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑇)) Fn (1...𝑁)) |
110 | 13, 109 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)) Fn (1...𝑁)) |
111 | | fnsnfv 6168 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((2nd ‘(1st ‘𝑇)) Fn (1...𝑁) ∧ 𝑀 ∈ (1...𝑁)) → {((2nd
‘(1st ‘𝑇))‘𝑀)} = ((2nd ‘(1st
‘𝑇)) “ {𝑀})) |
112 | 110, 26, 111 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → {((2nd
‘(1st ‘𝑇))‘𝑀)} = ((2nd ‘(1st
‘𝑇)) “ {𝑀})) |
113 | 112 | uneq1d 3728 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ({((2nd
‘(1st ‘𝑇))‘𝑀)} ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ {𝑀}) ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
114 | 105, 108,
113 | 3eqtr4a 2670 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)) = ({((2nd
‘(1st ‘𝑇))‘𝑀)} ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
115 | 114 | xpeq1d 5062 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}) = (({((2nd
‘(1st ‘𝑇))‘𝑀)} ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) × {0})) |
116 | | xpundir 5095 |
. . . . . . . . . . . . . . . 16
⊢
(({((2nd ‘(1st ‘𝑇))‘𝑀)} ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) × {0}) = (({((2nd
‘(1st ‘𝑇))‘𝑀)} × {0}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) |
117 | 115, 116 | syl6eq 2660 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}) = (({((2nd
‘(1st ‘𝑇))‘𝑀)} × {0}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) |
118 | 117 | uneq2d 3729 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(({((2nd ‘(1st ‘𝑇))‘𝑀)} × {0}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))) |
119 | | un12 3733 |
. . . . . . . . . . . . . 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}))) |
120 | 118, 119 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})) = (({((2nd
‘(1st ‘𝑇))‘𝑀)} × {0}) ∪ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))) |
121 | 120 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘𝑛) = ((({((2nd
‘(1st ‘𝑇))‘𝑀)} × {0}) ∪ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛)) |
122 | 121 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘𝑛) = ((({((2nd
‘(1st ‘𝑇))‘𝑀)} × {0}) ∪ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛)) |
123 | | fnconstg 6006 |
. . . . . . . . . . . . . . . . 17
⊢ (0 ∈
V → (((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) |
124 | 36, 123 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) |
125 | 35, 124 | pm3.2i 470 |
. . . . . . . . . . . . . . 15
⊢
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn
((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∧ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) |
126 | | imain 5888 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
◡(2nd ‘(1st
‘𝑇)) →
((2nd ‘(1st ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
127 | 42, 126 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
128 | 75 | zred 11358 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑀 − 1) ∈ ℝ) |
129 | | peano2re 10088 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈
ℝ) |
130 | 47, 129 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑀 + 1) ∈ ℝ) |
131 | 47 | ltp1d 10833 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 < (𝑀 + 1)) |
132 | 128, 47, 130, 48, 131 | lttrd 10077 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑀 − 1) < (𝑀 + 1)) |
133 | | fzdisj 12239 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 − 1) < (𝑀 + 1) → ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁)) = ∅) |
134 | 132, 133 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁)) = ∅) |
135 | 134 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁))) = ((2nd
‘(1st ‘𝑇)) “ ∅)) |
136 | 135, 52 | syl6eq 2660 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁))) = ∅) |
137 | 127, 136 | eqtr3d 2646 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅) |
138 | | fnun 5911 |
. . . . . . . . . . . . . . 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)...𝑁)))) |
139 | 125, 137,
138 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
140 | | imaundi 5464 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘(1st ‘𝑇)) “ ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) |
141 | | imadif 5887 |
. . . . . . . . . . . . . . . . . 18
⊢ (Fun
◡(2nd ‘(1st
‘𝑇)) →
((2nd ‘(1st ‘𝑇)) “ ((1...𝑁) ∖ {𝑀})) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) ∖ ((2nd
‘(1st ‘𝑇)) “ {𝑀}))) |
142 | 42, 141 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...𝑁) ∖ {𝑀})) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) ∖ ((2nd
‘(1st ‘𝑇)) “ {𝑀}))) |
143 | | fzsplit 12238 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ (1...𝑁) → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) |
144 | 26, 143 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) |
145 | 144 | difeq1d 3689 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((1...𝑁) ∖ {𝑀}) = (((1...𝑀) ∪ ((𝑀 + 1)...𝑁)) ∖ {𝑀})) |
146 | | difundir 3839 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((1...𝑀) ∪
((𝑀 + 1)...𝑁)) ∖ {𝑀}) = (((1...𝑀) ∖ {𝑀}) ∪ (((𝑀 + 1)...𝑁) ∖ {𝑀})) |
147 | | fzsplit2 12237 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑀 − 1) + 1) ∈
(ℤ≥‘1) ∧ 𝑀 ∈ (ℤ≥‘(𝑀 − 1))) → (1...𝑀) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑀))) |
148 | 73, 79, 147 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (1...𝑀) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑀))) |
149 | 59 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (((𝑀 − 1) + 1)...𝑀) = (𝑀...𝑀)) |
150 | | fzsn 12254 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀}) |
151 | 46, 150 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝑀...𝑀) = {𝑀}) |
152 | 149, 151 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (((𝑀 − 1) + 1)...𝑀) = {𝑀}) |
153 | 152 | uneq2d 3729 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑀)) = ((1...(𝑀 − 1)) ∪ {𝑀})) |
154 | 148, 153 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (1...𝑀) = ((1...(𝑀 − 1)) ∪ {𝑀})) |
155 | 154 | difeq1d 3689 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((1...𝑀) ∖ {𝑀}) = (((1...(𝑀 − 1)) ∪ {𝑀}) ∖ {𝑀})) |
156 | | difun2 4000 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((1...(𝑀 −
1)) ∪ {𝑀}) ∖
{𝑀}) = ((1...(𝑀 − 1)) ∖ {𝑀}) |
157 | 128, 47 | ltnled 10063 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((𝑀 − 1) < 𝑀 ↔ ¬ 𝑀 ≤ (𝑀 − 1))) |
158 | 48, 157 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ¬ 𝑀 ≤ (𝑀 − 1)) |
159 | | elfzle2 12216 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑀 ∈ (1...(𝑀 − 1)) → 𝑀 ≤ (𝑀 − 1)) |
160 | 158, 159 | nsyl 134 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ¬ 𝑀 ∈ (1...(𝑀 − 1))) |
161 | | difsn 4269 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
𝑀 ∈ (1...(𝑀 − 1)) → ((1...(𝑀 − 1)) ∖ {𝑀}) = (1...(𝑀 − 1))) |
162 | 160, 161 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((1...(𝑀 − 1)) ∖ {𝑀}) = (1...(𝑀 − 1))) |
163 | 156, 162 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (((1...(𝑀 − 1)) ∪ {𝑀}) ∖ {𝑀}) = (1...(𝑀 − 1))) |
164 | 155, 163 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((1...𝑀) ∖ {𝑀}) = (1...(𝑀 − 1))) |
165 | 47, 130 | ltnled 10063 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀)) |
166 | 131, 165 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ¬ (𝑀 + 1) ≤ 𝑀) |
167 | | elfzle1 12215 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 ∈ ((𝑀 + 1)...𝑁) → (𝑀 + 1) ≤ 𝑀) |
168 | 166, 167 | nsyl 134 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ¬ 𝑀 ∈ ((𝑀 + 1)...𝑁)) |
169 | | difsn 4269 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
𝑀 ∈ ((𝑀 + 1)...𝑁) → (((𝑀 + 1)...𝑁) ∖ {𝑀}) = ((𝑀 + 1)...𝑁)) |
170 | 168, 169 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (((𝑀 + 1)...𝑁) ∖ {𝑀}) = ((𝑀 + 1)...𝑁)) |
171 | 164, 170 | uneq12d 3730 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((1...𝑀) ∖ {𝑀}) ∪ (((𝑀 + 1)...𝑁) ∖ {𝑀})) = ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁))) |
172 | 146, 171 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((1...𝑀) ∪ ((𝑀 + 1)...𝑁)) ∖ {𝑀}) = ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁))) |
173 | 145, 172 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((1...𝑁) ∖ {𝑀}) = ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁))) |
174 | 173 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...𝑁) ∖ {𝑀})) = ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁)))) |
175 | 112 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ {𝑀}) = {((2nd
‘(1st ‘𝑇))‘𝑀)}) |
176 | 96, 175 | difeq12d 3691 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) ∖ ((2nd
‘(1st ‘𝑇)) “ {𝑀})) = ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)})) |
177 | 142, 174,
176 | 3eqtr3d 2652 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁))) = ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)})) |
178 | 140, 177 | syl5eqr 2658 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)})) |
179 | 178 | fneq2d 5896 |
. . . . . . . . . . . . . 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 ‘𝑇))‘𝑀)}))) |
180 | 139, 179 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)})) |
181 | | eldifsn 4260 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)}) ↔ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀))) |
182 | 181 | biimpri 217 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) → 𝑛 ∈ ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)})) |
183 | 182 | ancoms 468 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ≠ ((2nd
‘(1st ‘𝑇))‘𝑀) ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)})) |
184 | | disjdif 3992 |
. . . . . . . . . . . . . 14
⊢
({((2nd ‘(1st ‘𝑇))‘𝑀)} ∩ ((1...𝑁) ∖ {((2nd
‘(1st ‘𝑇))‘𝑀)})) = ∅ |
185 | | fnconstg 6006 |
. . . . . . . . . . . . . . . 16
⊢ (0 ∈
V → ({((2nd ‘(1st ‘𝑇))‘𝑀)} × {0}) Fn {((2nd
‘(1st ‘𝑇))‘𝑀)}) |
186 | 36, 185 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
({((2nd ‘(1st ‘𝑇))‘𝑀)} × {0}) Fn {((2nd
‘(1st ‘𝑇))‘𝑀)} |
187 | | fvun2 6180 |
. . . . . . . . . . . . . . 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}))‘𝑛)) |
188 | 186, 187 | mp3an1 1403 |
. . . . . . . . . . . . . 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}))‘𝑛)) |
189 | 184, 188 | mpanr1 715 |
. . . . . . . . . . . . 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}))‘𝑛)) |
190 | 180, 183,
189 | syl2an 493 |
. . . . . . . . . . . 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}))‘𝑛)) |
191 | 190 | anassrs 678 |
. . . . . . . . . . 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}))‘𝑛)) |
192 | 122, 191 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘𝑛) = (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)) |
193 | 32, 100, 102, 102, 103, 104, 192 | ofval 6804 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛) = (((1st ‘(1st
‘𝑇))‘𝑛) + (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))) |
194 | | fnconstg 6006 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
V → (((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) Fn ((2nd
‘(1st ‘𝑇)) “ (1...𝑀))) |
195 | 33, 194 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) Fn ((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) |
196 | 195, 124 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢
((((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) Fn ((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) ∧ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) |
197 | | imain 5888 |
. . . . . . . . . . . . . . 15
⊢ (Fun
◡(2nd ‘(1st
‘𝑇)) →
((2nd ‘(1st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) ∩ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
198 | 42, 197 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) ∩ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
199 | | fzdisj 12239 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅) |
200 | 131, 199 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅) |
201 | 200 | imaeq2d 5385 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ((2nd
‘(1st ‘𝑇)) “ ∅)) |
202 | 201, 52 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ∅) |
203 | 198, 202 | eqtr3d 2646 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) ∩ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅) |
204 | | fnun 5911 |
. . . . . . . . . . . . 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)...𝑁)))) |
205 | 196, 203,
204 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
206 | 144 | imaeq2d 5385 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = ((2nd ‘(1st
‘𝑇)) “
((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))) |
207 | | imaundi 5464 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘(1st ‘𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) |
208 | 206, 207 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)))) |
209 | 208, 96 | eqtr3d 2646 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) ∪ ((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁))) = (1...𝑁)) |
210 | 209 | fneq2d 5896 |
. . . . . . . . . . . 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...𝑁))) |
211 | 205, 210 | mpbid 221 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
212 | 211 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
213 | | imaundi 5464 |
. . . . . . . . . . . . . . . . . 18
⊢
((2nd ‘(1st ‘𝑇)) “ ((1...(𝑀 − 1)) ∪ {𝑀})) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ {𝑀})) |
214 | 154 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) = ((2nd ‘(1st
‘𝑇)) “
((1...(𝑀 − 1)) ∪
{𝑀}))) |
215 | 112 | uneq2d 3729 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ {((2nd
‘(1st ‘𝑇))‘𝑀)}) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd
‘(1st ‘𝑇)) “ {𝑀}))) |
216 | 213, 214,
215 | 3eqtr4a 2670 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ {((2nd
‘(1st ‘𝑇))‘𝑀)})) |
217 | 216 | xpeq1d 5062 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) = ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ {((2nd
‘(1st ‘𝑇))‘𝑀)}) × {1})) |
218 | | xpundir 5095 |
. . . . . . . . . . . . . . . 16
⊢
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) ∪ {((2nd
‘(1st ‘𝑇))‘𝑀)}) × {1}) = ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
({((2nd ‘(1st ‘𝑇))‘𝑀)} × {1})) |
219 | 217, 218 | syl6eq 2660 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) = ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
({((2nd ‘(1st ‘𝑇))‘𝑀)} × {1}))) |
220 | 219 | uneq1d 3728 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) = (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
({((2nd ‘(1st ‘𝑇))‘𝑀)} × {1})) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) |
221 | | un23 3734 |
. . . . . . . . . . . . . . 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})) |
222 | 221 | equncomi 3721 |
. . . . . . . . . . . . . 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}))) |
223 | 220, 222 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) = (({((2nd
‘(1st ‘𝑇))‘𝑀)} × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))) |
224 | 223 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛) = ((({((2nd
‘(1st ‘𝑇))‘𝑀)} × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛)) |
225 | 224 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛) = ((({((2nd
‘(1st ‘𝑇))‘𝑀)} × {1}) ∪ ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛)) |
226 | | fnconstg 6006 |
. . . . . . . . . . . . . . . 16
⊢ (1 ∈
V → ({((2nd ‘(1st ‘𝑇))‘𝑀)} × {1}) Fn {((2nd
‘(1st ‘𝑇))‘𝑀)}) |
227 | 33, 226 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
({((2nd ‘(1st ‘𝑇))‘𝑀)} × {1}) Fn {((2nd
‘(1st ‘𝑇))‘𝑀)} |
228 | | fvun2 6180 |
. . . . . . . . . . . . . . 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}))‘𝑛)) |
229 | 227, 228 | mp3an1 1403 |
. . . . . . . . . . . . . 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}))‘𝑛)) |
230 | 184, 229 | mpanr1 715 |
. . . . . . . . . . . . 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}))‘𝑛)) |
231 | 180, 183,
230 | syl2an 493 |
. . . . . . . . . . . 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}))‘𝑛)) |
232 | 231 | anassrs 678 |
. . . . . . . . . . 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}))‘𝑛)) |
233 | 225, 232 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛) = (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)) |
234 | 32, 212, 102, 102, 103, 104, 233 | ofval 6804 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((1st ‘(1st
‘𝑇))‘𝑛) + (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))) |
235 | 193, 234 | eqtr4d 2647 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛) = (((1st ‘(1st
‘𝑇))
∘𝑓 + ((((2nd ‘(1st
‘𝑇)) “
(1...𝑀)) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛)) |
236 | 235 | an32s 842 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀)) → (((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛) = (((1st ‘(1st
‘𝑇))
∘𝑓 + ((((2nd ‘(1st
‘𝑇)) “
(1...𝑀)) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛)) |
237 | 236 | anasss 677 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀))) → (((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛) = (((1st ‘(1st
‘𝑇))
∘𝑓 + ((((2nd ‘(1st
‘𝑇)) “
(1...𝑀)) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛)) |
238 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 𝑇 → (2nd ‘𝑡) = (2nd ‘𝑇)) |
239 | 238 | breq2d 4595 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 𝑇 → (𝑦 < (2nd ‘𝑡) ↔ 𝑦 < (2nd ‘𝑇))) |
240 | 239 | ifbid 4058 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑇 → if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1))) |
241 | 240 | csbeq1d 3506 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
242 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 𝑇 → (1st ‘𝑡) = (1st ‘𝑇)) |
243 | 242 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 𝑇 → (1st
‘(1st ‘𝑡)) = (1st ‘(1st
‘𝑇))) |
244 | 242 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = 𝑇 → (2nd
‘(1st ‘𝑡)) = (2nd ‘(1st
‘𝑇))) |
245 | 244 | imaeq1d 5384 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...𝑗))) |
246 | 245 | xpeq1d 5062 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1})) |
247 | 244 | imaeq1d 5384 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ ((𝑗 + 1)...𝑁))) |
248 | 247 | xpeq1d 5062 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) |
249 | 246, 248 | uneq12d 3730 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 𝑇 → ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) |
250 | 243, 249 | oveq12d 6567 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑇 → ((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
251 | 250 | csbeq2dv 3944 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
252 | 241, 251 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑇 → ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
253 | 252 | mpteq2dv 4673 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
254 | 253 | eqeq2d 2620 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
255 | 254, 3 | elrab2 3333 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ 𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
256 | 255 | simprbi 479 |
. . . . . . . . . 10
⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
257 | 1, 256 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
258 | | breq1 4586 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑀 − 2) → (𝑦 < (2nd ‘𝑇) ↔ (𝑀 − 2) < (2nd
‘𝑇))) |
259 | 258 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 2)) → (𝑦 < (2nd ‘𝑇) ↔ (𝑀 − 2) < (2nd
‘𝑇))) |
260 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑀 − 2) → (𝑦 + 1) = ((𝑀 − 2) + 1)) |
261 | | sub1m1 11161 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℂ → ((𝑀 − 1) − 1) = (𝑀 − 2)) |
262 | 57, 261 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑀 − 1) − 1) = (𝑀 − 2)) |
263 | 262 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝑀 − 1) − 1) + 1) = ((𝑀 − 2) +
1)) |
264 | 75 | zcnd 11359 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑀 − 1) ∈ ℂ) |
265 | | npcan1 10334 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 − 1) ∈ ℂ
→ (((𝑀 − 1)
− 1) + 1) = (𝑀
− 1)) |
266 | 264, 265 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝑀 − 1) − 1) + 1) = (𝑀 − 1)) |
267 | 263, 266 | eqtr3d 2646 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑀 − 2) + 1) = (𝑀 − 1)) |
268 | 260, 267 | sylan9eqr 2666 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 2)) → (𝑦 + 1) = (𝑀 − 1)) |
269 | 259, 268 | ifbieq2d 4061 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 2)) → if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) = if((𝑀 − 2) < (2nd
‘𝑇), 𝑦, (𝑀 − 1))) |
270 | 18 | nncnd 10913 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2nd
‘𝑇) ∈
ℂ) |
271 | | add1p1 11160 |
. . . . . . . . . . . . . . . . 17
⊢
((2nd ‘𝑇) ∈ ℂ → (((2nd
‘𝑇) + 1) + 1) =
((2nd ‘𝑇)
+ 2)) |
272 | 270, 271 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((2nd
‘𝑇) + 1) + 1) =
((2nd ‘𝑇)
+ 2)) |
273 | 272, 67 | eqbrtrrd 4607 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2nd
‘𝑇) + 2) ≤ 𝑀) |
274 | 18 | nnred 10912 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2nd
‘𝑇) ∈
ℝ) |
275 | | 2re 10967 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℝ |
276 | | leaddsub 10383 |
. . . . . . . . . . . . . . . . . 18
⊢
(((2nd ‘𝑇) ∈ ℝ ∧ 2 ∈ ℝ
∧ 𝑀 ∈ ℝ)
→ (((2nd ‘𝑇) + 2) ≤ 𝑀 ↔ (2nd ‘𝑇) ≤ (𝑀 − 2))) |
277 | 275, 276 | mp3an2 1404 |
. . . . . . . . . . . . . . . . 17
⊢
(((2nd ‘𝑇) ∈ ℝ ∧ 𝑀 ∈ ℝ) → (((2nd
‘𝑇) + 2) ≤ 𝑀 ↔ (2nd
‘𝑇) ≤ (𝑀 − 2))) |
278 | 274, 47, 277 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((2nd
‘𝑇) + 2) ≤ 𝑀 ↔ (2nd
‘𝑇) ≤ (𝑀 − 2))) |
279 | 60, 47 | posdifd 10493 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (1 < 𝑀 ↔ 0 < (𝑀 − 1))) |
280 | 68, 279 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 0 < (𝑀 − 1)) |
281 | | elnnz 11264 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 − 1) ∈ ℕ
↔ ((𝑀 − 1)
∈ ℤ ∧ 0 < (𝑀 − 1))) |
282 | 75, 280, 281 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑀 − 1) ∈ ℕ) |
283 | | nnm1nn0 11211 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 − 1) ∈ ℕ
→ ((𝑀 − 1)
− 1) ∈ ℕ0) |
284 | 282, 283 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑀 − 1) − 1) ∈
ℕ0) |
285 | 262, 284 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑀 − 2) ∈
ℕ0) |
286 | 285 | nn0red 11229 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑀 − 2) ∈ ℝ) |
287 | 274, 286 | lenltd 10062 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2nd
‘𝑇) ≤ (𝑀 − 2) ↔ ¬ (𝑀 − 2) < (2nd
‘𝑇))) |
288 | 278, 287 | bitrd 267 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2nd
‘𝑇) + 2) ≤ 𝑀 ↔ ¬ (𝑀 − 2) < (2nd
‘𝑇))) |
289 | 273, 288 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ¬ (𝑀 − 2) < (2nd
‘𝑇)) |
290 | 289 | iffalsed 4047 |
. . . . . . . . . . . . 13
⊢ (𝜑 → if((𝑀 − 2) < (2nd
‘𝑇), 𝑦, (𝑀 − 1)) = (𝑀 − 1)) |
291 | 290 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 2)) → if((𝑀 − 2) < (2nd
‘𝑇), 𝑦, (𝑀 − 1)) = (𝑀 − 1)) |
292 | 269, 291 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 2)) → if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) = (𝑀 − 1)) |
293 | 292 | csbeq1d 3506 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 2)) → ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋(𝑀 − 1) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
294 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = (𝑀 − 1) → (1...𝑗) = (1...(𝑀 − 1))) |
295 | 294 | imaeq2d 5385 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = (𝑀 − 1) → ((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...(𝑀 −
1)))) |
296 | 295 | xpeq1d 5062 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = (𝑀 − 1) → (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1})) |
297 | 296 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1})) |
298 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = (𝑀 − 1) → (𝑗 + 1) = ((𝑀 − 1) + 1)) |
299 | 298, 59 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (𝑗 + 1) = 𝑀) |
300 | 299 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((𝑗 + 1)...𝑁) = (𝑀...𝑁)) |
301 | 300 | imaeq2d 5385 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ (𝑀...𝑁))) |
302 | 301 | xpeq1d 5062 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})) |
303 | 297, 302 | uneq12d 3730 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}))) |
304 | 303 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))) |
305 | 75, 304 | csbied 3526 |
. . . . . . . . . . 11
⊢ (𝜑 → ⦋(𝑀 − 1) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))) |
306 | 305 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 2)) → ⦋(𝑀 − 1) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))) |
307 | 293, 306 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 2)) → ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))) |
308 | | poimir.0 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℕ) |
309 | | nnm1nn0 11211 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
310 | 308, 309 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 − 1) ∈
ℕ0) |
311 | 308 | nnred 10912 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℝ) |
312 | 47 | lem1d 10836 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀 − 1) ≤ 𝑀) |
313 | | elfzle2 12216 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ((((2nd
‘𝑇) + 1) + 1)...𝑁) → 𝑀 ≤ 𝑁) |
314 | 25, 313 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ≤ 𝑁) |
315 | 128, 47, 311, 312, 314 | letrd 10073 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀 − 1) ≤ 𝑁) |
316 | 128, 311,
60, 315 | lesub1dd 10522 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑀 − 1) − 1) ≤ (𝑁 − 1)) |
317 | 262, 316 | eqbrtrrd 4607 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 − 2) ≤ (𝑁 − 1)) |
318 | | elfz2nn0 12300 |
. . . . . . . . . 10
⊢ ((𝑀 − 2) ∈ (0...(𝑁 − 1)) ↔ ((𝑀 − 2) ∈
ℕ0 ∧ (𝑁 − 1) ∈ ℕ0 ∧
(𝑀 − 2) ≤ (𝑁 − 1))) |
319 | 285, 310,
317, 318 | syl3anbrc 1239 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 − 2) ∈ (0...(𝑁 − 1))) |
320 | | ovex 6577 |
. . . . . . . . . 10
⊢
((1st ‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}))) ∈ V |
321 | 320 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}))) ∈ V) |
322 | 257, 307,
319, 321 | fvmptd 6197 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘(𝑀 − 2)) = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))) |
323 | 322 | fveq1d 6105 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘(𝑀 − 2))‘𝑛) = (((1st ‘(1st
‘𝑇))
∘𝑓 + ((((2nd ‘(1st
‘𝑇)) “
(1...(𝑀 − 1)))
× {1}) ∪ (((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛)) |
324 | 323 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀))) → ((𝐹‘(𝑀 − 2))‘𝑛) = (((1st ‘(1st
‘𝑇))
∘𝑓 + ((((2nd ‘(1st
‘𝑇)) “
(1...(𝑀 − 1)))
× {1}) ∪ (((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛)) |
325 | | breq1 4586 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑀 − 1) → (𝑦 < (2nd ‘𝑇) ↔ (𝑀 − 1) < (2nd
‘𝑇))) |
326 | 325 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → (𝑦 < (2nd ‘𝑇) ↔ (𝑀 − 1) < (2nd
‘𝑇))) |
327 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑀 − 1) → (𝑦 + 1) = ((𝑀 − 1) + 1)) |
328 | 327, 59 | sylan9eqr 2666 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → (𝑦 + 1) = 𝑀) |
329 | 326, 328 | ifbieq2d 4061 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) = if((𝑀 − 1) < (2nd
‘𝑇), 𝑦, 𝑀)) |
330 | 62 | lep1d 10834 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2nd
‘𝑇) + 1) ≤
(((2nd ‘𝑇)
+ 1) + 1)) |
331 | 62, 61, 47, 330, 67 | letrd 10073 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2nd
‘𝑇) + 1) ≤ 𝑀) |
332 | | 1re 9918 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℝ |
333 | | leaddsub 10383 |
. . . . . . . . . . . . . . . . . 18
⊢
(((2nd ‘𝑇) ∈ ℝ ∧ 1 ∈ ℝ
∧ 𝑀 ∈ ℝ)
→ (((2nd ‘𝑇) + 1) ≤ 𝑀 ↔ (2nd ‘𝑇) ≤ (𝑀 − 1))) |
334 | 332, 333 | mp3an2 1404 |
. . . . . . . . . . . . . . . . 17
⊢
(((2nd ‘𝑇) ∈ ℝ ∧ 𝑀 ∈ ℝ) → (((2nd
‘𝑇) + 1) ≤ 𝑀 ↔ (2nd
‘𝑇) ≤ (𝑀 − 1))) |
335 | 274, 47, 334 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((2nd
‘𝑇) + 1) ≤ 𝑀 ↔ (2nd
‘𝑇) ≤ (𝑀 − 1))) |
336 | 274, 128 | lenltd 10062 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2nd
‘𝑇) ≤ (𝑀 − 1) ↔ ¬ (𝑀 − 1) < (2nd
‘𝑇))) |
337 | 335, 336 | bitrd 267 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((2nd
‘𝑇) + 1) ≤ 𝑀 ↔ ¬ (𝑀 − 1) < (2nd
‘𝑇))) |
338 | 331, 337 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ¬ (𝑀 − 1) < (2nd
‘𝑇)) |
339 | 338 | iffalsed 4047 |
. . . . . . . . . . . . 13
⊢ (𝜑 → if((𝑀 − 1) < (2nd
‘𝑇), 𝑦, 𝑀) = 𝑀) |
340 | 339 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → if((𝑀 − 1) < (2nd
‘𝑇), 𝑦, 𝑀) = 𝑀) |
341 | 329, 340 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) = 𝑀) |
342 | 341 | csbeq1d 3506 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑀 / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
343 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑀 → (1...𝑗) = (1...𝑀)) |
344 | 343 | imaeq2d 5385 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑀 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...𝑀))) |
345 | 344 | xpeq1d 5062 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑀 → (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1})) |
346 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑀 → (𝑗 + 1) = (𝑀 + 1)) |
347 | 346 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑀 → ((𝑗 + 1)...𝑁) = ((𝑀 + 1)...𝑁)) |
348 | 347 | imaeq2d 5385 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑀 → ((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ ((𝑀 + 1)...𝑁))) |
349 | 348 | xpeq1d 5062 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑀 → (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) |
350 | 345, 349 | uneq12d 3730 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑀 → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) |
351 | 350 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑀 → ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))) |
352 | 351 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 = 𝑀) → ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))) |
353 | 25, 352 | csbied 3526 |
. . . . . . . . . . 11
⊢ (𝜑 → ⦋𝑀 / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))) |
354 | 353 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋𝑀 / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))) |
355 | 342, 354 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))) |
356 | 282 | nnnn0d 11228 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 − 1) ∈
ℕ0) |
357 | 47, 311, 60, 314 | lesub1dd 10522 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 − 1) ≤ (𝑁 − 1)) |
358 | | elfz2nn0 12300 |
. . . . . . . . . 10
⊢ ((𝑀 − 1) ∈ (0...(𝑁 − 1)) ↔ ((𝑀 − 1) ∈
ℕ0 ∧ (𝑁 − 1) ∈ ℕ0 ∧
(𝑀 − 1) ≤ (𝑁 − 1))) |
359 | 356, 310,
357, 358 | syl3anbrc 1239 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 − 1) ∈ (0...(𝑁 − 1))) |
360 | | ovex 6577 |
. . . . . . . . . 10
⊢
((1st ‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) ∈ V |
361 | 360 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) ∈ V) |
362 | 257, 355,
359, 361 | fvmptd 6197 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘(𝑀 − 1)) = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))) |
363 | 362 | fveq1d 6105 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘(𝑀 − 1))‘𝑛) = (((1st ‘(1st
‘𝑇))
∘𝑓 + ((((2nd ‘(1st
‘𝑇)) “
(1...𝑀)) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛)) |
364 | 363 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀))) → ((𝐹‘(𝑀 − 1))‘𝑛) = (((1st ‘(1st
‘𝑇))
∘𝑓 + ((((2nd ‘(1st
‘𝑇)) “
(1...𝑀)) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛)) |
365 | 237, 324,
364 | 3eqtr4d 2654 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀))) → ((𝐹‘(𝑀 − 2))‘𝑛) = ((𝐹‘(𝑀 − 1))‘𝑛)) |
366 | 365 | expr 641 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 ≠ ((2nd ‘(1st
‘𝑇))‘𝑀) → ((𝐹‘(𝑀 − 2))‘𝑛) = ((𝐹‘(𝑀 − 1))‘𝑛))) |
367 | 366 | necon1d 2804 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛) → 𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑀))) |
368 | | elmapi 7765 |
. . . . . . . . . . 11
⊢
((1st ‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
369 | 29, 368 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
370 | 369, 27 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) ∈ (0..^𝐾)) |
371 | | elfzonn0 12380 |
. . . . . . . . 9
⊢
(((1st ‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) ∈ (0..^𝐾) → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) ∈
ℕ0) |
372 | 370, 371 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) ∈
ℕ0) |
373 | 372 | nn0red 11229 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) ∈ ℝ) |
374 | 373 | ltp1d 10833 |
. . . . . . 7
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) < (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) + 1)) |
375 | 373, 374 | ltned 10052 |
. . . . . 6
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) ≠ (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) + 1)) |
376 | 322 | fveq1d 6105 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘(𝑀 − 2))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = (((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘((2nd
‘(1st ‘𝑇))‘𝑀))) |
377 | 101 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (1...𝑁) ∈ V) |
378 | | eqidd 2611 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((2nd
‘(1st ‘𝑇))‘𝑀) ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = ((1st ‘(1st
‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀))) |
379 | | fzss1 12251 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈
(ℤ≥‘1) → (𝑀...𝑁) ⊆ (1...𝑁)) |
380 | 72, 379 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀...𝑁) ⊆ (1...𝑁)) |
381 | | eluzfz1 12219 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁)) |
382 | 83, 381 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁)) |
383 | | fnfvima 6400 |
. . . . . . . . . . . . 13
⊢
(((2nd ‘(1st ‘𝑇)) Fn (1...𝑁) ∧ (𝑀...𝑁) ⊆ (1...𝑁) ∧ 𝑀 ∈ (𝑀...𝑁)) → ((2nd
‘(1st ‘𝑇))‘𝑀) ∈ ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁))) |
384 | 110, 380,
382, 383 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇))‘𝑀) ∈ ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁))) |
385 | | fvun2 6180 |
. . . . . . . . . . . . 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 ‘𝑇))‘𝑀))) |
386 | 35, 38, 385 | mp3an12 1406 |
. . . . . . . . . . . 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 ‘𝑇))‘𝑀))) |
387 | 54, 384, 386 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = ((((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})‘((2nd
‘(1st ‘𝑇))‘𝑀))) |
388 | 36 | fvconst2 6374 |
. . . . . . . . . . . 12
⊢
(((2nd ‘(1st ‘𝑇))‘𝑀) ∈ ((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)) → ((((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})‘((2nd
‘(1st ‘𝑇))‘𝑀)) = 0) |
389 | 384, 388 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((2nd
‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})‘((2nd
‘(1st ‘𝑇))‘𝑀)) = 0) |
390 | 387, 389 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝜑 → (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = 0) |
391 | 390 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((2nd
‘(1st ‘𝑇))‘𝑀) ∈ (1...𝑁)) → (((((2nd
‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = 0) |
392 | 31, 99, 377, 377, 103, 378, 391 | ofval 6804 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((2nd
‘(1st ‘𝑇))‘𝑀) ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) + 0)) |
393 | 27, 392 | mpdan 699 |
. . . . . . 7
⊢ (𝜑 → (((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪
(((2nd ‘(1st ‘𝑇)) “ (𝑀...𝑁)) × {0})))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) + 0)) |
394 | 372 | nn0cnd 11230 |
. . . . . . . 8
⊢ (𝜑 → ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) ∈ ℂ) |
395 | 394 | addid1d 10115 |
. . . . . . 7
⊢ (𝜑 → (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) + 0) = ((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀))) |
396 | 376, 393,
395 | 3eqtrd 2648 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘(𝑀 − 2))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = ((1st ‘(1st
‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀))) |
397 | 362 | fveq1d 6105 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘(𝑀 − 1))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = (((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘((2nd
‘(1st ‘𝑇))‘𝑀))) |
398 | | fzss2 12252 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (1...𝑀) ⊆ (1...𝑁)) |
399 | 83, 398 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1...𝑀) ⊆ (1...𝑁)) |
400 | | elfz1end 12242 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ ↔ 𝑀 ∈ (1...𝑀)) |
401 | 71, 400 | sylib 207 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ (1...𝑀)) |
402 | | fnfvima 6400 |
. . . . . . . . . . . . 13
⊢
(((2nd ‘(1st ‘𝑇)) Fn (1...𝑁) ∧ (1...𝑀) ⊆ (1...𝑁) ∧ 𝑀 ∈ (1...𝑀)) → ((2nd
‘(1st ‘𝑇))‘𝑀) ∈ ((2nd
‘(1st ‘𝑇)) “ (1...𝑀))) |
403 | 110, 399,
401, 402 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇))‘𝑀) ∈ ((2nd
‘(1st ‘𝑇)) “ (1...𝑀))) |
404 | | fvun1 6179 |
. . . . . . . . . . . . 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 ‘𝑇))‘𝑀))) |
405 | 195, 124,
404 | mp3an12 1406 |
. . . . . . . . . . . 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 ‘𝑇))‘𝑀))) |
406 | 203, 403,
405 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1})‘((2nd
‘(1st ‘𝑇))‘𝑀))) |
407 | 33 | fvconst2 6374 |
. . . . . . . . . . . 12
⊢
(((2nd ‘(1st ‘𝑇))‘𝑀) ∈ ((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1})‘((2nd
‘(1st ‘𝑇))‘𝑀)) = 1) |
408 | 403, 407 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1})‘((2nd
‘(1st ‘𝑇))‘𝑀)) = 1) |
409 | 406, 408 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝜑 → (((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = 1) |
410 | 409 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((2nd
‘(1st ‘𝑇))‘𝑀) ∈ (1...𝑁)) → (((((2nd
‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = 1) |
411 | 31, 211, 377, 377, 103, 378, 410 | ofval 6804 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((2nd
‘(1st ‘𝑇))‘𝑀) ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) + 1)) |
412 | 27, 411 | mpdan 699 |
. . . . . . 7
⊢ (𝜑 → (((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) + 1)) |
413 | 397, 412 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘(𝑀 − 1))‘((2nd
‘(1st ‘𝑇))‘𝑀)) = (((1st
‘(1st ‘𝑇))‘((2nd
‘(1st ‘𝑇))‘𝑀)) + 1)) |
414 | 375, 396,
413 | 3netr4d 2859 |
. . . . 5
⊢ (𝜑 → ((𝐹‘(𝑀 − 2))‘((2nd
‘(1st ‘𝑇))‘𝑀)) ≠ ((𝐹‘(𝑀 − 1))‘((2nd
‘(1st ‘𝑇))‘𝑀))) |
415 | | fveq2 6103 |
. . . . . 6
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘𝑀) → ((𝐹‘(𝑀 − 2))‘𝑛) = ((𝐹‘(𝑀 − 2))‘((2nd
‘(1st ‘𝑇))‘𝑀))) |
416 | | fveq2 6103 |
. . . . . 6
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘𝑀) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘(𝑀 − 1))‘((2nd
‘(1st ‘𝑇))‘𝑀))) |
417 | 415, 416 | neeq12d 2843 |
. . . . 5
⊢ (𝑛 = ((2nd
‘(1st ‘𝑇))‘𝑀) → (((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛) ↔ ((𝐹‘(𝑀 − 2))‘((2nd
‘(1st ‘𝑇))‘𝑀)) ≠ ((𝐹‘(𝑀 − 1))‘((2nd
‘(1st ‘𝑇))‘𝑀)))) |
418 | 414, 417 | syl5ibrcom 236 |
. . . 4
⊢ (𝜑 → (𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑀) → ((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛))) |
419 | 418 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑀) → ((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛))) |
420 | 367, 419 | impbid 201 |
. 2
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛) ↔ 𝑛 = ((2nd ‘(1st
‘𝑇))‘𝑀))) |
421 | 27, 420 | riota5 6536 |
1
⊢ (𝜑 → (℩𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛)) = ((2nd ‘(1st
‘𝑇))‘𝑀)) |