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 37248
Description: Lemma for poimir 37257, 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 1909 . . . . . . . . 9 𝑗(𝜑𝑦 ∈ (0...(𝑁 − 1)))
2 nfcsb1v 3914 . . . . . . . . . 10 𝑗𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))
3 nfcv 2891 . . . . . . . . . 10 𝑗(1...𝑁)
4 nfcv 2891 . . . . . . . . . 10 𝑗(0...𝐾)
52, 3, 4nff 6719 . . . . . . . . 9 𝑗𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)
61, 5nfim 1891 . . . . . . . 8 𝑗((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
7 eleq1 2813 . . . . . . . . . 10 (𝑗 = 𝑦 → (𝑗 ∈ (0...(𝑁 − 1)) ↔ 𝑦 ∈ (0...(𝑁 − 1))))
87anbi2d 628 . . . . . . . . 9 (𝑗 = 𝑦 → ((𝜑𝑗 ∈ (0...(𝑁 − 1))) ↔ (𝜑𝑦 ∈ (0...(𝑁 − 1)))))
9 csbeq1a 3903 . . . . . . . . . 10 (𝑗 = 𝑦 → (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = 𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
109feq1d 6708 . . . . . . . . 9 (𝑗 = 𝑦 → ((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) ↔ 𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))
118, 10imbi12d 343 . . . . . . . 8 (𝑗 = 𝑦 → (((𝜑𝑗 ∈ (0...(𝑁 − 1))) → (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) ↔ ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))))
12 poimir.0 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℕ)
1312nncnd 12261 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℂ)
14 npcan1 11671 . . . . . . . . . . . . 13 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
1513, 14syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
1612nnzd 12618 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
17 peano2zm 12638 . . . . . . . . . . . . . 14 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
1816, 17syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑁 − 1) ∈ ℤ)
19 uzid 12870 . . . . . . . . . . . . 13 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
20 peano2uz 12918 . . . . . . . . . . . . 13 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
2118, 19, 203syl 18 . . . . . . . . . . . 12 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
2215, 21eqeltrrd 2826 . . . . . . . . . . 11 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
23 fzss2 13576 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (0...(𝑁 − 1)) ⊆ (0...𝑁))
2422, 23syl 17 . . . . . . . . . 10 (𝜑 → (0...(𝑁 − 1)) ⊆ (0...𝑁))
2524sselda 3976 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → 𝑗 ∈ (0...𝑁))
26 elun 4145 . . . . . . . . . . . . 13 (𝑦 ∈ ({1} ∪ {0}) ↔ (𝑦 ∈ {1} ∨ 𝑦 ∈ {0}))
27 fzofzp1 13765 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0..^𝐾) → (𝑥 + 1) ∈ (0...𝐾))
28 elsni 4647 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {1} → 𝑦 = 1)
2928oveq2d 7435 . . . . . . . . . . . . . . . 16 (𝑦 ∈ {1} → (𝑥 + 𝑦) = (𝑥 + 1))
3029eleq1d 2810 . . . . . . . . . . . . . . 15 (𝑦 ∈ {1} → ((𝑥 + 𝑦) ∈ (0...𝐾) ↔ (𝑥 + 1) ∈ (0...𝐾)))
3127, 30syl5ibrcom 246 . . . . . . . . . . . . . 14 (𝑥 ∈ (0..^𝐾) → (𝑦 ∈ {1} → (𝑥 + 𝑦) ∈ (0...𝐾)))
32 elfzoelz 13667 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (0..^𝐾) → 𝑥 ∈ ℤ)
3332zcnd 12700 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (0..^𝐾) → 𝑥 ∈ ℂ)
3433addridd 11446 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (0..^𝐾) → (𝑥 + 0) = 𝑥)
35 elfzofz 13683 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (0..^𝐾) → 𝑥 ∈ (0...𝐾))
3634, 35eqeltrd 2825 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0..^𝐾) → (𝑥 + 0) ∈ (0...𝐾))
37 elsni 4647 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {0} → 𝑦 = 0)
3837oveq2d 7435 . . . . . . . . . . . . . . . 16 (𝑦 ∈ {0} → (𝑥 + 𝑦) = (𝑥 + 0))
3938eleq1d 2810 . . . . . . . . . . . . . . 15 (𝑦 ∈ {0} → ((𝑥 + 𝑦) ∈ (0...𝐾) ↔ (𝑥 + 0) ∈ (0...𝐾)))
4036, 39syl5ibrcom 246 . . . . . . . . . . . . . 14 (𝑥 ∈ (0..^𝐾) → (𝑦 ∈ {0} → (𝑥 + 𝑦) ∈ (0...𝐾)))
4131, 40jaod 857 . . . . . . . . . . . . 13 (𝑥 ∈ (0..^𝐾) → ((𝑦 ∈ {1} ∨ 𝑦 ∈ {0}) → (𝑥 + 𝑦) ∈ (0...𝐾)))
4226, 41biimtrid 241 . . . . . . . . . . . 12 (𝑥 ∈ (0..^𝐾) → (𝑦 ∈ ({1} ∪ {0}) → (𝑥 + 𝑦) ∈ (0...𝐾)))
4342imp 405 . . . . . . . . . . 11 ((𝑥 ∈ (0..^𝐾) ∧ 𝑦 ∈ ({1} ∪ {0})) → (𝑥 + 𝑦) ∈ (0...𝐾))
4443adantl 480 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ (0..^𝐾) ∧ 𝑦 ∈ ({1} ∪ {0}))) → (𝑥 + 𝑦) ∈ (0...𝐾))
45 poimirlem25.3 . . . . . . . . . . 11 (𝜑𝑇:(1...𝑁)⟶(0..^𝐾))
4645adantr 479 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇:(1...𝑁)⟶(0..^𝐾))
47 1ex 11242 . . . . . . . . . . . . . 14 1 ∈ V
4847fconst 6783 . . . . . . . . . . . . 13 ((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1}
49 c0ex 11240 . . . . . . . . . . . . . 14 0 ∈ V
5049fconst 6783 . . . . . . . . . . . . 13 ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}
5148, 50pm3.2i 469 . . . . . . . . . . . 12 (((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0})
52 poimirlem25.4 . . . . . . . . . . . . . 14 (𝜑𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
53 dff1o3 6844 . . . . . . . . . . . . . . 15 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun 𝑈))
5453simprbi 495 . . . . . . . . . . . . . 14 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun 𝑈)
55 imain 6639 . . . . . . . . . . . . . 14 (Fun 𝑈 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))))
5652, 54, 553syl 18 . . . . . . . . . . . . 13 (𝜑 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))))
57 elfznn0 13629 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ0)
5857nn0red 12566 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
5958ltp1d 12177 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1))
60 fzdisj 13563 . . . . . . . . . . . . . . . 16 (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
6159, 60syl 17 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
6261imaeq2d 6064 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (𝑈 “ ∅))
63 ima0 6081 . . . . . . . . . . . . . 14 (𝑈 “ ∅) = ∅
6462, 63eqtrdi 2781 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
6556, 64sylan9req 2786 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
66 fun 6759 . . . . . . . . . . . 12 (((((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}) ∧ ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
6751, 65, 66sylancr 585 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
68 nn0p1nn 12544 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
6957, 68syl 17 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ)
70 nnuz 12898 . . . . . . . . . . . . . . . . 17 ℕ = (ℤ‘1)
7169, 70eleqtrdi 2835 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (ℤ‘1))
72 elfzuz3 13533 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ𝑗))
73 fzsplit2 13561 . . . . . . . . . . . . . . . 16 (((𝑗 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
7471, 72, 73syl2anc 582 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
7574imaeq2d 6064 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑁) → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))))
76 imaundi 6156 . . . . . . . . . . . . . 14 (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))
7775, 76eqtr2di 2782 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑁) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (𝑈 “ (1...𝑁)))
78 f1ofo 6845 . . . . . . . . . . . . . 14 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁))
79 foima 6815 . . . . . . . . . . . . . 14 (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁))
8052, 78, 793syl 18 . . . . . . . . . . . . 13 (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁))
8177, 80sylan9eqr 2787 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (1...𝑁))
8281feq2d 6709 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}) ↔ (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0})))
8367, 82mpbid 231 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
84 ovex 7452 . . . . . . . . . . 11 (1...𝑁) ∈ V
8584a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ V)
86 inidm 4217 . . . . . . . . . 10 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
8744, 46, 83, 85, 85, 86off 7703 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
8825, 87syldan 589 . . . . . . . 8 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
896, 11, 88chvarfv 2228 . . . . . . 7 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
90 fzp1elp1 13589 . . . . . . . . 9 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ (0...((𝑁 − 1) + 1)))
9115oveq2d 7435 . . . . . . . . . . 11 (𝜑 → (0...((𝑁 − 1) + 1)) = (0...𝑁))
9291eleq2d 2811 . . . . . . . . . 10 (𝜑 → ((𝑦 + 1) ∈ (0...((𝑁 − 1) + 1)) ↔ (𝑦 + 1) ∈ (0...𝑁)))
9392biimpa 475 . . . . . . . . 9 ((𝜑 ∧ (𝑦 + 1) ∈ (0...((𝑁 − 1) + 1))) → (𝑦 + 1) ∈ (0...𝑁))
9490, 93sylan2 591 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 + 1) ∈ (0...𝑁))
95 nfv 1909 . . . . . . . . . 10 𝑗(𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁))
96 nfcsb1v 3914 . . . . . . . . . . 11 𝑗(𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))
9796, 3, 4nff 6719 . . . . . . . . . 10 𝑗(𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)
9895, 97nfim 1891 . . . . . . . . 9 𝑗((𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁)) → (𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
99 ovex 7452 . . . . . . . . 9 (𝑦 + 1) ∈ V
100 eleq1 2813 . . . . . . . . . . 11 (𝑗 = (𝑦 + 1) → (𝑗 ∈ (0...𝑁) ↔ (𝑦 + 1) ∈ (0...𝑁)))
101100anbi2d 628 . . . . . . . . . 10 (𝑗 = (𝑦 + 1) → ((𝜑𝑗 ∈ (0...𝑁)) ↔ (𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁))))
102 csbeq1a 3903 . . . . . . . . . . 11 (𝑗 = (𝑦 + 1) → (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
103102feq1d 6708 . . . . . . . . . 10 (𝑗 = (𝑦 + 1) → ((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) ↔ (𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))
104101, 103imbi12d 343 . . . . . . . . 9 (𝑗 = (𝑦 + 1) → (((𝜑𝑗 ∈ (0...𝑁)) → (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) ↔ ((𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁)) → (𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))))
10598, 99, 104, 87vtoclf 3542 . . . . . . . 8 ((𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁)) → (𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
10694, 105syldan 589 . . . . . . 7 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
107 csbeq1 3892 . . . . . . . . 9 (𝑦 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → 𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
108107feq1d 6708 . . . . . . . 8 (𝑦 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → (𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) ↔ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))
109 csbeq1 3892 . . . . . . . . 9 ((𝑦 + 1) = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → (𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
110109feq1d 6708 . . . . . . . 8 ((𝑦 + 1) = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → ((𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) ↔ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))
111108, 110ifboth 4569 . . . . . . 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 582 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
113 ovex 7452 . . . . . . 7 (0...𝐾) ∈ V
114113, 84elmap 8890 . . . . . 6 (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ ((0...𝐾) ↑m (1...𝑁)) ↔ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
115112, 114sylibr 233 . . . . 5 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ ((0...𝐾) ↑m (1...𝑁)))
116115fmpttd 7124 . . . 4 (𝜑 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))):(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁)))
117 ovex 7452 . . . . 5 ((0...𝐾) ↑m (1...𝑁)) ∈ V
118 ovex 7452 . . . . 5 (0...(𝑁 − 1)) ∈ V
119117, 118elmap 8890 . . . 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 233 . . 3 (𝜑 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ∈ (((0...𝐾) ↑m (1...𝑁)) ↑m (0...(𝑁 − 1))))
121 rneq 5938 . . . . . . . 8 (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → ran 𝑥 = ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))
122121mpteq1d 5244 . . . . . . 7 (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → (𝑝 ∈ ran 𝑥𝐵) = (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵))
123122rneqd 5940 . . . . . 6 (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → ran (𝑝 ∈ ran 𝑥𝐵) = ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵))
124123sseq2d 4009 . . . . 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 3315 . . . . 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 630 . . . 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 3638 . . 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 3965 . . . 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 7452 . . . . . . . . . . . . 13 ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
131 poimirlem28.1 . . . . . . . . . . . . 13 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶)
132130, 131csbie 3925 . . . . . . . . . . . 12 ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵 = 𝐶
133132csbeq2i 3897 . . . . . . . . . . 11 𝑇, 𝑈⟩ / 𝑠((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵 = 𝑇, 𝑈⟩ / 𝑠𝐶
134 opex 5466 . . . . . . . . . . . . 13 𝑇, 𝑈⟩ ∈ V
135134a1i 11 . . . . . . . . . . . 12 (𝜑 → ⟨𝑇, 𝑈⟩ ∈ V)
136 fveq2 6896 . . . . . . . . . . . . . . 15 (𝑠 = ⟨𝑇, 𝑈⟩ → (1st𝑠) = (1st ‘⟨𝑇, 𝑈⟩))
137 fex 7238 . . . . . . . . . . . . . . . . 17 ((𝑇:(1...𝑁)⟶(0..^𝐾) ∧ (1...𝑁) ∈ V) → 𝑇 ∈ V)
13845, 84, 137sylancl 584 . . . . . . . . . . . . . . . 16 (𝜑𝑇 ∈ V)
139 f1oexrnex 7935 . . . . . . . . . . . . . . . . 17 ((𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ∧ (1...𝑁) ∈ V) → 𝑈 ∈ V)
14052, 84, 139sylancl 584 . . . . . . . . . . . . . . . 16 (𝜑𝑈 ∈ V)
141 op1stg 8006 . . . . . . . . . . . . . . . 16 ((𝑇 ∈ V ∧ 𝑈 ∈ V) → (1st ‘⟨𝑇, 𝑈⟩) = 𝑇)
142138, 140, 141syl2anc 582 . . . . . . . . . . . . . . 15 (𝜑 → (1st ‘⟨𝑇, 𝑈⟩) = 𝑇)
143136, 142sylan9eqr 2787 . . . . . . . . . . . . . 14 ((𝜑𝑠 = ⟨𝑇, 𝑈⟩) → (1st𝑠) = 𝑇)
144 fveq2 6896 . . . . . . . . . . . . . . . 16 (𝑠 = ⟨𝑇, 𝑈⟩ → (2nd𝑠) = (2nd ‘⟨𝑇, 𝑈⟩))
145 op2ndg 8007 . . . . . . . . . . . . . . . . 17 ((𝑇 ∈ V ∧ 𝑈 ∈ V) → (2nd ‘⟨𝑇, 𝑈⟩) = 𝑈)
146138, 140, 145syl2anc 582 . . . . . . . . . . . . . . . 16 (𝜑 → (2nd ‘⟨𝑇, 𝑈⟩) = 𝑈)
147144, 146sylan9eqr 2787 . . . . . . . . . . . . . . 15 ((𝜑𝑠 = ⟨𝑇, 𝑈⟩) → (2nd𝑠) = 𝑈)
148 imaeq1 6059 . . . . . . . . . . . . . . . . 17 ((2nd𝑠) = 𝑈 → ((2nd𝑠) “ (1...𝑗)) = (𝑈 “ (1...𝑗)))
149148xpeq1d 5707 . . . . . . . . . . . . . . . 16 ((2nd𝑠) = 𝑈 → (((2nd𝑠) “ (1...𝑗)) × {1}) = ((𝑈 “ (1...𝑗)) × {1}))
150 imaeq1 6059 . . . . . . . . . . . . . . . . 17 ((2nd𝑠) = 𝑈 → ((2nd𝑠) “ ((𝑗 + 1)...𝑁)) = (𝑈 “ ((𝑗 + 1)...𝑁)))
151150xpeq1d 5707 . . . . . . . . . . . . . . . 16 ((2nd𝑠) = 𝑈 → (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))
152149, 151uneq12d 4161 . . . . . . . . . . . . . . 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 7437 . . . . . . . . . . . . 13 ((𝜑𝑠 = ⟨𝑇, 𝑈⟩) → ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
155154csbeq1d 3893 . . . . . . . . . . . 12 ((𝜑𝑠 = ⟨𝑇, 𝑈⟩) → ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵 = (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
156135, 155csbied 3927 . . . . . . . . . . 11 (𝜑𝑇, 𝑈⟩ / 𝑠((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵 = (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
157133, 156eqtr3id 2779 . . . . . . . . . 10 (𝜑𝑇, 𝑈⟩ / 𝑠𝐶 = (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
158157csbeq2dv 3896 . . . . . . . . 9 (𝜑if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
159158eqeq2d 2736 . . . . . . . 8 (𝜑 → (𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵))
160159rexbidv 3168 . . . . . . 7 (𝜑 → (∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵))
161 vex 3465 . . . . . . . . 9 𝑖 ∈ V
162 eqid 2725 . . . . . . . . . 10 (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) = (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵)
163162elrnmpt 5958 . . . . . . . . 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 1909 . . . . . . . . 9 𝑘 𝑖 = 𝐵
166 nfcsb1v 3914 . . . . . . . . . 10 𝑝𝑘 / 𝑝𝐵
167166nfeq2 2909 . . . . . . . . 9 𝑝 𝑖 = 𝑘 / 𝑝𝐵
168 csbeq1a 3903 . . . . . . . . . 10 (𝑝 = 𝑘𝐵 = 𝑘 / 𝑝𝐵)
169168eqeq2d 2736 . . . . . . . . 9 (𝑝 = 𝑘 → (𝑖 = 𝐵𝑖 = 𝑘 / 𝑝𝐵))
170165, 167, 169cbvrexw 3294 . . . . . . . 8 (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))𝑖 = 𝐵 ↔ ∃𝑘 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))𝑖 = 𝑘 / 𝑝𝐵)
171 ovex 7452 . . . . . . . . . . 11 (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
172171csbex 5312 . . . . . . . . . 10 if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
173172rgenw 3054 . . . . . . . . 9 𝑦 ∈ (0...(𝑁 − 1))if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
174 eqid 2725 . . . . . . . . . 10 (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
175 csbeq1 3892 . . . . . . . . . . . 12 (𝑘 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝑘 / 𝑝𝐵 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
176 vex 3465 . . . . . . . . . . . . . 14 𝑦 ∈ V
177176, 99ifex 4580 . . . . . . . . . . . . 13 if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) ∈ V
178 csbnestgw 4423 . . . . . . . . . . . . 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 2783 . . . . . . . . . . 11 (𝑘 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝑘 / 𝑝𝐵 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
181180eqeq2d 2736 . . . . . . . . . 10 (𝑘 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑖 = 𝑘 / 𝑝𝐵𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵))
182174, 181rexrnmptw 7104 . . . . . . . . 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 296 . . . . . . 7 (𝑖 ∈ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
185160, 184bitr4di 288 . . . . . 6 (𝜑 → (∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑖 ∈ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵)))
18624sselda 3976 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ (0...𝑁))
187186adantr 479 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < 𝑉) → 𝑦 ∈ (0...𝑁))
188 elfzelz 13536 . . . . . . . . . . . . . 14 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℤ)
189188zred 12699 . . . . . . . . . . . . 13 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ)
190189adantl 480 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ ℝ)
191 ltne 11343 . . . . . . . . . . . . 13 ((𝑦 ∈ ℝ ∧ 𝑦 < 𝑉) → 𝑉𝑦)
192191necomd 2985 . . . . . . . . . . . 12 ((𝑦 ∈ ℝ ∧ 𝑦 < 𝑉) → 𝑦𝑉)
193190, 192sylan 578 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < 𝑉) → 𝑦𝑉)
194 eldifsn 4792 . . . . . . . . . . 11 (𝑦 ∈ ((0...𝑁) ∖ {𝑉}) ↔ (𝑦 ∈ (0...𝑁) ∧ 𝑦𝑉))
195187, 193, 194sylanbrc 581 . . . . . . . . . 10 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < 𝑉) → 𝑦 ∈ ((0...𝑁) ∖ {𝑉}))
19694adantr 479 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → (𝑦 + 1) ∈ (0...𝑁))
197 poimirlem24.5 . . . . . . . . . . . . . . 15 (𝜑𝑉 ∈ (0...𝑁))
198197elfzelzd 13537 . . . . . . . . . . . . . 14 (𝜑𝑉 ∈ ℤ)
199198zred 12699 . . . . . . . . . . . . 13 (𝜑𝑉 ∈ ℝ)
200199ad2antrr 724 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → 𝑉 ∈ ℝ)
201 zre 12595 . . . . . . . . . . . . . . . 16 (𝑉 ∈ ℤ → 𝑉 ∈ ℝ)
202 zre 12595 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℤ → 𝑦 ∈ ℝ)
203 lenlt 11324 . . . . . . . . . . . . . . . 16 ((𝑉 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑉𝑦 ↔ ¬ 𝑦 < 𝑉))
204201, 202, 203syl2an 594 . . . . . . . . . . . . . . 15 ((𝑉 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑉𝑦 ↔ ¬ 𝑦 < 𝑉))
205 zleltp1 12646 . . . . . . . . . . . . . . 15 ((𝑉 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑉𝑦𝑉 < (𝑦 + 1)))
206204, 205bitr3d 280 . . . . . . . . . . . . . 14 ((𝑉 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (¬ 𝑦 < 𝑉𝑉 < (𝑦 + 1)))
207198, 188, 206syl2an 594 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (¬ 𝑦 < 𝑉𝑉 < (𝑦 + 1)))
208207biimpa 475 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → 𝑉 < (𝑦 + 1))
209200, 208gtned 11381 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → (𝑦 + 1) ≠ 𝑉)
210 eldifsn 4792 . . . . . . . . . . 11 ((𝑦 + 1) ∈ ((0...𝑁) ∖ {𝑉}) ↔ ((𝑦 + 1) ∈ (0...𝑁) ∧ (𝑦 + 1) ≠ 𝑉))
211196, 209, 210sylanbrc 581 . . . . . . . . . 10 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → (𝑦 + 1) ∈ ((0...𝑁) ∖ {𝑉}))
212195, 211ifclda 4565 . . . . . . . . 9 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) ∈ ((0...𝑁) ∖ {𝑉}))
213 nfcsb1v 3914 . . . . . . . . . . . 12 𝑗if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
214213nfeq2 2909 . . . . . . . . . . 11 𝑗 𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
215 csbeq1a 3903 . . . . . . . . . . . 12 (𝑗 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → 𝑇, 𝑈⟩ / 𝑠𝐶 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
216215eqeq2d 2736 . . . . . . . . . . 11 (𝑗 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
217214, 216rspce 3595 . . . . . . . . . 10 ((if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) ∈ ((0...𝑁) ∖ {𝑉}) ∧ 𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
218217ex 411 . . . . . . . . 9 (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) ∈ ((0...𝑁) ∖ {𝑉}) → (𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
219212, 218syl 17 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
220219rexlimdva 3144 . . . . . . 7 (𝜑 → (∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
221 nfv 1909 . . . . . . . 8 𝑗𝜑
222 nfcv 2891 . . . . . . . . 9 𝑗(0...(𝑁 − 1))
223222, 214nfrexw 3300 . . . . . . . 8 𝑗𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
224 eldifi 4123 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ (0...𝑁))
225224, 57syl 17 . . . . . . . . . . . . . 14 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ ℕ0)
226225nn0ge0d 12568 . . . . . . . . . . . . 13 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 0 ≤ 𝑗)
227226ad2antlr 725 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 0 ≤ 𝑗)
228225nn0red 12566 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ ℝ)
229228ad2antlr 725 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 ∈ ℝ)
230199ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑉 ∈ ℝ)
23116zred 12699 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℝ)
232231ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑁 ∈ ℝ)
233 simpr 483 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 < 𝑉)
234 elfzle2 13540 . . . . . . . . . . . . . . . 16 (𝑉 ∈ (0...𝑁) → 𝑉𝑁)
235197, 234syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑉𝑁)
236235ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑉𝑁)
237229, 230, 232, 233, 236ltletrd 11406 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 < 𝑁)
238224elfzelzd 13537 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ ℤ)
239 zltlem1 12648 . . . . . . . . . . . . . . 15 ((𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 < 𝑁𝑗 ≤ (𝑁 − 1)))
240238, 16, 239syl2anr 595 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗 < 𝑁𝑗 ≤ (𝑁 − 1)))
241240adantr 479 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → (𝑗 < 𝑁𝑗 ≤ (𝑁 − 1)))
242237, 241mpbid 231 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 ≤ (𝑁 − 1))
243 0z 12602 . . . . . . . . . . . . . . 15 0 ∈ ℤ
244 elfz 13525 . . . . . . . . . . . . . . 15 ((𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑗 ∈ (0...(𝑁 − 1)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝑁 − 1))))
245243, 244mp3an2 1445 . . . . . . . . . . . . . 14 ((𝑗 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑗 ∈ (0...(𝑁 − 1)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝑁 − 1))))
246238, 18, 245syl2anr 595 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗 ∈ (0...(𝑁 − 1)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝑁 − 1))))
247246adantr 479 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → (𝑗 ∈ (0...(𝑁 − 1)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝑁 − 1))))
248227, 242, 247mpbir2and 711 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 ∈ (0...(𝑁 − 1)))
249 0red 11249 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 0 ∈ ℝ)
250199ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑉 ∈ ℝ)
251228ad2antlr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗 ∈ ℝ)
252 elfzle1 13539 . . . . . . . . . . . . . . . . 17 (𝑉 ∈ (0...𝑁) → 0 ≤ 𝑉)
253197, 252syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ 𝑉)
254253ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 0 ≤ 𝑉)
255 lenlt 11324 . . . . . . . . . . . . . . . . . 18 ((𝑉 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑉𝑗 ↔ ¬ 𝑗 < 𝑉))
256199, 228, 255syl2an 594 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑉𝑗 ↔ ¬ 𝑗 < 𝑉))
257256biimpar 476 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑉𝑗)
258 eldifsni 4795 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗𝑉)
259258ad2antlr 725 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗𝑉)
260 ltlen 11347 . . . . . . . . . . . . . . . . . 18 ((𝑉 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑉 < 𝑗 ↔ (𝑉𝑗𝑗𝑉)))
261199, 228, 260syl2an 594 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑉 < 𝑗 ↔ (𝑉𝑗𝑗𝑉)))
262261adantr 479 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → (𝑉 < 𝑗 ↔ (𝑉𝑗𝑗𝑉)))
263257, 259, 262mpbir2and 711 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑉 < 𝑗)
264249, 250, 251, 254, 263lelttrd 11404 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 0 < 𝑗)
265 zgt0ge1 12649 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℤ → (0 < 𝑗 ↔ 1 ≤ 𝑗))
266238, 265syl 17 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → (0 < 𝑗 ↔ 1 ≤ 𝑗))
267266ad2antlr 725 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → (0 < 𝑗 ↔ 1 ≤ 𝑗))
268264, 267mpbid 231 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 1 ≤ 𝑗)
269 elfzle2 13540 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑁) → 𝑗𝑁)
270224, 269syl 17 . . . . . . . . . . . . . 14 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗𝑁)
271270ad2antlr 725 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗𝑁)
272 1z 12625 . . . . . . . . . . . . . . . 16 1 ∈ ℤ
273 elfz 13525 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 ∈ (1...𝑁) ↔ (1 ≤ 𝑗𝑗𝑁)))
274272, 273mp3an2 1445 . . . . . . . . . . . . . . 15 ((𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 ∈ (1...𝑁) ↔ (1 ≤ 𝑗𝑗𝑁)))
275238, 16, 274syl2anr 595 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗 ∈ (1...𝑁) ↔ (1 ≤ 𝑗𝑗𝑁)))
276275adantr 479 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → (𝑗 ∈ (1...𝑁) ↔ (1 ≤ 𝑗𝑗𝑁)))
277268, 271, 276mpbir2and 711 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗 ∈ (1...𝑁))
278 elfzmlbm 13646 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑁) → (𝑗 − 1) ∈ (0...(𝑁 − 1)))
279277, 278syl 17 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → (𝑗 − 1) ∈ (0...(𝑁 − 1)))
280248, 279ifclda 4565 . . . . . . . . . 10 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) ∈ (0...(𝑁 − 1)))
281 breq1 5152 . . . . . . . . . . . . . . . 16 (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 < 𝑉 ↔ if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉))
282 id 22 . . . . . . . . . . . . . . . 16 (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → 𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)))
283 oveq1 7426 . . . . . . . . . . . . . . . 16 (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 + 1) = (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))
284281, 282, 283ifbieq12d 4558 . . . . . . . . . . . . . . 15 (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)) = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)))
285284eqeq2d 2736 . . . . . . . . . . . . . 14 (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)) ↔ 𝑗 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))))
286 breq1 5152 . . . . . . . . . . . . . . . 16 ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → ((𝑗 − 1) < 𝑉 ↔ if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉))
287 id 22 . . . . . . . . . . . . . . . 16 ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)))
288 oveq1 7426 . . . . . . . . . . . . . . . 16 ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → ((𝑗 − 1) + 1) = (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))
289286, 287, 288ifbieq12d 4558 . . . . . . . . . . . . . . 15 ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → if((𝑗 − 1) < 𝑉, (𝑗 − 1), ((𝑗 − 1) + 1)) = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)))
290289eqeq2d 2736 . . . . . . . . . . . . . 14 ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 = if((𝑗 − 1) < 𝑉, (𝑗 − 1), ((𝑗 − 1) + 1)) ↔ 𝑗 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))))
291 iftrue 4536 . . . . . . . . . . . . . . . 16 (𝑗 < 𝑉 → if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)) = 𝑗)
292291eqcomd 2731 . . . . . . . . . . . . . . 15 (𝑗 < 𝑉𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)))
293292adantl 480 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)))
294 zlem1lt 12647 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ℤ ∧ 𝑉 ∈ ℤ) → (𝑗𝑉 ↔ (𝑗 − 1) < 𝑉))
295238, 198, 294syl2anr 595 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗𝑉 ↔ (𝑗 − 1) < 𝑉))
296258necomd 2985 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑉𝑗)
297296adantl 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → 𝑉𝑗)
298 ltlen 11347 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑗 < 𝑉 ↔ (𝑗𝑉𝑉𝑗)))
299228, 199, 298syl2anr 595 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗 < 𝑉 ↔ (𝑗𝑉𝑉𝑗)))
300299biimprd 247 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → ((𝑗𝑉𝑉𝑗) → 𝑗 < 𝑉))
301297, 300mpan2d 692 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗𝑉𝑗 < 𝑉))
302295, 301sylbird 259 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → ((𝑗 − 1) < 𝑉𝑗 < 𝑉))
303302con3dimp 407 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → ¬ (𝑗 − 1) < 𝑉)
304303iffalsed 4541 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → if((𝑗 − 1) < 𝑉, (𝑗 − 1), ((𝑗 − 1) + 1)) = ((𝑗 − 1) + 1))
305225nn0cnd 12567 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ ℂ)
306 npcan1 11671 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℂ → ((𝑗 − 1) + 1) = 𝑗)
307305, 306syl 17 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → ((𝑗 − 1) + 1) = 𝑗)
308307ad2antlr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → ((𝑗 − 1) + 1) = 𝑗)
309304, 308eqtr2d 2766 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗 = if((𝑗 − 1) < 𝑉, (𝑗 − 1), ((𝑗 − 1) + 1)))
310285, 290, 293, 309ifbothda 4568 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → 𝑗 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)))
311 csbeq1a 3903 . . . . . . . . . . . . 13 (𝑗 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) → 𝑇, 𝑈⟩ / 𝑠𝐶 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
312310, 311syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → 𝑇, 𝑈⟩ / 𝑠𝐶 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
313312eqeq2d 2736 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
314313biimpd 228 . . . . . . . . . 10 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
315 breq1 5152 . . . . . . . . . . . . . 14 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑦 < 𝑉 ↔ if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉))
316 id 22 . . . . . . . . . . . . . 14 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → 𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)))
317 oveq1 7426 . . . . . . . . . . . . . 14 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑦 + 1) = (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))
318315, 316, 317ifbieq12d 4558 . . . . . . . . . . . . 13 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)))
319318csbeq1d 3893 . . . . . . . . . . . 12 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
320319eqeq2d 2736 . . . . . . . . . . 11 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
321320rspcev 3606 . . . . . . . . . 10 ((if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) ∈ (0...(𝑁 − 1)) ∧ 𝑖 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
322280, 314, 321syl6an 682 . . . . . . . . 9 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
323322ex 411 . . . . . . . 8 (𝜑 → (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)))
324221, 223, 323rexlimd 3253 . . . . . . 7 (𝜑 → (∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
325220, 324impbid 211 . . . . . 6 (𝜑 → (∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
326185, 325bitr3d 280 . . . . 5 (𝜑 → (𝑖 ∈ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ↔ ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
327326ralbidv 3167 . . . 4 (𝜑 → (∀𝑖 ∈ (0...(𝑁 − 1))𝑖 ∈ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
328129, 327bitrid 282 . . 3 (𝜑 → ((0...(𝑁 − 1)) ⊆ ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) ↔ ∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
329328anbi1d 629 . 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)))
33012, 45, 52, 197poimirlem23 37247 . . 3 (𝜑 → (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁))))
331330anbi2d 628 . 2 (𝜑 → ((∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ ∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0) ↔ (∀𝑖 ∈ (0...(𝑁 − 1))∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 ∧ ¬ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁)))))
332128, 329, 3313bitrd 304 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 205  wa 394  wo 845   = wceq 1533  wcel 2098  wne 2929  wral 3050  wrex 3059  Vcvv 3461  csb 3889  cdif 3941  cun 3942  cin 3943  wss 3944  c0 4322  ifcif 4530  {csn 4630  cop 4636   class class class wbr 5149  cmpt 5232   × cxp 5676  ccnv 5677  ran crn 5679  cima 5681  Fun wfun 6543  wf 6545  ontowfo 6547  1-1-ontowf1o 6548  cfv 6549  (class class class)co 7419  f cof 7683  1st c1st 7992  2nd c2nd 7993  m cmap 8845  cc 11138  cr 11139  0cc0 11140  1c1 11141   + caddc 11143   < clt 11280  cle 11281  cmin 11476  cn 12245  0cn0 12505  cz 12591  cuz 12855  ...cfz 13519  ..^cfzo 13662
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-cnex 11196  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216  ax-pre-mulgt0 11217
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-of 7685  df-om 7872  df-1st 7994  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-er 8725  df-map 8847  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-sub 11478  df-neg 11479  df-nn 12246  df-n0 12506  df-z 12592  df-uz 12856  df-fz 13520  df-fzo 13663
This theorem is referenced by:  poimirlem27  37251
  Copyright terms: Public domain W3C validator