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

Theorem poimirlem31 32610
 Description: Lemma for poimir 32612, assigning values to the vertices of the tessellation that meet the hypotheses of both poimirlem30 32609 and poimirlem28 32607. Equation (2) of [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0 (𝜑𝑁 ∈ ℕ)
poimir.i 𝐼 = ((0[,]1) ↑𝑚 (1...𝑁))
poimir.r 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))
poimir.1 (𝜑𝐹 ∈ ((𝑅t 𝐼) Cn 𝑅))
poimir.2 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 0)) → ((𝐹𝑧)‘𝑛) ≤ 0)
poimirlem31.p 𝑃 = ((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
poimirlem31.3 (𝜑𝐺:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
poimirlem31.4 ((𝜑𝑘 ∈ ℕ) → ran (1st ‘(𝐺𝑘)) ⊆ (0..^𝑘))
poimirlem31.5 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑁))) → ∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ))
Assertion
Ref Expression
poimirlem31 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))
Distinct variable groups:   𝑓,𝑖,𝑗,𝑘,𝑛,𝑧   𝜑,𝑗,𝑛   𝑗,𝐹,𝑛   𝑗,𝑁,𝑛   𝜑,𝑖,𝑘   𝑓,𝑁,𝑖,𝑘   𝜑,𝑧   𝑓,𝐹,𝑘,𝑧   𝑧,𝑁   𝑖,𝑟,𝑗,𝑘,𝑛,𝑧,𝜑   𝑎,𝑏,𝑓,𝑖,𝑗,𝑘,𝑛,𝑟,𝑧,𝐹   𝐺,𝑎,𝑏,𝑓,𝑖,𝑗,𝑘,𝑛,𝑟,𝑧   𝐼,𝑎,𝑏,𝑓,𝑖,𝑗,𝑘,𝑛,𝑟,𝑧   𝑁,𝑎,𝑏,𝑟   𝑅,𝑎,𝑏,𝑓,𝑖,𝑗,𝑘,𝑛,𝑟,𝑧   𝑃,𝑎,𝑏,𝑓,𝑖,𝑛,𝑟,𝑧
Allowed substitution hints:   𝜑(𝑓,𝑎,𝑏)   𝑃(𝑗,𝑘)

