| Step | Hyp | Ref
| Expression |
| 1 | | poimirlem2.3 |
. . . . 5
⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁)) |
| 2 | | f1of 6848 |
. . . . 5
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)⟶(1...𝑁)) |
| 3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑈:(1...𝑁)⟶(1...𝑁)) |
| 4 | | poimir.0 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 5 | 4 | nncnd 12282 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℂ) |
| 6 | | npcan1 11688 |
. . . . . . . 8
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
| 7 | 5, 6 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
| 8 | 4 | nnzd 12640 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 9 | | peano2zm 12660 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
| 10 | | uzid 12893 |
. . . . . . . 8
⊢ ((𝑁 − 1) ∈ ℤ
→ (𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1))) |
| 11 | | peano2uz 12943 |
. . . . . . . 8
⊢ ((𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
| 12 | 8, 9, 10, 11 | 4syl 19 |
. . . . . . 7
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
| 13 | 7, 12 | eqeltrrd 2842 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) |
| 14 | | fzss2 13604 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁)) |
| 15 | 13, 14 | syl 17 |
. . . . 5
⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁)) |
| 16 | | poimirlem1.4 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 − 1))) |
| 17 | 15, 16 | sseldd 3984 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ (1...𝑁)) |
| 18 | 3, 17 | ffvelcdmd 7105 |
. . 3
⊢ (𝜑 → (𝑈‘𝑀) ∈ (1...𝑁)) |
| 19 | | fzp1elp1 13617 |
. . . . . 6
⊢ (𝑀 ∈ (1...(𝑁 − 1)) → (𝑀 + 1) ∈ (1...((𝑁 − 1) + 1))) |
| 20 | 16, 19 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑀 + 1) ∈ (1...((𝑁 − 1) + 1))) |
| 21 | 7 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁)) |
| 22 | 20, 21 | eleqtrd 2843 |
. . . 4
⊢ (𝜑 → (𝑀 + 1) ∈ (1...𝑁)) |
| 23 | 3, 22 | ffvelcdmd 7105 |
. . 3
⊢ (𝜑 → (𝑈‘(𝑀 + 1)) ∈ (1...𝑁)) |
| 24 | | imassrn 6089 |
. . . . . . . . . 10
⊢ (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ ran 𝑈 |
| 25 | | frn 6743 |
. . . . . . . . . . 11
⊢ (𝑈:(1...𝑁)⟶(1...𝑁) → ran 𝑈 ⊆ (1...𝑁)) |
| 26 | 1, 2, 25 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → ran 𝑈 ⊆ (1...𝑁)) |
| 27 | 24, 26 | sstrid 3995 |
. . . . . . . . 9
⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (1...𝑁)) |
| 28 | 27 | sselda 3983 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → 𝑛 ∈ (1...𝑁)) |
| 29 | | poimirlem2.2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇:(1...𝑁)⟶ℤ) |
| 30 | 29 | ffvelcdmda 7104 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) ∈ ℤ) |
| 31 | 30 | zred 12722 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) ∈ ℝ) |
| 32 | 31 | ltp1d 12198 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) < ((𝑇‘𝑛) + 1)) |
| 33 | 31, 32 | ltned 11397 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) ≠ ((𝑇‘𝑛) + 1)) |
| 34 | 28, 33 | syldan 591 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (𝑇‘𝑛) ≠ ((𝑇‘𝑛) + 1)) |
| 35 | | poimirlem2.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))) |
| 36 | | breq1 5146 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑀 − 1) → (𝑦 < 𝑀 ↔ (𝑀 − 1) < 𝑀)) |
| 37 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑀 − 1) → 𝑦 = (𝑀 − 1)) |
| 38 | 36, 37 | ifbieq1d 4550 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑀 − 1) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑀 − 1) < 𝑀, (𝑀 − 1), (𝑦 + 1))) |
| 39 | | elfzelz 13564 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ (1...(𝑁 − 1)) → 𝑀 ∈ ℤ) |
| 40 | 16, 39 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 41 | 40 | zred 12722 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 42 | 41 | ltm1d 12200 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀 − 1) < 𝑀) |
| 43 | 42 | iftrued 4533 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → if((𝑀 − 1) < 𝑀, (𝑀 − 1), (𝑦 + 1)) = (𝑀 − 1)) |
| 44 | 38, 43 | sylan9eqr 2799 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑀 − 1)) |
| 45 | 44 | csbeq1d 3903 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋(𝑀 − 1) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) |
| 46 | 8, 9 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) |
| 47 | | elfzm1b 13642 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ)
→ (𝑀 ∈
(1...(𝑁 − 1)) ↔
(𝑀 − 1) ∈
(0...((𝑁 − 1) −
1)))) |
| 48 | 40, 46, 47 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀 ∈ (1...(𝑁 − 1)) ↔ (𝑀 − 1) ∈ (0...((𝑁 − 1) − 1)))) |
| 49 | 16, 48 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀 − 1) ∈ (0...((𝑁 − 1) − 1))) |
| 50 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = (𝑀 − 1) → (1...𝑗) = (1...(𝑀 − 1))) |
| 51 | 50 | imaeq2d 6078 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = (𝑀 − 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑀 − 1)))) |
| 52 | 51 | xpeq1d 5714 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = (𝑀 − 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑀 − 1))) × {1})) |
| 53 | 52 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑀 − 1))) × {1})) |
| 54 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = (𝑀 − 1) → (𝑗 + 1) = ((𝑀 − 1) + 1)) |
| 55 | 40 | zcnd 12723 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑀 ∈ ℂ) |
| 56 | | npcan1 11688 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ ℂ → ((𝑀 − 1) + 1) = 𝑀) |
| 57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑀 − 1) + 1) = 𝑀) |
| 58 | 54, 57 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (𝑗 + 1) = 𝑀) |
| 59 | 58 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((𝑗 + 1)...𝑁) = (𝑀...𝑁)) |
| 60 | 59 | imaeq2d 6078 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (𝑀...𝑁))) |
| 61 | 60 | xpeq1d 5714 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (𝑀...𝑁)) × {0})) |
| 62 | 53, 61 | uneq12d 4169 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))) |
| 63 | 62 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))) |
| 64 | 49, 63 | csbied 3935 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ⦋(𝑀 − 1) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))) |
| 65 | 64 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋(𝑀 − 1) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))) |
| 66 | 45, 65 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))) |
| 67 | 46 | zcnd 12723 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 − 1) ∈ ℂ) |
| 68 | | npcan1 11688 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 − 1) ∈ ℂ
→ (((𝑁 − 1)
− 1) + 1) = (𝑁
− 1)) |
| 69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑁 − 1) − 1) + 1) = (𝑁 − 1)) |
| 70 | | peano2zm 12660 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 − 1) ∈ ℤ
→ ((𝑁 − 1)
− 1) ∈ ℤ) |
| 71 | | uzid 12893 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 − 1) − 1) ∈
ℤ → ((𝑁 −
1) − 1) ∈ (ℤ≥‘((𝑁 − 1) − 1))) |
| 72 | | peano2uz 12943 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 − 1) − 1) ∈
(ℤ≥‘((𝑁 − 1) − 1)) → (((𝑁 − 1) − 1) + 1)
∈ (ℤ≥‘((𝑁 − 1) − 1))) |
| 73 | 46, 70, 71, 72 | 4syl 19 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑁 − 1) − 1) + 1) ∈
(ℤ≥‘((𝑁 − 1) − 1))) |
| 74 | 69, 73 | eqeltrrd 2842 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 − 1) ∈
(ℤ≥‘((𝑁 − 1) − 1))) |
| 75 | | fzss2 13604 |
. . . . . . . . . . . . 13
⊢ ((𝑁 − 1) ∈
(ℤ≥‘((𝑁 − 1) − 1)) → (0...((𝑁 − 1) − 1)) ⊆
(0...(𝑁 −
1))) |
| 76 | 74, 75 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0...((𝑁 − 1) − 1)) ⊆ (0...(𝑁 − 1))) |
| 77 | 76, 49 | sseldd 3984 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀 − 1) ∈ (0...(𝑁 − 1))) |
| 78 | | ovexd 7466 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 ∘f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))) ∈ V) |
| 79 | 35, 66, 77, 78 | fvmptd 7023 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘(𝑀 − 1)) = (𝑇 ∘f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))) |
| 80 | 79 | fveq1d 6908 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))‘𝑛)) |
| 81 | 80 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))‘𝑛)) |
| 82 | 29 | ffnd 6737 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 Fn (1...𝑁)) |
| 83 | 82 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → 𝑇 Fn (1...𝑁)) |
| 84 | | 1ex 11257 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
V |
| 85 | | fnconstg 6796 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
V → ((𝑈 “
(1...(𝑀 − 1)))
× {1}) Fn (𝑈 “
(1...(𝑀 −
1)))) |
| 86 | 84, 85 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 “ (1...(𝑀 − 1))) × {1}) Fn (𝑈 “ (1...(𝑀 − 1))) |
| 87 | | c0ex 11255 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
V |
| 88 | | fnconstg 6796 |
. . . . . . . . . . . . . . 15
⊢ (0 ∈
V → ((𝑈 “ (𝑀...𝑁)) × {0}) Fn (𝑈 “ (𝑀...𝑁))) |
| 89 | 87, 88 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 “ (𝑀...𝑁)) × {0}) Fn (𝑈 “ (𝑀...𝑁)) |
| 90 | 86, 89 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢ (((𝑈 “ (1...(𝑀 − 1))) × {1}) Fn (𝑈 “ (1...(𝑀 − 1))) ∧ ((𝑈 “ (𝑀...𝑁)) × {0}) Fn (𝑈 “ (𝑀...𝑁))) |
| 91 | | dff1o3 6854 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun ◡𝑈)) |
| 92 | 91 | simprbi 496 |
. . . . . . . . . . . . . . 15
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun ◡𝑈) |
| 93 | | imain 6651 |
. . . . . . . . . . . . . . 15
⊢ (Fun
◡𝑈 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁)))) |
| 94 | 1, 92, 93 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁)))) |
| 95 | | fzdisj 13591 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 − 1) < 𝑀 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑁)) = ∅) |
| 96 | 42, 95 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑁)) = ∅) |
| 97 | 96 | imaeq2d 6078 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = (𝑈 “ ∅)) |
| 98 | | ima0 6095 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 “ ∅) =
∅ |
| 99 | 97, 98 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ∅) |
| 100 | 94, 99 | eqtr3d 2779 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅) |
| 101 | | fnun 6682 |
. . . . . . . . . . . . 13
⊢
(((((𝑈 “
(1...(𝑀 − 1)))
× {1}) Fn (𝑈 “
(1...(𝑀 − 1))) ∧
((𝑈 “ (𝑀...𝑁)) × {0}) Fn (𝑈 “ (𝑀...𝑁))) ∧ ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅) → (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁)))) |
| 102 | 90, 100, 101 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁)))) |
| 103 | | elfzuz 13560 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈ (1...(𝑁 − 1)) → 𝑀 ∈
(ℤ≥‘1)) |
| 104 | 16, 103 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
| 105 | 57, 104 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑀 − 1) + 1) ∈
(ℤ≥‘1)) |
| 106 | | peano2zm 12660 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈
ℤ) |
| 107 | | uzid 12893 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 − 1) ∈ ℤ
→ (𝑀 − 1) ∈
(ℤ≥‘(𝑀 − 1))) |
| 108 | | peano2uz 12943 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 − 1) ∈
(ℤ≥‘(𝑀 − 1)) → ((𝑀 − 1) + 1) ∈
(ℤ≥‘(𝑀 − 1))) |
| 109 | 40, 106, 107, 108 | 4syl 19 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑀 − 1) + 1) ∈
(ℤ≥‘(𝑀 − 1))) |
| 110 | 57, 109 | eqeltrrd 2842 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘(𝑀 − 1))) |
| 111 | | peano2uz 12943 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈
(ℤ≥‘(𝑀 − 1)) → (𝑀 + 1) ∈
(ℤ≥‘(𝑀 − 1))) |
| 112 | | uzss 12901 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 + 1) ∈
(ℤ≥‘(𝑀 − 1)) →
(ℤ≥‘(𝑀 + 1)) ⊆
(ℤ≥‘(𝑀 − 1))) |
| 113 | 110, 111,
112 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 →
(ℤ≥‘(𝑀 + 1)) ⊆
(ℤ≥‘(𝑀 − 1))) |
| 114 | | elfzuz3 13561 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ (1...(𝑁 − 1)) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
| 115 | | eluzp1p1 12906 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 − 1) ∈
(ℤ≥‘𝑀) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
| 116 | 16, 114, 115 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
| 117 | 7, 116 | eqeltrrd 2842 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) |
| 118 | 113, 117 | sseldd 3984 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 − 1))) |
| 119 | | fzsplit2 13589 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑀 − 1) + 1) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 − 1))) → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁))) |
| 120 | 105, 118,
119 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁))) |
| 121 | 57 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝑀 − 1) + 1)...𝑁) = (𝑀...𝑁)) |
| 122 | 121 | uneq2d 4168 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁)) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))) |
| 123 | 120, 122 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))) |
| 124 | 123 | imaeq2d 6078 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑀 − 1)) ∪ (𝑀...𝑁)))) |
| 125 | | imaundi 6169 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 “ ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))) = ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁))) |
| 126 | 124, 125 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈 “ (1...𝑁)) = ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁)))) |
| 127 | | f1ofo 6855 |
. . . . . . . . . . . . . . 15
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁)) |
| 128 | | foima 6825 |
. . . . . . . . . . . . . . 15
⊢ (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁)) |
| 129 | 1, 127, 128 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁)) |
| 130 | 126, 129 | eqtr3d 2779 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁))) = (1...𝑁)) |
| 131 | 130 | fneq2d 6662 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁))) ↔ (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn (1...𝑁))) |
| 132 | 102, 131 | mpbid 232 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn (1...𝑁)) |
| 133 | 132 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn (1...𝑁)) |
| 134 | | ovexd 7466 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (1...𝑁) ∈ V) |
| 135 | | inidm 4227 |
. . . . . . . . . 10
⊢
((1...𝑁) ∩
(1...𝑁)) = (1...𝑁) |
| 136 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛)) |
| 137 | 100 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅) |
| 138 | | fzss2 13604 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → (𝑀...(𝑀 + 1)) ⊆ (𝑀...𝑁)) |
| 139 | | imass2 6120 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀...(𝑀 + 1)) ⊆ (𝑀...𝑁) → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (𝑀...𝑁))) |
| 140 | 117, 138,
139 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (𝑀...𝑁))) |
| 141 | 140 | sselda 3983 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → 𝑛 ∈ (𝑈 “ (𝑀...𝑁))) |
| 142 | | fvun2 7001 |
. . . . . . . . . . . . . 14
⊢ ((((𝑈 “ (1...(𝑀 − 1))) × {1}) Fn (𝑈 “ (1...(𝑀 − 1))) ∧ ((𝑈 “ (𝑀...𝑁)) × {0}) Fn (𝑈 “ (𝑀...𝑁)) ∧ (((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (𝑀...𝑁)))) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛)) |
| 143 | 86, 89, 142 | mp3an12 1453 |
. . . . . . . . . . . . 13
⊢ ((((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (𝑀...𝑁))) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛)) |
| 144 | 137, 141,
143 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛)) |
| 145 | 87 | fvconst2 7224 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (𝑈 “ (𝑀...𝑁)) → (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛) = 0) |
| 146 | 141, 145 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛) = 0) |
| 147 | 144, 146 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = 0) |
| 148 | 147 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = 0) |
| 149 | 83, 133, 134, 134, 135, 136, 148 | ofval 7708 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0)) |
| 150 | 28, 149 | mpdan 687 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0)) |
| 151 | 30 | zcnd 12723 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) ∈ ℂ) |
| 152 | 151 | addridd 11461 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇‘𝑛) + 0) = (𝑇‘𝑛)) |
| 153 | 28, 152 | syldan 591 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑇‘𝑛) + 0) = (𝑇‘𝑛)) |
| 154 | 81, 150, 153 | 3eqtrd 2781 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘(𝑀 − 1))‘𝑛) = (𝑇‘𝑛)) |
| 155 | | breq1 5146 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑀 → (𝑦 < 𝑀 ↔ 𝑀 < 𝑀)) |
| 156 | | oveq1 7438 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑀 → (𝑦 + 1) = (𝑀 + 1)) |
| 157 | 155, 156 | ifbieq2d 4552 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑀 → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if(𝑀 < 𝑀, 𝑦, (𝑀 + 1))) |
| 158 | 41 | ltnrd 11395 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ¬ 𝑀 < 𝑀) |
| 159 | 158 | iffalsed 4536 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → if(𝑀 < 𝑀, 𝑦, (𝑀 + 1)) = (𝑀 + 1)) |
| 160 | 157, 159 | sylan9eqr 2799 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 = 𝑀) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑀 + 1)) |
| 161 | 160 | csbeq1d 3903 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 = 𝑀) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋(𝑀 + 1) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) |
| 162 | | ovex 7464 |
. . . . . . . . . . . . 13
⊢ (𝑀 + 1) ∈ V |
| 163 | | oveq2 7439 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = (𝑀 + 1) → (1...𝑗) = (1...(𝑀 + 1))) |
| 164 | 163 | imaeq2d 6078 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = (𝑀 + 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑀 + 1)))) |
| 165 | 164 | xpeq1d 5714 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = (𝑀 + 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑀 + 1))) × {1})) |
| 166 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = (𝑀 + 1) → (𝑗 + 1) = ((𝑀 + 1) + 1)) |
| 167 | 166 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = (𝑀 + 1) → ((𝑗 + 1)...𝑁) = (((𝑀 + 1) + 1)...𝑁)) |
| 168 | 167 | imaeq2d 6078 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = (𝑀 + 1) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) |
| 169 | 168 | xpeq1d 5714 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = (𝑀 + 1) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})) |
| 170 | 165, 169 | uneq12d 4169 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = (𝑀 + 1) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))) |
| 171 | 170 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝑗 = (𝑀 + 1) → (𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))) |
| 172 | 162, 171 | csbie 3934 |
. . . . . . . . . . . 12
⊢
⦋(𝑀 +
1) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))) |
| 173 | 161, 172 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 = 𝑀) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))) |
| 174 | | fz1ssfz0 13663 |
. . . . . . . . . . . 12
⊢
(1...(𝑁 − 1))
⊆ (0...(𝑁 −
1)) |
| 175 | 174, 16 | sselid 3981 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ (0...(𝑁 − 1))) |
| 176 | | ovexd 7466 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 ∘f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))) ∈ V) |
| 177 | 35, 173, 175, 176 | fvmptd 7023 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝑀) = (𝑇 ∘f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))) |
| 178 | 177 | fveq1d 6908 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹‘𝑀)‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))‘𝑛)) |
| 179 | 178 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘𝑀)‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))‘𝑛)) |
| 180 | | fnconstg 6796 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
V → ((𝑈 “
(1...(𝑀 + 1))) × {1})
Fn (𝑈 “ (1...(𝑀 + 1)))) |
| 181 | 84, 180 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 “ (1...(𝑀 + 1))) × {1}) Fn (𝑈 “ (1...(𝑀 + 1))) |
| 182 | | fnconstg 6796 |
. . . . . . . . . . . . . . 15
⊢ (0 ∈
V → ((𝑈 “
(((𝑀 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) |
| 183 | 87, 182 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑀 + 1) + 1)...𝑁)) |
| 184 | 181, 183 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢ (((𝑈 “ (1...(𝑀 + 1))) × {1}) Fn (𝑈 “ (1...(𝑀 + 1))) ∧ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) |
| 185 | | imain 6651 |
. . . . . . . . . . . . . . . 16
⊢ (Fun
◡𝑈 → (𝑈 “ ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁)))) |
| 186 | 1, 92, 185 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑈 “ ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁)))) |
| 187 | | peano2re 11434 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈
ℝ) |
| 188 | 41, 187 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑀 + 1) ∈ ℝ) |
| 189 | 188 | ltp1d 12198 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑀 + 1) < ((𝑀 + 1) + 1)) |
| 190 | | fzdisj 13591 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 + 1) < ((𝑀 + 1) + 1) → ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁)) = ∅) |
| 191 | 189, 190 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁)) = ∅) |
| 192 | 191 | imaeq2d 6078 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑈 “ ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁))) = (𝑈 “ ∅)) |
| 193 | 186, 192 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = (𝑈 “ ∅)) |
| 194 | 193, 98 | eqtrdi 2793 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = ∅) |
| 195 | | fnun 6682 |
. . . . . . . . . . . . 13
⊢
(((((𝑈 “
(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)...𝑁)))) |
| 196 | 184, 194,
195 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁)))) |
| 197 | | fzsplit 13590 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 + 1) ∈ (1...𝑁) → (1...𝑁) = ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁))) |
| 198 | 22, 197 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1...𝑁) = ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁))) |
| 199 | 198 | imaeq2d 6078 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)))) |
| 200 | | imaundi 6169 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 “ ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) |
| 201 | 199, 200 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈 “ (1...𝑁)) = ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁)))) |
| 202 | 201, 129 | eqtr3d 2779 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = (1...𝑁)) |
| 203 | 202 | fneq2d 6662 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) ↔ (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))) |
| 204 | 196, 203 | mpbid 232 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
| 205 | 204 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
| 206 | 194 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = ∅) |
| 207 | | fzss1 13603 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈
(ℤ≥‘1) → (𝑀...(𝑀 + 1)) ⊆ (1...(𝑀 + 1))) |
| 208 | | imass2 6120 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀...(𝑀 + 1)) ⊆ (1...(𝑀 + 1)) → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (1...(𝑀 + 1)))) |
| 209 | 104, 207,
208 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (1...(𝑀 + 1)))) |
| 210 | 209 | sselda 3983 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → 𝑛 ∈ (𝑈 “ (1...(𝑀 + 1)))) |
| 211 | | fvun1 7000 |
. . . . . . . . . . . . . 14
⊢ ((((𝑈 “ (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})‘𝑛)) |
| 212 | 181, 183,
211 | mp3an12 1453 |
. . . . . . . . . . . . 13
⊢ ((((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑀 + 1)))) → ((((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑀 + 1))) × {1})‘𝑛)) |
| 213 | 206, 210,
212 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑀 + 1))) × {1})‘𝑛)) |
| 214 | 84 | fvconst2 7224 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (𝑈 “ (1...(𝑀 + 1))) → (((𝑈 “ (1...(𝑀 + 1))) × {1})‘𝑛) = 1) |
| 215 | 210, 214 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (((𝑈 “ (1...(𝑀 + 1))) × {1})‘𝑛) = 1) |
| 216 | 213, 215 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1) |
| 217 | 216 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1) |
| 218 | 83, 205, 134, 134, 135, 136, 217 | ofval 7708 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1)) |
| 219 | 28, 218 | mpdan 687 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1)) |
| 220 | 179, 219 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘𝑀)‘𝑛) = ((𝑇‘𝑛) + 1)) |
| 221 | 34, 154, 220 | 3netr4d 3018 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛)) |
| 222 | 221 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛)) |
| 223 | | fzpr 13619 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → (𝑀...(𝑀 + 1)) = {𝑀, (𝑀 + 1)}) |
| 224 | 16, 39, 223 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (𝑀...(𝑀 + 1)) = {𝑀, (𝑀 + 1)}) |
| 225 | 224 | imaeq2d 6078 |
. . . . . 6
⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) = (𝑈 “ {𝑀, (𝑀 + 1)})) |
| 226 | | f1ofn 6849 |
. . . . . . . 8
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 Fn (1...𝑁)) |
| 227 | 1, 226 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑈 Fn (1...𝑁)) |
| 228 | | fnimapr 6992 |
. . . . . . 7
⊢ ((𝑈 Fn (1...𝑁) ∧ 𝑀 ∈ (1...𝑁) ∧ (𝑀 + 1) ∈ (1...𝑁)) → (𝑈 “ {𝑀, (𝑀 + 1)}) = {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))}) |
| 229 | 227, 17, 22, 228 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → (𝑈 “ {𝑀, (𝑀 + 1)}) = {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))}) |
| 230 | 225, 229 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) = {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))}) |
| 231 | 222, 230 | raleqtrdv 3328 |
. . . 4
⊢ (𝜑 → ∀𝑛 ∈ {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))} ((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛)) |
| 232 | | fvex 6919 |
. . . . 5
⊢ (𝑈‘𝑀) ∈ V |
| 233 | | fvex 6919 |
. . . . 5
⊢ (𝑈‘(𝑀 + 1)) ∈ V |
| 234 | | fveq2 6906 |
. . . . . 6
⊢ (𝑛 = (𝑈‘𝑀) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀))) |
| 235 | | fveq2 6906 |
. . . . . 6
⊢ (𝑛 = (𝑈‘𝑀) → ((𝐹‘𝑀)‘𝑛) = ((𝐹‘𝑀)‘(𝑈‘𝑀))) |
| 236 | 234, 235 | neeq12d 3002 |
. . . . 5
⊢ (𝑛 = (𝑈‘𝑀) → (((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)))) |
| 237 | | fveq2 6906 |
. . . . . 6
⊢ (𝑛 = (𝑈‘(𝑀 + 1)) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1)))) |
| 238 | | fveq2 6906 |
. . . . . 6
⊢ (𝑛 = (𝑈‘(𝑀 + 1)) → ((𝐹‘𝑀)‘𝑛) = ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))) |
| 239 | 237, 238 | neeq12d 3002 |
. . . . 5
⊢ (𝑛 = (𝑈‘(𝑀 + 1)) → (((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1))))) |
| 240 | 232, 233,
236, 239 | ralpr 4700 |
. . . 4
⊢
(∀𝑛 ∈
{(𝑈‘𝑀), (𝑈‘(𝑀 + 1))} ((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ (((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1))))) |
| 241 | 231, 240 | sylib 218 |
. . 3
⊢ (𝜑 → (((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1))))) |
| 242 | 41 | ltp1d 12198 |
. . . . 5
⊢ (𝜑 → 𝑀 < (𝑀 + 1)) |
| 243 | 41, 242 | ltned 11397 |
. . . 4
⊢ (𝜑 → 𝑀 ≠ (𝑀 + 1)) |
| 244 | | f1of1 6847 |
. . . . . . 7
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–1-1→(1...𝑁)) |
| 245 | 1, 244 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑈:(1...𝑁)–1-1→(1...𝑁)) |
| 246 | | f1veqaeq 7277 |
. . . . . 6
⊢ ((𝑈:(1...𝑁)–1-1→(1...𝑁) ∧ (𝑀 ∈ (1...𝑁) ∧ (𝑀 + 1) ∈ (1...𝑁))) → ((𝑈‘𝑀) = (𝑈‘(𝑀 + 1)) → 𝑀 = (𝑀 + 1))) |
| 247 | 245, 17, 22, 246 | syl12anc 837 |
. . . . 5
⊢ (𝜑 → ((𝑈‘𝑀) = (𝑈‘(𝑀 + 1)) → 𝑀 = (𝑀 + 1))) |
| 248 | 247 | necon3d 2961 |
. . . 4
⊢ (𝜑 → (𝑀 ≠ (𝑀 + 1) → (𝑈‘𝑀) ≠ (𝑈‘(𝑀 + 1)))) |
| 249 | 243, 248 | mpd 15 |
. . 3
⊢ (𝜑 → (𝑈‘𝑀) ≠ (𝑈‘(𝑀 + 1))) |
| 250 | 236 | anbi1d 631 |
. . . . 5
⊢ (𝑛 = (𝑈‘𝑀) → ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ↔ (((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)))) |
| 251 | | neeq1 3003 |
. . . . 5
⊢ (𝑛 = (𝑈‘𝑀) → (𝑛 ≠ 𝑚 ↔ (𝑈‘𝑀) ≠ 𝑚)) |
| 252 | 250, 251 | anbi12d 632 |
. . . 4
⊢ (𝑛 = (𝑈‘𝑀) → (((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ((((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ (𝑈‘𝑀) ≠ 𝑚))) |
| 253 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → ((𝐹‘(𝑀 − 1))‘𝑚) = ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1)))) |
| 254 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → ((𝐹‘𝑀)‘𝑚) = ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))) |
| 255 | 253, 254 | neeq12d 3002 |
. . . . . 6
⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → (((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚) ↔ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1))))) |
| 256 | 255 | anbi2d 630 |
. . . . 5
⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → ((((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ↔ (((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))))) |
| 257 | | neeq2 3004 |
. . . . 5
⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → ((𝑈‘𝑀) ≠ 𝑚 ↔ (𝑈‘𝑀) ≠ (𝑈‘(𝑀 + 1)))) |
| 258 | 256, 257 | anbi12d 632 |
. . . 4
⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → (((((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ (𝑈‘𝑀) ≠ 𝑚) ↔ ((((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))) ∧ (𝑈‘𝑀) ≠ (𝑈‘(𝑀 + 1))))) |
| 259 | 252, 258 | rspc2ev 3635 |
. . 3
⊢ (((𝑈‘𝑀) ∈ (1...𝑁) ∧ (𝑈‘(𝑀 + 1)) ∈ (1...𝑁) ∧ ((((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))) ∧ (𝑈‘𝑀) ≠ (𝑈‘(𝑀 + 1)))) → ∃𝑛 ∈ (1...𝑁)∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚)) |
| 260 | 18, 23, 241, 249, 259 | syl112anc 1376 |
. 2
⊢ (𝜑 → ∃𝑛 ∈ (1...𝑁)∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚)) |
| 261 | | dfrex2 3073 |
. . 3
⊢
(∃𝑛 ∈
(1...𝑁)∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ¬ ∀𝑛 ∈ (1...𝑁) ¬ ∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚)) |
| 262 | | fveq2 6906 |
. . . . . 6
⊢ (𝑛 = 𝑚 → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘(𝑀 − 1))‘𝑚)) |
| 263 | | fveq2 6906 |
. . . . . 6
⊢ (𝑛 = 𝑚 → ((𝐹‘𝑀)‘𝑛) = ((𝐹‘𝑀)‘𝑚)) |
| 264 | 262, 263 | neeq12d 3002 |
. . . . 5
⊢ (𝑛 = 𝑚 → (((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚))) |
| 265 | 264 | rmo4 3736 |
. . . 4
⊢
(∃*𝑛 ∈
(1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁)∀𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚)) |
| 266 | | dfral2 3099 |
. . . . . 6
⊢
(∀𝑚 ∈
(1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚) ↔ ¬ ∃𝑚 ∈ (1...𝑁) ¬ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚)) |
| 267 | | df-ne 2941 |
. . . . . . . . 9
⊢ (𝑛 ≠ 𝑚 ↔ ¬ 𝑛 = 𝑚) |
| 268 | 267 | anbi2i 623 |
. . . . . . . 8
⊢
(((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ ¬ 𝑛 = 𝑚)) |
| 269 | | annim 403 |
. . . . . . . 8
⊢
(((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ ¬ 𝑛 = 𝑚) ↔ ¬ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚)) |
| 270 | 268, 269 | bitri 275 |
. . . . . . 7
⊢
(((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ¬ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚)) |
| 271 | 270 | rexbii 3094 |
. . . . . 6
⊢
(∃𝑚 ∈
(1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ∃𝑚 ∈ (1...𝑁) ¬ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚)) |
| 272 | 266, 271 | xchbinxr 335 |
. . . . 5
⊢
(∀𝑚 ∈
(1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚) ↔ ¬ ∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚)) |
| 273 | 272 | ralbii 3093 |
. . . 4
⊢
(∀𝑛 ∈
(1...𝑁)∀𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚) ↔ ∀𝑛 ∈ (1...𝑁) ¬ ∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚)) |
| 274 | 265, 273 | bitri 275 |
. . 3
⊢
(∃*𝑛 ∈
(1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁) ¬ ∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚)) |
| 275 | 261, 274 | xchbinxr 335 |
. 2
⊢
(∃𝑛 ∈
(1...𝑁)∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛)) |
| 276 | 260, 275 | sylib 218 |
1
⊢ (𝜑 → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛)) |