Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  poimirlem31 Structured version   Visualization version   GIF version
Theorem poimirlem31 36457
Description: Lemma for poimir 36459, assigning values to the vertices of the tessellation that meet the hypotheses of both poimirlem30 36456 and poimirlem28 36454. Equation (2) of [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0 (πœ‘ β†’ 𝑁 ∈ β„•)
poimir.i 𝐼 = ((0[,]1) ↑m (1...𝑁))
poimir.r 𝑅 = (∏tβ€˜((1...𝑁) Γ— {(topGenβ€˜ran (,))}))
poimir.1 (πœ‘ β†’ 𝐹 ∈ ((𝑅 β†Ύt 𝐼) Cn 𝑅))
poimir.2 ((πœ‘ ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (π‘§β€˜π‘›) = 0)) β†’ ((πΉβ€˜π‘§)β€˜π‘›) ≀ 0)
poimirlem31.p 𝑃 = ((1st β€˜(πΊβ€˜π‘˜)) ∘f + ((((2nd β€˜(πΊβ€˜π‘˜)) β€œ (1...𝑗)) Γ— {1}) βˆͺ (((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((𝑗 + 1)...𝑁)) Γ— {0})))
poimirlem31.3 (πœ‘ β†’ 𝐺:β„•βŸΆ((β„•0 ↑m (1...𝑁)) Γ— {𝑓 ∣ 𝑓:(1...𝑁)–1-1-ontoβ†’(1...𝑁)}))
poimirlem31.4 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ran (1st β€˜(πΊβ€˜π‘˜)) βŠ† (0..^π‘˜))
poimirlem31.5 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 𝑖 ∈ (0...𝑁))) β†’ βˆƒπ‘— ∈ (0...𝑁)𝑖 = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ))
Assertion
Ref Expression
poimirlem31 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 𝑛 ∈ (1...𝑁) ∧ π‘Ÿ ∈ { ≀ , β—‘ ≀ })) β†’ βˆƒπ‘— ∈ (0...𝑁)0π‘Ÿ((πΉβ€˜(𝑃 ∘f / ((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 4649 . . . 4 (π‘Ÿ ∈ { ≀ , β—‘ ≀ } β†’ (π‘Ÿ = ≀ ∨ π‘Ÿ = β—‘ ≀ ))
2 simprr 772 . . . . . . 7 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 𝑛 ∈ (1...𝑁))) β†’ 𝑛 ∈ (1...𝑁))
3 fz1ssfz0 13593 . . . . . . . . . 10 (1...𝑁) βŠ† (0...𝑁)
43sseli 3977 . . . . . . . . 9 (𝑛 ∈ (1...𝑁) β†’ 𝑛 ∈ (0...𝑁))
54anim2i 618 . . . . . . . 8 ((π‘˜ ∈ β„• ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘˜ ∈ β„• ∧ 𝑛 ∈ (0...𝑁)))
6 eleq1 2822 . . . . . . . . . . . . 13 (𝑖 = 𝑛 β†’ (𝑖 ∈ (0...𝑁) ↔ 𝑛 ∈ (0...𝑁)))
76anbi2d 630 . . . . . . . . . . . 12 (𝑖 = 𝑛 β†’ ((π‘˜ ∈ β„• ∧ 𝑖 ∈ (0...𝑁)) ↔ (π‘˜ ∈ β„• ∧ 𝑛 ∈ (0...𝑁))))
87anbi2d 630 . . . . . . . . . . 11 (𝑖 = 𝑛 β†’ ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 𝑖 ∈ (0...𝑁))) ↔ (πœ‘ ∧ (π‘˜ ∈ β„• ∧ 𝑛 ∈ (0...𝑁)))))
9 eqeq1 2737 . . . . . . . . . . . 12 (𝑖 = 𝑛 β†’ (𝑖 = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) ↔ 𝑛 = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < )))
109rexbidv 3179 . . . . . . . . . . 11 (𝑖 = 𝑛 β†’ (βˆƒπ‘— ∈ (0...𝑁)𝑖 = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) ↔ βˆƒπ‘— ∈ (0...𝑁)𝑛 = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < )))
118, 10imbi12d 345 . . . . . . . . . 10 (𝑖 = 𝑛 β†’ (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 𝑖 ∈ (0...𝑁))) β†’ βˆƒπ‘— ∈ (0...𝑁)𝑖 = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < )) ↔ ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 𝑛 ∈ (0...𝑁))) β†’ βˆƒπ‘— ∈ (0...𝑁)𝑛 = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ))))
12 poimirlem31.5 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 𝑖 ∈ (0...𝑁))) β†’ βˆƒπ‘— ∈ (0...𝑁)𝑖 = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ))
1311, 12chvarvv 2003 . . . . . . . . 9 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 𝑛 ∈ (0...𝑁))) β†’ βˆƒπ‘— ∈ (0...𝑁)𝑛 = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ))
14 elfzle1 13500 . . . . . . . . . . . . 13 (𝑛 ∈ (1...𝑁) β†’ 1 ≀ 𝑛)
15 1re 11210 . . . . . . . . . . . . . 14 1 ∈ ℝ
16 elfzelz 13497 . . . . . . . . . . . . . . 15 (𝑛 ∈ (1...𝑁) β†’ 𝑛 ∈ β„€)
1716zred 12662 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) β†’ 𝑛 ∈ ℝ)
18 lenlt 11288 . . . . . . . . . . . . . 14 ((1 ∈ ℝ ∧ 𝑛 ∈ ℝ) β†’ (1 ≀ 𝑛 ↔ Β¬ 𝑛 < 1))
1915, 17, 18sylancr 588 . . . . . . . . . . . . 13 (𝑛 ∈ (1...𝑁) β†’ (1 ≀ 𝑛 ↔ Β¬ 𝑛 < 1))
2014, 19mpbid 231 . . . . . . . . . . . 12 (𝑛 ∈ (1...𝑁) β†’ Β¬ 𝑛 < 1)
21 elsni 4644 . . . . . . . . . . . . 13 (𝑛 ∈ {0} β†’ 𝑛 = 0)
22 0lt1 11732 . . . . . . . . . . . . 13 0 < 1
2321, 22eqbrtrdi 5186 . . . . . . . . . . . 12 (𝑛 ∈ {0} β†’ 𝑛 < 1)
2420, 23nsyl 140 . . . . . . . . . . 11 (𝑛 ∈ (1...𝑁) β†’ Β¬ 𝑛 ∈ {0})
25 ltso 11290 . . . . . . . . . . . . . . 15 < Or ℝ
26 snfi 9040 . . . . . . . . . . . . . . . . 17 {0} ∈ Fin
27 fzfi 13933 . . . . . . . . . . . . . . . . . 18 (1...𝑁) ∈ Fin
28 rabfi 9265 . . . . . . . . . . . . . . . . . 18 ((1...𝑁) ∈ Fin β†’ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)} ∈ Fin)
2927, 28ax-mp 5 . . . . . . . . . . . . . . . . 17 {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)} ∈ Fin
30 unfi 9168 . . . . . . . . . . . . . . . . 17 (({0} ∈ Fin ∧ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)} ∈ Fin) β†’ ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}) ∈ Fin)
3126, 29, 30mp2an 691 . . . . . . . . . . . . . . . 16 ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}) ∈ Fin
32 c0ex 11204 . . . . . . . . . . . . . . . . . 18 0 ∈ V
3332snid 4663 . . . . . . . . . . . . . . . . 17 0 ∈ {0}
34 elun1 4175 . . . . . . . . . . . . . . . . 17 (0 ∈ {0} β†’ 0 ∈ ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}))
35 ne0i 4333 . . . . . . . . . . . . . . . . 17 (0 ∈ ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}) β†’ ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}) β‰  βˆ…)
3633, 34, 35mp2b 10 . . . . . . . . . . . . . . . 16 ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}) β‰  βˆ…
37 0re 11212 . . . . . . . . . . . . . . . . . 18 0 ∈ ℝ
38 snssi 4810 . . . . . . . . . . . . . . . . . 18 (0 ∈ ℝ β†’ {0} βŠ† ℝ)
3937, 38ax-mp 5 . . . . . . . . . . . . . . . . 17 {0} βŠ† ℝ
40 ssrab2 4076 . . . . . . . . . . . . . . . . . 18 {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)} βŠ† (1...𝑁)
4116ssriv 3985 . . . . . . . . . . . . . . . . . . 19 (1...𝑁) βŠ† β„€
42 zssre 12561 . . . . . . . . . . . . . . . . . . 19 β„€ βŠ† ℝ
4341, 42sstri 3990 . . . . . . . . . . . . . . . . . 18 (1...𝑁) βŠ† ℝ
4440, 43sstri 3990 . . . . . . . . . . . . . . . . 17 {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)} βŠ† ℝ
4539, 44unssi 4184 . . . . . . . . . . . . . . . 16 ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}) βŠ† ℝ
4631, 36, 453pm3.2i 1340 . . . . . . . . . . . . . . 15 (({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}) ∈ Fin ∧ ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}) β‰  βˆ… ∧ ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}) βŠ† ℝ)
47 fisupcl 9460 . . . . . . . . . . . . . . 15 (( < Or ℝ ∧ (({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}) ∈ Fin ∧ ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}) β‰  βˆ… ∧ ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}) βŠ† ℝ)) β†’ sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) ∈ ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}))
4825, 46, 47mp2an 691 . . . . . . . . . . . . . 14 sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) ∈ ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)})
49 eleq1 2822 . . . . . . . . . . . . . 14 (𝑛 = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) β†’ (𝑛 ∈ ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}) ↔ sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) ∈ ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)})))
5048, 49mpbiri 258 . . . . . . . . . . . . 13 (𝑛 = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) β†’ 𝑛 ∈ ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}))
51 elun 4147 . . . . . . . . . . . . 13 (𝑛 ∈ ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}) ↔ (𝑛 ∈ {0} ∨ 𝑛 ∈ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}))
5250, 51sylib 217 . . . . . . . . . . . 12 (𝑛 = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) β†’ (𝑛 ∈ {0} ∨ 𝑛 ∈ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}))
53 oveq2 7412 . . . . . . . . . . . . . . . 16 (π‘Ž = 𝑛 β†’ (1...π‘Ž) = (1...𝑛))
5453raleqdv 3326 . . . . . . . . . . . . . . 15 (π‘Ž = 𝑛 β†’ (βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0) ↔ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)))
5554elrab 3682 . . . . . . . . . . . . . 14 (𝑛 ∈ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)} ↔ (𝑛 ∈ (1...𝑁) ∧ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)))
56 elfzuz 13493 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (1...𝑁) β†’ 𝑛 ∈ (β„€β‰₯β€˜1))
57 eluzfz2 13505 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (β„€β‰₯β€˜1) β†’ 𝑛 ∈ (1...𝑛))
5856, 57syl 17 . . . . . . . . . . . . . . 15 (𝑛 ∈ (1...𝑁) β†’ 𝑛 ∈ (1...𝑛))
59 simpl 484 . . . . . . . . . . . . . . . 16 ((0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0) β†’ 0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘))
6059ralimi 3084 . . . . . . . . . . . . . . 15 (βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0) β†’ βˆ€π‘ ∈ (1...𝑛)0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘))
61 fveq2 6888 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑛 β†’ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) = ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›))
6261breq2d 5159 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑛 β†’ (0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ↔ 0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›)))
6362rspcva 3610 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (1...𝑛) ∧ βˆ€π‘ ∈ (1...𝑛)0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘)) β†’ 0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›))
6458, 60, 63syl2an 597 . . . . . . . . . . . . . 14 ((𝑛 ∈ (1...𝑁) ∧ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)) β†’ 0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›))
6555, 64sylbi 216 . . . . . . . . . . . . 13 (𝑛 ∈ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)} β†’ 0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›))
6665orim2i 910 . . . . . . . . . . . 12 ((𝑛 ∈ {0} ∨ 𝑛 ∈ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}) β†’ (𝑛 ∈ {0} ∨ 0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›)))
6752, 66syl 17 . . . . . . . . . . 11 (𝑛 = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) β†’ (𝑛 ∈ {0} ∨ 0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›)))
68 orel1 888 . . . . . . . . . . 11 (Β¬ 𝑛 ∈ {0} β†’ ((𝑛 ∈ {0} ∨ 0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›)) β†’ 0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›)))
6924, 67, 68syl2im 40 . . . . . . . . . 10 (𝑛 ∈ (1...𝑁) β†’ (𝑛 = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) β†’ 0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›)))
7069reximdv 3171 . . . . . . . . 9 (𝑛 ∈ (1...𝑁) β†’ (βˆƒπ‘— ∈ (0...𝑁)𝑛 = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) β†’ βˆƒπ‘— ∈ (0...𝑁)0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›)))
7113, 70syl5 34 . . . . . . . 8 (𝑛 ∈ (1...𝑁) β†’ ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 𝑛 ∈ (0...𝑁))) β†’ βˆƒπ‘— ∈ (0...𝑁)0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›)))
725, 71sylan2i 607 . . . . . . 7 (𝑛 ∈ (1...𝑁) β†’ ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 𝑛 ∈ (1...𝑁))) β†’ βˆƒπ‘— ∈ (0...𝑁)0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›)))
732, 72mpcom 38 . . . . . 6 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 𝑛 ∈ (1...𝑁))) β†’ βˆƒπ‘— ∈ (0...𝑁)0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›))
74 breq 5149 . . . . . . 7 (π‘Ÿ = ≀ β†’ (0π‘Ÿ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ↔ 0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›)))
7574rexbidv 3179 . . . . . 6 (π‘Ÿ = ≀ β†’ (βˆƒπ‘— ∈ (0...𝑁)0π‘Ÿ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ↔ βˆƒπ‘— ∈ (0...𝑁)0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›)))
7673, 75syl5ibrcom 246 . . . . 5 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 𝑛 ∈ (1...𝑁))) β†’ (π‘Ÿ = ≀ β†’ βˆƒπ‘— ∈ (0...𝑁)0π‘Ÿ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›)))
77 poimir.0 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑁 ∈ β„•)
7877nnzd 12581 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑁 ∈ β„€)
79 elfzm1b 13575 . . . . . . . . . . . . . . 15 ((𝑛 ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ (𝑛 ∈ (1...𝑁) ↔ (𝑛 βˆ’ 1) ∈ (0...(𝑁 βˆ’ 1))))
8016, 78, 79syl2anr 598 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (𝑛 ∈ (1...𝑁) ↔ (𝑛 βˆ’ 1) ∈ (0...(𝑁 βˆ’ 1))))
8180biimpd 228 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...𝑁)) β†’ (𝑛 ∈ (1...𝑁) β†’ (𝑛 βˆ’ 1) ∈ (0...(𝑁 βˆ’ 1))))
8281ex 414 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑛 ∈ (1...𝑁) β†’ (𝑛 ∈ (1...𝑁) β†’ (𝑛 βˆ’ 1) ∈ (0...(𝑁 βˆ’ 1)))))
8382pm2.43d 53 . . . . . . . . . . 11 (πœ‘ β†’ (𝑛 ∈ (1...𝑁) β†’ (𝑛 βˆ’ 1) ∈ (0...(𝑁 βˆ’ 1))))
8477nncnd 12224 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑁 ∈ β„‚)
85 npcan1 11635 . . . . . . . . . . . . . . 15 (𝑁 ∈ β„‚ β†’ ((𝑁 βˆ’ 1) + 1) = 𝑁)
8684, 85syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝑁 βˆ’ 1) + 1) = 𝑁)
87 nnm1nn0 12509 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ β„• β†’ (𝑁 βˆ’ 1) ∈ β„•0)
8877, 87syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑁 βˆ’ 1) ∈ β„•0)
8988nn0zd 12580 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑁 βˆ’ 1) ∈ β„€)
90 uzid 12833 . . . . . . . . . . . . . . 15 ((𝑁 βˆ’ 1) ∈ β„€ β†’ (𝑁 βˆ’ 1) ∈ (β„€β‰₯β€˜(𝑁 βˆ’ 1)))
91 peano2uz 12881 . . . . . . . . . . . . . . 15 ((𝑁 βˆ’ 1) ∈ (β„€β‰₯β€˜(𝑁 βˆ’ 1)) β†’ ((𝑁 βˆ’ 1) + 1) ∈ (β„€β‰₯β€˜(𝑁 βˆ’ 1)))
9289, 90, 913syl 18 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝑁 βˆ’ 1) + 1) ∈ (β„€β‰₯β€˜(𝑁 βˆ’ 1)))
9386, 92eqeltrrd 2835 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑁 ∈ (β„€β‰₯β€˜(𝑁 βˆ’ 1)))
94 fzss2 13537 . . . . . . . . . . . . 13 (𝑁 ∈ (β„€β‰₯β€˜(𝑁 βˆ’ 1)) β†’ (0...(𝑁 βˆ’ 1)) βŠ† (0...𝑁))
9593, 94syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (0...(𝑁 βˆ’ 1)) βŠ† (0...𝑁))
9695sseld 3980 . . . . . . . . . . 11 (πœ‘ β†’ ((𝑛 βˆ’ 1) ∈ (0...(𝑁 βˆ’ 1)) β†’ (𝑛 βˆ’ 1) ∈ (0...𝑁)))
9783, 96syld 47 . . . . . . . . . 10 (πœ‘ β†’ (𝑛 ∈ (1...𝑁) β†’ (𝑛 βˆ’ 1) ∈ (0...𝑁)))
9897anim2d 613 . . . . . . . . 9 (πœ‘ β†’ ((π‘˜ ∈ β„• ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘˜ ∈ β„• ∧ (𝑛 βˆ’ 1) ∈ (0...𝑁))))
9998imp 408 . . . . . . . 8 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 𝑛 ∈ (1...𝑁))) β†’ (π‘˜ ∈ β„• ∧ (𝑛 βˆ’ 1) ∈ (0...𝑁)))
100 ovex 7437 . . . . . . . . 9 (𝑛 βˆ’ 1) ∈ V
101 eleq1 2822 . . . . . . . . . . . 12 (𝑖 = (𝑛 βˆ’ 1) β†’ (𝑖 ∈ (0...𝑁) ↔ (𝑛 βˆ’ 1) ∈ (0...𝑁)))
102101anbi2d 630 . . . . . . . . . . 11 (𝑖 = (𝑛 βˆ’ 1) β†’ ((π‘˜ ∈ β„• ∧ 𝑖 ∈ (0...𝑁)) ↔ (π‘˜ ∈ β„• ∧ (𝑛 βˆ’ 1) ∈ (0...𝑁))))
103102anbi2d 630 . . . . . . . . . 10 (𝑖 = (𝑛 βˆ’ 1) β†’ ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 𝑖 ∈ (0...𝑁))) ↔ (πœ‘ ∧ (π‘˜ ∈ β„• ∧ (𝑛 βˆ’ 1) ∈ (0...𝑁)))))
104 eqeq1 2737 . . . . . . . . . . 11 (𝑖 = (𝑛 βˆ’ 1) β†’ (𝑖 = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) ↔ (𝑛 βˆ’ 1) = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < )))
105104rexbidv 3179 . . . . . . . . . 10 (𝑖 = (𝑛 βˆ’ 1) β†’ (βˆƒπ‘— ∈ (0...𝑁)𝑖 = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) ↔ βˆƒπ‘— ∈ (0...𝑁)(𝑛 βˆ’ 1) = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < )))
106103, 105imbi12d 345 . . . . . . . . 9 (𝑖 = (𝑛 βˆ’ 1) β†’ (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 𝑖 ∈ (0...𝑁))) β†’ βˆƒπ‘— ∈ (0...𝑁)𝑖 = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < )) ↔ ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (𝑛 βˆ’ 1) ∈ (0...𝑁))) β†’ βˆƒπ‘— ∈ (0...𝑁)(𝑛 βˆ’ 1) = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ))))
107100, 106, 12vtocl 3549 . . . . . . . 8 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (𝑛 βˆ’ 1) ∈ (0...𝑁))) β†’ βˆƒπ‘— ∈ (0...𝑁)(𝑛 βˆ’ 1) = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ))
10899, 107syldan 592 . . . . . . 7 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 𝑛 ∈ (1...𝑁))) β†’ βˆƒπ‘— ∈ (0...𝑁)(𝑛 βˆ’ 1) = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ))
109 eleq1 2822 . . . . . . . . . . . . . . . 16 ((𝑛 βˆ’ 1) = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) β†’ ((𝑛 βˆ’ 1) ∈ ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}) ↔ sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) ∈ ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)})))
11048, 109mpbiri 258 . . . . . . . . . . . . . . 15 ((𝑛 βˆ’ 1) = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) β†’ (𝑛 βˆ’ 1) ∈ ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}))
111 elun 4147 . . . . . . . . . . . . . . . 16 ((𝑛 βˆ’ 1) ∈ ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}) ↔ ((𝑛 βˆ’ 1) ∈ {0} ∨ (𝑛 βˆ’ 1) ∈ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}))
112100elsn 4642 . . . . . . . . . . . . . . . . 17 ((𝑛 βˆ’ 1) ∈ {0} ↔ (𝑛 βˆ’ 1) = 0)
113 oveq2 7412 . . . . . . . . . . . . . . . . . . 19 (π‘Ž = (𝑛 βˆ’ 1) β†’ (1...π‘Ž) = (1...(𝑛 βˆ’ 1)))
114113raleqdv 3326 . . . . . . . . . . . . . . . . . 18 (π‘Ž = (𝑛 βˆ’ 1) β†’ (βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0) ↔ βˆ€π‘ ∈ (1...(𝑛 βˆ’ 1))(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)))
115114elrab 3682 . . . . . . . . . . . . . . . . 17 ((𝑛 βˆ’ 1) ∈ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)} ↔ ((𝑛 βˆ’ 1) ∈ (1...𝑁) ∧ βˆ€π‘ ∈ (1...(𝑛 βˆ’ 1))(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)))
116112, 115orbi12i 914 . . . . . . . . . . . . . . . 16 (((𝑛 βˆ’ 1) ∈ {0} ∨ (𝑛 βˆ’ 1) ∈ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}) ↔ ((𝑛 βˆ’ 1) = 0 ∨ ((𝑛 βˆ’ 1) ∈ (1...𝑁) ∧ βˆ€π‘ ∈ (1...(𝑛 βˆ’ 1))(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0))))
117111, 116bitri 275 . . . . . . . . . . . . . . 15 ((𝑛 βˆ’ 1) ∈ ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}) ↔ ((𝑛 βˆ’ 1) = 0 ∨ ((𝑛 βˆ’ 1) ∈ (1...𝑁) ∧ βˆ€π‘ ∈ (1...(𝑛 βˆ’ 1))(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0))))
118110, 117sylib 217 . . . . . . . . . . . . . 14 ((𝑛 βˆ’ 1) = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) β†’ ((𝑛 βˆ’ 1) = 0 ∨ ((𝑛 βˆ’ 1) ∈ (1...𝑁) ∧ βˆ€π‘ ∈ (1...(𝑛 βˆ’ 1))(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0))))
119118a1i 11 . . . . . . . . . . . . 13 (𝑛 ∈ (1...𝑁) β†’ ((𝑛 βˆ’ 1) = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) β†’ ((𝑛 βˆ’ 1) = 0 ∨ ((𝑛 βˆ’ 1) ∈ (1...𝑁) ∧ βˆ€π‘ ∈ (1...(𝑛 βˆ’ 1))(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)))))
120 ltm1 12052 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℝ β†’ (𝑛 βˆ’ 1) < 𝑛)
121 peano2rem 11523 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℝ β†’ (𝑛 βˆ’ 1) ∈ ℝ)
122 ltnle 11289 . . . . . . . . . . . . . . . . . . 19 (((𝑛 βˆ’ 1) ∈ ℝ ∧ 𝑛 ∈ ℝ) β†’ ((𝑛 βˆ’ 1) < 𝑛 ↔ Β¬ 𝑛 ≀ (𝑛 βˆ’ 1)))
123121, 122mpancom 687 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℝ β†’ ((𝑛 βˆ’ 1) < 𝑛 ↔ Β¬ 𝑛 ≀ (𝑛 βˆ’ 1)))
124120, 123mpbid 231 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℝ β†’ Β¬ 𝑛 ≀ (𝑛 βˆ’ 1))
12517, 124syl 17 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (1...𝑁) β†’ Β¬ 𝑛 ≀ (𝑛 βˆ’ 1))
126 breq2 5151 . . . . . . . . . . . . . . . . 17 ((𝑛 βˆ’ 1) = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) β†’ (𝑛 ≀ (𝑛 βˆ’ 1) ↔ 𝑛 ≀ sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < )))
127126notbid 318 . . . . . . . . . . . . . . . 16 ((𝑛 βˆ’ 1) = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) β†’ (Β¬ 𝑛 ≀ (𝑛 βˆ’ 1) ↔ Β¬ 𝑛 ≀ sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < )))
128125, 127syl5ibcom 244 . . . . . . . . . . . . . . 15 (𝑛 ∈ (1...𝑁) β†’ ((𝑛 βˆ’ 1) = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) β†’ Β¬ 𝑛 ≀ sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < )))
129 elun2 4176 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)} β†’ 𝑛 ∈ ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}))
130 fimaxre2 12155 . . . . . . . . . . . . . . . . . . . . 21 ((({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}) βŠ† ℝ ∧ ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}) ∈ Fin) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)})𝑦 ≀ π‘₯)
13145, 31, 130mp2an 691 . . . . . . . . . . . . . . . . . . . 20 βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)})𝑦 ≀ π‘₯
13245, 36, 1313pm3.2i 1340 . . . . . . . . . . . . . . . . . . 19 (({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}) βŠ† ℝ ∧ ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)})𝑦 ≀ π‘₯)
133132suprubii 12185 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}) β†’ 𝑛 ≀ sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ))
134129, 133syl 17 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)} β†’ 𝑛 ≀ sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ))
135134con3i 154 . . . . . . . . . . . . . . . 16 (Β¬ 𝑛 ≀ sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) β†’ Β¬ 𝑛 ∈ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)})
136 ianor 981 . . . . . . . . . . . . . . . . 17 (Β¬ (𝑛 ∈ (1...𝑁) ∧ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)) ↔ (Β¬ 𝑛 ∈ (1...𝑁) ∨ Β¬ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)))
137136, 55xchnxbir 333 . . . . . . . . . . . . . . . 16 (Β¬ 𝑛 ∈ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)} ↔ (Β¬ 𝑛 ∈ (1...𝑁) ∨ Β¬ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)))
138135, 137sylib 217 . . . . . . . . . . . . . . 15 (Β¬ 𝑛 ≀ sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) β†’ (Β¬ 𝑛 ∈ (1...𝑁) ∨ Β¬ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)))
139128, 138syl6 35 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) β†’ ((𝑛 βˆ’ 1) = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) β†’ (Β¬ 𝑛 ∈ (1...𝑁) ∨ Β¬ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0))))
140 pm2.63 940 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (1...𝑁) ∨ Β¬ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)) β†’ ((Β¬ 𝑛 ∈ (1...𝑁) ∨ Β¬ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)) β†’ Β¬ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)))
141140orcs 874 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) β†’ ((Β¬ 𝑛 ∈ (1...𝑁) ∨ Β¬ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)) β†’ Β¬ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)))
142139, 141syld 47 . . . . . . . . . . . . 13 (𝑛 ∈ (1...𝑁) β†’ ((𝑛 βˆ’ 1) = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) β†’ Β¬ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)))
143119, 142jcad 514 . . . . . . . . . . . 12 (𝑛 ∈ (1...𝑁) β†’ ((𝑛 βˆ’ 1) = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) β†’ (((𝑛 βˆ’ 1) = 0 ∨ ((𝑛 βˆ’ 1) ∈ (1...𝑁) ∧ βˆ€π‘ ∈ (1...(𝑛 βˆ’ 1))(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0))) ∧ Β¬ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0))))
144 andir 1008 . . . . . . . . . . . . . 14 ((((𝑛 βˆ’ 1) = 0 ∨ ((𝑛 βˆ’ 1) ∈ (1...𝑁) ∧ βˆ€π‘ ∈ (1...(𝑛 βˆ’ 1))(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0))) ∧ Β¬ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)) ↔ (((𝑛 βˆ’ 1) = 0 ∧ Β¬ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)) ∨ (((𝑛 βˆ’ 1) ∈ (1...𝑁) ∧ βˆ€π‘ ∈ (1...(𝑛 βˆ’ 1))(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)) ∧ Β¬ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0))))
14516zcnd 12663 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (1...𝑁) β†’ 𝑛 ∈ β„‚)
146 ax-1cn 11164 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ β„‚
147 0cn 11202 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ β„‚
148 subadd 11459 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ β„‚ ∧ 1 ∈ β„‚ ∧ 0 ∈ β„‚) β†’ ((𝑛 βˆ’ 1) = 0 ↔ (1 + 0) = 𝑛))
149146, 147, 148mp3an23 1454 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ β„‚ β†’ ((𝑛 βˆ’ 1) = 0 ↔ (1 + 0) = 𝑛))
150145, 149syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑁) β†’ ((𝑛 βˆ’ 1) = 0 ↔ (1 + 0) = 𝑛))
151150biimpa 478 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (1...𝑁) ∧ (𝑛 βˆ’ 1) = 0) β†’ (1 + 0) = 𝑛)
152 1p0e1 12332 . . . . . . . . . . . . . . . . . 18 (1 + 0) = 1
153151, 152eqtr3di 2788 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (1...𝑁) ∧ (𝑛 βˆ’ 1) = 0) β†’ 𝑛 = 1)
154 1z 12588 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ β„€
155 fzsn 13539 . . . . . . . . . . . . . . . . . . . . . 22 (1 ∈ β„€ β†’ (1...1) = {1})
156154, 155ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (1...1) = {1}
157 oveq2 7412 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 1 β†’ (1...𝑛) = (1...1))
158 sneq 4637 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 1 β†’ {𝑛} = {1})
159156, 157, 1583eqtr4a 2799 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 β†’ (1...𝑛) = {𝑛})
160159raleqdv 3326 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 β†’ (βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0) ↔ βˆ€π‘ ∈ {𝑛} (0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)))
161160notbid 318 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 β†’ (Β¬ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0) ↔ Β¬ βˆ€π‘ ∈ {𝑛} (0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)))
162161biimpd 228 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 β†’ (Β¬ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0) β†’ Β¬ βˆ€π‘ ∈ {𝑛} (0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)))
163153, 162syl 17 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (1...𝑁) ∧ (𝑛 βˆ’ 1) = 0) β†’ (Β¬ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0) β†’ Β¬ βˆ€π‘ ∈ {𝑛} (0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)))
164163expimpd 455 . . . . . . . . . . . . . . 15 (𝑛 ∈ (1...𝑁) β†’ (((𝑛 βˆ’ 1) = 0 ∧ Β¬ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)) β†’ Β¬ βˆ€π‘ ∈ {𝑛} (0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)))
165 ralun 4191 . . . . . . . . . . . . . . . . . . . 20 ((βˆ€π‘ ∈ (1...(𝑛 βˆ’ 1))(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0) ∧ βˆ€π‘ ∈ {𝑛} (0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)) β†’ βˆ€π‘ ∈ ((1...(𝑛 βˆ’ 1)) βˆͺ {𝑛})(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0))
166 npcan1 11635 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ β„‚ β†’ ((𝑛 βˆ’ 1) + 1) = 𝑛)
167145, 166syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) β†’ ((𝑛 βˆ’ 1) + 1) = 𝑛)
168167, 56eqeltrd 2834 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...𝑁) β†’ ((𝑛 βˆ’ 1) + 1) ∈ (β„€β‰₯β€˜1))
169 peano2zm 12601 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ β„€ β†’ (𝑛 βˆ’ 1) ∈ β„€)
170 uzid 12833 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 βˆ’ 1) ∈ β„€ β†’ (𝑛 βˆ’ 1) ∈ (β„€β‰₯β€˜(𝑛 βˆ’ 1)))
171 peano2uz 12881 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 βˆ’ 1) ∈ (β„€β‰₯β€˜(𝑛 βˆ’ 1)) β†’ ((𝑛 βˆ’ 1) + 1) ∈ (β„€β‰₯β€˜(𝑛 βˆ’ 1)))
17216, 169, 170, 1714syl 19 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) β†’ ((𝑛 βˆ’ 1) + 1) ∈ (β„€β‰₯β€˜(𝑛 βˆ’ 1)))
173167, 172eqeltrrd 2835 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...𝑁) β†’ 𝑛 ∈ (β„€β‰₯β€˜(𝑛 βˆ’ 1)))
174 fzsplit2 13522 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑛 βˆ’ 1) + 1) ∈ (β„€β‰₯β€˜1) ∧ 𝑛 ∈ (β„€β‰₯β€˜(𝑛 βˆ’ 1))) β†’ (1...𝑛) = ((1...(𝑛 βˆ’ 1)) βˆͺ (((𝑛 βˆ’ 1) + 1)...𝑛)))
175168, 173, 174syl2anc 585 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (1...𝑁) β†’ (1...𝑛) = ((1...(𝑛 βˆ’ 1)) βˆͺ (((𝑛 βˆ’ 1) + 1)...𝑛)))
176167oveq1d 7419 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) β†’ (((𝑛 βˆ’ 1) + 1)...𝑛) = (𝑛...𝑛))
177 fzsn 13539 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ β„€ β†’ (𝑛...𝑛) = {𝑛})
17816, 177syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) β†’ (𝑛...𝑛) = {𝑛})
179176, 178eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...𝑁) β†’ (((𝑛 βˆ’ 1) + 1)...𝑛) = {𝑛})
180179uneq2d 4162 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (1...𝑁) β†’ ((1...(𝑛 βˆ’ 1)) βˆͺ (((𝑛 βˆ’ 1) + 1)...𝑛)) = ((1...(𝑛 βˆ’ 1)) βˆͺ {𝑛}))
181175, 180eqtrd 2773 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (1...𝑁) β†’ (1...𝑛) = ((1...(𝑛 βˆ’ 1)) βˆͺ {𝑛}))
182181raleqdv 3326 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (1...𝑁) β†’ (βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0) ↔ βˆ€π‘ ∈ ((1...(𝑛 βˆ’ 1)) βˆͺ {𝑛})(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)))
183165, 182imbitrrid 245 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑁) β†’ ((βˆ€π‘ ∈ (1...(𝑛 βˆ’ 1))(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0) ∧ βˆ€π‘ ∈ {𝑛} (0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)) β†’ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)))
184183expdimp 454 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ (1...𝑁) ∧ βˆ€π‘ ∈ (1...(𝑛 βˆ’ 1))(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)) β†’ (βˆ€π‘ ∈ {𝑛} (0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0) β†’ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)))
185184con3d 152 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (1...𝑁) ∧ βˆ€π‘ ∈ (1...(𝑛 βˆ’ 1))(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)) β†’ (Β¬ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0) β†’ Β¬ βˆ€π‘ ∈ {𝑛} (0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)))
186185adantrl 715 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (1...𝑁) ∧ ((𝑛 βˆ’ 1) ∈ (1...𝑁) ∧ βˆ€π‘ ∈ (1...(𝑛 βˆ’ 1))(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0))) β†’ (Β¬ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0) β†’ Β¬ βˆ€π‘ ∈ {𝑛} (0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)))
187186expimpd 455 . . . . . . . . . . . . . . 15 (𝑛 ∈ (1...𝑁) β†’ ((((𝑛 βˆ’ 1) ∈ (1...𝑁) ∧ βˆ€π‘ ∈ (1...(𝑛 βˆ’ 1))(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)) ∧ Β¬ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)) β†’ Β¬ βˆ€π‘ ∈ {𝑛} (0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)))
188164, 187jaod 858 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) β†’ ((((𝑛 βˆ’ 1) = 0 ∧ Β¬ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)) ∨ (((𝑛 βˆ’ 1) ∈ (1...𝑁) ∧ βˆ€π‘ ∈ (1...(𝑛 βˆ’ 1))(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)) ∧ Β¬ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0))) β†’ Β¬ βˆ€π‘ ∈ {𝑛} (0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)))
189144, 188biimtrid 241 . . . . . . . . . . . . 13 (𝑛 ∈ (1...𝑁) β†’ ((((𝑛 βˆ’ 1) = 0 ∨ ((𝑛 βˆ’ 1) ∈ (1...𝑁) ∧ βˆ€π‘ ∈ (1...(𝑛 βˆ’ 1))(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0))) ∧ Β¬ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)) β†’ Β¬ βˆ€π‘ ∈ {𝑛} (0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)))
190 fveq2 6888 . . . . . . . . . . . . . . . . . 18 (𝑏 = 𝑛 β†’ (π‘ƒβ€˜π‘) = (π‘ƒβ€˜π‘›))
191190neeq1d 3001 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝑛 β†’ ((π‘ƒβ€˜π‘) β‰  0 ↔ (π‘ƒβ€˜π‘›) β‰  0))
19262, 191anbi12d 632 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑛 β†’ ((0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0) ↔ (0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ∧ (π‘ƒβ€˜π‘›) β‰  0)))
193192ralsng 4676 . . . . . . . . . . . . . . 15 (𝑛 ∈ (1...𝑁) β†’ (βˆ€π‘ ∈ {𝑛} (0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0) ↔ (0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ∧ (π‘ƒβ€˜π‘›) β‰  0)))
194193notbid 318 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) β†’ (Β¬ βˆ€π‘ ∈ {𝑛} (0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0) ↔ Β¬ (0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ∧ (π‘ƒβ€˜π‘›) β‰  0)))
195 ianor 981 . . . . . . . . . . . . . . 15 (Β¬ (0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ∧ (π‘ƒβ€˜π‘›) β‰  0) ↔ (Β¬ 0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ∨ Β¬ (π‘ƒβ€˜π‘›) β‰  0))
196 nne 2945 . . . . . . . . . . . . . . . 16 (Β¬ (π‘ƒβ€˜π‘›) β‰  0 ↔ (π‘ƒβ€˜π‘›) = 0)
197196orbi2i 912 . . . . . . . . . . . . . . 15 ((Β¬ 0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ∨ Β¬ (π‘ƒβ€˜π‘›) β‰  0) ↔ (Β¬ 0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ∨ (π‘ƒβ€˜π‘›) = 0))
198195, 197bitri 275 . . . . . . . . . . . . . 14 (Β¬ (0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ∧ (π‘ƒβ€˜π‘›) β‰  0) ↔ (Β¬ 0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ∨ (π‘ƒβ€˜π‘›) = 0))
199194, 198bitrdi 287 . . . . . . . . . . . . 13 (𝑛 ∈ (1...𝑁) β†’ (Β¬ βˆ€π‘ ∈ {𝑛} (0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0) ↔ (Β¬ 0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ∨ (π‘ƒβ€˜π‘›) = 0)))
200189, 199sylibd 238 . . . . . . . . . . . 12 (𝑛 ∈ (1...𝑁) β†’ ((((𝑛 βˆ’ 1) = 0 ∨ ((𝑛 βˆ’ 1) ∈ (1...𝑁) ∧ βˆ€π‘ ∈ (1...(𝑛 βˆ’ 1))(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0))) ∧ Β¬ βˆ€π‘ ∈ (1...𝑛)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)) β†’ (Β¬ 0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ∨ (π‘ƒβ€˜π‘›) = 0)))
201143, 200syld 47 . . . . . . . . . . 11 (𝑛 ∈ (1...𝑁) β†’ ((𝑛 βˆ’ 1) = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) β†’ (Β¬ 0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ∨ (π‘ƒβ€˜π‘›) = 0)))
202201ad2antlr 726 . . . . . . . . . 10 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) β†’ ((𝑛 βˆ’ 1) = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) β†’ (Β¬ 0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ∨ (π‘ƒβ€˜π‘›) = 0)))
203 poimir.1 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐹 ∈ ((𝑅 β†Ύt 𝐼) Cn 𝑅))
204 poimir.r . . . . . . . . . . . . . . . . . . . . . 22 𝑅 = (∏tβ€˜((1...𝑁) Γ— {(topGenβ€˜ran (,))}))
205 retop 24260 . . . . . . . . . . . . . . . . . . . . . . . 24 (topGenβ€˜ran (,)) ∈ Top
206205fconst6 6778 . . . . . . . . . . . . . . . . . . . . . . 23 ((1...𝑁) Γ— {(topGenβ€˜ran (,))}):(1...𝑁)⟢Top
207 pttop 23068 . . . . . . . . . . . . . . . . . . . . . . 23 (((1...𝑁) ∈ Fin ∧ ((1...𝑁) Γ— {(topGenβ€˜ran (,))}):(1...𝑁)⟢Top) β†’ (∏tβ€˜((1...𝑁) Γ— {(topGenβ€˜ran (,))})) ∈ Top)
20827, 206, 207mp2an 691 . . . . . . . . . . . . . . . . . . . . . 22 (∏tβ€˜((1...𝑁) Γ— {(topGenβ€˜ran (,))})) ∈ Top
209204, 208eqeltri 2830 . . . . . . . . . . . . . . . . . . . . 21 𝑅 ∈ Top
210 poimir.i . . . . . . . . . . . . . . . . . . . . . 22 𝐼 = ((0[,]1) ↑m (1...𝑁))
211 reex 11197 . . . . . . . . . . . . . . . . . . . . . . 23 ℝ ∈ V
212 unitssre 13472 . . . . . . . . . . . . . . . . . . . . . . 23 (0[,]1) βŠ† ℝ
213 mapss 8879 . . . . . . . . . . . . . . . . . . . . . . 23 ((ℝ ∈ V ∧ (0[,]1) βŠ† ℝ) β†’ ((0[,]1) ↑m (1...𝑁)) βŠ† (ℝ ↑m (1...𝑁)))
214211, 212, 213mp2an 691 . . . . . . . . . . . . . . . . . . . . . 22 ((0[,]1) ↑m (1...𝑁)) βŠ† (ℝ ↑m (1...𝑁))
215210, 214eqsstri 4015 . . . . . . . . . . . . . . . . . . . . 21 𝐼 βŠ† (ℝ ↑m (1...𝑁))
216 uniretop 24261 . . . . . . . . . . . . . . . . . . . . . . . 24 ℝ = βˆͺ (topGenβ€˜ran (,))
217204, 216ptuniconst 23084 . . . . . . . . . . . . . . . . . . . . . . 23 (((1...𝑁) ∈ Fin ∧ (topGenβ€˜ran (,)) ∈ Top) β†’ (ℝ ↑m (1...𝑁)) = βˆͺ 𝑅)
21827, 205, 217mp2an 691 . . . . . . . . . . . . . . . . . . . . . 22 (ℝ ↑m (1...𝑁)) = βˆͺ 𝑅
219218restuni 22648 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ Top ∧ 𝐼 βŠ† (ℝ ↑m (1...𝑁))) β†’ 𝐼 = βˆͺ (𝑅 β†Ύt 𝐼))
220209, 215, 219mp2an 691 . . . . . . . . . . . . . . . . . . . 20 𝐼 = βˆͺ (𝑅 β†Ύt 𝐼)
221220, 218cnf 22732 . . . . . . . . . . . . . . . . . . 19 (𝐹 ∈ ((𝑅 β†Ύt 𝐼) Cn 𝑅) β†’ 𝐹:𝐼⟢(ℝ ↑m (1...𝑁)))
222203, 221syl 17 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐹:𝐼⟢(ℝ ↑m (1...𝑁)))
223222ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (0...𝑁)) β†’ 𝐹:𝐼⟢(ℝ ↑m (1...𝑁)))
224 simplr 768 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (0...𝑁)) β†’ π‘˜ ∈ β„•)
225 elfzelz 13497 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π‘₯ ∈ (0...π‘˜) β†’ π‘₯ ∈ β„€)
226225zred 12662 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘₯ ∈ (0...π‘˜) β†’ π‘₯ ∈ ℝ)
227226adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘₯ ∈ (0...π‘˜) ∧ π‘˜ ∈ β„•) β†’ π‘₯ ∈ ℝ)
228 nnre 12215 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘˜ ∈ β„• β†’ π‘˜ ∈ ℝ)
229228adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘₯ ∈ (0...π‘˜) ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ ℝ)
230 nnne0 12242 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘˜ ∈ β„• β†’ π‘˜ β‰  0)
231230adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘₯ ∈ (0...π‘˜) ∧ π‘˜ ∈ β„•) β†’ π‘˜ β‰  0)
232227, 229, 231redivcld 12038 . . . . . . . . . . . . . . . . . . . . . . . 24 ((π‘₯ ∈ (0...π‘˜) ∧ π‘˜ ∈ β„•) β†’ (π‘₯ / π‘˜) ∈ ℝ)
233 elfzle1 13500 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘₯ ∈ (0...π‘˜) β†’ 0 ≀ π‘₯)
234226, 233jca 513 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ ∈ (0...π‘˜) β†’ (π‘₯ ∈ ℝ ∧ 0 ≀ π‘₯))
235 nnrp 12981 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘˜ ∈ β„• β†’ π‘˜ ∈ ℝ+)
236235rpregt0d 13018 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘˜ ∈ β„• β†’ (π‘˜ ∈ ℝ ∧ 0 < π‘˜))
237 divge0 12079 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((π‘₯ ∈ ℝ ∧ 0 ≀ π‘₯) ∧ (π‘˜ ∈ ℝ ∧ 0 < π‘˜)) β†’ 0 ≀ (π‘₯ / π‘˜))
238234, 236, 237syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . 24 ((π‘₯ ∈ (0...π‘˜) ∧ π‘˜ ∈ β„•) β†’ 0 ≀ (π‘₯ / π‘˜))
239 elfzle2 13501 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘₯ ∈ (0...π‘˜) β†’ π‘₯ ≀ π‘˜)
240239adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘₯ ∈ (0...π‘˜) ∧ π‘˜ ∈ β„•) β†’ π‘₯ ≀ π‘˜)
241 1red 11211 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((π‘₯ ∈ (0...π‘˜) ∧ π‘˜ ∈ β„•) β†’ 1 ∈ ℝ)
242235adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((π‘₯ ∈ (0...π‘˜) ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ ℝ+)
243227, 241, 242ledivmuld 13065 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘₯ ∈ (0...π‘˜) ∧ π‘˜ ∈ β„•) β†’ ((π‘₯ / π‘˜) ≀ 1 ↔ π‘₯ ≀ (π‘˜ Β· 1)))
244 nncn 12216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„‚)
245244mulridd 11227 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (π‘˜ ∈ β„• β†’ (π‘˜ Β· 1) = π‘˜)
246245breq2d 5159 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π‘˜ ∈ β„• β†’ (π‘₯ ≀ (π‘˜ Β· 1) ↔ π‘₯ ≀ π‘˜))
247246adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘₯ ∈ (0...π‘˜) ∧ π‘˜ ∈ β„•) β†’ (π‘₯ ≀ (π‘˜ Β· 1) ↔ π‘₯ ≀ π‘˜))
248243, 247bitrd 279 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘₯ ∈ (0...π‘˜) ∧ π‘˜ ∈ β„•) β†’ ((π‘₯ / π‘˜) ≀ 1 ↔ π‘₯ ≀ π‘˜))
249240, 248mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . 24 ((π‘₯ ∈ (0...π‘˜) ∧ π‘˜ ∈ β„•) β†’ (π‘₯ / π‘˜) ≀ 1)
250 elicc01 13439 . . . . . . . . . . . . . . . . . . . . . . . 24 ((π‘₯ / π‘˜) ∈ (0[,]1) ↔ ((π‘₯ / π‘˜) ∈ ℝ ∧ 0 ≀ (π‘₯ / π‘˜) ∧ (π‘₯ / π‘˜) ≀ 1))
251232, 238, 249, 250syl3anbrc 1344 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘₯ ∈ (0...π‘˜) ∧ π‘˜ ∈ β„•) β†’ (π‘₯ / π‘˜) ∈ (0[,]1))
252251ancoms 460 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘˜ ∈ β„• ∧ π‘₯ ∈ (0...π‘˜)) β†’ (π‘₯ / π‘˜) ∈ (0[,]1))
253 elsni 4644 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ {π‘˜} β†’ 𝑦 = π‘˜)
254253oveq2d 7420 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ {π‘˜} β†’ (π‘₯ / 𝑦) = (π‘₯ / π‘˜))
255254eleq1d 2819 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ {π‘˜} β†’ ((π‘₯ / 𝑦) ∈ (0[,]1) ↔ (π‘₯ / π‘˜) ∈ (0[,]1)))
256252, 255syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . 21 ((π‘˜ ∈ β„• ∧ π‘₯ ∈ (0...π‘˜)) β†’ (𝑦 ∈ {π‘˜} β†’ (π‘₯ / 𝑦) ∈ (0[,]1)))
257256impr 456 . . . . . . . . . . . . . . . . . . . 20 ((π‘˜ ∈ β„• ∧ (π‘₯ ∈ (0...π‘˜) ∧ 𝑦 ∈ {π‘˜})) β†’ (π‘₯ / 𝑦) ∈ (0[,]1))
258224, 257sylan 581 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘₯ ∈ (0...π‘˜) ∧ 𝑦 ∈ {π‘˜})) β†’ (π‘₯ / 𝑦) ∈ (0[,]1))
259 elun 4147 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ({1} βˆͺ {0}) ↔ (𝑦 ∈ {1} ∨ 𝑦 ∈ {0}))
260 fzofzp1 13725 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘₯ ∈ (0..^π‘˜) β†’ (π‘₯ + 1) ∈ (0...π‘˜))
261 elsni 4644 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ {1} β†’ 𝑦 = 1)
262261oveq2d 7420 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ {1} β†’ (π‘₯ + 𝑦) = (π‘₯ + 1))
263262eleq1d 2819 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ {1} β†’ ((π‘₯ + 𝑦) ∈ (0...π‘˜) ↔ (π‘₯ + 1) ∈ (0...π‘˜)))
264260, 263syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ ∈ (0..^π‘˜) β†’ (𝑦 ∈ {1} β†’ (π‘₯ + 𝑦) ∈ (0...π‘˜)))
265 elfzonn0 13673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (π‘₯ ∈ (0..^π‘˜) β†’ π‘₯ ∈ β„•0)
266265nn0cnd 12530 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (π‘₯ ∈ (0..^π‘˜) β†’ π‘₯ ∈ β„‚)
267266addridd 11410 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π‘₯ ∈ (0..^π‘˜) β†’ (π‘₯ + 0) = π‘₯)
268 elfzofz 13644 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π‘₯ ∈ (0..^π‘˜) β†’ π‘₯ ∈ (0...π‘˜))
269267, 268eqeltrd 2834 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘₯ ∈ (0..^π‘˜) β†’ (π‘₯ + 0) ∈ (0...π‘˜))
270 elsni 4644 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ {0} β†’ 𝑦 = 0)
271270oveq2d 7420 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ {0} β†’ (π‘₯ + 𝑦) = (π‘₯ + 0))
272271eleq1d 2819 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ {0} β†’ ((π‘₯ + 𝑦) ∈ (0...π‘˜) ↔ (π‘₯ + 0) ∈ (0...π‘˜)))
273269, 272syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ ∈ (0..^π‘˜) β†’ (𝑦 ∈ {0} β†’ (π‘₯ + 𝑦) ∈ (0...π‘˜)))
274264, 273jaod 858 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘₯ ∈ (0..^π‘˜) β†’ ((𝑦 ∈ {1} ∨ 𝑦 ∈ {0}) β†’ (π‘₯ + 𝑦) ∈ (0...π‘˜)))
275259, 274biimtrid 241 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ ∈ (0..^π‘˜) β†’ (𝑦 ∈ ({1} βˆͺ {0}) β†’ (π‘₯ + 𝑦) ∈ (0...π‘˜)))
276275imp 408 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘₯ ∈ (0..^π‘˜) ∧ 𝑦 ∈ ({1} βˆͺ {0})) β†’ (π‘₯ + 𝑦) ∈ (0...π‘˜))
277276adantl 483 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘₯ ∈ (0..^π‘˜) ∧ 𝑦 ∈ ({1} βˆͺ {0}))) β†’ (π‘₯ + 𝑦) ∈ (0...π‘˜))
278 poimirlem31.3 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 𝐺:β„•βŸΆ((β„•0 ↑m (1...𝑁)) Γ— {𝑓 ∣ 𝑓:(1...𝑁)–1-1-ontoβ†’(1...𝑁)}))
279278ffvelcdmda 7082 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (πΊβ€˜π‘˜) ∈ ((β„•0 ↑m (1...𝑁)) Γ— {𝑓 ∣ 𝑓:(1...𝑁)–1-1-ontoβ†’(1...𝑁)}))
280 xp1st 8002 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πΊβ€˜π‘˜) ∈ ((β„•0 ↑m (1...𝑁)) Γ— {𝑓 ∣ 𝑓:(1...𝑁)–1-1-ontoβ†’(1...𝑁)}) β†’ (1st β€˜(πΊβ€˜π‘˜)) ∈ (β„•0 ↑m (1...𝑁)))
281 elmapfn 8855 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1st β€˜(πΊβ€˜π‘˜)) ∈ (β„•0 ↑m (1...𝑁)) β†’ (1st β€˜(πΊβ€˜π‘˜)) Fn (1...𝑁))
282279, 280, 2813syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1st β€˜(πΊβ€˜π‘˜)) Fn (1...𝑁))
283 poimirlem31.4 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ran (1st β€˜(πΊβ€˜π‘˜)) βŠ† (0..^π‘˜))
284 df-f 6544 . . . . . . . . . . . . . . . . . . . . . . 23 ((1st β€˜(πΊβ€˜π‘˜)):(1...𝑁)⟢(0..^π‘˜) ↔ ((1st β€˜(πΊβ€˜π‘˜)) Fn (1...𝑁) ∧ ran (1st β€˜(πΊβ€˜π‘˜)) βŠ† (0..^π‘˜)))
285282, 283, 284sylanbrc 584 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1st β€˜(πΊβ€˜π‘˜)):(1...𝑁)⟢(0..^π‘˜))
286285adantr 482 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (0...𝑁)) β†’ (1st β€˜(πΊβ€˜π‘˜)):(1...𝑁)⟢(0..^π‘˜))
287 1ex 11206 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ V
288287fconst 6774 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2nd β€˜(πΊβ€˜π‘˜)) β€œ (1...𝑗)) Γ— {1}):((2nd β€˜(πΊβ€˜π‘˜)) β€œ (1...𝑗))⟢{1}
28932fconst 6774 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((𝑗 + 1)...𝑁)) Γ— {0}):((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((𝑗 + 1)...𝑁))⟢{0}
290288, 289pm3.2i 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((((2nd β€˜(πΊβ€˜π‘˜)) β€œ (1...𝑗)) Γ— {1}):((2nd β€˜(πΊβ€˜π‘˜)) β€œ (1...𝑗))⟢{1} ∧ (((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((𝑗 + 1)...𝑁)) Γ— {0}):((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((𝑗 + 1)...𝑁))⟢{0})
291 xp2nd 8003 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πΊβ€˜π‘˜) ∈ ((β„•0 ↑m (1...𝑁)) Γ— {𝑓 ∣ 𝑓:(1...𝑁)–1-1-ontoβ†’(1...𝑁)}) β†’ (2nd β€˜(πΊβ€˜π‘˜)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-ontoβ†’(1...𝑁)})
292279, 291syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (2nd β€˜(πΊβ€˜π‘˜)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-ontoβ†’(1...𝑁)})
293 fvex 6901 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (2nd β€˜(πΊβ€˜π‘˜)) ∈ V
294 f1oeq1 6818 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓 = (2nd β€˜(πΊβ€˜π‘˜)) β†’ (𝑓:(1...𝑁)–1-1-ontoβ†’(1...𝑁) ↔ (2nd β€˜(πΊβ€˜π‘˜)):(1...𝑁)–1-1-ontoβ†’(1...𝑁)))
295293, 294elab 3667 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2nd β€˜(πΊβ€˜π‘˜)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-ontoβ†’(1...𝑁)} ↔ (2nd β€˜(πΊβ€˜π‘˜)):(1...𝑁)–1-1-ontoβ†’(1...𝑁))
296292, 295sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (2nd β€˜(πΊβ€˜π‘˜)):(1...𝑁)–1-1-ontoβ†’(1...𝑁))
297 dff1o3 6836 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2nd β€˜(πΊβ€˜π‘˜)):(1...𝑁)–1-1-ontoβ†’(1...𝑁) ↔ ((2nd β€˜(πΊβ€˜π‘˜)):(1...𝑁)–ontoβ†’(1...𝑁) ∧ Fun β—‘(2nd β€˜(πΊβ€˜π‘˜))))
298297simprbi 498 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2nd β€˜(πΊβ€˜π‘˜)):(1...𝑁)–1-1-ontoβ†’(1...𝑁) β†’ Fun β—‘(2nd β€˜(πΊβ€˜π‘˜)))
299 imain 6630 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Fun β—‘(2nd β€˜(πΊβ€˜π‘˜)) β†’ ((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd β€˜(πΊβ€˜π‘˜)) β€œ (1...𝑗)) ∩ ((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((𝑗 + 1)...𝑁))))
300296, 298, 2993syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2nd β€˜(πΊβ€˜π‘˜)) β€œ (1...𝑗)) ∩ ((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((𝑗 + 1)...𝑁))))
301 elfznn0 13590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0...𝑁) β†’ 𝑗 ∈ β„•0)
302301nn0red 12529 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (0...𝑁) β†’ 𝑗 ∈ ℝ)
303302ltp1d 12140 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑁) β†’ 𝑗 < (𝑗 + 1))
304 fzdisj 13524 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 < (𝑗 + 1) β†’ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = βˆ…)
305303, 304syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ (0...𝑁) β†’ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = βˆ…)
306305imaeq2d 6057 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 ∈ (0...𝑁) β†’ ((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((2nd β€˜(πΊβ€˜π‘˜)) β€œ βˆ…))
307 ima0 6073 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2nd β€˜(πΊβ€˜π‘˜)) β€œ βˆ…) = βˆ…
308306, 307eqtrdi 2789 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (0...𝑁) β†’ ((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = βˆ…)
309300, 308sylan9req 2794 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (0...𝑁)) β†’ (((2nd β€˜(πΊβ€˜π‘˜)) β€œ (1...𝑗)) ∩ ((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((𝑗 + 1)...𝑁))) = βˆ…)
310 fun 6750 . . . . . . . . . . . . . . . . . . . . . . 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}))
311290, 309, 310sylancr 588 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (0...𝑁)) β†’ ((((2nd β€˜(πΊβ€˜π‘˜)) β€œ (1...𝑗)) Γ— {1}) βˆͺ (((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((𝑗 + 1)...𝑁)) Γ— {0})):(((2nd β€˜(πΊβ€˜π‘˜)) β€œ (1...𝑗)) βˆͺ ((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((𝑗 + 1)...𝑁)))⟢({1} βˆͺ {0}))
312 imaundi 6146 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((1...𝑗) βˆͺ ((𝑗 + 1)...𝑁))) = (((2nd β€˜(πΊβ€˜π‘˜)) β€œ (1...𝑗)) βˆͺ ((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((𝑗 + 1)...𝑁)))
313 nn0p1nn 12507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ β„•0 β†’ (𝑗 + 1) ∈ β„•)
314301, 313syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0...𝑁) β†’ (𝑗 + 1) ∈ β„•)
315 nnuz 12861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 β„• = (β„€β‰₯β€˜1)
316314, 315eleqtrdi 2844 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (0...𝑁) β†’ (𝑗 + 1) ∈ (β„€β‰₯β€˜1))
317 elfzuz3 13494 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (0...𝑁) β†’ 𝑁 ∈ (β„€β‰₯β€˜π‘—))
318 fzsplit2 13522 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑗 + 1) ∈ (β„€β‰₯β€˜1) ∧ 𝑁 ∈ (β„€β‰₯β€˜π‘—)) β†’ (1...𝑁) = ((1...𝑗) βˆͺ ((𝑗 + 1)...𝑁)))
319316, 317, 318syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑁) β†’ (1...𝑁) = ((1...𝑗) βˆͺ ((𝑗 + 1)...𝑁)))
320319imaeq2d 6057 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ (0...𝑁) β†’ ((2nd β€˜(πΊβ€˜π‘˜)) β€œ (1...𝑁)) = ((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((1...𝑗) βˆͺ ((𝑗 + 1)...𝑁))))
321 f1ofo 6837 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((2nd β€˜(πΊβ€˜π‘˜)):(1...𝑁)–1-1-ontoβ†’(1...𝑁) β†’ (2nd β€˜(πΊβ€˜π‘˜)):(1...𝑁)–ontoβ†’(1...𝑁))
322 foima 6807 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((2nd β€˜(πΊβ€˜π‘˜)):(1...𝑁)–ontoβ†’(1...𝑁) β†’ ((2nd β€˜(πΊβ€˜π‘˜)) β€œ (1...𝑁)) = (1...𝑁))
323296, 321, 3223syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((2nd β€˜(πΊβ€˜π‘˜)) β€œ (1...𝑁)) = (1...𝑁))
324320, 323sylan9req 2794 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗 ∈ (0...𝑁) ∧ (πœ‘ ∧ π‘˜ ∈ β„•)) β†’ ((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((1...𝑗) βˆͺ ((𝑗 + 1)...𝑁))) = (1...𝑁))
325324ancoms 460 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (0...𝑁)) β†’ ((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((1...𝑗) βˆͺ ((𝑗 + 1)...𝑁))) = (1...𝑁))
326312, 325eqtr3id 2787 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (0...𝑁)) β†’ (((2nd β€˜(πΊβ€˜π‘˜)) β€œ (1...𝑗)) βˆͺ ((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((𝑗 + 1)...𝑁))) = (1...𝑁))
327326feq2d 6700 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (0...𝑁)) β†’ (((((2nd β€˜(πΊβ€˜π‘˜)) β€œ (1...𝑗)) Γ— {1}) βˆͺ (((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((𝑗 + 1)...𝑁)) Γ— {0})):(((2nd β€˜(πΊβ€˜π‘˜)) β€œ (1...𝑗)) βˆͺ ((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((𝑗 + 1)...𝑁)))⟢({1} βˆͺ {0}) ↔ ((((2nd β€˜(πΊβ€˜π‘˜)) β€œ (1...𝑗)) Γ— {1}) βˆͺ (((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((𝑗 + 1)...𝑁)) Γ— {0})):(1...𝑁)⟢({1} βˆͺ {0})))
328311, 327mpbid 231 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (0...𝑁)) β†’ ((((2nd β€˜(πΊβ€˜π‘˜)) β€œ (1...𝑗)) Γ— {1}) βˆͺ (((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((𝑗 + 1)...𝑁)) Γ— {0})):(1...𝑁)⟢({1} βˆͺ {0}))
329 fzfid 13934 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (0...𝑁)) β†’ (1...𝑁) ∈ Fin)
330 inidm 4217 . . . . . . . . . . . . . . . . . . . . 21 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
331277, 286, 328, 329, 329, 330off 7683 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (0...𝑁)) β†’ ((1st β€˜(πΊβ€˜π‘˜)) ∘f + ((((2nd β€˜(πΊβ€˜π‘˜)) β€œ (1...𝑗)) Γ— {1}) βˆͺ (((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((𝑗 + 1)...𝑁)) Γ— {0}))):(1...𝑁)⟢(0...π‘˜))
332 poimirlem31.p . . . . . . . . . . . . . . . . . . . . 21 𝑃 = ((1st β€˜(πΊβ€˜π‘˜)) ∘f + ((((2nd β€˜(πΊβ€˜π‘˜)) β€œ (1...𝑗)) Γ— {1}) βˆͺ (((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((𝑗 + 1)...𝑁)) Γ— {0})))
333332feq1i 6705 . . . . . . . . . . . . . . . . . . . 20 (𝑃:(1...𝑁)⟢(0...π‘˜) ↔ ((1st β€˜(πΊβ€˜π‘˜)) ∘f + ((((2nd β€˜(πΊβ€˜π‘˜)) β€œ (1...𝑗)) Γ— {1}) βˆͺ (((2nd β€˜(πΊβ€˜π‘˜)) β€œ ((𝑗 + 1)...𝑁)) Γ— {0}))):(1...𝑁)⟢(0...π‘˜))
334331, 333sylibr 233 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (0...𝑁)) β†’ 𝑃:(1...𝑁)⟢(0...π‘˜))
335 vex 3479 . . . . . . . . . . . . . . . . . . . . 21 π‘˜ ∈ V
336335fconst 6774 . . . . . . . . . . . . . . . . . . . 20 ((1...𝑁) Γ— {π‘˜}):(1...𝑁)⟢{π‘˜}
337336a1i 11 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (0...𝑁)) β†’ ((1...𝑁) Γ— {π‘˜}):(1...𝑁)⟢{π‘˜})
338258, 334, 337, 329, 329, 330off 7683 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (0...𝑁)) β†’ (𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})):(1...𝑁)⟢(0[,]1))
339210eleq2i 2826 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})) ∈ 𝐼 ↔ (𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})) ∈ ((0[,]1) ↑m (1...𝑁)))
340 ovex 7437 . . . . . . . . . . . . . . . . . . . 20 (0[,]1) ∈ V
341 ovex 7437 . . . . . . . . . . . . . . . . . . . 20 (1...𝑁) ∈ V
342340, 341elmap 8861 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})) ∈ ((0[,]1) ↑m (1...𝑁)) ↔ (𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})):(1...𝑁)⟢(0[,]1))
343339, 342bitri 275 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})) ∈ 𝐼 ↔ (𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})):(1...𝑁)⟢(0[,]1))
344338, 343sylibr 233 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (0...𝑁)) β†’ (𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})) ∈ 𝐼)
345223, 344ffvelcdmd 7083 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (0...𝑁)) β†’ (πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜}))) ∈ (ℝ ↑m (1...𝑁)))
346 elmapi 8839 . . . . . . . . . . . . . . . 16 ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜}))) ∈ (ℝ ↑m (1...𝑁)) β†’ (πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜}))):(1...𝑁)βŸΆβ„)
347345, 346syl 17 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (0...𝑁)) β†’ (πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜}))):(1...𝑁)βŸΆβ„)
348347ffvelcdmda 7082 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ∈ ℝ)
349348an32s 651 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) β†’ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ∈ ℝ)
350 0red 11213 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) β†’ 0 ∈ ℝ)
351349, 350ltnled 11357 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) β†’ (((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) < 0 ↔ Β¬ 0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›)))
352 ltle 11298 . . . . . . . . . . . . 13 ((((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ∈ ℝ ∧ 0 ∈ ℝ) β†’ (((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) < 0 β†’ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ≀ 0))
353349, 37, 352sylancl 587 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) β†’ (((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) < 0 β†’ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ≀ 0))
354351, 353sylbird 260 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) β†’ (Β¬ 0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) β†’ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ≀ 0))
355244, 230div0d 11985 . . . . . . . . . . . . . . 15 (π‘˜ ∈ β„• β†’ (0 / π‘˜) = 0)
356 oveq1 7411 . . . . . . . . . . . . . . . 16 ((π‘ƒβ€˜π‘›) = 0 β†’ ((π‘ƒβ€˜π‘›) / π‘˜) = (0 / π‘˜))
357356eqeq1d 2735 . . . . . . . . . . . . . . 15 ((π‘ƒβ€˜π‘›) = 0 β†’ (((π‘ƒβ€˜π‘›) / π‘˜) = 0 ↔ (0 / π‘˜) = 0))
358355, 357syl5ibrcom 246 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„• β†’ ((π‘ƒβ€˜π‘›) = 0 β†’ ((π‘ƒβ€˜π‘›) / π‘˜) = 0))
359358ad3antlr 730 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) β†’ ((π‘ƒβ€˜π‘›) = 0 β†’ ((π‘ƒβ€˜π‘›) / π‘˜) = 0))
360334ffnd 6715 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (0...𝑁)) β†’ 𝑃 Fn (1...𝑁))
361 fnconstg 6776 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ V β†’ ((1...𝑁) Γ— {π‘˜}) Fn (1...𝑁))
362335, 361mp1i 13 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (0...𝑁)) β†’ ((1...𝑁) Γ— {π‘˜}) Fn (1...𝑁))
363 eqidd 2734 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘ƒβ€˜π‘›) = (π‘ƒβ€˜π‘›))
364335fvconst2 7200 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (1...𝑁) β†’ (((1...𝑁) Γ— {π‘˜})β€˜π‘›) = π‘˜)
365364adantl 483 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ (((1...𝑁) Γ— {π‘˜})β€˜π‘›) = π‘˜)
366360, 362, 329, 329, 330, 363, 365ofval 7676 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((𝑃 ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘›) = ((π‘ƒβ€˜π‘›) / π‘˜))
367366an32s 651 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) β†’ ((𝑃 ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘›) = ((π‘ƒβ€˜π‘›) / π‘˜))
368367eqeq1d 2735 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) β†’ (((𝑃 ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘›) = 0 ↔ ((π‘ƒβ€˜π‘›) / π‘˜) = 0))
369359, 368sylibrd 259 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) β†’ ((π‘ƒβ€˜π‘›) = 0 β†’ ((𝑃 ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘›) = 0))
370 simplll 774 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) β†’ πœ‘)
371 simplr 768 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) β†’ 𝑛 ∈ (1...𝑁))
372344adantlr 714 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) β†’ (𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})) ∈ 𝐼)
373 ovex 7437 . . . . . . . . . . . . . 14 (𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})) ∈ V
374 eleq1 2822 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})) β†’ (𝑧 ∈ 𝐼 ↔ (𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})) ∈ 𝐼))
375 fveq1 6887 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})) β†’ (π‘§β€˜π‘›) = ((𝑃 ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘›))
376375eqeq1d 2735 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})) β†’ ((π‘§β€˜π‘›) = 0 ↔ ((𝑃 ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘›) = 0))
377 fveq2 6888 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})) β†’ (πΉβ€˜π‘§) = (πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜}))))
378377fveq1d 6890 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})) β†’ ((πΉβ€˜π‘§)β€˜π‘›) = ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›))
379378breq1d 5157 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})) β†’ (((πΉβ€˜π‘§)β€˜π‘›) ≀ 0 ↔ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ≀ 0))
380376, 379imbi12d 345 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})) β†’ (((π‘§β€˜π‘›) = 0 β†’ ((πΉβ€˜π‘§)β€˜π‘›) ≀ 0) ↔ (((𝑃 ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘›) = 0 β†’ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ≀ 0)))
381374, 380imbi12d 345 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})) β†’ ((𝑧 ∈ 𝐼 β†’ ((π‘§β€˜π‘›) = 0 β†’ ((πΉβ€˜π‘§)β€˜π‘›) ≀ 0)) ↔ ((𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})) ∈ 𝐼 β†’ (((𝑃 ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘›) = 0 β†’ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ≀ 0))))
382381imbi2d 341 . . . . . . . . . . . . . . 15 (𝑧 = (𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})) β†’ ((𝑛 ∈ (1...𝑁) β†’ (𝑧 ∈ 𝐼 β†’ ((π‘§β€˜π‘›) = 0 β†’ ((πΉβ€˜π‘§)β€˜π‘›) ≀ 0))) ↔ (𝑛 ∈ (1...𝑁) β†’ ((𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})) ∈ 𝐼 β†’ (((𝑃 ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘›) = 0 β†’ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ≀ 0)))))
383382imbi2d 341 . . . . . . . . . . . . . 14 (𝑧 = (𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})) β†’ ((πœ‘ β†’ (𝑛 ∈ (1...𝑁) β†’ (𝑧 ∈ 𝐼 β†’ ((π‘§β€˜π‘›) = 0 β†’ ((πΉβ€˜π‘§)β€˜π‘›) ≀ 0)))) ↔ (πœ‘ β†’ (𝑛 ∈ (1...𝑁) β†’ ((𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})) ∈ 𝐼 β†’ (((𝑃 ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘›) = 0 β†’ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ≀ 0))))))
384 poimir.2 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (π‘§β€˜π‘›) = 0)) β†’ ((πΉβ€˜π‘§)β€˜π‘›) ≀ 0)
3853843exp2 1355 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑛 ∈ (1...𝑁) β†’ (𝑧 ∈ 𝐼 β†’ ((π‘§β€˜π‘›) = 0 β†’ ((πΉβ€˜π‘§)β€˜π‘›) ≀ 0))))
386373, 383, 385vtocl 3549 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑛 ∈ (1...𝑁) β†’ ((𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})) ∈ 𝐼 β†’ (((𝑃 ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘›) = 0 β†’ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ≀ 0))))
387370, 371, 372, 386syl3c 66 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) β†’ (((𝑃 ∘f / ((1...𝑁) Γ— {π‘˜}))β€˜π‘›) = 0 β†’ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ≀ 0))
388369, 387syld 47 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) β†’ ((π‘ƒβ€˜π‘›) = 0 β†’ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ≀ 0))
389354, 388jaod 858 . . . . . . . . . 10 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) β†’ ((Β¬ 0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ∨ (π‘ƒβ€˜π‘›) = 0) β†’ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ≀ 0))
390202, 389syld 47 . . . . . . . . 9 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) β†’ ((𝑛 βˆ’ 1) = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) β†’ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ≀ 0))
391390reximdva 3169 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ (1...𝑁)) β†’ (βˆƒπ‘— ∈ (0...𝑁)(𝑛 βˆ’ 1) = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) β†’ βˆƒπ‘— ∈ (0...𝑁)((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ≀ 0))
392391anasss 468 . . . . . . 7 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 𝑛 ∈ (1...𝑁))) β†’ (βˆƒπ‘— ∈ (0...𝑁)(𝑛 βˆ’ 1) = sup(({0} βˆͺ {π‘Ž ∈ (1...𝑁) ∣ βˆ€π‘ ∈ (1...π‘Ž)(0 ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘) ∧ (π‘ƒβ€˜π‘) β‰  0)}), ℝ, < ) β†’ βˆƒπ‘— ∈ (0...𝑁)((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ≀ 0))
393108, 392mpd 15 . . . . . 6 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 𝑛 ∈ (1...𝑁))) β†’ βˆƒπ‘— ∈ (0...𝑁)((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ≀ 0)
394 breq 5149 . . . . . . . 8 (π‘Ÿ = β—‘ ≀ β†’ (0π‘Ÿ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ↔ 0β—‘ ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›)))
395 fvex 6901 . . . . . . . . 9 ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ∈ V
39632, 395brcnv 5880 . . . . . . . 8 (0β—‘ ≀ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ↔ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ≀ 0)
397394, 396bitrdi 287 . . . . . . 7 (π‘Ÿ = β—‘ ≀ β†’ (0π‘Ÿ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ↔ ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ≀ 0))
398397rexbidv 3179 . . . . . 6 (π‘Ÿ = β—‘ ≀ β†’ (βˆƒπ‘— ∈ (0...𝑁)0π‘Ÿ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ↔ βˆƒπ‘— ∈ (0...𝑁)((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›) ≀ 0))
399393, 398syl5ibrcom 246 . . . . 5 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 𝑛 ∈ (1...𝑁))) β†’ (π‘Ÿ = β—‘ ≀ β†’ βˆƒπ‘— ∈ (0...𝑁)0π‘Ÿ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›)))
40076, 399jaod 858 . . . 4 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 𝑛 ∈ (1...𝑁))) β†’ ((π‘Ÿ = ≀ ∨ π‘Ÿ = β—‘ ≀ ) β†’ βˆƒπ‘— ∈ (0...𝑁)0π‘Ÿ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›)))
4011, 400syl5 34 . . 3 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 𝑛 ∈ (1...𝑁))) β†’ (π‘Ÿ ∈ { ≀ , β—‘ ≀ } β†’ βˆƒπ‘— ∈ (0...𝑁)0π‘Ÿ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›)))
402401exp32 422 . 2 (πœ‘ β†’ (π‘˜ ∈ β„• β†’ (𝑛 ∈ (1...𝑁) β†’ (π‘Ÿ ∈ { ≀ , β—‘ ≀ } β†’ βˆƒπ‘— ∈ (0...𝑁)0π‘Ÿ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›)))))
4034023imp2 1350 1 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 𝑛 ∈ (1...𝑁) ∧ π‘Ÿ ∈ { ≀ , β—‘ ≀ })) β†’ βˆƒπ‘— ∈ (0...𝑁)0π‘Ÿ((πΉβ€˜(𝑃 ∘f / ((1...𝑁) Γ— {π‘˜})))β€˜π‘›))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  {cab 2710   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  {crab 3433  Vcvv 3475   βˆͺ cun 3945   ∩ cin 3946   βŠ† wss 3947  βˆ…c0 4321  {csn 4627  {cpr 4629  βˆͺ cuni 4907   class class class wbr 5147   Or wor 5586   Γ— cxp 5673  β—‘ccnv 5674  ran crn 5676   β€œ cima 5678  Fun wfun 6534   Fn wfn 6535  βŸΆwf 6536  β€“ontoβ†’wfo 6538  β€“1-1-ontoβ†’wf1o 6539  β€˜cfv 6540  (class class class)co 7404   ∘f cof 7663  1st c1st 7968  2nd c2nd 7969   ↑m cmap 8816  Fincfn 8935  supcsup 9431  β„‚cc 11104  β„cr 11105  0cc0 11106  1c1 11107   + caddc 11109   Β· cmul 11111   < clt 11244   ≀ cle 11245   βˆ’ cmin 11440   / cdiv 11867  β„•cn 12208  β„•0cn0 12468  β„€cz 12554  β„€β‰₯cuz 12818  β„+crp 12970  (,)cioo 13320  [,]cicc 13323  ...cfz 13480  ..^cfzo 13623   β†Ύt crest 17362  topGenctg 17379  βˆtcpt 17380  Topctop 22377   Cn ccn 22710
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-of 7665  df-om 7851  df-1st 7970  df-2nd 7971  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-er 8699  df-map 8818  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fi 9402  df-sup 9433  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-n0 12469  df-z 12555  df-uz 12819  df-rp 12971  df-ioo 13324  df-icc 13327  df-fz 13481  df-fzo 13624  df-rest 17364  df-topgen 17385  df-pt 17386  df-top 22378  df-topon 22395  df-bases 22431  df-cn 22713
This theorem is referenced by:  poimirlem32  36458
  Copyright terms: Public domain W3C validator