Proof of Theorem poimirlem31
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elpri 4145 . . . 4 (𝑟 ∈ { ≤ , ≤ } → (𝑟 = ≤ ∨ 𝑟 = ≤ ))
2 simprr 792 . . . . . . 7 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → 𝑛 ∈ (1...𝑁))
3 1eluzge0 11608 . . . . . . . . . . 11 1 ∈ (ℤ‘0)
4 fzss1 12251 . . . . . . . . . . 11 (1 ∈ (ℤ‘0) → (1...𝑁) ⊆ (0...𝑁))
53, 4ax-mp 5 . . . . . . . . . 10 (1...𝑁) ⊆ (0...𝑁)
65sseli 3564 . . . . . . . . 9 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ (0...𝑁))
76anim2i 591 . . . . . . . 8 ((𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (𝑘 ∈ ℕ ∧ 𝑛 ∈ (0...𝑁)))
8 eleq1 2676 . . . . . . . . . . . . 13 (𝑖 = 𝑛 → (𝑖 ∈ (0...𝑁) ↔ 𝑛 ∈ (0...𝑁)))
98anbi2d 736 . . . . . . . . . . . 12 (𝑖 = 𝑛 → ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑁)) ↔ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (0...𝑁))))
109anbi2d 736 . . . . . . . . . . 11 (𝑖 = 𝑛 → ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑁))) ↔ (𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (0...𝑁)))))
11 eqeq1 2614 . . . . . . . . . . . 12 (𝑖 = 𝑛 → (𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) ↔ 𝑛 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < )))
1211rexbidv 3034 . . . . . . . . . . 11 (𝑖 = 𝑛 → (∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) ↔ ∃𝑗 ∈ (0...𝑁)𝑛 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < )))
1310, 12imbi12d 333 . . . . . . . . . 10 (𝑖 = 𝑛 → (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑁))) → ∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < )) ↔ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (0...𝑁))) → ∃𝑗 ∈ (0...𝑁)𝑛 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ))))
14 poimirlem31.5 . . . . . . . . . 10 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑁))) → ∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ))
1513, 14chvarv 2251 . . . . . . . . 9 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (0...𝑁))) → ∃𝑗 ∈ (0...𝑁)𝑛 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ))
16 elfzle1 12215 . . . . . . . . . . . . 13 (𝑛 ∈ (1...𝑁) → 1 ≤ 𝑛)
17 1re 9918 . . . . . . . . . . . . . 14 1 ∈ ℝ
18 elfzelz 12213 . . . . . . . . . . . . . . 15 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℤ)
1918zred 11358 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℝ)
20 lenlt 9995 . . . . . . . . . . . . . 14 ((1 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (1 ≤ 𝑛 ↔ ¬ 𝑛 < 1))
2117, 19, 20sylancr 694 . . . . . . . . . . . . 13 (𝑛 ∈ (1...𝑁) → (1 ≤ 𝑛 ↔ ¬ 𝑛 < 1))
2216, 21mpbid 221 . . . . . . . . . . . 12 (𝑛 ∈ (1...𝑁) → ¬ 𝑛 < 1)
23 elsni 4142 . . . . . . . . . . . . 13 (𝑛 ∈ {0} → 𝑛 = 0)
24 0lt1 10429 . . . . . . . . . . . . 13 0 < 1
2523, 24syl6eqbr 4622 . . . . . . . . . . . 12 (𝑛 ∈ {0} → 𝑛 < 1)
2622, 25nsyl 134 . . . . . . . . . . 11 (𝑛 ∈ (1...𝑁) → ¬ 𝑛 ∈ {0})
27 ltso 9997 . . . . . . . . . . . . . . 15 < Or ℝ
28 snfi 7923 . . . . . . . . . . . . . . . . 17 {0} ∈ Fin
29 fzfi 12633 . . . . . . . . . . . . . . . . . 18 (1...𝑁) ∈ Fin
30 rabfi 8070 . . . . . . . . . . . . . . . . . 18 ((1...𝑁) ∈ Fin → {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)} ∈ Fin)
3129, 30ax-mp 5 . . . . . . . . . . . . . . . . 17 {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)} ∈ Fin
32 unfi 8112 . . . . . . . . . . . . . . . . 17 (({0} ∈ Fin ∧ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)} ∈ Fin) → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}) ∈ Fin)
3328, 31, 32mp2an 704 . . . . . . . . . . . . . . . 16 ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}) ∈ Fin
34 c0ex 9913 . . . . . . . . . . . . . . . . . 18 0 ∈ V
3534snid 4155 . . . . . . . . . . . . . . . . 17 0 ∈ {0}
36 elun1 3742 . . . . . . . . . . . . . . . . 17 (0 ∈ {0} → 0 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}))
37 ne0i 3880 . . . . . . . . . . . . . . . . 17 (0 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}) → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}) ≠ ∅)
3835, 36, 37mp2b 10 . . . . . . . . . . . . . . . 16 ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}) ≠ ∅
39 0re 9919 . . . . . . . . . . . . . . . . . 18 0 ∈ ℝ
40 snssi 4280 . . . . . . . . . . . . . . . . . 18 (0 ∈ ℝ → {0} ⊆ ℝ)
4139, 40ax-mp 5 . . . . . . . . . . . . . . . . 17 {0} ⊆ ℝ
42 ssrab2 3650 . . . . . . . . . . . . . . . . . 18 {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)} ⊆ (1...𝑁)
4318ssriv 3572 . . . . . . . . . . . . . . . . . . 19 (1...𝑁) ⊆ ℤ
44 zssre 11261 . . . . . . . . . . . . . . . . . . 19 ℤ ⊆ ℝ
4543, 44sstri 3577 . . . . . . . . . . . . . . . . . 18 (1...𝑁) ⊆ ℝ
4642, 45sstri 3577 . . . . . . . . . . . . . . . . 17 {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)} ⊆ ℝ
4741, 46unssi 3750 . . . . . . . . . . . . . . . 16 ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}) ⊆ ℝ
4833, 38, 473pm3.2i 1232 . . . . . . . . . . . . . . 15 (({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}) ∈ Fin ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}) ≠ ∅ ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}) ⊆ ℝ)
49 fisupcl 8258 . . . . . . . . . . . . . . 15 (( < Or ℝ ∧ (({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}) ∈ Fin ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}) ≠ ∅ ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}) ⊆ ℝ)) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}))
5027, 48, 49mp2an 704 . . . . . . . . . . . . . 14 sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)})
51 eleq1 2676 . . . . . . . . . . . . . 14 (𝑛 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) → (𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}) ↔ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)})))
5250, 51mpbiri 247 . . . . . . . . . . . . 13 (𝑛 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) → 𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}))
53 elun 3715 . . . . . . . . . . . . 13 (𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}) ↔ (𝑛 ∈ {0} ∨ 𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}))
5452, 53sylib 207 . . . . . . . . . . . 12 (𝑛 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) → (𝑛 ∈ {0} ∨ 𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}))
55 oveq2 6557 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑛 → (1...𝑎) = (1...𝑛))
5655raleqdv 3121 . . . . . . . . . . . . . . 15 (𝑎 = 𝑛 → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)))
5756elrab 3331 . . . . . . . . . . . . . 14 (𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)} ↔ (𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)))
58 elfzuz 12209 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ (ℤ‘1))
59 eluzfz2 12220 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (ℤ‘1) → 𝑛 ∈ (1...𝑛))
6058, 59syl 17 . . . . . . . . . . . . . . 15 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ (1...𝑛))
61 simpl 472 . . . . . . . . . . . . . . . 16 ((0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0) → 0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏))
6261ralimi 2936 . . . . . . . . . . . . . . 15 (∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏))
63 fveq2 6103 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑛 → ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) = ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))
6463breq2d 4595 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑛 → (0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ↔ 0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
6564rspcva 3280 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (1...𝑛) ∧ ∀𝑏 ∈ (1...𝑛)0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏)) → 0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))
6660, 62, 65syl2an 493 . . . . . . . . . . . . . 14 ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)) → 0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))
6757, 66sylbi 206 . . . . . . . . . . . . 13 (𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)} → 0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))
6867orim2i 539 . . . . . . . . . . . 12 ((𝑛 ∈ {0} ∨ 𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}) → (𝑛 ∈ {0} ∨ 0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
6954, 68syl 17 . . . . . . . . . . 11 (𝑛 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) → (𝑛 ∈ {0} ∨ 0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
70 orel1 396 . . . . . . . . . . 11 𝑛 ∈ {0} → ((𝑛 ∈ {0} ∨ 0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)) → 0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
7126, 69, 70syl2im 39 . . . . . . . . . 10 (𝑛 ∈ (1...𝑁) → (𝑛 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) → 0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
7271reximdv 2999 . . . . . . . . 9 (𝑛 ∈ (1...𝑁) → (∃𝑗 ∈ (0...𝑁)𝑛 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) → ∃𝑗 ∈ (0...𝑁)0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
7315, 72syl5 33 . . . . . . . 8 (𝑛 ∈ (1...𝑁) → ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (0...𝑁))) → ∃𝑗 ∈ (0...𝑁)0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
747, 73sylan2i 685 . . . . . . 7 (𝑛 ∈ (1...𝑁) → ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → ∃𝑗 ∈ (0...𝑁)0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
752, 74mpcom 37 . . . . . 6 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → ∃𝑗 ∈ (0...𝑁)0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))
76 breq 4585 . . . . . . 7 (𝑟 = ≤ → (0𝑟((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ↔ 0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
7776rexbidv 3034 . . . . . 6 (𝑟 = ≤ → (∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ↔ ∃𝑗 ∈ (0...𝑁)0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
7875, 77syl5ibrcom 236 . . . . 5 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → (𝑟 = ≤ → ∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
79 poimir.0 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℕ)
8079nnzd 11357 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℤ)
81 elfzm1b 12287 . . . . . . . . . . . . . . 15 ((𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑛 ∈ (1...𝑁) ↔ (𝑛 − 1) ∈ (0...(𝑁 − 1))))
8218, 80, 81syl2anr 494 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑛 ∈ (1...𝑁) ↔ (𝑛 − 1) ∈ (0...(𝑁 − 1))))
8382biimpd 218 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑛 ∈ (1...𝑁) → (𝑛 − 1) ∈ (0...(𝑁 − 1))))
8483ex 449 . . . . . . . . . . . 12 (𝜑 → (𝑛 ∈ (1...𝑁) → (𝑛 ∈ (1...𝑁) → (𝑛 − 1) ∈ (0...(𝑁 − 1)))))
8584pm2.43d 51 . . . . . . . . . . 11 (𝜑 → (𝑛 ∈ (1...𝑁) → (𝑛 − 1) ∈ (0...(𝑁 − 1))))
8679nncnd 10913 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℂ)
87 npcan1 10334 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
8886, 87syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
89 nnm1nn0 11211 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
9079, 89syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 − 1) ∈ ℕ0)
9190nn0zd 11356 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 − 1) ∈ ℤ)
92 uzid 11578 . . . . . . . . . . . . . . 15 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
93 peano2uz 11617 . . . . . . . . . . . . . . 15 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
9491, 92, 933syl 18 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
9588, 94eqeltrrd 2689 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
96 fzss2 12252 . . . . . . . . . . . . 13 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (0...(𝑁 − 1)) ⊆ (0...𝑁))
9795, 96syl 17 . . . . . . . . . . . 12 (𝜑 → (0...(𝑁 − 1)) ⊆ (0...𝑁))
9897sseld 3567 . . . . . . . . . . 11 (𝜑 → ((𝑛 − 1) ∈ (0...(𝑁 − 1)) → (𝑛 − 1) ∈ (0...𝑁)))
9985, 98syld 46 . . . . . . . . . 10 (𝜑 → (𝑛 ∈ (1...𝑁) → (𝑛 − 1) ∈ (0...𝑁)))
10099anim2d 587 . . . . . . . . 9 (𝜑 → ((𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (𝑘 ∈ ℕ ∧ (𝑛 − 1) ∈ (0...𝑁))))
101100imp 444 . . . . . . . 8 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → (𝑘 ∈ ℕ ∧ (𝑛 − 1) ∈ (0...𝑁)))
102 ovex 6577 . . . . . . . . 9 (𝑛 − 1) ∈ V
103 eleq1 2676 . . . . . . . . . . . 12 (𝑖 = (𝑛 − 1) → (𝑖 ∈ (0...𝑁) ↔ (𝑛 − 1) ∈ (0...𝑁)))
104103anbi2d 736 . . . . . . . . . . 11 (𝑖 = (𝑛 − 1) → ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑁)) ↔ (𝑘 ∈ ℕ ∧ (𝑛 − 1) ∈ (0...𝑁))))
105104anbi2d 736 . . . . . . . . . 10 (𝑖 = (𝑛 − 1) → ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑁))) ↔ (𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑛 − 1) ∈ (0...𝑁)))))
106 eqeq1 2614 . . . . . . . . . . 11 (𝑖 = (𝑛 − 1) → (𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) ↔ (𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < )))
107106rexbidv 3034 . . . . . . . . . 10 (𝑖 = (𝑛 − 1) → (∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) ↔ ∃𝑗 ∈ (0...𝑁)(𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < )))
108105, 107imbi12d 333 . . . . . . . . 9 (𝑖 = (𝑛 − 1) → (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑁))) → ∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < )) ↔ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑛 − 1) ∈ (0...𝑁))) → ∃𝑗 ∈ (0...𝑁)(𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ))))
109102, 108, 14vtocl 3232 . . . . . . . 8 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑛 − 1) ∈ (0...𝑁))) → ∃𝑗 ∈ (0...𝑁)(𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ))
110101, 109syldan 486 . . . . . . 7 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → ∃𝑗 ∈ (0...𝑁)(𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ))
111 eleq1 2676 . . . . . . . . . . . . . . . 16 ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}) ↔ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)})))
11250, 111mpbiri 247 . . . . . . . . . . . . . . 15 ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) → (𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}))
113 elun 3715 . . . . . . . . . . . . . . . 16 ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}) ↔ ((𝑛 − 1) ∈ {0} ∨ (𝑛 − 1) ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}))
114102elsn 4140 . . . . . . . . . . . . . . . . 17 ((𝑛 − 1) ∈ {0} ↔ (𝑛 − 1) = 0)
115 oveq2 6557 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝑛 − 1) → (1...𝑎) = (1...(𝑛 − 1)))
116115raleqdv 3121 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑛 − 1) → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)))
117116elrab 3331 . . . . . . . . . . . . . . . . 17 ((𝑛 − 1) ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)} ↔ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)))
118114, 117orbi12i 542 . . . . . . . . . . . . . . . 16 (((𝑛 − 1) ∈ {0} ∨ (𝑛 − 1) ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}) ↔ ((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0))))
119113, 118bitri 263 . . . . . . . . . . . . . . 15 ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}) ↔ ((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0))))
120112, 119sylib 207 . . . . . . . . . . . . . 14 ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) → ((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0))))
121120a1i 11 . . . . . . . . . . . . 13 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) → ((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)))))
122 ltm1 10742 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℝ → (𝑛 − 1) < 𝑛)
123 peano2rem 10227 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
124 ltnle 9996 . . . . . . . . . . . . . . . . . . 19 (((𝑛 − 1) ∈ ℝ ∧ 𝑛 ∈ ℝ) → ((𝑛 − 1) < 𝑛 ↔ ¬ 𝑛 ≤ (𝑛 − 1)))
125123, 124mpancom 700 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℝ → ((𝑛 − 1) < 𝑛 ↔ ¬ 𝑛 ≤ (𝑛 − 1)))
126122, 125mpbid 221 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℝ → ¬ 𝑛 ≤ (𝑛 − 1))
12719, 126syl 17 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (1...𝑁) → ¬ 𝑛 ≤ (𝑛 − 1))
128 breq2 4587 . . . . . . . . . . . . . . . . 17 ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) → (𝑛 ≤ (𝑛 − 1) ↔ 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < )))
129128notbid 307 . . . . . . . . . . . . . . . 16 ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) → (¬ 𝑛 ≤ (𝑛 − 1) ↔ ¬ 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < )))
130127, 129syl5ibcom 234 . . . . . . . . . . . . . . 15 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) → ¬ 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < )))
131 elun2 3743 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)} → 𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}))
132 fimaxre2 10848 . . . . . . . . . . . . . . . . . . . . 21 ((({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}) ⊆ ℝ ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}) ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)})𝑦𝑥)
13347, 33, 132mp2an 704 . . . . . . . . . . . . . . . . . . . 20 𝑥 ∈ ℝ ∀𝑦 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)})𝑦𝑥
13447, 38, 1333pm3.2i 1232 . . . . . . . . . . . . . . . . . . 19 (({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}) ⊆ ℝ ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)})𝑦𝑥)
135134suprubii 10875 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}) → 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ))
136131, 135syl 17 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)} → 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ))
137136con3i 149 . . . . . . . . . . . . . . . 16 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) → ¬ 𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)})
138 ianor 508 . . . . . . . . . . . . . . . . 17 (¬ (𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)) ↔ (¬ 𝑛 ∈ (1...𝑁) ∨ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)))
139138, 57xchnxbir 322 . . . . . . . . . . . . . . . 16 𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)} ↔ (¬ 𝑛 ∈ (1...𝑁) ∨ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)))
140137, 139sylib 207 . . . . . . . . . . . . . . 15 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) → (¬ 𝑛 ∈ (1...𝑁) ∨ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)))
141130, 140syl6 34 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) → (¬ 𝑛 ∈ (1...𝑁) ∨ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0))))
142 pm2.63 825 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (1...𝑁) ∨ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)) → ((¬ 𝑛 ∈ (1...𝑁) ∨ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)) → ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)))
143142orcs 408 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) → ((¬ 𝑛 ∈ (1...𝑁) ∨ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)) → ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)))
144141, 143syld 46 . . . . . . . . . . . . 13 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) → ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)))
145121, 144jcad 554 . . . . . . . . . . . 12 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) → (((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0))) ∧ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0))))
146 andir 908 . . . . . . . . . . . . . 14 ((((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0))) ∧ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)) ↔ (((𝑛 − 1) = 0 ∧ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)) ∨ (((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)) ∧ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0))))
147 1p0e1 11010 . . . . . . . . . . . . . . . . . 18 (1 + 0) = 1
14818zcnd 11359 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ)
149 ax-1cn 9873 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℂ
150 0cn 9911 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ ℂ
151 subadd 10163 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ ∧ 0 ∈ ℂ) → ((𝑛 − 1) = 0 ↔ (1 + 0) = 𝑛))
152149, 150, 151mp3an23 1408 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℂ → ((𝑛 − 1) = 0 ↔ (1 + 0) = 𝑛))
153148, 152syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) = 0 ↔ (1 + 0) = 𝑛))
154153biimpa 500 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (1...𝑁) ∧ (𝑛 − 1) = 0) → (1 + 0) = 𝑛)
155147, 154syl5reqr 2659 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (1...𝑁) ∧ (𝑛 − 1) = 0) → 𝑛 = 1)
156 1z 11284 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℤ
157 fzsn 12254 . . . . . . . . . . . . . . . . . . . . . 22 (1 ∈ ℤ → (1...1) = {1})
158156, 157ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (1...1) = {1}
159 oveq2 6557 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 1 → (1...𝑛) = (1...1))
160 sneq 4135 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 1 → {𝑛} = {1})
161158, 159, 1603eqtr4a 2670 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 → (1...𝑛) = {𝑛})
162161raleqdv 3121 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 → (∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0) ↔ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)))
163162notbid 307 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → (¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0) ↔ ¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)))
164163biimpd 218 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → (¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0) → ¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)))
165155, 164syl 17 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (1...𝑁) ∧ (𝑛 − 1) = 0) → (¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0) → ¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)))
166165expimpd 627 . . . . . . . . . . . . . . 15 (𝑛 ∈ (1...𝑁) → (((𝑛 − 1) = 0 ∧ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)) → ¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)))
167 ralun 3757 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)) → ∀𝑏 ∈ ((1...(𝑛 − 1)) ∪ {𝑛})(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0))
168 npcan1 10334 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ℂ → ((𝑛 − 1) + 1) = 𝑛)
169148, 168syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) + 1) = 𝑛)
170169, 58eqeltrd 2688 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) + 1) ∈ (ℤ‘1))
171 peano2zm 11297 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ℤ → (𝑛 − 1) ∈ ℤ)
172 uzid 11578 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 − 1) ∈ ℤ → (𝑛 − 1) ∈ (ℤ‘(𝑛 − 1)))
173 peano2uz 11617 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 − 1) ∈ (ℤ‘(𝑛 − 1)) → ((𝑛 − 1) + 1) ∈ (ℤ‘(𝑛 − 1)))
17418, 171, 172, 1734syl 19 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) + 1) ∈ (ℤ‘(𝑛 − 1)))
175169, 174eqeltrrd 2689 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ (ℤ‘(𝑛 − 1)))
176 fzsplit2 12237 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑛 − 1) + 1) ∈ (ℤ‘1) ∧ 𝑛 ∈ (ℤ‘(𝑛 − 1))) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)))
177170, 175, 176syl2anc 691 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (1...𝑁) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)))
178169oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → (((𝑛 − 1) + 1)...𝑛) = (𝑛...𝑛))
179 fzsn 12254 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ℤ → (𝑛...𝑛) = {𝑛})
18018, 179syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → (𝑛...𝑛) = {𝑛})
181178, 180eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...𝑁) → (((𝑛 − 1) + 1)...𝑛) = {𝑛})
182181uneq2d 3729 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (1...𝑁) → ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)) = ((1...(𝑛 − 1)) ∪ {𝑛}))
183177, 182eqtrd 2644 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (1...𝑁) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ {𝑛}))
184183raleqdv 3121 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0) ↔ ∀𝑏 ∈ ((1...(𝑛 − 1)) ∪ {𝑛})(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)))
185167, 184syl5ibr 235 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑁) → ((∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)))
186185expdimp 452 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)))
187186con3d 147 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)) → (¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0) → ¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)))
188187adantrl 748 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (1...𝑁) ∧ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0))) → (¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0) → ¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)))
189188expimpd 627 . . . . . . . . . . . . . . 15 (𝑛 ∈ (1...𝑁) → ((((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)) ∧ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)) → ¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)))
190166, 189jaod 394 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) → ((((𝑛 − 1) = 0 ∧ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)) ∨ (((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)) ∧ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0))) → ¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)))
191146, 190syl5bi 231 . . . . . . . . . . . . 13 (𝑛 ∈ (1...𝑁) → ((((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0))) ∧ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)) → ¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)))
192 fveq2 6103 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝑛 → (𝑃𝑏) = (𝑃𝑛))
193192neeq1d 2841 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑛 → ((𝑃𝑏) ≠ 0 ↔ (𝑃𝑛) ≠ 0))
19464, 193anbi12d 743 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑛 → ((0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∧ (𝑃𝑛) ≠ 0)))
195194ralsng 4165 . . . . . . . . . . . . . . 15 (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∧ (𝑃𝑛) ≠ 0)))
196195notbid 307 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) → (¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0) ↔ ¬ (0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∧ (𝑃𝑛) ≠ 0)))
197 ianor 508 . . . . . . . . . . . . . . 15 (¬ (0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∧ (𝑃𝑛) ≠ 0) ↔ (¬ 0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∨ ¬ (𝑃𝑛) ≠ 0))
198 nne 2786 . . . . . . . . . . . . . . . 16 (¬ (𝑃𝑛) ≠ 0 ↔ (𝑃𝑛) = 0)
199198orbi2i 540 . . . . . . . . . . . . . . 15 ((¬ 0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∨ ¬ (𝑃𝑛) ≠ 0) ↔ (¬ 0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∨ (𝑃𝑛) = 0))
200197, 199bitri 263 . . . . . . . . . . . . . 14 (¬ (0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∧ (𝑃𝑛) ≠ 0) ↔ (¬ 0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∨ (𝑃𝑛) = 0))
201196, 200syl6bb 275 . . . . . . . . . . . . 13 (𝑛 ∈ (1...𝑁) → (¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0) ↔ (¬ 0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∨ (𝑃𝑛) = 0)))
202191, 201sylibd 228 . . . . . . . . . . . 12 (𝑛 ∈ (1...𝑁) → ((((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0))) ∧ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)) → (¬ 0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∨ (𝑃𝑛) = 0)))
203145, 202syld 46 . . . . . . . . . . 11 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) → (¬ 0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∨ (𝑃𝑛) = 0)))
204203ad2antlr 759 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) → (¬ 0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∨ (𝑃𝑛) = 0)))
205 poimir.1 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐹 ∈ ((𝑅t 𝐼) Cn 𝑅))
206 poimir.r . . . . . . . . . . . . . . . . . . . . . 22 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))
207 retop 22375 . . . . . . . . . . . . . . . . . . . . . . . 24 (topGen‘ran (,)) ∈ Top
208207fconst6 6008 . . . . . . . . . . . . . . . . . . . . . . 23 ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top
209 pttop 21195 . . . . . . . . . . . . . . . . . . . . . . 23 (((1...𝑁) ∈ Fin ∧ ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top) → (∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈ Top)
21029, 208, 209mp2an 704 . . . . . . . . . . . . . . . . . . . . . 22 (∏t‘((1...𝑁) × {(topGen‘ran (,))})) ∈ Top
211206, 210eqeltri 2684 . . . . . . . . . . . . . . . . . . . . 21 𝑅 ∈ Top
212 poimir.i . . . . . . . . . . . . . . . . . . . . . 22 𝐼 = ((0[,]1) ↑𝑚 (1...𝑁))
213 reex 9906 . . . . . . . . . . . . . . . . . . . . . . 23 ℝ ∈ V
214 unitssre 12190 . . . . . . . . . . . . . . . . . . . . . . 23 (0[,]1) ⊆ ℝ
215 mapss 7786 . . . . . . . . . . . . . . . . . . . . . . 23 ((ℝ ∈ V ∧ (0[,]1) ⊆ ℝ) → ((0[,]1) ↑𝑚 (1...𝑁)) ⊆ (ℝ ↑𝑚 (1...𝑁)))
216213, 214, 215mp2an 704 . . . . . . . . . . . . . . . . . . . . . 22 ((0[,]1) ↑𝑚 (1...𝑁)) ⊆ (ℝ ↑𝑚 (1...𝑁))
217212, 216eqsstri 3598 . . . . . . . . . . . . . . . . . . . . 21 𝐼 ⊆ (ℝ ↑𝑚 (1...𝑁))
218 uniretop 22376 . . . . . . . . . . . . . . . . . . . . . . . 24 ℝ = (topGen‘ran (,))
219206, 218ptuniconst 21211 . . . . . . . . . . . . . . . . . . . . . . 23 (((1...𝑁) ∈ Fin ∧ (topGen‘ran (,)) ∈ Top) → (ℝ ↑𝑚 (1...𝑁)) = 𝑅)
22029, 207, 219mp2an 704 . . . . . . . . . . . . . . . . . . . . . 22 (ℝ ↑𝑚 (1...𝑁)) = 𝑅
221220restuni 20776 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ Top ∧ 𝐼 ⊆ (ℝ ↑𝑚 (1...𝑁))) → 𝐼 = (𝑅t 𝐼))
222211, 217, 221mp2an 704 . . . . . . . . . . . . . . . . . . . 20 𝐼 = (𝑅t 𝐼)
223222, 220cnf 20860 . . . . . . . . . . . . . . . . . . 19 (𝐹 ∈ ((𝑅t 𝐼) Cn 𝑅) → 𝐹:𝐼⟶(ℝ ↑𝑚 (1...𝑁)))
224205, 223syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹:𝐼⟶(ℝ ↑𝑚 (1...𝑁)))
225224ad2antrr 758 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝐹:𝐼⟶(ℝ ↑𝑚 (1...𝑁)))
226 simplr 788 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝑘 ∈ ℕ)
227 elfzelz 12213 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ (0...𝑘) → 𝑥 ∈ ℤ)
228227zred 11358 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ (0...𝑘) → 𝑥 ∈ ℝ)
229228adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑥 ∈ ℝ)
230 nnre 10904 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
231230adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ)
232 nnne0 10930 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 ∈ ℕ → 𝑘 ≠ 0)
233232adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ≠ 0)
234229, 231, 233redivcld 10732 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑥 / 𝑘) ∈ ℝ)
235 elfzle1 12215 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ (0...𝑘) → 0 ≤ 𝑥)
236228, 235jca 553 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ (0...𝑘) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
237 nnrp 11718 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
238237rpregt0d 11754 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 < 𝑘))
239 divge0 10771 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → 0 ≤ (𝑥 / 𝑘))
240236, 238, 239syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝑥 / 𝑘))
241 elfzle2 12216 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ (0...𝑘) → 𝑥𝑘)
242241adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑥𝑘)
243 1red 9934 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
244237adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+)
245229, 243, 244ledivmuld 11801 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑥 / 𝑘) ≤ 1 ↔ 𝑥 ≤ (𝑘 · 1)))
246 nncn 10905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
247246mulid1d 9936 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 ∈ ℕ → (𝑘 · 1) = 𝑘)
248247breq2d 4595 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 ∈ ℕ → (𝑥 ≤ (𝑘 · 1) ↔ 𝑥𝑘))
249248adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑥 ≤ (𝑘 · 1) ↔ 𝑥𝑘))
250245, 249bitrd 267 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑥 / 𝑘) ≤ 1 ↔ 𝑥𝑘))
251242, 250mpbird 246 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑥 / 𝑘) ≤ 1)
25239, 17elicc2i 12110 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 / 𝑘) ∈ (0[,]1) ↔ ((𝑥 / 𝑘) ∈ ℝ ∧ 0 ≤ (𝑥 / 𝑘) ∧ (𝑥 / 𝑘) ≤ 1))
253234, 240, 251, 252syl3anbrc 1239 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑥 / 𝑘) ∈ (0[,]1))
254253ancoms 468 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ℕ ∧ 𝑥 ∈ (0...𝑘)) → (𝑥 / 𝑘) ∈ (0[,]1))
255 elsni 4142 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ {𝑘} → 𝑦 = 𝑘)
256255oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ {𝑘} → (𝑥 / 𝑦) = (𝑥 / 𝑘))
257256eleq1d 2672 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ {𝑘} → ((𝑥 / 𝑦) ∈ (0[,]1) ↔ (𝑥 / 𝑘) ∈ (0[,]1)))
258254, 257syl5ibrcom 236 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ ∧ 𝑥 ∈ (0...𝑘)) → (𝑦 ∈ {𝑘} → (𝑥 / 𝑦) ∈ (0[,]1)))
259258impr 647 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ ∧ (𝑥 ∈ (0...𝑘) ∧ 𝑦 ∈ {𝑘})) → (𝑥 / 𝑦) ∈ (0[,]1))
260226, 259sylan 487 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ (0...𝑘) ∧ 𝑦 ∈ {𝑘})) → (𝑥 / 𝑦) ∈ (0[,]1))
261 elun 3715 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ({1} ∪ {0}) ↔ (𝑦 ∈ {1} ∨ 𝑦 ∈ {0}))
262 fzofzp1 12431 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ (0..^𝑘) → (𝑥 + 1) ∈ (0...𝑘))
263 elsni 4142 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ {1} → 𝑦 = 1)
264263oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ {1} → (𝑥 + 𝑦) = (𝑥 + 1))
265264eleq1d 2672 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ {1} → ((𝑥 + 𝑦) ∈ (0...𝑘) ↔ (𝑥 + 1) ∈ (0...𝑘)))
266262, 265syl5ibrcom 236 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ (0..^𝑘) → (𝑦 ∈ {1} → (𝑥 + 𝑦) ∈ (0...𝑘)))
267 elfzonn0 12380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ (0..^𝑘) → 𝑥 ∈ ℕ0)
268267nn0cnd 11230 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ (0..^𝑘) → 𝑥 ∈ ℂ)
269268addid1d 10115 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ (0..^𝑘) → (𝑥 + 0) = 𝑥)
270 elfzofz 12354 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ (0..^𝑘) → 𝑥 ∈ (0...𝑘))
271269, 270eqeltrd 2688 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ (0..^𝑘) → (𝑥 + 0) ∈ (0...𝑘))
272 elsni 4142 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ {0} → 𝑦 = 0)
273272oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ {0} → (𝑥 + 𝑦) = (𝑥 + 0))
274273eleq1d 2672 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ {0} → ((𝑥 + 𝑦) ∈ (0...𝑘) ↔ (𝑥 + 0) ∈ (0...𝑘)))
275271, 274syl5ibrcom 236 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ (0..^𝑘) → (𝑦 ∈ {0} → (𝑥 + 𝑦) ∈ (0...𝑘)))
276266, 275jaod 394 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ (0..^𝑘) → ((𝑦 ∈ {1} ∨ 𝑦 ∈ {0}) → (𝑥 + 𝑦) ∈ (0...𝑘)))
277261, 276syl5bi 231 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (0..^𝑘) → (𝑦 ∈ ({1} ∪ {0}) → (𝑥 + 𝑦) ∈ (0...𝑘)))
278277imp 444 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ (0..^𝑘) ∧ 𝑦 ∈ ({1} ∪ {0})) → (𝑥 + 𝑦) ∈ (0...𝑘))
279278adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ (0..^𝑘) ∧ 𝑦 ∈ ({1} ∪ {0}))) → (𝑥 + 𝑦) ∈ (0...𝑘))
280 poimirlem31.3 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐺:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
281280ffvelrnda 6267 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
282 xp1st 7089 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺𝑘) ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(𝐺𝑘)) ∈ (ℕ0𝑚 (1...𝑁)))
283 elmapfn 7766 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1st ‘(𝐺𝑘)) ∈ (ℕ0𝑚 (1...𝑁)) → (1st ‘(𝐺𝑘)) Fn (1...𝑁))
284281, 282, 2833syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)) Fn (1...𝑁))
285 poimirlem31.4 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ ℕ) → ran (1st ‘(𝐺𝑘)) ⊆ (0..^𝑘))
286 df-f 5808 . . . . . . . . . . . . . . . . . . . . . . 23 ((1st ‘(𝐺𝑘)):(1...𝑁)⟶(0..^𝑘) ↔ ((1st ‘(𝐺𝑘)) Fn (1...𝑁) ∧ ran (1st ‘(𝐺𝑘)) ⊆ (0..^𝑘)))
287284, 285, 286sylanbrc 695 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶(0..^𝑘))
288287adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (1st ‘(𝐺𝑘)):(1...𝑁)⟶(0..^𝑘))
289 1ex 9914 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ V
290289fconst 6004 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}):((2nd ‘(𝐺𝑘)) “ (1...𝑗))⟶{1}
29134fconst 6004 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}):((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))⟶{0}
292290, 291pm3.2i 470 . . . . . . . . . . . . . . . . . . . . . . 23 ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}):((2nd ‘(𝐺𝑘)) “ (1...𝑗))⟶{1} ∧ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}):((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))⟶{0})
293 xp2nd 7090 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐺𝑘) ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(𝐺𝑘)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
294281, 293syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ ℕ) → (2nd ‘(𝐺𝑘)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
295 fvex 6113 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (2nd ‘(𝐺𝑘)) ∈ V
296 f1oeq1 6040 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓 = (2nd ‘(𝐺𝑘)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁)))
297295, 296elab 3319 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2nd ‘(𝐺𝑘)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁))
298294, 297sylib 207 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ ℕ) → (2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁))
299 dff1o3 6056 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(𝐺𝑘)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(𝐺𝑘))))
300299simprbi 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(𝐺𝑘)))
301 imain 5888 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Fun (2nd ‘(𝐺𝑘)) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∩ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))))
302298, 300, 3013syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ ℕ) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∩ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))))
303 elfznn0 12302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ0)
304303nn0red 11229 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
305304ltp1d 10833 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1))
306 fzdisj 12239 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
307305, 306syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
308307imaeq2d 5385 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 ∈ (0...𝑁) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((2nd ‘(𝐺𝑘)) “ ∅))
309 ima0 5400 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2nd ‘(𝐺𝑘)) “ ∅) = ∅
310308, 309syl6eq 2660 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (0...𝑁) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
311302, 310sylan9req 2665 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∩ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))) = ∅)
312 fun 5979 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}):((2nd ‘(𝐺𝑘)) “ (1...𝑗))⟶{1} ∧ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}):((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))⟶{0}) ∧ (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∩ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))) = ∅) → ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∪ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
313292, 311, 312sylancr 694 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∪ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
314 imaundi 5464 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∪ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)))
315 nn0p1nn 11209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
316303, 315syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ)
317 nnuz 11599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ℕ = (ℤ‘1)
318316, 317syl6eleq 2698 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (ℤ‘1))
319 elfzuz3 12210 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ𝑗))
320 fzsplit2 12237 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑗 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
321318, 319, 320syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
322321imaeq2d 5385 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ (0...𝑁) → ((2nd ‘(𝐺𝑘)) “ (1...𝑁)) = ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))))
323 f1ofo 6057 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((2nd ‘(𝐺𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(𝐺𝑘)):(1...𝑁)–onto→(1...𝑁))
324 foima 6033 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((2nd ‘(𝐺𝑘)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(𝐺𝑘)) “ (1...𝑁)) = (1...𝑁))
325298, 323, 3243syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ ℕ) → ((2nd ‘(𝐺𝑘)) “ (1...𝑁)) = (1...𝑁))
326322, 325sylan9req 2665 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗 ∈ (0...𝑁) ∧ (𝜑𝑘 ∈ ℕ)) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (1...𝑁))
327326ancoms 468 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((2nd ‘(𝐺𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (1...𝑁))
328314, 327syl5eqr 2658 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∪ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁))) = (1...𝑁))
329328feq2d 5944 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(((2nd ‘(𝐺𝑘)) “ (1...𝑗)) ∪ ((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}) ↔ ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0})))
330313, 329mpbid 221 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
331 fzfid 12634 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin)
332 inidm 3784 . . . . . . . . . . . . . . . . . . . . 21 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
333279, 288, 330, 331, 331, 332off 6810 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝑘))
334 poimirlem31.p . . . . . . . . . . . . . . . . . . . . 21 𝑃 = ((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
335334feq1i 5949 . . . . . . . . . . . . . . . . . . . 20 (𝑃:(1...𝑁)⟶(0...𝑘) ↔ ((1st ‘(𝐺𝑘)) ∘𝑓 + ((((2nd ‘(𝐺𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝐺𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝑘))
336333, 335sylibr 223 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝑃:(1...𝑁)⟶(0...𝑘))
337 vex 3176 . . . . . . . . . . . . . . . . . . . . 21 𝑘 ∈ V
338337fconst 6004 . . . . . . . . . . . . . . . . . . . 20 ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘}
339338a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘})
340260, 336, 339, 331, 331, 332off 6810 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (𝑃𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
341212eleq2i 2680 . . . . . . . . . . . . . . . . . . 19 ((𝑃𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (𝑃𝑓 / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑𝑚 (1...𝑁)))
342 ovex 6577 . . . . . . . . . . . . . . . . . . . 20 (0[,]1) ∈ V
343 ovex 6577 . . . . . . . . . . . . . . . . . . . 20 (1...𝑁) ∈ V
344342, 343elmap 7772 . . . . . . . . . . . . . . . . . . 19 ((𝑃𝑓 / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑𝑚 (1...𝑁)) ↔ (𝑃𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
345341, 344bitri 263 . . . . . . . . . . . . . . . . . 18 ((𝑃𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (𝑃𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
346340, 345sylibr 223 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (𝑃𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼)
347225, 346ffvelrnd 6268 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘}))) ∈ (ℝ ↑𝑚 (1...𝑁)))
348 elmapi 7765 . . . . . . . . . . . . . . . 16 ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘}))) ∈ (ℝ ↑𝑚 (1...𝑁)) → (𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘}))):(1...𝑁)⟶ℝ)
349347, 348syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘}))):(1...𝑁)⟶ℝ)
350349ffvelrnda 6267 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∈ ℝ)
351350an32s 842 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∈ ℝ)
352 0red 9920 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → 0 ∈ ℝ)
353351, 352ltnled 10063 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → (((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) < 0 ↔ ¬ 0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
354 ltle 10005 . . . . . . . . . . . . 13 ((((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∈ ℝ ∧ 0 ∈ ℝ) → (((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) < 0 → ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
355351, 39, 354sylancl 693 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → (((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) < 0 → ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
356353, 355sylbird 249 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → (¬ 0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) → ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
357246, 232div0d 10679 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → (0 / 𝑘) = 0)
358 oveq1 6556 . . . . . . . . . . . . . . . 16 ((𝑃𝑛) = 0 → ((𝑃𝑛) / 𝑘) = (0 / 𝑘))
359358eqeq1d 2612 . . . . . . . . . . . . . . 15 ((𝑃𝑛) = 0 → (((𝑃𝑛) / 𝑘) = 0 ↔ (0 / 𝑘) = 0))
360357, 359syl5ibrcom 236 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → ((𝑃𝑛) = 0 → ((𝑃𝑛) / 𝑘) = 0))
361360ad3antlr 763 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑃𝑛) = 0 → ((𝑃𝑛) / 𝑘) = 0))
362 ffn 5958 . . . . . . . . . . . . . . . . 17 (𝑃:(1...𝑁)⟶(0...𝑘) → 𝑃 Fn (1...𝑁))
363336, 362syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝑃 Fn (1...𝑁))
364 fnconstg 6006 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ V → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
365337, 364mp1i 13 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
366 eqidd 2611 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑃𝑛) = (𝑃𝑛))
367337fvconst2 6374 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {𝑘})‘𝑛) = 𝑘)
368367adantl 481 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {𝑘})‘𝑛) = 𝑘)
369363, 365, 331, 331, 332, 366, 368ofval 6804 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑃𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = ((𝑃𝑛) / 𝑘))
370369an32s 842 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑃𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = ((𝑃𝑛) / 𝑘))
371370eqeq1d 2612 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → (((𝑃𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 0 ↔ ((𝑃𝑛) / 𝑘) = 0))
372361, 371sylibrd 248 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑃𝑛) = 0 → ((𝑃𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 0))
373 simplll 794 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → 𝜑)
374 simplr 788 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → 𝑛 ∈ (1...𝑁))
375346adantlr 747 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → (𝑃𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼)
376 ovex 6577 . . . . . . . . . . . . . 14 (𝑃𝑓 / ((1...𝑁) × {𝑘})) ∈ V
377 eleq1 2676 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑃𝑓 / ((1...𝑁) × {𝑘})) → (𝑧𝐼 ↔ (𝑃𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼))
378 fveq1 6102 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑃𝑓 / ((1...𝑁) × {𝑘})) → (𝑧𝑛) = ((𝑃𝑓 / ((1...𝑁) × {𝑘}))‘𝑛))
379378eqeq1d 2612 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑃𝑓 / ((1...𝑁) × {𝑘})) → ((𝑧𝑛) = 0 ↔ ((𝑃𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 0))
380 fveq2 6103 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝑃𝑓 / ((1...𝑁) × {𝑘})) → (𝐹𝑧) = (𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘}))))
381380fveq1d 6105 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑃𝑓 / ((1...𝑁) × {𝑘})) → ((𝐹𝑧)‘𝑛) = ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))
382381breq1d 4593 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑃𝑓 / ((1...𝑁) × {𝑘})) → (((𝐹𝑧)‘𝑛) ≤ 0 ↔ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
383379, 382imbi12d 333 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑃𝑓 / ((1...𝑁) × {𝑘})) → (((𝑧𝑛) = 0 → ((𝐹𝑧)‘𝑛) ≤ 0) ↔ (((𝑃𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 0 → ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0)))
384377, 383imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑃𝑓 / ((1...𝑁) × {𝑘})) → ((𝑧𝐼 → ((𝑧𝑛) = 0 → ((𝐹𝑧)‘𝑛) ≤ 0)) ↔ ((𝑃𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 → (((𝑃𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 0 → ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))))
385384imbi2d 329 . . . . . . . . . . . . . . 15 (𝑧 = (𝑃𝑓 / ((1...𝑁) × {𝑘})) → ((𝑛 ∈ (1...𝑁) → (𝑧𝐼 → ((𝑧𝑛) = 0 → ((𝐹𝑧)‘𝑛) ≤ 0))) ↔ (𝑛 ∈ (1...𝑁) → ((𝑃𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 → (((𝑃𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 0 → ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0)))))
386385imbi2d 329 . . . . . . . . . . . . . 14 (𝑧 = (𝑃𝑓 / ((1...𝑁) × {𝑘})) → ((𝜑 → (𝑛 ∈ (1...𝑁) → (𝑧𝐼 → ((𝑧𝑛) = 0 → ((𝐹𝑧)‘𝑛) ≤ 0)))) ↔ (𝜑 → (𝑛 ∈ (1...𝑁) → ((𝑃𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 → (((𝑃𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 0 → ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))))))
387 poimir.2 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 0)) → ((𝐹𝑧)‘𝑛) ≤ 0)
3883873exp2 1277 . . . . . . . . . . . . . 14 (𝜑 → (𝑛 ∈ (1...𝑁) → (𝑧𝐼 → ((𝑧𝑛) = 0 → ((𝐹𝑧)‘𝑛) ≤ 0))))
389376, 386, 388vtocl 3232 . . . . . . . . . . . . 13 (𝜑 → (𝑛 ∈ (1...𝑁) → ((𝑃𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 → (((𝑃𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 0 → ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))))
390373, 374, 375, 389syl3c 64 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → (((𝑃𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 0 → ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
391372, 390syld 46 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑃𝑛) = 0 → ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
392356, 391jaod 394 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → ((¬ 0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∨ (𝑃𝑛) = 0) → ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
393204, 392syld 46 . . . . . . . . 9 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) → ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
394393reximdva 3000 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) → (∃𝑗 ∈ (0...𝑁)(𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) → ∃𝑗 ∈ (0...𝑁)((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
395394anasss 677 . . . . . . 7 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → (∃𝑗 ∈ (0...𝑁)(𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃𝑏) ≠ 0)}), ℝ, < ) → ∃𝑗 ∈ (0...𝑁)((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
396110, 395mpd 15 . . . . . 6 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → ∃𝑗 ∈ (0...𝑁)((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0)
397 breq 4585 . . . . . . . 8 (𝑟 = ≤ → (0𝑟((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ↔ 0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
398 fvex 6113 . . . . . . . . 9 ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∈ V
39934, 398brcnv 5227 . . . . . . . 8 (0 ≤ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ↔ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0)
400397, 399syl6bb 275 . . . . . . 7 (𝑟 = ≤ → (0𝑟((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ↔ ((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
401400rexbidv 3034 . . . . . 6 (𝑟 = ≤ → (∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ↔ ∃𝑗 ∈ (0...𝑁)((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
402396, 401syl5ibrcom 236 . . . . 5 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → (𝑟 = ≤ → ∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
40378, 402jaod 394 . . . 4 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → ((𝑟 = ≤ ∨ 𝑟 = ≤ ) → ∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
4041, 403syl5 33 . . 3 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → (𝑟 ∈ { ≤ , ≤ } → ∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
405404exp32 629 . 2 (𝜑 → (𝑘 ∈ ℕ → (𝑛 ∈ (1...𝑁) → (𝑟 ∈ { ≤ , ≤ } → ∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))))
4064053imp2 1274 1 ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  {cab 2596   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  {csn 4125  {cpr 4127  ∪ cuni 4372   class class class wbr 4583   Or wor 4958   × cxp 5036  ◡ccnv 5037  ran crn 5039   “ cima 5041  Fun wfun 5798   Fn wfn 5799  ⟶wf 5800  –onto→wfo 5802  –1-1-onto→wf1o 5803  ‘cfv 5804  (class class class)co 6549   ∘𝑓 cof 6793  1st c1st 7057  2nd c2nd 7058   ↑𝑚 cmap 7744  Fincfn 7841  supcsup 8229  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820   < clt 9953   ≤ cle 9954   − cmin 10145   / cdiv 10563  ℕcn 10897  ℕ0cn0 11169  ℤcz 11254  ℤ≥cuz 11563  ℝ+crp 11708  (,)cioo 12046  [,]cicc 12049  ...cfz 12197  ..^cfzo 12334   ↾t crest 15904  topGenctg 15921  ∏tcpt 15922  Topctop 20517   Cn ccn 20838 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fi 8200  df-sup 8231  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-n0 11170  df-z 11255  df-uz 11564  df-rp 11709  df-ioo 12050  df-icc 12053  df-fz 12198  df-fzo 12335  df-rest 15906  df-topgen 15927  df-pt 15928  df-top 20521  df-bases 20522  df-topon 20523  df-cn 20841 This theorem is referenced by:  poimirlem32  32611
 Copyright terms: Public domain W3C validator