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

Theorem poimirlem24 33563
Description: Lemma for poimir 33572, two ways of expressing that a simplex has an admissible face on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0 (𝜑𝑁 ∈ ℕ)
poimirlem28.1 (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶)
poimirlem28.2 ((𝜑𝑝:(1...𝑁)⟶(0...𝐾)) → 𝐵 ∈ (0...𝑁))
poimirlem25.3 (𝜑𝑇:(1...𝑁)⟶(0..^𝐾))
poimirlem25.4 (𝜑𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
poimirlem24.5 (𝜑𝑉 ∈ (0...𝑁))
Assertion
Ref Expression
poimirlem24 (𝜑 → (∃𝑥 ∈ (((0...𝐾) ↑𝑚 (1...𝑁)) ↑𝑚 (0...(𝑁 − 1)))(𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ∧ ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran 𝑥𝐵) ∧ ∃𝑝 ∈ ran 𝑥(𝑝𝑁) ≠ 0)) ↔ (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ ¬ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁)))))
Distinct variable groups:   𝑖,𝑗,𝑝,𝑠,𝑥,𝑦,𝜑   𝑗,𝑁,𝑦   𝑇,𝑗,𝑦   𝑈,𝑗,𝑦   𝑗,𝑉,𝑦   𝜑,𝑖,𝑝,𝑠   𝐵,𝑖,𝑗,𝑠   𝑖,𝐾,𝑗,𝑝,𝑠   𝑖,𝑁,𝑝,𝑠   𝑇,𝑖,𝑝   𝑈,𝑖,𝑝   𝑇,𝑠   𝜑,𝑥   𝑥,𝐵,𝑦   𝐶,𝑖,𝑝,𝑥,𝑦   𝑥,𝐾,𝑦   𝑥,𝑁   𝑥,𝑇   𝑈,𝑠,𝑥   𝑖,𝑉,𝑝,𝑠,𝑥
Allowed substitution hints:   𝐵(𝑝)   𝐶(𝑗,𝑠)

