Proof of Theorem poimirlem23
Step | Hyp | Ref
| Expression |
1 | | ovex 6577 |
. . . . . 6
⊢ (𝑇 ∘𝑓 +
(((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V |
2 | 1 | csbex 4721 |
. . . . 5
⊢
⦋if(𝑦
< 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V |
3 | 2 | rgenw 2908 |
. . . 4
⊢
∀𝑦 ∈
(0...(𝑁 −
1))⦋if(𝑦 <
𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V |
4 | | eqid 2610 |
. . . . 5
⊢ (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) |
5 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑝 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑝‘𝑁) = (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁)) |
6 | 5 | neeq1d 2841 |
. . . . . 6
⊢ (𝑝 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝑝‘𝑁) ≠ 0 ↔ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0)) |
7 | | df-ne 2782 |
. . . . . 6
⊢
((⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0 ↔ ¬
(⦋if(𝑦 <
𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0) |
8 | 6, 7 | syl6bb 275 |
. . . . 5
⊢ (𝑝 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝑝‘𝑁) ≠ 0 ↔ ¬
(⦋if(𝑦 <
𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)) |
9 | 4, 8 | rexrnmpt 6277 |
. . . 4
⊢
(∀𝑦 ∈
(0...(𝑁 −
1))⦋if(𝑦 <
𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V →
(∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝‘𝑁) ≠ 0 ↔ ∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)) |
10 | 3, 9 | ax-mp 5 |
. . 3
⊢
(∃𝑝 ∈ ran
(𝑦 ∈ (0...(𝑁 − 1)) ↦
⦋if(𝑦 <
𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝‘𝑁) ≠ 0 ↔ ∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0) |
11 | | rexnal 2978 |
. . 3
⊢
(∃𝑦 ∈
(0...(𝑁 − 1)) ¬
(⦋if(𝑦 <
𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0) |
12 | 10, 11 | bitri 263 |
. 2
⊢
(∃𝑝 ∈ ran
(𝑦 ∈ (0...(𝑁 − 1)) ↦
⦋if(𝑦 <
𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝‘𝑁) ≠ 0 ↔ ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0) |
13 | | poimir.0 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℕ) |
14 | 13 | nnzd 11357 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℤ) |
15 | | poimirlem23.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑉 ∈ (0...𝑁)) |
16 | | elfzelz 12213 |
. . . . . . . . . . 11
⊢ (𝑉 ∈ (0...𝑁) → 𝑉 ∈ ℤ) |
17 | 15, 16 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑉 ∈ ℤ) |
18 | | zlem1lt 11306 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝑉 ∈ ℤ) → (𝑁 ≤ 𝑉 ↔ (𝑁 − 1) < 𝑉)) |
19 | 14, 17, 18 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 ≤ 𝑉 ↔ (𝑁 − 1) < 𝑉)) |
20 | | elfzle2 12216 |
. . . . . . . . . . 11
⊢ (𝑉 ∈ (0...𝑁) → 𝑉 ≤ 𝑁) |
21 | 15, 20 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑉 ≤ 𝑁) |
22 | 17 | zred 11358 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑉 ∈ ℝ) |
23 | 13 | nnred 10912 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℝ) |
24 | 22, 23 | letri3d 10058 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑉 = 𝑁 ↔ (𝑉 ≤ 𝑁 ∧ 𝑁 ≤ 𝑉))) |
25 | 24 | biimprd 237 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑉 ≤ 𝑁 ∧ 𝑁 ≤ 𝑉) → 𝑉 = 𝑁)) |
26 | 21, 25 | mpand 707 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 ≤ 𝑉 → 𝑉 = 𝑁)) |
27 | 19, 26 | sylbird 249 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 − 1) < 𝑉 → 𝑉 = 𝑁)) |
28 | 27 | necon3ad 2795 |
. . . . . . 7
⊢ (𝜑 → (𝑉 ≠ 𝑁 → ¬ (𝑁 − 1) < 𝑉)) |
29 | | nnm1nn0 11211 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
30 | 13, 29 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 − 1) ∈
ℕ0) |
31 | | nn0fz0 12306 |
. . . . . . . . . . . 12
⊢ ((𝑁 − 1) ∈
ℕ0 ↔ (𝑁 − 1) ∈ (0...(𝑁 − 1))) |
32 | 30, 31 | sylib 207 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 − 1) ∈ (0...(𝑁 − 1))) |
33 | 32 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (𝑁 − 1) ∈ (0...(𝑁 − 1))) |
34 | | iffalse 4045 |
. . . . . . . . . . . . . . . 16
⊢ (¬
(𝑁 − 1) < 𝑉 → if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) = ((𝑁 − 1) + 1)) |
35 | 13 | nncnd 10913 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ ℂ) |
36 | | npcan1 10334 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
38 | 34, 37 | sylan9eqr 2666 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) = 𝑁) |
39 | 38 | csbeq1d 3506 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑁 / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) |
40 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 𝑁 → (1...𝑗) = (1...𝑁)) |
41 | 40 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = 𝑁 → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...𝑁))) |
42 | 41 | xpeq1d 5062 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = 𝑁 → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...𝑁)) × {1})) |
43 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 𝑁 → (𝑗 + 1) = (𝑁 + 1)) |
44 | 43 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 𝑁 → ((𝑗 + 1)...𝑁) = ((𝑁 + 1)...𝑁)) |
45 | 44 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = 𝑁 → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ ((𝑁 + 1)...𝑁))) |
46 | 45 | xpeq1d 5062 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = 𝑁 → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0})) |
47 | 42, 46 | uneq12d 3730 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑁 → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...𝑁)) × {1}) ∪ ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0}))) |
48 | | poimirlem23.2 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁)) |
49 | | f1ofo 6057 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁)) |
50 | | foima 6033 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁)) |
51 | 48, 49, 50 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁)) |
52 | 51 | xpeq1d 5062 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑈 “ (1...𝑁)) × {1}) = ((1...𝑁) × {1})) |
53 | 23 | ltp1d 10833 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑁 < (𝑁 + 1)) |
54 | 14 | peano2zd 11361 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝑁 + 1) ∈ ℤ) |
55 | | fzn 12228 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑁 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < (𝑁 + 1) ↔ ((𝑁 + 1)...𝑁) = ∅)) |
56 | 54, 14, 55 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑁 < (𝑁 + 1) ↔ ((𝑁 + 1)...𝑁) = ∅)) |
57 | 53, 56 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((𝑁 + 1)...𝑁) = ∅) |
58 | 57 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑈 “ ((𝑁 + 1)...𝑁)) = (𝑈 “ ∅)) |
59 | 58 | xpeq1d 5062 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0}) = ((𝑈 “ ∅) ×
{0})) |
60 | | ima0 5400 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑈 “ ∅) =
∅ |
61 | 60 | xpeq1i 5059 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑈 “ ∅) × {0}) =
(∅ × {0}) |
62 | | 0xp 5122 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (∅
× {0}) = ∅ |
63 | 61, 62 | eqtri 2632 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑈 “ ∅) × {0}) =
∅ |
64 | 59, 63 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0}) = ∅) |
65 | 52, 64 | uneq12d 3730 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((𝑈 “ (1...𝑁)) × {1}) ∪ ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0})) = (((1...𝑁) × {1}) ∪
∅)) |
66 | | un0 3919 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((1...𝑁) ×
{1}) ∪ ∅) = ((1...𝑁) × {1}) |
67 | 65, 66 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝑈 “ (1...𝑁)) × {1}) ∪ ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0})) = ((1...𝑁) × {1})) |
68 | 47, 67 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 = 𝑁) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = ((1...𝑁) × {1})) |
69 | 68 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 = 𝑁) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + ((1...𝑁) ×
{1}))) |
70 | 13, 69 | csbied 3526 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ⦋𝑁 / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + ((1...𝑁) ×
{1}))) |
71 | 70 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ⦋𝑁 / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + ((1...𝑁) ×
{1}))) |
72 | 39, 71 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + ((1...𝑁) ×
{1}))) |
73 | 72 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = ((𝑇 ∘𝑓 + ((1...𝑁) × {1}))‘𝑁)) |
74 | | elfzonn0 12380 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (0..^𝐾) → 𝑗 ∈ ℕ0) |
75 | | nn0p1nn 11209 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℕ0
→ (𝑗 + 1) ∈
ℕ) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (0..^𝐾) → (𝑗 + 1) ∈ ℕ) |
77 | | elsni 4142 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ {1} → 𝑦 = 1) |
78 | 77 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ {1} → (𝑗 + 𝑦) = (𝑗 + 1)) |
79 | 78 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ {1} → ((𝑗 + 𝑦) ∈ ℕ ↔ (𝑗 + 1) ∈ ℕ)) |
80 | 76, 79 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (0..^𝐾) → (𝑦 ∈ {1} → (𝑗 + 𝑦) ∈ ℕ)) |
81 | 80 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ (0..^𝐾) ∧ 𝑦 ∈ {1}) → (𝑗 + 𝑦) ∈ ℕ) |
82 | 81 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ (0..^𝐾) ∧ 𝑦 ∈ {1})) → (𝑗 + 𝑦) ∈ ℕ) |
83 | | poimirlem23.1 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑇:(1...𝑁)⟶(0..^𝐾)) |
84 | | 1ex 9914 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
V |
85 | 84 | fconst 6004 |
. . . . . . . . . . . . . . . 16
⊢
((1...𝑁) ×
{1}):(1...𝑁)⟶{1} |
86 | 85 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((1...𝑁) × {1}):(1...𝑁)⟶{1}) |
87 | | ovex 6577 |
. . . . . . . . . . . . . . . 16
⊢
(1...𝑁) ∈
V |
88 | 87 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1...𝑁) ∈ V) |
89 | | inidm 3784 |
. . . . . . . . . . . . . . 15
⊢
((1...𝑁) ∩
(1...𝑁)) = (1...𝑁) |
90 | 82, 83, 86, 88, 88, 89 | off 6810 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑇 ∘𝑓 + ((1...𝑁) × {1})):(1...𝑁)⟶ℕ) |
91 | | elfz1end 12242 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁)) |
92 | 13, 91 | sylib 207 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ (1...𝑁)) |
93 | 90, 92 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑇 ∘𝑓 + ((1...𝑁) × {1}))‘𝑁) ∈
ℕ) |
94 | 93 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ((𝑇 ∘𝑓 + ((1...𝑁) × {1}))‘𝑁) ∈
ℕ) |
95 | 73, 94 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ∈ ℕ) |
96 | 95 | nnne0d 10942 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0) |
97 | | breq1 4586 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑁 − 1) → (𝑦 < 𝑉 ↔ (𝑁 − 1) < 𝑉)) |
98 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑁 − 1) → 𝑦 = (𝑁 − 1)) |
99 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑁 − 1) → (𝑦 + 1) = ((𝑁 − 1) + 1)) |
100 | 97, 98, 99 | ifbieq12d 4063 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑁 − 1) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1))) |
101 | 100 | csbeq1d 3506 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑁 − 1) → ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) |
102 | 101 | fveq1d 6105 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑁 − 1) → (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁)) |
103 | 102 | neeq1d 2841 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑁 − 1) → ((⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0 ↔ (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0)) |
104 | 7, 103 | syl5bbr 273 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑁 − 1) → (¬
(⦋if(𝑦 <
𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0)) |
105 | 104 | rspcev 3282 |
. . . . . . . . . 10
⊢ (((𝑁 − 1) ∈ (0...(𝑁 − 1)) ∧
(⦋if((𝑁
− 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0) → ∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0) |
106 | 33, 96, 105 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0) |
107 | 106, 11 | sylib 207 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0) |
108 | 107 | ex 449 |
. . . . . . 7
⊢ (𝜑 → (¬ (𝑁 − 1) < 𝑉 → ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)) |
109 | 28, 108 | syld 46 |
. . . . . 6
⊢ (𝜑 → (𝑉 ≠ 𝑁 → ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)) |
110 | 109 | necon4ad 2801 |
. . . . 5
⊢ (𝜑 → (∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 → 𝑉 = 𝑁)) |
111 | 110 | pm4.71rd 665 |
. . . 4
⊢ (𝜑 → (∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (𝑉 = 𝑁 ∧ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))) |
112 | 30 | nn0zd 11356 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) |
113 | | uzid 11578 |
. . . . . . . . . . . . 13
⊢ ((𝑁 − 1) ∈ ℤ
→ (𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1))) |
114 | | peano2uz 11617 |
. . . . . . . . . . . . 13
⊢ ((𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
115 | 112, 113,
114 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
116 | 37, 115 | eqeltrrd 2689 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) |
117 | | fzss2 12252 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘(𝑁 − 1)) → (0...(𝑁 − 1)) ⊆ (0...𝑁)) |
118 | 116, 117 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (0...(𝑁 − 1)) ⊆ (0...𝑁)) |
119 | 118 | sselda 3568 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑗 ∈ (0...𝑁)) |
120 | 92 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑁 ∈ (1...𝑁)) |
121 | | ffn 5958 |
. . . . . . . . . . . . . . 15
⊢ (𝑇:(1...𝑁)⟶(0..^𝐾) → 𝑇 Fn (1...𝑁)) |
122 | 83, 121 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑇 Fn (1...𝑁)) |
123 | 122 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑇 Fn (1...𝑁)) |
124 | 84 | fconst 6004 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} |
125 | | c0ex 9913 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
V |
126 | 125 | fconst 6004 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0} |
127 | 124, 126 | pm3.2i 470 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}) |
128 | | dff1o3 6056 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun ◡𝑈)) |
129 | 128 | simprbi 479 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun ◡𝑈) |
130 | | imain 5888 |
. . . . . . . . . . . . . . . . . 18
⊢ (Fun
◡𝑈 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁)))) |
131 | 48, 129, 130 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁)))) |
132 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ) |
133 | 132 | zred 11358 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ) |
134 | 133 | ltp1d 10833 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1)) |
135 | | fzdisj 12239 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅) |
136 | 134, 135 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅) |
137 | 136 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (𝑈 “ ∅)) |
138 | 137, 60 | syl6eq 2660 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅) |
139 | 131, 138 | sylan9req 2665 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅) |
140 | | fun 5979 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑈 “
(1...𝑗)) ×
{1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}) ∧ ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0})) |
141 | 127, 139,
140 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0})) |
142 | | elfznn0 12302 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ0) |
143 | 142, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ) |
144 | | nnuz 11599 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ℕ =
(ℤ≥‘1) |
145 | 143, 144 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈
(ℤ≥‘1)) |
146 | | elfzuz3 12210 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ≥‘𝑗)) |
147 | | fzsplit2 12237 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑗 + 1) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) |
148 | 145, 146,
147 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) |
149 | 148 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (0...𝑁) → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))) |
150 | | imaundi 5464 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) |
151 | 149, 150 | syl6req 2661 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (0...𝑁) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (𝑈 “ (1...𝑁))) |
152 | 151, 51 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (1...𝑁)) |
153 | 152 | feq2d 5944 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}) ↔ (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))) |
154 | 141, 153 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0})) |
155 | | ffn 5958 |
. . . . . . . . . . . . . 14
⊢ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
156 | 154, 155 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
157 | 87 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ V) |
158 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑁 ∈ (1...𝑁)) → (𝑇‘𝑁) = (𝑇‘𝑁)) |
159 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑁 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)) |
160 | 123, 156,
157, 157, 89, 158, 159 | ofval 6804 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑁 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = ((𝑇‘𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))) |
161 | 120, 160 | mpdan 699 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = ((𝑇‘𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))) |
162 | 161 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇‘𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)) = 0)) |
163 | 83, 92 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑇‘𝑁) ∈ (0..^𝐾)) |
164 | | elfzonn0 12380 |
. . . . . . . . . . . . . 14
⊢ ((𝑇‘𝑁) ∈ (0..^𝐾) → (𝑇‘𝑁) ∈
ℕ0) |
165 | 163, 164 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑇‘𝑁) ∈
ℕ0) |
166 | 165 | nn0red 11229 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑇‘𝑁) ∈ ℝ) |
167 | 166 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑇‘𝑁) ∈ ℝ) |
168 | 165 | nn0ge0d 11231 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ (𝑇‘𝑁)) |
169 | 168 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 0 ≤ (𝑇‘𝑁)) |
170 | | 1re 9918 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ |
171 | | snssi 4280 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
ℝ → {1} ⊆ ℝ) |
172 | 170, 171 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ {1}
⊆ ℝ |
173 | | 0re 9919 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
174 | | snssi 4280 |
. . . . . . . . . . . . . 14
⊢ (0 ∈
ℝ → {0} ⊆ ℝ) |
175 | 173, 174 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ {0}
⊆ ℝ |
176 | 172, 175 | unssi 3750 |
. . . . . . . . . . . 12
⊢ ({1}
∪ {0}) ⊆ ℝ |
177 | 154, 120 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ({1} ∪ {0})) |
178 | 176, 177 | sseldi 3566 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ℝ) |
179 | | elun 3715 |
. . . . . . . . . . . . 13
⊢
(((((𝑈 “
(1...𝑗)) × {1}) ∪
((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ({1} ∪ {0}) ↔ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} ∨ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0})) |
180 | | 0le1 10430 |
. . . . . . . . . . . . . . 15
⊢ 0 ≤
1 |
181 | | elsni 4142 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑈 “
(1...𝑗)) × {1}) ∪
((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 1) |
182 | 180, 181 | syl5breqr 4621 |
. . . . . . . . . . . . . 14
⊢
(((((𝑈 “
(1...𝑗)) × {1}) ∪
((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)) |
183 | | 0le0 10987 |
. . . . . . . . . . . . . . 15
⊢ 0 ≤
0 |
184 | | elsni 4142 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑈 “
(1...𝑗)) × {1}) ∪
((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0} → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0) |
185 | 183, 184 | syl5breqr 4621 |
. . . . . . . . . . . . . 14
⊢
(((((𝑈 “
(1...𝑗)) × {1}) ∪
((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0} → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)) |
186 | 182, 185 | jaoi 393 |
. . . . . . . . . . . . 13
⊢
((((((𝑈 “
(1...𝑗)) × {1}) ∪
((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} ∨ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0}) → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)) |
187 | 179, 186 | sylbi 206 |
. . . . . . . . . . . 12
⊢
(((((𝑈 “
(1...𝑗)) × {1}) ∪
((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ({1} ∪ {0}) → 0 ≤
((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)) |
188 | 177, 187 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)) |
189 | | add20 10419 |
. . . . . . . . . . 11
⊢ ((((𝑇‘𝑁) ∈ ℝ ∧ 0 ≤ (𝑇‘𝑁)) ∧ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ℝ ∧ 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))) → (((𝑇‘𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)) = 0 ↔ ((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))) |
190 | 167, 169,
178, 188, 189 | syl22anc 1319 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑇‘𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)) = 0 ↔ ((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))) |
191 | 162, 190 | bitrd 267 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))) |
192 | 119, 191 | syldan 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))) |
193 | 192 | ralbidva 2968 |
. . . . . . 7
⊢ (𝜑 → (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))) |
194 | 193 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑉 = 𝑁) → (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))) |
195 | | breq2 4587 |
. . . . . . . . . . . . . 14
⊢ (𝑉 = 𝑁 → (𝑦 < 𝑉 ↔ 𝑦 < 𝑁)) |
196 | 195 | ifbid 4058 |
. . . . . . . . . . . . 13
⊢ (𝑉 = 𝑁 → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = if(𝑦 < 𝑁, 𝑦, (𝑦 + 1))) |
197 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℤ) |
198 | 197 | zred 11358 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ) |
199 | 198 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ ℝ) |
200 | 30 | nn0red 11229 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 − 1) ∈ ℝ) |
201 | 200 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ) |
202 | 23 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℝ) |
203 | | elfzle2 12216 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ≤ (𝑁 − 1)) |
204 | 203 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ≤ (𝑁 − 1)) |
205 | 23 | ltm1d 10835 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 − 1) < 𝑁) |
206 | 205 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) < 𝑁) |
207 | 199, 201,
202, 204, 206 | lelttrd 10074 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 < 𝑁) |
208 | 207 | iftrued 4044 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑁, 𝑦, (𝑦 + 1)) = 𝑦) |
209 | 196, 208 | sylan9eqr 2666 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑉 = 𝑁) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = 𝑦) |
210 | 209 | an32s 842 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = 𝑦) |
211 | 210 | csbeq1d 3506 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑦 / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) |
212 | 211 | fveq1d 6105 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) →
(⦋if(𝑦 <
𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = (⦋𝑦 / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁)) |
213 | 212 | eqeq1d 2612 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) →
((⦋if(𝑦 <
𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (⦋𝑦 / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)) |
214 | 213 | ralbidva 2968 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑉 = 𝑁) → (∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋𝑦 / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)) |
215 | | nfv 1830 |
. . . . . . . 8
⊢
Ⅎ𝑦((𝑇 ∘𝑓 +
(((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 |
216 | | nfcsb1v 3515 |
. . . . . . . . . 10
⊢
Ⅎ𝑗⦋𝑦 / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) |
217 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑗𝑁 |
218 | 216, 217 | nffv 6110 |
. . . . . . . . 9
⊢
Ⅎ𝑗(⦋𝑦 / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) |
219 | 218 | nfeq1 2764 |
. . . . . . . 8
⊢
Ⅎ𝑗(⦋𝑦 / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 |
220 | | csbeq1a 3508 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑦 → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑦 / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) |
221 | 220 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝑗 = 𝑦 → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = (⦋𝑦 / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁)) |
222 | 221 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑗 = 𝑦 → (((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (⦋𝑦 / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)) |
223 | 215, 219,
222 | cbvral 3143 |
. . . . . . 7
⊢
(∀𝑗 ∈
(0...(𝑁 − 1))((𝑇 ∘𝑓 +
(((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋𝑦 / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0) |
224 | 214, 223 | syl6bbr 277 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑉 = 𝑁) → (∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)) |
225 | | ne0i 3880 |
. . . . . . . . . 10
⊢ ((𝑁 − 1) ∈ (0...(𝑁 − 1)) → (0...(𝑁 − 1)) ≠
∅) |
226 | | r19.3rzv 4016 |
. . . . . . . . . 10
⊢
((0...(𝑁 − 1))
≠ ∅ → ((𝑇‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))(𝑇‘𝑁) = 0)) |
227 | 32, 225, 226 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑇‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))(𝑇‘𝑁) = 0)) |
228 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℤ) |
229 | 228 | zred 11358 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℝ) |
230 | 229 | ltp1d 10833 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 < (𝑗 + 1)) |
231 | 230, 135 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (0...(𝑁 − 1)) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅) |
232 | 231 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (𝑈 “ ∅)) |
233 | 232, 60 | syl6eq 2660 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅) |
234 | 131, 233 | sylan9req 2665 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅) |
235 | 234 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅) |
236 | | simplr 788 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑈‘𝑁) = 𝑁) |
237 | | f1ofn 6051 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 Fn (1...𝑁)) |
238 | 48, 237 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑈 Fn (1...𝑁)) |
239 | 238 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑈 Fn (1...𝑁)) |
240 | | elfznn0 12302 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℕ0) |
241 | 240, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑗 + 1) ∈ ℕ) |
242 | 241, 144 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑗 + 1) ∈
(ℤ≥‘1)) |
243 | | fzss1 12251 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 + 1) ∈
(ℤ≥‘1) → ((𝑗 + 1)...𝑁) ⊆ (1...𝑁)) |
244 | 242, 243 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (0...(𝑁 − 1)) → ((𝑗 + 1)...𝑁) ⊆ (1...𝑁)) |
245 | 244 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑗 + 1)...𝑁) ⊆ (1...𝑁)) |
246 | 37 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁) |
247 | | elfzuz3 12210 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈
(ℤ≥‘𝑗)) |
248 | | eluzp1p1 11589 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 − 1) ∈
(ℤ≥‘𝑗) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑗 + 1))) |
249 | 247, 248 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑗 + 1))) |
250 | 249 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑗 + 1))) |
251 | 246, 250 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ≥‘(𝑗 + 1))) |
252 | | eluzfz2 12220 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈
(ℤ≥‘(𝑗 + 1)) → 𝑁 ∈ ((𝑗 + 1)...𝑁)) |
253 | 251, 252 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ((𝑗 + 1)...𝑁)) |
254 | | fnfvima 6400 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈 Fn (1...𝑁) ∧ ((𝑗 + 1)...𝑁) ⊆ (1...𝑁) ∧ 𝑁 ∈ ((𝑗 + 1)...𝑁)) → (𝑈‘𝑁) ∈ (𝑈 “ ((𝑗 + 1)...𝑁))) |
255 | 239, 245,
253, 254 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑈‘𝑁) ∈ (𝑈 “ ((𝑗 + 1)...𝑁))) |
256 | 255 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑈‘𝑁) ∈ (𝑈 “ ((𝑗 + 1)...𝑁))) |
257 | 236, 256 | eqeltrrd 2689 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁))) |
258 | | fnconstg 6006 |
. . . . . . . . . . . . . . . 16
⊢ (1 ∈
V → ((𝑈 “
(1...𝑗)) × {1}) Fn
(𝑈 “ (1...𝑗))) |
259 | 84, 258 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)) |
260 | | fnconstg 6006 |
. . . . . . . . . . . . . . . 16
⊢ (0 ∈
V → ((𝑈 “
((𝑗 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑁))) |
261 | 125, 260 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑁)) |
262 | | fvun2 6180 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)) ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑁)) ∧ (((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁)) |
263 | 259, 261,
262 | mp3an12 1406 |
. . . . . . . . . . . . . 14
⊢ ((((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁)) |
264 | 235, 257,
263 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁)) |
265 | 125 | fvconst2 6374 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁)) → (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁) = 0) |
266 | 257, 265 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁) = 0) |
267 | 264, 266 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0) |
268 | 267 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑈‘𝑁) = 𝑁) → ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0) |
269 | 268 | ex 449 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑈‘𝑁) = 𝑁 → ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)) |
270 | 32 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → (𝑁 − 1) ∈ (0...(𝑁 − 1))) |
271 | | ax-1ne0 9884 |
. . . . . . . . . . . . . . 15
⊢ 1 ≠
0 |
272 | | imain 5888 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (Fun
◡𝑈 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁)))) |
273 | 48, 129, 272 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁)))) |
274 | 205, 37 | breqtrrd 4611 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑁 − 1) < ((𝑁 − 1) + 1)) |
275 | | fzdisj 12239 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 − 1) < ((𝑁 − 1) + 1) →
((1...(𝑁 − 1)) ∩
(((𝑁 − 1) +
1)...𝑁)) =
∅) |
276 | 274, 275 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁)) = ∅) |
277 | 276 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = (𝑈 “ ∅)) |
278 | 277, 60 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = ∅) |
279 | 273, 278 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅) |
280 | 279 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅) |
281 | 92 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → 𝑁 ∈ (1...𝑁)) |
282 | | elimasni 5411 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ (𝑈 “ {𝑁}) → 𝑁𝑈𝑁) |
283 | | fnbrfvb 6146 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑈 Fn (1...𝑁) ∧ 𝑁 ∈ (1...𝑁)) → ((𝑈‘𝑁) = 𝑁 ↔ 𝑁𝑈𝑁)) |
284 | 238, 92, 283 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((𝑈‘𝑁) = 𝑁 ↔ 𝑁𝑈𝑁)) |
285 | 282, 284 | syl5ibr 235 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑁 ∈ (𝑈 “ {𝑁}) → (𝑈‘𝑁) = 𝑁)) |
286 | 285 | necon3ad 2795 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑈‘𝑁) ≠ 𝑁 → ¬ 𝑁 ∈ (𝑈 “ {𝑁}))) |
287 | 286 | imp 444 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ¬ 𝑁 ∈ (𝑈 “ {𝑁})) |
288 | 281, 287 | eldifd 3551 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → 𝑁 ∈ ((1...𝑁) ∖ (𝑈 “ {𝑁}))) |
289 | | imadif 5887 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (Fun
◡𝑈 → (𝑈 “ ((1...𝑁) ∖ {𝑁})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑁}))) |
290 | 48, 129, 289 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑁})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑁}))) |
291 | | difun2 4000 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((1...(𝑁 −
1)) ∪ {𝑁}) ∖
{𝑁}) = ((1...(𝑁 − 1)) ∖ {𝑁}) |
292 | 13, 144 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) |
293 | | fzm1 12289 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈
(ℤ≥‘1) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁))) |
294 | 292, 293 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝑗 ∈ (1...𝑁) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁))) |
295 | | elun 3715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑗 ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 ∈ {𝑁})) |
296 | | velsn 4141 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑗 ∈ {𝑁} ↔ 𝑗 = 𝑁) |
297 | 296 | orbi2i 540 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 ∈ {𝑁}) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁)) |
298 | 295, 297 | bitri 263 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑗 ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁)) |
299 | 294, 298 | syl6rbbr 278 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝑗 ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ 𝑗 ∈ (1...𝑁))) |
300 | 299 | eqrdv 2608 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ {𝑁}) = (1...𝑁)) |
301 | 300 | difeq1d 3689 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ {𝑁}) = ((1...𝑁) ∖ {𝑁})) |
302 | 200, 23 | ltnled 10063 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1))) |
303 | 205, 302 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1)) |
304 | | elfzle2 12216 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1)) |
305 | 303, 304 | nsyl 134 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1))) |
306 | | difsn 4269 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
𝑁 ∈ (1...(𝑁 − 1)) → ((1...(𝑁 − 1)) ∖ {𝑁}) = (1...(𝑁 − 1))) |
307 | 305, 306 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((1...(𝑁 − 1)) ∖ {𝑁}) = (1...(𝑁 − 1))) |
308 | 291, 301,
307 | 3eqtr3a 2668 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1))) |
309 | 308 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑁})) = (𝑈 “ (1...(𝑁 − 1)))) |
310 | 51 | difeq1d 3689 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑁})) = ((1...𝑁) ∖ (𝑈 “ {𝑁}))) |
311 | 290, 309,
310 | 3eqtr3rd 2653 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((1...𝑁) ∖ (𝑈 “ {𝑁})) = (𝑈 “ (1...(𝑁 − 1)))) |
312 | 311 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ((1...𝑁) ∖ (𝑈 “ {𝑁})) = (𝑈 “ (1...(𝑁 − 1)))) |
313 | 288, 312 | eleqtrd 2690 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → 𝑁 ∈ (𝑈 “ (1...(𝑁 − 1)))) |
314 | | fnconstg 6006 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1 ∈
V → ((𝑈 “
(1...(𝑁 − 1)))
× {1}) Fn (𝑈 “
(1...(𝑁 −
1)))) |
315 | 84, 314 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 “ (1...(𝑁 − 1))) × {1}) Fn (𝑈 “ (1...(𝑁 − 1))) |
316 | | fnconstg 6006 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
V → ((𝑈 “
(((𝑁 − 1) +
1)...𝑁)) × {0}) Fn
(𝑈 “ (((𝑁 − 1) + 1)...𝑁))) |
317 | 125, 316 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑁 − 1) + 1)...𝑁)) |
318 | | fvun1 6179 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑈 “ (1...(𝑁 − 1))) × {1}) Fn (𝑈 “ (1...(𝑁 − 1))) ∧ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑁 − 1) + 1)...𝑁)) ∧ (((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ (1...(𝑁 − 1))))) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁)) |
319 | 315, 317,
318 | mp3an12 1406 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ (1...(𝑁 − 1)))) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁)) |
320 | 280, 313,
319 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁)) |
321 | 84 | fvconst2 6374 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ (𝑈 “ (1...(𝑁 − 1))) → (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁) = 1) |
322 | 313, 321 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁) = 1) |
323 | 320, 322 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = 1) |
324 | 323 | neeq1d 2841 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → (((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0 ↔ 1 ≠ 0)) |
325 | 271, 324 | mpbiri 247 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0) |
326 | | df-ne 2782 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑈 “
(1...𝑗)) × {1}) ∪
((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ≠ 0 ↔ ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0) |
327 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = (𝑁 − 1) → (1...𝑗) = (1...(𝑁 − 1))) |
328 | 327 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = (𝑁 − 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑁 − 1)))) |
329 | 328 | xpeq1d 5062 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = (𝑁 − 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑁 − 1))) × {1})) |
330 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = (𝑁 − 1) → (𝑗 + 1) = ((𝑁 − 1) + 1)) |
331 | 330 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = (𝑁 − 1) → ((𝑗 + 1)...𝑁) = (((𝑁 − 1) + 1)...𝑁)) |
332 | 331 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = (𝑁 − 1) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) |
333 | 332 | xpeq1d 5062 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = (𝑁 − 1) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0})) |
334 | 329, 333 | uneq12d 3730 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = (𝑁 − 1) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))) |
335 | 334 | fveq1d 6105 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = (𝑁 − 1) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁)) |
336 | 335 | neeq1d 2841 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = (𝑁 − 1) → (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ≠ 0 ↔ ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0)) |
337 | 326, 336 | syl5bbr 273 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = (𝑁 − 1) → (¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0 ↔ ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0)) |
338 | 337 | rspcev 3282 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 − 1) ∈ (0...(𝑁 − 1)) ∧ ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0) → ∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0) |
339 | 270, 325,
338 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0) |
340 | 339 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑈‘𝑁) ≠ 𝑁 → ∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)) |
341 | | rexnal 2978 |
. . . . . . . . . . . 12
⊢
(∃𝑗 ∈
(0...(𝑁 − 1)) ¬
((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0 ↔ ¬ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0) |
342 | 340, 341 | syl6ib 240 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑈‘𝑁) ≠ 𝑁 → ¬ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)) |
343 | 342 | necon4ad 2801 |
. . . . . . . . . 10
⊢ (𝜑 → (∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0 → (𝑈‘𝑁) = 𝑁)) |
344 | 269, 343 | impbid 201 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑈‘𝑁) = 𝑁 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)) |
345 | 227, 344 | anbi12d 743 |
. . . . . . . 8
⊢ (𝜑 → (((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁) ↔ (∀𝑗 ∈ (0...(𝑁 − 1))(𝑇‘𝑁) = 0 ∧ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))) |
346 | | r19.26 3046 |
. . . . . . . 8
⊢
(∀𝑗 ∈
(0...(𝑁 − 1))((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0) ↔ (∀𝑗 ∈ (0...(𝑁 − 1))(𝑇‘𝑁) = 0 ∧ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)) |
347 | 345, 346 | syl6bbr 277 |
. . . . . . 7
⊢ (𝜑 → (((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁) ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))) |
348 | 347 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑉 = 𝑁) → (((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁) ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))) |
349 | 194, 224,
348 | 3bitr4d 299 |
. . . . 5
⊢ ((𝜑 ∧ 𝑉 = 𝑁) → (∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁))) |
350 | 349 | pm5.32da 671 |
. . . 4
⊢ (𝜑 → ((𝑉 = 𝑁 ∧ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0) ↔ (𝑉 = 𝑁 ∧ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁)))) |
351 | 111, 350 | bitrd 267 |
. . 3
⊢ (𝜑 → (∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (𝑉 = 𝑁 ∧ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁)))) |
352 | 351 | notbid 307 |
. 2
⊢ (𝜑 → (¬ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁)))) |
353 | 12, 352 | syl5bb 271 |
1
⊢ (𝜑 → (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝‘𝑁) ≠ 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁)))) |