Step | Hyp | Ref
| Expression |
1 | | poimirlem2.3 |
. . . . 5
⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁)) |
2 | | f1of 6050 |
. . . . 5
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)⟶(1...𝑁)) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑈:(1...𝑁)⟶(1...𝑁)) |
4 | | poimir.0 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℕ) |
5 | 4 | nncnd 10913 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℂ) |
6 | | npcan1 10334 |
. . . . . . . 8
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
7 | 5, 6 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
8 | 4 | nnzd 11357 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℤ) |
9 | | peano2zm 11297 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
10 | | uzid 11578 |
. . . . . . . 8
⊢ ((𝑁 − 1) ∈ ℤ
→ (𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1))) |
11 | | peano2uz 11617 |
. . . . . . . 8
⊢ ((𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
12 | 8, 9, 10, 11 | 4syl 19 |
. . . . . . 7
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
13 | 7, 12 | eqeltrrd 2689 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) |
14 | | fzss2 12252 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁)) |
15 | 13, 14 | syl 17 |
. . . . 5
⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁)) |
16 | | poimirlem1.4 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 − 1))) |
17 | 15, 16 | sseldd 3569 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ (1...𝑁)) |
18 | 3, 17 | ffvelrnd 6268 |
. . 3
⊢ (𝜑 → (𝑈‘𝑀) ∈ (1...𝑁)) |
19 | | fzp1elp1 12264 |
. . . . . 6
⊢ (𝑀 ∈ (1...(𝑁 − 1)) → (𝑀 + 1) ∈ (1...((𝑁 − 1) + 1))) |
20 | 16, 19 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑀 + 1) ∈ (1...((𝑁 − 1) + 1))) |
21 | 7 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁)) |
22 | 20, 21 | eleqtrd 2690 |
. . . 4
⊢ (𝜑 → (𝑀 + 1) ∈ (1...𝑁)) |
23 | 3, 22 | ffvelrnd 6268 |
. . 3
⊢ (𝜑 → (𝑈‘(𝑀 + 1)) ∈ (1...𝑁)) |
24 | | imassrn 5396 |
. . . . . . . . . 10
⊢ (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ ran 𝑈 |
25 | | frn 5966 |
. . . . . . . . . . 11
⊢ (𝑈:(1...𝑁)⟶(1...𝑁) → ran 𝑈 ⊆ (1...𝑁)) |
26 | 1, 2, 25 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → ran 𝑈 ⊆ (1...𝑁)) |
27 | 24, 26 | syl5ss 3579 |
. . . . . . . . 9
⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (1...𝑁)) |
28 | 27 | sselda 3568 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → 𝑛 ∈ (1...𝑁)) |
29 | | poimirlem2.2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇:(1...𝑁)⟶ℤ) |
30 | 29 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) ∈ ℤ) |
31 | 30 | zred 11358 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) ∈ ℝ) |
32 | 31 | ltp1d 10833 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) < ((𝑇‘𝑛) + 1)) |
33 | 31, 32 | ltned 10052 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) ≠ ((𝑇‘𝑛) + 1)) |
34 | 28, 33 | syldan 486 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (𝑇‘𝑛) ≠ ((𝑇‘𝑛) + 1)) |
35 | | poimirlem2.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))) |
36 | | breq1 4586 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑀 − 1) → (𝑦 < 𝑀 ↔ (𝑀 − 1) < 𝑀)) |
37 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑀 − 1) → 𝑦 = (𝑀 − 1)) |
38 | 36, 37 | ifbieq1d 4059 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑀 − 1) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑀 − 1) < 𝑀, (𝑀 − 1), (𝑦 + 1))) |
39 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ (1...(𝑁 − 1)) → 𝑀 ∈ ℤ) |
40 | 16, 39 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑀 ∈ ℤ) |
41 | 40 | zred 11358 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ∈ ℝ) |
42 | 41 | ltm1d 10835 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀 − 1) < 𝑀) |
43 | 42 | iftrued 4044 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → if((𝑀 − 1) < 𝑀, (𝑀 − 1), (𝑦 + 1)) = (𝑀 − 1)) |
44 | 38, 43 | sylan9eqr 2666 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑀 − 1)) |
45 | 44 | csbeq1d 3506 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋(𝑀 − 1) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) |
46 | 8, 9 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) |
47 | | elfzm1b 12287 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ)
→ (𝑀 ∈
(1...(𝑁 − 1)) ↔
(𝑀 − 1) ∈
(0...((𝑁 − 1) −
1)))) |
48 | 40, 46, 47 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀 ∈ (1...(𝑁 − 1)) ↔ (𝑀 − 1) ∈ (0...((𝑁 − 1) − 1)))) |
49 | 16, 48 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀 − 1) ∈ (0...((𝑁 − 1) − 1))) |
50 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = (𝑀 − 1) → (1...𝑗) = (1...(𝑀 − 1))) |
51 | 50 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = (𝑀 − 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑀 − 1)))) |
52 | 51 | xpeq1d 5062 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = (𝑀 − 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑀 − 1))) × {1})) |
53 | 52 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑀 − 1))) × {1})) |
54 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = (𝑀 − 1) → (𝑗 + 1) = ((𝑀 − 1) + 1)) |
55 | 40 | zcnd 11359 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑀 ∈ ℂ) |
56 | | npcan1 10334 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ ℂ → ((𝑀 − 1) + 1) = 𝑀) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑀 − 1) + 1) = 𝑀) |
58 | 54, 57 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (𝑗 + 1) = 𝑀) |
59 | 58 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((𝑗 + 1)...𝑁) = (𝑀...𝑁)) |
60 | 59 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (𝑀...𝑁))) |
61 | 60 | xpeq1d 5062 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (𝑀...𝑁)) × {0})) |
62 | 53, 61 | uneq12d 3730 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))) |
63 | 62 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))) |
64 | 49, 63 | csbied 3526 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ⦋(𝑀 − 1) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))) |
65 | 64 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋(𝑀 − 1) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))) |
66 | 45, 65 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))) |
67 | 46 | zcnd 11359 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 − 1) ∈ ℂ) |
68 | | npcan1 10334 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 − 1) ∈ ℂ
→ (((𝑁 − 1)
− 1) + 1) = (𝑁
− 1)) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑁 − 1) − 1) + 1) = (𝑁 − 1)) |
70 | | peano2zm 11297 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 − 1) ∈ ℤ
→ ((𝑁 − 1)
− 1) ∈ ℤ) |
71 | | uzid 11578 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 − 1) − 1) ∈
ℤ → ((𝑁 −
1) − 1) ∈ (ℤ≥‘((𝑁 − 1) − 1))) |
72 | | peano2uz 11617 |
. . . . . . . . . . . . . . 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 2689 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 − 1) ∈
(ℤ≥‘((𝑁 − 1) − 1))) |
75 | | fzss2 12252 |
. . . . . . . . . . . . 13
⊢ ((𝑁 − 1) ∈
(ℤ≥‘((𝑁 − 1) − 1)) → (0...((𝑁 − 1) − 1)) ⊆
(0...(𝑁 −
1))) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0...((𝑁 − 1) − 1)) ⊆ (0...(𝑁 − 1))) |
77 | 76, 49 | sseldd 3569 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀 − 1) ∈ (0...(𝑁 − 1))) |
78 | | ovex 6577 |
. . . . . . . . . . . 12
⊢ (𝑇 ∘𝑓 +
(((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪
((𝑈 “ (𝑀...𝑁)) × {0}))) ∈ V |
79 | 78 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))) ∈ V) |
80 | 35, 66, 77, 79 | fvmptd 6197 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘(𝑀 − 1)) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))) |
81 | 80 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))‘𝑛)) |
82 | 81 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))‘𝑛)) |
83 | | ffn 5958 |
. . . . . . . . . . . 12
⊢ (𝑇:(1...𝑁)⟶ℤ → 𝑇 Fn (1...𝑁)) |
84 | 29, 83 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 Fn (1...𝑁)) |
85 | 84 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → 𝑇 Fn (1...𝑁)) |
86 | | 1ex 9914 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
V |
87 | | fnconstg 6006 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
V → ((𝑈 “
(1...(𝑀 − 1)))
× {1}) Fn (𝑈 “
(1...(𝑀 −
1)))) |
88 | 86, 87 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 “ (1...(𝑀 − 1))) × {1}) Fn (𝑈 “ (1...(𝑀 − 1))) |
89 | | c0ex 9913 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
V |
90 | | fnconstg 6006 |
. . . . . . . . . . . . . . 15
⊢ (0 ∈
V → ((𝑈 “ (𝑀...𝑁)) × {0}) Fn (𝑈 “ (𝑀...𝑁))) |
91 | 89, 90 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 “ (𝑀...𝑁)) × {0}) Fn (𝑈 “ (𝑀...𝑁)) |
92 | 88, 91 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢ (((𝑈 “ (1...(𝑀 − 1))) × {1}) Fn (𝑈 “ (1...(𝑀 − 1))) ∧ ((𝑈 “ (𝑀...𝑁)) × {0}) Fn (𝑈 “ (𝑀...𝑁))) |
93 | | dff1o3 6056 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun ◡𝑈)) |
94 | 93 | simprbi 479 |
. . . . . . . . . . . . . . 15
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun ◡𝑈) |
95 | | imain 5888 |
. . . . . . . . . . . . . . 15
⊢ (Fun
◡𝑈 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁)))) |
96 | 1, 94, 95 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁)))) |
97 | | fzdisj 12239 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 − 1) < 𝑀 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑁)) = ∅) |
98 | 42, 97 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑁)) = ∅) |
99 | 98 | imaeq2d 5385 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = (𝑈 “ ∅)) |
100 | | ima0 5400 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 “ ∅) =
∅ |
101 | 99, 100 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ∅) |
102 | 96, 101 | eqtr3d 2646 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅) |
103 | | fnun 5911 |
. . . . . . . . . . . . 13
⊢
(((((𝑈 “
(1...(𝑀 − 1)))
× {1}) Fn (𝑈 “
(1...(𝑀 − 1))) ∧
((𝑈 “ (𝑀...𝑁)) × {0}) Fn (𝑈 “ (𝑀...𝑁))) ∧ ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅) → (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁)))) |
104 | 92, 102, 103 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁)))) |
105 | | elfzuz 12209 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈ (1...(𝑁 − 1)) → 𝑀 ∈
(ℤ≥‘1)) |
106 | 16, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
107 | 57, 106 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑀 − 1) + 1) ∈
(ℤ≥‘1)) |
108 | | peano2zm 11297 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈
ℤ) |
109 | | uzid 11578 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 − 1) ∈ ℤ
→ (𝑀 − 1) ∈
(ℤ≥‘(𝑀 − 1))) |
110 | | peano2uz 11617 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 − 1) ∈
(ℤ≥‘(𝑀 − 1)) → ((𝑀 − 1) + 1) ∈
(ℤ≥‘(𝑀 − 1))) |
111 | 40, 108, 109, 110 | 4syl 19 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑀 − 1) + 1) ∈
(ℤ≥‘(𝑀 − 1))) |
112 | 57, 111 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘(𝑀 − 1))) |
113 | | peano2uz 11617 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈
(ℤ≥‘(𝑀 − 1)) → (𝑀 + 1) ∈
(ℤ≥‘(𝑀 − 1))) |
114 | | uzss 11584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 + 1) ∈
(ℤ≥‘(𝑀 − 1)) →
(ℤ≥‘(𝑀 + 1)) ⊆
(ℤ≥‘(𝑀 − 1))) |
115 | 112, 113,
114 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 →
(ℤ≥‘(𝑀 + 1)) ⊆
(ℤ≥‘(𝑀 − 1))) |
116 | | elfzuz3 12210 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ (1...(𝑁 − 1)) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
117 | | eluzp1p1 11589 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 − 1) ∈
(ℤ≥‘𝑀) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
118 | 16, 116, 117 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
119 | 7, 118 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) |
120 | 115, 119 | sseldd 3569 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 − 1))) |
121 | | fzsplit2 12237 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑀 − 1) + 1) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 − 1))) → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁))) |
122 | 107, 120,
121 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁))) |
123 | 57 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝑀 − 1) + 1)...𝑁) = (𝑀...𝑁)) |
124 | 123 | uneq2d 3729 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁)) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))) |
125 | 122, 124 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))) |
126 | 125 | imaeq2d 5385 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑀 − 1)) ∪ (𝑀...𝑁)))) |
127 | | imaundi 5464 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 “ ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))) = ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁))) |
128 | 126, 127 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈 “ (1...𝑁)) = ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁)))) |
129 | | f1ofo 6057 |
. . . . . . . . . . . . . . 15
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁)) |
130 | | foima 6033 |
. . . . . . . . . . . . . . 15
⊢ (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁)) |
131 | 1, 129, 130 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁)) |
132 | 128, 131 | eqtr3d 2646 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁))) = (1...𝑁)) |
133 | 132 | fneq2d 5896 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁))) ↔ (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn (1...𝑁))) |
134 | 104, 133 | mpbid 221 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn (1...𝑁)) |
135 | 134 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn (1...𝑁)) |
136 | | ovex 6577 |
. . . . . . . . . . 11
⊢
(1...𝑁) ∈
V |
137 | 136 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (1...𝑁) ∈ V) |
138 | | inidm 3784 |
. . . . . . . . . 10
⊢
((1...𝑁) ∩
(1...𝑁)) = (1...𝑁) |
139 | | eqidd 2611 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛)) |
140 | 102 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅) |
141 | | fzss2 12252 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → (𝑀...(𝑀 + 1)) ⊆ (𝑀...𝑁)) |
142 | | imass2 5420 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀...(𝑀 + 1)) ⊆ (𝑀...𝑁) → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (𝑀...𝑁))) |
143 | 119, 141,
142 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (𝑀...𝑁))) |
144 | 143 | sselda 3568 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → 𝑛 ∈ (𝑈 “ (𝑀...𝑁))) |
145 | | fvun2 6180 |
. . . . . . . . . . . . . 14
⊢ ((((𝑈 “ (1...(𝑀 − 1))) × {1}) Fn (𝑈 “ (1...(𝑀 − 1))) ∧ ((𝑈 “ (𝑀...𝑁)) × {0}) Fn (𝑈 “ (𝑀...𝑁)) ∧ (((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (𝑀...𝑁)))) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛)) |
146 | 88, 91, 145 | mp3an12 1406 |
. . . . . . . . . . . . 13
⊢ ((((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (𝑀...𝑁))) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛)) |
147 | 140, 144,
146 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛)) |
148 | 89 | fvconst2 6374 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (𝑈 “ (𝑀...𝑁)) → (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛) = 0) |
149 | 144, 148 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛) = 0) |
150 | 147, 149 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = 0) |
151 | 150 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = 0) |
152 | 85, 135, 137, 137, 138, 139, 151 | ofval 6804 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0)) |
153 | 28, 152 | mpdan 699 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0)) |
154 | 30 | zcnd 11359 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) ∈ ℂ) |
155 | 154 | addid1d 10115 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇‘𝑛) + 0) = (𝑇‘𝑛)) |
156 | 28, 155 | syldan 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑇‘𝑛) + 0) = (𝑇‘𝑛)) |
157 | 82, 153, 156 | 3eqtrd 2648 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘(𝑀 − 1))‘𝑛) = (𝑇‘𝑛)) |
158 | | breq1 4586 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑀 → (𝑦 < 𝑀 ↔ 𝑀 < 𝑀)) |
159 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑀 → (𝑦 + 1) = (𝑀 + 1)) |
160 | 158, 159 | ifbieq2d 4061 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑀 → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if(𝑀 < 𝑀, 𝑦, (𝑀 + 1))) |
161 | 41 | ltnrd 10050 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ¬ 𝑀 < 𝑀) |
162 | 161 | iffalsed 4047 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → if(𝑀 < 𝑀, 𝑦, (𝑀 + 1)) = (𝑀 + 1)) |
163 | 160, 162 | sylan9eqr 2666 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 = 𝑀) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑀 + 1)) |
164 | 163 | csbeq1d 3506 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 = 𝑀) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋(𝑀 + 1) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) |
165 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ (𝑀 + 1) ∈ V |
166 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = (𝑀 + 1) → (1...𝑗) = (1...(𝑀 + 1))) |
167 | 166 | imaeq2d 5385 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = (𝑀 + 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑀 + 1)))) |
168 | 167 | xpeq1d 5062 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = (𝑀 + 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑀 + 1))) × {1})) |
169 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = (𝑀 + 1) → (𝑗 + 1) = ((𝑀 + 1) + 1)) |
170 | 169 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = (𝑀 + 1) → ((𝑗 + 1)...𝑁) = (((𝑀 + 1) + 1)...𝑁)) |
171 | 170 | imaeq2d 5385 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = (𝑀 + 1) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) |
172 | 171 | xpeq1d 5062 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = (𝑀 + 1) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})) |
173 | 168, 172 | uneq12d 3730 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = (𝑀 + 1) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))) |
174 | 173 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑗 = (𝑀 + 1) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))) |
175 | 165, 174 | csbie 3525 |
. . . . . . . . . . . 12
⊢
⦋(𝑀 +
1) / 𝑗⦌(𝑇 ∘𝑓 +
(((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))) |
176 | 164, 175 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 = 𝑀) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))) |
177 | | 1eluzge0 11608 |
. . . . . . . . . . . . 13
⊢ 1 ∈
(ℤ≥‘0) |
178 | | fzss1 12251 |
. . . . . . . . . . . . 13
⊢ (1 ∈
(ℤ≥‘0) → (1...(𝑁 − 1)) ⊆ (0...(𝑁 − 1))) |
179 | 177, 178 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(1...(𝑁 − 1))
⊆ (0...(𝑁 −
1)) |
180 | 179, 16 | sseldi 3566 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ (0...(𝑁 − 1))) |
181 | | ovex 6577 |
. . . . . . . . . . . 12
⊢ (𝑇 ∘𝑓 +
(((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪
((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))) ∈ V |
182 | 181 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))) ∈ V) |
183 | 35, 176, 180, 182 | fvmptd 6197 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝑀) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))) |
184 | 183 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹‘𝑀)‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))‘𝑛)) |
185 | 184 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘𝑀)‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))‘𝑛)) |
186 | | fnconstg 6006 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
V → ((𝑈 “
(1...(𝑀 + 1))) × {1})
Fn (𝑈 “ (1...(𝑀 + 1)))) |
187 | 86, 186 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 “ (1...(𝑀 + 1))) × {1}) Fn (𝑈 “ (1...(𝑀 + 1))) |
188 | | fnconstg 6006 |
. . . . . . . . . . . . . . 15
⊢ (0 ∈
V → ((𝑈 “
(((𝑀 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) |
189 | 89, 188 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑀 + 1) + 1)...𝑁)) |
190 | 187, 189 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢ (((𝑈 “ (1...(𝑀 + 1))) × {1}) Fn (𝑈 “ (1...(𝑀 + 1))) ∧ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) |
191 | | imain 5888 |
. . . . . . . . . . . . . . . 16
⊢ (Fun
◡𝑈 → (𝑈 “ ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁)))) |
192 | 1, 94, 191 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑈 “ ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁)))) |
193 | | peano2re 10088 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈
ℝ) |
194 | 41, 193 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑀 + 1) ∈ ℝ) |
195 | 194 | ltp1d 10833 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑀 + 1) < ((𝑀 + 1) + 1)) |
196 | | fzdisj 12239 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 + 1) < ((𝑀 + 1) + 1) → ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁)) = ∅) |
197 | 195, 196 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁)) = ∅) |
198 | 197 | imaeq2d 5385 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑈 “ ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁))) = (𝑈 “ ∅)) |
199 | 192, 198 | eqtr3d 2646 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = (𝑈 “ ∅)) |
200 | 199, 100 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = ∅) |
201 | | fnun 5911 |
. . . . . . . . . . . . 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)...𝑁)))) |
202 | 190, 200,
201 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁)))) |
203 | | fzsplit 12238 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 + 1) ∈ (1...𝑁) → (1...𝑁) = ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁))) |
204 | 22, 203 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1...𝑁) = ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁))) |
205 | 204 | imaeq2d 5385 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)))) |
206 | | imaundi 5464 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 “ ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) |
207 | 205, 206 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈 “ (1...𝑁)) = ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁)))) |
208 | 207, 131 | eqtr3d 2646 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = (1...𝑁)) |
209 | 208 | fneq2d 5896 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) ↔ (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))) |
210 | 202, 209 | mpbid 221 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
211 | 210 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁)) |
212 | 200 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = ∅) |
213 | | fzss1 12251 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈
(ℤ≥‘1) → (𝑀...(𝑀 + 1)) ⊆ (1...(𝑀 + 1))) |
214 | | imass2 5420 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀...(𝑀 + 1)) ⊆ (1...(𝑀 + 1)) → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (1...(𝑀 + 1)))) |
215 | 106, 213,
214 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (1...(𝑀 + 1)))) |
216 | 215 | sselda 3568 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → 𝑛 ∈ (𝑈 “ (1...(𝑀 + 1)))) |
217 | | fvun1 6179 |
. . . . . . . . . . . . . 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})‘𝑛)) |
218 | 187, 189,
217 | mp3an12 1406 |
. . . . . . . . . . . . 13
⊢ ((((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑀 + 1)))) → ((((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑀 + 1))) × {1})‘𝑛)) |
219 | 212, 216,
218 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑀 + 1))) × {1})‘𝑛)) |
220 | 86 | fvconst2 6374 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (𝑈 “ (1...(𝑀 + 1))) → (((𝑈 “ (1...(𝑀 + 1))) × {1})‘𝑛) = 1) |
221 | 216, 220 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (((𝑈 “ (1...(𝑀 + 1))) × {1})‘𝑛) = 1) |
222 | 219, 221 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1) |
223 | 222 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1) |
224 | 85, 211, 137, 137, 138, 139, 223 | ofval 6804 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1)) |
225 | 28, 224 | mpdan 699 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1)) |
226 | 185, 225 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘𝑀)‘𝑛) = ((𝑇‘𝑛) + 1)) |
227 | 34, 157, 226 | 3netr4d 2859 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛)) |
228 | 227 | ralrimiva 2949 |
. . . . 5
⊢ (𝜑 → ∀𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛)) |
229 | | fzpr 12266 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℤ → (𝑀...(𝑀 + 1)) = {𝑀, (𝑀 + 1)}) |
230 | 16, 39, 229 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (𝑀...(𝑀 + 1)) = {𝑀, (𝑀 + 1)}) |
231 | 230 | imaeq2d 5385 |
. . . . . . 7
⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) = (𝑈 “ {𝑀, (𝑀 + 1)})) |
232 | | f1ofn 6051 |
. . . . . . . . 9
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 Fn (1...𝑁)) |
233 | 1, 232 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 Fn (1...𝑁)) |
234 | | fnimapr 6172 |
. . . . . . . 8
⊢ ((𝑈 Fn (1...𝑁) ∧ 𝑀 ∈ (1...𝑁) ∧ (𝑀 + 1) ∈ (1...𝑁)) → (𝑈 “ {𝑀, (𝑀 + 1)}) = {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))}) |
235 | 233, 17, 22, 234 | syl3anc 1318 |
. . . . . . 7
⊢ (𝜑 → (𝑈 “ {𝑀, (𝑀 + 1)}) = {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))}) |
236 | 231, 235 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) = {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))}) |
237 | 236 | raleqdv 3121 |
. . . . 5
⊢ (𝜑 → (∀𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ∀𝑛 ∈ {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))} ((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛))) |
238 | 228, 237 | mpbid 221 |
. . . 4
⊢ (𝜑 → ∀𝑛 ∈ {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))} ((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛)) |
239 | | fvex 6113 |
. . . . 5
⊢ (𝑈‘𝑀) ∈ V |
240 | | fvex 6113 |
. . . . 5
⊢ (𝑈‘(𝑀 + 1)) ∈ V |
241 | | fveq2 6103 |
. . . . . 6
⊢ (𝑛 = (𝑈‘𝑀) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀))) |
242 | | fveq2 6103 |
. . . . . 6
⊢ (𝑛 = (𝑈‘𝑀) → ((𝐹‘𝑀)‘𝑛) = ((𝐹‘𝑀)‘(𝑈‘𝑀))) |
243 | 241, 242 | neeq12d 2843 |
. . . . 5
⊢ (𝑛 = (𝑈‘𝑀) → (((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)))) |
244 | | fveq2 6103 |
. . . . . 6
⊢ (𝑛 = (𝑈‘(𝑀 + 1)) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1)))) |
245 | | fveq2 6103 |
. . . . . 6
⊢ (𝑛 = (𝑈‘(𝑀 + 1)) → ((𝐹‘𝑀)‘𝑛) = ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))) |
246 | 244, 245 | neeq12d 2843 |
. . . . 5
⊢ (𝑛 = (𝑈‘(𝑀 + 1)) → (((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1))))) |
247 | 239, 240,
243, 246 | ralpr 4185 |
. . . 4
⊢
(∀𝑛 ∈
{(𝑈‘𝑀), (𝑈‘(𝑀 + 1))} ((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ (((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1))))) |
248 | 238, 247 | sylib 207 |
. . 3
⊢ (𝜑 → (((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1))))) |
249 | 41 | ltp1d 10833 |
. . . . 5
⊢ (𝜑 → 𝑀 < (𝑀 + 1)) |
250 | 41, 249 | ltned 10052 |
. . . 4
⊢ (𝜑 → 𝑀 ≠ (𝑀 + 1)) |
251 | | f1of1 6049 |
. . . . . . 7
⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–1-1→(1...𝑁)) |
252 | 1, 251 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑈:(1...𝑁)–1-1→(1...𝑁)) |
253 | | f1veqaeq 6418 |
. . . . . 6
⊢ ((𝑈:(1...𝑁)–1-1→(1...𝑁) ∧ (𝑀 ∈ (1...𝑁) ∧ (𝑀 + 1) ∈ (1...𝑁))) → ((𝑈‘𝑀) = (𝑈‘(𝑀 + 1)) → 𝑀 = (𝑀 + 1))) |
254 | 252, 17, 22, 253 | syl12anc 1316 |
. . . . 5
⊢ (𝜑 → ((𝑈‘𝑀) = (𝑈‘(𝑀 + 1)) → 𝑀 = (𝑀 + 1))) |
255 | 254 | necon3d 2803 |
. . . 4
⊢ (𝜑 → (𝑀 ≠ (𝑀 + 1) → (𝑈‘𝑀) ≠ (𝑈‘(𝑀 + 1)))) |
256 | 250, 255 | mpd 15 |
. . 3
⊢ (𝜑 → (𝑈‘𝑀) ≠ (𝑈‘(𝑀 + 1))) |
257 | 243 | anbi1d 737 |
. . . . 5
⊢ (𝑛 = (𝑈‘𝑀) → ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ↔ (((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)))) |
258 | | neeq1 2844 |
. . . . 5
⊢ (𝑛 = (𝑈‘𝑀) → (𝑛 ≠ 𝑚 ↔ (𝑈‘𝑀) ≠ 𝑚)) |
259 | 257, 258 | anbi12d 743 |
. . . 4
⊢ (𝑛 = (𝑈‘𝑀) → (((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ((((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ (𝑈‘𝑀) ≠ 𝑚))) |
260 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → ((𝐹‘(𝑀 − 1))‘𝑚) = ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1)))) |
261 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → ((𝐹‘𝑀)‘𝑚) = ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))) |
262 | 260, 261 | neeq12d 2843 |
. . . . . 6
⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → (((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚) ↔ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1))))) |
263 | 262 | anbi2d 736 |
. . . . 5
⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → ((((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ↔ (((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))))) |
264 | | neeq2 2845 |
. . . . 5
⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → ((𝑈‘𝑀) ≠ 𝑚 ↔ (𝑈‘𝑀) ≠ (𝑈‘(𝑀 + 1)))) |
265 | 263, 264 | anbi12d 743 |
. . . 4
⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → (((((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ (𝑈‘𝑀) ≠ 𝑚) ↔ ((((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))) ∧ (𝑈‘𝑀) ≠ (𝑈‘(𝑀 + 1))))) |
266 | 259, 265 | rspc2ev 3295 |
. . 3
⊢ (((𝑈‘𝑀) ∈ (1...𝑁) ∧ (𝑈‘(𝑀 + 1)) ∈ (1...𝑁) ∧ ((((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))) ∧ (𝑈‘𝑀) ≠ (𝑈‘(𝑀 + 1)))) → ∃𝑛 ∈ (1...𝑁)∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚)) |
267 | 18, 23, 248, 256, 266 | syl112anc 1322 |
. 2
⊢ (𝜑 → ∃𝑛 ∈ (1...𝑁)∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚)) |
268 | | dfrex2 2979 |
. . 3
⊢
(∃𝑛 ∈
(1...𝑁)∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ¬ ∀𝑛 ∈ (1...𝑁) ¬ ∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚)) |
269 | | fveq2 6103 |
. . . . . 6
⊢ (𝑛 = 𝑚 → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘(𝑀 − 1))‘𝑚)) |
270 | | fveq2 6103 |
. . . . . 6
⊢ (𝑛 = 𝑚 → ((𝐹‘𝑀)‘𝑛) = ((𝐹‘𝑀)‘𝑚)) |
271 | 269, 270 | neeq12d 2843 |
. . . . 5
⊢ (𝑛 = 𝑚 → (((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚))) |
272 | 271 | rmo4 3366 |
. . . 4
⊢
(∃*𝑛 ∈
(1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁)∀𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚)) |
273 | | dfral2 2977 |
. . . . . 6
⊢
(∀𝑚 ∈
(1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚) ↔ ¬ ∃𝑚 ∈ (1...𝑁) ¬ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚)) |
274 | | df-ne 2782 |
. . . . . . . . 9
⊢ (𝑛 ≠ 𝑚 ↔ ¬ 𝑛 = 𝑚) |
275 | 274 | anbi2i 726 |
. . . . . . . 8
⊢
(((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ ¬ 𝑛 = 𝑚)) |
276 | | annim 440 |
. . . . . . . 8
⊢
(((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ ¬ 𝑛 = 𝑚) ↔ ¬ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚)) |
277 | 275, 276 | bitri 263 |
. . . . . . 7
⊢
(((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ¬ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚)) |
278 | 277 | rexbii 3023 |
. . . . . 6
⊢
(∃𝑚 ∈
(1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ∃𝑚 ∈ (1...𝑁) ¬ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚)) |
279 | 273, 278 | xchbinxr 324 |
. . . . 5
⊢
(∀𝑚 ∈
(1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚) ↔ ¬ ∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚)) |
280 | 279 | ralbii 2963 |
. . . 4
⊢
(∀𝑛 ∈
(1...𝑁)∀𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚) ↔ ∀𝑛 ∈ (1...𝑁) ¬ ∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚)) |
281 | 272, 280 | bitri 263 |
. . 3
⊢
(∃*𝑛 ∈
(1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁) ¬ ∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚)) |
282 | 268, 281 | xchbinxr 324 |
. 2
⊢
(∃𝑛 ∈
(1...𝑁)∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛)) |
283 | 267, 282 | sylib 207 |
1
⊢ (𝜑 → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛)) |