poimirlem31 - Mathbox for Brendan Leahy

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

Theorem poimirlem31 33440

Description: Lemma for poimir 33442, assigning values to the vertices of the tessellation that meet the hypotheses of both poimirlem30 33439 and poimirlem28 33437. 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	⊢ 𝑃 = ((1^st ‘(𝐺‘𝑘)) ∘_𝑓 + ((((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
poimirlem31.3	⊢ (𝜑 → 𝐺:ℕ⟶((ℕ₀ ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
poimirlem31.4	⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran (1^st ‘(𝐺‘𝑘)) ⊆ (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.

Step	Hyp	Ref	Expression
1		elpri 4197	. . . 4 ⊢ (𝑟 ∈ { ≤ , ^◡ ≤ } → (𝑟 = ≤ ∨ 𝑟 = ^◡ ≤ ))
2		simprr 796	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → 𝑛 ∈ (1...𝑁))
3		1eluzge0 11732	. . . . . . . . . . 11 ⊢ 1 ∈ (ℤ_≥‘0)
4		fzss1 12380	. . . . . . . . . . 11 ⊢ (1 ∈ (ℤ_≥‘0) → (1...𝑁) ⊆ (0...𝑁))
5	3, 4	ax-mp 5	. . . . . . . . . 10 ⊢ (1...𝑁) ⊆ (0...𝑁)
6	5	sseli 3599	. . . . . . . . 9 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ (0...𝑁))
7	6	anim2i 593	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (𝑘 ∈ ℕ ∧ 𝑛 ∈ (0...𝑁)))
8		eleq1 2689	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑛 → (𝑖 ∈ (0...𝑁) ↔ 𝑛 ∈ (0...𝑁)))
9	8	anbi2d 740	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑛 → ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑁)) ↔ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (0...𝑁))))
10	9	anbi2d 740	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑛 → ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑁))) ↔ (𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (0...𝑁)))))
11		eqeq1 2626	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑛 → (𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) ↔ 𝑛 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < )))
12	11	rexbidv 3052	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑛 → (∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) ↔ ∃𝑗 ∈ (0...𝑁)𝑛 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < )))
13	10, 12	imbi12d 334	. . . . . . . . . 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)}), ℝ, < ))
15	13, 14	chvarv 2263	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (0...𝑁))) → ∃𝑗 ∈ (0...𝑁)𝑛 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ))
16		elfzle1 12344	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...𝑁) → 1 ≤ 𝑛)
17		1re 10039	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ
18		elfzelz 12342	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℤ)
19	18	zred 11482	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℝ)
20		lenlt 10116	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (1 ≤ 𝑛 ↔ ¬ 𝑛 < 1))
21	17, 19, 20	sylancr 695	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...𝑁) → (1 ≤ 𝑛 ↔ ¬ 𝑛 < 1))
22	16, 21	mpbid 222	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...𝑁) → ¬ 𝑛 < 1)
23		elsni 4194	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ {0} → 𝑛 = 0)
24		0lt1 10550	. . . . . . . . . . . . 13 ⊢ 0 < 1
25	23, 24	syl6eqbr 4692	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ {0} → 𝑛 < 1)
26	22, 25	nsyl 135	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...𝑁) → ¬ 𝑛 ∈ {0})
27		ltso 10118	. . . . . . . . . . . . . . 15 ⊢ < Or ℝ
28		snfi 8038	. . . . . . . . . . . . . . . . 17 ⊢ {0} ∈ Fin
29		fzfi 12771	. . . . . . . . . . . . . . . . . 18 ⊢ (1...𝑁) ∈ Fin
30		rabfi 8185	. . . . . . . . . . . . . . . . . 18 ⊢ ((1...𝑁) ∈ Fin → {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)} ∈ Fin)
31	29, 30	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)} ∈ Fin
32		unfi 8227	. . . . . . . . . . . . . . . . 17 ⊢ (({0} ∈ Fin ∧ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)} ∈ Fin) → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ∈ Fin)
33	28, 31, 32	mp2an 708	. . . . . . . . . . . . . . . 16 ⊢ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ∈ Fin
34		c0ex 10034	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ V
35	34	snid 4208	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ {0}
36		elun1 3780	. . . . . . . . . . . . . . . . 17 ⊢ (0 ∈ {0} → 0 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}))
37		ne0i 3921	. . . . . . . . . . . . . . . . 17 ⊢ (0 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ≠ ∅)
38	35, 36, 37	mp2b 10	. . . . . . . . . . . . . . . 16 ⊢ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ≠ ∅
39		0re 10040	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℝ
40		snssi 4339	. . . . . . . . . . . . . . . . . 18 ⊢ (0 ∈ ℝ → {0} ⊆ ℝ)
41	39, 40	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ {0} ⊆ ℝ
42		ssrab2 3687	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)} ⊆ (1...𝑁)
43	18	ssriv 3607	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...𝑁) ⊆ ℤ
44		zssre 11384	. . . . . . . . . . . . . . . . . . 19 ⊢ ℤ ⊆ ℝ
45	43, 44	sstri 3612	. . . . . . . . . . . . . . . . . 18 ⊢ (1...𝑁) ⊆ ℝ
46	42, 45	sstri 3612	. . . . . . . . . . . . . . . . 17 ⊢ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)} ⊆ ℝ
47	41, 46	unssi 3788	. . . . . . . . . . . . . . . 16 ⊢ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ⊆ ℝ
48	33, 38, 47	3pm3.2i 1239	. . . . . . . . . . . . . . 15 ⊢ (({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ∈ Fin ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ≠ ∅ ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ⊆ ℝ)
49		fisupcl 8375	. . . . . . . . . . . . . . 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)}))
50	27, 48, 49	mp2an 708	. . . . . . . . . . . . . 14 ⊢ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)})
51		eleq1 2689	. . . . . . . . . . . . . 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)})))
52	50, 51	mpbiri 248	. . . . . . . . . . . . 13 ⊢ (𝑛 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → 𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}))
53		elun 3753	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ↔ (𝑛 ∈ {0} ∨ 𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}))
54	52, 53	sylib 208	. . . . . . . . . . . 12 ⊢ (𝑛 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → (𝑛 ∈ {0} ∨ 𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}))
55		oveq2 6658	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑛 → (1...𝑎) = (1...𝑛))
56	55	raleqdv 3144	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑛 → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
57	56	elrab 3363	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)} ↔ (𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
58		elfzuz 12338	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ (ℤ_≥‘1))
59		eluzfz2 12349	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (ℤ_≥‘1) → 𝑛 ∈ (1...𝑛))
60	58, 59	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ (1...𝑛))
61		simpl 473	. . . . . . . . . . . . . . . 16 ⊢ ((0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) → 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏))
62	61	ralimi 2952	. . . . . . . . . . . . . . 15 ⊢ (∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏))
63		fveq2 6191	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑛 → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) = ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))
64	63	breq2d 4665	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑛 → (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ↔ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
65	64	rspcva 3307	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (1...𝑛) ∧ ∀𝑏 ∈ (1...𝑛)0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏)) → 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))
66	60, 62, 65	syl2an 494	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) → 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))
67	57, 66	sylbi 207	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)} → 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))
68	67	orim2i 540	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ {0} ∨ 𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) → (𝑛 ∈ {0} ∨ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
69	54, 68	syl 17	. . . . . . . . . . 11 ⊢ (𝑛 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → (𝑛 ∈ {0} ∨ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
70		orel1 397	. . . . . . . . . . 11 ⊢ (¬ 𝑛 ∈ {0} → ((𝑛 ∈ {0} ∨ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)) → 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
71	26, 69, 70	syl2im 40	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...𝑁) → (𝑛 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
72	71	reximdv 3016	. . . . . . . . 9 ⊢ (𝑛 ∈ (1...𝑁) → (∃𝑗 ∈ (0...𝑁)𝑛 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → ∃𝑗 ∈ (0...𝑁)0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
73	15, 72	syl5 34	. . . . . . . 8 ⊢ (𝑛 ∈ (1...𝑁) → ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (0...𝑁))) → ∃𝑗 ∈ (0...𝑁)0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
74	7, 73	sylan2i 687	. . . . . . 7 ⊢ (𝑛 ∈ (1...𝑁) → ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → ∃𝑗 ∈ (0...𝑁)0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
75	2, 74	mpcom 38	. . . . . 6 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → ∃𝑗 ∈ (0...𝑁)0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))
76		breq 4655	. . . . . . 7 ⊢ (𝑟 = ≤ → (0𝑟((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ↔ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
77	76	rexbidv 3052	. . . . . 6 ⊢ (𝑟 = ≤ → (∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ↔ ∃𝑗 ∈ (0...𝑁)0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
78	75, 77	syl5ibrcom 237	. . . . 5 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → (𝑟 = ≤ → ∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
79		poimir.0	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℕ)
80	79	nnzd 11481	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℤ)
81		elfzm1b 12418	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑛 ∈ (1...𝑁) ↔ (𝑛 − 1) ∈ (0...(𝑁 − 1))))
82	18, 80, 81	syl2anr 495	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 ∈ (1...𝑁) ↔ (𝑛 − 1) ∈ (0...(𝑁 − 1))))
83	82	biimpd 219	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 ∈ (1...𝑁) → (𝑛 − 1) ∈ (0...(𝑁 − 1))))
84	83	ex 450	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑛 ∈ (1...𝑁) → (𝑛 ∈ (1...𝑁) → (𝑛 − 1) ∈ (0...(𝑁 − 1)))))
85	84	pm2.43d 53	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑛 ∈ (1...𝑁) → (𝑛 − 1) ∈ (0...(𝑁 − 1))))
86	79	nncnd 11036	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℂ)
87		npcan1 10455	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
88	86, 87	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
89		nnm1nn0 11334	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
90	79, 89	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ₀)
91	90	nn0zd 11480	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
92		uzid 11702	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)))
93		peano2uz 11741	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
94	91, 92, 93	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
95	88, 94	eqeltrrd 2702	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑁 − 1)))
96		fzss2 12381	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑁 − 1)) → (0...(𝑁 − 1)) ⊆ (0...𝑁))
97	95, 96	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (0...(𝑁 − 1)) ⊆ (0...𝑁))
98	97	sseld 3602	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑛 − 1) ∈ (0...(𝑁 − 1)) → (𝑛 − 1) ∈ (0...𝑁)))
99	85, 98	syld 47	. . . . . . . . . 10 ⊢ (𝜑 → (𝑛 ∈ (1...𝑁) → (𝑛 − 1) ∈ (0...𝑁)))
100	99	anim2d 589	. . . . . . . . 9 ⊢ (𝜑 → ((𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (𝑘 ∈ ℕ ∧ (𝑛 − 1) ∈ (0...𝑁))))
101	100	imp 445	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → (𝑘 ∈ ℕ ∧ (𝑛 − 1) ∈ (0...𝑁)))
102		ovex 6678	. . . . . . . . 9 ⊢ (𝑛 − 1) ∈ V
103		eleq1 2689	. . . . . . . . . . . 12 ⊢ (𝑖 = (𝑛 − 1) → (𝑖 ∈ (0...𝑁) ↔ (𝑛 − 1) ∈ (0...𝑁)))
104	103	anbi2d 740	. . . . . . . . . . 11 ⊢ (𝑖 = (𝑛 − 1) → ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑁)) ↔ (𝑘 ∈ ℕ ∧ (𝑛 − 1) ∈ (0...𝑁))))
105	104	anbi2d 740	. . . . . . . . . 10 ⊢ (𝑖 = (𝑛 − 1) → ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑁))) ↔ (𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑛 − 1) ∈ (0...𝑁)))))
106		eqeq1 2626	. . . . . . . . . . 11 ⊢ (𝑖 = (𝑛 − 1) → (𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) ↔ (𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < )))
107	106	rexbidv 3052	. . . . . . . . . 10 ⊢ (𝑖 = (𝑛 − 1) → (∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) ↔ ∃𝑗 ∈ (0...𝑁)(𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < )))
108	105, 107	imbi12d 334	. . . . . . . . 9 ⊢ (𝑖 = (𝑛 − 1) → (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑁))) → ∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < )) ↔ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑛 − 1) ∈ (0...𝑁))) → ∃𝑗 ∈ (0...𝑁)(𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ))))
109	102, 108, 14	vtocl 3259	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑛 − 1) ∈ (0...𝑁))) → ∃𝑗 ∈ (0...𝑁)(𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ))
110	101, 109	syldan 487	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → ∃𝑗 ∈ (0...𝑁)(𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ))
111		eleq1 2689	. . . . . . . . . . . . . . . 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)})))
112	50, 111	mpbiri 248	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → (𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}))
113		elun 3753	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ↔ ((𝑛 − 1) ∈ {0} ∨ (𝑛 − 1) ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}))
114	102	elsn 4192	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 − 1) ∈ {0} ↔ (𝑛 − 1) = 0)
115		oveq2 6658	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (𝑛 − 1) → (1...𝑎) = (1...(𝑛 − 1)))
116	115	raleqdv 3144	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑛 − 1) → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
117	116	elrab 3363	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 − 1) ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)} ↔ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
118	114, 117	orbi12i 543	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 − 1) ∈ {0} ∨ (𝑛 − 1) ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ↔ ((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0))))
119	113, 118	bitri 264	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ↔ ((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0))))
120	112, 119	sylib 208	. . . . . . . . . . . . . 14 ⊢ ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → ((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0))))
121	120	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → ((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))))
122		ltm1 10863	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℝ → (𝑛 − 1) < 𝑛)
123		peano2rem 10348	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
124		ltnle 10117	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 − 1) ∈ ℝ ∧ 𝑛 ∈ ℝ) → ((𝑛 − 1) < 𝑛 ↔ ¬ 𝑛 ≤ (𝑛 − 1)))
125	123, 124	mpancom 703	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℝ → ((𝑛 − 1) < 𝑛 ↔ ¬ 𝑛 ≤ (𝑛 − 1)))
126	122, 125	mpbid 222	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℝ → ¬ 𝑛 ≤ (𝑛 − 1))
127	19, 126	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (1...𝑁) → ¬ 𝑛 ≤ (𝑛 − 1))
128		breq2 4657	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → (𝑛 ≤ (𝑛 − 1) ↔ 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < )))
129	128	notbid 308	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → (¬ 𝑛 ≤ (𝑛 − 1) ↔ ¬ 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < )))
130	127, 129	syl5ibcom 235	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → ¬ 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < )))
131		elun2 3781	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)} → 𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}))
132		fimaxre2 10969	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ⊆ ℝ ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)})𝑦 ≤ 𝑥)
133	47, 33, 132	mp2an 708	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)})𝑦 ≤ 𝑥
134	47, 38, 133	3pm3.2i 1239	. . . . . . . . . . . . . . . . . . 19 ⊢ (({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ⊆ ℝ ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)})𝑦 ≤ 𝑥)
135	134	suprubii 10998	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) → 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ))
136	131, 135	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)} → 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ))
137	136	con3i 150	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → ¬ 𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)})
138		ianor 509	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) ↔ (¬ 𝑛 ∈ (1...𝑁) ∨ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
139	138, 57	xchnxbir 323	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)} ↔ (¬ 𝑛 ∈ (1...𝑁) ∨ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
140	137, 139	sylib 208	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → (¬ 𝑛 ∈ (1...𝑁) ∨ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
141	130, 140	syl6 35	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → (¬ 𝑛 ∈ (1...𝑁) ∨ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0))))
142		pm2.63 829	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (1...𝑁) ∨ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) → ((¬ 𝑛 ∈ (1...𝑁) ∨ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) → ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
143	142	orcs 409	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (1...𝑁) → ((¬ 𝑛 ∈ (1...𝑁) ∨ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) → ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
144	141, 143	syld 47	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
145	121, 144	jcad 555	. . . . . . . . . . . 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 912	. . . . . . . . . . . . . 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 11133	. . . . . . . . . . . . . . . . . 18 ⊢ (1 + 0) = 1
148	18	zcnd 11483	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ)
149		ax-1cn 9994	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℂ
150		0cn 10032	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ ℂ
151		subadd 10284	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ ∧ 0 ∈ ℂ) → ((𝑛 − 1) = 0 ↔ (1 + 0) = 𝑛))
152	149, 150, 151	mp3an23 1416	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℂ → ((𝑛 − 1) = 0 ↔ (1 + 0) = 𝑛))
153	148, 152	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) = 0 ↔ (1 + 0) = 𝑛))
154	153	biimpa 501	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (1...𝑁) ∧ (𝑛 − 1) = 0) → (1 + 0) = 𝑛)
155	147, 154	syl5reqr 2671	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (1...𝑁) ∧ (𝑛 − 1) = 0) → 𝑛 = 1)
156		1z 11407	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℤ
157		fzsn 12383	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 ∈ ℤ → (1...1) = {1})
158	156, 157	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1...1) = {1}
159		oveq2 6658	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 1 → (1...𝑛) = (1...1))
160		sneq 4187	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 1 → {𝑛} = {1})
161	158, 159, 160	3eqtr4a 2682	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 1 → (1...𝑛) = {𝑛})
162	161	raleqdv 3144	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 1 → (∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) ↔ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
163	162	notbid 308	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 1 → (¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) ↔ ¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
164	163	biimpd 219	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 1 → (¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) → ¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
165	155, 164	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ (1...𝑁) ∧ (𝑛 − 1) = 0) → (¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) → ¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
166	165	expimpd 629	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (1...𝑁) → (((𝑛 − 1) = 0 ∧ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) → ¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
167		ralun 3795	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) → ∀𝑏 ∈ ((1...(𝑛 − 1)) ∪ {𝑛})(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0))
168		npcan1 10455	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ ℂ → ((𝑛 − 1) + 1) = 𝑛)
169	148, 168	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) + 1) = 𝑛)
170	169, 58	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) + 1) ∈ (ℤ_≥‘1))
171		peano2zm 11420	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ ℤ → (𝑛 − 1) ∈ ℤ)
172		uzid 11702	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 − 1) ∈ ℤ → (𝑛 − 1) ∈ (ℤ_≥‘(𝑛 − 1)))
173		peano2uz 11741	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 − 1) ∈ (ℤ_≥‘(𝑛 − 1)) → ((𝑛 − 1) + 1) ∈ (ℤ_≥‘(𝑛 − 1)))
174	18, 171, 172, 173	4syl 19	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) + 1) ∈ (ℤ_≥‘(𝑛 − 1)))
175	169, 174	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ (ℤ_≥‘(𝑛 − 1)))
176		fzsplit2 12366	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑛 − 1) + 1) ∈ (ℤ_≥‘1) ∧ 𝑛 ∈ (ℤ_≥‘(𝑛 − 1))) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)))
177	170, 175, 176	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ (1...𝑁) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)))
178	169	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ (1...𝑁) → (((𝑛 − 1) + 1)...𝑛) = (𝑛...𝑛))
179		fzsn 12383	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ ℤ → (𝑛...𝑛) = {𝑛})
180	18, 179	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ (1...𝑁) → (𝑛...𝑛) = {𝑛})
181	178, 180	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ (1...𝑁) → (((𝑛 − 1) + 1)...𝑛) = {𝑛})
182	181	uneq2d 3767	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ (1...𝑁) → ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)) = ((1...(𝑛 − 1)) ∪ {𝑛}))
183	177, 182	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ (1...𝑁) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ {𝑛}))
184	183	raleqdv 3144	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) ↔ ∀𝑏 ∈ ((1...(𝑛 − 1)) ∪ {𝑛})(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
185	167, 184	syl5ibr 236	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (1...𝑁) → ((∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
186	185	expdimp 453	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
187	186	con3d 148	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) → (¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) → ¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
188	187	adantrl 752	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ (1...𝑁) ∧ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0))) → (¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) → ¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
189	188	expimpd 629	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (1...𝑁) → ((((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) ∧ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) → ¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
190	166, 189	jaod 395	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (1...𝑁) → ((((𝑛 − 1) = 0 ∧ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) ∨ (((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) ∧ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0))) → ¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
191	146, 190	syl5bi 232	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...𝑁) → ((((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0))) ∧ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) → ¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
192		fveq2 6191	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑛 → (𝑃‘𝑏) = (𝑃‘𝑛))
193	192	neeq1d 2853	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑛 → ((𝑃‘𝑏) ≠ 0 ↔ (𝑃‘𝑛) ≠ 0))
194	64, 193	anbi12d 747	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑛 → ((0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∧ (𝑃‘𝑛) ≠ 0)))
195	194	ralsng 4218	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∧ (𝑃‘𝑛) ≠ 0)))
196	195	notbid 308	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (1...𝑁) → (¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) ↔ ¬ (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∧ (𝑃‘𝑛) ≠ 0)))
197		ianor 509	. . . . . . . . . . . . . . 15 ⊢ (¬ (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∧ (𝑃‘𝑛) ≠ 0) ↔ (¬ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∨ ¬ (𝑃‘𝑛) ≠ 0))
198		nne 2798	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑃‘𝑛) ≠ 0 ↔ (𝑃‘𝑛) = 0)
199	198	orbi2i 541	. . . . . . . . . . . . . . 15 ⊢ ((¬ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∨ ¬ (𝑃‘𝑛) ≠ 0) ↔ (¬ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∨ (𝑃‘𝑛) = 0))
200	197, 199	bitri 264	. . . . . . . . . . . . . 14 ⊢ (¬ (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∧ (𝑃‘𝑛) ≠ 0) ↔ (¬ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∨ (𝑃‘𝑛) = 0))
201	196, 200	syl6bb 276	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...𝑁) → (¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) ↔ (¬ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∨ (𝑃‘𝑛) = 0)))
202	191, 201	sylibd 229	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...𝑁) → ((((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0))) ∧ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) → (¬ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∨ (𝑃‘𝑛) = 0)))
203	145, 202	syld 47	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → (¬ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∨ (𝑃‘𝑛) = 0)))
204	203	ad2antlr 763	. . . . . . . . . 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 22565	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (topGen‘ran (,)) ∈ Top
208	207	fconst6 6095	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top
209		pttop 21385	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1...𝑁) ∈ Fin ∧ ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top) → (∏_t‘((1...𝑁) × {(topGen‘ran (,))})) ∈ Top)
210	29, 208, 209	mp2an 708	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∏_t‘((1...𝑁) × {(topGen‘ran (,))})) ∈ Top
211	206, 210	eqeltri 2697	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑅 ∈ Top
212		poimir.i	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐼 = ((0[,]1) ↑_𝑚 (1...𝑁))
213		reex 10027	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℝ ∈ V
214		unitssre 12319	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0[,]1) ⊆ ℝ
215		mapss 7900	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℝ ∈ V ∧ (0[,]1) ⊆ ℝ) → ((0[,]1) ↑_𝑚 (1...𝑁)) ⊆ (ℝ ↑_𝑚 (1...𝑁)))
216	213, 214, 215	mp2an 708	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0[,]1) ↑_𝑚 (1...𝑁)) ⊆ (ℝ ↑_𝑚 (1...𝑁))
217	212, 216	eqsstri 3635	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐼 ⊆ (ℝ ↑_𝑚 (1...𝑁))
218		uniretop 22566	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℝ = ∪ (topGen‘ran (,))
219	206, 218	ptuniconst 21401	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1...𝑁) ∈ Fin ∧ (topGen‘ran (,)) ∈ Top) → (ℝ ↑_𝑚 (1...𝑁)) = ∪ 𝑅)
220	29, 207, 219	mp2an 708	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℝ ↑_𝑚 (1...𝑁)) = ∪ 𝑅
221	220	restuni 20966	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Top ∧ 𝐼 ⊆ (ℝ ↑_𝑚 (1...𝑁))) → 𝐼 = ∪ (𝑅 ↾_t 𝐼))
222	211, 217, 221	mp2an 708	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐼 = ∪ (𝑅 ↾_t 𝐼)
223	222, 220	cnf 21050	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ ((𝑅 ↾_t 𝐼) Cn 𝑅) → 𝐹:𝐼⟶(ℝ ↑_𝑚 (1...𝑁)))
224	205, 223	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹:𝐼⟶(ℝ ↑_𝑚 (1...𝑁)))
225	224	ad2antrr 762	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝐹:𝐼⟶(ℝ ↑_𝑚 (1...𝑁)))
226		simplr 792	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝑘 ∈ ℕ)
227		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ (0...𝑘) → 𝑥 ∈ ℤ)
228	227	zred 11482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ (0...𝑘) → 𝑥 ∈ ℝ)
229	228	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑥 ∈ ℝ)
230		nnre 11027	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
231	230	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ)
232		nnne0 11053	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 ∈ ℕ → 𝑘 ≠ 0)
233	232	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ≠ 0)
234	229, 231, 233	redivcld 10853	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑥 / 𝑘) ∈ ℝ)
235		elfzle1 12344	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ (0...𝑘) → 0 ≤ 𝑥)
236	228, 235	jca 554	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ (0...𝑘) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
237		nnrp 11842	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ⁺)
238	237	rpregt0d 11878	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 < 𝑘))
239		divge0 10892	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → 0 ≤ (𝑥 / 𝑘))
240	236, 238, 239	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝑥 / 𝑘))
241		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ (0...𝑘) → 𝑥 ≤ 𝑘)
242	241	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑥 ≤ 𝑘)
243		1red 10055	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
244	237	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ⁺)
245	229, 243, 244	ledivmuld 11925	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑥 / 𝑘) ≤ 1 ↔ 𝑥 ≤ (𝑘 · 1)))
246		nncn 11028	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
247	246	mulid1d 10057	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 ∈ ℕ → (𝑘 · 1) = 𝑘)
248	247	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ∈ ℕ → (𝑥 ≤ (𝑘 · 1) ↔ 𝑥 ≤ 𝑘))
249	248	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑥 ≤ (𝑘 · 1) ↔ 𝑥 ≤ 𝑘))
250	245, 249	bitrd 268	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑥 / 𝑘) ≤ 1 ↔ 𝑥 ≤ 𝑘))
251	242, 250	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑥 / 𝑘) ≤ 1)
252	39, 17	elicc2i 12239	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 / 𝑘) ∈ (0[,]1) ↔ ((𝑥 / 𝑘) ∈ ℝ ∧ 0 ≤ (𝑥 / 𝑘) ∧ (𝑥 / 𝑘) ≤ 1))
253	234, 240, 251, 252	syl3anbrc 1246	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑥 / 𝑘) ∈ (0[,]1))
254	253	ancoms 469	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ (0...𝑘)) → (𝑥 / 𝑘) ∈ (0[,]1))
255		elsni 4194	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ {𝑘} → 𝑦 = 𝑘)
256	255	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ {𝑘} → (𝑥 / 𝑦) = (𝑥 / 𝑘))
257	256	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ {𝑘} → ((𝑥 / 𝑦) ∈ (0[,]1) ↔ (𝑥 / 𝑘) ∈ (0[,]1)))
258	254, 257	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ (0...𝑘)) → (𝑦 ∈ {𝑘} → (𝑥 / 𝑦) ∈ (0[,]1)))
259	258	impr 649	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ ∧ (𝑥 ∈ (0...𝑘) ∧ 𝑦 ∈ {𝑘})) → (𝑥 / 𝑦) ∈ (0[,]1))
260	226, 259	sylan 488	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ (0...𝑘) ∧ 𝑦 ∈ {𝑘})) → (𝑥 / 𝑦) ∈ (0[,]1))
261		elun 3753	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ ({1} ∪ {0}) ↔ (𝑦 ∈ {1} ∨ 𝑦 ∈ {0}))
262		fzofzp1 12565	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ (0..^𝑘) → (𝑥 + 1) ∈ (0...𝑘))
263		elsni 4194	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 ∈ {1} → 𝑦 = 1)
264	263	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ {1} → (𝑥 + 𝑦) = (𝑥 + 1))
265	264	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ {1} → ((𝑥 + 𝑦) ∈ (0...𝑘) ↔ (𝑥 + 1) ∈ (0...𝑘)))
266	262, 265	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ (0..^𝑘) → (𝑦 ∈ {1} → (𝑥 + 𝑦) ∈ (0...𝑘)))
267		elfzonn0 12512	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 ∈ (0..^𝑘) → 𝑥 ∈ ℕ₀)
268	267	nn0cnd 11353	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∈ (0..^𝑘) → 𝑥 ∈ ℂ)
269	268	addid1d 10236	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ (0..^𝑘) → (𝑥 + 0) = 𝑥)
270		elfzofz 12485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ (0..^𝑘) → 𝑥 ∈ (0...𝑘))
271	269, 270	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ (0..^𝑘) → (𝑥 + 0) ∈ (0...𝑘))
272		elsni 4194	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 ∈ {0} → 𝑦 = 0)
273	272	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ {0} → (𝑥 + 𝑦) = (𝑥 + 0))
274	273	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ {0} → ((𝑥 + 𝑦) ∈ (0...𝑘) ↔ (𝑥 + 0) ∈ (0...𝑘)))
275	271, 274	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ (0..^𝑘) → (𝑦 ∈ {0} → (𝑥 + 𝑦) ∈ (0...𝑘)))
276	266, 275	jaod 395	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ (0..^𝑘) → ((𝑦 ∈ {1} ∨ 𝑦 ∈ {0}) → (𝑥 + 𝑦) ∈ (0...𝑘)))
277	261, 276	syl5bi 232	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ (0..^𝑘) → (𝑦 ∈ ({1} ∪ {0}) → (𝑥 + 𝑦) ∈ (0...𝑘)))
278	277	imp 445	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ (0..^𝑘) ∧ 𝑦 ∈ ({1} ∪ {0})) → (𝑥 + 𝑦) ∈ (0...𝑘))
279	278	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ (0..^𝑘) ∧ 𝑦 ∈ ({1} ∪ {0}))) → (𝑥 + 𝑦) ∈ (0...𝑘))
280		poimirlem31.3	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐺:ℕ⟶((ℕ₀ ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
281	280	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ((ℕ₀ ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
282		xp1st 7198	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺‘𝑘) ∈ ((ℕ₀ ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^st ‘(𝐺‘𝑘)) ∈ (ℕ₀ ↑_𝑚 (1...𝑁)))
283		elmapfn 7880	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1^st ‘(𝐺‘𝑘)) ∈ (ℕ₀ ↑_𝑚 (1...𝑁)) → (1^st ‘(𝐺‘𝑘)) Fn (1...𝑁))
284	281, 282, 283	3syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1^st ‘(𝐺‘𝑘)) Fn (1...𝑁))
285		poimirlem31.4	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran (1^st ‘(𝐺‘𝑘)) ⊆ (0..^𝑘))
286		df-f 5892	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1^st ‘(𝐺‘𝑘)):(1...𝑁)⟶(0..^𝑘) ↔ ((1^st ‘(𝐺‘𝑘)) Fn (1...𝑁) ∧ ran (1^st ‘(𝐺‘𝑘)) ⊆ (0..^𝑘)))
287	284, 285, 286	sylanbrc 698	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1^st ‘(𝐺‘𝑘)):(1...𝑁)⟶(0..^𝑘))
288	287	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (1^st ‘(𝐺‘𝑘)):(1...𝑁)⟶(0..^𝑘))
289		1ex 10035	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 ∈ V
290	289	fconst 6091	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}):((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗))⟶{1}
291	34	fconst 6091	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}):((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁))⟶{0}
292	290, 291	pm3.2i 471	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}):((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗))⟶{1} ∧ (((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}):((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁))⟶{0})
293		xp2nd 7199	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐺‘𝑘) ∈ ((ℕ₀ ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2^nd ‘(𝐺‘𝑘)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
294	281, 293	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2^nd ‘(𝐺‘𝑘)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
295		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (2^nd ‘(𝐺‘𝑘)) ∈ V
296		f1oeq1 6127	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = (2^nd ‘(𝐺‘𝑘)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(𝐺‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁)))
297	295, 296	elab 3350	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((2^nd ‘(𝐺‘𝑘)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(𝐺‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁))
298	294, 297	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2^nd ‘(𝐺‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁))
299		dff1o3 6143	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((2^nd ‘(𝐺‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2^nd ‘(𝐺‘𝑘)):(1...𝑁)–onto→(1...𝑁) ∧ Fun ^◡(2^nd ‘(𝐺‘𝑘))))
300	299	simprbi 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((2^nd ‘(𝐺‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ^◡(2^nd ‘(𝐺‘𝑘)))
301		imain 5974	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Fun ^◡(2^nd ‘(𝐺‘𝑘)) → ((2^nd ‘(𝐺‘𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) ∩ ((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁))))
302	298, 300, 301	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2^nd ‘(𝐺‘𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) ∩ ((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁))))
303		elfznn0 12433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ₀)
304	303	nn0red 11352	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
305	304	ltp1d 10954	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1))
306		fzdisj 12368	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
307	305, 306	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
308	307	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 ∈ (0...𝑁) → ((2^nd ‘(𝐺‘𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((2^nd ‘(𝐺‘𝑘)) “ ∅))
309		ima0 5481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((2^nd ‘(𝐺‘𝑘)) “ ∅) = ∅
310	308, 309	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ (0...𝑁) → ((2^nd ‘(𝐺‘𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
311	302, 310	sylan9req 2677	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) ∩ ((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁))) = ∅)
312		fun 6066	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}):((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗))⟶{1} ∧ (((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}):((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁))⟶{0}) ∧ (((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) ∩ ((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁))) = ∅) → ((((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) ∪ ((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
313	292, 311, 312	sylancr 695	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) ∪ ((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
314		imaundi 5545	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((2^nd ‘(𝐺‘𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) ∪ ((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)))
315		nn0p1nn 11332	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑗 ∈ ℕ₀ → (𝑗 + 1) ∈ ℕ)
316	303, 315	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ)
317		nnuz 11723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ℕ = (ℤ_≥‘1)
318	316, 317	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (ℤ_≥‘1))
319		elfzuz3 12339	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ_≥‘𝑗))
320		fzsplit2 12366	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑗 + 1) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ (ℤ_≥‘𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
321	318, 319, 320	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
322	321	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ (0...𝑁) → ((2^nd ‘(𝐺‘𝑘)) “ (1...𝑁)) = ((2^nd ‘(𝐺‘𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))))
323		f1ofo 6144	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((2^nd ‘(𝐺‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(𝐺‘𝑘)):(1...𝑁)–onto→(1...𝑁))
324		foima 6120	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((2^nd ‘(𝐺‘𝑘)):(1...𝑁)–onto→(1...𝑁) → ((2^nd ‘(𝐺‘𝑘)) “ (1...𝑁)) = (1...𝑁))
325	298, 323, 324	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2^nd ‘(𝐺‘𝑘)) “ (1...𝑁)) = (1...𝑁))
326	322, 325	sylan9req 2677	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑗 ∈ (0...𝑁) ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → ((2^nd ‘(𝐺‘𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (1...𝑁))
327	326	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((2^nd ‘(𝐺‘𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (1...𝑁))
328	314, 327	syl5eqr 2670	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) ∪ ((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁))) = (1...𝑁))
329	328	feq2d 6031	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) ∪ ((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}) ↔ ((((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0})))
330	313, 329	mpbid 222	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
331		fzfid 12772	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin)
332		inidm 3822	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
333	279, 288, 330, 331, 331, 332	off 6912	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1^st ‘(𝐺‘𝑘)) ∘_𝑓 + ((((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝑘))
334		poimirlem31.p	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑃 = ((1^st ‘(𝐺‘𝑘)) ∘_𝑓 + ((((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
335	334	feq1i 6036	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃:(1...𝑁)⟶(0...𝑘) ↔ ((1^st ‘(𝐺‘𝑘)) ∘_𝑓 + ((((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝑘))
336	333, 335	sylibr 224	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝑃:(1...𝑁)⟶(0...𝑘))
337		vex 3203	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑘 ∈ V
338	337	fconst 6091	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘}
339	338	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘})
340	260, 336, 339, 331, 331, 332	off 6912	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
341	212	eleq2i 2693	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑_𝑚 (1...𝑁)))
342		ovex 6678	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0[,]1) ∈ V
343		ovex 6678	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...𝑁) ∈ V
344	342, 343	elmap 7886	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑_𝑚 (1...𝑁)) ↔ (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
345	341, 344	bitri 264	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
346	340, 345	sylibr 224	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼)
347	225, 346	ffvelrnd 6360	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))) ∈ (ℝ ↑_𝑚 (1...𝑁)))
348		elmapi 7879	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))) ∈ (ℝ ↑_𝑚 (1...𝑁)) → (𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))):(1...𝑁)⟶ℝ)
349	347, 348	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))):(1...𝑁)⟶ℝ)
350	349	ffvelrnda 6359	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∈ ℝ)
351	350	an32s 846	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∈ ℝ)
352		0red 10041	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → 0 ∈ ℝ)
353	351, 352	ltnled 10184	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → (((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) < 0 ↔ ¬ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
354		ltle 10126	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∈ ℝ ∧ 0 ∈ ℝ) → (((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) < 0 → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
355	351, 39, 354	sylancl 694	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → (((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) < 0 → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
356	353, 355	sylbird 250	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → (¬ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
357	246, 232	div0d 10800	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ → (0 / 𝑘) = 0)
358		oveq1 6657	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃‘𝑛) = 0 → ((𝑃‘𝑛) / 𝑘) = (0 / 𝑘))
359	358	eqeq1d 2624	. . . . . . . . . . . . . . 15 ⊢ ((𝑃‘𝑛) = 0 → (((𝑃‘𝑛) / 𝑘) = 0 ↔ (0 / 𝑘) = 0))
360	357, 359	syl5ibrcom 237	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → ((𝑃‘𝑛) = 0 → ((𝑃‘𝑛) / 𝑘) = 0))
361	360	ad3antlr 767	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑃‘𝑛) = 0 → ((𝑃‘𝑛) / 𝑘) = 0))
362		ffn 6045	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃:(1...𝑁)⟶(0...𝑘) → 𝑃 Fn (1...𝑁))
363	336, 362	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝑃 Fn (1...𝑁))
364		fnconstg 6093	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ V → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
365	337, 364	mp1i 13	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
366		eqidd 2623	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑃‘𝑛) = (𝑃‘𝑛))
367	337	fvconst2 6469	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {𝑘})‘𝑛) = 𝑘)
368	367	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {𝑘})‘𝑛) = 𝑘)
369	363, 365, 331, 331, 332, 366, 368	ofval 6906	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = ((𝑃‘𝑛) / 𝑘))
370	369	an32s 846	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = ((𝑃‘𝑛) / 𝑘))
371	370	eqeq1d 2624	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → (((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 0 ↔ ((𝑃‘𝑛) / 𝑘) = 0))
372	361, 371	sylibrd 249	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑃‘𝑛) = 0 → ((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 0))
373		simplll 798	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → 𝜑)
374		simplr 792	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → 𝑛 ∈ (1...𝑁))
375	346	adantlr 751	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼)
376		ovex 6678	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) ∈ V
377		eleq1 2689	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) → (𝑧 ∈ 𝐼 ↔ (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼))
378		fveq1 6190	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) → (𝑧‘𝑛) = ((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))‘𝑛))
379	378	eqeq1d 2624	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) → ((𝑧‘𝑛) = 0 ↔ ((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 0))
380		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) → (𝐹‘𝑧) = (𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))))
381	380	fveq1d 6193	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) → ((𝐹‘𝑧)‘𝑛) = ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))
382	381	breq1d 4663	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) → (((𝐹‘𝑧)‘𝑛) ≤ 0 ↔ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
383	379, 382	imbi12d 334	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) → (((𝑧‘𝑛) = 0 → ((𝐹‘𝑧)‘𝑛) ≤ 0) ↔ (((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 0 → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0)))
384	377, 383	imbi12d 334	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) → ((𝑧 ∈ 𝐼 → ((𝑧‘𝑛) = 0 → ((𝐹‘𝑧)‘𝑛) ≤ 0)) ↔ ((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 → (((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 0 → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))))
385	384	imbi2d 330	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) → ((𝑛 ∈ (1...𝑁) → (𝑧 ∈ 𝐼 → ((𝑧‘𝑛) = 0 → ((𝐹‘𝑧)‘𝑛) ≤ 0))) ↔ (𝑛 ∈ (1...𝑁) → ((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 → (((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 0 → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0)))))
386	385	imbi2d 330	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) → ((𝜑 → (𝑛 ∈ (1...𝑁) → (𝑧 ∈ 𝐼 → ((𝑧‘𝑛) = 0 → ((𝐹‘𝑧)‘𝑛) ≤ 0)))) ↔ (𝜑 → (𝑛 ∈ (1...𝑁) → ((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 → (((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 0 → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))))))
387		poimir.2	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → ((𝐹‘𝑧)‘𝑛) ≤ 0)
388	387	3exp2 1285	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑛 ∈ (1...𝑁) → (𝑧 ∈ 𝐼 → ((𝑧‘𝑛) = 0 → ((𝐹‘𝑧)‘𝑛) ≤ 0))))
389	376, 386, 388	vtocl 3259	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑛 ∈ (1...𝑁) → ((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 → (((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 0 → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))))
390	373, 374, 375, 389	syl3c 66	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → (((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 0 → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
391	372, 390	syld 47	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑃‘𝑛) = 0 → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
392	356, 391	jaod 395	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → ((¬ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∨ (𝑃‘𝑛) = 0) → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
393	204, 392	syld 47	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
394	393	reximdva 3017	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) → (∃𝑗 ∈ (0...𝑁)(𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → ∃𝑗 ∈ (0...𝑁)((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
395	394	anasss 679	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → (∃𝑗 ∈ (0...𝑁)(𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → ∃𝑗 ∈ (0...𝑁)((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
396	110, 395	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → ∃𝑗 ∈ (0...𝑁)((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0)
397		breq 4655	. . . . . . . 8 ⊢ (𝑟 = ^◡ ≤ → (0𝑟((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ↔ 0^◡ ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
398		fvex 6201	. . . . . . . . 9 ⊢ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∈ V
399	34, 398	brcnv 5305	. . . . . . . 8 ⊢ (0^◡ ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ↔ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0)
400	397, 399	syl6bb 276	. . . . . . 7 ⊢ (𝑟 = ^◡ ≤ → (0𝑟((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ↔ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
401	400	rexbidv 3052	. . . . . 6 ⊢ (𝑟 = ^◡ ≤ → (∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ↔ ∃𝑗 ∈ (0...𝑁)((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
402	396, 401	syl5ibrcom 237	. . . . 5 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → (𝑟 = ^◡ ≤ → ∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
403	78, 402	jaod 395	. . . 4 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → ((𝑟 = ≤ ∨ 𝑟 = ^◡ ≤ ) → ∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
404	1, 403	syl5 34	. . 3 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → (𝑟 ∈ { ≤ , ^◡ ≤ } → ∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
405	404	exp32 631	. 2 ⊢ (𝜑 → (𝑘 ∈ ℕ → (𝑛 ∈ (1...𝑁) → (𝑟 ∈ { ≤ , ^◡ ≤ } → ∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))))
406	405	3imp2 1282	1 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ^◡ ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∨ wo 383 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 {cab 2608 ≠ wne 2794 ∀wral 2912 ∃wrex 2913 {crab 2916 Vcvv 3200 ∪ cun 3572 ∩ cin 3573 ⊆ wss 3574 ∅c0 3915 {csn 4177 {cpr 4179 ∪ cuni 4436 class class class wbr 4653 Or wor 5034 × cxp 5112 ^◡ccnv 5113 ran crn 5115 “ cima 5117 Fun wfun 5882 Fn wfn 5883 ⟶wf 5884 –onto→wfo 5886 –1-1-onto→wf1o 5887 ‘cfv 5888 (class class class)co 6650 ∘_𝑓 cof 6895 1^st c1st 7166 2^nd c2nd 7167 ↑_𝑚 cmap 7857 Fincfn 7955 supcsup 8346 ℂcc 9934 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 < clt 10074 ≤ cle 10075 − cmin 10266 / cdiv 10684 ℕcn 11020 ℕ₀cn0 11292 ℤcz 11377 ℤ_≥cuz 11687 ℝ⁺crp 11832 (,)cioo 12175 [,]cicc 12178 ...cfz 12326 ..^cfzo 12465 ↾_t crest 16081 topGenctg 16098 ∏_tcpt 16099 Topctop 20698 Cn ccn 21028

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-map 7859 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fi 8317 df-sup 8348 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-n0 11293 df-z 11378 df-uz 11688 df-rp 11833 df-ioo 12179 df-icc 12182 df-fz 12327 df-fzo 12466 df-rest 16083 df-topgen 16104 df-pt 16105 df-top 20699 df-topon 20716 df-bases 20750 df-cn 21031

This theorem is referenced by: poimirlem32 33441

W3C validator