Proof of Theorem poimirlem24
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 nfv 1883 . . . . . . . . 9 𝑗(𝜑𝑦 ∈ (0...(𝑁 − 1)))
2 nfcsb1v 3582 . . . . . . . . . 10 𝑗𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))
3 nfcv 2793 . . . . . . . . . 10 𝑗(1...𝑁)
4 nfcv 2793 . . . . . . . . . 10 𝑗(0...𝐾)
52, 3, 4nff 6079 . . . . . . . . 9 𝑗𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)
61, 5nfim 1865 . . . . . . . 8 𝑗((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
7 eleq1 2718 . . . . . . . . . 10 (𝑗 = 𝑦 → (𝑗 ∈ (0...(𝑁 − 1)) ↔ 𝑦 ∈ (0...(𝑁 − 1))))
87anbi2d 740 . . . . . . . . 9 (𝑗 = 𝑦 → ((𝜑𝑗 ∈ (0...(𝑁 − 1))) ↔ (𝜑𝑦 ∈ (0...(𝑁 − 1)))))
9 csbeq1a 3575 . . . . . . . . . 10 (𝑗 = 𝑦 → (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = 𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
109feq1d 6068 . . . . . . . . 9 (𝑗 = 𝑦 → ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) ↔ 𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))
118, 10imbi12d 333 . . . . . . . 8 (𝑗 = 𝑦 → (((𝜑𝑗 ∈ (0...(𝑁 − 1))) → (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) ↔ ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))))
12 poimir.0 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℕ)
1312nncnd 11074 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℂ)
14 npcan1 10493 . . . . . . . . . . . . 13 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
1513, 14syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
1612nnzd 11519 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
17 peano2zm 11458 . . . . . . . . . . . . . 14 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
1816, 17syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑁 − 1) ∈ ℤ)
19 uzid 11740 . . . . . . . . . . . . 13 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
20 peano2uz 11779 . . . . . . . . . . . . 13 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
2118, 19, 203syl 18 . . . . . . . . . . . 12 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
2215, 21eqeltrrd 2731 . . . . . . . . . . 11 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
23 fzss2 12419 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (0...(𝑁 − 1)) ⊆ (0...𝑁))
2422, 23syl 17 . . . . . . . . . 10 (𝜑 → (0...(𝑁 − 1)) ⊆ (0...𝑁))
2524sselda 3636 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → 𝑗 ∈ (0...𝑁))
26 elun 3786 . . . . . . . . . . . . 13 (𝑦 ∈ ({1} ∪ {0}) ↔ (𝑦 ∈ {1} ∨ 𝑦 ∈ {0}))
27 fzofzp1 12605 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0..^𝐾) → (𝑥 + 1) ∈ (0...𝐾))
28 elsni 4227 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {1} → 𝑦 = 1)
2928oveq2d 6706 . . . . . . . . . . . . . . . 16 (𝑦 ∈ {1} → (𝑥 + 𝑦) = (𝑥 + 1))
3029eleq1d 2715 . . . . . . . . . . . . . . 15 (𝑦 ∈ {1} → ((𝑥 + 𝑦) ∈ (0...𝐾) ↔ (𝑥 + 1) ∈ (0...𝐾)))
3127, 30syl5ibrcom 237 . . . . . . . . . . . . . 14 (𝑥 ∈ (0..^𝐾) → (𝑦 ∈ {1} → (𝑥 + 𝑦) ∈ (0...𝐾)))
32 elfzoelz 12509 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (0..^𝐾) → 𝑥 ∈ ℤ)
3332zcnd 11521 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (0..^𝐾) → 𝑥 ∈ ℂ)
3433addid1d 10274 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (0..^𝐾) → (𝑥 + 0) = 𝑥)
35 elfzofz 12524 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (0..^𝐾) → 𝑥 ∈ (0...𝐾))
3634, 35eqeltrd 2730 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0..^𝐾) → (𝑥 + 0) ∈ (0...𝐾))
37 elsni 4227 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {0} → 𝑦 = 0)
3837oveq2d 6706 . . . . . . . . . . . . . . . 16 (𝑦 ∈ {0} → (𝑥 + 𝑦) = (𝑥 + 0))
3938eleq1d 2715 . . . . . . . . . . . . . . 15 (𝑦 ∈ {0} → ((𝑥 + 𝑦) ∈ (0...𝐾) ↔ (𝑥 + 0) ∈ (0...𝐾)))
4036, 39syl5ibrcom 237 . . . . . . . . . . . . . 14 (𝑥 ∈ (0..^𝐾) → (𝑦 ∈ {0} → (𝑥 + 𝑦) ∈ (0...𝐾)))
4131, 40jaod 394 . . . . . . . . . . . . 13 (𝑥 ∈ (0..^𝐾) → ((𝑦 ∈ {1} ∨ 𝑦 ∈ {0}) → (𝑥 + 𝑦) ∈ (0...𝐾)))
4226, 41syl5bi 232 . . . . . . . . . . . 12 (𝑥 ∈ (0..^𝐾) → (𝑦 ∈ ({1} ∪ {0}) → (𝑥 + 𝑦) ∈ (0...𝐾)))
4342imp 444 . . . . . . . . . . 11 ((𝑥 ∈ (0..^𝐾) ∧ 𝑦 ∈ ({1} ∪ {0})) → (𝑥 + 𝑦) ∈ (0...𝐾))
4443adantl 481 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ (0..^𝐾) ∧ 𝑦 ∈ ({1} ∪ {0}))) → (𝑥 + 𝑦) ∈ (0...𝐾))
45 poimirlem25.3 . . . . . . . . . . 11 (𝜑𝑇:(1...𝑁)⟶(0..^𝐾))
4645adantr 480 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇:(1...𝑁)⟶(0..^𝐾))
47 1ex 10073 . . . . . . . . . . . . . 14 1 ∈ V
4847fconst 6129 . . . . . . . . . . . . 13 ((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1}
49 c0ex 10072 . . . . . . . . . . . . . 14 0 ∈ V
5049fconst 6129 . . . . . . . . . . . . 13 ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}
5148, 50pm3.2i 470 . . . . . . . . . . . 12 (((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0})
52 poimirlem25.4 . . . . . . . . . . . . . 14 (𝜑𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
53 dff1o3 6181 . . . . . . . . . . . . . . 15 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun 𝑈))
5453simprbi 479 . . . . . . . . . . . . . 14 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun 𝑈)
55 imain 6012 . . . . . . . . . . . . . 14 (Fun 𝑈 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))))
5652, 54, 553syl 18 . . . . . . . . . . . . 13 (𝜑 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))))
57 elfznn0 12471 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ0)
5857nn0red 11390 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
5958ltp1d 10992 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1))
60 fzdisj 12406 . . . . . . . . . . . . . . . 16 (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
6159, 60syl 17 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
6261imaeq2d 5501 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (𝑈 “ ∅))
63 ima0 5516 . . . . . . . . . . . . . 14 (𝑈 “ ∅) = ∅
6462, 63syl6eq 2701 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
6556, 64sylan9req 2706 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
66 fun 6104 . . . . . . . . . . . 12 (((((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}) ∧ ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
6751, 65, 66sylancr 696 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
68 nn0p1nn 11370 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
6957, 68syl 17 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ)
70 nnuz 11761 . . . . . . . . . . . . . . . . 17 ℕ = (ℤ‘1)
7169, 70syl6eleq 2740 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (ℤ‘1))
72 elfzuz3 12377 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ𝑗))
73 fzsplit2 12404 . . . . . . . . . . . . . . . 16 (((𝑗 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
7471, 72, 73syl2anc 694 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
7574imaeq2d 5501 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑁) → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))))
76 imaundi 5580 . . . . . . . . . . . . . 14 (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))
7775, 76syl6req 2702 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑁) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (𝑈 “ (1...𝑁)))
78 f1ofo 6182 . . . . . . . . . . . . . 14 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁))
79 foima 6158 . . . . . . . . . . . . . 14 (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁))
8052, 78, 793syl 18 . . . . . . . . . . . . 13 (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁))
8177, 80sylan9eqr 2707 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (1...𝑁))
8281feq2d 6069 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}) ↔ (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0})))
8367, 82mpbid 222 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
84 ovex 6718 . . . . . . . . . . 11 (1...𝑁) ∈ V
8584a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ V)
86 inidm 3855 . . . . . . . . . 10 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
8744, 46, 83, 85, 85, 86off 6954 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
8825, 87syldan 486 . . . . . . . 8 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
896, 11, 88chvar 2298 . . . . . . 7 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
90 fzp1elp1 12432 . . . . . . . . 9 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ (0...((𝑁 − 1) + 1)))
9115oveq2d 6706 . . . . . . . . . . 11 (𝜑 → (0...((𝑁 − 1) + 1)) = (0...𝑁))
9291eleq2d 2716 . . . . . . . . . 10 (𝜑 → ((𝑦 + 1) ∈ (0...((𝑁 − 1) + 1)) ↔ (𝑦 + 1) ∈ (0...𝑁)))
9392biimpa 500 . . . . . . . . 9 ((𝜑 ∧ (𝑦 + 1) ∈ (0...((𝑁 − 1) + 1))) → (𝑦 + 1) ∈ (0...𝑁))
9490, 93sylan2 490 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 + 1) ∈ (0...𝑁))
95 nfv 1883 . . . . . . . . . 10 𝑗(𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁))
96 nfcsb1v 3582 . . . . . . . . . . 11 𝑗(𝑦 + 1) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))
9796, 3, 4nff 6079 . . . . . . . . . 10 𝑗(𝑦 + 1) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)
9895, 97nfim 1865 . . . . . . . . 9 𝑗((𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁)) → (𝑦 + 1) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
99 ovex 6718 . . . . . . . . 9 (𝑦 + 1) ∈ V
100 eleq1 2718 . . . . . . . . . . 11 (𝑗 = (𝑦 + 1) → (𝑗 ∈ (0...𝑁) ↔ (𝑦 + 1) ∈ (0...𝑁)))
101100anbi2d 740 . . . . . . . . . 10 (𝑗 = (𝑦 + 1) → ((𝜑𝑗 ∈ (0...𝑁)) ↔ (𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁))))
102 csbeq1a 3575 . . . . . . . . . . 11 (𝑗 = (𝑦 + 1) → (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑦 + 1) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
103102feq1d 6068 . . . . . . . . . 10 (𝑗 = (𝑦 + 1) → ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) ↔ (𝑦 + 1) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))
104101, 103imbi12d 333 . . . . . . . . 9 (𝑗 = (𝑦 + 1) → (((𝜑𝑗 ∈ (0...𝑁)) → (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) ↔ ((𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁)) → (𝑦 + 1) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))))
10598, 99, 104, 87vtoclf 3289 . . . . . . . 8 ((𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁)) → (𝑦 + 1) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
10694, 105syldan 486 . . . . . . 7 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 + 1) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
107 csbeq1 3569 . . . . . . . . 9 (𝑦 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → 𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
108107feq1d 6068 . . . . . . . 8 (𝑦 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → (𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) ↔ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))
109 csbeq1 3569 . . . . . . . . 9 ((𝑦 + 1) = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → (𝑦 + 1) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
110109feq1d 6068 . . . . . . . 8 ((𝑦 + 1) = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → ((𝑦 + 1) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) ↔ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))
111108, 110ifboth 4157 . . . . . . 7 ((𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) ∧ (𝑦 + 1) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
11289, 106, 111syl2anc 694 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
113 ovex 6718 . . . . . . 7 (0...𝐾) ∈ V
114113, 84elmap 7928 . . . . . 6 (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ ((0...𝐾) ↑𝑚 (1...𝑁)) ↔ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
115112, 114sylibr 224 . . . . 5 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ ((0...𝐾) ↑𝑚 (1...𝑁)))
116 eqid 2651 . . . . 5 (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
117115, 116fmptd 6425 . . . 4 (𝜑 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))):(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))
118 ovex 6718 . . . . 5 ((0...𝐾) ↑𝑚 (1...𝑁)) ∈ V
119 ovex 6718 . . . . 5 (0...(𝑁 − 1)) ∈ V
120118, 119elmap 7928 . . . 4 ((𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ∈ (((0...𝐾) ↑𝑚 (1...𝑁)) ↑𝑚 (0...(𝑁 − 1))) ↔ (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))):(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))
121117, 120sylibr 224 . . 3 (𝜑 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ∈ (((0...𝐾) ↑𝑚 (1...𝑁)) ↑𝑚 (0...(𝑁 − 1))))
122 rneq 5383 . . . . . . . 8 (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → ran 𝑥 = ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))
123122mpteq1d 4771 . . . . . . 7 (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → (𝑝 ∈ ran 𝑥𝐵) = (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵))
124123rneqd 5385 . . . . . 6 (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → ran (𝑝 ∈ ran 𝑥𝐵) = ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵))
125124sseq2d 3666 . . . . 5 (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran 𝑥𝐵) ↔ (0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵)))
126122rexeqdv 3175 . . . . 5 (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → (∃𝑝 ∈ ran 𝑥(𝑝𝑁) ≠ 0 ↔ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0))
127125, 126anbi12d 747 . . . 4 (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → (((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran 𝑥𝐵) ∧ ∃𝑝 ∈ ran 𝑥(𝑝𝑁) ≠ 0) ↔ ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ∧ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0)))
128127ceqsrexv 3367 . . 3 ((𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ∈ (((0...𝐾) ↑𝑚 (1...𝑁)) ↑𝑚 (0...(𝑁 − 1))) → (∃𝑥 ∈ (((0...𝐾) ↑𝑚 (1...𝑁)) ↑𝑚 (0...(𝑁 − 1)))(𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ∧ ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran 𝑥𝐵) ∧ ∃𝑝 ∈ ran 𝑥(𝑝𝑁) ≠ 0)) ↔ ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ∧ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0)))
129121, 128syl 17 . 2 (𝜑 → (∃𝑥 ∈ (((0...𝐾) ↑𝑚 (1...𝑁)) ↑𝑚 (0...(𝑁 − 1)))(𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ∧ ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran 𝑥𝐵) ∧ ∃𝑝 ∈ ran 𝑥(𝑝𝑁) ≠ 0)) ↔ ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ∧ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0)))
130 dfss3 3625 . . . 4 ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ↔ ∀𝑖 ∈ (0...(𝑁 − 1))𝑖 ∈ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵))
131 ovex 6718 . . . . . . . . . . . . 13 ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
132 poimirlem28.1 . . . . . . . . . . . . 13 (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶)
133131, 132csbie 3592 . . . . . . . . . . . 12 ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵 = 𝐶
134133csbeq2i 4026 . . . . . . . . . . 11 𝑇, 𝑈⟩ / 𝑠((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵 = 𝑇, 𝑈⟩ / 𝑠𝐶
135 opex 4962 . . . . . . . . . . . . 13 𝑇, 𝑈⟩ ∈ V
136135a1i 11 . . . . . . . . . . . 12 (𝜑 → ⟨𝑇, 𝑈⟩ ∈ V)
137 fveq2 6229 . . . . . . . . . . . . . . 15 (𝑠 = ⟨𝑇, 𝑈⟩ → (1st𝑠) = (1st ‘⟨𝑇, 𝑈⟩))
138 fex 6530 . . . . . . . . . . . . . . . . 17 ((𝑇:(1...𝑁)⟶(0..^𝐾) ∧ (1...𝑁) ∈ V) → 𝑇 ∈ V)
13945, 84, 138sylancl 695 . . . . . . . . . . . . . . . 16 (𝜑𝑇 ∈ V)
140 f1oexrnex 7157 . . . . . . . . . . . . . . . . 17 ((𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ∧ (1...𝑁) ∈ V) → 𝑈 ∈ V)
14152, 84, 140sylancl 695 . . . . . . . . . . . . . . . 16 (𝜑𝑈 ∈ V)
142 op1stg 7222 . . . . . . . . . . . . . . . 16 ((𝑇 ∈ V ∧ 𝑈 ∈ V) → (1st ‘⟨𝑇, 𝑈⟩) = 𝑇)
143139, 141, 142syl2anc 694 . . . . . . . . . . . . . . 15 (𝜑 → (1st ‘⟨𝑇, 𝑈⟩) = 𝑇)
144137, 143sylan9eqr 2707 . . . . . . . . . . . . . 14 ((𝜑𝑠 = ⟨𝑇, 𝑈⟩) → (1st𝑠) = 𝑇)
145 fveq2 6229 . . . . . . . . . . . . . . . 16 (𝑠 = ⟨𝑇, 𝑈⟩ → (2nd𝑠) = (2nd ‘⟨𝑇, 𝑈⟩))
146 op2ndg 7223 . . . . . . . . . . . . . . . . 17 ((𝑇 ∈ V ∧ 𝑈 ∈ V) → (2nd ‘⟨𝑇, 𝑈⟩) = 𝑈)
147139, 141, 146syl2anc 694 . . . . . . . . . . . . . . . 16 (𝜑 → (2nd ‘⟨𝑇, 𝑈⟩) = 𝑈)
148145, 147sylan9eqr 2707 . . . . . . . . . . . . . . 15 ((𝜑𝑠 = ⟨𝑇, 𝑈⟩) → (2nd𝑠) = 𝑈)
149 imaeq1 5496 . . . . . . . . . . . . . . . . 17 ((2nd𝑠) = 𝑈 → ((2nd𝑠) “ (1...𝑗)) = (𝑈 “ (1...𝑗)))
150149xpeq1d 5172 . . . . . . . . . . . . . . . 16 ((2nd𝑠) = 𝑈 → (((2nd𝑠) “ (1...𝑗)) × {1}) = ((𝑈 “ (1...𝑗)) × {1}))
151 imaeq1 5496 . . . . . . . . . . . . . . . . 17 ((2nd𝑠) = 𝑈 → ((2nd𝑠) “ ((𝑗 + 1)...𝑁)) = (𝑈 “ ((𝑗 + 1)...𝑁)))
152151xpeq1d 5172 . . . . . . . . . . . . . . . 16 ((2nd𝑠) = 𝑈 → (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))
153150, 152uneq12d 3801 . . . . . . . . . . . . . . 15 ((2nd𝑠) = 𝑈 → ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))
154148, 153syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑠 = ⟨𝑇, 𝑈⟩) → ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))
155144, 154oveq12d 6708 . . . . . . . . . . . . 13 ((𝜑𝑠 = ⟨𝑇, 𝑈⟩) → ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
156155csbeq1d 3573 . . . . . . . . . . . 12 ((𝜑𝑠 = ⟨𝑇, 𝑈⟩) → ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵 = (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
157136, 156csbied 3593 . . . . . . . . . . 11 (𝜑𝑇, 𝑈⟩ / 𝑠((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵 = (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
158134, 157syl5eqr 2699 . . . . . . . . . 10 (𝜑𝑇, 𝑈⟩ / 𝑠𝐶 = (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
159158csbeq2dv 4025 . . . . . . . . 9 (𝜑if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
160159eqeq2d 2661 . . . . . . . 8 (𝜑 → (𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵))
161160rexbidv 3081 . . . . . . 7 (𝜑 → (∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵))
162 vex 3234 . . . . . . . . 9 𝑖 ∈ V
163 eqid 2651 . . . . . . . . . 10 (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) = (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵)
164163elrnmpt 5404 . . . . . . . . 9 (𝑖 ∈ V → (𝑖 ∈ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ↔ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))𝑖 = 𝐵))
165162, 164ax-mp 5 . . . . . . . 8 (𝑖 ∈ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ↔ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))𝑖 = 𝐵)
166 nfv 1883 . . . . . . . . 9 𝑘 𝑖 = 𝐵
167 nfcsb1v 3582 . . . . . . . . . 10 𝑝𝑘 / 𝑝𝐵
168167nfeq2 2809 . . . . . . . . 9 𝑝 𝑖 = 𝑘 / 𝑝𝐵
169 csbeq1a 3575 . . . . . . . . . 10 (𝑝 = 𝑘𝐵 = 𝑘 / 𝑝𝐵)
170169eqeq2d 2661 . . . . . . . . 9 (𝑝 = 𝑘 → (𝑖 = 𝐵𝑖 = 𝑘 / 𝑝𝐵))
171166, 168, 170cbvrex 3198 . . . . . . . 8 (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))𝑖 = 𝐵 ↔ ∃𝑘 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))𝑖 = 𝑘 / 𝑝𝐵)
172 ovex 6718 . . . . . . . . . . 11 (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
173172csbex 4826 . . . . . . . . . 10 if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
174173rgenw 2953 . . . . . . . . 9 𝑦 ∈ (0...(𝑁 − 1))if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
175 csbeq1 3569 . . . . . . . . . . . 12 (𝑘 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝑘 / 𝑝𝐵 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
176 vex 3234 . . . . . . . . . . . . . 14 𝑦 ∈ V
177176, 99ifex 4189 . . . . . . . . . . . . 13 if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) ∈ V
178 csbnestg 4031 . . . . . . . . . . . . 13 (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) ∈ V → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
179177, 178ax-mp 5 . . . . . . . . . . . 12 if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵
180175, 179syl6eqr 2703 . . . . . . . . . . 11 (𝑘 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝑘 / 𝑝𝐵 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
181180eqeq2d 2661 . . . . . . . . . 10 (𝑘 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑖 = 𝑘 / 𝑝𝐵𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵))
182116, 181rexrnmpt 6409 . . . . . . . . 9 (∀𝑦 ∈ (0...(𝑁 − 1))if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V → (∃𝑘 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))𝑖 = 𝑘 / 𝑝𝐵 ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵))
183174, 182ax-mp 5 . . . . . . . 8 (∃𝑘 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))𝑖 = 𝑘 / 𝑝𝐵 ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
184165, 171, 1833bitri 286 . . . . . . 7 (𝑖 ∈ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
185161, 184syl6bbr 278 . . . . . 6 (𝜑 → (∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑖 ∈ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵)))
18624sselda 3636 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ (0...𝑁))
187186adantr 480 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < 𝑉) → 𝑦 ∈ (0...𝑁))
188 elfzelz 12380 . . . . . . . . . . . . . 14 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℤ)
189188zred 11520 . . . . . . . . . . . . 13 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ)
190189adantl 481 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ ℝ)
191 ltne 10172 . . . . . . . . . . . . 13 ((𝑦 ∈ ℝ ∧ 𝑦 < 𝑉) → 𝑉𝑦)
192191necomd 2878 . . . . . . . . . . . 12 ((𝑦 ∈ ℝ ∧ 𝑦 < 𝑉) → 𝑦𝑉)
193190, 192sylan 487 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < 𝑉) → 𝑦𝑉)
194 eldifsn 4350 . . . . . . . . . . 11 (𝑦 ∈ ((0...𝑁) ∖ {𝑉}) ↔ (𝑦 ∈ (0...𝑁) ∧ 𝑦𝑉))
195187, 193, 194sylanbrc 699 . . . . . . . . . 10 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < 𝑉) → 𝑦 ∈ ((0...𝑁) ∖ {𝑉}))
19694adantr 480 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → (𝑦 + 1) ∈ (0...𝑁))
197 poimirlem24.5 . . . . . . . . . . . . . . 15 (𝜑𝑉 ∈ (0...𝑁))
198 elfzelz 12380 . . . . . . . . . . . . . . 15 (𝑉 ∈ (0...𝑁) → 𝑉 ∈ ℤ)
199197, 198syl 17 . . . . . . . . . . . . . 14 (𝜑𝑉 ∈ ℤ)
200199zred 11520 . . . . . . . . . . . . 13 (𝜑𝑉 ∈ ℝ)
201200ad2antrr 762 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → 𝑉 ∈ ℝ)
202 zre 11419 . . . . . . . . . . . . . . . 16 (𝑉 ∈ ℤ → 𝑉 ∈ ℝ)
203 zre 11419 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℤ → 𝑦 ∈ ℝ)
204 lenlt 10154 . . . . . . . . . . . . . . . 16 ((𝑉 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑉𝑦 ↔ ¬ 𝑦 < 𝑉))
205202, 203, 204syl2an 493 . . . . . . . . . . . . . . 15 ((𝑉 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑉𝑦 ↔ ¬ 𝑦 < 𝑉))
206 zleltp1 11466 . . . . . . . . . . . . . . 15 ((𝑉 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑉𝑦𝑉 < (𝑦 + 1)))
207205, 206bitr3d 270 . . . . . . . . . . . . . 14 ((𝑉 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (¬ 𝑦 < 𝑉𝑉 < (𝑦 + 1)))
208199, 188, 207syl2an 493 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (¬ 𝑦 < 𝑉𝑉 < (𝑦 + 1)))
209208biimpa 500 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → 𝑉 < (𝑦 + 1))
210201, 209gtned 10210 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → (𝑦 + 1) ≠ 𝑉)
211 eldifsn 4350 . . . . . . . . . . 11 ((𝑦 + 1) ∈ ((0...𝑁) ∖ {𝑉}) ↔ ((𝑦 + 1) ∈ (0...𝑁) ∧ (𝑦 + 1) ≠ 𝑉))
212196, 210, 211sylanbrc 699 . . . . . . . . . 10 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → (𝑦 + 1) ∈ ((0...𝑁) ∖ {𝑉}))
213195, 212ifclda 4153 . . . . . . . . 9 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) ∈ ((0...𝑁) ∖ {𝑉}))
214 nfcsb1v 3582 . . . . . . . . . . . 12 𝑗if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
215214nfeq2 2809 . . . . . . . . . . 11 𝑗 𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
216 csbeq1a 3575 . . . . . . . . . . . 12 (𝑗 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → 𝑇, 𝑈⟩ / 𝑠𝐶 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
217216eqeq2d 2661 . . . . . . . . . . 11 (𝑗 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
218215, 217rspce 3335 . . . . . . . . . 10 ((if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) ∈ ((0...𝑁) ∖ {𝑉}) ∧ 𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
219218ex 449 . . . . . . . . 9 (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) ∈ ((0...𝑁) ∖ {𝑉}) → (𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
220213, 219syl 17 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
221220rexlimdva 3060 . . . . . . 7 (𝜑 → (∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
222 nfv 1883 . . . . . . . 8 𝑗𝜑
223 nfcv 2793 . . . . . . . . 9 𝑗(0...(𝑁 − 1))
224223, 215nfrex 3036 . . . . . . . 8 𝑗𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
225 eldifi 3765 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ (0...𝑁))
226225, 57syl 17 . . . . . . . . . . . . . 14 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ ℕ0)
227226nn0ge0d 11392 . . . . . . . . . . . . 13 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 0 ≤ 𝑗)
228227ad2antlr 763 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 0 ≤ 𝑗)
229226nn0red 11390 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ ℝ)
230229ad2antlr 763 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 ∈ ℝ)
231200ad2antrr 762 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑉 ∈ ℝ)
23216zred 11520 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℝ)
233232ad2antrr 762 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑁 ∈ ℝ)
234 simpr 476 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 < 𝑉)
235 elfzle2 12383 . . . . . . . . . . . . . . . 16 (𝑉 ∈ (0...𝑁) → 𝑉𝑁)
236197, 235syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑉𝑁)
237236ad2antrr 762 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑉𝑁)
238230, 231, 233, 234, 237ltletrd 10235 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 < 𝑁)
239226nn0zd 11518 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ ℤ)
240 zltlem1 11468 . . . . . . . . . . . . . . 15 ((𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 < 𝑁𝑗 ≤ (𝑁 − 1)))
241239, 16, 240syl2anr 494 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗 < 𝑁𝑗 ≤ (𝑁 − 1)))
242241adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → (𝑗 < 𝑁𝑗 ≤ (𝑁 − 1)))
243238, 242mpbid 222 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 ≤ (𝑁 − 1))
244 0z 11426 . . . . . . . . . . . . . . 15 0 ∈ ℤ
245 elfz 12370 . . . . . . . . . . . . . . 15 ((𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑗 ∈ (0...(𝑁 − 1)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝑁 − 1))))
246244, 245mp3an2 1452 . . . . . . . . . . . . . 14 ((𝑗 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑗 ∈ (0...(𝑁 − 1)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝑁 − 1))))
247239, 18, 246syl2anr 494 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗 ∈ (0...(𝑁 − 1)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝑁 − 1))))
248247adantr 480 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → (𝑗 ∈ (0...(𝑁 − 1)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝑁 − 1))))
249228, 243, 248mpbir2and 977 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 ∈ (0...(𝑁 − 1)))
250 0red 10079 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 0 ∈ ℝ)
251200ad2antrr 762 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑉 ∈ ℝ)
252229ad2antlr 763 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗 ∈ ℝ)
253 elfzle1 12382 . . . . . . . . . . . . . . . . 17 (𝑉 ∈ (0...𝑁) → 0 ≤ 𝑉)
254197, 253syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ 𝑉)
255254ad2antrr 762 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 0 ≤ 𝑉)
256 lenlt 10154 . . . . . . . . . . . . . . . . . 18 ((𝑉 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑉𝑗 ↔ ¬ 𝑗 < 𝑉))
257200, 229, 256syl2an 493 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑉𝑗 ↔ ¬ 𝑗 < 𝑉))
258257biimpar 501 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑉𝑗)
259 eldifsni 4353 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗𝑉)
260259ad2antlr 763 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗𝑉)
261 ltlen 10176 . . . . . . . . . . . . . . . . . 18 ((𝑉 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑉 < 𝑗 ↔ (𝑉𝑗𝑗𝑉)))
262200, 229, 261syl2an 493 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑉 < 𝑗 ↔ (𝑉𝑗𝑗𝑉)))
263262adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → (𝑉 < 𝑗 ↔ (𝑉𝑗𝑗𝑉)))
264258, 260, 263mpbir2and 977 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑉 < 𝑗)
265250, 251, 252, 255, 264lelttrd 10233 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 0 < 𝑗)
266 zgt0ge1 11469 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℤ → (0 < 𝑗 ↔ 1 ≤ 𝑗))
267239, 266syl 17 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → (0 < 𝑗 ↔ 1 ≤ 𝑗))
268267ad2antlr 763 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → (0 < 𝑗 ↔ 1 ≤ 𝑗))
269265, 268mpbid 222 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 1 ≤ 𝑗)
270 elfzle2 12383 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑁) → 𝑗𝑁)
271225, 270syl 17 . . . . . . . . . . . . . 14 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗𝑁)
272271ad2antlr 763 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗𝑁)
273 1z 11445 . . . . . . . . . . . . . . . 16 1 ∈ ℤ
274 elfz 12370 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 ∈ (1...𝑁) ↔ (1 ≤ 𝑗𝑗𝑁)))
275273, 274mp3an2 1452 . . . . . . . . . . . . . . 15 ((𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 ∈ (1...𝑁) ↔ (1 ≤ 𝑗𝑗𝑁)))
276239, 16, 275syl2anr 494 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗 ∈ (1...𝑁) ↔ (1 ≤ 𝑗𝑗𝑁)))
277276adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → (𝑗 ∈ (1...𝑁) ↔ (1 ≤ 𝑗𝑗𝑁)))
278269, 272, 277mpbir2and 977 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗 ∈ (1...𝑁))
279 elfzmlbm 12488 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑁) → (𝑗 − 1) ∈ (0...(𝑁 − 1)))
280278, 279syl 17 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → (𝑗 − 1) ∈ (0...(𝑁 − 1)))
281249, 280ifclda 4153 . . . . . . . . . 10 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) ∈ (0...(𝑁 − 1)))
282 breq1 4688 . . . . . . . . . . . . . . . 16 (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 < 𝑉 ↔ if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉))
283 id 22 . . . . . . . . . . . . . . . 16 (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → 𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)))
284 oveq1 6697 . . . . . . . . . . . . . . . 16 (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 + 1) = (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))
285282, 283, 284ifbieq12d 4146 . . . . . . . . . . . . . . 15 (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)) = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)))
286285eqeq2d 2661 . . . . . . . . . . . . . 14 (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)) ↔ 𝑗 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))))
287 breq1 4688 . . . . . . . . . . . . . . . 16 ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → ((𝑗 − 1) < 𝑉 ↔ if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉))
288 id 22 . . . . . . . . . . . . . . . 16 ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)))
289 oveq1 6697 . . . . . . . . . . . . . . . 16 ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → ((𝑗 − 1) + 1) = (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))
290287, 288, 289ifbieq12d 4146 . . . . . . . . . . . . . . 15 ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → if((𝑗 − 1) < 𝑉, (𝑗 − 1), ((𝑗 − 1) + 1)) = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)))
291290eqeq2d 2661 . . . . . . . . . . . . . 14 ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 = if((𝑗 − 1) < 𝑉, (𝑗 − 1), ((𝑗 − 1) + 1)) ↔ 𝑗 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))))
292 iftrue 4125 . . . . . . . . . . . . . . . 16 (𝑗 < 𝑉 → if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)) = 𝑗)
293292eqcomd 2657 . . . . . . . . . . . . . . 15 (𝑗 < 𝑉𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)))
294293adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)))
295 zlem1lt 11467 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ℤ ∧ 𝑉 ∈ ℤ) → (𝑗𝑉 ↔ (𝑗 − 1) < 𝑉))
296239, 199, 295syl2anr 494 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗𝑉 ↔ (𝑗 − 1) < 𝑉))
297259necomd 2878 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑉𝑗)
298297adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → 𝑉𝑗)
299 ltlen 10176 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑗 < 𝑉 ↔ (𝑗𝑉𝑉𝑗)))
300229, 200, 299syl2anr 494 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗 < 𝑉 ↔ (𝑗𝑉𝑉𝑗)))
301300biimprd 238 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → ((𝑗𝑉𝑉𝑗) → 𝑗 < 𝑉))
302298, 301mpan2d 710 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗𝑉𝑗 < 𝑉))
303296, 302sylbird 250 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → ((𝑗 − 1) < 𝑉𝑗 < 𝑉))
304303con3dimp 456 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → ¬ (𝑗 − 1) < 𝑉)
305304iffalsed 4130 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → if((𝑗 − 1) < 𝑉, (𝑗 − 1), ((𝑗 − 1) + 1)) = ((𝑗 − 1) + 1))
306226nn0cnd 11391 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ ℂ)
307 npcan1 10493 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℂ → ((𝑗 − 1) + 1) = 𝑗)
308306, 307syl 17 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → ((𝑗 − 1) + 1) = 𝑗)
309308ad2antlr 763 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → ((𝑗 − 1) + 1) = 𝑗)
310305, 309eqtr2d 2686 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗 = if((𝑗 − 1) < 𝑉, (𝑗 − 1), ((𝑗 − 1) + 1)))
311286, 291, 294, 310ifbothda 4156 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → 𝑗 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)))
312 csbeq1a 3575 . . . . . . . . . . . . 13 (𝑗 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) → 𝑇, 𝑈⟩ / 𝑠𝐶 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
313311, 312syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → 𝑇, 𝑈⟩ / 𝑠𝐶 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
314313eqeq2d 2661 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
315314biimpd 219 . . . . . . . . . 10 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
316 breq1 4688 . . . . . . . . . . . . . 14 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑦 < 𝑉 ↔ if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉))
317 id 22 . . . . . . . . . . . . . 14 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → 𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)))
318 oveq1 6697 . . . . . . . . . . . . . 14 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑦 + 1) = (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))
319316, 317, 318ifbieq12d 4146 . . . . . . . . . . . . 13 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)))
320319csbeq1d 3573 . . . . . . . . . . . 12 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
321320eqeq2d 2661 . . . . . . . . . . 11 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
322321rspcev 3340 . . . . . . . . . 10 ((if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) ∈ (0...(𝑁 − 1)) ∧ 𝑖 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
323281, 315, 322syl6an 567 . . . . . . . . 9 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
324323ex 449 . . . . . . . 8 (𝜑 → (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)))
325222, 224, 324rexlimd 3055 . . . . . . 7 (𝜑 → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
326221, 325impbid 202 . . . . . 6 (𝜑 → (∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
327185, 326bitr3d 270 . . . . 5 (𝜑 → (𝑖 ∈ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
328327ralbidv 3015 . . . 4 (𝜑 → (∀𝑖 ∈ (0...(𝑁 − 1))𝑖 ∈ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
329130, 328syl5bb 272 . . 3 (𝜑 → ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
330329anbi1d 741 . 2 (𝜑 → (((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ∧ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0) ↔ (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0)))
33112, 45, 52, 197poimirlem23 33562 . . 3 (𝜑 → (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁))))
332331anbi2d 740 . 2 (𝜑 → ((∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0) ↔ (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ ¬ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁)))))
333129, 330, 3323bitrd 294 1 (𝜑 → (∃𝑥 ∈ (((0...𝐾) ↑𝑚 (1...𝑁)) ↑𝑚 (0...(𝑁 − 1)))(𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ∧ ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran 𝑥𝐵) ∧ ∃𝑝 ∈ ran 𝑥(𝑝𝑁) ≠ 0)) ↔ (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ ¬ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383   = wceq 1523  wcel 2030  wne 2823  wral 2941  wrex 2942  Vcvv 3231  csb 3566  cdif 3604  cun 3605  cin 3606  wss 3607  c0 3948  ifcif 4119  {csn 4210  cop 4216   class class class wbr 4685  cmpt 4762   × cxp 5141  ccnv 5142  ran crn 5144  cima 5146  Fun wfun 5920  wf 5922  ontowfo 5924  1-1-ontowf1o 5925  cfv 5926  (class class class)co 6690  𝑓 cof 6937  1st c1st 7208  2nd c2nd 7209  𝑚 cmap 7899  cc 9972  cr 9973  0cc0 9974  1c1 9975   + caddc 9977   < clt 10112  cle 10113  cmin 10304  cn 11058  0cn0 11330  cz 11415  cuz 11725  ...cfz 12364  ..^cfzo 12504
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365  df-fzo 12505
This theorem is referenced by:  poimirlem27  33566
  Copyright terms: Public domain W3C validator