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 35899
Description: Lemma for poimir 35908, 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 1916 . . . . . . . . 9 𝑗(𝜑𝑦 ∈ (0...(𝑁 − 1)))
2 nfcsb1v 3867 . . . . . . . . . 10 𝑗𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))
3 nfcv 2904 . . . . . . . . . 10 𝑗(1...𝑁)
4 nfcv 2904 . . . . . . . . . 10 𝑗(0...𝐾)
52, 3, 4nff 6641 . . . . . . . . 9 𝑗𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)
61, 5nfim 1898 . . . . . . . 8 𝑗((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
7 eleq1 2824 . . . . . . . . . 10 (𝑗 = 𝑦 → (𝑗 ∈ (0...(𝑁 − 1)) ↔ 𝑦 ∈ (0...(𝑁 − 1))))
87anbi2d 629 . . . . . . . . 9 (𝑗 = 𝑦 → ((𝜑𝑗 ∈ (0...(𝑁 − 1))) ↔ (𝜑𝑦 ∈ (0...(𝑁 − 1)))))
9 csbeq1a 3856 . . . . . . . . . 10 (𝑗 = 𝑦 → (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = 𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
109feq1d 6630 . . . . . . . . 9 (𝑗 = 𝑦 → ((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) ↔ 𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))
118, 10imbi12d 344 . . . . . . . 8 (𝑗 = 𝑦 → (((𝜑𝑗 ∈ (0...(𝑁 − 1))) → (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)) ↔ ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))))
12 poimir.0 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℕ)
1312nncnd 12082 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℂ)
14 npcan1 11493 . . . . . . . . . . . . 13 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
1513, 14syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
1612nnzd 12518 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
17 peano2zm 12456 . . . . . . . . . . . . . 14 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
1816, 17syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑁 − 1) ∈ ℤ)
19 uzid 12690 . . . . . . . . . . . . 13 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
20 peano2uz 12734 . . . . . . . . . . . . 13 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
2118, 19, 203syl 18 . . . . . . . . . . . 12 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
2215, 21eqeltrrd 2838 . . . . . . . . . . 11 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
23 fzss2 13389 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (0...(𝑁 − 1)) ⊆ (0...𝑁))
2422, 23syl 17 . . . . . . . . . 10 (𝜑 → (0...(𝑁 − 1)) ⊆ (0...𝑁))
2524sselda 3931 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → 𝑗 ∈ (0...𝑁))
26 elun 4094 . . . . . . . . . . . . 13 (𝑦 ∈ ({1} ∪ {0}) ↔ (𝑦 ∈ {1} ∨ 𝑦 ∈ {0}))
27 fzofzp1 13577 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0..^𝐾) → (𝑥 + 1) ∈ (0...𝐾))
28 elsni 4589 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {1} → 𝑦 = 1)
2928oveq2d 7345 . . . . . . . . . . . . . . . 16 (𝑦 ∈ {1} → (𝑥 + 𝑦) = (𝑥 + 1))
3029eleq1d 2821 . . . . . . . . . . . . . . 15 (𝑦 ∈ {1} → ((𝑥 + 𝑦) ∈ (0...𝐾) ↔ (𝑥 + 1) ∈ (0...𝐾)))
3127, 30syl5ibrcom 246 . . . . . . . . . . . . . 14 (𝑥 ∈ (0..^𝐾) → (𝑦 ∈ {1} → (𝑥 + 𝑦) ∈ (0...𝐾)))
32 elfzoelz 13480 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (0..^𝐾) → 𝑥 ∈ ℤ)
3332zcnd 12520 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (0..^𝐾) → 𝑥 ∈ ℂ)
3433addid1d 11268 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (0..^𝐾) → (𝑥 + 0) = 𝑥)
35 elfzofz 13496 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (0..^𝐾) → 𝑥 ∈ (0...𝐾))
3634, 35eqeltrd 2837 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0..^𝐾) → (𝑥 + 0) ∈ (0...𝐾))
37 elsni 4589 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {0} → 𝑦 = 0)
3837oveq2d 7345 . . . . . . . . . . . . . . . 16 (𝑦 ∈ {0} → (𝑥 + 𝑦) = (𝑥 + 0))
3938eleq1d 2821 . . . . . . . . . . . . . . 15 (𝑦 ∈ {0} → ((𝑥 + 𝑦) ∈ (0...𝐾) ↔ (𝑥 + 0) ∈ (0...𝐾)))
4036, 39syl5ibrcom 246 . . . . . . . . . . . . . 14 (𝑥 ∈ (0..^𝐾) → (𝑦 ∈ {0} → (𝑥 + 𝑦) ∈ (0...𝐾)))
4131, 40jaod 856 . . . . . . . . . . . . 13 (𝑥 ∈ (0..^𝐾) → ((𝑦 ∈ {1} ∨ 𝑦 ∈ {0}) → (𝑥 + 𝑦) ∈ (0...𝐾)))
4226, 41biimtrid 241 . . . . . . . . . . . 12 (𝑥 ∈ (0..^𝐾) → (𝑦 ∈ ({1} ∪ {0}) → (𝑥 + 𝑦) ∈ (0...𝐾)))
4342imp 407 . . . . . . . . . . 11 ((𝑥 ∈ (0..^𝐾) ∧ 𝑦 ∈ ({1} ∪ {0})) → (𝑥 + 𝑦) ∈ (0...𝐾))
4443adantl 482 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ (0..^𝐾) ∧ 𝑦 ∈ ({1} ∪ {0}))) → (𝑥 + 𝑦) ∈ (0...𝐾))
45 poimirlem25.3 . . . . . . . . . . 11 (𝜑𝑇:(1...𝑁)⟶(0..^𝐾))
4645adantr 481 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇:(1...𝑁)⟶(0..^𝐾))
47 1ex 11064 . . . . . . . . . . . . . 14 1 ∈ V
4847fconst 6705 . . . . . . . . . . . . 13 ((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1}
49 c0ex 11062 . . . . . . . . . . . . . 14 0 ∈ V
5049fconst 6705 . . . . . . . . . . . . 13 ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}
5148, 50pm3.2i 471 . . . . . . . . . . . 12 (((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0})
52 poimirlem25.4 . . . . . . . . . . . . . 14 (𝜑𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
53 dff1o3 6767 . . . . . . . . . . . . . . 15 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun 𝑈))
5453simprbi 497 . . . . . . . . . . . . . 14 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun 𝑈)
55 imain 6563 . . . . . . . . . . . . . 14 (Fun 𝑈 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))))
5652, 54, 553syl 18 . . . . . . . . . . . . 13 (𝜑 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))))
57 elfznn0 13442 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ0)
5857nn0red 12387 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
5958ltp1d 11998 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1))
60 fzdisj 13376 . . . . . . . . . . . . . . . 16 (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
6159, 60syl 17 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
6261imaeq2d 5993 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (𝑈 “ ∅))
63 ima0 6009 . . . . . . . . . . . . . 14 (𝑈 “ ∅) = ∅
6462, 63eqtrdi 2792 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
6556, 64sylan9req 2797 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
66 fun 6681 . . . . . . . . . . . 12 (((((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}) ∧ ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
6751, 65, 66sylancr 587 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
68 nn0p1nn 12365 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
6957, 68syl 17 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ)
70 nnuz 12714 . . . . . . . . . . . . . . . . 17 ℕ = (ℤ‘1)
7169, 70eleqtrdi 2847 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (ℤ‘1))
72 elfzuz3 13346 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ𝑗))
73 fzsplit2 13374 . . . . . . . . . . . . . . . 16 (((𝑗 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
7471, 72, 73syl2anc 584 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
7574imaeq2d 5993 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑁) → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))))
76 imaundi 6082 . . . . . . . . . . . . . 14 (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))
7775, 76eqtr2di 2793 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑁) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (𝑈 “ (1...𝑁)))
78 f1ofo 6768 . . . . . . . . . . . . . 14 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁))
79 foima 6738 . . . . . . . . . . . . . 14 (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁))
8052, 78, 793syl 18 . . . . . . . . . . . . 13 (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁))
8177, 80sylan9eqr 2798 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (1...𝑁))
8281feq2d 6631 . . . . . . . . . . 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 7362 . . . . . . . . . . 11 (1...𝑁) ∈ V
8584a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ V)
86 inidm 4164 . . . . . . . . . 10 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
8744, 46, 83, 85, 85, 86off 7605 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
8825, 87syldan 591 . . . . . . . 8 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
896, 11, 88chvarfv 2232 . . . . . . 7 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
90 fzp1elp1 13402 . . . . . . . . 9 (𝑦 ∈ (0...(𝑁 − 1)) → (𝑦 + 1) ∈ (0...((𝑁 − 1) + 1)))
9115oveq2d 7345 . . . . . . . . . . 11 (𝜑 → (0...((𝑁 − 1) + 1)) = (0...𝑁))
9291eleq2d 2822 . . . . . . . . . 10 (𝜑 → ((𝑦 + 1) ∈ (0...((𝑁 − 1) + 1)) ↔ (𝑦 + 1) ∈ (0...𝑁)))
9392biimpa 477 . . . . . . . . 9 ((𝜑 ∧ (𝑦 + 1) ∈ (0...((𝑁 − 1) + 1))) → (𝑦 + 1) ∈ (0...𝑁))
9490, 93sylan2 593 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 + 1) ∈ (0...𝑁))
95 nfv 1916 . . . . . . . . . 10 𝑗(𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁))
96 nfcsb1v 3867 . . . . . . . . . . 11 𝑗(𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))
9796, 3, 4nff 6641 . . . . . . . . . 10 𝑗(𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)
9895, 97nfim 1898 . . . . . . . . 9 𝑗((𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁)) → (𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
99 ovex 7362 . . . . . . . . 9 (𝑦 + 1) ∈ V
100 eleq1 2824 . . . . . . . . . . 11 (𝑗 = (𝑦 + 1) → (𝑗 ∈ (0...𝑁) ↔ (𝑦 + 1) ∈ (0...𝑁)))
101100anbi2d 629 . . . . . . . . . 10 (𝑗 = (𝑦 + 1) → ((𝜑𝑗 ∈ (0...𝑁)) ↔ (𝜑 ∧ (𝑦 + 1) ∈ (0...𝑁))))
102 csbeq1a 3856 . . . . . . . . . . 11 (𝑗 = (𝑦 + 1) → (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
103102feq1d 6630 . . . . . . . . . 10 (𝑗 = (𝑦 + 1) → ((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) ↔ (𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))
104101, 103imbi12d 344 . . . . . . . . 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 591 . . . . . . 7 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
107 csbeq1 3845 . . . . . . . . 9 (𝑦 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → 𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
108107feq1d 6630 . . . . . . . 8 (𝑦 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → (𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) ↔ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))
109 csbeq1 3845 . . . . . . . . 9 ((𝑦 + 1) = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → (𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
110109feq1d 6630 . . . . . . . 8 ((𝑦 + 1) = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → ((𝑦 + 1) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾) ↔ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾)))
111108, 110ifboth 4511 . . . . . . 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 584 . . . . . 6 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝐾))
113 ovex 7362 . . . . . . 7 (0...𝐾) ∈ V
114113, 84elmap 8722 . . . . . 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 7039 . . . 4 (𝜑 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))):(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁)))
117 ovex 7362 . . . . 5 ((0...𝐾) ↑m (1...𝑁)) ∈ V
118 ovex 7362 . . . . 5 (0...(𝑁 − 1)) ∈ V
119117, 118elmap 8722 . . . 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 5871 . . . . . . . 8 (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → ran 𝑥 = ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))
122121mpteq1d 5184 . . . . . . 7 (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → (𝑝 ∈ ran 𝑥𝐵) = (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵))
123122rneqd 5873 . . . . . 6 (𝑥 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) → ran (𝑝 ∈ ran 𝑥𝐵) = ran (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵))
124123sseq2d 3963 . . . . 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 3310 . . . . 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 631 . . . 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 3594 . . 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 3919 . . . 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 7362 . . . . . . . . . . . . 13 ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
131 poimirlem28.1 . . . . . . . . . . . . 13 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝐵 = 𝐶)
132130, 131csbie 3878 . . . . . . . . . . . 12 ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵 = 𝐶
133132csbeq2i 3850 . . . . . . . . . . 11 𝑇, 𝑈⟩ / 𝑠((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵 = 𝑇, 𝑈⟩ / 𝑠𝐶
134 opex 5403 . . . . . . . . . . . . 13 𝑇, 𝑈⟩ ∈ V
135134a1i 11 . . . . . . . . . . . 12 (𝜑 → ⟨𝑇, 𝑈⟩ ∈ V)
136 fveq2 6819 . . . . . . . . . . . . . . 15 (𝑠 = ⟨𝑇, 𝑈⟩ → (1st𝑠) = (1st ‘⟨𝑇, 𝑈⟩))
137 fex 7152 . . . . . . . . . . . . . . . . 17 ((𝑇:(1...𝑁)⟶(0..^𝐾) ∧ (1...𝑁) ∈ V) → 𝑇 ∈ V)
13845, 84, 137sylancl 586 . . . . . . . . . . . . . . . 16 (𝜑𝑇 ∈ V)
139 f1oexrnex 7834 . . . . . . . . . . . . . . . . 17 ((𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ∧ (1...𝑁) ∈ V) → 𝑈 ∈ V)
14052, 84, 139sylancl 586 . . . . . . . . . . . . . . . 16 (𝜑𝑈 ∈ V)
141 op1stg 7903 . . . . . . . . . . . . . . . 16 ((𝑇 ∈ V ∧ 𝑈 ∈ V) → (1st ‘⟨𝑇, 𝑈⟩) = 𝑇)
142138, 140, 141syl2anc 584 . . . . . . . . . . . . . . 15 (𝜑 → (1st ‘⟨𝑇, 𝑈⟩) = 𝑇)
143136, 142sylan9eqr 2798 . . . . . . . . . . . . . 14 ((𝜑𝑠 = ⟨𝑇, 𝑈⟩) → (1st𝑠) = 𝑇)
144 fveq2 6819 . . . . . . . . . . . . . . . 16 (𝑠 = ⟨𝑇, 𝑈⟩ → (2nd𝑠) = (2nd ‘⟨𝑇, 𝑈⟩))
145 op2ndg 7904 . . . . . . . . . . . . . . . . 17 ((𝑇 ∈ V ∧ 𝑈 ∈ V) → (2nd ‘⟨𝑇, 𝑈⟩) = 𝑈)
146138, 140, 145syl2anc 584 . . . . . . . . . . . . . . . 16 (𝜑 → (2nd ‘⟨𝑇, 𝑈⟩) = 𝑈)
147144, 146sylan9eqr 2798 . . . . . . . . . . . . . . 15 ((𝜑𝑠 = ⟨𝑇, 𝑈⟩) → (2nd𝑠) = 𝑈)
148 imaeq1 5988 . . . . . . . . . . . . . . . . 17 ((2nd𝑠) = 𝑈 → ((2nd𝑠) “ (1...𝑗)) = (𝑈 “ (1...𝑗)))
149148xpeq1d 5643 . . . . . . . . . . . . . . . 16 ((2nd𝑠) = 𝑈 → (((2nd𝑠) “ (1...𝑗)) × {1}) = ((𝑈 “ (1...𝑗)) × {1}))
150 imaeq1 5988 . . . . . . . . . . . . . . . . 17 ((2nd𝑠) = 𝑈 → ((2nd𝑠) “ ((𝑗 + 1)...𝑁)) = (𝑈 “ ((𝑗 + 1)...𝑁)))
151150xpeq1d 5643 . . . . . . . . . . . . . . . 16 ((2nd𝑠) = 𝑈 → (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))
152149, 151uneq12d 4110 . . . . . . . . . . . . . . 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 7347 . . . . . . . . . . . . 13 ((𝜑𝑠 = ⟨𝑇, 𝑈⟩) → ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
155154csbeq1d 3846 . . . . . . . . . . . 12 ((𝜑𝑠 = ⟨𝑇, 𝑈⟩) → ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵 = (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
156135, 155csbied 3880 . . . . . . . . . . 11 (𝜑𝑇, 𝑈⟩ / 𝑠((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵 = (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
157133, 156eqtr3id 2790 . . . . . . . . . 10 (𝜑𝑇, 𝑈⟩ / 𝑠𝐶 = (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
158157csbeq2dv 3849 . . . . . . . . 9 (𝜑if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
159158eqeq2d 2747 . . . . . . . 8 (𝜑 → (𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵))
160159rexbidv 3171 . . . . . . 7 (𝜑 → (∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 ↔ ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵))
161 vex 3445 . . . . . . . . 9 𝑖 ∈ V
162 eqid 2736 . . . . . . . . . 10 (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵) = (𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) ↦ 𝐵)
163162elrnmpt 5891 . . . . . . . . 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 1916 . . . . . . . . 9 𝑘 𝑖 = 𝐵
166 nfcsb1v 3867 . . . . . . . . . 10 𝑝𝑘 / 𝑝𝐵
167166nfeq2 2921 . . . . . . . . 9 𝑝 𝑖 = 𝑘 / 𝑝𝐵
168 csbeq1a 3856 . . . . . . . . . 10 (𝑝 = 𝑘𝐵 = 𝑘 / 𝑝𝐵)
169168eqeq2d 2747 . . . . . . . . 9 (𝑝 = 𝑘 → (𝑖 = 𝐵𝑖 = 𝑘 / 𝑝𝐵))
170165, 167, 169cbvrexw 3286 . . . . . . . 8 (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))𝑖 = 𝐵 ↔ ∃𝑘 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))𝑖 = 𝑘 / 𝑝𝐵)
171 ovex 7362 . . . . . . . . . . 11 (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
172171csbex 5252 . . . . . . . . . 10 if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
173172rgenw 3065 . . . . . . . . 9 𝑦 ∈ (0...(𝑁 − 1))if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
174 eqid 2736 . . . . . . . . . 10 (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
175 csbeq1 3845 . . . . . . . . . . . 12 (𝑘 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝑘 / 𝑝𝐵 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
176 vex 3445 . . . . . . . . . . . . . 14 𝑦 ∈ V
177176, 99ifex 4522 . . . . . . . . . . . . 13 if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) ∈ V
178 csbnestgw 4367 . . . . . . . . . . . . 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 2794 . . . . . . . . . . 11 (𝑘 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → 𝑘 / 𝑝𝐵 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵)
181180eqeq2d 2747 . . . . . . . . . 10 (𝑘 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑖 = 𝑘 / 𝑝𝐵𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) / 𝑝𝐵))
182174, 181rexrnmptw 7021 . . . . . . . . 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 3931 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ (0...𝑁))
187186adantr 481 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < 𝑉) → 𝑦 ∈ (0...𝑁))
188 elfzelz 13349 . . . . . . . . . . . . . 14 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℤ)
189188zred 12519 . . . . . . . . . . . . 13 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ)
190189adantl 482 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ ℝ)
191 ltne 11165 . . . . . . . . . . . . 13 ((𝑦 ∈ ℝ ∧ 𝑦 < 𝑉) → 𝑉𝑦)
192191necomd 2996 . . . . . . . . . . . 12 ((𝑦 ∈ ℝ ∧ 𝑦 < 𝑉) → 𝑦𝑉)
193190, 192sylan 580 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < 𝑉) → 𝑦𝑉)
194 eldifsn 4733 . . . . . . . . . . 11 (𝑦 ∈ ((0...𝑁) ∖ {𝑉}) ↔ (𝑦 ∈ (0...𝑁) ∧ 𝑦𝑉))
195187, 193, 194sylanbrc 583 . . . . . . . . . 10 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑦 < 𝑉) → 𝑦 ∈ ((0...𝑁) ∖ {𝑉}))
19694adantr 481 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → (𝑦 + 1) ∈ (0...𝑁))
197 poimirlem24.5 . . . . . . . . . . . . . . 15 (𝜑𝑉 ∈ (0...𝑁))
198197elfzelzd 13350 . . . . . . . . . . . . . 14 (𝜑𝑉 ∈ ℤ)
199198zred 12519 . . . . . . . . . . . . 13 (𝜑𝑉 ∈ ℝ)
200199ad2antrr 723 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → 𝑉 ∈ ℝ)
201 zre 12416 . . . . . . . . . . . . . . . 16 (𝑉 ∈ ℤ → 𝑉 ∈ ℝ)
202 zre 12416 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℤ → 𝑦 ∈ ℝ)
203 lenlt 11146 . . . . . . . . . . . . . . . 16 ((𝑉 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑉𝑦 ↔ ¬ 𝑦 < 𝑉))
204201, 202, 203syl2an 596 . . . . . . . . . . . . . . 15 ((𝑉 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑉𝑦 ↔ ¬ 𝑦 < 𝑉))
205 zleltp1 12464 . . . . . . . . . . . . . . 15 ((𝑉 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑉𝑦𝑉 < (𝑦 + 1)))
206204, 205bitr3d 280 . . . . . . . . . . . . . 14 ((𝑉 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (¬ 𝑦 < 𝑉𝑉 < (𝑦 + 1)))
207198, 188, 206syl2an 596 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (¬ 𝑦 < 𝑉𝑉 < (𝑦 + 1)))
208207biimpa 477 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → 𝑉 < (𝑦 + 1))
209200, 208gtned 11203 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → (𝑦 + 1) ≠ 𝑉)
210 eldifsn 4733 . . . . . . . . . . 11 ((𝑦 + 1) ∈ ((0...𝑁) ∖ {𝑉}) ↔ ((𝑦 + 1) ∈ (0...𝑁) ∧ (𝑦 + 1) ≠ 𝑉))
211196, 209, 210sylanbrc 583 . . . . . . . . . 10 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ ¬ 𝑦 < 𝑉) → (𝑦 + 1) ∈ ((0...𝑁) ∖ {𝑉}))
212195, 211ifclda 4507 . . . . . . . . 9 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) ∈ ((0...𝑁) ∖ {𝑉}))
213 nfcsb1v 3867 . . . . . . . . . . . 12 𝑗if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
214213nfeq2 2921 . . . . . . . . . . 11 𝑗 𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
215 csbeq1a 3856 . . . . . . . . . . . 12 (𝑗 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → 𝑇, 𝑈⟩ / 𝑠𝐶 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
216215eqeq2d 2747 . . . . . . . . . . 11 (𝑗 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
217214, 216rspce 3559 . . . . . . . . . 10 ((if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) ∈ ((0...𝑁) ∖ {𝑉}) ∧ 𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶)
218217ex 413 . . . . . . . . 9 (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) ∈ ((0...𝑁) ∖ {𝑉}) → (𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
219212, 218syl 17 . . . . . . . 8 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
220219rexlimdva 3148 . . . . . . 7 (𝜑 → (∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑗 ∈ ((0...𝑁) ∖ {𝑉})𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶))
221 nfv 1916 . . . . . . . 8 𝑗𝜑
222 nfcv 2904 . . . . . . . . 9 𝑗(0...(𝑁 − 1))
223222, 214nfrexw 3292 . . . . . . . 8 𝑗𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶
224 eldifi 4072 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ (0...𝑁))
225224, 57syl 17 . . . . . . . . . . . . . 14 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ ℕ0)
226225nn0ge0d 12389 . . . . . . . . . . . . 13 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 0 ≤ 𝑗)
227226ad2antlr 724 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 0 ≤ 𝑗)
228225nn0red 12387 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ ℝ)
229228ad2antlr 724 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 ∈ ℝ)
230199ad2antrr 723 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑉 ∈ ℝ)
23116zred 12519 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℝ)
232231ad2antrr 723 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑁 ∈ ℝ)
233 simpr 485 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 < 𝑉)
234 elfzle2 13353 . . . . . . . . . . . . . . . 16 (𝑉 ∈ (0...𝑁) → 𝑉𝑁)
235197, 234syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑉𝑁)
236235ad2antrr 723 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑉𝑁)
237229, 230, 232, 233, 236ltletrd 11228 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 < 𝑁)
238224elfzelzd 13350 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ ℤ)
239 zltlem1 12466 . . . . . . . . . . . . . . 15 ((𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 < 𝑁𝑗 ≤ (𝑁 − 1)))
240238, 16, 239syl2anr 597 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗 < 𝑁𝑗 ≤ (𝑁 − 1)))
241240adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → (𝑗 < 𝑁𝑗 ≤ (𝑁 − 1)))
242237, 241mpbid 231 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 ≤ (𝑁 − 1))
243 0z 12423 . . . . . . . . . . . . . . 15 0 ∈ ℤ
244 elfz 13338 . . . . . . . . . . . . . . 15 ((𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑗 ∈ (0...(𝑁 − 1)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝑁 − 1))))
245243, 244mp3an2 1448 . . . . . . . . . . . . . 14 ((𝑗 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑗 ∈ (0...(𝑁 − 1)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝑁 − 1))))
246238, 18, 245syl2anr 597 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗 ∈ (0...(𝑁 − 1)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝑁 − 1))))
247246adantr 481 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → (𝑗 ∈ (0...(𝑁 − 1)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝑁 − 1))))
248227, 242, 247mpbir2and 710 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 ∈ (0...(𝑁 − 1)))
249 0red 11071 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 0 ∈ ℝ)
250199ad2antrr 723 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑉 ∈ ℝ)
251228ad2antlr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗 ∈ ℝ)
252 elfzle1 13352 . . . . . . . . . . . . . . . . 17 (𝑉 ∈ (0...𝑁) → 0 ≤ 𝑉)
253197, 252syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ 𝑉)
254253ad2antrr 723 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 0 ≤ 𝑉)
255 lenlt 11146 . . . . . . . . . . . . . . . . . 18 ((𝑉 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑉𝑗 ↔ ¬ 𝑗 < 𝑉))
256199, 228, 255syl2an 596 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑉𝑗 ↔ ¬ 𝑗 < 𝑉))
257256biimpar 478 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑉𝑗)
258 eldifsni 4736 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗𝑉)
259258ad2antlr 724 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗𝑉)
260 ltlen 11169 . . . . . . . . . . . . . . . . . 18 ((𝑉 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑉 < 𝑗 ↔ (𝑉𝑗𝑗𝑉)))
261199, 228, 260syl2an 596 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑉 < 𝑗 ↔ (𝑉𝑗𝑗𝑉)))
262261adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → (𝑉 < 𝑗 ↔ (𝑉𝑗𝑗𝑉)))
263257, 259, 262mpbir2and 710 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑉 < 𝑗)
264249, 250, 251, 254, 263lelttrd 11226 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 0 < 𝑗)
265 zgt0ge1 12467 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℤ → (0 < 𝑗 ↔ 1 ≤ 𝑗))
266238, 265syl 17 . . . . . . . . . . . . . . 15 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → (0 < 𝑗 ↔ 1 ≤ 𝑗))
267266ad2antlr 724 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → (0 < 𝑗 ↔ 1 ≤ 𝑗))
268264, 267mpbid 231 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 1 ≤ 𝑗)
269 elfzle2 13353 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑁) → 𝑗𝑁)
270224, 269syl 17 . . . . . . . . . . . . . 14 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗𝑁)
271270ad2antlr 724 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗𝑁)
272 1z 12443 . . . . . . . . . . . . . . . 16 1 ∈ ℤ
273 elfz 13338 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 ∈ (1...𝑁) ↔ (1 ≤ 𝑗𝑗𝑁)))
274272, 273mp3an2 1448 . . . . . . . . . . . . . . 15 ((𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 ∈ (1...𝑁) ↔ (1 ≤ 𝑗𝑗𝑁)))
275238, 16, 274syl2anr 597 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗 ∈ (1...𝑁) ↔ (1 ≤ 𝑗𝑗𝑁)))
276275adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → (𝑗 ∈ (1...𝑁) ↔ (1 ≤ 𝑗𝑗𝑁)))
277268, 271, 276mpbir2and 710 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗 ∈ (1...𝑁))
278 elfzmlbm 13459 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑁) → (𝑗 − 1) ∈ (0...(𝑁 − 1)))
279277, 278syl 17 . . . . . . . . . . 11 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → (𝑗 − 1) ∈ (0...(𝑁 − 1)))
280248, 279ifclda 4507 . . . . . . . . . 10 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) ∈ (0...(𝑁 − 1)))
281 breq1 5092 . . . . . . . . . . . . . . . 16 (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 < 𝑉 ↔ if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉))
282 id 22 . . . . . . . . . . . . . . . 16 (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → 𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)))
283 oveq1 7336 . . . . . . . . . . . . . . . 16 (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 + 1) = (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))
284281, 282, 283ifbieq12d 4500 . . . . . . . . . . . . . . 15 (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)) = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)))
285284eqeq2d 2747 . . . . . . . . . . . . . 14 (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)) ↔ 𝑗 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))))
286 breq1 5092 . . . . . . . . . . . . . . . 16 ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → ((𝑗 − 1) < 𝑉 ↔ if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉))
287 id 22 . . . . . . . . . . . . . . . 16 ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)))
288 oveq1 7336 . . . . . . . . . . . . . . . 16 ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → ((𝑗 − 1) + 1) = (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))
289286, 287, 288ifbieq12d 4500 . . . . . . . . . . . . . . 15 ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → if((𝑗 − 1) < 𝑉, (𝑗 − 1), ((𝑗 − 1) + 1)) = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)))
290289eqeq2d 2747 . . . . . . . . . . . . . 14 ((𝑗 − 1) = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑗 = if((𝑗 − 1) < 𝑉, (𝑗 − 1), ((𝑗 − 1) + 1)) ↔ 𝑗 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))))
291 iftrue 4478 . . . . . . . . . . . . . . . 16 (𝑗 < 𝑉 → if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)) = 𝑗)
292291eqcomd 2742 . . . . . . . . . . . . . . 15 (𝑗 < 𝑉𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)))
293292adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ 𝑗 < 𝑉) → 𝑗 = if(𝑗 < 𝑉, 𝑗, (𝑗 + 1)))
294 zlem1lt 12465 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ℤ ∧ 𝑉 ∈ ℤ) → (𝑗𝑉 ↔ (𝑗 − 1) < 𝑉))
295238, 198, 294syl2anr 597 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗𝑉 ↔ (𝑗 − 1) < 𝑉))
296258necomd 2996 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑉𝑗)
297296adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → 𝑉𝑗)
298 ltlen 11169 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑗 < 𝑉 ↔ (𝑗𝑉𝑉𝑗)))
299228, 199, 298syl2anr 597 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗 < 𝑉 ↔ (𝑗𝑉𝑉𝑗)))
300299biimprd 247 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → ((𝑗𝑉𝑉𝑗) → 𝑗 < 𝑉))
301297, 300mpan2d 691 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑗𝑉𝑗 < 𝑉))
302295, 301sylbird 259 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → ((𝑗 − 1) < 𝑉𝑗 < 𝑉))
303302con3dimp 409 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → ¬ (𝑗 − 1) < 𝑉)
304303iffalsed 4483 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → if((𝑗 − 1) < 𝑉, (𝑗 − 1), ((𝑗 − 1) + 1)) = ((𝑗 − 1) + 1))
305225nn0cnd 12388 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑗 ∈ ℂ)
306 npcan1 11493 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ℂ → ((𝑗 − 1) + 1) = 𝑗)
307305, 306syl 17 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → ((𝑗 − 1) + 1) = 𝑗)
308307ad2antlr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → ((𝑗 − 1) + 1) = 𝑗)
309304, 308eqtr2d 2777 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) ∧ ¬ 𝑗 < 𝑉) → 𝑗 = if((𝑗 − 1) < 𝑉, (𝑗 − 1), ((𝑗 − 1) + 1)))
310285, 290, 293, 309ifbothda 4510 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → 𝑗 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)))
311 csbeq1a 3856 . . . . . . . . . . . . 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 2747 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
314313biimpd 228 . . . . . . . . . 10 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
315 breq1 5092 . . . . . . . . . . . . . 14 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑦 < 𝑉 ↔ if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉))
316 id 22 . . . . . . . . . . . . . 14 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → 𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)))
317 oveq1 7336 . . . . . . . . . . . . . 14 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑦 + 1) = (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1))
318315, 316, 317ifbieq12d 4500 . . . . . . . . . . . . 13 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)))
319318csbeq1d 3846 . . . . . . . . . . . 12 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
320319eqeq2d 2747 . . . . . . . . . . 11 (𝑦 = if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) → (𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶𝑖 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
321320rspcev 3570 . . . . . . . . . 10 ((if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) ∈ (0...(𝑁 − 1)) ∧ 𝑖 = if(if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) < 𝑉, if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)), (if(𝑗 < 𝑉, 𝑗, (𝑗 − 1)) + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶) → ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)
322280, 314, 321syl6an 681 . . . . . . . . 9 ((𝜑𝑗 ∈ ((0...𝑁) ∖ {𝑉})) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶))
323322ex 413 . . . . . . . 8 (𝜑 → (𝑗 ∈ ((0...𝑁) ∖ {𝑉}) → (𝑖 = 𝑇, 𝑈⟩ / 𝑠𝐶 → ∃𝑦 ∈ (0...(𝑁 − 1))𝑖 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗𝑇, 𝑈⟩ / 𝑠𝐶)))
324221, 223, 323rexlimd 3245 . . . . . . 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 3170 . . . 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 630 . 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 35898 . . 3 (𝜑 → (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁))))
331330anbi2d 629 . 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 396  wo 844   = wceq 1540  wcel 2105  wne 2940  wral 3061  wrex 3070  Vcvv 3441  csb 3842  cdif 3894  cun 3895  cin 3896  wss 3897  c0 4268  ifcif 4472  {csn 4572  cop 4578   class class class wbr 5089  cmpt 5172   × cxp 5612  ccnv 5613  ran crn 5615  cima 5617  Fun wfun 6467  wf 6469  ontowfo 6471  1-1-ontowf1o 6472  cfv 6473  (class class class)co 7329  f cof 7585  1st c1st 7889  2nd c2nd 7890  m cmap 8678  cc 10962  cr 10963  0cc0 10964  1c1 10965   + caddc 10967   < clt 11102  cle 11103  cmin 11298  cn 12066  0cn0 12326  cz 12412  cuz 12675  ...cfz 13332  ..^cfzo 13475
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5226  ax-sep 5240  ax-nul 5247  ax-pow 5305  ax-pr 5369  ax-un 7642  ax-cnex 11020  ax-resscn 11021  ax-1cn 11022  ax-icn 11023  ax-addcl 11024  ax-addrcl 11025  ax-mulcl 11026  ax-mulrcl 11027  ax-mulcom 11028  ax-addass 11029  ax-mulass 11030  ax-distr 11031  ax-i2m1 11032  ax-1ne0 11033  ax-1rid 11034  ax-rnegex 11035  ax-rrecex 11036  ax-cnre 11037  ax-pre-lttri 11038  ax-pre-lttrn 11039  ax-pre-ltadd 11040  ax-pre-mulgt0 11041
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-iun 4940  df-br 5090  df-opab 5152  df-mpt 5173  df-tr 5207  df-id 5512  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5569  df-we 5571  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6232  df-ord 6299  df-on 6300  df-lim 6301  df-suc 6302  df-iota 6425  df-fun 6475  df-fn 6476  df-f 6477  df-f1 6478  df-fo 6479  df-f1o 6480  df-fv 6481  df-riota 7286  df-ov 7332  df-oprab 7333  df-mpo 7334  df-of 7587  df-om 7773  df-1st 7891  df-2nd 7892  df-frecs 8159  df-wrecs 8190  df-recs 8264  df-rdg 8303  df-er 8561  df-map 8680  df-en 8797  df-dom 8798  df-sdom 8799  df-pnf 11104  df-mnf 11105  df-xr 11106  df-ltxr 11107  df-le 11108  df-sub 11300  df-neg 11301  df-nn 12067  df-n0 12327  df-z 12413  df-uz 12676  df-fz 13333  df-fzo 13476
This theorem is referenced by:  poimirlem27  35902
  Copyright terms: Public domain W3C validator