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

Theorem poimirlem2 33082
Description: Lemma for poimir 33113- consecutive vertices differ in at most one dimension. (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...𝑁))
poimirlem2.4 (𝜑𝑉 ∈ (1...(𝑁 − 1)))
poimirlem2.5 (𝜑𝑀 ∈ ((0...𝑁) ∖ {𝑉}))
Assertion
Ref Expression
poimirlem2 (𝜑 → ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛))
Distinct variable groups:   𝑗,𝑛,𝑦,𝜑   𝑗,𝐹,𝑛,𝑦   𝑗,𝑀,𝑛,𝑦   𝑗,𝑁,𝑛,𝑦   𝑇,𝑗,𝑛,𝑦   𝑈,𝑗,𝑛,𝑦   𝑗,𝑉,𝑛,𝑦

Proof of Theorem poimirlem2
Dummy variable 𝑚 is distinct from all other variables.
StepHypRef Expression
1 poimirlem2.3 . . . . . . . . . . . . . . . 16 (𝜑𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
2 dff1o3 6110 . . . . . . . . . . . . . . . . 17 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun 𝑈))
32simprbi 480 . . . . . . . . . . . . . . . 16 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun 𝑈)
41, 3syl 17 . . . . . . . . . . . . . . 15 (𝜑 → Fun 𝑈)
5 imadif 5941 . . . . . . . . . . . . . . 15 (Fun 𝑈 → (𝑈 “ ((1...𝑁) ∖ {(𝑉 + 1)})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})))
64, 5syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑈 “ ((1...𝑁) ∖ {(𝑉 + 1)})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})))
7 poimirlem2.4 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑉 ∈ (1...(𝑁 − 1)))
8 fzp1elp1 12352 . . . . . . . . . . . . . . . . . . . 20 (𝑉 ∈ (1...(𝑁 − 1)) → (𝑉 + 1) ∈ (1...((𝑁 − 1) + 1)))
97, 8syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑉 + 1) ∈ (1...((𝑁 − 1) + 1)))
10 poimir.0 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑁 ∈ ℕ)
1110nncnd 10996 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑁 ∈ ℂ)
12 npcan1 10415 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
1311, 12syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
1413oveq2d 6631 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁))
159, 14eleqtrd 2700 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑉 + 1) ∈ (1...𝑁))
16 fzsplit 12325 . . . . . . . . . . . . . . . . . 18 ((𝑉 + 1) ∈ (1...𝑁) → (1...𝑁) = ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)))
1715, 16syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (1...𝑁) = ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)))
1817difeq1d 3711 . . . . . . . . . . . . . . . 16 (𝜑 → ((1...𝑁) ∖ {(𝑉 + 1)}) = (((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)) ∖ {(𝑉 + 1)}))
19 difundir 3862 . . . . . . . . . . . . . . . . 17 (((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)) ∖ {(𝑉 + 1)}) = (((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) ∪ ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)}))
20 elfzuz 12296 . . . . . . . . . . . . . . . . . . . . . 22 (𝑉 ∈ (1...(𝑁 − 1)) → 𝑉 ∈ (ℤ‘1))
217, 20syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑉 ∈ (ℤ‘1))
22 fzsuc 12346 . . . . . . . . . . . . . . . . . . . . 21 (𝑉 ∈ (ℤ‘1) → (1...(𝑉 + 1)) = ((1...𝑉) ∪ {(𝑉 + 1)}))
2321, 22syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1...(𝑉 + 1)) = ((1...𝑉) ∪ {(𝑉 + 1)}))
2423difeq1d 3711 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) = (((1...𝑉) ∪ {(𝑉 + 1)}) ∖ {(𝑉 + 1)}))
25 difun2 4026 . . . . . . . . . . . . . . . . . . . 20 (((1...𝑉) ∪ {(𝑉 + 1)}) ∖ {(𝑉 + 1)}) = ((1...𝑉) ∖ {(𝑉 + 1)})
26 elfzelz 12300 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑉 ∈ (1...(𝑁 − 1)) → 𝑉 ∈ ℤ)
277, 26syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑉 ∈ ℤ)
2827zred 11442 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑉 ∈ ℝ)
2928ltp1d 10914 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑉 < (𝑉 + 1))
3027peano2zd 11445 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑉 + 1) ∈ ℤ)
3130zred 11442 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑉 + 1) ∈ ℝ)
3228, 31ltnled 10144 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑉 < (𝑉 + 1) ↔ ¬ (𝑉 + 1) ≤ 𝑉))
3329, 32mpbid 222 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ¬ (𝑉 + 1) ≤ 𝑉)
34 elfzle2 12303 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑉 + 1) ∈ (1...𝑉) → (𝑉 + 1) ≤ 𝑉)
3533, 34nsyl 135 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ¬ (𝑉 + 1) ∈ (1...𝑉))
36 difsn 4304 . . . . . . . . . . . . . . . . . . . . 21 (¬ (𝑉 + 1) ∈ (1...𝑉) → ((1...𝑉) ∖ {(𝑉 + 1)}) = (1...𝑉))
3735, 36syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((1...𝑉) ∖ {(𝑉 + 1)}) = (1...𝑉))
3825, 37syl5eq 2667 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((1...𝑉) ∪ {(𝑉 + 1)}) ∖ {(𝑉 + 1)}) = (1...𝑉))
3924, 38eqtrd 2655 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) = (1...𝑉))
4031ltp1d 10914 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑉 + 1) < ((𝑉 + 1) + 1))
41 peano2re 10169 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑉 + 1) ∈ ℝ → ((𝑉 + 1) + 1) ∈ ℝ)
4231, 41syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑉 + 1) + 1) ∈ ℝ)
4331, 42ltnled 10144 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑉 + 1) < ((𝑉 + 1) + 1) ↔ ¬ ((𝑉 + 1) + 1) ≤ (𝑉 + 1)))
4440, 43mpbid 222 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ¬ ((𝑉 + 1) + 1) ≤ (𝑉 + 1))
45 elfzle1 12302 . . . . . . . . . . . . . . . . . . . 20 ((𝑉 + 1) ∈ (((𝑉 + 1) + 1)...𝑁) → ((𝑉 + 1) + 1) ≤ (𝑉 + 1))
4644, 45nsyl 135 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ¬ (𝑉 + 1) ∈ (((𝑉 + 1) + 1)...𝑁))
47 difsn 4304 . . . . . . . . . . . . . . . . . . 19 (¬ (𝑉 + 1) ∈ (((𝑉 + 1) + 1)...𝑁) → ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)}) = (((𝑉 + 1) + 1)...𝑁))
4846, 47syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)}) = (((𝑉 + 1) + 1)...𝑁))
4939, 48uneq12d 3752 . . . . . . . . . . . . . . . . 17 (𝜑 → (((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) ∪ ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)})) = ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁)))
5019, 49syl5eq 2667 . . . . . . . . . . . . . . . 16 (𝜑 → (((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)) ∖ {(𝑉 + 1)}) = ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁)))
5118, 50eqtrd 2655 . . . . . . . . . . . . . . 15 (𝜑 → ((1...𝑁) ∖ {(𝑉 + 1)}) = ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁)))
5251imaeq2d 5435 . . . . . . . . . . . . . 14 (𝜑 → (𝑈 “ ((1...𝑁) ∖ {(𝑉 + 1)})) = (𝑈 “ ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁))))
536, 52eqtr3d 2657 . . . . . . . . . . . . 13 (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) = (𝑈 “ ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁))))
54 imaundi 5514 . . . . . . . . . . . . 13 (𝑈 “ ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))
5553, 54syl6eq 2671 . . . . . . . . . . . 12 (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) = ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))
5655eleq2d 2684 . . . . . . . . . . 11 (𝜑 → (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) ↔ 𝑛 ∈ ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))))
57 eldif 3570 . . . . . . . . . . 11 (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})))
58 elun 3737 . . . . . . . . . . 11 (𝑛 ∈ ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ↔ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))
5956, 57, 583bitr3g 302 . . . . . . . . . 10 (𝜑 → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))))
6059adantr 481 . . . . . . . . 9 ((𝜑𝑀 < 𝑉) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))))
61 imassrn 5446 . . . . . . . . . . . . . . . 16 (𝑈 “ (1...𝑉)) ⊆ ran 𝑈
62 f1of 6104 . . . . . . . . . . . . . . . . . 18 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)⟶(1...𝑁))
631, 62syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝑈:(1...𝑁)⟶(1...𝑁))
64 frn 6020 . . . . . . . . . . . . . . . . 17 (𝑈:(1...𝑁)⟶(1...𝑁) → ran 𝑈 ⊆ (1...𝑁))
6563, 64syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ran 𝑈 ⊆ (1...𝑁))
6661, 65syl5ss 3599 . . . . . . . . . . . . . . 15 (𝜑 → (𝑈 “ (1...𝑉)) ⊆ (1...𝑁))
6766sselda 3588 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (𝑈 “ (1...𝑉))) → 𝑛 ∈ (1...𝑁))
68 poimirlem2.2 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇:(1...𝑁)⟶ℤ)
69 ffn 6012 . . . . . . . . . . . . . . . . . 18 (𝑇:(1...𝑁)⟶ℤ → 𝑇 Fn (1...𝑁))
7068, 69syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝑇 Fn (1...𝑁))
7170adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (𝑈 “ (1...𝑉))) → 𝑇 Fn (1...𝑁))
72 1ex 9995 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ V
73 fnconstg 6060 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ V → ((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)))
7472, 73ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉))
75 c0ex 9994 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ V
76 fnconstg 6060 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ V → ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁)))
7775, 76ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁))
7874, 77pm3.2i 471 . . . . . . . . . . . . . . . . . . 19 (((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁)))
79 imain 5942 . . . . . . . . . . . . . . . . . . . . 21 (Fun 𝑈 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))))
804, 79syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))))
81 fzdisj 12326 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑉 < (𝑉 + 1) → ((1...𝑉) ∩ ((𝑉 + 1)...𝑁)) = ∅)
8229, 81syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...𝑉) ∩ ((𝑉 + 1)...𝑁)) = ∅)
8382imaeq2d 5435 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = (𝑈 “ ∅))
84 ima0 5450 . . . . . . . . . . . . . . . . . . . . 21 (𝑈 “ ∅) = ∅
8583, 84syl6eq 2671 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = ∅)
8680, 85eqtr3d 2657 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅)
87 fnun 5965 . . . . . . . . . . . . . . . . . . 19 (((((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))))
8878, 86, 87sylancr 694 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))))
89 imaundi 5514 . . . . . . . . . . . . . . . . . . . 20 (𝑈 “ ((1...𝑉) ∪ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁)))
9010nnzd 11441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑁 ∈ ℤ)
91 peano2zm 11380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
9290, 91syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑁 − 1) ∈ ℤ)
93 uzid 11662 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
9492, 93syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
95 peano2uz 11701 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
9694, 95syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
9713, 96eqeltrrd 2699 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
98 fzss2 12339 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
9997, 98syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
10099, 7sseldd 3589 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑉 ∈ (1...𝑁))
101 fzsplit 12325 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑉 ∈ (1...𝑁) → (1...𝑁) = ((1...𝑉) ∪ ((𝑉 + 1)...𝑁)))
102100, 101syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (1...𝑁) = ((1...𝑉) ∪ ((𝑉 + 1)...𝑁)))
103102imaeq2d 5435 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...𝑉) ∪ ((𝑉 + 1)...𝑁))))
104 f1ofo 6111 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁))
1051, 104syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑈:(1...𝑁)–onto→(1...𝑁))
106 foima 6087 . . . . . . . . . . . . . . . . . . . . . 22 (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁))
107105, 106syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁))
108103, 107eqtr3d 2657 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...𝑉) ∪ ((𝑉 + 1)...𝑁))) = (1...𝑁))
10989, 108syl5eqr 2669 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))) = (1...𝑁))
110109fneq2d 5950 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))) ↔ (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁)))
11188, 110mpbid 222 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁))
112111adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (𝑈 “ (1...𝑉))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁))
113 fzfid 12728 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (𝑈 “ (1...𝑉))) → (1...𝑁) ∈ Fin)
114 inidm 3806 . . . . . . . . . . . . . . . 16 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
115 eqidd 2622 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇𝑛) = (𝑇𝑛))
116 fvun1 6236 . . . . . . . . . . . . . . . . . . . 20 ((((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁)) ∧ (((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...𝑉)))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...𝑉)) × {1})‘𝑛))
11774, 77, 116mp3an12 1411 . . . . . . . . . . . . . . . . . . 19 ((((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...𝑉)) × {1})‘𝑛))
11886, 117sylan 488 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...𝑉)) × {1})‘𝑛))
11972fvconst2 6434 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (𝑈 “ (1...𝑉)) → (((𝑈 “ (1...𝑉)) × {1})‘𝑛) = 1)
120119adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ (𝑈 “ (1...𝑉))) → (((𝑈 “ (1...𝑉)) × {1})‘𝑛) = 1)
121118, 120eqtrd 2655 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1)
122121adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1)
12371, 112, 113, 113, 114, 115, 122ofval 6871 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇𝑛) + 1))
124 fnconstg 6060 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ V → ((𝑈 “ (1...(𝑉 + 1))) × {1}) Fn (𝑈 “ (1...(𝑉 + 1))))
12572, 124ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 “ (1...(𝑉 + 1))) × {1}) Fn (𝑈 “ (1...(𝑉 + 1)))
126 fnconstg 6060 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ V → ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))
12775, 126ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁))
128125, 127pm3.2i 471 . . . . . . . . . . . . . . . . . . 19 (((𝑈 “ (1...(𝑉 + 1))) × {1}) Fn (𝑈 “ (1...(𝑉 + 1))) ∧ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))
129 imain 5942 . . . . . . . . . . . . . . . . . . . . 21 (Fun 𝑈 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))
1304, 129syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))
131 fzdisj 12326 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑉 + 1) < ((𝑉 + 1) + 1) → ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁)) = ∅)
13240, 131syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁)) = ∅)
133132imaeq2d 5435 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = (𝑈 “ ∅))
134133, 84syl6eq 2671 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = ∅)
135130, 134eqtr3d 2657 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅)
136 fnun 5965 . . . . . . . . . . . . . . . . . . 19 (((((𝑈 “ (1...(𝑉 + 1))) × {1}) Fn (𝑈 “ (1...(𝑉 + 1))) ∧ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ ((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅) → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))
137128, 135, 136sylancr 694 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))
138 imaundi 5514 . . . . . . . . . . . . . . . . . . . 20 (𝑈 “ ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))
13917imaeq2d 5435 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁))))
140139, 107eqtr3d 2657 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁))) = (1...𝑁))
141138, 140syl5eqr 2669 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = (1...𝑁))
142141fneq2d 5950 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ↔ (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁)))
143137, 142mpbid 222 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))
144143adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (𝑈 “ (1...𝑉))) → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))
145 uzid 11662 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑉 ∈ ℤ → 𝑉 ∈ (ℤ𝑉))
14627, 145syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑉 ∈ (ℤ𝑉))
147 peano2uz 11701 . . . . . . . . . . . . . . . . . . . . . 22 (𝑉 ∈ (ℤ𝑉) → (𝑉 + 1) ∈ (ℤ𝑉))
148146, 147syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑉 + 1) ∈ (ℤ𝑉))
149 fzss2 12339 . . . . . . . . . . . . . . . . . . . . 21 ((𝑉 + 1) ∈ (ℤ𝑉) → (1...𝑉) ⊆ (1...(𝑉 + 1)))
150148, 149syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1...𝑉) ⊆ (1...(𝑉 + 1)))
151 imass2 5470 . . . . . . . . . . . . . . . . . . . 20 ((1...𝑉) ⊆ (1...(𝑉 + 1)) → (𝑈 “ (1...𝑉)) ⊆ (𝑈 “ (1...(𝑉 + 1))))
152150, 151syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑈 “ (1...𝑉)) ⊆ (𝑈 “ (1...(𝑉 + 1))))
153152sselda 3588 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ (𝑈 “ (1...𝑉))) → 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1))))
154 fvun1 6236 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑈 “ (1...(𝑉 + 1))) × {1}) Fn (𝑈 “ (1...(𝑉 + 1))) ∧ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ∧ (((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1))))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛))
155125, 127, 154mp3an12 1411 . . . . . . . . . . . . . . . . . . . 20 ((((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛))
156135, 155sylan 488 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛))
15772fvconst2 6434 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (𝑈 “ (1...(𝑉 + 1))) → (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛) = 1)
158157adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛) = 1)
159156, 158eqtrd 2655 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1)
160153, 159syldan 487 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1)
161160adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1)
16271, 144, 113, 113, 114, 115, 161ofval 6871 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇𝑛) + 1))
163123, 162eqtr4d 2658 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
16467, 163mpdan 701 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (𝑈 “ (1...𝑉))) → ((𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
165 imassrn 5446 . . . . . . . . . . . . . . . 16 (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ ran 𝑈
166165, 65syl5ss 3599 . . . . . . . . . . . . . . 15 (𝜑 → (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ (1...𝑁))
167166sselda 3588 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → 𝑛 ∈ (1...𝑁))
16870adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → 𝑇 Fn (1...𝑁))
169111adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁))
170 fzfid 12728 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (1...𝑁) ∈ Fin)
171 eqidd 2622 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇𝑛) = (𝑇𝑛))
172 uzid 11662 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑉 + 1) ∈ ℤ → (𝑉 + 1) ∈ (ℤ‘(𝑉 + 1)))
17330, 172syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑉 + 1) ∈ (ℤ‘(𝑉 + 1)))
174 peano2uz 11701 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑉 + 1) ∈ (ℤ‘(𝑉 + 1)) → ((𝑉 + 1) + 1) ∈ (ℤ‘(𝑉 + 1)))
175173, 174syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑉 + 1) + 1) ∈ (ℤ‘(𝑉 + 1)))
176 fzss1 12338 . . . . . . . . . . . . . . . . . . . . 21 (((𝑉 + 1) + 1) ∈ (ℤ‘(𝑉 + 1)) → (((𝑉 + 1) + 1)...𝑁) ⊆ ((𝑉 + 1)...𝑁))
177175, 176syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝑉 + 1) + 1)...𝑁) ⊆ ((𝑉 + 1)...𝑁))
178 imass2 5470 . . . . . . . . . . . . . . . . . . . 20 ((((𝑉 + 1) + 1)...𝑁) ⊆ ((𝑉 + 1)...𝑁) → (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ (𝑈 “ ((𝑉 + 1)...𝑁)))
179177, 178syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ (𝑈 “ ((𝑉 + 1)...𝑁)))
180179sselda 3588 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))
181 fvun2 6237 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁)) ∧ (((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛))
18274, 77, 181mp3an12 1411 . . . . . . . . . . . . . . . . . . . 20 ((((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛))
18386, 182sylan 488 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛))
18475fvconst2 6434 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)) → (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛) = 0)
185184adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛) = 0)
186183, 185eqtrd 2655 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0)
187180, 186syldan 487 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0)
188187adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0)
189168, 169, 170, 170, 114, 171, 188ofval 6871 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇𝑛) + 0))
190143adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))
191 fvun2 6237 . . . . . . . . . . . . . . . . . . . 20 ((((𝑈 “ (1...(𝑉 + 1))) × {1}) Fn (𝑈 “ (1...(𝑉 + 1))) ∧ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ∧ (((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛))
192125, 127, 191mp3an12 1411 . . . . . . . . . . . . . . . . . . 19 ((((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛))
193135, 192sylan 488 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛))
19475fvconst2 6434 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) → (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛) = 0)
195194adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛) = 0)
196193, 195eqtrd 2655 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 0)
197196adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 0)
198168, 190, 170, 170, 114, 171, 197ofval 6871 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇𝑛) + 0))
199189, 198eqtr4d 2658 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
200167, 199mpdan 701 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
201164, 200jaodan 825 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
202201adantlr 750 . . . . . . . . . . 11 (((𝜑𝑀 < 𝑉) ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
203 poimirlem2.1 . . . . . . . . . . . . . . 15 (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))
204203adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑀 < 𝑉) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))
205 vex 3193 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
206 ovex 6643 . . . . . . . . . . . . . . . . 17 (𝑦 + 1) ∈ V
207205, 206ifex 4134 . . . . . . . . . . . . . . . 16 if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V
208207a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
209 breq1 4626 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑉 − 1) → (𝑦 < 𝑀 ↔ (𝑉 − 1) < 𝑀))
210209adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 = (𝑉 − 1)) → (𝑦 < 𝑀 ↔ (𝑉 − 1) < 𝑀))
211 simpr 477 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 = (𝑉 − 1)) → 𝑦 = (𝑉 − 1))
212 oveq1 6622 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑉 − 1) → (𝑦 + 1) = ((𝑉 − 1) + 1))
21327zcnd 11443 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑉 ∈ ℂ)
214 npcan1 10415 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑉 ∈ ℂ → ((𝑉 − 1) + 1) = 𝑉)
215213, 214syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑉 − 1) + 1) = 𝑉)
216212, 215sylan9eqr 2677 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 = (𝑉 − 1)) → (𝑦 + 1) = 𝑉)
217210, 211, 216ifbieq12d 4091 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉))
218217adantlr 750 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉))
219 poimirlem2.5 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑀 ∈ ((0...𝑁) ∖ {𝑉}))
220219eldifad 3572 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑀 ∈ (0...𝑁))
221 elfzelz 12300 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ (0...𝑁) → 𝑀 ∈ ℤ)
222220, 221syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑀 ∈ ℤ)
223 zltlem1 11390 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀 ∈ ℤ ∧ 𝑉 ∈ ℤ) → (𝑀 < 𝑉𝑀 ≤ (𝑉 − 1)))
224222, 27, 223syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑀 < 𝑉𝑀 ≤ (𝑉 − 1)))
225222zred 11442 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑀 ∈ ℝ)
226 peano2zm 11380 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑉 ∈ ℤ → (𝑉 − 1) ∈ ℤ)
22727, 226syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑉 − 1) ∈ ℤ)
228227zred 11442 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑉 − 1) ∈ ℝ)
229225, 228lenltd 10143 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑀 ≤ (𝑉 − 1) ↔ ¬ (𝑉 − 1) < 𝑀))
230224, 229bitrd 268 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑀 < 𝑉 ↔ ¬ (𝑉 − 1) < 𝑀))
231230biimpa 501 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑀 < 𝑉) → ¬ (𝑉 − 1) < 𝑀)
232231iffalsed 4075 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑀 < 𝑉) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = 𝑉)
233232adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = 𝑉)
234218, 233eqtrd 2655 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = 𝑉)
235234eqeq2d 2631 . . . . . . . . . . . . . . . . 17 (((𝜑𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → (𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ↔ 𝑗 = 𝑉))
236235biimpa 501 . . . . . . . . . . . . . . . 16 ((((𝜑𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → 𝑗 = 𝑉)
237 oveq2 6623 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑉 → (1...𝑗) = (1...𝑉))
238237imaeq2d 5435 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑉 → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...𝑉)))
239238xpeq1d 5108 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑉 → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...𝑉)) × {1}))
240 oveq1 6622 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑉 → (𝑗 + 1) = (𝑉 + 1))
241240oveq1d 6630 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑉 → ((𝑗 + 1)...𝑁) = ((𝑉 + 1)...𝑁))
242241imaeq2d 5435 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑉 → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ ((𝑉 + 1)...𝑁)))
243242xpeq1d 5108 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑉 → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))
244239, 243uneq12d 3752 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑉 → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))
245244oveq2d 6631 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑉 → (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
246236, 245syl 17 . . . . . . . . . . . . . . 15 ((((𝜑𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
247208, 246csbied 3546 . . . . . . . . . . . . . 14 (((𝜑𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
248 elfzm1b 12375 . . . . . . . . . . . . . . . . 17 ((𝑉 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑉 ∈ (1...𝑁) ↔ (𝑉 − 1) ∈ (0...(𝑁 − 1))))
24927, 90, 248syl2anc 692 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑉 ∈ (1...𝑁) ↔ (𝑉 − 1) ∈ (0...(𝑁 − 1))))
250100, 249mpbid 222 . . . . . . . . . . . . . . 15 (𝜑 → (𝑉 − 1) ∈ (0...(𝑁 − 1)))
251250adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑀 < 𝑉) → (𝑉 − 1) ∈ (0...(𝑁 − 1)))
252 ovexd 6645 . . . . . . . . . . . . . 14 ((𝜑𝑀 < 𝑉) → (𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))) ∈ V)
253204, 247, 251, 252fvmptd 6255 . . . . . . . . . . . . 13 ((𝜑𝑀 < 𝑉) → (𝐹‘(𝑉 − 1)) = (𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
254253fveq1d 6160 . . . . . . . . . . . 12 ((𝜑𝑀 < 𝑉) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
255254adantr 481 . . . . . . . . . . 11 (((𝜑𝑀 < 𝑉) ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
256207a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
257 breq1 4626 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑉 → (𝑦 < 𝑀𝑉 < 𝑀))
258 id 22 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑉𝑦 = 𝑉)
259 oveq1 6622 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑉 → (𝑦 + 1) = (𝑉 + 1))
260257, 258, 259ifbieq12d 4091 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑉 → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if(𝑉 < 𝑀, 𝑉, (𝑉 + 1)))
261 ltnsym 10095 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑀 < 𝑉 → ¬ 𝑉 < 𝑀))
262225, 28, 261syl2anc 692 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑀 < 𝑉 → ¬ 𝑉 < 𝑀))
263262imp 445 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑀 < 𝑉) → ¬ 𝑉 < 𝑀)
264263iffalsed 4075 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑀 < 𝑉) → if(𝑉 < 𝑀, 𝑉, (𝑉 + 1)) = (𝑉 + 1))
265260, 264sylan9eqr 2677 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑉 + 1))
266265eqeq2d 2631 . . . . . . . . . . . . . . . . 17 (((𝜑𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → (𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ↔ 𝑗 = (𝑉 + 1)))
267266biimpa 501 . . . . . . . . . . . . . . . 16 ((((𝜑𝑀 < 𝑉) ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → 𝑗 = (𝑉 + 1))
268 oveq2 6623 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = (𝑉 + 1) → (1...𝑗) = (1...(𝑉 + 1)))
269268imaeq2d 5435 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑉 + 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑉 + 1))))
270269xpeq1d 5108 . . . . . . . . . . . . . . . . . 18 (𝑗 = (𝑉 + 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑉 + 1))) × {1}))
271 oveq1 6622 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = (𝑉 + 1) → (𝑗 + 1) = ((𝑉 + 1) + 1))
272271oveq1d 6630 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = (𝑉 + 1) → ((𝑗 + 1)...𝑁) = (((𝑉 + 1) + 1)...𝑁))
273272imaeq2d 5435 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑉 + 1) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))
274273xpeq1d 5108 . . . . . . . . . . . . . . . . . 18 (𝑗 = (𝑉 + 1) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))
275270, 274uneq12d 3752 . . . . . . . . . . . . . . . . 17 (𝑗 = (𝑉 + 1) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))
276275oveq2d 6631 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑉 + 1) → (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))))
277267, 276syl 17 . . . . . . . . . . . . . . 15 ((((𝜑𝑀 < 𝑉) ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))))
278256, 277csbied 3546 . . . . . . . . . . . . . 14 (((𝜑𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))))
279 1eluzge0 11692 . . . . . . . . . . . . . . . . 17 1 ∈ (ℤ‘0)
280 fzss1 12338 . . . . . . . . . . . . . . . . 17 (1 ∈ (ℤ‘0) → (1...(𝑁 − 1)) ⊆ (0...(𝑁 − 1)))
281279, 280ax-mp 5 . . . . . . . . . . . . . . . 16 (1...(𝑁 − 1)) ⊆ (0...(𝑁 − 1))
282281, 7sseldi 3586 . . . . . . . . . . . . . . 15 (𝜑𝑉 ∈ (0...(𝑁 − 1)))
283282adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑀 < 𝑉) → 𝑉 ∈ (0...(𝑁 − 1)))
284 ovexd 6645 . . . . . . . . . . . . . 14 ((𝜑𝑀 < 𝑉) → (𝑇𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))) ∈ V)
285204, 278, 283, 284fvmptd 6255 . . . . . . . . . . . . 13 ((𝜑𝑀 < 𝑉) → (𝐹𝑉) = (𝑇𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))))
286285fveq1d 6160 . . . . . . . . . . . 12 ((𝜑𝑀 < 𝑉) → ((𝐹𝑉)‘𝑛) = ((𝑇𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
287286adantr 481 . . . . . . . . . . 11 (((𝜑𝑀 < 𝑉) ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝐹𝑉)‘𝑛) = ((𝑇𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
288202, 255, 2873eqtr4d 2665 . . . . . . . . . 10 (((𝜑𝑀 < 𝑉) ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹𝑉)‘𝑛))
289288ex 450 . . . . . . . . 9 ((𝜑𝑀 < 𝑉) → ((𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹𝑉)‘𝑛)))
29060, 289sylbid 230 . . . . . . . 8 ((𝜑𝑀 < 𝑉) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹𝑉)‘𝑛)))
291290expdimp 453 . . . . . . 7 (((𝜑𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹𝑉)‘𝑛)))
292291necon1ad 2807 . . . . . 6 (((𝜑𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛) → 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})))
293 elimasni 5461 . . . . . . . 8 (𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → (𝑉 + 1)𝑈𝑛)
294 eqcom 2628 . . . . . . . . 9 (𝑛 = (𝑈‘(𝑉 + 1)) ↔ (𝑈‘(𝑉 + 1)) = 𝑛)
295 f1ofn 6105 . . . . . . . . . . 11 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 Fn (1...𝑁))
2961, 295syl 17 . . . . . . . . . 10 (𝜑𝑈 Fn (1...𝑁))
297 fnbrfvb 6203 . . . . . . . . . 10 ((𝑈 Fn (1...𝑁) ∧ (𝑉 + 1) ∈ (1...𝑁)) → ((𝑈‘(𝑉 + 1)) = 𝑛 ↔ (𝑉 + 1)𝑈𝑛))
298296, 15, 297syl2anc 692 . . . . . . . . 9 (𝜑 → ((𝑈‘(𝑉 + 1)) = 𝑛 ↔ (𝑉 + 1)𝑈𝑛))
299294, 298syl5bb 272 . . . . . . . 8 (𝜑 → (𝑛 = (𝑈‘(𝑉 + 1)) ↔ (𝑉 + 1)𝑈𝑛))
300293, 299syl5ibr 236 . . . . . . 7 (𝜑 → (𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → 𝑛 = (𝑈‘(𝑉 + 1))))
301300ad2antrr 761 . . . . . 6 (((𝜑𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → 𝑛 = (𝑈‘(𝑉 + 1))))
302292, 301syld 47 . . . . 5 (((𝜑𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1))))
303302ralrimiva 2962 . . . 4 ((𝜑𝑀 < 𝑉) → ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1))))
304 fvex 6168 . . . . 5 (𝑈‘(𝑉 + 1)) ∈ V
305 eqeq2 2632 . . . . . . 7 (𝑚 = (𝑈‘(𝑉 + 1)) → (𝑛 = 𝑚𝑛 = (𝑈‘(𝑉 + 1))))
306305imbi2d 330 . . . . . 6 (𝑚 = (𝑈‘(𝑉 + 1)) → ((((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1)))))
307306ralbidv 2982 . . . . 5 (𝑚 = (𝑈‘(𝑉 + 1)) → (∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1)))))
308304, 307spcev 3290 . . . 4 (∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1))) → ∃𝑚𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛) → 𝑛 = 𝑚))
309303, 308syl 17 . . 3 ((𝜑𝑀 < 𝑉) → ∃𝑚𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛) → 𝑛 = 𝑚))
310 imadif 5941 . . . . . . . . . . . . . . 15 (Fun 𝑈 → (𝑈 “ ((1...𝑁) ∖ {𝑉})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})))
3114, 310syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑉})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})))
312102difeq1d 3711 . . . . . . . . . . . . . . . 16 (𝜑 → ((1...𝑁) ∖ {𝑉}) = (((1...𝑉) ∪ ((𝑉 + 1)...𝑁)) ∖ {𝑉}))
313 difundir 3862 . . . . . . . . . . . . . . . . 17 (((1...𝑉) ∪ ((𝑉 + 1)...𝑁)) ∖ {𝑉}) = (((1...𝑉) ∖ {𝑉}) ∪ (((𝑉 + 1)...𝑁) ∖ {𝑉}))
314215, 21eqeltrd 2698 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑉 − 1) + 1) ∈ (ℤ‘1))
315 uzid 11662 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑉 − 1) ∈ ℤ → (𝑉 − 1) ∈ (ℤ‘(𝑉 − 1)))
316227, 315syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑉 − 1) ∈ (ℤ‘(𝑉 − 1)))
317 peano2uz 11701 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑉 − 1) ∈ (ℤ‘(𝑉 − 1)) → ((𝑉 − 1) + 1) ∈ (ℤ‘(𝑉 − 1)))
318316, 317syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑉 − 1) + 1) ∈ (ℤ‘(𝑉 − 1)))
319215, 318eqeltrrd 2699 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑉 ∈ (ℤ‘(𝑉 − 1)))
320 fzsplit2 12324 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑉 − 1) + 1) ∈ (ℤ‘1) ∧ 𝑉 ∈ (ℤ‘(𝑉 − 1))) → (1...𝑉) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑉)))
321314, 319, 320syl2anc 692 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (1...𝑉) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑉)))
322215oveq1d 6630 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((𝑉 − 1) + 1)...𝑉) = (𝑉...𝑉))
323 fzsn 12341 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑉 ∈ ℤ → (𝑉...𝑉) = {𝑉})
32427, 323syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑉...𝑉) = {𝑉})
325322, 324eqtrd 2655 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝑉 − 1) + 1)...𝑉) = {𝑉})
326325uneq2d 3751 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑉)) = ((1...(𝑉 − 1)) ∪ {𝑉}))
327321, 326eqtrd 2655 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1...𝑉) = ((1...(𝑉 − 1)) ∪ {𝑉}))
328327difeq1d 3711 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((1...𝑉) ∖ {𝑉}) = (((1...(𝑉 − 1)) ∪ {𝑉}) ∖ {𝑉}))
329 difun2 4026 . . . . . . . . . . . . . . . . . . . 20 (((1...(𝑉 − 1)) ∪ {𝑉}) ∖ {𝑉}) = ((1...(𝑉 − 1)) ∖ {𝑉})
33028ltm1d 10916 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑉 − 1) < 𝑉)
331228, 28ltnled 10144 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑉 − 1) < 𝑉 ↔ ¬ 𝑉 ≤ (𝑉 − 1)))
332330, 331mpbid 222 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ¬ 𝑉 ≤ (𝑉 − 1))
333 elfzle2 12303 . . . . . . . . . . . . . . . . . . . . . 22 (𝑉 ∈ (1...(𝑉 − 1)) → 𝑉 ≤ (𝑉 − 1))
334332, 333nsyl 135 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ¬ 𝑉 ∈ (1...(𝑉 − 1)))
335 difsn 4304 . . . . . . . . . . . . . . . . . . . . 21 𝑉 ∈ (1...(𝑉 − 1)) → ((1...(𝑉 − 1)) ∖ {𝑉}) = (1...(𝑉 − 1)))
336334, 335syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((1...(𝑉 − 1)) ∖ {𝑉}) = (1...(𝑉 − 1)))
337329, 336syl5eq 2667 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((1...(𝑉 − 1)) ∪ {𝑉}) ∖ {𝑉}) = (1...(𝑉 − 1)))
338328, 337eqtrd 2655 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((1...𝑉) ∖ {𝑉}) = (1...(𝑉 − 1)))
339 elfzle1 12302 . . . . . . . . . . . . . . . . . . . 20 (𝑉 ∈ ((𝑉 + 1)...𝑁) → (𝑉 + 1) ≤ 𝑉)
34033, 339nsyl 135 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ¬ 𝑉 ∈ ((𝑉 + 1)...𝑁))
341 difsn 4304 . . . . . . . . . . . . . . . . . . 19 𝑉 ∈ ((𝑉 + 1)...𝑁) → (((𝑉 + 1)...𝑁) ∖ {𝑉}) = ((𝑉 + 1)...𝑁))
342340, 341syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑉 + 1)...𝑁) ∖ {𝑉}) = ((𝑉 + 1)...𝑁))
343338, 342uneq12d 3752 . . . . . . . . . . . . . . . . 17 (𝜑 → (((1...𝑉) ∖ {𝑉}) ∪ (((𝑉 + 1)...𝑁) ∖ {𝑉})) = ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁)))
344313, 343syl5eq 2667 . . . . . . . . . . . . . . . 16 (𝜑 → (((1...𝑉) ∪ ((𝑉 + 1)...𝑁)) ∖ {𝑉}) = ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁)))
345312, 344eqtrd 2655 . . . . . . . . . . . . . . 15 (𝜑 → ((1...𝑁) ∖ {𝑉}) = ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁)))
346345imaeq2d 5435 . . . . . . . . . . . . . 14 (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑉})) = (𝑈 “ ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁))))
347311, 346eqtr3d 2657 . . . . . . . . . . . . 13 (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) = (𝑈 “ ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁))))
348 imaundi 5514 . . . . . . . . . . . . 13 (𝑈 “ ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁)))
349347, 348syl6eq 2671 . . . . . . . . . . . 12 (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) = ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))))
350349eleq2d 2684 . . . . . . . . . . 11 (𝜑 → (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) ↔ 𝑛 ∈ ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁)))))
351 eldif 3570 . . . . . . . . . . 11 (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉})))
352 elun 3737 . . . . . . . . . . 11 (𝑛 ∈ ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))) ↔ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))))
353350, 351, 3523bitr3g 302 . . . . . . . . . 10 (𝜑 → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉})) ↔ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))))
354353adantr 481 . . . . . . . . 9 ((𝜑𝑉 < 𝑀) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉})) ↔ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))))
355 imassrn 5446 . . . . . . . . . . . . . . . 16 (𝑈 “ (1...(𝑉 − 1))) ⊆ ran 𝑈
356355, 65syl5ss 3599 . . . . . . . . . . . . . . 15 (𝜑 → (𝑈 “ (1...(𝑉 − 1))) ⊆ (1...𝑁))
357356sselda 3588 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → 𝑛 ∈ (1...𝑁))
35870adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → 𝑇 Fn (1...𝑁))
359 fnconstg 6060 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ V → ((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))))
36072, 359ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1)))
361 fnconstg 6060 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ V → ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁)))
36275, 361ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁))
363360, 362pm3.2i 471 . . . . . . . . . . . . . . . . . . 19 (((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) ∧ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁)))
364 imain 5942 . . . . . . . . . . . . . . . . . . . . 21 (Fun 𝑈 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))))
3654, 364syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))))
366 fzdisj 12326 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑉 − 1) < 𝑉 → ((1...(𝑉 − 1)) ∩ (𝑉...𝑁)) = ∅)
367330, 366syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...(𝑉 − 1)) ∩ (𝑉...𝑁)) = ∅)
368367imaeq2d 5435 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = (𝑈 “ ∅))
369368, 84syl6eq 2671 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = ∅)
370365, 369eqtr3d 2657 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅)
371 fnun 5965 . . . . . . . . . . . . . . . . . . 19 (((((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) ∧ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁))) ∧ ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅) → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁))))
372363, 370, 371sylancr 694 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁))))
373 imaundi 5514 . . . . . . . . . . . . . . . . . . . 20 (𝑈 “ ((1...(𝑉 − 1)) ∪ (𝑉...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁)))
374 uzss 11668 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑉 ∈ (ℤ‘(𝑉 − 1)) → (ℤ𝑉) ⊆ (ℤ‘(𝑉 − 1)))
375319, 374syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (ℤ𝑉) ⊆ (ℤ‘(𝑉 − 1)))
376 elfzuz3 12297 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑉 ∈ (1...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ𝑉))
3777, 376syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑁 − 1) ∈ (ℤ𝑉))
378375, 377sseldd 3589 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑁 − 1) ∈ (ℤ‘(𝑉 − 1)))
379 peano2uz 11701 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑁 − 1) ∈ (ℤ‘(𝑉 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑉 − 1)))
380378, 379syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑉 − 1)))
38113, 380eqeltrrd 2699 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑁 ∈ (ℤ‘(𝑉 − 1)))
382 fzsplit2 12324 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑉 − 1) + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ‘(𝑉 − 1))) → (1...𝑁) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑁)))
383314, 381, 382syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1...𝑁) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑁)))
384215oveq1d 6630 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝑉 − 1) + 1)...𝑁) = (𝑉...𝑁))
385384uneq2d 3751 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑁)) = ((1...(𝑉 − 1)) ∪ (𝑉...𝑁)))
386383, 385eqtrd 2655 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (1...𝑁) = ((1...(𝑉 − 1)) ∪ (𝑉...𝑁)))
387386imaeq2d 5435 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑉 − 1)) ∪ (𝑉...𝑁))))
388387, 107eqtr3d 2657 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∪ (𝑉...𝑁))) = (1...𝑁))
389373, 388syl5eqr 2669 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁))) = (1...𝑁))
390389fneq2d 5950 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁))) ↔ (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁)))
391372, 390mpbid 222 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁))
392391adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁))
393 fzfid 12728 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (1...𝑁) ∈ Fin)
394 eqidd 2622 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇𝑛) = (𝑇𝑛))
395 fvun1 6236 . . . . . . . . . . . . . . . . . . . 20 ((((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) ∧ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁)) ∧ (((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛))
396360, 362, 395mp3an12 1411 . . . . . . . . . . . . . . . . . . 19 ((((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛))
397370, 396sylan 488 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛))
39872fvconst2 6434 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) → (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛) = 1)
399398adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛) = 1)
400397, 399eqtrd 2655 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 1)
401400adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 1)
402358, 392, 393, 393, 114, 394, 401ofval 6871 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇𝑛) + 1))
403111adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁))
404 fzss2 12339 . . . . . . . . . . . . . . . . . . . . 21 (𝑉 ∈ (ℤ‘(𝑉 − 1)) → (1...(𝑉 − 1)) ⊆ (1...𝑉))
405319, 404syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1...(𝑉 − 1)) ⊆ (1...𝑉))
406 imass2 5470 . . . . . . . . . . . . . . . . . . . 20 ((1...(𝑉 − 1)) ⊆ (1...𝑉) → (𝑈 “ (1...(𝑉 − 1))) ⊆ (𝑈 “ (1...𝑉)))
407405, 406syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑈 “ (1...(𝑉 − 1))) ⊆ (𝑈 “ (1...𝑉)))
408407sselda 3588 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → 𝑛 ∈ (𝑈 “ (1...𝑉)))
409408, 121syldan 487 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1)
410409adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1)
411358, 403, 393, 393, 114, 394, 410ofval 6871 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇𝑛) + 1))
412402, 411eqtr4d 2658 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
413357, 412mpdan 701 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((𝑇𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
414 imassrn 5446 . . . . . . . . . . . . . . . 16 (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ ran 𝑈
415414, 65syl5ss 3599 . . . . . . . . . . . . . . 15 (𝜑 → (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ (1...𝑁))
416415sselda 3588 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → 𝑛 ∈ (1...𝑁))
41770adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → 𝑇 Fn (1...𝑁))
418391adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁))
419 fzfid 12728 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (1...𝑁) ∈ Fin)
420 eqidd 2622 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇𝑛) = (𝑇𝑛))
421 fzss1 12338 . . . . . . . . . . . . . . . . . . . . 21 ((𝑉 + 1) ∈ (ℤ𝑉) → ((𝑉 + 1)...𝑁) ⊆ (𝑉...𝑁))
422148, 421syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑉 + 1)...𝑁) ⊆ (𝑉...𝑁))
423 imass2 5470 . . . . . . . . . . . . . . . . . . . 20 (((𝑉 + 1)...𝑁) ⊆ (𝑉...𝑁) → (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ (𝑈 “ (𝑉...𝑁)))
424422, 423syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ (𝑈 “ (𝑉...𝑁)))
425424sselda 3588 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → 𝑛 ∈ (𝑈 “ (𝑉...𝑁)))
426 fvun2 6237 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) ∧ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁)) ∧ (((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛))
427360, 362, 426mp3an12 1411 . . . . . . . . . . . . . . . . . . . 20 ((((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛))
428370, 427sylan 488 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛))
42975fvconst2 6434 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (𝑈 “ (𝑉...𝑁)) → (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛) = 0)
430429adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛) = 0)
431428, 430eqtrd 2655 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 0)
432425, 431syldan 487 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 0)
433432adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 0)
434417, 418, 419, 419, 114, 420, 433ofval 6871 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇𝑛) + 0))
435111adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁))
436186adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0)
437417, 435, 419, 419, 114, 420, 436ofval 6871 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇𝑛) + 0))
438434, 437eqtr4d 2658 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
439416, 438mpdan 701 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((𝑇𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
440413, 439jaodan 825 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝑇𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
441440adantlr 750 . . . . . . . . . . 11 (((𝜑𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝑇𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
442203adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑉 < 𝑀) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))
443207a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
444217adantlr 750 . . . . . . . . . . . . . . . 16 (((𝜑𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉))
445 lttr 10074 . . . . . . . . . . . . . . . . . . . . 21 (((𝑉 − 1) ∈ ℝ ∧ 𝑉 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (((𝑉 − 1) < 𝑉𝑉 < 𝑀) → (𝑉 − 1) < 𝑀))
446228, 28, 225, 445syl3anc 1323 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝑉 − 1) < 𝑉𝑉 < 𝑀) → (𝑉 − 1) < 𝑀))
447330, 446mpand 710 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑉 < 𝑀 → (𝑉 − 1) < 𝑀))
448447imp 445 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑉 < 𝑀) → (𝑉 − 1) < 𝑀)
449448iftrued 4072 . . . . . . . . . . . . . . . . 17 ((𝜑𝑉 < 𝑀) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = (𝑉 − 1))
450449adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = (𝑉 − 1))
451444, 450eqtrd 2655 . . . . . . . . . . . . . . 15 (((𝜑𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑉 − 1))
452 simpll 789 . . . . . . . . . . . . . . . 16 (((𝜑𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → 𝜑)
453 oveq2 6623 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = (𝑉 − 1) → (1...𝑗) = (1...(𝑉 − 1)))
454453imaeq2d 5435 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = (𝑉 − 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑉 − 1))))
455454xpeq1d 5108 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑉 − 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑉 − 1))) × {1}))
456455adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 = (𝑉 − 1)) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑉 − 1))) × {1}))
457 oveq1 6622 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝑉 − 1) → (𝑗 + 1) = ((𝑉 − 1) + 1))
458457, 215sylan9eqr 2677 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 = (𝑉 − 1)) → (𝑗 + 1) = 𝑉)
459458oveq1d 6630 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 = (𝑉 − 1)) → ((𝑗 + 1)...𝑁) = (𝑉...𝑁))
460459imaeq2d 5435 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 = (𝑉 − 1)) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (𝑉...𝑁)))
461460xpeq1d 5108 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 = (𝑉 − 1)) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (𝑉...𝑁)) × {0}))
462456, 461uneq12d 3752 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 = (𝑉 − 1)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))
463462oveq2d 6631 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 = (𝑉 − 1)) → (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))))
464452, 463sylan 488 . . . . . . . . . . . . . . 15 ((((𝜑𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) ∧ 𝑗 = (𝑉 − 1)) → (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))))
465443, 451, 464csbied2 3547 . . . . . . . . . . . . . 14 (((𝜑𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))))
466250adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑉 < 𝑀) → (𝑉 − 1) ∈ (0...(𝑁 − 1)))
467 ovexd 6645 . . . . . . . . . . . . . 14 ((𝜑𝑉 < 𝑀) → (𝑇𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))) ∈ V)
468442, 465, 466, 467fvmptd 6255 . . . . . . . . . . . . 13 ((𝜑𝑉 < 𝑀) → (𝐹‘(𝑉 − 1)) = (𝑇𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))))
469468fveq1d 6160 . . . . . . . . . . . 12 ((𝜑𝑉 < 𝑀) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛))
470469adantr 481 . . . . . . . . . . 11 (((𝜑𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛))
471207a1i 11 . . . . . . . . . . . . . . . 16 ((𝑉 < 𝑀𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
472 iftrue 4070 . . . . . . . . . . . . . . . . . . . 20 (𝑉 < 𝑀 → if(𝑉 < 𝑀, 𝑉, (𝑉 + 1)) = 𝑉)
473260, 472sylan9eqr 2677 . . . . . . . . . . . . . . . . . . 19 ((𝑉 < 𝑀𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = 𝑉)
474473eqeq2d 2631 . . . . . . . . . . . . . . . . . 18 ((𝑉 < 𝑀𝑦 = 𝑉) → (𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ↔ 𝑗 = 𝑉))
475474biimpa 501 . . . . . . . . . . . . . . . . 17 (((𝑉 < 𝑀𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → 𝑗 = 𝑉)
476475, 245syl 17 . . . . . . . . . . . . . . . 16 (((𝑉 < 𝑀𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
477471, 476csbied 3546 . . . . . . . . . . . . . . 15 ((𝑉 < 𝑀𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
478477adantll 749 . . . . . . . . . . . . . 14 (((𝜑𝑉 < 𝑀) ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
479282adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑉 < 𝑀) → 𝑉 ∈ (0...(𝑁 − 1)))
480 ovexd 6645 . . . . . . . . . . . . . 14 ((𝜑𝑉 < 𝑀) → (𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))) ∈ V)
481442, 478, 479, 480fvmptd 6255 . . . . . . . . . . . . 13 ((𝜑𝑉 < 𝑀) → (𝐹𝑉) = (𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
482481fveq1d 6160 . . . . . . . . . . . 12 ((𝜑𝑉 < 𝑀) → ((𝐹𝑉)‘𝑛) = ((𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
483482adantr 481 . . . . . . . . . . 11 (((𝜑𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝐹𝑉)‘𝑛) = ((𝑇𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
484441, 470, 4833eqtr4d 2665 . . . . . . . . . 10 (((𝜑𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹𝑉)‘𝑛))
485484ex 450 . . . . . . . . 9 ((𝜑𝑉 < 𝑀) → ((𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹𝑉)‘𝑛)))
486354, 485sylbid 230 . . . . . . . 8 ((𝜑𝑉 < 𝑀) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉})) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹𝑉)‘𝑛)))
487486expdimp 453 . . . . . . 7 (((𝜑𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (¬ 𝑛 ∈ (𝑈 “ {𝑉}) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹𝑉)‘𝑛)))
488487necon1ad 2807 . . . . . 6 (((𝜑𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛) → 𝑛 ∈ (𝑈 “ {𝑉})))
489 elimasni 5461 . . . . . . . 8 (𝑛 ∈ (𝑈 “ {𝑉}) → 𝑉𝑈𝑛)
490 eqcom 2628 . . . . . . . . 9 (𝑛 = (𝑈𝑉) ↔ (𝑈𝑉) = 𝑛)
491 fnbrfvb 6203 . . . . . . . . . 10 ((𝑈 Fn (1...𝑁) ∧ 𝑉 ∈ (1...𝑁)) → ((𝑈𝑉) = 𝑛𝑉𝑈𝑛))
492296, 100, 491syl2anc 692 . . . . . . . . 9 (𝜑 → ((𝑈𝑉) = 𝑛𝑉𝑈𝑛))
493490, 492syl5bb 272 . . . . . . . 8 (𝜑 → (𝑛 = (𝑈𝑉) ↔ 𝑉𝑈𝑛))
494489, 493syl5ibr 236 . . . . . . 7 (𝜑 → (𝑛 ∈ (𝑈 “ {𝑉}) → 𝑛 = (𝑈𝑉)))
495494ad2antrr 761 . . . . . 6 (((𝜑𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (𝑛 ∈ (𝑈 “ {𝑉}) → 𝑛 = (𝑈𝑉)))
496488, 495syld 47 . . . . 5 (((𝜑𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛) → 𝑛 = (𝑈𝑉)))
497496ralrimiva 2962 . . . 4 ((𝜑𝑉 < 𝑀) → ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛) → 𝑛 = (𝑈𝑉)))
498 fvex 6168 . . . . 5 (𝑈𝑉) ∈ V
499 eqeq2 2632 . . . . . . 7 (𝑚 = (𝑈𝑉) → (𝑛 = 𝑚𝑛 = (𝑈𝑉)))
500499imbi2d 330 . . . . . 6 (𝑚 = (𝑈𝑉) → ((((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛) → 𝑛 = (𝑈𝑉))))
501500ralbidv 2982 . . . . 5 (𝑚 = (𝑈𝑉) → (∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛) → 𝑛 = (𝑈𝑉))))
502498, 501spcev 3290 . . . 4 (∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛) → 𝑛 = (𝑈𝑉)) → ∃𝑚𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛) → 𝑛 = 𝑚))
503497, 502syl 17 . . 3 ((𝜑𝑉 < 𝑀) → ∃𝑚𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛) → 𝑛 = 𝑚))
504 eldifsni 4296 . . . . 5 (𝑀 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑀𝑉)
505219, 504syl 17 . . . 4 (𝜑𝑀𝑉)
506225, 28lttri2d 10136 . . . 4 (𝜑 → (𝑀𝑉 ↔ (𝑀 < 𝑉𝑉 < 𝑀)))
507505, 506mpbid 222 . . 3 (𝜑 → (𝑀 < 𝑉𝑉 < 𝑀))
508309, 503, 507mpjaodan 826 . 2 (𝜑 → ∃𝑚𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛) → 𝑛 = 𝑚))
509 nfv 1840 . . . 4 𝑚((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛)
510509rmo2 3512 . . 3 (∃*𝑛 ∈ (𝑈 “ (1...𝑁))((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛) ↔ ∃𝑚𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛) → 𝑛 = 𝑚))
511 rmoeq1 3134 . . . 4 ((𝑈 “ (1...𝑁)) = (1...𝑁) → (∃*𝑛 ∈ (𝑈 “ (1...𝑁))((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛) ↔ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛)))
512107, 511syl 17 . . 3 (𝜑 → (∃*𝑛 ∈ (𝑈 “ (1...𝑁))((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛) ↔ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛)))
513510, 512syl5bbr 274 . 2 (𝜑 → (∃𝑚𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛)))
514508, 513mpbid 222 1 (𝜑 → ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹𝑉)‘𝑛))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384   = wceq 1480  wex 1701  wcel 1987  wne 2790  wral 2908  ∃*wrmo 2911  Vcvv 3190  csb 3519  cdif 3557  cun 3558  cin 3559  wss 3560  c0 3897  ifcif 4064  {csn 4155   class class class wbr 4623  cmpt 4683   × cxp 5082  ccnv 5083  ran crn 5085  cima 5087  Fun wfun 5851   Fn wfn 5852  wf 5853  ontowfo 5855  1-1-ontowf1o 5856  cfv 5857  (class class class)co 6615  𝑓 cof 6860  Fincfn 7915  cc 9894  cr 9895  0cc0 9896  1c1 9897   + caddc 9899   < clt 10034  cle 10035  cmin 10226  cn 10980  cz 11337  cuz 11647  ...cfz 12284
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-cnex 9952  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-iun 4494  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-of 6862  df-om 7028  df-1st 7128  df-2nd 7129  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-1o 7520  df-er 7702  df-en 7916  df-dom 7917  df-sdom 7918  df-fin 7919  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-nn 10981  df-n0 11253  df-z 11338  df-uz 11648  df-fz 12285
This theorem is referenced by:  poimirlem8  33088  poimirlem18  33098  poimirlem21  33101  poimirlem22  33102
  Copyright terms: Public domain W3C validator