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 33100
Description: Lemma for poimir 33109, 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 1840 . . . . . . . . 9 𝑗(𝜑𝑦 ∈ (0...(𝑁 − 1)))
2 nfcsb1v 3534 . . . . . . . . . 10 𝑗𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))
3 nfcv 2761 . . . . . . . . . 10 𝑗(1...𝑁)
4 nfcv 2761 . . . . . . . . . 10 𝑗(0...𝐾)
52, 3, 4nff 6003 . . . . . . . . 9 𝑗𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)
61, 5nfim 1822 . . . . . . . 8 𝑗((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
7 eleq1 2686 . . . . . . . . . 10 (𝑗 = 𝑦 → (𝑗 ∈ (0...(𝑁 − 1)) ↔ 𝑦 ∈ (0...(𝑁 − 1))))
87anbi2d 739 . . . . . . . . 9 (𝑗 = 𝑦 → ((𝜑𝑗 ∈ (0...(𝑁 − 1))) ↔ (𝜑𝑦 ∈ (0...(𝑁 − 1)))))
9 csbeq1a 3527 . . . . . . . . . 10 (𝑗 = 𝑦 → (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = 𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
109feq1d 5992 . . . . . . . . 9 (𝑗 = 𝑦 → ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) ↔ 𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))
118, 10imbi12d 334 . . . . . . . 8 (𝑗 = 𝑦 → (((𝜑𝑗 ∈ (0...(𝑁 − 1))) → (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) ↔ ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))))
12 poimir.0 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℕ)
1312nncnd 10988 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℂ)
14 npcan1 10407 . . . . . . . . . . . . 13 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
1513, 14syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
1612nnzd 11433 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
17 peano2zm 11372 . . . . . . . . . . . . . 14 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
1816, 17syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑁 − 1) ∈ ℤ)
19 uzid 11654 . . . . . . . . . . . . 13 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
20 peano2uz 11693 . . . . . . . . . . . . 13 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
2118, 19, 203syl 18 . . . . . . . . . . . 12 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
2215, 21eqeltrrd 2699 . . . . . . . . . . 11 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
23 fzss2 12331 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (0...(𝑁 − 1)) ⊆ (0...𝑁))
2422, 23syl 17 . . . . . . . . . 10 (𝜑 → (0...(𝑁 − 1)) ⊆ (0...𝑁))
2524sselda 3587 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → 𝑗 ∈ (0...𝑁))
26 elun 3736 . . . . . . . . . . . . 13 (𝑦 ∈ ({1} ∪ {0}) ↔ (𝑦 ∈ {1} ∨ 𝑦 ∈ {0}))
27 fzofzp1 12514 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0..^𝐾) → (𝑥 + 1) ∈ (0...𝐾))
28 elsni 4170 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {1} → 𝑦 = 1)
2928oveq2d 6626 . . . . . . . . . . . . . . . 16 (𝑦 ∈ {1} → (𝑥 + 𝑦) = (𝑥 + 1))
3029eleq1d 2683 . . . . . . . . . . . . . . 15 (𝑦 ∈ {1} → ((𝑥 + 𝑦) ∈ (0...𝐾) ↔ (𝑥 + 1) ∈ (0...𝐾)))
3127, 30syl5ibrcom 237 . . . . . . . . . . . . . 14 (𝑥 ∈ (0..^𝐾) → (𝑦 ∈ {1} → (𝑥 + 𝑦) ∈ (0...𝐾)))
32 elfzoelz 12419 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (0..^𝐾) → 𝑥 ∈ ℤ)
3332zcnd 11435 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (0..^𝐾) → 𝑥 ∈ ℂ)
3433addid1d 10188 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (0..^𝐾) → (𝑥 + 0) = 𝑥)
35 elfzofz 12434 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (0..^𝐾) → 𝑥 ∈ (0...𝐾))
3634, 35eqeltrd 2698 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0..^𝐾) → (𝑥 + 0) ∈ (0...𝐾))
37 elsni 4170 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {0} → 𝑦 = 0)
3837oveq2d 6626 . . . . . . . . . . . . . . . 16 (𝑦 ∈ {0} → (𝑥 + 𝑦) = (𝑥 + 0))
3938eleq1d 2683 . . . . . . . . . . . . . . 15 (𝑦 ∈ {0} → ((𝑥 + 𝑦) ∈ (0...𝐾) ↔ (𝑥 + 0) ∈ (0...𝐾)))
4036, 39syl5ibrcom 237 . . . . . . . . . . . . . 14 (𝑥 ∈ (0..^𝐾) → (𝑦 ∈ {0} → (𝑥 + 𝑦) ∈ (0...𝐾)))
4131, 40jaod 395 . . . . . . . . . . . . 13 (𝑥 ∈ (0..^𝐾) → ((𝑦 ∈ {1} ∨ 𝑦 ∈ {0}) → (𝑥 + 𝑦) ∈ (0...𝐾)))
4226, 41syl5bi 232 . . . . . . . . . . . 12 (𝑥 ∈ (0..^𝐾) → (𝑦 ∈ ({1} ∪ {0}) → (𝑥 + 𝑦) ∈ (0...𝐾)))
4342imp 445 . . . . . . . . . . 11 ((𝑥 ∈ (0..^𝐾) ∧ 𝑦 ∈ ({1} ∪ {0})) → (𝑥 + 𝑦) ∈ (0...𝐾))
4443adantl 482 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ (0..^𝐾) ∧ 𝑦 ∈ ({1} ∪ {0}))) → (𝑥 + 𝑦) ∈ (0...𝐾))
45 poimirlem25.3 . . . . . . . . . . 11 (𝜑𝑇:(1...𝑁)⟶(0..^𝐾))
4645adantr 481 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇:(1...𝑁)⟶(0..^𝐾))
47 1ex 9987 . . . . . . . . . . . . . 14 1 ∈ V
4847fconst 6053 . . . . . . . . . . . . 13 ((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1}
49 c0ex 9986 . . . . . . . . . . . . . 14 0 ∈ V
5049fconst 6053 . . . . . . . . . . . . 13 ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}
5148, 50pm3.2i 471 . . . . . . . . . . . 12 (((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0})
52 poimirlem25.4 . . . . . . . . . . . . . 14 (𝜑𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
53 dff1o3 6105 . . . . . . . . . . . . . . 15 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun 𝑈))
5453simprbi 480 . . . . . . . . . . . . . 14 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun 𝑈)
55 imain 5937 . . . . . . . . . . . . . 14 (Fun 𝑈 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))))
5652, 54, 553syl 18 . . . . . . . . . . . . 13 (𝜑 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))))
57 elfznn0 12382 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ0)
5857nn0red 11304 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
5958ltp1d 10906 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1))
60 fzdisj 12318 . . . . . . . . . . . . . . . 16 (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
6159, 60syl 17 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
6261imaeq2d 5430 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (𝑈 “ ∅))
63 ima0 5445 . . . . . . . . . . . . . 14 (𝑈 “ ∅) = ∅
6462, 63syl6eq 2671 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
6556, 64sylan9req 2676 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
66 fun 6028 . . . . . . . . . . . 12 (((((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}) ∧ ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
6751, 65, 66sylancr 694 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
68 nn0p1nn 11284 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
6957, 68syl 17 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ)
70 nnuz 11675 . . . . . . . . . . . . . . . . 17 ℕ = (ℤ‘1)
7169, 70syl6eleq 2708 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (ℤ‘1))
72 elfzuz3 12289 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ𝑗))
73 fzsplit2 12316 . . . . . . . . . . . . . . . 16 (((𝑗 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
7471, 72, 73syl2anc 692 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
7574imaeq2d 5430 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑁) → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))))
76 imaundi 5509 . . . . . . . . . . . . . 14 (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))
7775, 76syl6req 2672 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑁) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (𝑈 “ (1...𝑁)))
78 f1ofo 6106 . . . . . . . . . . . . . 14 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁))
79 foima 6082 . . . . . . . . . . . . . 14 (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁))
8052, 78, 793syl 18 . . . . . . . . . . . . 13 (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁))
8177, 80sylan9eqr 2677 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (1...𝑁))
8281feq2d 5993 . . . . . . . . . . 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 6638 . . . . . . . . . . 11 (1...𝑁) ∈ V
8584a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ V)
86 inidm 3805 . . . . . . . . . 10 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
8744, 46, 83, 85, 85, 86off 6872 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
8825, 87syldan 487 . . . . . . . 8 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
896, 11, 88chvar 2261 . . . . . . 7 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
90 fzp1elp1 12344 . . . . . . . . 9 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ (0...((𝑁 − 1) + 1)))
9115oveq2d 6626 . . . . . . . . . . 11 (𝜑 → (0...((𝑁 − 1) + 1)) = (0...𝑁))
9291eleq2d 2684 . . . . . . . . . 10 (𝜑 → ((𝑦 + 1) ∈ (0...((𝑁 − 1) + 1)) ↔ (𝑦 + 1) ∈ (0...𝑁)))
9392biimpa 501 . . . . . . . . 9 ((𝜑 ∧ (𝑦 + 1) ∈ (0...((𝑁 − 1) + 1))) → (𝑦 + 1) ∈ (0...𝑁))
9490, 93sylan2 491 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 + 1) ∈ (0...𝑁))
95 nfv 1840 . . . . . . . . . 10 𝑗(𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁))
96 nfcsb1v 3534 . . . . . . . . . . 11 𝑗(𝑦 + 1) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))
9796, 3, 4nff 6003 . . . . . . . . . 10 𝑗(𝑦 + 1) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)
9895, 97nfim 1822 . . . . . . . . 9 𝑗((𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁)) → (𝑦 + 1) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
99 ovex 6638 . . . . . . . . 9 (𝑦 + 1) ∈ V
100 eleq1 2686 . . . . . . . . . . 11 (𝑗 = (𝑦 + 1) → (𝑗 ∈ (0...𝑁) ↔ (𝑦 + 1) ∈ (0...𝑁)))
101100anbi2d 739 . . . . . . . . . 10 (𝑗 = (𝑦 + 1) → ((𝜑𝑗 ∈ (0...𝑁)) ↔ (𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁))))
102 csbeq1a 3527 . . . . . . . . . . 11 (𝑗 = (𝑦 + 1) → (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑦 + 1) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
103102feq1d 5992 . . . . . . . . . 10 (𝑗 = (𝑦 + 1) → ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) ↔ (𝑦 + 1) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))
104101, 103imbi12d 334 . . . . . . . . 9 (𝑗 = (𝑦 + 1) → (((𝜑𝑗 ∈ (0...𝑁)) → (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) ↔ ((𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁)) → (𝑦 + 1) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))))
10598, 99, 104, 87vtoclf 3247 . . . . . . . 8 ((𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁)) → (𝑦 + 1) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
10694, 105syldan 487 . . . . . . 7 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 + 1) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
107 csbeq1 3521 . . . . . . . . 9 (𝑦 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → 𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
108107feq1d 5992 . . . . . . . 8 (𝑦 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → (𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) ↔ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))
109 csbeq1 3521 . . . . . . . . 9 ((𝑦 + 1) = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → (𝑦 + 1) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
110109feq1d 5992 . . . . . . . 8 ((𝑦 + 1) = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → ((𝑦 + 1) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) ↔ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))
111108, 110ifboth 4101 . . . . . . 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 692 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
113 ovex 6638 . . . . . . 7 (0...𝐾) ∈ V
114113, 84elmap 7838 . . . . . 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 2621 . . . . 5 (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
117115, 116fmptd 6346 . . . 4 (𝜑 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))):(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))
118 ovex 6638 . . . . 5 ((0...𝐾) ↑𝑚 (1...𝑁)) ∈ V
119 ovex 6638 . . . . 5 (0...(𝑁 − 1)) ∈ V
120118, 119elmap 7838 . . . 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 5316 . . . . . . . 8 (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → ran 𝑥 = ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))
123122mpteq1d 4703 . . . . . . 7 (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → (𝑝 ∈ ran 𝑥𝐵) = (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵))
124123rneqd 5318 . . . . . 6 (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → ran (𝑝 ∈ ran 𝑥𝐵) = ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵))
125124sseq2d 3617 . . . . 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 3137 . . . . 5 (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → (∃𝑝 ∈ ran 𝑥(𝑝𝑁) ≠ 0 ↔ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0))
127125, 126anbi12d 746 . . . 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 3323 . . 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 3577 . . . 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 6638 . . . . . . . . . . . . 13 ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
132 poimirlem28.1 . . . . . . . . . . . . 13 (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶)
133131, 132csbie 3544 . . . . . . . . . . . 12 ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵 = 𝐶
134133csbeq2i 3970 . . . . . . . . . . 11 𝑇, 𝑈⟩ / 𝑠((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵 = 𝑇, 𝑈⟩ / 𝑠𝐶
135 opex 4898 . . . . . . . . . . . . 13 𝑇, 𝑈⟩ ∈ V
136135a1i 11 . . . . . . . . . . . 12 (𝜑 → ⟨𝑇, 𝑈⟩ ∈ V)
137 fveq2 6153 . . . . . . . . . . . . . . 15 (𝑠 = ⟨𝑇, 𝑈⟩ → (1st𝑠) = (1st ‘⟨𝑇, 𝑈⟩))
138 fex 6450 . . . . . . . . . . . . . . . . 17 ((𝑇:(1...𝑁)⟶(0..^𝐾) ∧ (1...𝑁) ∈ V) → 𝑇 ∈ V)
13945, 84, 138sylancl 693 . . . . . . . . . . . . . . . 16 (𝜑𝑇 ∈ V)
140 f1oexrnex 7069 . . . . . . . . . . . . . . . . 17 ((𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ∧ (1...𝑁) ∈ V) → 𝑈 ∈ V)
14152, 84, 140sylancl 693 . . . . . . . . . . . . . . . 16 (𝜑𝑈 ∈ V)
142 op1stg 7132 . . . . . . . . . . . . . . . 16 ((𝑇 ∈ V ∧ 𝑈 ∈ V) → (1st ‘⟨𝑇, 𝑈⟩) = 𝑇)
143139, 141, 142syl2anc 692 . . . . . . . . . . . . . . 15 (𝜑 → (1st ‘⟨𝑇, 𝑈⟩) = 𝑇)
144137, 143sylan9eqr 2677 . . . . . . . . . . . . . 14 ((𝜑𝑠 = ⟨𝑇, 𝑈⟩) → (1st𝑠) = 𝑇)
145 fveq2 6153 . . . . . . . . . . . . . . . 16 (𝑠 = ⟨𝑇, 𝑈⟩ → (2nd𝑠) = (2nd ‘⟨𝑇, 𝑈⟩))
146 op2ndg 7133 . . . . . . . . . . . . . . . . 17 ((𝑇 ∈ V ∧ 𝑈 ∈ V) → (2nd ‘⟨𝑇, 𝑈⟩) = 𝑈)
147139, 141, 146syl2anc 692 . . . . . . . . . . . . . . . 16 (𝜑 → (2nd ‘⟨𝑇, 𝑈⟩) = 𝑈)
148145, 147sylan9eqr 2677 . . . . . . . . . . . . . . 15 ((𝜑𝑠 = ⟨𝑇, 𝑈⟩) → (2nd𝑠) = 𝑈)
149 imaeq1 5425 . . . . . . . . . . . . . . . . 17 ((2nd𝑠) = 𝑈 → ((2nd𝑠) “ (1...𝑗)) = (𝑈 “ (1...𝑗)))
150149xpeq1d 5103 . . . . . . . . . . . . . . . 16 ((2nd𝑠) = 𝑈 → (((2nd𝑠) “ (1...𝑗)) × {1}) = ((𝑈 “ (1...𝑗)) × {1}))
151 imaeq1 5425 . . . . . . . . . . . . . . . . 17 ((2nd𝑠) = 𝑈 → ((2nd𝑠) “ ((𝑗 + 1)...𝑁)) = (𝑈 “ ((𝑗 + 1)...𝑁)))
152151xpeq1d 5103 . . . . . . . . . . . . . . . 16 ((2nd𝑠) = 𝑈 → (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))
153150, 152uneq12d 3751 . . . . . . . . . . . . . . 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 6628 . . . . . . . . . . . . 13 ((𝜑𝑠 = ⟨𝑇, 𝑈⟩) → ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
156155csbeq1d 3525 . . . . . . . . . . . 12 ((𝜑𝑠 = ⟨𝑇, 𝑈⟩) → ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵 = (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
157136, 156csbied 3545 . . . . . . . . . . 11 (𝜑𝑇, 𝑈⟩ / 𝑠((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵 = (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
158134, 157syl5eqr 2669 . . . . . . . . . 10 (𝜑𝑇, 𝑈⟩ / 𝑠𝐶 = (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
159158csbeq2dv 3969 . . . . . . . . 9 (𝜑if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
160159eqeq2d 2631 . . . . . . . 8 (𝜑 → (𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵))
161160rexbidv 3046 . . . . . . 7 (𝜑 → (∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵))
162 vex 3192 . . . . . . . . 9 𝑖 ∈ V
163 eqid 2621 . . . . . . . . . 10 (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) = (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵)
164163elrnmpt 5337 . . . . . . . . 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 1840 . . . . . . . . 9 𝑘 𝑖 = 𝐵
167 nfcsb1v 3534 . . . . . . . . . 10 𝑝𝑘 / 𝑝𝐵
168167nfeq2 2776 . . . . . . . . 9 𝑝 𝑖 = 𝑘 / 𝑝𝐵
169 csbeq1a 3527 . . . . . . . . . 10 (𝑝 = 𝑘𝐵 = 𝑘 / 𝑝𝐵)
170169eqeq2d 2631 . . . . . . . . 9 (𝑝 = 𝑘 → (𝑖 = 𝐵𝑖 = 𝑘 / 𝑝𝐵))
171166, 168, 170cbvrex 3159 . . . . . . . 8 (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))𝑖 = 𝐵 ↔ ∃𝑘 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))𝑖 = 𝑘 / 𝑝𝐵)
172 ovex 6638 . . . . . . . . . . 11 (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
173172csbex 4758 . . . . . . . . . 10 if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
174173rgenw 2919 . . . . . . . . 9 𝑦 ∈ (0...(𝑁 − 1))if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
175 csbeq1 3521 . . . . . . . . . . . 12 (𝑘 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝑘 / 𝑝𝐵 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
176 vex 3192 . . . . . . . . . . . . . 14 𝑦 ∈ V
177176, 99ifex 4133 . . . . . . . . . . . . 13 if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) ∈ V
178 csbnestg 3975 . . . . . . . . . . . . 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 2673 . . . . . . . . . . 11 (𝑘 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝑘 / 𝑝𝐵 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
181180eqeq2d 2631 . . . . . . . . . 10 (𝑘 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑖 = 𝑘 / 𝑝𝐵𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵))
182116, 181rexrnmpt 6330 . . . . . . . . 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 3587 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ (0...𝑁))
187186adantr 481 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < 𝑉) → 𝑦 ∈ (0...𝑁))
188 elfzelz 12292 . . . . . . . . . . . . . 14 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℤ)
189188zred 11434 . . . . . . . . . . . . 13 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ)
190189adantl 482 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ ℝ)
191 ltne 10086 . . . . . . . . . . . . 13 ((𝑦 ∈ ℝ ∧ 𝑦 < 𝑉) → 𝑉𝑦)
192191necomd 2845 . . . . . . . . . . . 12 ((𝑦 ∈ ℝ ∧ 𝑦 < 𝑉) → 𝑦𝑉)
193190, 192sylan 488 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < 𝑉) → 𝑦𝑉)
194 eldifsn 4292 . . . . . . . . . . 11 (𝑦 ∈ ((0...𝑁) ∖ {𝑉}) ↔ (𝑦 ∈ (0...𝑁) ∧ 𝑦𝑉))
195187, 193, 194sylanbrc 697 . . . . . . . . . 10 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < 𝑉) → 𝑦 ∈ ((0...𝑁) ∖ {𝑉}))
19694adantr 481 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → (𝑦 + 1) ∈ (0...𝑁))
197 poimirlem24.5 . . . . . . . . . . . . . . 15 (𝜑𝑉 ∈ (0...𝑁))
198 elfzelz 12292 . . . . . . . . . . . . . . 15 (𝑉 ∈ (0...𝑁) → 𝑉 ∈ ℤ)
199197, 198syl 17 . . . . . . . . . . . . . 14 (𝜑𝑉 ∈ ℤ)
200199zred 11434 . . . . . . . . . . . . 13 (𝜑𝑉 ∈ ℝ)
201200ad2antrr 761 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → 𝑉 ∈ ℝ)
202 zre 11333 . . . . . . . . . . . . . . . 16 (𝑉 ∈ ℤ → 𝑉 ∈ ℝ)
203 zre 11333 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℤ → 𝑦 ∈ ℝ)
204 lenlt 10068 . . . . . . . . . . . . . . . 16 ((𝑉 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑉𝑦 ↔ ¬ 𝑦 < 𝑉))
205202, 203, 204syl2an 494 . . . . . . . . . . . . . . 15 ((𝑉 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑉𝑦 ↔ ¬ 𝑦 < 𝑉))
206 zleltp1 11380 . . . . . . . . . . . . . . 15 ((𝑉 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑉𝑦𝑉 < (𝑦 + 1)))
207205, 206bitr3d 270 . . . . . . . . . . . . . 14 ((𝑉 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (¬ 𝑦 < 𝑉𝑉 < (𝑦 + 1)))
208199, 188, 207syl2an 494 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (¬ 𝑦 < 𝑉𝑉 < (𝑦 + 1)))
209208biimpa 501 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → 𝑉 < (𝑦 + 1))
210201, 209gtned 10124 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → (𝑦 + 1) ≠ 𝑉)
211 eldifsn 4292 . . . . . . . . . . 11 ((𝑦 + 1) ∈ ((0...𝑁) ∖ {𝑉}) ↔ ((𝑦 + 1) ∈ (0...𝑁) ∧ (𝑦 + 1) ≠ 𝑉))
212196, 210, 211sylanbrc 697 . . . . . . . . . 10 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → (𝑦 + 1) ∈ ((0...𝑁) ∖ {𝑉}))
213195, 212ifclda 4097 . . . . . . . . 9 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) ∈ ((0...𝑁) ∖ {𝑉}))
214 nfcsb1v 3534 . . . . . . . . . . . 12 𝑗if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
215214nfeq2 2776 . . . . . . . . . . 11 𝑗 𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
216 csbeq1a 3527 . . . . . . . . . . . 12 (𝑗 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → 𝑇, 𝑈⟩ / 𝑠𝐶 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
217216eqeq2d 2631 . . . . . . . . . . 11 (𝑗 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
218215, 217rspce 3293 . . . . . . . . . 10 ((if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) ∈ ((0...𝑁) ∖ {𝑉}) ∧ 𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
219218ex 450 . . . . . . . . 9 (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) ∈ ((0...𝑁) ∖ {𝑉}) → (𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
220213, 219syl 17 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
221220rexlimdva 3025 . . . . . . 7 (𝜑 → (∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
222 nfv 1840 . . . . . . . 8 𝑗𝜑
223 nfcv 2761 . . . . . . . . 9 𝑗(0...(𝑁 − 1))
224223, 215nfrex 3002 . . . . . . . 8 𝑗𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
225 eldifi 3715 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ (0...𝑁))
226225, 57syl 17 . . . . . . . . . . . . . 14 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ ℕ0)
227226nn0ge0d 11306 . . . . . . . . . . . . 13 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 0 ≤ 𝑗)
228227ad2antlr 762 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 0 ≤ 𝑗)
229226nn0red 11304 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ ℝ)
230229ad2antlr 762 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 ∈ ℝ)
231200ad2antrr 761 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑉 ∈ ℝ)
23216zred 11434 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℝ)
233232ad2antrr 761 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑁 ∈ ℝ)
234 simpr 477 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 < 𝑉)
235 elfzle2 12295 . . . . . . . . . . . . . . . 16 (𝑉 ∈ (0...𝑁) → 𝑉𝑁)
236197, 235syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑉𝑁)
237236ad2antrr 761 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑉𝑁)
238230, 231, 233, 234, 237ltletrd 10149 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 < 𝑁)
239226nn0zd 11432 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ ℤ)
240 zltlem1 11382 . . . . . . . . . . . . . . 15 ((𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 < 𝑁𝑗 ≤ (𝑁 − 1)))
241239, 16, 240syl2anr 495 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗 < 𝑁𝑗 ≤ (𝑁 − 1)))
242241adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → (𝑗 < 𝑁𝑗 ≤ (𝑁 − 1)))
243238, 242mpbid 222 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 ≤ (𝑁 − 1))
244 0z 11340 . . . . . . . . . . . . . . 15 0 ∈ ℤ
245 elfz 12282 . . . . . . . . . . . . . . 15 ((𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑗 ∈ (0...(𝑁 − 1)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝑁 − 1))))
246244, 245mp3an2 1409 . . . . . . . . . . . . . 14 ((𝑗 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑗 ∈ (0...(𝑁 − 1)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝑁 − 1))))
247239, 18, 246syl2anr 495 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗 ∈ (0...(𝑁 − 1)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝑁 − 1))))
248247adantr 481 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → (𝑗 ∈ (0...(𝑁 − 1)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝑁 − 1))))
249228, 243, 248mpbir2and 956 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 ∈ (0...(𝑁 − 1)))
250 0red 9993 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 0 ∈ ℝ)
251200ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑉 ∈ ℝ)
252229ad2antlr 762 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗 ∈ ℝ)
253 elfzle1 12294 . . . . . . . . . . . . . . . . 17 (𝑉 ∈ (0...𝑁) → 0 ≤ 𝑉)
254197, 253syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ 𝑉)
255254ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 0 ≤ 𝑉)
256 lenlt 10068 . . . . . . . . . . . . . . . . . 18 ((𝑉 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑉𝑗 ↔ ¬ 𝑗 < 𝑉))
257200, 229, 256syl2an 494 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑉𝑗 ↔ ¬ 𝑗 < 𝑉))
258257biimpar 502 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑉𝑗)
259 eldifsni 4294 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗𝑉)
260259ad2antlr 762 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗𝑉)
261 ltlen 10090 . . . . . . . . . . . . . . . . . 18 ((𝑉 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑉 < 𝑗 ↔ (𝑉𝑗𝑗𝑉)))
262200, 229, 261syl2an 494 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑉 < 𝑗 ↔ (𝑉𝑗𝑗𝑉)))
263262adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → (𝑉 < 𝑗 ↔ (𝑉𝑗𝑗𝑉)))
264258, 260, 263mpbir2and 956 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑉 < 𝑗)
265250, 251, 252, 255, 264lelttrd 10147 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 0 < 𝑗)
266 zgt0ge1 11383 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℤ → (0 < 𝑗 ↔ 1 ≤ 𝑗))
267239, 266syl 17 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → (0 < 𝑗 ↔ 1 ≤ 𝑗))
268267ad2antlr 762 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → (0 < 𝑗 ↔ 1 ≤ 𝑗))
269265, 268mpbid 222 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 1 ≤ 𝑗)
270 elfzle2 12295 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑁) → 𝑗𝑁)
271225, 270syl 17 . . . . . . . . . . . . . 14 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗𝑁)
272271ad2antlr 762 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗𝑁)
273 1z 11359 . . . . . . . . . . . . . . . 16 1 ∈ ℤ
274 elfz 12282 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 ∈ (1...𝑁) ↔ (1 ≤ 𝑗𝑗𝑁)))
275273, 274mp3an2 1409 . . . . . . . . . . . . . . 15 ((𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 ∈ (1...𝑁) ↔ (1 ≤ 𝑗𝑗𝑁)))
276239, 16, 275syl2anr 495 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗 ∈ (1...𝑁) ↔ (1 ≤ 𝑗𝑗𝑁)))
277276adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → (𝑗 ∈ (1...𝑁) ↔ (1 ≤ 𝑗𝑗𝑁)))
278269, 272, 277mpbir2and 956 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗 ∈ (1...𝑁))
279 elfzmlbm 12398 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑁) → (𝑗 − 1) ∈ (0...(𝑁 − 1)))
280278, 279syl 17 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → (𝑗 − 1) ∈ (0...(𝑁 − 1)))
281249, 280ifclda 4097 . . . . . . . . . 10 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) ∈ (0...(𝑁 − 1)))
282 breq1 4621 . . . . . . . . . . . . . . . 16 (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 < 𝑉 ↔ if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉))
283 id 22 . . . . . . . . . . . . . . . 16 (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → 𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)))
284 oveq1 6617 . . . . . . . . . . . . . . . 16 (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 + 1) = (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))
285282, 283, 284ifbieq12d 4090 . . . . . . . . . . . . . . 15 (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)) = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)))
286285eqeq2d 2631 . . . . . . . . . . . . . 14 (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)) ↔ 𝑗 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))))
287 breq1 4621 . . . . . . . . . . . . . . . 16 ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → ((𝑗 − 1) < 𝑉 ↔ if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉))
288 id 22 . . . . . . . . . . . . . . . 16 ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)))
289 oveq1 6617 . . . . . . . . . . . . . . . 16 ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → ((𝑗 − 1) + 1) = (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))
290287, 288, 289ifbieq12d 4090 . . . . . . . . . . . . . . 15 ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → if((𝑗 − 1) < 𝑉, (𝑗 − 1), ((𝑗 − 1) + 1)) = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)))
291290eqeq2d 2631 . . . . . . . . . . . . . 14 ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 = if((𝑗 − 1) < 𝑉, (𝑗 − 1), ((𝑗 − 1) + 1)) ↔ 𝑗 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))))
292 iftrue 4069 . . . . . . . . . . . . . . . 16 (𝑗 < 𝑉 → if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)) = 𝑗)
293292eqcomd 2627 . . . . . . . . . . . . . . 15 (𝑗 < 𝑉𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)))
294293adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)))
295 zlem1lt 11381 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ℤ ∧ 𝑉 ∈ ℤ) → (𝑗𝑉 ↔ (𝑗 − 1) < 𝑉))
296239, 199, 295syl2anr 495 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗𝑉 ↔ (𝑗 − 1) < 𝑉))
297259necomd 2845 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑉𝑗)
298297adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → 𝑉𝑗)
299 ltlen 10090 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑗 < 𝑉 ↔ (𝑗𝑉𝑉𝑗)))
300229, 200, 299syl2anr 495 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗 < 𝑉 ↔ (𝑗𝑉𝑉𝑗)))
301300biimprd 238 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → ((𝑗𝑉𝑉𝑗) → 𝑗 < 𝑉))
302298, 301mpan2d 709 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗𝑉𝑗 < 𝑉))
303296, 302sylbird 250 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → ((𝑗 − 1) < 𝑉𝑗 < 𝑉))
304303con3dimp 457 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → ¬ (𝑗 − 1) < 𝑉)
305304iffalsed 4074 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → if((𝑗 − 1) < 𝑉, (𝑗 − 1), ((𝑗 − 1) + 1)) = ((𝑗 − 1) + 1))
306226nn0cnd 11305 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ ℂ)
307 npcan1 10407 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℂ → ((𝑗 − 1) + 1) = 𝑗)
308306, 307syl 17 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → ((𝑗 − 1) + 1) = 𝑗)
309308ad2antlr 762 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → ((𝑗 − 1) + 1) = 𝑗)
310305, 309eqtr2d 2656 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗 = if((𝑗 − 1) < 𝑉, (𝑗 − 1), ((𝑗 − 1) + 1)))
311286, 291, 294, 310ifbothda 4100 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → 𝑗 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)))
312 csbeq1a 3527 . . . . . . . . . . . . 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 2631 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
315314biimpd 219 . . . . . . . . . 10 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
316 breq1 4621 . . . . . . . . . . . . . 14 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑦 < 𝑉 ↔ if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉))
317 id 22 . . . . . . . . . . . . . 14 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → 𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)))
318 oveq1 6617 . . . . . . . . . . . . . 14 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑦 + 1) = (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))
319316, 317, 318ifbieq12d 4090 . . . . . . . . . . . . 13 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)))
320319csbeq1d 3525 . . . . . . . . . . . 12 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
321320eqeq2d 2631 . . . . . . . . . . 11 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
322321rspcev 3298 . . . . . . . . . 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 450 . . . . . . . 8 (𝜑 → (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)))
325222, 224, 324rexlimd 3020 . . . . . . 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 2981 . . . 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 740 . 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 33099 . . 3 (𝜑 → (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁))))
332331anbi2d 739 . 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 383  wa 384   = wceq 1480  wcel 1987  wne 2790  wral 2907  wrex 2908  Vcvv 3189  csb 3518  cdif 3556  cun 3557  cin 3558  wss 3559  c0 3896  ifcif 4063  {csn 4153  cop 4159   class class class wbr 4618  cmpt 4678   × cxp 5077  ccnv 5078  ran crn 5080  cima 5082  Fun wfun 5846  wf 5848  ontowfo 5850  1-1-ontowf1o 5851  cfv 5852  (class class class)co 6610  𝑓 cof 6855  1st c1st 7118  2nd c2nd 7119  𝑚 cmap 7809  cc 9886  cr 9887  0cc0 9888  1c1 9889   + caddc 9891   < clt 10026  cle 10027  cmin 10218  cn 10972  0cn0 11244  cz 11329  cuz 11639  ...cfz 12276  ..^cfzo 12414
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 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-cnex 9944  ax-resscn 9945  ax-1cn 9946  ax-icn 9947  ax-addcl 9948  ax-addrcl 9949  ax-mulcl 9950  ax-mulrcl 9951  ax-mulcom 9952  ax-addass 9953  ax-mulass 9954  ax-distr 9955  ax-i2m1 9956  ax-1ne0 9957  ax-1rid 9958  ax-rnegex 9959  ax-rrecex 9960  ax-cnre 9961  ax-pre-lttri 9962  ax-pre-lttrn 9963  ax-pre-ltadd 9964  ax-pre-mulgt0 9965
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  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 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-of 6857  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-er 7694  df-map 7811  df-en 7908  df-dom 7909  df-sdom 7910  df-pnf 10028  df-mnf 10029  df-xr 10030  df-ltxr 10031  df-le 10032  df-sub 10220  df-neg 10221  df-nn 10973  df-n0 11245  df-z 11330  df-uz 11640  df-fz 12277  df-fzo 12415
This theorem is referenced by:  poimirlem27  33103
  Copyright terms: Public domain W3C validator