Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  poimirlem1 Structured version   Visualization version   GIF version

Theorem poimirlem1 32379
Description: Lemma for poimir 32411- the vertices on either side of a skipped vertex differ in at least two dimensions. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0 (𝜑𝑁 ∈ ℕ)
poimirlem2.1 (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))
poimirlem2.2 (𝜑𝑇:(1...𝑁)⟶ℤ)
poimirlem2.3 (𝜑𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
poimirlem1.4 (𝜑𝑀 ∈ (1...(𝑁 − 1)))
Assertion
Ref Expression
poimirlem1 (𝜑 → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛))
Distinct variable groups:   𝑗,𝑛,𝑦,𝜑   𝑗,𝐹,𝑛,𝑦   𝑗,𝑀,𝑛,𝑦   𝑗,𝑁,𝑛,𝑦   𝑇,𝑗,𝑛,𝑦   𝑈,𝑗,𝑛,𝑦

Proof of Theorem poimirlem1
Dummy variable 𝑚 is distinct from all other variables.
StepHypRef Expression
1 poimirlem2.3 . . . . 5 (𝜑𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
2 f1of 6031 . . . . 5 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)⟶(1...𝑁))
31, 2syl 17 . . . 4 (𝜑𝑈:(1...𝑁)⟶(1...𝑁))
4 poimir.0 . . . . . . . . 9 (𝜑𝑁 ∈ ℕ)
54nncnd 10879 . . . . . . . 8 (𝜑𝑁 ∈ ℂ)
6 npcan1 10302 . . . . . . . 8 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
75, 6syl 17 . . . . . . 7 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
84nnzd 11309 . . . . . . . 8 (𝜑𝑁 ∈ ℤ)
9 peano2zm 11249 . . . . . . . 8 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
10 uzid 11530 . . . . . . . 8 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
11 peano2uz 11569 . . . . . . . 8 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
128, 9, 10, 114syl 19 . . . . . . 7 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
137, 12eqeltrrd 2684 . . . . . 6 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
14 fzss2 12203 . . . . . 6 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
1513, 14syl 17 . . . . 5 (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
16 poimirlem1.4 . . . . 5 (𝜑𝑀 ∈ (1...(𝑁 − 1)))
1715, 16sseldd 3564 . . . 4 (𝜑𝑀 ∈ (1...𝑁))
183, 17ffvelrnd 6249 . . 3 (𝜑 → (𝑈𝑀) ∈ (1...𝑁))
19 fzp1elp1 12215 . . . . . 6 (𝑀 ∈ (1...(𝑁 − 1)) → (𝑀 + 1) ∈ (1...((𝑁 − 1) + 1)))
2016, 19syl 17 . . . . 5 (𝜑 → (𝑀 + 1) ∈ (1...((𝑁 − 1) + 1)))
217oveq2d 6539 . . . . 5 (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁))
2220, 21eleqtrd 2685 . . . 4 (𝜑 → (𝑀 + 1) ∈ (1...𝑁))
233, 22ffvelrnd 6249 . . 3 (𝜑 → (𝑈‘(𝑀 + 1)) ∈ (1...𝑁))
24 imassrn 5379 . . . . . . . . . 10 (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ ran 𝑈
25 frn 5948 . . . . . . . . . . 11 (𝑈:(1...𝑁)⟶(1...𝑁) → ran 𝑈 ⊆ (1...𝑁))
261, 2, 253syl 18 . . . . . . . . . 10 (𝜑 → ran 𝑈 ⊆ (1...𝑁))
2724, 26syl5ss 3574 . . . . . . . . 9 (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (1...𝑁))
2827sselda 3563 . . . . . . . 8 ((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → 𝑛 ∈ (1...𝑁))
29 poimirlem2.2 . . . . . . . . . . 11 (𝜑𝑇:(1...𝑁)⟶ℤ)
3029ffvelrnda 6248 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑇𝑛) ∈ ℤ)
3130zred 11310 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑇𝑛) ∈ ℝ)
3231ltp1d 10799 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑇𝑛) < ((𝑇𝑛) + 1))
3331, 32ltned 10020 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑇𝑛) ≠ ((𝑇𝑛) + 1))
3428, 33syldan 485 . . . . . . 7 ((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (𝑇𝑛) ≠ ((𝑇𝑛) + 1))
35 poimirlem2.1 . . . . . . . . . . 11 (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))
36 breq1 4576 . . . . . . . . . . . . . . 15 (𝑦 = (𝑀 − 1) → (𝑦 < 𝑀 ↔ (𝑀 − 1) < 𝑀))
37 id 22 . . . . . . . . . . . . . . 15 (𝑦 = (𝑀 − 1) → 𝑦 = (𝑀 − 1))
3836, 37ifbieq1d 4054 . . . . . . . . . . . . . 14 (𝑦 = (𝑀 − 1) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑀 − 1) < 𝑀, (𝑀 − 1), (𝑦 + 1)))
39 elfzelz 12164 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ (1...(𝑁 − 1)) → 𝑀 ∈ ℤ)
4016, 39syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ ℤ)
4140zred 11310 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℝ)
4241ltm1d 10801 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 − 1) < 𝑀)
4342iftrued 4039 . . . . . . . . . . . . . 14 (𝜑 → if((𝑀 − 1) < 𝑀, (𝑀 − 1), (𝑦 + 1)) = (𝑀 − 1))
4438, 43sylan9eqr 2661 . . . . . . . . . . . . 13 ((𝜑𝑦 = (𝑀 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑀 − 1))
4544csbeq1d 3501 . . . . . . . . . . . 12 ((𝜑𝑦 = (𝑀 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑀 − 1) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
468, 9syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 − 1) ∈ ℤ)
47 elfzm1b 12238 . . . . . . . . . . . . . . . 16 ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑀 ∈ (1...(𝑁 − 1)) ↔ (𝑀 − 1) ∈ (0...((𝑁 − 1) − 1))))
4840, 46, 47syl2anc 690 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 ∈ (1...(𝑁 − 1)) ↔ (𝑀 − 1) ∈ (0...((𝑁 − 1) − 1))))
4916, 48mpbid 220 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 − 1) ∈ (0...((𝑁 − 1) − 1)))
50 oveq2 6531 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑀 − 1) → (1...𝑗) = (1...(𝑀 − 1)))
5150imaeq2d 5368 . . . . . . . . . . . . . . . . . 18 (𝑗 = (𝑀 − 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑀 − 1))))
5251xpeq1d 5048 . . . . . . . . . . . . . . . . 17 (𝑗 = (𝑀 − 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑀 − 1))) × {1}))
5352adantl 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 = (𝑀 − 1)) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑀 − 1))) × {1}))
54 oveq1 6530 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = (𝑀 − 1) → (𝑗 + 1) = ((𝑀 − 1) + 1))
5540zcnd 11311 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑀 ∈ ℂ)
56 npcan1 10302 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 ∈ ℂ → ((𝑀 − 1) + 1) = 𝑀)
5755, 56syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
5854, 57sylan9eqr 2661 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 = (𝑀 − 1)) → (𝑗 + 1) = 𝑀)
5958oveq1d 6538 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 = (𝑀 − 1)) → ((𝑗 + 1)...𝑁) = (𝑀...𝑁))
6059imaeq2d 5368 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 = (𝑀 − 1)) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (𝑀...𝑁)))
6160xpeq1d 5048 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 = (𝑀 − 1)) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (𝑀...𝑁)) × {0}))
6253, 61uneq12d 3725 . . . . . . . . . . . . . . 15 ((𝜑𝑗 = (𝑀 − 1)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))
6362oveq2d 6539 . . . . . . . . . . . . . 14 ((𝜑𝑗 = (𝑀 − 1)) → (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇𝑓 + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))))
6449, 63csbied 3521 . . . . . . . . . . . . 13 (𝜑(𝑀 − 1) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇𝑓 + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))))
6564adantr 479 . . . . . . . . . . . 12 ((𝜑𝑦 = (𝑀 − 1)) → (𝑀 − 1) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇𝑓 + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))))
6645, 65eqtrd 2639 . . . . . . . . . . 11 ((𝜑𝑦 = (𝑀 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇𝑓 + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))))
6746zcnd 11311 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 − 1) ∈ ℂ)
68 npcan1 10302 . . . . . . . . . . . . . . 15 ((𝑁 − 1) ∈ ℂ → (((𝑁 − 1) − 1) + 1) = (𝑁 − 1))
6967, 68syl 17 . . . . . . . . . . . . . 14 (𝜑 → (((𝑁 − 1) − 1) + 1) = (𝑁 − 1))
70 peano2zm 11249 . . . . . . . . . . . . . . 15 ((𝑁 − 1) ∈ ℤ → ((𝑁 − 1) − 1) ∈ ℤ)
71 uzid 11530 . . . . . . . . . . . . . . 15 (((𝑁 − 1) − 1) ∈ ℤ → ((𝑁 − 1) − 1) ∈ (ℤ‘((𝑁 − 1) − 1)))
72 peano2uz 11569 . . . . . . . . . . . . . . 15 (((𝑁 − 1) − 1) ∈ (ℤ‘((𝑁 − 1) − 1)) → (((𝑁 − 1) − 1) + 1) ∈ (ℤ‘((𝑁 − 1) − 1)))
7346, 70, 71, 724syl 19 . . . . . . . . . . . . . 14 (𝜑 → (((𝑁 − 1) − 1) + 1) ∈ (ℤ‘((𝑁 − 1) − 1)))
7469, 73eqeltrrd 2684 . . . . . . . . . . . . 13 (𝜑 → (𝑁 − 1) ∈ (ℤ‘((𝑁 − 1) − 1)))
75 fzss2 12203 . . . . . . . . . . . . 13 ((𝑁 − 1) ∈ (ℤ‘((𝑁 − 1) − 1)) → (0...((𝑁 − 1) − 1)) ⊆ (0...(𝑁 − 1)))
7674, 75syl 17 . . . . . . . . . . . 12 (𝜑 → (0...((𝑁 − 1) − 1)) ⊆ (0...(𝑁 − 1)))
7776, 49sseldd 3564 . . . . . . . . . . 11 (𝜑 → (𝑀 − 1) ∈ (0...(𝑁 − 1)))
78 ovex 6551 . . . . . . . . . . . 12 (𝑇𝑓 + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))) ∈ V
7978a1i 11 . . . . . . . . . . 11 (𝜑 → (𝑇𝑓 + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))) ∈ V)
8035, 66, 77, 79fvmptd 6178 . . . . . . . . . 10 (𝜑 → (𝐹‘(𝑀 − 1)) = (𝑇𝑓 + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))))
8180fveq1d 6086 . . . . . . . . 9 (𝜑 → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝑇𝑓 + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))‘𝑛))
8281adantr 479 . . . . . . . 8 ((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝑇𝑓 + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))‘𝑛))
83 ffn 5940 . . . . . . . . . . . 12 (𝑇:(1...𝑁)⟶ℤ → 𝑇 Fn (1...𝑁))
8429, 83syl 17 . . . . . . . . . . 11 (𝜑𝑇 Fn (1...𝑁))
8584adantr 479 . . . . . . . . . 10 ((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → 𝑇 Fn (1...𝑁))
86 1ex 9887 . . . . . . . . . . . . . . 15 1 ∈ V
87 fnconstg 5987 . . . . . . . . . . . . . . 15 (1 ∈ V → ((𝑈 “ (1...(𝑀 − 1))) × {1}) Fn (𝑈 “ (1...(𝑀 − 1))))
8886, 87ax-mp 5 . . . . . . . . . . . . . 14 ((𝑈 “ (1...(𝑀 − 1))) × {1}) Fn (𝑈 “ (1...(𝑀 − 1)))
89 c0ex 9886 . . . . . . . . . . . . . . 15 0 ∈ V
90 fnconstg 5987 . . . . . . . . . . . . . . 15 (0 ∈ V → ((𝑈 “ (𝑀...𝑁)) × {0}) Fn (𝑈 “ (𝑀...𝑁)))
9189, 90ax-mp 5 . . . . . . . . . . . . . 14 ((𝑈 “ (𝑀...𝑁)) × {0}) Fn (𝑈 “ (𝑀...𝑁))
9288, 91pm3.2i 469 . . . . . . . . . . . . 13 (((𝑈 “ (1...(𝑀 − 1))) × {1}) Fn (𝑈 “ (1...(𝑀 − 1))) ∧ ((𝑈 “ (𝑀...𝑁)) × {0}) Fn (𝑈 “ (𝑀...𝑁)))
93 dff1o3 6037 . . . . . . . . . . . . . . . 16 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun 𝑈))
9493simprbi 478 . . . . . . . . . . . . . . 15 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun 𝑈)
95 imain 5870 . . . . . . . . . . . . . . 15 (Fun 𝑈 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))))
961, 94, 953syl 18 . . . . . . . . . . . . . 14 (𝜑 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))))
97 fzdisj 12190 . . . . . . . . . . . . . . . . 17 ((𝑀 − 1) < 𝑀 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑁)) = ∅)
9842, 97syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑁)) = ∅)
9998imaeq2d 5368 . . . . . . . . . . . . . . 15 (𝜑 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = (𝑈 “ ∅))
100 ima0 5383 . . . . . . . . . . . . . . 15 (𝑈 “ ∅) = ∅
10199, 100syl6eq 2655 . . . . . . . . . . . . . 14 (𝜑 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ∅)
10296, 101eqtr3d 2641 . . . . . . . . . . . . 13 (𝜑 → ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅)
103 fnun 5893 . . . . . . . . . . . . 13 (((((𝑈 “ (1...(𝑀 − 1))) × {1}) Fn (𝑈 “ (1...(𝑀 − 1))) ∧ ((𝑈 “ (𝑀...𝑁)) × {0}) Fn (𝑈 “ (𝑀...𝑁))) ∧ ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅) → (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁))))
10492, 102, 103sylancr 693 . . . . . . . . . . . 12 (𝜑 → (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁))))
105 elfzuz 12160 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ (1...(𝑁 − 1)) → 𝑀 ∈ (ℤ‘1))
10616, 105syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑀 ∈ (ℤ‘1))
10757, 106eqeltrd 2683 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑀 − 1) + 1) ∈ (ℤ‘1))
108 peano2zm 11249 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
109 uzid 11530 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀 − 1) ∈ ℤ → (𝑀 − 1) ∈ (ℤ‘(𝑀 − 1)))
110 peano2uz 11569 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀 − 1) ∈ (ℤ‘(𝑀 − 1)) → ((𝑀 − 1) + 1) ∈ (ℤ‘(𝑀 − 1)))
11140, 108, 109, 1104syl 19 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑀 − 1) + 1) ∈ (ℤ‘(𝑀 − 1)))
11257, 111eqeltrrd 2684 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 ∈ (ℤ‘(𝑀 − 1)))
113 peano2uz 11569 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ (ℤ‘(𝑀 − 1)) → (𝑀 + 1) ∈ (ℤ‘(𝑀 − 1)))
114 uzss 11536 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 + 1) ∈ (ℤ‘(𝑀 − 1)) → (ℤ‘(𝑀 + 1)) ⊆ (ℤ‘(𝑀 − 1)))
115112, 113, 1143syl 18 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (ℤ‘(𝑀 + 1)) ⊆ (ℤ‘(𝑀 − 1)))
116 elfzuz3 12161 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 ∈ (1...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ𝑀))
117 eluzp1p1 11541 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 − 1) ∈ (ℤ𝑀) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑀 + 1)))
11816, 116, 1173syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑀 + 1)))
1197, 118eqeltrrd 2684 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ (ℤ‘(𝑀 + 1)))
120115, 119sseldd 3564 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ (ℤ‘(𝑀 − 1)))
121 fzsplit2 12188 . . . . . . . . . . . . . . . . . 18 ((((𝑀 − 1) + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ‘(𝑀 − 1))) → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁)))
122107, 120, 121syl2anc 690 . . . . . . . . . . . . . . . . 17 (𝜑 → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁)))
12357oveq1d 6538 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑀 − 1) + 1)...𝑁) = (𝑀...𝑁))
124123uneq2d 3724 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁)) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑁)))
125122, 124eqtrd 2639 . . . . . . . . . . . . . . . 16 (𝜑 → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑁)))
126125imaeq2d 5368 . . . . . . . . . . . . . . 15 (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))))
127 imaundi 5446 . . . . . . . . . . . . . . 15 (𝑈 “ ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))) = ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁)))
128126, 127syl6eq 2655 . . . . . . . . . . . . . 14 (𝜑 → (𝑈 “ (1...𝑁)) = ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁))))
129 f1ofo 6038 . . . . . . . . . . . . . . 15 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁))
130 foima 6014 . . . . . . . . . . . . . . 15 (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁))
1311, 129, 1303syl 18 . . . . . . . . . . . . . 14 (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁))
132128, 131eqtr3d 2641 . . . . . . . . . . . . 13 (𝜑 → ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁))) = (1...𝑁))
133132fneq2d 5878 . . . . . . . . . . . 12 (𝜑 → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁))) ↔ (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn (1...𝑁)))
134104, 133mpbid 220 . . . . . . . . . . 11 (𝜑 → (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn (1...𝑁))
135134adantr 479 . . . . . . . . . 10 ((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn (1...𝑁))
136 ovex 6551 . . . . . . . . . . 11 (1...𝑁) ∈ V
137136a1i 11 . . . . . . . . . 10 ((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (1...𝑁) ∈ V)
138 inidm 3779 . . . . . . . . . 10 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
139 eqidd 2606 . . . . . . . . . 10 (((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇𝑛) = (𝑇𝑛))
140102adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅)
141 fzss2 12203 . . . . . . . . . . . . . . 15 (𝑁 ∈ (ℤ‘(𝑀 + 1)) → (𝑀...(𝑀 + 1)) ⊆ (𝑀...𝑁))
142 imass2 5403 . . . . . . . . . . . . . . 15 ((𝑀...(𝑀 + 1)) ⊆ (𝑀...𝑁) → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (𝑀...𝑁)))
143119, 141, 1423syl 18 . . . . . . . . . . . . . 14 (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (𝑀...𝑁)))
144143sselda 3563 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → 𝑛 ∈ (𝑈 “ (𝑀...𝑁)))
145 fvun2 6161 . . . . . . . . . . . . . 14 ((((𝑈 “ (1...(𝑀 − 1))) × {1}) Fn (𝑈 “ (1...(𝑀 − 1))) ∧ ((𝑈 “ (𝑀...𝑁)) × {0}) Fn (𝑈 “ (𝑀...𝑁)) ∧ (((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (𝑀...𝑁)))) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛))
14688, 91, 145mp3an12 1405 . . . . . . . . . . . . 13 ((((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (𝑀...𝑁))) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛))
147140, 144, 146syl2anc 690 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛))
14889fvconst2 6348 . . . . . . . . . . . . 13 (𝑛 ∈ (𝑈 “ (𝑀...𝑁)) → (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛) = 0)
149144, 148syl 17 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛) = 0)
150147, 149eqtrd 2639 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = 0)
151150adantr 479 . . . . . . . . . 10 (((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = 0)
15285, 135, 137, 137, 138, 139, 151ofval 6777 . . . . . . . . 9 (((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇𝑓 + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))‘𝑛) = ((𝑇𝑛) + 0))
15328, 152mpdan 698 . . . . . . . 8 ((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑇𝑓 + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))‘𝑛) = ((𝑇𝑛) + 0))
15430zcnd 11311 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑇𝑛) ∈ ℂ)
155154addid1d 10083 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑇𝑛) + 0) = (𝑇𝑛))
15628, 155syldan 485 . . . . . . . 8 ((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑇𝑛) + 0) = (𝑇𝑛))
15782, 153, 1563eqtrd 2643 . . . . . . 7 ((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘(𝑀 − 1))‘𝑛) = (𝑇𝑛))
158 breq1 4576 . . . . . . . . . . . . . . 15 (𝑦 = 𝑀 → (𝑦 < 𝑀𝑀 < 𝑀))
159 oveq1 6530 . . . . . . . . . . . . . . 15 (𝑦 = 𝑀 → (𝑦 + 1) = (𝑀 + 1))
160158, 159ifbieq2d 4056 . . . . . . . . . . . . . 14 (𝑦 = 𝑀 → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if(𝑀 < 𝑀, 𝑦, (𝑀 + 1)))
16141ltnrd 10018 . . . . . . . . . . . . . . 15 (𝜑 → ¬ 𝑀 < 𝑀)
162161iffalsed 4042 . . . . . . . . . . . . . 14 (𝜑 → if(𝑀 < 𝑀, 𝑦, (𝑀 + 1)) = (𝑀 + 1))
163160, 162sylan9eqr 2661 . . . . . . . . . . . . 13 ((𝜑𝑦 = 𝑀) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑀 + 1))
164163csbeq1d 3501 . . . . . . . . . . . 12 ((𝜑𝑦 = 𝑀) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑀 + 1) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
165 ovex 6551 . . . . . . . . . . . . 13 (𝑀 + 1) ∈ V
166 oveq2 6531 . . . . . . . . . . . . . . . . 17 (𝑗 = (𝑀 + 1) → (1...𝑗) = (1...(𝑀 + 1)))
167166imaeq2d 5368 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑀 + 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑀 + 1))))
168167xpeq1d 5048 . . . . . . . . . . . . . . 15 (𝑗 = (𝑀 + 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑀 + 1))) × {1}))
169 oveq1 6530 . . . . . . . . . . . . . . . . . 18 (𝑗 = (𝑀 + 1) → (𝑗 + 1) = ((𝑀 + 1) + 1))
170169oveq1d 6538 . . . . . . . . . . . . . . . . 17 (𝑗 = (𝑀 + 1) → ((𝑗 + 1)...𝑁) = (((𝑀 + 1) + 1)...𝑁))
171170imaeq2d 5368 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑀 + 1) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (((𝑀 + 1) + 1)...𝑁)))
172171xpeq1d 5048 . . . . . . . . . . . . . . 15 (𝑗 = (𝑀 + 1) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))
173168, 172uneq12d 3725 . . . . . . . . . . . . . 14 (𝑗 = (𝑀 + 1) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))
174173oveq2d 6539 . . . . . . . . . . . . 13 (𝑗 = (𝑀 + 1) → (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇𝑓 + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))))
175165, 174csbie 3520 . . . . . . . . . . . 12 (𝑀 + 1) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇𝑓 + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))
176164, 175syl6eq 2655 . . . . . . . . . . 11 ((𝜑𝑦 = 𝑀) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇𝑓 + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))))
177 1eluzge0 11560 . . . . . . . . . . . . 13 1 ∈ (ℤ‘0)
178 fzss1 12202 . . . . . . . . . . . . 13 (1 ∈ (ℤ‘0) → (1...(𝑁 − 1)) ⊆ (0...(𝑁 − 1)))
179177, 178ax-mp 5 . . . . . . . . . . . 12 (1...(𝑁 − 1)) ⊆ (0...(𝑁 − 1))
180179, 16sseldi 3561 . . . . . . . . . . 11 (𝜑𝑀 ∈ (0...(𝑁 − 1)))
181 ovex 6551 . . . . . . . . . . . 12 (𝑇𝑓 + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))) ∈ V
182181a1i 11 . . . . . . . . . . 11 (𝜑 → (𝑇𝑓 + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))) ∈ V)
18335, 176, 180, 182fvmptd 6178 . . . . . . . . . 10 (𝜑 → (𝐹𝑀) = (𝑇𝑓 + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))))
184183fveq1d 6086 . . . . . . . . 9 (𝜑 → ((𝐹𝑀)‘𝑛) = ((𝑇𝑓 + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))‘𝑛))
185184adantr 479 . . . . . . . 8 ((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹𝑀)‘𝑛) = ((𝑇𝑓 + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))‘𝑛))
186 fnconstg 5987 . . . . . . . . . . . . . . 15 (1 ∈ V → ((𝑈 “ (1...(𝑀 + 1))) × {1}) Fn (𝑈 “ (1...(𝑀 + 1))))
18786, 186ax-mp 5 . . . . . . . . . . . . . 14 ((𝑈 “ (1...(𝑀 + 1))) × {1}) Fn (𝑈 “ (1...(𝑀 + 1)))
188 fnconstg 5987 . . . . . . . . . . . . . . 15 (0 ∈ V → ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑀 + 1) + 1)...𝑁)))
18989, 188ax-mp 5 . . . . . . . . . . . . . 14 ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑀 + 1) + 1)...𝑁))
190187, 189pm3.2i 469 . . . . . . . . . . . . 13 (((𝑈 “ (1...(𝑀 + 1))) × {1}) Fn (𝑈 “ (1...(𝑀 + 1))) ∧ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑀 + 1) + 1)...𝑁)))
191 imain 5870 . . . . . . . . . . . . . . . 16 (Fun 𝑈 → (𝑈 “ ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))))
1921, 94, 1913syl 18 . . . . . . . . . . . . . . 15 (𝜑 → (𝑈 “ ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))))
193 peano2re 10056 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
19441, 193syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑀 + 1) ∈ ℝ)
195194ltp1d 10799 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 + 1) < ((𝑀 + 1) + 1))
196 fzdisj 12190 . . . . . . . . . . . . . . . . 17 ((𝑀 + 1) < ((𝑀 + 1) + 1) → ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁)) = ∅)
197195, 196syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁)) = ∅)
198197imaeq2d 5368 . . . . . . . . . . . . . . 15 (𝜑 → (𝑈 “ ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁))) = (𝑈 “ ∅))
199192, 198eqtr3d 2641 . . . . . . . . . . . . . 14 (𝜑 → ((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = (𝑈 “ ∅))
200199, 100syl6eq 2655 . . . . . . . . . . . . 13 (𝜑 → ((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = ∅)
201 fnun 5893 . . . . . . . . . . . . 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)...𝑁))))
202190, 200, 201sylancr 693 . . . . . . . . . . . 12 (𝜑 → (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))))
203 fzsplit 12189 . . . . . . . . . . . . . . . . 17 ((𝑀 + 1) ∈ (1...𝑁) → (1...𝑁) = ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)))
20422, 203syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (1...𝑁) = ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)))
205204imaeq2d 5368 . . . . . . . . . . . . . . 15 (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁))))
206 imaundi 5446 . . . . . . . . . . . . . . 15 (𝑈 “ ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁)))
207205, 206syl6eq 2655 . . . . . . . . . . . . . 14 (𝜑 → (𝑈 “ (1...𝑁)) = ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))))
208207, 131eqtr3d 2641 . . . . . . . . . . . . 13 (𝜑 → ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = (1...𝑁))
209208fneq2d 5878 . . . . . . . . . . . 12 (𝜑 → ((((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) ↔ (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁)))
210202, 209mpbid 220 . . . . . . . . . . 11 (𝜑 → (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))
211210adantr 479 . . . . . . . . . 10 ((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))
212200adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = ∅)
213 fzss1 12202 . . . . . . . . . . . . . . 15 (𝑀 ∈ (ℤ‘1) → (𝑀...(𝑀 + 1)) ⊆ (1...(𝑀 + 1)))
214 imass2 5403 . . . . . . . . . . . . . . 15 ((𝑀...(𝑀 + 1)) ⊆ (1...(𝑀 + 1)) → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (1...(𝑀 + 1))))
215106, 213, 2143syl 18 . . . . . . . . . . . . . 14 (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (1...(𝑀 + 1))))
216215sselda 3563 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → 𝑛 ∈ (𝑈 “ (1...(𝑀 + 1))))
217 fvun1 6160 . . . . . . . . . . . . . 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})‘𝑛))
218187, 189, 217mp3an12 1405 . . . . . . . . . . . . 13 ((((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑀 + 1)))) → ((((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑀 + 1))) × {1})‘𝑛))
219212, 216, 218syl2anc 690 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑀 + 1))) × {1})‘𝑛))
22086fvconst2 6348 . . . . . . . . . . . . 13 (𝑛 ∈ (𝑈 “ (1...(𝑀 + 1))) → (((𝑈 “ (1...(𝑀 + 1))) × {1})‘𝑛) = 1)
221216, 220syl 17 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (((𝑈 “ (1...(𝑀 + 1))) × {1})‘𝑛) = 1)
222219, 221eqtrd 2639 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1)
223222adantr 479 . . . . . . . . . 10 (((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1)
22485, 211, 137, 137, 138, 139, 223ofval 6777 . . . . . . . . 9 (((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇𝑓 + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇𝑛) + 1))
22528, 224mpdan 698 . . . . . . . 8 ((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑇𝑓 + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇𝑛) + 1))
226185, 225eqtrd 2639 . . . . . . 7 ((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹𝑀)‘𝑛) = ((𝑇𝑛) + 1))
22734, 157, 2263netr4d 2854 . . . . . 6 ((𝜑𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛))
228227ralrimiva 2944 . . . . 5 (𝜑 → ∀𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛))
229 fzpr 12217 . . . . . . . . 9 (𝑀 ∈ ℤ → (𝑀...(𝑀 + 1)) = {𝑀, (𝑀 + 1)})
23016, 39, 2293syl 18 . . . . . . . 8 (𝜑 → (𝑀...(𝑀 + 1)) = {𝑀, (𝑀 + 1)})
231230imaeq2d 5368 . . . . . . 7 (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) = (𝑈 “ {𝑀, (𝑀 + 1)}))
232 f1ofn 6032 . . . . . . . . 9 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 Fn (1...𝑁))
2331, 232syl 17 . . . . . . . 8 (𝜑𝑈 Fn (1...𝑁))
234 fnimapr 6153 . . . . . . . 8 ((𝑈 Fn (1...𝑁) ∧ 𝑀 ∈ (1...𝑁) ∧ (𝑀 + 1) ∈ (1...𝑁)) → (𝑈 “ {𝑀, (𝑀 + 1)}) = {(𝑈𝑀), (𝑈‘(𝑀 + 1))})
235233, 17, 22, 234syl3anc 1317 . . . . . . 7 (𝜑 → (𝑈 “ {𝑀, (𝑀 + 1)}) = {(𝑈𝑀), (𝑈‘(𝑀 + 1))})
236231, 235eqtrd 2639 . . . . . 6 (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) = {(𝑈𝑀), (𝑈‘(𝑀 + 1))})
237236raleqdv 3116 . . . . 5 (𝜑 → (∀𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ↔ ∀𝑛 ∈ {(𝑈𝑀), (𝑈‘(𝑀 + 1))} ((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛)))
238228, 237mpbid 220 . . . 4 (𝜑 → ∀𝑛 ∈ {(𝑈𝑀), (𝑈‘(𝑀 + 1))} ((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛))
239 fvex 6094 . . . . 5 (𝑈𝑀) ∈ V
240 fvex 6094 . . . . 5 (𝑈‘(𝑀 + 1)) ∈ V
241 fveq2 6084 . . . . . 6 (𝑛 = (𝑈𝑀) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘(𝑀 − 1))‘(𝑈𝑀)))
242 fveq2 6084 . . . . . 6 (𝑛 = (𝑈𝑀) → ((𝐹𝑀)‘𝑛) = ((𝐹𝑀)‘(𝑈𝑀)))
243241, 242neeq12d 2838 . . . . 5 (𝑛 = (𝑈𝑀) → (((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ↔ ((𝐹‘(𝑀 − 1))‘(𝑈𝑀)) ≠ ((𝐹𝑀)‘(𝑈𝑀))))
244 fveq2 6084 . . . . . 6 (𝑛 = (𝑈‘(𝑀 + 1)) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))))
245 fveq2 6084 . . . . . 6 (𝑛 = (𝑈‘(𝑀 + 1)) → ((𝐹𝑀)‘𝑛) = ((𝐹𝑀)‘(𝑈‘(𝑀 + 1))))
246244, 245neeq12d 2838 . . . . 5 (𝑛 = (𝑈‘(𝑀 + 1)) → (((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ↔ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹𝑀)‘(𝑈‘(𝑀 + 1)))))
247239, 240, 243, 246ralpr 4180 . . . 4 (∀𝑛 ∈ {(𝑈𝑀), (𝑈‘(𝑀 + 1))} ((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ↔ (((𝐹‘(𝑀 − 1))‘(𝑈𝑀)) ≠ ((𝐹𝑀)‘(𝑈𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹𝑀)‘(𝑈‘(𝑀 + 1)))))
248238, 247sylib 206 . . 3 (𝜑 → (((𝐹‘(𝑀 − 1))‘(𝑈𝑀)) ≠ ((𝐹𝑀)‘(𝑈𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹𝑀)‘(𝑈‘(𝑀 + 1)))))
24941ltp1d 10799 . . . . 5 (𝜑𝑀 < (𝑀 + 1))
25041, 249ltned 10020 . . . 4 (𝜑𝑀 ≠ (𝑀 + 1))
251 f1of1 6030 . . . . . . 7 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–1-1→(1...𝑁))
2521, 251syl 17 . . . . . 6 (𝜑𝑈:(1...𝑁)–1-1→(1...𝑁))
253 f1veqaeq 6392 . . . . . 6 ((𝑈:(1...𝑁)–1-1→(1...𝑁) ∧ (𝑀 ∈ (1...𝑁) ∧ (𝑀 + 1) ∈ (1...𝑁))) → ((𝑈𝑀) = (𝑈‘(𝑀 + 1)) → 𝑀 = (𝑀 + 1)))
254252, 17, 22, 253syl12anc 1315 . . . . 5 (𝜑 → ((𝑈𝑀) = (𝑈‘(𝑀 + 1)) → 𝑀 = (𝑀 + 1)))
255254necon3d 2798 . . . 4 (𝜑 → (𝑀 ≠ (𝑀 + 1) → (𝑈𝑀) ≠ (𝑈‘(𝑀 + 1))))
256250, 255mpd 15 . . 3 (𝜑 → (𝑈𝑀) ≠ (𝑈‘(𝑀 + 1)))
257243anbi1d 736 . . . . 5 (𝑛 = (𝑈𝑀) → ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚)) ↔ (((𝐹‘(𝑀 − 1))‘(𝑈𝑀)) ≠ ((𝐹𝑀)‘(𝑈𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚))))
258 neeq1 2839 . . . . 5 (𝑛 = (𝑈𝑀) → (𝑛𝑚 ↔ (𝑈𝑀) ≠ 𝑚))
259257, 258anbi12d 742 . . . 4 (𝑛 = (𝑈𝑀) → (((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚)) ∧ 𝑛𝑚) ↔ ((((𝐹‘(𝑀 − 1))‘(𝑈𝑀)) ≠ ((𝐹𝑀)‘(𝑈𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚)) ∧ (𝑈𝑀) ≠ 𝑚)))
260 fveq2 6084 . . . . . . 7 (𝑚 = (𝑈‘(𝑀 + 1)) → ((𝐹‘(𝑀 − 1))‘𝑚) = ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))))
261 fveq2 6084 . . . . . . 7 (𝑚 = (𝑈‘(𝑀 + 1)) → ((𝐹𝑀)‘𝑚) = ((𝐹𝑀)‘(𝑈‘(𝑀 + 1))))
262260, 261neeq12d 2838 . . . . . 6 (𝑚 = (𝑈‘(𝑀 + 1)) → (((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚) ↔ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹𝑀)‘(𝑈‘(𝑀 + 1)))))
263262anbi2d 735 . . . . 5 (𝑚 = (𝑈‘(𝑀 + 1)) → ((((𝐹‘(𝑀 − 1))‘(𝑈𝑀)) ≠ ((𝐹𝑀)‘(𝑈𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚)) ↔ (((𝐹‘(𝑀 − 1))‘(𝑈𝑀)) ≠ ((𝐹𝑀)‘(𝑈𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹𝑀)‘(𝑈‘(𝑀 + 1))))))
264 neeq2 2840 . . . . 5 (𝑚 = (𝑈‘(𝑀 + 1)) → ((𝑈𝑀) ≠ 𝑚 ↔ (𝑈𝑀) ≠ (𝑈‘(𝑀 + 1))))
265263, 264anbi12d 742 . . . 4 (𝑚 = (𝑈‘(𝑀 + 1)) → (((((𝐹‘(𝑀 − 1))‘(𝑈𝑀)) ≠ ((𝐹𝑀)‘(𝑈𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚)) ∧ (𝑈𝑀) ≠ 𝑚) ↔ ((((𝐹‘(𝑀 − 1))‘(𝑈𝑀)) ≠ ((𝐹𝑀)‘(𝑈𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹𝑀)‘(𝑈‘(𝑀 + 1)))) ∧ (𝑈𝑀) ≠ (𝑈‘(𝑀 + 1)))))
266259, 265rspc2ev 3290 . . 3 (((𝑈𝑀) ∈ (1...𝑁) ∧ (𝑈‘(𝑀 + 1)) ∈ (1...𝑁) ∧ ((((𝐹‘(𝑀 − 1))‘(𝑈𝑀)) ≠ ((𝐹𝑀)‘(𝑈𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹𝑀)‘(𝑈‘(𝑀 + 1)))) ∧ (𝑈𝑀) ≠ (𝑈‘(𝑀 + 1)))) → ∃𝑛 ∈ (1...𝑁)∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚)) ∧ 𝑛𝑚))
26718, 23, 248, 256, 266syl112anc 1321 . 2 (𝜑 → ∃𝑛 ∈ (1...𝑁)∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚)) ∧ 𝑛𝑚))
268 dfrex2 2974 . . 3 (∃𝑛 ∈ (1...𝑁)∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚)) ∧ 𝑛𝑚) ↔ ¬ ∀𝑛 ∈ (1...𝑁) ¬ ∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚)) ∧ 𝑛𝑚))
269 fveq2 6084 . . . . . 6 (𝑛 = 𝑚 → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘(𝑀 − 1))‘𝑚))
270 fveq2 6084 . . . . . 6 (𝑛 = 𝑚 → ((𝐹𝑀)‘𝑛) = ((𝐹𝑀)‘𝑚))
271269, 270neeq12d 2838 . . . . 5 (𝑛 = 𝑚 → (((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ↔ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚)))
272271rmo4 3361 . . . 4 (∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁)∀𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚)) → 𝑛 = 𝑚))
273 dfral2 2972 . . . . . 6 (∀𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚)) → 𝑛 = 𝑚) ↔ ¬ ∃𝑚 ∈ (1...𝑁) ¬ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚)) → 𝑛 = 𝑚))
274 df-ne 2777 . . . . . . . . 9 (𝑛𝑚 ↔ ¬ 𝑛 = 𝑚)
275274anbi2i 725 . . . . . . . 8 (((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚)) ∧ 𝑛𝑚) ↔ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚)) ∧ ¬ 𝑛 = 𝑚))
276 annim 439 . . . . . . . 8 (((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚)) ∧ ¬ 𝑛 = 𝑚) ↔ ¬ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚)) → 𝑛 = 𝑚))
277275, 276bitri 262 . . . . . . 7 (((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚)) ∧ 𝑛𝑚) ↔ ¬ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚)) → 𝑛 = 𝑚))
278277rexbii 3018 . . . . . 6 (∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚)) ∧ 𝑛𝑚) ↔ ∃𝑚 ∈ (1...𝑁) ¬ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚)) → 𝑛 = 𝑚))
279273, 278xchbinxr 323 . . . . 5 (∀𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚)) → 𝑛 = 𝑚) ↔ ¬ ∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚)) ∧ 𝑛𝑚))
280279ralbii 2958 . . . 4 (∀𝑛 ∈ (1...𝑁)∀𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚)) → 𝑛 = 𝑚) ↔ ∀𝑛 ∈ (1...𝑁) ¬ ∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚)) ∧ 𝑛𝑚))
281272, 280bitri 262 . . 3 (∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁) ¬ ∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚)) ∧ 𝑛𝑚))
282268, 281xchbinxr 323 . 2 (∃𝑛 ∈ (1...𝑁)∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹𝑀)‘𝑚)) ∧ 𝑛𝑚) ↔ ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛))
283267, 282sylib 206 1 (𝜑 → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹𝑀)‘𝑛))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382   = wceq 1474  wcel 1975  wne 2775  wral 2891  wrex 2892  ∃*wrmo 2894  Vcvv 3168  csb 3494  cun 3533  cin 3534  wss 3535  c0 3869  ifcif 4031  {csn 4120  {cpr 4122   class class class wbr 4573  cmpt 4633   × cxp 5022  ccnv 5023  ran crn 5025  cima 5027  Fun wfun 5780   Fn wfn 5781  wf 5782  1-1wf1 5783  ontowfo 5784  1-1-ontowf1o 5785  cfv 5786  (class class class)co 6523  𝑓 cof 6766  cc 9786  cr 9787  0cc0 9788  1c1 9789   + caddc 9791   < clt 9926  cmin 10113  cn 10863  cz 11206  cuz 11515  ...cfz 12148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-rep 4689  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824  ax-un 6820  ax-cnex 9844  ax-resscn 9845  ax-1cn 9846  ax-icn 9847  ax-addcl 9848  ax-addrcl 9849  ax-mulcl 9850  ax-mulrcl 9851  ax-mulcom 9852  ax-addass 9853  ax-mulass 9854  ax-distr 9855  ax-i2m1 9856  ax-1ne0 9857  ax-1rid 9858  ax-rnegex 9859  ax-rrecex 9860  ax-cnre 9861  ax-pre-lttri 9862  ax-pre-lttrn 9863  ax-pre-ltadd 9864  ax-pre-mulgt0 9865
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-nel 2778  df-ral 2896  df-rex 2897  df-reu 2898  df-rmo 2899  df-rab 2900  df-v 3170  df-sbc 3398  df-csb 3495  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-pss 3551  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-tp 4125  df-op 4127  df-uni 4363  df-iun 4447  df-br 4574  df-opab 4634  df-mpt 4635  df-tr 4671  df-eprel 4935  df-id 4939  df-po 4945  df-so 4946  df-fr 4983  df-we 4985  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-pred 5579  df-ord 5625  df-on 5626  df-lim 5627  df-suc 5628  df-iota 5750  df-fun 5788  df-fn 5789  df-f 5790  df-f1 5791  df-fo 5792  df-f1o 5793  df-fv 5794  df-riota 6485  df-ov 6526  df-oprab 6527  df-mpt2 6528  df-of 6768  df-om 6931  df-1st 7032  df-2nd 7033  df-wrecs 7267  df-recs 7328  df-rdg 7366  df-er 7602  df-en 7815  df-dom 7816  df-sdom 7817  df-pnf 9928  df-mnf 9929  df-xr 9930  df-ltxr 9931  df-le 9932  df-sub 10115  df-neg 10116  df-nn 10864  df-n0 11136  df-z 11207  df-uz 11516  df-fz 12149
This theorem is referenced by:  poimirlem8  32386  poimirlem18  32396  poimirlem21  32399  poimirlem22  32400
  Copyright terms: Public domain W3C validator