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 35081
Description: Lemma for poimir 35090, 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𝑠) ∘f + ((((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...𝐾) ↑m (1...𝑁)) ↑m (0...(𝑁 − 1)))(𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (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 1915 . . . . . . . . 9 𝑗(𝜑𝑦 ∈ (0...(𝑁 − 1)))
2 nfcsb1v 3852 . . . . . . . . . 10 𝑗𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))
3 nfcv 2955 . . . . . . . . . 10 𝑗(1...𝑁)
4 nfcv 2955 . . . . . . . . . 10 𝑗(0...𝐾)
52, 3, 4nff 6483 . . . . . . . . 9 𝑗𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)
61, 5nfim 1897 . . . . . . . 8 𝑗((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
7 eleq1 2877 . . . . . . . . . 10 (𝑗 = 𝑦 → (𝑗 ∈ (0...(𝑁 − 1)) ↔ 𝑦 ∈ (0...(𝑁 − 1))))
87anbi2d 631 . . . . . . . . 9 (𝑗 = 𝑦 → ((𝜑𝑗 ∈ (0...(𝑁 − 1))) ↔ (𝜑𝑦 ∈ (0...(𝑁 − 1)))))
9 csbeq1a 3842 . . . . . . . . . 10 (𝑗 = 𝑦 → (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = 𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
109feq1d 6472 . . . . . . . . 9 (𝑗 = 𝑦 → ((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) ↔ 𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))
118, 10imbi12d 348 . . . . . . . 8 (𝑗 = 𝑦 → (((𝜑𝑗 ∈ (0...(𝑁 − 1))) → (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) ↔ ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))))
12 poimir.0 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℕ)
1312nncnd 11641 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℂ)
14 npcan1 11054 . . . . . . . . . . . . 13 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
1513, 14syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
1612nnzd 12074 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
17 peano2zm 12013 . . . . . . . . . . . . . 14 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
1816, 17syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑁 − 1) ∈ ℤ)
19 uzid 12246 . . . . . . . . . . . . 13 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
20 peano2uz 12289 . . . . . . . . . . . . 13 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
2118, 19, 203syl 18 . . . . . . . . . . . 12 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
2215, 21eqeltrrd 2891 . . . . . . . . . . 11 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
23 fzss2 12942 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (0...(𝑁 − 1)) ⊆ (0...𝑁))
2422, 23syl 17 . . . . . . . . . 10 (𝜑 → (0...(𝑁 − 1)) ⊆ (0...𝑁))
2524sselda 3915 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → 𝑗 ∈ (0...𝑁))
26 elun 4076 . . . . . . . . . . . . 13 (𝑦 ∈ ({1} ∪ {0}) ↔ (𝑦 ∈ {1} ∨ 𝑦 ∈ {0}))
27 fzofzp1 13129 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0..^𝐾) → (𝑥 + 1) ∈ (0...𝐾))
28 elsni 4542 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {1} → 𝑦 = 1)
2928oveq2d 7151 . . . . . . . . . . . . . . . 16 (𝑦 ∈ {1} → (𝑥 + 𝑦) = (𝑥 + 1))
3029eleq1d 2874 . . . . . . . . . . . . . . 15 (𝑦 ∈ {1} → ((𝑥 + 𝑦) ∈ (0...𝐾) ↔ (𝑥 + 1) ∈ (0...𝐾)))
3127, 30syl5ibrcom 250 . . . . . . . . . . . . . 14 (𝑥 ∈ (0..^𝐾) → (𝑦 ∈ {1} → (𝑥 + 𝑦) ∈ (0...𝐾)))
32 elfzoelz 13033 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (0..^𝐾) → 𝑥 ∈ ℤ)
3332zcnd 12076 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (0..^𝐾) → 𝑥 ∈ ℂ)
3433addid1d 10829 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (0..^𝐾) → (𝑥 + 0) = 𝑥)
35 elfzofz 13048 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (0..^𝐾) → 𝑥 ∈ (0...𝐾))
3634, 35eqeltrd 2890 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0..^𝐾) → (𝑥 + 0) ∈ (0...𝐾))
37 elsni 4542 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {0} → 𝑦 = 0)
3837oveq2d 7151 . . . . . . . . . . . . . . . 16 (𝑦 ∈ {0} → (𝑥 + 𝑦) = (𝑥 + 0))
3938eleq1d 2874 . . . . . . . . . . . . . . 15 (𝑦 ∈ {0} → ((𝑥 + 𝑦) ∈ (0...𝐾) ↔ (𝑥 + 0) ∈ (0...𝐾)))
4036, 39syl5ibrcom 250 . . . . . . . . . . . . . 14 (𝑥 ∈ (0..^𝐾) → (𝑦 ∈ {0} → (𝑥 + 𝑦) ∈ (0...𝐾)))
4131, 40jaod 856 . . . . . . . . . . . . 13 (𝑥 ∈ (0..^𝐾) → ((𝑦 ∈ {1} ∨ 𝑦 ∈ {0}) → (𝑥 + 𝑦) ∈ (0...𝐾)))
4226, 41syl5bi 245 . . . . . . . . . . . 12 (𝑥 ∈ (0..^𝐾) → (𝑦 ∈ ({1} ∪ {0}) → (𝑥 + 𝑦) ∈ (0...𝐾)))
4342imp 410 . . . . . . . . . . 11 ((𝑥 ∈ (0..^𝐾) ∧ 𝑦 ∈ ({1} ∪ {0})) → (𝑥 + 𝑦) ∈ (0...𝐾))
4443adantl 485 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ (0..^𝐾) ∧ 𝑦 ∈ ({1} ∪ {0}))) → (𝑥 + 𝑦) ∈ (0...𝐾))
45 poimirlem25.3 . . . . . . . . . . 11 (𝜑𝑇:(1...𝑁)⟶(0..^𝐾))
4645adantr 484 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇:(1...𝑁)⟶(0..^𝐾))
47 1ex 10626 . . . . . . . . . . . . . 14 1 ∈ V
4847fconst 6539 . . . . . . . . . . . . 13 ((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1}
49 c0ex 10624 . . . . . . . . . . . . . 14 0 ∈ V
5049fconst 6539 . . . . . . . . . . . . 13 ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}
5148, 50pm3.2i 474 . . . . . . . . . . . 12 (((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0})
52 poimirlem25.4 . . . . . . . . . . . . . 14 (𝜑𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
53 dff1o3 6596 . . . . . . . . . . . . . . 15 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun 𝑈))
5453simprbi 500 . . . . . . . . . . . . . 14 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun 𝑈)
55 imain 6409 . . . . . . . . . . . . . 14 (Fun 𝑈 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))))
5652, 54, 553syl 18 . . . . . . . . . . . . 13 (𝜑 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))))
57 elfznn0 12995 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ0)
5857nn0red 11944 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
5958ltp1d 11559 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1))
60 fzdisj 12929 . . . . . . . . . . . . . . . 16 (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
6159, 60syl 17 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
6261imaeq2d 5896 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (𝑈 “ ∅))
63 ima0 5912 . . . . . . . . . . . . . 14 (𝑈 “ ∅) = ∅
6462, 63eqtrdi 2849 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
6556, 64sylan9req 2854 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
66 fun 6514 . . . . . . . . . . . 12 (((((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}) ∧ ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
6751, 65, 66sylancr 590 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
68 nn0p1nn 11924 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
6957, 68syl 17 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ)
70 nnuz 12269 . . . . . . . . . . . . . . . . 17 ℕ = (ℤ‘1)
7169, 70eleqtrdi 2900 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (ℤ‘1))
72 elfzuz3 12899 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ𝑗))
73 fzsplit2 12927 . . . . . . . . . . . . . . . 16 (((𝑗 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
7471, 72, 73syl2anc 587 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
7574imaeq2d 5896 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑁) → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))))
76 imaundi 5975 . . . . . . . . . . . . . 14 (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))
7775, 76eqtr2di 2850 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑁) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (𝑈 “ (1...𝑁)))
78 f1ofo 6597 . . . . . . . . . . . . . 14 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁))
79 foima 6570 . . . . . . . . . . . . . 14 (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁))
8052, 78, 793syl 18 . . . . . . . . . . . . 13 (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁))
8177, 80sylan9eqr 2855 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (1...𝑁))
8281feq2d 6473 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}) ↔ (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0})))
8367, 82mpbid 235 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
84 ovex 7168 . . . . . . . . . . 11 (1...𝑁) ∈ V
8584a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ V)
86 inidm 4145 . . . . . . . . . 10 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
8744, 46, 83, 85, 85, 86off 7404 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
8825, 87syldan 594 . . . . . . . 8 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
896, 11, 88chvarfv 2240 . . . . . . 7 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
90 fzp1elp1 12955 . . . . . . . . 9 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ (0...((𝑁 − 1) + 1)))
9115oveq2d 7151 . . . . . . . . . . 11 (𝜑 → (0...((𝑁 − 1) + 1)) = (0...𝑁))
9291eleq2d 2875 . . . . . . . . . 10 (𝜑 → ((𝑦 + 1) ∈ (0...((𝑁 − 1) + 1)) ↔ (𝑦 + 1) ∈ (0...𝑁)))
9392biimpa 480 . . . . . . . . 9 ((𝜑 ∧ (𝑦 + 1) ∈ (0...((𝑁 − 1) + 1))) → (𝑦 + 1) ∈ (0...𝑁))
9490, 93sylan2 595 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 + 1) ∈ (0...𝑁))
95 nfv 1915 . . . . . . . . . 10 𝑗(𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁))
96 nfcsb1v 3852 . . . . . . . . . . 11 𝑗(𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))
9796, 3, 4nff 6483 . . . . . . . . . 10 𝑗(𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)
9895, 97nfim 1897 . . . . . . . . 9 𝑗((𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁)) → (𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
99 ovex 7168 . . . . . . . . 9 (𝑦 + 1) ∈ V
100 eleq1 2877 . . . . . . . . . . 11 (𝑗 = (𝑦 + 1) → (𝑗 ∈ (0...𝑁) ↔ (𝑦 + 1) ∈ (0...𝑁)))
101100anbi2d 631 . . . . . . . . . 10 (𝑗 = (𝑦 + 1) → ((𝜑𝑗 ∈ (0...𝑁)) ↔ (𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁))))
102 csbeq1a 3842 . . . . . . . . . . 11 (𝑗 = (𝑦 + 1) → (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
103102feq1d 6472 . . . . . . . . . 10 (𝑗 = (𝑦 + 1) → ((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) ↔ (𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))
104101, 103imbi12d 348 . . . . . . . . 9 (𝑗 = (𝑦 + 1) → (((𝜑𝑗 ∈ (0...𝑁)) → (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) ↔ ((𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁)) → (𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))))
10598, 99, 104, 87vtoclf 3506 . . . . . . . 8 ((𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁)) → (𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
10694, 105syldan 594 . . . . . . 7 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
107 csbeq1 3831 . . . . . . . . 9 (𝑦 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → 𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
108107feq1d 6472 . . . . . . . 8 (𝑦 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → (𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) ↔ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))
109 csbeq1 3831 . . . . . . . . 9 ((𝑦 + 1) = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → (𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
110109feq1d 6472 . . . . . . . 8 ((𝑦 + 1) = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → ((𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) ↔ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))
111108, 110ifboth 4463 . . . . . . 7 ((𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) ∧ (𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
11289, 106, 111syl2anc 587 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
113 ovex 7168 . . . . . . 7 (0...𝐾) ∈ V
114113, 84elmap 8418 . . . . . 6 (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ ((0...𝐾) ↑m (1...𝑁)) ↔ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
115112, 114sylibr 237 . . . . 5 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ ((0...𝐾) ↑m (1...𝑁)))
116115fmpttd 6856 . . . 4 (𝜑 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))):(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁)))
117 ovex 7168 . . . . 5 ((0...𝐾) ↑m (1...𝑁)) ∈ V
118 ovex 7168 . . . . 5 (0...(𝑁 − 1)) ∈ V
119117, 118elmap 8418 . . . 4 ((𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ∈ (((0...𝐾) ↑m (1...𝑁)) ↑m (0...(𝑁 − 1))) ↔ (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))):(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁)))
120116, 119sylibr 237 . . 3 (𝜑 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ∈ (((0...𝐾) ↑m (1...𝑁)) ↑m (0...(𝑁 − 1))))
121 rneq 5770 . . . . . . . 8 (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → ran 𝑥 = ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))
122121mpteq1d 5119 . . . . . . 7 (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → (𝑝 ∈ ran 𝑥𝐵) = (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵))
123122rneqd 5772 . . . . . 6 (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → ran (𝑝 ∈ ran 𝑥𝐵) = ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵))
124123sseq2d 3947 . . . . 5 (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran 𝑥𝐵) ↔ (0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵)))
125121rexeqdv 3365 . . . . 5 (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → (∃𝑝 ∈ ran 𝑥(𝑝𝑁) ≠ 0 ↔ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0))
126124, 125anbi12d 633 . . . 4 (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → (((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran 𝑥𝐵) ∧ ∃𝑝 ∈ ran 𝑥(𝑝𝑁) ≠ 0) ↔ ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ∧ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0)))
127126ceqsrexv 3597 . . 3 ((𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ∈ (((0...𝐾) ↑m (1...𝑁)) ↑m (0...(𝑁 − 1))) → (∃𝑥 ∈ (((0...𝐾) ↑m (1...𝑁)) ↑m (0...(𝑁 − 1)))(𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ∧ ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran 𝑥𝐵) ∧ ∃𝑝 ∈ ran 𝑥(𝑝𝑁) ≠ 0)) ↔ ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ∧ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0)))
128120, 127syl 17 . 2 (𝜑 → (∃𝑥 ∈ (((0...𝐾) ↑m (1...𝑁)) ↑m (0...(𝑁 − 1)))(𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ∧ ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran 𝑥𝐵) ∧ ∃𝑝 ∈ ran 𝑥(𝑝𝑁) ≠ 0)) ↔ ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ∧ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0)))
129 dfss3 3903 . . . 4 ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ↔ ∀𝑖 ∈ (0...(𝑁 − 1))𝑖 ∈ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵))
130 ovex 7168 . . . . . . . . . . . . 13 ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
131 poimirlem28.1 . . . . . . . . . . . . 13 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶)
132130, 131csbie 3863 . . . . . . . . . . . 12 ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵 = 𝐶
133132csbeq2i 3836 . . . . . . . . . . 11 𝑇, 𝑈⟩ / 𝑠((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵 = 𝑇, 𝑈⟩ / 𝑠𝐶
134 opex 5321 . . . . . . . . . . . . 13 𝑇, 𝑈⟩ ∈ V
135134a1i 11 . . . . . . . . . . . 12 (𝜑 → ⟨𝑇, 𝑈⟩ ∈ V)
136 fveq2 6645 . . . . . . . . . . . . . . 15 (𝑠 = ⟨𝑇, 𝑈⟩ → (1st𝑠) = (1st ‘⟨𝑇, 𝑈⟩))
137 fex 6966 . . . . . . . . . . . . . . . . 17 ((𝑇:(1...𝑁)⟶(0..^𝐾) ∧ (1...𝑁) ∈ V) → 𝑇 ∈ V)
13845, 84, 137sylancl 589 . . . . . . . . . . . . . . . 16 (𝜑𝑇 ∈ V)
139 f1oexrnex 7614 . . . . . . . . . . . . . . . . 17 ((𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ∧ (1...𝑁) ∈ V) → 𝑈 ∈ V)
14052, 84, 139sylancl 589 . . . . . . . . . . . . . . . 16 (𝜑𝑈 ∈ V)
141 op1stg 7683 . . . . . . . . . . . . . . . 16 ((𝑇 ∈ V ∧ 𝑈 ∈ V) → (1st ‘⟨𝑇, 𝑈⟩) = 𝑇)
142138, 140, 141syl2anc 587 . . . . . . . . . . . . . . 15 (𝜑 → (1st ‘⟨𝑇, 𝑈⟩) = 𝑇)
143136, 142sylan9eqr 2855 . . . . . . . . . . . . . 14 ((𝜑𝑠 = ⟨𝑇, 𝑈⟩) → (1st𝑠) = 𝑇)
144 fveq2 6645 . . . . . . . . . . . . . . . 16 (𝑠 = ⟨𝑇, 𝑈⟩ → (2nd𝑠) = (2nd ‘⟨𝑇, 𝑈⟩))
145 op2ndg 7684 . . . . . . . . . . . . . . . . 17 ((𝑇 ∈ V ∧ 𝑈 ∈ V) → (2nd ‘⟨𝑇, 𝑈⟩) = 𝑈)
146138, 140, 145syl2anc 587 . . . . . . . . . . . . . . . 16 (𝜑 → (2nd ‘⟨𝑇, 𝑈⟩) = 𝑈)
147144, 146sylan9eqr 2855 . . . . . . . . . . . . . . 15 ((𝜑𝑠 = ⟨𝑇, 𝑈⟩) → (2nd𝑠) = 𝑈)
148 imaeq1 5891 . . . . . . . . . . . . . . . . 17 ((2nd𝑠) = 𝑈 → ((2nd𝑠) “ (1...𝑗)) = (𝑈 “ (1...𝑗)))
149148xpeq1d 5548 . . . . . . . . . . . . . . . 16 ((2nd𝑠) = 𝑈 → (((2nd𝑠) “ (1...𝑗)) × {1}) = ((𝑈 “ (1...𝑗)) × {1}))
150 imaeq1 5891 . . . . . . . . . . . . . . . . 17 ((2nd𝑠) = 𝑈 → ((2nd𝑠) “ ((𝑗 + 1)...𝑁)) = (𝑈 “ ((𝑗 + 1)...𝑁)))
151150xpeq1d 5548 . . . . . . . . . . . . . . . 16 ((2nd𝑠) = 𝑈 → (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))
152149, 151uneq12d 4091 . . . . . . . . . . . . . . 15 ((2nd𝑠) = 𝑈 → ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))
153147, 152syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑠 = ⟨𝑇, 𝑈⟩) → ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))
154143, 153oveq12d 7153 . . . . . . . . . . . . 13 ((𝜑𝑠 = ⟨𝑇, 𝑈⟩) → ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
155154csbeq1d 3832 . . . . . . . . . . . 12 ((𝜑𝑠 = ⟨𝑇, 𝑈⟩) → ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵 = (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
156135, 155csbied 3864 . . . . . . . . . . 11 (𝜑𝑇, 𝑈⟩ / 𝑠((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵 = (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
157133, 156syl5eqr 2847 . . . . . . . . . 10 (𝜑𝑇, 𝑈⟩ / 𝑠𝐶 = (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
158157csbeq2dv 3835 . . . . . . . . 9 (𝜑if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
159158eqeq2d 2809 . . . . . . . 8 (𝜑 → (𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵))
160159rexbidv 3256 . . . . . . 7 (𝜑 → (∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵))
161 vex 3444 . . . . . . . . 9 𝑖 ∈ V
162 eqid 2798 . . . . . . . . . 10 (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) = (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵)
163162elrnmpt 5792 . . . . . . . . 9 (𝑖 ∈ V → (𝑖 ∈ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ↔ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))𝑖 = 𝐵))
164161, 163ax-mp 5 . . . . . . . 8 (𝑖 ∈ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ↔ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))𝑖 = 𝐵)
165 nfv 1915 . . . . . . . . 9 𝑘 𝑖 = 𝐵
166 nfcsb1v 3852 . . . . . . . . . 10 𝑝𝑘 / 𝑝𝐵
167166nfeq2 2972 . . . . . . . . 9 𝑝 𝑖 = 𝑘 / 𝑝𝐵
168 csbeq1a 3842 . . . . . . . . . 10 (𝑝 = 𝑘𝐵 = 𝑘 / 𝑝𝐵)
169168eqeq2d 2809 . . . . . . . . 9 (𝑝 = 𝑘 → (𝑖 = 𝐵𝑖 = 𝑘 / 𝑝𝐵))
170165, 167, 169cbvrexw 3388 . . . . . . . 8 (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))𝑖 = 𝐵 ↔ ∃𝑘 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))𝑖 = 𝑘 / 𝑝𝐵)
171 ovex 7168 . . . . . . . . . . 11 (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
172171csbex 5179 . . . . . . . . . 10 if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
173172rgenw 3118 . . . . . . . . 9 𝑦 ∈ (0...(𝑁 − 1))if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
174 eqid 2798 . . . . . . . . . 10 (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
175 csbeq1 3831 . . . . . . . . . . . 12 (𝑘 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝑘 / 𝑝𝐵 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
176 vex 3444 . . . . . . . . . . . . . 14 𝑦 ∈ V
177176, 99ifex 4473 . . . . . . . . . . . . 13 if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) ∈ V
178 csbnestgw 4329 . . . . . . . . . . . . 13 (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) ∈ V → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
179177, 178ax-mp 5 . . . . . . . . . . . 12 if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵
180175, 179eqtr4di 2851 . . . . . . . . . . 11 (𝑘 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝑘 / 𝑝𝐵 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
181180eqeq2d 2809 . . . . . . . . . 10 (𝑘 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑖 = 𝑘 / 𝑝𝐵𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵))
182174, 181rexrnmptw 6838 . . . . . . . . 9 (∀𝑦 ∈ (0...(𝑁 − 1))if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V → (∃𝑘 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))𝑖 = 𝑘 / 𝑝𝐵 ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵))
183173, 182ax-mp 5 . . . . . . . 8 (∃𝑘 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))𝑖 = 𝑘 / 𝑝𝐵 ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
184164, 170, 1833bitri 300 . . . . . . 7 (𝑖 ∈ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
185160, 184syl6bbr 292 . . . . . 6 (𝜑 → (∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑖 ∈ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵)))
18624sselda 3915 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ (0...𝑁))
187186adantr 484 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < 𝑉) → 𝑦 ∈ (0...𝑁))
188 elfzelz 12902 . . . . . . . . . . . . . 14 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℤ)
189188zred 12075 . . . . . . . . . . . . 13 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ)
190189adantl 485 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ ℝ)
191 ltne 10726 . . . . . . . . . . . . 13 ((𝑦 ∈ ℝ ∧ 𝑦 < 𝑉) → 𝑉𝑦)
192191necomd 3042 . . . . . . . . . . . 12 ((𝑦 ∈ ℝ ∧ 𝑦 < 𝑉) → 𝑦𝑉)
193190, 192sylan 583 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < 𝑉) → 𝑦𝑉)
194 eldifsn 4680 . . . . . . . . . . 11 (𝑦 ∈ ((0...𝑁) ∖ {𝑉}) ↔ (𝑦 ∈ (0...𝑁) ∧ 𝑦𝑉))
195187, 193, 194sylanbrc 586 . . . . . . . . . 10 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < 𝑉) → 𝑦 ∈ ((0...𝑁) ∖ {𝑉}))
19694adantr 484 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → (𝑦 + 1) ∈ (0...𝑁))
197 poimirlem24.5 . . . . . . . . . . . . . . 15 (𝜑𝑉 ∈ (0...𝑁))
198 elfzelz 12902 . . . . . . . . . . . . . . 15 (𝑉 ∈ (0...𝑁) → 𝑉 ∈ ℤ)
199197, 198syl 17 . . . . . . . . . . . . . 14 (𝜑𝑉 ∈ ℤ)
200199zred 12075 . . . . . . . . . . . . 13 (𝜑𝑉 ∈ ℝ)
201200ad2antrr 725 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → 𝑉 ∈ ℝ)
202 zre 11973 . . . . . . . . . . . . . . . 16 (𝑉 ∈ ℤ → 𝑉 ∈ ℝ)
203 zre 11973 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℤ → 𝑦 ∈ ℝ)
204 lenlt 10708 . . . . . . . . . . . . . . . 16 ((𝑉 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑉𝑦 ↔ ¬ 𝑦 < 𝑉))
205202, 203, 204syl2an 598 . . . . . . . . . . . . . . 15 ((𝑉 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑉𝑦 ↔ ¬ 𝑦 < 𝑉))
206 zleltp1 12021 . . . . . . . . . . . . . . 15 ((𝑉 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑉𝑦𝑉 < (𝑦 + 1)))
207205, 206bitr3d 284 . . . . . . . . . . . . . 14 ((𝑉 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (¬ 𝑦 < 𝑉𝑉 < (𝑦 + 1)))
208199, 188, 207syl2an 598 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (¬ 𝑦 < 𝑉𝑉 < (𝑦 + 1)))
209208biimpa 480 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → 𝑉 < (𝑦 + 1))
210201, 209gtned 10764 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → (𝑦 + 1) ≠ 𝑉)
211 eldifsn 4680 . . . . . . . . . . 11 ((𝑦 + 1) ∈ ((0...𝑁) ∖ {𝑉}) ↔ ((𝑦 + 1) ∈ (0...𝑁) ∧ (𝑦 + 1) ≠ 𝑉))
212196, 210, 211sylanbrc 586 . . . . . . . . . 10 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → (𝑦 + 1) ∈ ((0...𝑁) ∖ {𝑉}))
213195, 212ifclda 4459 . . . . . . . . 9 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) ∈ ((0...𝑁) ∖ {𝑉}))
214 nfcsb1v 3852 . . . . . . . . . . . 12 𝑗if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
215214nfeq2 2972 . . . . . . . . . . 11 𝑗 𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
216 csbeq1a 3842 . . . . . . . . . . . 12 (𝑗 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → 𝑇, 𝑈⟩ / 𝑠𝐶 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
217216eqeq2d 2809 . . . . . . . . . . 11 (𝑗 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
218215, 217rspce 3560 . . . . . . . . . 10 ((if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) ∈ ((0...𝑁) ∖ {𝑉}) ∧ 𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
219218ex 416 . . . . . . . . 9 (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) ∈ ((0...𝑁) ∖ {𝑉}) → (𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
220213, 219syl 17 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
221220rexlimdva 3243 . . . . . . 7 (𝜑 → (∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
222 nfv 1915 . . . . . . . 8 𝑗𝜑
223 nfcv 2955 . . . . . . . . 9 𝑗(0...(𝑁 − 1))
224223, 215nfrex 3268 . . . . . . . 8 𝑗𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
225 eldifi 4054 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ (0...𝑁))
226225, 57syl 17 . . . . . . . . . . . . . 14 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ ℕ0)
227226nn0ge0d 11946 . . . . . . . . . . . . 13 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 0 ≤ 𝑗)
228227ad2antlr 726 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 0 ≤ 𝑗)
229226nn0red 11944 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ ℝ)
230229ad2antlr 726 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 ∈ ℝ)
231200ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑉 ∈ ℝ)
23216zred 12075 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℝ)
233232ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑁 ∈ ℝ)
234 simpr 488 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 < 𝑉)
235 elfzle2 12906 . . . . . . . . . . . . . . . 16 (𝑉 ∈ (0...𝑁) → 𝑉𝑁)
236197, 235syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑉𝑁)
237236ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑉𝑁)
238230, 231, 233, 234, 237ltletrd 10789 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 < 𝑁)
239226nn0zd 12073 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ ℤ)
240 zltlem1 12023 . . . . . . . . . . . . . . 15 ((𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 < 𝑁𝑗 ≤ (𝑁 − 1)))
241239, 16, 240syl2anr 599 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗 < 𝑁𝑗 ≤ (𝑁 − 1)))
242241adantr 484 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → (𝑗 < 𝑁𝑗 ≤ (𝑁 − 1)))
243238, 242mpbid 235 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 ≤ (𝑁 − 1))
244 0z 11980 . . . . . . . . . . . . . . 15 0 ∈ ℤ
245 elfz 12891 . . . . . . . . . . . . . . 15 ((𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑗 ∈ (0...(𝑁 − 1)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝑁 − 1))))
246244, 245mp3an2 1446 . . . . . . . . . . . . . 14 ((𝑗 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑗 ∈ (0...(𝑁 − 1)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝑁 − 1))))
247239, 18, 246syl2anr 599 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗 ∈ (0...(𝑁 − 1)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝑁 − 1))))
248247adantr 484 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → (𝑗 ∈ (0...(𝑁 − 1)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝑁 − 1))))
249228, 243, 248mpbir2and 712 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 ∈ (0...(𝑁 − 1)))
250 0red 10633 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 0 ∈ ℝ)
251200ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑉 ∈ ℝ)
252229ad2antlr 726 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗 ∈ ℝ)
253 elfzle1 12905 . . . . . . . . . . . . . . . . 17 (𝑉 ∈ (0...𝑁) → 0 ≤ 𝑉)
254197, 253syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ 𝑉)
255254ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 0 ≤ 𝑉)
256 lenlt 10708 . . . . . . . . . . . . . . . . . 18 ((𝑉 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑉𝑗 ↔ ¬ 𝑗 < 𝑉))
257200, 229, 256syl2an 598 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑉𝑗 ↔ ¬ 𝑗 < 𝑉))
258257biimpar 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑉𝑗)
259 eldifsni 4683 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗𝑉)
260259ad2antlr 726 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗𝑉)
261 ltlen 10730 . . . . . . . . . . . . . . . . . 18 ((𝑉 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑉 < 𝑗 ↔ (𝑉𝑗𝑗𝑉)))
262200, 229, 261syl2an 598 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑉 < 𝑗 ↔ (𝑉𝑗𝑗𝑉)))
263262adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → (𝑉 < 𝑗 ↔ (𝑉𝑗𝑗𝑉)))
264258, 260, 263mpbir2and 712 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑉 < 𝑗)
265250, 251, 252, 255, 264lelttrd 10787 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 0 < 𝑗)
266 zgt0ge1 12024 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℤ → (0 < 𝑗 ↔ 1 ≤ 𝑗))
267239, 266syl 17 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → (0 < 𝑗 ↔ 1 ≤ 𝑗))
268267ad2antlr 726 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → (0 < 𝑗 ↔ 1 ≤ 𝑗))
269265, 268mpbid 235 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 1 ≤ 𝑗)
270 elfzle2 12906 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑁) → 𝑗𝑁)
271225, 270syl 17 . . . . . . . . . . . . . 14 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗𝑁)
272271ad2antlr 726 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗𝑁)
273 1z 12000 . . . . . . . . . . . . . . . 16 1 ∈ ℤ
274 elfz 12891 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 ∈ (1...𝑁) ↔ (1 ≤ 𝑗𝑗𝑁)))
275273, 274mp3an2 1446 . . . . . . . . . . . . . . 15 ((𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 ∈ (1...𝑁) ↔ (1 ≤ 𝑗𝑗𝑁)))
276239, 16, 275syl2anr 599 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗 ∈ (1...𝑁) ↔ (1 ≤ 𝑗𝑗𝑁)))
277276adantr 484 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → (𝑗 ∈ (1...𝑁) ↔ (1 ≤ 𝑗𝑗𝑁)))
278269, 272, 277mpbir2and 712 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗 ∈ (1...𝑁))
279 elfzmlbm 13012 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑁) → (𝑗 − 1) ∈ (0...(𝑁 − 1)))
280278, 279syl 17 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → (𝑗 − 1) ∈ (0...(𝑁 − 1)))
281249, 280ifclda 4459 . . . . . . . . . 10 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) ∈ (0...(𝑁 − 1)))
282 breq1 5033 . . . . . . . . . . . . . . . 16 (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 < 𝑉 ↔ if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉))
283 id 22 . . . . . . . . . . . . . . . 16 (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → 𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)))
284 oveq1 7142 . . . . . . . . . . . . . . . 16 (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 + 1) = (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))
285282, 283, 284ifbieq12d 4452 . . . . . . . . . . . . . . 15 (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)) = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)))
286285eqeq2d 2809 . . . . . . . . . . . . . 14 (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)) ↔ 𝑗 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))))
287 breq1 5033 . . . . . . . . . . . . . . . 16 ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → ((𝑗 − 1) < 𝑉 ↔ if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉))
288 id 22 . . . . . . . . . . . . . . . 16 ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)))
289 oveq1 7142 . . . . . . . . . . . . . . . 16 ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → ((𝑗 − 1) + 1) = (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))
290287, 288, 289ifbieq12d 4452 . . . . . . . . . . . . . . 15 ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → if((𝑗 − 1) < 𝑉, (𝑗 − 1), ((𝑗 − 1) + 1)) = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)))
291290eqeq2d 2809 . . . . . . . . . . . . . 14 ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 = if((𝑗 − 1) < 𝑉, (𝑗 − 1), ((𝑗 − 1) + 1)) ↔ 𝑗 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))))
292 iftrue 4431 . . . . . . . . . . . . . . . 16 (𝑗 < 𝑉 → if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)) = 𝑗)
293292eqcomd 2804 . . . . . . . . . . . . . . 15 (𝑗 < 𝑉𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)))
294293adantl 485 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)))
295 zlem1lt 12022 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ℤ ∧ 𝑉 ∈ ℤ) → (𝑗𝑉 ↔ (𝑗 − 1) < 𝑉))
296239, 199, 295syl2anr 599 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗𝑉 ↔ (𝑗 − 1) < 𝑉))
297259necomd 3042 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑉𝑗)
298297adantl 485 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → 𝑉𝑗)
299 ltlen 10730 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑗 < 𝑉 ↔ (𝑗𝑉𝑉𝑗)))
300229, 200, 299syl2anr 599 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗 < 𝑉 ↔ (𝑗𝑉𝑉𝑗)))
301300biimprd 251 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → ((𝑗𝑉𝑉𝑗) → 𝑗 < 𝑉))
302298, 301mpan2d 693 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗𝑉𝑗 < 𝑉))
303296, 302sylbird 263 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → ((𝑗 − 1) < 𝑉𝑗 < 𝑉))
304303con3dimp 412 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → ¬ (𝑗 − 1) < 𝑉)
305304iffalsed 4436 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → if((𝑗 − 1) < 𝑉, (𝑗 − 1), ((𝑗 − 1) + 1)) = ((𝑗 − 1) + 1))
306226nn0cnd 11945 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ ℂ)
307 npcan1 11054 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℂ → ((𝑗 − 1) + 1) = 𝑗)
308306, 307syl 17 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → ((𝑗 − 1) + 1) = 𝑗)
309308ad2antlr 726 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → ((𝑗 − 1) + 1) = 𝑗)
310305, 309eqtr2d 2834 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗 = if((𝑗 − 1) < 𝑉, (𝑗 − 1), ((𝑗 − 1) + 1)))
311286, 291, 294, 310ifbothda 4462 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → 𝑗 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)))
312 csbeq1a 3842 . . . . . . . . . . . . 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 2809 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
315314biimpd 232 . . . . . . . . . 10 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
316 breq1 5033 . . . . . . . . . . . . . 14 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑦 < 𝑉 ↔ if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉))
317 id 22 . . . . . . . . . . . . . 14 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → 𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)))
318 oveq1 7142 . . . . . . . . . . . . . 14 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑦 + 1) = (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))
319316, 317, 318ifbieq12d 4452 . . . . . . . . . . . . 13 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)))
320319csbeq1d 3832 . . . . . . . . . . . 12 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
321320eqeq2d 2809 . . . . . . . . . . 11 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
322321rspcev 3571 . . . . . . . . . 10 ((if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) ∈ (0...(𝑁 − 1)) ∧ 𝑖 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
323281, 315, 322syl6an 683 . . . . . . . . 9 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
324323ex 416 . . . . . . . 8 (𝜑 → (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)))
325222, 224, 324rexlimd 3276 . . . . . . 7 (𝜑 → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
326221, 325impbid 215 . . . . . 6 (𝜑 → (∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
327185, 326bitr3d 284 . . . . 5 (𝜑 → (𝑖 ∈ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
328327ralbidv 3162 . . . 4 (𝜑 → (∀𝑖 ∈ (0...(𝑁 − 1))𝑖 ∈ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
329129, 328syl5bb 286 . . 3 (𝜑 → ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
330329anbi1d 632 . 2 (𝜑 → (((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ∧ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0) ↔ (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0)))
33112, 45, 52, 197poimirlem23 35080 . . 3 (𝜑 → (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁))))
332331anbi2d 631 . 2 (𝜑 → ((∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0) ↔ (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ ¬ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁)))))
333128, 330, 3323bitrd 308 1 (𝜑 → (∃𝑥 ∈ (((0...𝐾) ↑m (1...𝑁)) ↑m (0...(𝑁 − 1)))(𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (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 209  wa 399  wo 844   = wceq 1538  wcel 2111  wne 2987  wral 3106  wrex 3107  Vcvv 3441  csb 3828  cdif 3878  cun 3879  cin 3880  wss 3881  c0 4243  ifcif 4425  {csn 4525  cop 4531   class class class wbr 5030  cmpt 5110   × cxp 5517  ccnv 5518  ran crn 5520  cima 5522  Fun wfun 6318  wf 6320  ontowfo 6322  1-1-ontowf1o 6323  cfv 6324  (class class class)co 7135  f cof 7387  1st c1st 7669  2nd c2nd 7670  m cmap 8389  cc 10524  cr 10525  0cc0 10526  1c1 10527   + caddc 10529   < clt 10664  cle 10665  cmin 10859  cn 11625  0cn0 11885  cz 11969  cuz 12231  ...cfz 12885  ..^cfzo 13028
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-of 7389  df-om 7561  df-1st 7671  df-2nd 7672  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-er 8272  df-map 8391  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11626  df-n0 11886  df-z 11970  df-uz 12232  df-fz 12886  df-fzo 13029
This theorem is referenced by:  poimirlem27  35084
  Copyright terms: Public domain W3C validator