| Step | Hyp | Ref
| Expression |
| 1 | | poimirlem2.3 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁)) |
| 2 | | dff1o3 6854 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun ◡𝑈)) |
| 3 | 2 | simprbi 496 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun ◡𝑈) |
| 4 | 1, 3 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Fun ◡𝑈) |
| 5 | | imadif 6650 |
. . . . . . . . . . . . . . 15
⊢ (Fun
◡𝑈 → (𝑈 “ ((1...𝑁) ∖ {(𝑉 + 1)})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)}))) |
| 6 | 4, 5 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈 “ ((1...𝑁) ∖ {(𝑉 + 1)})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)}))) |
| 7 | | poimirlem2.4 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑉 ∈ (1...(𝑁 − 1))) |
| 8 | | fzp1elp1 13617 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑉 ∈ (1...(𝑁 − 1)) → (𝑉 + 1) ∈ (1...((𝑁 − 1) + 1))) |
| 9 | 7, 8 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑉 + 1) ∈ (1...((𝑁 − 1) + 1))) |
| 10 | | poimir.0 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 11 | 10 | nncnd 12282 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑁 ∈ ℂ) |
| 12 | | npcan1 11688 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
| 13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
| 14 | 13 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁)) |
| 15 | 9, 14 | eleqtrd 2843 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑉 + 1) ∈ (1...𝑁)) |
| 16 | | fzsplit 13590 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑉 + 1) ∈ (1...𝑁) → (1...𝑁) = ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁))) |
| 17 | 15, 16 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1...𝑁) = ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁))) |
| 18 | 17 | difeq1d 4125 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1...𝑁) ∖ {(𝑉 + 1)}) = (((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)) ∖ {(𝑉 + 1)})) |
| 19 | | difundir 4291 |
. . . . . . . . . . . . . . . . 17
⊢
(((1...(𝑉 + 1))
∪ (((𝑉 + 1) +
1)...𝑁)) ∖ {(𝑉 + 1)}) = (((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) ∪ ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)})) |
| 20 | | elfzuz 13560 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑉 ∈ (1...(𝑁 − 1)) → 𝑉 ∈
(ℤ≥‘1)) |
| 21 | 7, 20 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑉 ∈
(ℤ≥‘1)) |
| 22 | | fzsuc 13611 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑉 ∈
(ℤ≥‘1) → (1...(𝑉 + 1)) = ((1...𝑉) ∪ {(𝑉 + 1)})) |
| 23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1...(𝑉 + 1)) = ((1...𝑉) ∪ {(𝑉 + 1)})) |
| 24 | 23 | difeq1d 4125 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) = (((1...𝑉) ∪ {(𝑉 + 1)}) ∖ {(𝑉 + 1)})) |
| 25 | | difun2 4481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((1...𝑉) ∪
{(𝑉 + 1)}) ∖ {(𝑉 + 1)}) = ((1...𝑉) ∖ {(𝑉 + 1)}) |
| 26 | 7 | elfzelzd 13565 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑉 ∈ ℤ) |
| 27 | 26 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑉 ∈ ℝ) |
| 28 | 27 | ltp1d 12198 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑉 < (𝑉 + 1)) |
| 29 | 26 | peano2zd 12725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝑉 + 1) ∈ ℤ) |
| 30 | 29 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑉 + 1) ∈ ℝ) |
| 31 | 27, 30 | ltnled 11408 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑉 < (𝑉 + 1) ↔ ¬ (𝑉 + 1) ≤ 𝑉)) |
| 32 | 28, 31 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ¬ (𝑉 + 1) ≤ 𝑉) |
| 33 | | elfzle2 13568 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑉 + 1) ∈ (1...𝑉) → (𝑉 + 1) ≤ 𝑉) |
| 34 | 32, 33 | nsyl 140 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ¬ (𝑉 + 1) ∈ (1...𝑉)) |
| 35 | | difsn 4798 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
(𝑉 + 1) ∈ (1...𝑉) → ((1...𝑉) ∖ {(𝑉 + 1)}) = (1...𝑉)) |
| 36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((1...𝑉) ∖ {(𝑉 + 1)}) = (1...𝑉)) |
| 37 | 25, 36 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((1...𝑉) ∪ {(𝑉 + 1)}) ∖ {(𝑉 + 1)}) = (1...𝑉)) |
| 38 | 24, 37 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) = (1...𝑉)) |
| 39 | 30 | ltp1d 12198 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑉 + 1) < ((𝑉 + 1) + 1)) |
| 40 | | peano2re 11434 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑉 + 1) ∈ ℝ →
((𝑉 + 1) + 1) ∈
ℝ) |
| 41 | 30, 40 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((𝑉 + 1) + 1) ∈ ℝ) |
| 42 | 30, 41 | ltnled 11408 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑉 + 1) < ((𝑉 + 1) + 1) ↔ ¬ ((𝑉 + 1) + 1) ≤ (𝑉 + 1))) |
| 43 | 39, 42 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ¬ ((𝑉 + 1) + 1) ≤ (𝑉 + 1)) |
| 44 | | elfzle1 13567 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑉 + 1) ∈ (((𝑉 + 1) + 1)...𝑁) → ((𝑉 + 1) + 1) ≤ (𝑉 + 1)) |
| 45 | 43, 44 | nsyl 140 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ¬ (𝑉 + 1) ∈ (((𝑉 + 1) + 1)...𝑁)) |
| 46 | | difsn 4798 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
(𝑉 + 1) ∈ (((𝑉 + 1) + 1)...𝑁) → ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)}) = (((𝑉 + 1) + 1)...𝑁)) |
| 47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)}) = (((𝑉 + 1) + 1)...𝑁)) |
| 48 | 38, 47 | uneq12d 4169 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) ∪ ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)})) = ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁))) |
| 49 | 19, 48 | eqtrid 2789 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)) ∖ {(𝑉 + 1)}) = ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁))) |
| 50 | 18, 49 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((1...𝑁) ∖ {(𝑉 + 1)}) = ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁))) |
| 51 | 50 | imaeq2d 6078 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈 “ ((1...𝑁) ∖ {(𝑉 + 1)})) = (𝑈 “ ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁)))) |
| 52 | 6, 51 | eqtr3d 2779 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) = (𝑈 “ ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁)))) |
| 53 | | imaundi 6169 |
. . . . . . . . . . . . 13
⊢ (𝑈 “ ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) |
| 54 | 52, 53 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) = ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) |
| 55 | 54 | eleq2d 2827 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) ↔ 𝑛 ∈ ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))) |
| 56 | | eldif 3961 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)}))) |
| 57 | | elun 4153 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ↔ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) |
| 58 | 55, 56, 57 | 3bitr3g 313 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))) |
| 59 | 58 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))) |
| 60 | | imassrn 6089 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈 “ (1...𝑉)) ⊆ ran 𝑈 |
| 61 | | f1of 6848 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)⟶(1...𝑁)) |
| 62 | 1, 61 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑈:(1...𝑁)⟶(1...𝑁)) |
| 63 | 62 | frnd 6744 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ran 𝑈 ⊆ (1...𝑁)) |
| 64 | 60, 63 | sstrid 3995 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑈 “ (1...𝑉)) ⊆ (1...𝑁)) |
| 65 | 64 | sselda 3983 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → 𝑛 ∈ (1...𝑁)) |
| 66 | | poimirlem2.2 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑇:(1...𝑁)⟶ℤ) |
| 67 | 66 | ffnd 6737 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑇 Fn (1...𝑁)) |
| 68 | 67 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → 𝑇 Fn (1...𝑁)) |
| 69 | | 1ex 11257 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
V |
| 70 | | fnconstg 6796 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1 ∈
V → ((𝑈 “
(1...𝑉)) × {1}) Fn
(𝑈 “ (1...𝑉))) |
| 71 | 69, 70 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) |
| 72 | | c0ex 11255 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ∈
V |
| 73 | | fnconstg 6796 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (0 ∈
V → ((𝑈 “
((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁))) |
| 74 | 72, 73 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁)) |
| 75 | 71, 74 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁))) |
| 76 | | imain 6651 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (Fun
◡𝑈 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁)))) |
| 77 | 4, 76 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁)))) |
| 78 | | fzdisj 13591 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑉 < (𝑉 + 1) → ((1...𝑉) ∩ ((𝑉 + 1)...𝑁)) = ∅) |
| 79 | 28, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((1...𝑉) ∩ ((𝑉 + 1)...𝑁)) = ∅) |
| 80 | 79 | imaeq2d 6078 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = (𝑈 “ ∅)) |
| 81 | | ima0 6095 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑈 “ ∅) =
∅ |
| 82 | 80, 81 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = ∅) |
| 83 | 77, 82 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅) |
| 84 | | fnun 6682 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑈 “
(1...𝑉)) × {1}) Fn
(𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁)))) |
| 85 | 75, 83, 84 | sylancr 587 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁)))) |
| 86 | | imaundi 6169 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑈 “ ((1...𝑉) ∪ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))) |
| 87 | 10 | nnzd 12640 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 88 | | peano2zm 12660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
| 89 | | uzid 12893 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑁 − 1) ∈ ℤ
→ (𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1))) |
| 90 | | peano2uz 12943 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
| 91 | 87, 88, 89, 90 | 4syl 19 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
| 92 | 13, 91 | eqeltrrd 2842 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) |
| 93 | | fzss2 13604 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈
(ℤ≥‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁)) |
| 94 | 92, 93 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁)) |
| 95 | 94, 7 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑉 ∈ (1...𝑁)) |
| 96 | | fzsplit 13590 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑉 ∈ (1...𝑁) → (1...𝑁) = ((1...𝑉) ∪ ((𝑉 + 1)...𝑁))) |
| 97 | 95, 96 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (1...𝑁) = ((1...𝑉) ∪ ((𝑉 + 1)...𝑁))) |
| 98 | 97 | imaeq2d 6078 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...𝑉) ∪ ((𝑉 + 1)...𝑁)))) |
| 99 | | f1ofo 6855 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁)) |
| 100 | 1, 99 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑈:(1...𝑁)–onto→(1...𝑁)) |
| 101 | | foima 6825 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁)) |
| 102 | 100, 101 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁)) |
| 103 | 98, 102 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑈 “ ((1...𝑉) ∪ ((𝑉 + 1)...𝑁))) = (1...𝑁)) |
| 104 | 86, 103 | eqtr3id 2791 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))) = (1...𝑁)) |
| 105 | 104 | fneq2d 6662 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))) ↔ (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁))) |
| 106 | 85, 105 | mpbid 232 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
| 107 | 106 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
| 108 | | fzfid 14014 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → (1...𝑁) ∈ Fin) |
| 109 | | inidm 4227 |
. . . . . . . . . . . . . . . 16
⊢
((1...𝑁) ∩
(1...𝑁)) = (1...𝑁) |
| 110 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛)) |
| 111 | | fvun1 7000 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁)) ∧ (((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...𝑉)))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...𝑉)) × {1})‘𝑛)) |
| 112 | 71, 74, 111 | mp3an12 1453 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...𝑉)) × {1})‘𝑛)) |
| 113 | 83, 112 | sylan 580 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...𝑉)) × {1})‘𝑛)) |
| 114 | 69 | fvconst2 7224 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ (𝑈 “ (1...𝑉)) → (((𝑈 “ (1...𝑉)) × {1})‘𝑛) = 1) |
| 115 | 114 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → (((𝑈 “ (1...𝑉)) × {1})‘𝑛) = 1) |
| 116 | 113, 115 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1) |
| 117 | 116 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1) |
| 118 | 68, 107, 108, 108, 109, 110, 117 | ofval 7708 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1)) |
| 119 | | fnconstg 6796 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1 ∈
V → ((𝑈 “
(1...(𝑉 + 1))) × {1})
Fn (𝑈 “ (1...(𝑉 + 1)))) |
| 120 | 69, 119 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑈 “ (1...(𝑉 + 1))) × {1}) Fn (𝑈 “ (1...(𝑉 + 1))) |
| 121 | | fnconstg 6796 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (0 ∈
V → ((𝑈 “
(((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) |
| 122 | 72, 121 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) |
| 123 | 120, 122 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑈 “ (1...(𝑉 + 1))) × {1}) Fn (𝑈 “ (1...(𝑉 + 1))) ∧ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) |
| 124 | | imain 6651 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (Fun
◡𝑈 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) |
| 125 | 4, 124 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) |
| 126 | | fzdisj 13591 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑉 + 1) < ((𝑉 + 1) + 1) → ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁)) = ∅) |
| 127 | 39, 126 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁)) = ∅) |
| 128 | 127 | imaeq2d 6078 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = (𝑈 “ ∅)) |
| 129 | 128, 81 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = ∅) |
| 130 | 125, 129 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅) |
| 131 | | fnun 6682 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑈 “
(1...(𝑉 + 1))) × {1})
Fn (𝑈 “ (1...(𝑉 + 1))) ∧ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ ((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅) → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) |
| 132 | 123, 130,
131 | sylancr 587 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) |
| 133 | | imaundi 6169 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑈 “ ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) |
| 134 | 17 | imaeq2d 6078 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)))) |
| 135 | 134, 102 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁))) = (1...𝑁)) |
| 136 | 133, 135 | eqtr3id 2791 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = (1...𝑁)) |
| 137 | 136 | fneq2d 6662 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ↔ (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))) |
| 138 | 132, 137 | mpbid 232 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
| 139 | 138 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
| 140 | | uzid 12893 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑉 ∈ ℤ → 𝑉 ∈
(ℤ≥‘𝑉)) |
| 141 | 26, 140 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑉 ∈ (ℤ≥‘𝑉)) |
| 142 | | peano2uz 12943 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑉 ∈
(ℤ≥‘𝑉) → (𝑉 + 1) ∈
(ℤ≥‘𝑉)) |
| 143 | | fzss2 13604 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑉 + 1) ∈
(ℤ≥‘𝑉) → (1...𝑉) ⊆ (1...(𝑉 + 1))) |
| 144 | | imass2 6120 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1...𝑉) ⊆
(1...(𝑉 + 1)) → (𝑈 “ (1...𝑉)) ⊆ (𝑈 “ (1...(𝑉 + 1)))) |
| 145 | 141, 142,
143, 144 | 4syl 19 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑈 “ (1...𝑉)) ⊆ (𝑈 “ (1...(𝑉 + 1)))) |
| 146 | 145 | sselda 3983 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) |
| 147 | | fvun1 7000 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑈 “ (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})‘𝑛)) |
| 148 | 120, 122,
147 | mp3an12 1453 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛)) |
| 149 | 130, 148 | sylan 580 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛)) |
| 150 | 69 | fvconst2 7224 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ (𝑈 “ (1...(𝑉 + 1))) → (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛) = 1) |
| 151 | 150 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛) = 1) |
| 152 | 149, 151 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1) |
| 153 | 146, 152 | syldan 591 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1) |
| 154 | 153 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1) |
| 155 | 68, 139, 108, 108, 109, 110, 154 | ofval 7708 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1)) |
| 156 | 118, 155 | eqtr4d 2780 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛)) |
| 157 | 65, 156 | mpdan 687 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛)) |
| 158 | | imassrn 6089 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ ran 𝑈 |
| 159 | 158, 63 | sstrid 3995 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ (1...𝑁)) |
| 160 | 159 | sselda 3983 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → 𝑛 ∈ (1...𝑁)) |
| 161 | 67 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → 𝑇 Fn (1...𝑁)) |
| 162 | 106 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
| 163 | | fzfid 14014 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (1...𝑁) ∈ Fin) |
| 164 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛)) |
| 165 | | uzid 12893 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑉 + 1) ∈ ℤ →
(𝑉 + 1) ∈
(ℤ≥‘(𝑉 + 1))) |
| 166 | 29, 165 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑉 + 1) ∈
(ℤ≥‘(𝑉 + 1))) |
| 167 | | peano2uz 12943 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑉 + 1) ∈
(ℤ≥‘(𝑉 + 1)) → ((𝑉 + 1) + 1) ∈
(ℤ≥‘(𝑉 + 1))) |
| 168 | | fzss1 13603 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑉 + 1) + 1) ∈
(ℤ≥‘(𝑉 + 1)) → (((𝑉 + 1) + 1)...𝑁) ⊆ ((𝑉 + 1)...𝑁)) |
| 169 | | imass2 6120 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑉 + 1) + 1)...𝑁) ⊆ ((𝑉 + 1)...𝑁) → (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ (𝑈 “ ((𝑉 + 1)...𝑁))) |
| 170 | 166, 167,
168, 169 | 4syl 19 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ (𝑈 “ ((𝑉 + 1)...𝑁))) |
| 171 | 170 | sselda 3983 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) |
| 172 | | fvun2 7001 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁)) ∧ (((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛)) |
| 173 | 71, 74, 172 | mp3an12 1453 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛)) |
| 174 | 83, 173 | sylan 580 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛)) |
| 175 | 72 | fvconst2 7224 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)) → (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛) = 0) |
| 176 | 175 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛) = 0) |
| 177 | 174, 176 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0) |
| 178 | 171, 177 | syldan 591 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0) |
| 179 | 178 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0) |
| 180 | 161, 162,
163, 163, 109, 164, 179 | ofval 7708 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0)) |
| 181 | 138 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
| 182 | | fvun2 7001 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑈 “ (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)...𝑁)) × {0})‘𝑛)) |
| 183 | 120, 122,
182 | mp3an12 1453 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛)) |
| 184 | 130, 183 | sylan 580 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛)) |
| 185 | 72 | fvconst2 7224 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) → (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛) = 0) |
| 186 | 185 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛) = 0) |
| 187 | 184, 186 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 0) |
| 188 | 187 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 0) |
| 189 | 161, 181,
163, 163, 109, 164, 188 | ofval 7708 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0)) |
| 190 | 180, 189 | eqtr4d 2780 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛)) |
| 191 | 160, 190 | mpdan 687 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛)) |
| 192 | 157, 191 | jaodan 960 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛)) |
| 193 | 192 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛)) |
| 194 | | poimirlem2.1 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))) |
| 195 | 194 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))) |
| 196 | | vex 3484 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑦 ∈ V |
| 197 | | ovex 7464 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 + 1) ∈ V |
| 198 | 196, 197 | ifex 4576 |
. . . . . . . . . . . . . . . 16
⊢ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V |
| 199 | 198 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V) |
| 200 | | breq1 5146 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = (𝑉 − 1) → (𝑦 < 𝑀 ↔ (𝑉 − 1) < 𝑀)) |
| 201 | 200 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 = (𝑉 − 1)) → (𝑦 < 𝑀 ↔ (𝑉 − 1) < 𝑀)) |
| 202 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 = (𝑉 − 1)) → 𝑦 = (𝑉 − 1)) |
| 203 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = (𝑉 − 1) → (𝑦 + 1) = ((𝑉 − 1) + 1)) |
| 204 | 26 | zcnd 12723 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑉 ∈ ℂ) |
| 205 | | npcan1 11688 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑉 ∈ ℂ → ((𝑉 − 1) + 1) = 𝑉) |
| 206 | 204, 205 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((𝑉 − 1) + 1) = 𝑉) |
| 207 | 203, 206 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 = (𝑉 − 1)) → (𝑦 + 1) = 𝑉) |
| 208 | 201, 202,
207 | ifbieq12d 4554 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉)) |
| 209 | 208 | adantlr 715 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉)) |
| 210 | | poimirlem2.5 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝑀 ∈ ((0...𝑁) ∖ {𝑉})) |
| 211 | 210 | eldifad 3963 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑀 ∈ (0...𝑁)) |
| 212 | 211 | elfzelzd 13565 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 213 | | zltlem1 12670 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑀 ∈ ℤ ∧ 𝑉 ∈ ℤ) → (𝑀 < 𝑉 ↔ 𝑀 ≤ (𝑉 − 1))) |
| 214 | 212, 26, 213 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑀 < 𝑉 ↔ 𝑀 ≤ (𝑉 − 1))) |
| 215 | 212 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 216 | | peano2zm 12660 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑉 ∈ ℤ → (𝑉 − 1) ∈
ℤ) |
| 217 | 26, 216 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝑉 − 1) ∈ ℤ) |
| 218 | 217 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑉 − 1) ∈ ℝ) |
| 219 | 215, 218 | lenltd 11407 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑀 ≤ (𝑉 − 1) ↔ ¬ (𝑉 − 1) < 𝑀)) |
| 220 | 214, 219 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑀 < 𝑉 ↔ ¬ (𝑉 − 1) < 𝑀)) |
| 221 | 220 | biimpa 476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ¬ (𝑉 − 1) < 𝑀) |
| 222 | 221 | iffalsed 4536 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = 𝑉) |
| 223 | 222 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = 𝑉) |
| 224 | 209, 223 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = 𝑉) |
| 225 | 224 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → (𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ↔ 𝑗 = 𝑉)) |
| 226 | 225 | biimpa 476 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → 𝑗 = 𝑉) |
| 227 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = 𝑉 → (1...𝑗) = (1...𝑉)) |
| 228 | 227 | imaeq2d 6078 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = 𝑉 → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...𝑉))) |
| 229 | 228 | xpeq1d 5714 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑉 → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...𝑉)) × {1})) |
| 230 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 𝑉 → (𝑗 + 1) = (𝑉 + 1)) |
| 231 | 230 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = 𝑉 → ((𝑗 + 1)...𝑁) = ((𝑉 + 1)...𝑁)) |
| 232 | 231 | imaeq2d 6078 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = 𝑉 → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ ((𝑉 + 1)...𝑁))) |
| 233 | 232 | xpeq1d 5714 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑉 → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) |
| 234 | 229, 233 | uneq12d 4169 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑉 → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))) |
| 235 | 234 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑉 → (𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))) |
| 236 | 226, 235 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → (𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))) |
| 237 | 199, 236 | csbied 3935 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))) |
| 238 | | elfzm1b 13642 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑉 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑉 ∈ (1...𝑁) ↔ (𝑉 − 1) ∈ (0...(𝑁 − 1)))) |
| 239 | 26, 87, 238 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑉 ∈ (1...𝑁) ↔ (𝑉 − 1) ∈ (0...(𝑁 − 1)))) |
| 240 | 95, 239 | mpbid 232 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑉 − 1) ∈ (0...(𝑁 − 1))) |
| 241 | 240 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → (𝑉 − 1) ∈ (0...(𝑁 − 1))) |
| 242 | | ovexd 7466 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))) ∈ V) |
| 243 | 195, 237,
241, 242 | fvmptd 7023 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → (𝐹‘(𝑉 − 1)) = (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))) |
| 244 | 243 | fveq1d 6908 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛)) |
| 245 | 244 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛)) |
| 246 | 198 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V) |
| 247 | | breq1 5146 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑉 → (𝑦 < 𝑀 ↔ 𝑉 < 𝑀)) |
| 248 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑉 → 𝑦 = 𝑉) |
| 249 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑉 → (𝑦 + 1) = (𝑉 + 1)) |
| 250 | 247, 248,
249 | ifbieq12d 4554 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑉 → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if(𝑉 < 𝑀, 𝑉, (𝑉 + 1))) |
| 251 | | ltnsym 11359 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑀 < 𝑉 → ¬ 𝑉 < 𝑀)) |
| 252 | 215, 27, 251 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑀 < 𝑉 → ¬ 𝑉 < 𝑀)) |
| 253 | 252 | imp 406 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ¬ 𝑉 < 𝑀) |
| 254 | 253 | iffalsed 4536 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → if(𝑉 < 𝑀, 𝑉, (𝑉 + 1)) = (𝑉 + 1)) |
| 255 | 250, 254 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑉 + 1)) |
| 256 | 255 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → (𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ↔ 𝑗 = (𝑉 + 1))) |
| 257 | 256 | biimpa 476 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → 𝑗 = (𝑉 + 1)) |
| 258 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = (𝑉 + 1) → (1...𝑗) = (1...(𝑉 + 1))) |
| 259 | 258 | imaeq2d 6078 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = (𝑉 + 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑉 + 1)))) |
| 260 | 259 | xpeq1d 5714 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = (𝑉 + 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑉 + 1))) × {1})) |
| 261 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = (𝑉 + 1) → (𝑗 + 1) = ((𝑉 + 1) + 1)) |
| 262 | 261 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = (𝑉 + 1) → ((𝑗 + 1)...𝑁) = (((𝑉 + 1) + 1)...𝑁)) |
| 263 | 262 | imaeq2d 6078 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = (𝑉 + 1) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) |
| 264 | 263 | xpeq1d 5714 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = (𝑉 + 1) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) |
| 265 | 260, 264 | uneq12d 4169 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = (𝑉 + 1) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))) |
| 266 | 265 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = (𝑉 + 1) → (𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))) |
| 267 | 257, 266 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → (𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))) |
| 268 | 246, 267 | csbied 3935 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))) |
| 269 | | fz1ssfz0 13663 |
. . . . . . . . . . . . . . . 16
⊢
(1...(𝑁 − 1))
⊆ (0...(𝑁 −
1)) |
| 270 | 269, 7 | sselid 3981 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑉 ∈ (0...(𝑁 − 1))) |
| 271 | 270 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → 𝑉 ∈ (0...(𝑁 − 1))) |
| 272 | | ovexd 7466 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → (𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))) ∈ V) |
| 273 | 195, 268,
271, 272 | fvmptd 7023 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → (𝐹‘𝑉) = (𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))) |
| 274 | 273 | fveq1d 6908 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ((𝐹‘𝑉)‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛)) |
| 275 | 274 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝐹‘𝑉)‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛)) |
| 276 | 193, 245,
275 | 3eqtr4d 2787 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)) |
| 277 | 276 | ex 412 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ((𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛))) |
| 278 | 59, 277 | sylbid 240 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛))) |
| 279 | 278 | expdimp 452 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛))) |
| 280 | 279 | necon1ad 2957 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 ∈ (𝑈 “ {(𝑉 + 1)}))) |
| 281 | | elimasni 6109 |
. . . . . . . 8
⊢ (𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → (𝑉 + 1)𝑈𝑛) |
| 282 | | eqcom 2744 |
. . . . . . . . 9
⊢ (𝑛 = (𝑈‘(𝑉 + 1)) ↔ (𝑈‘(𝑉 + 1)) = 𝑛) |
| 283 | | f1ofn 6849 |
. . . . . . . . . . 11
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 Fn (1...𝑁)) |
| 284 | 1, 283 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑈 Fn (1...𝑁)) |
| 285 | | fnbrfvb 6959 |
. . . . . . . . . 10
⊢ ((𝑈 Fn (1...𝑁) ∧ (𝑉 + 1) ∈ (1...𝑁)) → ((𝑈‘(𝑉 + 1)) = 𝑛 ↔ (𝑉 + 1)𝑈𝑛)) |
| 286 | 284, 15, 285 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑈‘(𝑉 + 1)) = 𝑛 ↔ (𝑉 + 1)𝑈𝑛)) |
| 287 | 282, 286 | bitrid 283 |
. . . . . . . 8
⊢ (𝜑 → (𝑛 = (𝑈‘(𝑉 + 1)) ↔ (𝑉 + 1)𝑈𝑛)) |
| 288 | 281, 287 | imbitrrid 246 |
. . . . . . 7
⊢ (𝜑 → (𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → 𝑛 = (𝑈‘(𝑉 + 1)))) |
| 289 | 288 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → 𝑛 = (𝑈‘(𝑉 + 1)))) |
| 290 | 280, 289 | syld 47 |
. . . . 5
⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1)))) |
| 291 | 290 | ralrimiva 3146 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1)))) |
| 292 | | fvex 6919 |
. . . . 5
⊢ (𝑈‘(𝑉 + 1)) ∈ V |
| 293 | | eqeq2 2749 |
. . . . . . 7
⊢ (𝑚 = (𝑈‘(𝑉 + 1)) → (𝑛 = 𝑚 ↔ 𝑛 = (𝑈‘(𝑉 + 1)))) |
| 294 | 293 | imbi2d 340 |
. . . . . 6
⊢ (𝑚 = (𝑈‘(𝑉 + 1)) → ((((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1))))) |
| 295 | 294 | ralbidv 3178 |
. . . . 5
⊢ (𝑚 = (𝑈‘(𝑉 + 1)) → (∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1))))) |
| 296 | 292, 295 | spcev 3606 |
. . . 4
⊢
(∀𝑛 ∈
(𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1))) → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚)) |
| 297 | 291, 296 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚)) |
| 298 | | imadif 6650 |
. . . . . . . . . . . . . . 15
⊢ (Fun
◡𝑈 → (𝑈 “ ((1...𝑁) ∖ {𝑉})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉}))) |
| 299 | 4, 298 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑉})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉}))) |
| 300 | 97 | difeq1d 4125 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1...𝑁) ∖ {𝑉}) = (((1...𝑉) ∪ ((𝑉 + 1)...𝑁)) ∖ {𝑉})) |
| 301 | | difundir 4291 |
. . . . . . . . . . . . . . . . 17
⊢
(((1...𝑉) ∪
((𝑉 + 1)...𝑁)) ∖ {𝑉}) = (((1...𝑉) ∖ {𝑉}) ∪ (((𝑉 + 1)...𝑁) ∖ {𝑉})) |
| 302 | 206, 21 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((𝑉 − 1) + 1) ∈
(ℤ≥‘1)) |
| 303 | | uzid 12893 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑉 − 1) ∈ ℤ
→ (𝑉 − 1) ∈
(ℤ≥‘(𝑉 − 1))) |
| 304 | | peano2uz 12943 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑉 − 1) ∈
(ℤ≥‘(𝑉 − 1)) → ((𝑉 − 1) + 1) ∈
(ℤ≥‘(𝑉 − 1))) |
| 305 | 26, 216, 303, 304 | 4syl 19 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((𝑉 − 1) + 1) ∈
(ℤ≥‘(𝑉 − 1))) |
| 306 | 206, 305 | eqeltrrd 2842 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑉 ∈ (ℤ≥‘(𝑉 − 1))) |
| 307 | | fzsplit2 13589 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑉 − 1) + 1) ∈
(ℤ≥‘1) ∧ 𝑉 ∈ (ℤ≥‘(𝑉 − 1))) → (1...𝑉) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑉))) |
| 308 | 302, 306,
307 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (1...𝑉) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑉))) |
| 309 | 206 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (((𝑉 − 1) + 1)...𝑉) = (𝑉...𝑉)) |
| 310 | | fzsn 13606 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑉 ∈ ℤ → (𝑉...𝑉) = {𝑉}) |
| 311 | 26, 310 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑉...𝑉) = {𝑉}) |
| 312 | 309, 311 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (((𝑉 − 1) + 1)...𝑉) = {𝑉}) |
| 313 | 312 | uneq2d 4168 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑉)) = ((1...(𝑉 − 1)) ∪ {𝑉})) |
| 314 | 308, 313 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1...𝑉) = ((1...(𝑉 − 1)) ∪ {𝑉})) |
| 315 | 314 | difeq1d 4125 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((1...𝑉) ∖ {𝑉}) = (((1...(𝑉 − 1)) ∪ {𝑉}) ∖ {𝑉})) |
| 316 | | difun2 4481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((1...(𝑉 −
1)) ∪ {𝑉}) ∖
{𝑉}) = ((1...(𝑉 − 1)) ∖ {𝑉}) |
| 317 | 27 | ltm1d 12200 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑉 − 1) < 𝑉) |
| 318 | 218, 27 | ltnled 11408 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((𝑉 − 1) < 𝑉 ↔ ¬ 𝑉 ≤ (𝑉 − 1))) |
| 319 | 317, 318 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ¬ 𝑉 ≤ (𝑉 − 1)) |
| 320 | | elfzle2 13568 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑉 ∈ (1...(𝑉 − 1)) → 𝑉 ≤ (𝑉 − 1)) |
| 321 | 319, 320 | nsyl 140 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ¬ 𝑉 ∈ (1...(𝑉 − 1))) |
| 322 | | difsn 4798 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
𝑉 ∈ (1...(𝑉 − 1)) → ((1...(𝑉 − 1)) ∖ {𝑉}) = (1...(𝑉 − 1))) |
| 323 | 321, 322 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((1...(𝑉 − 1)) ∖ {𝑉}) = (1...(𝑉 − 1))) |
| 324 | 316, 323 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((1...(𝑉 − 1)) ∪ {𝑉}) ∖ {𝑉}) = (1...(𝑉 − 1))) |
| 325 | 315, 324 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((1...𝑉) ∖ {𝑉}) = (1...(𝑉 − 1))) |
| 326 | | elfzle1 13567 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑉 ∈ ((𝑉 + 1)...𝑁) → (𝑉 + 1) ≤ 𝑉) |
| 327 | 32, 326 | nsyl 140 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ¬ 𝑉 ∈ ((𝑉 + 1)...𝑁)) |
| 328 | | difsn 4798 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑉 ∈ ((𝑉 + 1)...𝑁) → (((𝑉 + 1)...𝑁) ∖ {𝑉}) = ((𝑉 + 1)...𝑁)) |
| 329 | 327, 328 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝑉 + 1)...𝑁) ∖ {𝑉}) = ((𝑉 + 1)...𝑁)) |
| 330 | 325, 329 | uneq12d 4169 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((1...𝑉) ∖ {𝑉}) ∪ (((𝑉 + 1)...𝑁) ∖ {𝑉})) = ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁))) |
| 331 | 301, 330 | eqtrid 2789 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((1...𝑉) ∪ ((𝑉 + 1)...𝑁)) ∖ {𝑉}) = ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁))) |
| 332 | 300, 331 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((1...𝑁) ∖ {𝑉}) = ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁))) |
| 333 | 332 | imaeq2d 6078 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑉})) = (𝑈 “ ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁)))) |
| 334 | 299, 333 | eqtr3d 2779 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) = (𝑈 “ ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁)))) |
| 335 | | imaundi 6169 |
. . . . . . . . . . . . 13
⊢ (𝑈 “ ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))) |
| 336 | 334, 335 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) = ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁)))) |
| 337 | 336 | eleq2d 2827 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) ↔ 𝑛 ∈ ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))))) |
| 338 | | eldif 3961 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉}))) |
| 339 | | elun 4153 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))) ↔ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) |
| 340 | 337, 338,
339 | 3bitr3g 313 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉})) ↔ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))))) |
| 341 | 340 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉})) ↔ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))))) |
| 342 | | imassrn 6089 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈 “ (1...(𝑉 − 1))) ⊆ ran 𝑈 |
| 343 | 342, 63 | sstrid 3995 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑈 “ (1...(𝑉 − 1))) ⊆ (1...𝑁)) |
| 344 | 343 | sselda 3983 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → 𝑛 ∈ (1...𝑁)) |
| 345 | 67 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → 𝑇 Fn (1...𝑁)) |
| 346 | | fnconstg 6796 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1 ∈
V → ((𝑈 “
(1...(𝑉 − 1)))
× {1}) Fn (𝑈 “
(1...(𝑉 −
1)))) |
| 347 | 69, 346 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) |
| 348 | | fnconstg 6796 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (0 ∈
V → ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁))) |
| 349 | 72, 348 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁)) |
| 350 | 347, 349 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) ∧ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁))) |
| 351 | | imain 6651 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (Fun
◡𝑈 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁)))) |
| 352 | 4, 351 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁)))) |
| 353 | | fzdisj 13591 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑉 − 1) < 𝑉 → ((1...(𝑉 − 1)) ∩ (𝑉...𝑁)) = ∅) |
| 354 | 317, 353 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((1...(𝑉 − 1)) ∩ (𝑉...𝑁)) = ∅) |
| 355 | 354 | imaeq2d 6078 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = (𝑈 “ ∅)) |
| 356 | 355, 81 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = ∅) |
| 357 | 352, 356 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅) |
| 358 | | fnun 6682 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑈 “
(1...(𝑉 − 1)))
× {1}) Fn (𝑈 “
(1...(𝑉 − 1))) ∧
((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁))) ∧ ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅) → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁)))) |
| 359 | 350, 357,
358 | sylancr 587 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁)))) |
| 360 | | imaundi 6169 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑈 “ ((1...(𝑉 − 1)) ∪ (𝑉...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁))) |
| 361 | | uzss 12901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑉 ∈
(ℤ≥‘(𝑉 − 1)) →
(ℤ≥‘𝑉) ⊆
(ℤ≥‘(𝑉 − 1))) |
| 362 | 306, 361 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 →
(ℤ≥‘𝑉) ⊆
(ℤ≥‘(𝑉 − 1))) |
| 363 | | elfzuz3 13561 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑉 ∈ (1...(𝑁 − 1)) → (𝑁 − 1) ∈
(ℤ≥‘𝑉)) |
| 364 | 7, 363 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝑁 − 1) ∈
(ℤ≥‘𝑉)) |
| 365 | 362, 364 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝑁 − 1) ∈
(ℤ≥‘(𝑉 − 1))) |
| 366 | | peano2uz 12943 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑁 − 1) ∈
(ℤ≥‘(𝑉 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑉 − 1))) |
| 367 | 365, 366 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑉 − 1))) |
| 368 | 13, 367 | eqeltrrd 2842 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑉 − 1))) |
| 369 | | fzsplit2 13589 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑉 − 1) + 1) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘(𝑉 − 1))) → (1...𝑁) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑁))) |
| 370 | 302, 368,
369 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (1...𝑁) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑁))) |
| 371 | 206 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (((𝑉 − 1) + 1)...𝑁) = (𝑉...𝑁)) |
| 372 | 371 | uneq2d 4168 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑁)) = ((1...(𝑉 − 1)) ∪ (𝑉...𝑁))) |
| 373 | 370, 372 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (1...𝑁) = ((1...(𝑉 − 1)) ∪ (𝑉...𝑁))) |
| 374 | 373 | imaeq2d 6078 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑉 − 1)) ∪ (𝑉...𝑁)))) |
| 375 | 374, 102 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∪ (𝑉...𝑁))) = (1...𝑁)) |
| 376 | 360, 375 | eqtr3id 2791 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁))) = (1...𝑁)) |
| 377 | 376 | fneq2d 6662 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁))) ↔ (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁))) |
| 378 | 359, 377 | mpbid 232 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁)) |
| 379 | 378 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁)) |
| 380 | | fzfid 14014 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (1...𝑁) ∈ Fin) |
| 381 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛)) |
| 382 | | fvun1 7000 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) ∧ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁)) ∧ (((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛)) |
| 383 | 347, 349,
382 | mp3an12 1453 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛)) |
| 384 | 357, 383 | sylan 580 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛)) |
| 385 | 69 | fvconst2 7224 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) → (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛) = 1) |
| 386 | 385 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛) = 1) |
| 387 | 384, 386 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 1) |
| 388 | 387 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 1) |
| 389 | 345, 379,
380, 380, 109, 381, 388 | ofval 7708 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1)) |
| 390 | 106 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
| 391 | | fzss2 13604 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑉 ∈
(ℤ≥‘(𝑉 − 1)) → (1...(𝑉 − 1)) ⊆ (1...𝑉)) |
| 392 | 306, 391 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1...(𝑉 − 1)) ⊆ (1...𝑉)) |
| 393 | | imass2 6120 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1...(𝑉 − 1))
⊆ (1...𝑉) →
(𝑈 “ (1...(𝑉 − 1))) ⊆ (𝑈 “ (1...𝑉))) |
| 394 | 392, 393 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑈 “ (1...(𝑉 − 1))) ⊆ (𝑈 “ (1...𝑉))) |
| 395 | 394 | sselda 3983 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → 𝑛 ∈ (𝑈 “ (1...𝑉))) |
| 396 | 395, 116 | syldan 591 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1) |
| 397 | 396 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1) |
| 398 | 345, 390,
380, 380, 109, 381, 397 | ofval 7708 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1)) |
| 399 | 389, 398 | eqtr4d 2780 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛)) |
| 400 | 344, 399 | mpdan 687 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛)) |
| 401 | | imassrn 6089 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ ran 𝑈 |
| 402 | 401, 63 | sstrid 3995 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ (1...𝑁)) |
| 403 | 402 | sselda 3983 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → 𝑛 ∈ (1...𝑁)) |
| 404 | 67 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → 𝑇 Fn (1...𝑁)) |
| 405 | 378 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁)) |
| 406 | | fzfid 14014 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (1...𝑁) ∈ Fin) |
| 407 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛)) |
| 408 | | fzss1 13603 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑉 + 1) ∈
(ℤ≥‘𝑉) → ((𝑉 + 1)...𝑁) ⊆ (𝑉...𝑁)) |
| 409 | | imass2 6120 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑉 + 1)...𝑁) ⊆ (𝑉...𝑁) → (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ (𝑈 “ (𝑉...𝑁))) |
| 410 | 141, 142,
408, 409 | 4syl 19 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ (𝑈 “ (𝑉...𝑁))) |
| 411 | 410 | sselda 3983 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → 𝑛 ∈ (𝑈 “ (𝑉...𝑁))) |
| 412 | | fvun2 7001 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) ∧ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁)) ∧ (((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛)) |
| 413 | 347, 349,
412 | mp3an12 1453 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛)) |
| 414 | 357, 413 | sylan 580 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛)) |
| 415 | 72 | fvconst2 7224 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ (𝑈 “ (𝑉...𝑁)) → (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛) = 0) |
| 416 | 415 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛) = 0) |
| 417 | 414, 416 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 0) |
| 418 | 411, 417 | syldan 591 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 0) |
| 419 | 418 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 0) |
| 420 | 404, 405,
406, 406, 109, 407, 419 | ofval 7708 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0)) |
| 421 | 106 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
| 422 | 177 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0) |
| 423 | 404, 421,
406, 406, 109, 407, 422 | ofval 7708 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0)) |
| 424 | 420, 423 | eqtr4d 2780 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛)) |
| 425 | 403, 424 | mpdan 687 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛)) |
| 426 | 400, 425 | jaodan 960 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛)) |
| 427 | 426 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛)) |
| 428 | 194 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))) |
| 429 | 198 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V) |
| 430 | 208 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉)) |
| 431 | | lttr 11337 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑉 − 1) ∈ ℝ ∧
𝑉 ∈ ℝ ∧
𝑀 ∈ ℝ) →
(((𝑉 − 1) < 𝑉 ∧ 𝑉 < 𝑀) → (𝑉 − 1) < 𝑀)) |
| 432 | 218, 27, 215, 431 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((𝑉 − 1) < 𝑉 ∧ 𝑉 < 𝑀) → (𝑉 − 1) < 𝑀)) |
| 433 | 317, 432 | mpand 695 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑉 < 𝑀 → (𝑉 − 1) < 𝑀)) |
| 434 | 433 | imp 406 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → (𝑉 − 1) < 𝑀) |
| 435 | 434 | iftrued 4533 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = (𝑉 − 1)) |
| 436 | 435 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = (𝑉 − 1)) |
| 437 | 430, 436 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑉 − 1)) |
| 438 | | simpll 767 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → 𝜑) |
| 439 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = (𝑉 − 1) → (1...𝑗) = (1...(𝑉 − 1))) |
| 440 | 439 | imaeq2d 6078 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = (𝑉 − 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑉 − 1)))) |
| 441 | 440 | xpeq1d 5714 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = (𝑉 − 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑉 − 1))) × {1})) |
| 442 | 441 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑉 − 1))) × {1})) |
| 443 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = (𝑉 − 1) → (𝑗 + 1) = ((𝑉 − 1) + 1)) |
| 444 | 443, 206 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → (𝑗 + 1) = 𝑉) |
| 445 | 444 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → ((𝑗 + 1)...𝑁) = (𝑉...𝑁)) |
| 446 | 445 | imaeq2d 6078 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (𝑉...𝑁))) |
| 447 | 446 | xpeq1d 5714 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (𝑉...𝑁)) × {0})) |
| 448 | 442, 447 | uneq12d 4169 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))) |
| 449 | 448 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → (𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))) |
| 450 | 438, 449 | sylan 580 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) ∧ 𝑗 = (𝑉 − 1)) → (𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))) |
| 451 | 429, 437,
450 | csbied2 3936 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))) |
| 452 | 240 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → (𝑉 − 1) ∈ (0...(𝑁 − 1))) |
| 453 | | ovexd 7466 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → (𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))) ∈ V) |
| 454 | 428, 451,
452, 453 | fvmptd 7023 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → (𝐹‘(𝑉 − 1)) = (𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))) |
| 455 | 454 | fveq1d 6908 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛)) |
| 456 | 455 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛)) |
| 457 | 198 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V) |
| 458 | | iftrue 4531 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑉 < 𝑀 → if(𝑉 < 𝑀, 𝑉, (𝑉 + 1)) = 𝑉) |
| 459 | 250, 458 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = 𝑉) |
| 460 | 459 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) → (𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ↔ 𝑗 = 𝑉)) |
| 461 | 460 | biimpa 476 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → 𝑗 = 𝑉) |
| 462 | 461, 235 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → (𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))) |
| 463 | 457, 462 | csbied 3935 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))) |
| 464 | 463 | adantll 714 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = 𝑉) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))) |
| 465 | 270 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → 𝑉 ∈ (0...(𝑁 − 1))) |
| 466 | | ovexd 7466 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))) ∈ V) |
| 467 | 428, 464,
465, 466 | fvmptd 7023 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → (𝐹‘𝑉) = (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))) |
| 468 | 467 | fveq1d 6908 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ((𝐹‘𝑉)‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛)) |
| 469 | 468 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝐹‘𝑉)‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛)) |
| 470 | 427, 456,
469 | 3eqtr4d 2787 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)) |
| 471 | 470 | ex 412 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ((𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛))) |
| 472 | 341, 471 | sylbid 240 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉})) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛))) |
| 473 | 472 | expdimp 452 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (¬ 𝑛 ∈ (𝑈 “ {𝑉}) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛))) |
| 474 | 473 | necon1ad 2957 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 ∈ (𝑈 “ {𝑉}))) |
| 475 | | elimasni 6109 |
. . . . . . . 8
⊢ (𝑛 ∈ (𝑈 “ {𝑉}) → 𝑉𝑈𝑛) |
| 476 | | eqcom 2744 |
. . . . . . . . 9
⊢ (𝑛 = (𝑈‘𝑉) ↔ (𝑈‘𝑉) = 𝑛) |
| 477 | | fnbrfvb 6959 |
. . . . . . . . . 10
⊢ ((𝑈 Fn (1...𝑁) ∧ 𝑉 ∈ (1...𝑁)) → ((𝑈‘𝑉) = 𝑛 ↔ 𝑉𝑈𝑛)) |
| 478 | 284, 95, 477 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑈‘𝑉) = 𝑛 ↔ 𝑉𝑈𝑛)) |
| 479 | 476, 478 | bitrid 283 |
. . . . . . . 8
⊢ (𝜑 → (𝑛 = (𝑈‘𝑉) ↔ 𝑉𝑈𝑛)) |
| 480 | 475, 479 | imbitrrid 246 |
. . . . . . 7
⊢ (𝜑 → (𝑛 ∈ (𝑈 “ {𝑉}) → 𝑛 = (𝑈‘𝑉))) |
| 481 | 480 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (𝑛 ∈ (𝑈 “ {𝑉}) → 𝑛 = (𝑈‘𝑉))) |
| 482 | 474, 481 | syld 47 |
. . . . 5
⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉))) |
| 483 | 482 | ralrimiva 3146 |
. . . 4
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉))) |
| 484 | | fvex 6919 |
. . . . 5
⊢ (𝑈‘𝑉) ∈ V |
| 485 | | eqeq2 2749 |
. . . . . . 7
⊢ (𝑚 = (𝑈‘𝑉) → (𝑛 = 𝑚 ↔ 𝑛 = (𝑈‘𝑉))) |
| 486 | 485 | imbi2d 340 |
. . . . . 6
⊢ (𝑚 = (𝑈‘𝑉) → ((((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉)))) |
| 487 | 486 | ralbidv 3178 |
. . . . 5
⊢ (𝑚 = (𝑈‘𝑉) → (∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉)))) |
| 488 | 484, 487 | spcev 3606 |
. . . 4
⊢
(∀𝑛 ∈
(𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉)) → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚)) |
| 489 | 483, 488 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚)) |
| 490 | | eldifsni 4790 |
. . . . 5
⊢ (𝑀 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑀 ≠ 𝑉) |
| 491 | 210, 490 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑀 ≠ 𝑉) |
| 492 | 215, 27 | lttri2d 11400 |
. . . 4
⊢ (𝜑 → (𝑀 ≠ 𝑉 ↔ (𝑀 < 𝑉 ∨ 𝑉 < 𝑀))) |
| 493 | 491, 492 | mpbid 232 |
. . 3
⊢ (𝜑 → (𝑀 < 𝑉 ∨ 𝑉 < 𝑀)) |
| 494 | 297, 489,
493 | mpjaodan 961 |
. 2
⊢ (𝜑 → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚)) |
| 495 | | nfv 1914 |
. . . 4
⊢
Ⅎ𝑚((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) |
| 496 | 495 | rmo2 3887 |
. . 3
⊢
(∃*𝑛 ∈
(𝑈 “ (1...𝑁))((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) ↔ ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚)) |
| 497 | | rmoeq1 3416 |
. . . 4
⊢ ((𝑈 “ (1...𝑁)) = (1...𝑁) → (∃*𝑛 ∈ (𝑈 “ (1...𝑁))((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) ↔ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛))) |
| 498 | 1, 99, 101, 497 | 4syl 19 |
. . 3
⊢ (𝜑 → (∃*𝑛 ∈ (𝑈 “ (1...𝑁))((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) ↔ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛))) |
| 499 | 496, 498 | bitr3id 285 |
. 2
⊢ (𝜑 → (∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛))) |
| 500 | 494, 499 | mpbid 232 |
1
⊢ (𝜑 → ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛)) |