Step | Hyp | Ref
| Expression |
1 | | ovex 6577 |
. . 3
⊢
(1...𝑁) ∈
V |
2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → (1...𝑁) ∈ V) |
3 | | poimirlem22.1 |
. . . 4
⊢ (𝜑 → 𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁))) |
4 | | poimir.0 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) |
5 | | nnm1nn0 11211 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
6 | 4, 5 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑁 − 1) ∈
ℕ0) |
7 | | nn0fz0 12306 |
. . . . 5
⊢ ((𝑁 − 1) ∈
ℕ0 ↔ (𝑁 − 1) ∈ (0...(𝑁 − 1))) |
8 | 6, 7 | sylib 207 |
. . . 4
⊢ (𝜑 → (𝑁 − 1) ∈ (0...(𝑁 − 1))) |
9 | 3, 8 | ffvelrnd 6268 |
. . 3
⊢ (𝜑 → (𝐹‘(𝑁 − 1)) ∈ ((0...𝐾) ↑𝑚 (1...𝑁))) |
10 | | elmapfn 7766 |
. . 3
⊢ ((𝐹‘(𝑁 − 1)) ∈ ((0...𝐾) ↑𝑚 (1...𝑁)) → (𝐹‘(𝑁 − 1)) Fn (1...𝑁)) |
11 | 9, 10 | syl 17 |
. 2
⊢ (𝜑 → (𝐹‘(𝑁 − 1)) Fn (1...𝑁)) |
12 | | 1ex 9914 |
. . 3
⊢ 1 ∈
V |
13 | | fnconstg 6006 |
. . 3
⊢ (1 ∈
V → ((1...𝑁) ×
{1}) Fn (1...𝑁)) |
14 | 12, 13 | mp1i 13 |
. 2
⊢ (𝜑 → ((1...𝑁) × {1}) Fn (1...𝑁)) |
15 | | poimirlem12.2 |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈ 𝑆) |
16 | | elrabi 3328 |
. . . . . . 7
⊢ (𝑇 ∈ {𝑡 ∈ ((((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...𝑁))) |
17 | | poimirlem22.s |
. . . . . . 7
⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} |
18 | 16, 17 | eleq2s 2706 |
. . . . . 6
⊢ (𝑇 ∈ 𝑆 → 𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
19 | 15, 18 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁))) |
20 | | xp1st 7089 |
. . . . 5
⊢ (𝑇 ∈ ((((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st ‘𝑇) ∈ (((0..^𝐾) ↑𝑚
(1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
21 | 19, 20 | syl 17 |
. . . 4
⊢ (𝜑 → (1st
‘𝑇) ∈
(((0..^𝐾)
↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) |
22 | | xp1st 7089 |
. . . 4
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁))) |
23 | 21, 22 | syl 17 |
. . 3
⊢ (𝜑 → (1st
‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁))) |
24 | | elmapfn 7766 |
. . 3
⊢
((1st ‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st
‘(1st ‘𝑇)) Fn (1...𝑁)) |
25 | 23, 24 | syl 17 |
. 2
⊢ (𝜑 → (1st
‘(1st ‘𝑇)) Fn (1...𝑁)) |
26 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑇 → (2nd ‘𝑡) = (2nd ‘𝑇)) |
27 | 26 | breq2d 4595 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑇 → (𝑦 < (2nd ‘𝑡) ↔ 𝑦 < (2nd ‘𝑇))) |
28 | 27 | ifbid 4058 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑇 → if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1))) |
29 | 28 | csbeq1d 3506 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑇 → ⦋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})))) |
30 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑇 → (1st ‘𝑡) = (1st ‘𝑇)) |
31 | 30 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑇 → (1st
‘(1st ‘𝑡)) = (1st ‘(1st
‘𝑇))) |
32 | 30 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 𝑇 → (2nd
‘(1st ‘𝑡)) = (2nd ‘(1st
‘𝑇))) |
33 | 32 | imaeq1d 5384 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...𝑗))) |
34 | 33 | xpeq1d 5062 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) = (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1})) |
35 | 32 | imaeq1d 5384 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑇 → ((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “ ((𝑗 + 1)...𝑁))) |
36 | 35 | xpeq1d 5062 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑇 → (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) |
37 | 34, 36 | uneq12d 3730 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑇 → ((((2nd
‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) |
38 | 31, 37 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑇 → ((1st
‘(1st ‘𝑡)) ∘𝑓 +
((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
39 | 38 | csbeq2dv 3944 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑇 → ⦋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})))) |
40 | 29, 39 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑇 → ⦋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})))) |
41 | 40 | mpteq2dv 4673 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑇 → (𝑦 ∈ (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}))))) |
42 | 41 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (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})))))) |
43 | 42, 17 | elrab2 3333 |
. . . . . . . 8
⊢ (𝑇 ∈ 𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))) |
44 | 43 | simprbi 479 |
. . . . . . 7
⊢ (𝑇 ∈ 𝑆 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
45 | 15, 44 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))) |
46 | | poimirlem11.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2nd
‘𝑇) =
0) |
47 | | breq12 4588 |
. . . . . . . . . . . 12
⊢ ((𝑦 = (𝑁 − 1) ∧ (2nd
‘𝑇) = 0) →
(𝑦 < (2nd
‘𝑇) ↔ (𝑁 − 1) <
0)) |
48 | 46, 47 | sylan2 490 |
. . . . . . . . . . 11
⊢ ((𝑦 = (𝑁 − 1) ∧ 𝜑) → (𝑦 < (2nd ‘𝑇) ↔ (𝑁 − 1) < 0)) |
49 | 48 | ancoms 468 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝑁 − 1)) → (𝑦 < (2nd ‘𝑇) ↔ (𝑁 − 1) < 0)) |
50 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑁 − 1) → (𝑦 + 1) = ((𝑁 − 1) + 1)) |
51 | 4 | nncnd 10913 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℂ) |
52 | | npcan1 10334 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
54 | 50, 53 | sylan9eqr 2666 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝑁 − 1)) → (𝑦 + 1) = 𝑁) |
55 | 49, 54 | ifbieq2d 4061 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝑁 − 1)) → if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) = if((𝑁 − 1) < 0, 𝑦, 𝑁)) |
56 | 6 | nn0ge0d 11231 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ (𝑁 − 1)) |
57 | | 0red 9920 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈
ℝ) |
58 | 6 | nn0red 11229 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 − 1) ∈ ℝ) |
59 | 57, 58 | lenltd 10062 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 ≤ (𝑁 − 1) ↔ ¬ (𝑁 − 1) < 0)) |
60 | 56, 59 | mpbid 221 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ (𝑁 − 1) < 0) |
61 | 60 | iffalsed 4047 |
. . . . . . . . . 10
⊢ (𝜑 → if((𝑁 − 1) < 0, 𝑦, 𝑁) = 𝑁) |
62 | 61 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝑁 − 1)) → if((𝑁 − 1) < 0, 𝑦, 𝑁) = 𝑁) |
63 | 55, 62 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = (𝑁 − 1)) → if(𝑦 < (2nd ‘𝑇), 𝑦, (𝑦 + 1)) = 𝑁) |
64 | 63 | csbeq1d 3506 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = (𝑁 − 1)) → ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑁 / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))) |
65 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑁 → (1...𝑗) = (1...𝑁)) |
66 | 65 | imaeq2d 5385 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑁 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) = ((2nd ‘(1st
‘𝑇)) “
(1...𝑁))) |
67 | | xp2nd 7090 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
68 | 21, 67 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) |
69 | | fvex 6113 |
. . . . . . . . . . . . . . . . 17
⊢
(2nd ‘(1st ‘𝑇)) ∈ V |
70 | | f1oeq1 6040 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (2nd
‘(1st ‘𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))) |
71 | 69, 70 | elab 3319 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘(1st ‘𝑇)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
72 | 68, 71 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2nd
‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)) |
73 | | f1ofo 6057 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd
‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁)) |
74 | | foima 6033 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘(1st ‘𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) |
75 | 72, 73, 74 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2nd
‘(1st ‘𝑇)) “ (1...𝑁)) = (1...𝑁)) |
76 | 66, 75 | sylan9eqr 2666 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 = 𝑁) → ((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) = (1...𝑁)) |
77 | 76 | xpeq1d 5062 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 = 𝑁) → (((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) = ((1...𝑁) × {1})) |
78 | | oveq1 6556 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑁 → (𝑗 + 1) = (𝑁 + 1)) |
79 | 78 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑁 → ((𝑗 + 1)...𝑁) = ((𝑁 + 1)...𝑁)) |
80 | 4 | nnred 10912 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ ℝ) |
81 | 80 | ltp1d 10833 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 < (𝑁 + 1)) |
82 | 4 | nnzd 11357 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℤ) |
83 | 82 | peano2zd 11361 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑁 + 1) ∈ ℤ) |
84 | | fzn 12228 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < (𝑁 + 1) ↔ ((𝑁 + 1)...𝑁) = ∅)) |
85 | 83, 82, 84 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁 < (𝑁 + 1) ↔ ((𝑁 + 1)...𝑁) = ∅)) |
86 | 81, 85 | mpbid 221 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑁 + 1)...𝑁) = ∅) |
87 | 79, 86 | sylan9eqr 2666 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 = 𝑁) → ((𝑗 + 1)...𝑁) = ∅) |
88 | 87 | imaeq2d 5385 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 = 𝑁) → ((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st
‘𝑇)) “
∅)) |
89 | 88 | xpeq1d 5062 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 = 𝑁) → (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd
‘(1st ‘𝑇)) “ ∅) ×
{0})) |
90 | | ima0 5400 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘(1st ‘𝑇)) “ ∅) =
∅ |
91 | 90 | xpeq1i 5059 |
. . . . . . . . . . . . . 14
⊢
(((2nd ‘(1st ‘𝑇)) “ ∅) × {0}) = (∅
× {0}) |
92 | | 0xp 5122 |
. . . . . . . . . . . . . 14
⊢ (∅
× {0}) = ∅ |
93 | 91, 92 | eqtri 2632 |
. . . . . . . . . . . . 13
⊢
(((2nd ‘(1st ‘𝑇)) “ ∅) × {0}) =
∅ |
94 | 89, 93 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 = 𝑁) → (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = ∅) |
95 | 77, 94 | uneq12d 3730 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 = 𝑁) → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = (((1...𝑁) × {1}) ∪
∅)) |
96 | | un0 3919 |
. . . . . . . . . . 11
⊢
(((1...𝑁) ×
{1}) ∪ ∅) = ((1...𝑁) × {1}) |
97 | 95, 96 | syl6eq 2660 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 = 𝑁) → ((((2nd
‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((1...𝑁) × {1})) |
98 | 97 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 = 𝑁) → ((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 + ((1...𝑁) ×
{1}))) |
99 | 4, 98 | csbied 3526 |
. . . . . . . 8
⊢ (𝜑 → ⦋𝑁 / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 + ((1...𝑁) ×
{1}))) |
100 | 99 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = (𝑁 − 1)) → ⦋𝑁 / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 + ((1...𝑁) ×
{1}))) |
101 | 64, 100 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 = (𝑁 − 1)) → ⦋if(𝑦 < (2nd
‘𝑇), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st
‘(1st ‘𝑇)) ∘𝑓 +
((((2nd ‘(1st ‘𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd
‘(1st ‘𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st
‘(1st ‘𝑇)) ∘𝑓 + ((1...𝑁) ×
{1}))) |
102 | | ovex 6577 |
. . . . . . 7
⊢
((1st ‘(1st ‘𝑇)) ∘𝑓 + ((1...𝑁) × {1})) ∈
V |
103 | 102 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ((1st
‘(1st ‘𝑇)) ∘𝑓 + ((1...𝑁) × {1})) ∈
V) |
104 | 45, 101, 8, 103 | fvmptd 6197 |
. . . . 5
⊢ (𝜑 → (𝐹‘(𝑁 − 1)) = ((1st
‘(1st ‘𝑇)) ∘𝑓 + ((1...𝑁) ×
{1}))) |
105 | 104 | fveq1d 6105 |
. . . 4
⊢ (𝜑 → ((𝐹‘(𝑁 − 1))‘𝑛) = (((1st ‘(1st
‘𝑇))
∘𝑓 + ((1...𝑁) × {1}))‘𝑛)) |
106 | 105 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘(𝑁 − 1))‘𝑛) = (((1st ‘(1st
‘𝑇))
∘𝑓 + ((1...𝑁) × {1}))‘𝑛)) |
107 | | inidm 3784 |
. . . 4
⊢
((1...𝑁) ∩
(1...𝑁)) = (1...𝑁) |
108 | | eqidd 2611 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) = ((1st ‘(1st
‘𝑇))‘𝑛)) |
109 | 12 | fvconst2 6374 |
. . . . 5
⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {1})‘𝑛) = 1) |
110 | 109 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {1})‘𝑛) = 1) |
111 | 25, 14, 2, 2, 107, 108, 110 | ofval 6804 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((1st
‘(1st ‘𝑇)) ∘𝑓 + ((1...𝑁) × {1}))‘𝑛) = (((1st
‘(1st ‘𝑇))‘𝑛) + 1)) |
112 | 106, 111 | eqtrd 2644 |
. 2
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘(𝑁 − 1))‘𝑛) = (((1st ‘(1st
‘𝑇))‘𝑛) + 1)) |
113 | | elmapi 7765 |
. . . . . . 7
⊢
((1st ‘(1st ‘𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
114 | 23, 113 | syl 17 |
. . . . . 6
⊢ (𝜑 → (1st
‘(1st ‘𝑇)):(1...𝑁)⟶(0..^𝐾)) |
115 | 114 | ffvelrnda 6267 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈ (0..^𝐾)) |
116 | | elfzonn0 12380 |
. . . . 5
⊢
(((1st ‘(1st ‘𝑇))‘𝑛) ∈ (0..^𝐾) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈
ℕ0) |
117 | 115, 116 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈
ℕ0) |
118 | 117 | nn0cnd 11230 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1st
‘(1st ‘𝑇))‘𝑛) ∈ ℂ) |
119 | | pncan1 10333 |
. . 3
⊢
(((1st ‘(1st ‘𝑇))‘𝑛) ∈ ℂ → ((((1st
‘(1st ‘𝑇))‘𝑛) + 1) − 1) = ((1st
‘(1st ‘𝑇))‘𝑛)) |
120 | 118, 119 | syl 17 |
. 2
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((((1st
‘(1st ‘𝑇))‘𝑛) + 1) − 1) = ((1st
‘(1st ‘𝑇))‘𝑛)) |
121 | 2, 11, 14, 25, 112, 110, 120 | offveq 6816 |
1
⊢ (𝜑 → ((𝐹‘(𝑁 − 1)) ∘𝑓
− ((1...𝑁) ×
{1})) = (1st ‘(1st ‘𝑇))) |