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 32610

Description: Lemma for poimir 32612, assigning values to the vertices of the tessellation that meet the hypotheses of both poimirlem30 32609 and poimirlem28 32607. Equation (2) of [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.)

**Hypotheses**
Ref	Expression
poimir.0	⊢ (𝜑 → 𝑁 ∈ ℕ)
poimir.i	⊢ 𝐼 = ((0[,]1) ↑_𝑚 (1...𝑁))
poimir.r	⊢ 𝑅 = (∏_t‘((1...𝑁) × {(topGen‘ran (,))}))
poimir.1	⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾_t 𝐼) Cn 𝑅))
poimir.2	⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → ((𝐹‘𝑧)‘𝑛) ≤ 0)
poimirlem31.p	⊢ 𝑃 = ((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 4145	. . . 4 ⊢ (𝑟 ∈ { ≤ , ^◡ ≤ } → (𝑟 = ≤ ∨ 𝑟 = ^◡ ≤ ))
2		simprr 792	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → 𝑛 ∈ (1...𝑁))
3		1eluzge0 11608	. . . . . . . . . . 11 ⊢ 1 ∈ (ℤ_≥‘0)
4		fzss1 12251	. . . . . . . . . . 11 ⊢ (1 ∈ (ℤ_≥‘0) → (1...𝑁) ⊆ (0...𝑁))
5	3, 4	ax-mp 5	. . . . . . . . . 10 ⊢ (1...𝑁) ⊆ (0...𝑁)
6	5	sseli 3564	. . . . . . . . 9 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ (0...𝑁))
7	6	anim2i 591	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (𝑘 ∈ ℕ ∧ 𝑛 ∈ (0...𝑁)))
8		eleq1 2676	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑛 → (𝑖 ∈ (0...𝑁) ↔ 𝑛 ∈ (0...𝑁)))
9	8	anbi2d 736	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑛 → ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑁)) ↔ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (0...𝑁))))
10	9	anbi2d 736	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑛 → ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑁))) ↔ (𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (0...𝑁)))))
11		eqeq1 2614	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑛 → (𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) ↔ 𝑛 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < )))
12	11	rexbidv 3034	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑛 → (∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) ↔ ∃𝑗 ∈ (0...𝑁)𝑛 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < )))
13	10, 12	imbi12d 333	. . . . . . . . . 10 ⊢ (𝑖 = 𝑛 → (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑁))) → ∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < )) ↔ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (0...𝑁))) → ∃𝑗 ∈ (0...𝑁)𝑛 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ))))
14		poimirlem31.5	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑁))) → ∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ))
15	13, 14	chvarv 2251	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (0...𝑁))) → ∃𝑗 ∈ (0...𝑁)𝑛 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ))
16		elfzle1 12215	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...𝑁) → 1 ≤ 𝑛)
17		1re 9918	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ
18		elfzelz 12213	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℤ)
19	18	zred 11358	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℝ)
20		lenlt 9995	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (1 ≤ 𝑛 ↔ ¬ 𝑛 < 1))
21	17, 19, 20	sylancr 694	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...𝑁) → (1 ≤ 𝑛 ↔ ¬ 𝑛 < 1))
22	16, 21	mpbid 221	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...𝑁) → ¬ 𝑛 < 1)
23		elsni 4142	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ {0} → 𝑛 = 0)
24		0lt1 10429	. . . . . . . . . . . . 13 ⊢ 0 < 1
25	23, 24	syl6eqbr 4622	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ {0} → 𝑛 < 1)
26	22, 25	nsyl 134	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...𝑁) → ¬ 𝑛 ∈ {0})
27		ltso 9997	. . . . . . . . . . . . . . 15 ⊢ < Or ℝ
28		snfi 7923	. . . . . . . . . . . . . . . . 17 ⊢ {0} ∈ Fin
29		fzfi 12633	. . . . . . . . . . . . . . . . . 18 ⊢ (1...𝑁) ∈ Fin
30		rabfi 8070	. . . . . . . . . . . . . . . . . 18 ⊢ ((1...𝑁) ∈ Fin → {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)} ∈ Fin)
31	29, 30	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)} ∈ Fin
32		unfi 8112	. . . . . . . . . . . . . . . . 17 ⊢ (({0} ∈ Fin ∧ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)} ∈ Fin) → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ∈ Fin)
33	28, 31, 32	mp2an 704	. . . . . . . . . . . . . . . 16 ⊢ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ∈ Fin
34		c0ex 9913	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ V
35	34	snid 4155	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ {0}
36		elun1 3742	. . . . . . . . . . . . . . . . 17 ⊢ (0 ∈ {0} → 0 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}))
37		ne0i 3880	. . . . . . . . . . . . . . . . 17 ⊢ (0 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ≠ ∅)
38	35, 36, 37	mp2b 10	. . . . . . . . . . . . . . . 16 ⊢ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ≠ ∅
39		0re 9919	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℝ
40		snssi 4280	. . . . . . . . . . . . . . . . . 18 ⊢ (0 ∈ ℝ → {0} ⊆ ℝ)
41	39, 40	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ {0} ⊆ ℝ
42		ssrab2 3650	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)} ⊆ (1...𝑁)
43	18	ssriv 3572	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...𝑁) ⊆ ℤ
44		zssre 11261	. . . . . . . . . . . . . . . . . . 19 ⊢ ℤ ⊆ ℝ
45	43, 44	sstri 3577	. . . . . . . . . . . . . . . . . 18 ⊢ (1...𝑁) ⊆ ℝ
46	42, 45	sstri 3577	. . . . . . . . . . . . . . . . 17 ⊢ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)} ⊆ ℝ
47	41, 46	unssi 3750	. . . . . . . . . . . . . . . 16 ⊢ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ⊆ ℝ
48	33, 38, 47	3pm3.2i 1232	. . . . . . . . . . . . . . 15 ⊢ (({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ∈ Fin ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ≠ ∅ ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ⊆ ℝ)
49		fisupcl 8258	. . . . . . . . . . . . . . 15 ⊢ (( < Or ℝ ∧ (({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ∈ Fin ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ≠ ∅ ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ⊆ ℝ)) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}))
50	27, 48, 49	mp2an 704	. . . . . . . . . . . . . 14 ⊢ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)})
51		eleq1 2676	. . . . . . . . . . . . . 14 ⊢ (𝑛 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → (𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ↔ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)})))
52	50, 51	mpbiri 247	. . . . . . . . . . . . 13 ⊢ (𝑛 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → 𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}))
53		elun 3715	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ↔ (𝑛 ∈ {0} ∨ 𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}))
54	52, 53	sylib 207	. . . . . . . . . . . 12 ⊢ (𝑛 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → (𝑛 ∈ {0} ∨ 𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}))
55		oveq2 6557	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑛 → (1...𝑎) = (1...𝑛))
56	55	raleqdv 3121	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑛 → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
57	56	elrab 3331	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)} ↔ (𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
58		elfzuz 12209	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ (ℤ_≥‘1))
59		eluzfz2 12220	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (ℤ_≥‘1) → 𝑛 ∈ (1...𝑛))
60	58, 59	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ (1...𝑛))
61		simpl 472	. . . . . . . . . . . . . . . 16 ⊢ ((0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) → 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏))
62	61	ralimi 2936	. . . . . . . . . . . . . . 15 ⊢ (∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏))
63		fveq2 6103	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑛 → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) = ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))
64	63	breq2d 4595	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑛 → (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ↔ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
65	64	rspcva 3280	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (1...𝑛) ∧ ∀𝑏 ∈ (1...𝑛)0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏)) → 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))
66	60, 62, 65	syl2an 493	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) → 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))
67	57, 66	sylbi 206	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)} → 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))
68	67	orim2i 539	. . . . . . . . . . . 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 396	. . . . . . . . . . 11 ⊢ (¬ 𝑛 ∈ {0} → ((𝑛 ∈ {0} ∨ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)) → 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
71	26, 69, 70	syl2im 39	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...𝑁) → (𝑛 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
72	71	reximdv 2999	. . . . . . . . 9 ⊢ (𝑛 ∈ (1...𝑁) → (∃𝑗 ∈ (0...𝑁)𝑛 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → ∃𝑗 ∈ (0...𝑁)0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
73	15, 72	syl5 33	. . . . . . . 8 ⊢ (𝑛 ∈ (1...𝑁) → ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (0...𝑁))) → ∃𝑗 ∈ (0...𝑁)0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
74	7, 73	sylan2i 685	. . . . . . 7 ⊢ (𝑛 ∈ (1...𝑁) → ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → ∃𝑗 ∈ (0...𝑁)0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
75	2, 74	mpcom 37	. . . . . 6 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → ∃𝑗 ∈ (0...𝑁)0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))
76		breq 4585	. . . . . . 7 ⊢ (𝑟 = ≤ → (0𝑟((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ↔ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
77	76	rexbidv 3034	. . . . . 6 ⊢ (𝑟 = ≤ → (∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ↔ ∃𝑗 ∈ (0...𝑁)0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
78	75, 77	syl5ibrcom 236	. . . . 5 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → (𝑟 = ≤ → ∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
79		poimir.0	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℕ)
80	79	nnzd 11357	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℤ)
81		elfzm1b 12287	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑛 ∈ (1...𝑁) ↔ (𝑛 − 1) ∈ (0...(𝑁 − 1))))
82	18, 80, 81	syl2anr 494	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 ∈ (1...𝑁) ↔ (𝑛 − 1) ∈ (0...(𝑁 − 1))))
83	82	biimpd 218	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 ∈ (1...𝑁) → (𝑛 − 1) ∈ (0...(𝑁 − 1))))
84	83	ex 449	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑛 ∈ (1...𝑁) → (𝑛 ∈ (1...𝑁) → (𝑛 − 1) ∈ (0...(𝑁 − 1)))))
85	84	pm2.43d 51	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑛 ∈ (1...𝑁) → (𝑛 − 1) ∈ (0...(𝑁 − 1))))
86	79	nncnd 10913	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℂ)
87		npcan1 10334	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
88	86, 87	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
89		nnm1nn0 11211	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
90	79, 89	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ₀)
91	90	nn0zd 11356	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
92		uzid 11578	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)))
93		peano2uz 11617	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
94	91, 92, 93	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
95	88, 94	eqeltrrd 2689	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑁 − 1)))
96		fzss2 12252	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑁 − 1)) → (0...(𝑁 − 1)) ⊆ (0...𝑁))
97	95, 96	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (0...(𝑁 − 1)) ⊆ (0...𝑁))
98	97	sseld 3567	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑛 − 1) ∈ (0...(𝑁 − 1)) → (𝑛 − 1) ∈ (0...𝑁)))
99	85, 98	syld 46	. . . . . . . . . 10 ⊢ (𝜑 → (𝑛 ∈ (1...𝑁) → (𝑛 − 1) ∈ (0...𝑁)))
100	99	anim2d 587	. . . . . . . . 9 ⊢ (𝜑 → ((𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁)) → (𝑘 ∈ ℕ ∧ (𝑛 − 1) ∈ (0...𝑁))))
101	100	imp 444	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → (𝑘 ∈ ℕ ∧ (𝑛 − 1) ∈ (0...𝑁)))
102		ovex 6577	. . . . . . . . 9 ⊢ (𝑛 − 1) ∈ V
103		eleq1 2676	. . . . . . . . . . . 12 ⊢ (𝑖 = (𝑛 − 1) → (𝑖 ∈ (0...𝑁) ↔ (𝑛 − 1) ∈ (0...𝑁)))
104	103	anbi2d 736	. . . . . . . . . . 11 ⊢ (𝑖 = (𝑛 − 1) → ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑁)) ↔ (𝑘 ∈ ℕ ∧ (𝑛 − 1) ∈ (0...𝑁))))
105	104	anbi2d 736	. . . . . . . . . 10 ⊢ (𝑖 = (𝑛 − 1) → ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑁))) ↔ (𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑛 − 1) ∈ (0...𝑁)))))
106		eqeq1 2614	. . . . . . . . . . 11 ⊢ (𝑖 = (𝑛 − 1) → (𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) ↔ (𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < )))
107	106	rexbidv 3034	. . . . . . . . . 10 ⊢ (𝑖 = (𝑛 − 1) → (∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) ↔ ∃𝑗 ∈ (0...𝑁)(𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < )))
108	105, 107	imbi12d 333	. . . . . . . . 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 3232	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ (𝑛 − 1) ∈ (0...𝑁))) → ∃𝑗 ∈ (0...𝑁)(𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ))
110	101, 109	syldan 486	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → ∃𝑗 ∈ (0...𝑁)(𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ))
111		eleq1 2676	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ↔ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)})))
112	50, 111	mpbiri 247	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → (𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}))
113		elun 3715	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ↔ ((𝑛 − 1) ∈ {0} ∨ (𝑛 − 1) ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}))
114	102	elsn 4140	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 − 1) ∈ {0} ↔ (𝑛 − 1) = 0)
115		oveq2 6557	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (𝑛 − 1) → (1...𝑎) = (1...(𝑛 − 1)))
116	115	raleqdv 3121	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑛 − 1) → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
117	116	elrab 3331	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 − 1) ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)} ↔ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
118	114, 117	orbi12i 542	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 − 1) ∈ {0} ∨ (𝑛 − 1) ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ↔ ((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0))))
119	113, 118	bitri 263	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ↔ ((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0))))
120	112, 119	sylib 207	. . . . . . . . . . . . . 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 10742	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℝ → (𝑛 − 1) < 𝑛)
123		peano2rem 10227	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
124		ltnle 9996	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑛 − 1) ∈ ℝ ∧ 𝑛 ∈ ℝ) → ((𝑛 − 1) < 𝑛 ↔ ¬ 𝑛 ≤ (𝑛 − 1)))
125	123, 124	mpancom 700	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℝ → ((𝑛 − 1) < 𝑛 ↔ ¬ 𝑛 ≤ (𝑛 − 1)))
126	122, 125	mpbid 221	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℝ → ¬ 𝑛 ≤ (𝑛 − 1))
127	19, 126	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (1...𝑁) → ¬ 𝑛 ≤ (𝑛 − 1))
128		breq2 4587	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → (𝑛 ≤ (𝑛 − 1) ↔ 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < )))
129	128	notbid 307	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → (¬ 𝑛 ≤ (𝑛 − 1) ↔ ¬ 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < )))
130	127, 129	syl5ibcom 234	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → ¬ 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < )))
131		elun2 3743	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)} → 𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}))
132		fimaxre2 10848	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ⊆ ℝ ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)})𝑦 ≤ 𝑥)
133	47, 33, 132	mp2an 704	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)})𝑦 ≤ 𝑥
134	47, 38, 133	3pm3.2i 1232	. . . . . . . . . . . . . . . . . . 19 ⊢ (({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ⊆ ℝ ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)})𝑦 ≤ 𝑥)
135	134	suprubii 10875	. . . . . . . . . . . . . . . . . 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 149	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → ¬ 𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)})
138		ianor 508	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) ↔ (¬ 𝑛 ∈ (1...𝑁) ∨ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
139	138, 57	xchnxbir 322	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)} ↔ (¬ 𝑛 ∈ (1...𝑁) ∨ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
140	137, 139	sylib 207	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → (¬ 𝑛 ∈ (1...𝑁) ∨ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
141	130, 140	syl6 34	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → (¬ 𝑛 ∈ (1...𝑁) ∨ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0))))
142		pm2.63 825	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (1...𝑁) ∨ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) → ((¬ 𝑛 ∈ (1...𝑁) ∨ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) → ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
143	142	orcs 408	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (1...𝑁) → ((¬ 𝑛 ∈ (1...𝑁) ∨ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) → ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
144	141, 143	syld 46	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
145	121, 144	jcad 554	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → (((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0))) ∧ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0))))
146		andir 908	. . . . . . . . . . . . . 14 ⊢ ((((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0))) ∧ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) ↔ (((𝑛 − 1) = 0 ∧ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) ∨ (((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) ∧ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0))))
147		1p0e1 11010	. . . . . . . . . . . . . . . . . 18 ⊢ (1 + 0) = 1
148	18	zcnd 11359	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ)
149		ax-1cn 9873	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℂ
150		0cn 9911	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ ℂ
151		subadd 10163	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ ∧ 0 ∈ ℂ) → ((𝑛 − 1) = 0 ↔ (1 + 0) = 𝑛))
152	149, 150, 151	mp3an23 1408	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℂ → ((𝑛 − 1) = 0 ↔ (1 + 0) = 𝑛))
153	148, 152	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) = 0 ↔ (1 + 0) = 𝑛))
154	153	biimpa 500	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (1...𝑁) ∧ (𝑛 − 1) = 0) → (1 + 0) = 𝑛)
155	147, 154	syl5reqr 2659	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (1...𝑁) ∧ (𝑛 − 1) = 0) → 𝑛 = 1)
156		1z 11284	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℤ
157		fzsn 12254	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 ∈ ℤ → (1...1) = {1})
158	156, 157	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1...1) = {1}
159		oveq2 6557	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 1 → (1...𝑛) = (1...1))
160		sneq 4135	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 1 → {𝑛} = {1})
161	158, 159, 160	3eqtr4a 2670	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 1 → (1...𝑛) = {𝑛})
162	161	raleqdv 3121	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 1 → (∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) ↔ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
163	162	notbid 307	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 1 → (¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) ↔ ¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
164	163	biimpd 218	. . . . . . . . . . . . . . . . 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 627	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (1...𝑁) → (((𝑛 − 1) = 0 ∧ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) → ¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
167		ralun 3757	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) → ∀𝑏 ∈ ((1...(𝑛 − 1)) ∪ {𝑛})(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0))
168		npcan1 10334	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ ℂ → ((𝑛 − 1) + 1) = 𝑛)
169	148, 168	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) + 1) = 𝑛)
170	169, 58	eqeltrd 2688	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) + 1) ∈ (ℤ_≥‘1))
171		peano2zm 11297	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ ℤ → (𝑛 − 1) ∈ ℤ)
172		uzid 11578	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 − 1) ∈ ℤ → (𝑛 − 1) ∈ (ℤ_≥‘(𝑛 − 1)))
173		peano2uz 11617	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 − 1) ∈ (ℤ_≥‘(𝑛 − 1)) → ((𝑛 − 1) + 1) ∈ (ℤ_≥‘(𝑛 − 1)))
174	18, 171, 172, 173	4syl 19	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) + 1) ∈ (ℤ_≥‘(𝑛 − 1)))
175	169, 174	eqeltrrd 2689	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ (ℤ_≥‘(𝑛 − 1)))
176		fzsplit2 12237	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑛 − 1) + 1) ∈ (ℤ_≥‘1) ∧ 𝑛 ∈ (ℤ_≥‘(𝑛 − 1))) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)))
177	170, 175, 176	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ (1...𝑁) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)))
178	169	oveq1d 6564	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ (1...𝑁) → (((𝑛 − 1) + 1)...𝑛) = (𝑛...𝑛))
179		fzsn 12254	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ ℤ → (𝑛...𝑛) = {𝑛})
180	18, 179	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ (1...𝑁) → (𝑛...𝑛) = {𝑛})
181	178, 180	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ (1...𝑁) → (((𝑛 − 1) + 1)...𝑛) = {𝑛})
182	181	uneq2d 3729	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ (1...𝑁) → ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)) = ((1...(𝑛 − 1)) ∪ {𝑛}))
183	177, 182	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ (1...𝑁) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ {𝑛}))
184	183	raleqdv 3121	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) ↔ ∀𝑏 ∈ ((1...(𝑛 − 1)) ∪ {𝑛})(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
185	167, 184	syl5ibr 235	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (1...𝑁) → ((∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
186	185	expdimp 452	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
187	186	con3d 147	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) → (¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) → ¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
188	187	adantrl 748	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ (1...𝑁) ∧ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0))) → (¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) → ¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
189	188	expimpd 627	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (1...𝑁) → ((((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) ∧ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) → ¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
190	166, 189	jaod 394	. . . . . . . . . . . . . 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 231	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...𝑁) → ((((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0))) ∧ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) → ¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)))
192		fveq2 6103	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑛 → (𝑃‘𝑏) = (𝑃‘𝑛))
193	192	neeq1d 2841	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑛 → ((𝑃‘𝑏) ≠ 0 ↔ (𝑃‘𝑛) ≠ 0))
194	64, 193	anbi12d 743	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑛 → ((0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∧ (𝑃‘𝑛) ≠ 0)))
195	194	ralsng 4165	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∧ (𝑃‘𝑛) ≠ 0)))
196	195	notbid 307	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (1...𝑁) → (¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) ↔ ¬ (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∧ (𝑃‘𝑛) ≠ 0)))
197		ianor 508	. . . . . . . . . . . . . . 15 ⊢ (¬ (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∧ (𝑃‘𝑛) ≠ 0) ↔ (¬ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∨ ¬ (𝑃‘𝑛) ≠ 0))
198		nne 2786	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑃‘𝑛) ≠ 0 ↔ (𝑃‘𝑛) = 0)
199	198	orbi2i 540	. . . . . . . . . . . . . . 15 ⊢ ((¬ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∨ ¬ (𝑃‘𝑛) ≠ 0) ↔ (¬ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∨ (𝑃‘𝑛) = 0))
200	197, 199	bitri 263	. . . . . . . . . . . . . 14 ⊢ (¬ (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∧ (𝑃‘𝑛) ≠ 0) ↔ (¬ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∨ (𝑃‘𝑛) = 0))
201	196, 200	syl6bb 275	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...𝑁) → (¬ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0) ↔ (¬ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∨ (𝑃‘𝑛) = 0)))
202	191, 201	sylibd 228	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...𝑁) → ((((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0))) ∧ ¬ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)) → (¬ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∨ (𝑃‘𝑛) = 0)))
203	145, 202	syld 46	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → (¬ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∨ (𝑃‘𝑛) = 0)))
204	203	ad2antlr 759	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → (¬ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∨ (𝑃‘𝑛) = 0)))
205		poimir.1	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↾_t 𝐼) Cn 𝑅))
206		poimir.r	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑅 = (∏_t‘((1...𝑁) × {(topGen‘ran (,))}))
207		retop 22375	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (topGen‘ran (,)) ∈ Top
208	207	fconst6 6008	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top
209		pttop 21195	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1...𝑁) ∈ Fin ∧ ((1...𝑁) × {(topGen‘ran (,))}):(1...𝑁)⟶Top) → (∏_t‘((1...𝑁) × {(topGen‘ran (,))})) ∈ Top)
210	29, 208, 209	mp2an 704	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∏_t‘((1...𝑁) × {(topGen‘ran (,))})) ∈ Top
211	206, 210	eqeltri 2684	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑅 ∈ Top
212		poimir.i	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐼 = ((0[,]1) ↑_𝑚 (1...𝑁))
213		reex 9906	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℝ ∈ V
214		unitssre 12190	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0[,]1) ⊆ ℝ
215		mapss 7786	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℝ ∈ V ∧ (0[,]1) ⊆ ℝ) → ((0[,]1) ↑_𝑚 (1...𝑁)) ⊆ (ℝ ↑_𝑚 (1...𝑁)))
216	213, 214, 215	mp2an 704	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0[,]1) ↑_𝑚 (1...𝑁)) ⊆ (ℝ ↑_𝑚 (1...𝑁))
217	212, 216	eqsstri 3598	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐼 ⊆ (ℝ ↑_𝑚 (1...𝑁))
218		uniretop 22376	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℝ = ∪ (topGen‘ran (,))
219	206, 218	ptuniconst 21211	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1...𝑁) ∈ Fin ∧ (topGen‘ran (,)) ∈ Top) → (ℝ ↑_𝑚 (1...𝑁)) = ∪ 𝑅)
220	29, 207, 219	mp2an 704	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℝ ↑_𝑚 (1...𝑁)) = ∪ 𝑅
221	220	restuni 20776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Top ∧ 𝐼 ⊆ (ℝ ↑_𝑚 (1...𝑁))) → 𝐼 = ∪ (𝑅 ↾_t 𝐼))
222	211, 217, 221	mp2an 704	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐼 = ∪ (𝑅 ↾_t 𝐼)
223	222, 220	cnf 20860	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ ((𝑅 ↾_t 𝐼) Cn 𝑅) → 𝐹:𝐼⟶(ℝ ↑_𝑚 (1...𝑁)))
224	205, 223	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹:𝐼⟶(ℝ ↑_𝑚 (1...𝑁)))
225	224	ad2antrr 758	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝐹:𝐼⟶(ℝ ↑_𝑚 (1...𝑁)))
226		simplr 788	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝑘 ∈ ℕ)
227		elfzelz 12213	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ (0...𝑘) → 𝑥 ∈ ℤ)
228	227	zred 11358	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ (0...𝑘) → 𝑥 ∈ ℝ)
229	228	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑥 ∈ ℝ)
230		nnre 10904	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
231	230	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ)
232		nnne0 10930	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 ∈ ℕ → 𝑘 ≠ 0)
233	232	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ≠ 0)
234	229, 231, 233	redivcld 10732	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑥 / 𝑘) ∈ ℝ)
235		elfzle1 12215	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ (0...𝑘) → 0 ≤ 𝑥)
236	228, 235	jca 553	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ (0...𝑘) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
237		nnrp 11718	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ⁺)
238	237	rpregt0d 11754	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 < 𝑘))
239		divge0 10771	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → 0 ≤ (𝑥 / 𝑘))
240	236, 238, 239	syl2an 493	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝑥 / 𝑘))
241		elfzle2 12216	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ (0...𝑘) → 𝑥 ≤ 𝑘)
242	241	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑥 ≤ 𝑘)
243		1red 9934	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
244	237	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ⁺)
245	229, 243, 244	ledivmuld 11801	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑥 / 𝑘) ≤ 1 ↔ 𝑥 ≤ (𝑘 · 1)))
246		nncn 10905	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
247	246	mulid1d 9936	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 ∈ ℕ → (𝑘 · 1) = 𝑘)
248	247	breq2d 4595	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ∈ ℕ → (𝑥 ≤ (𝑘 · 1) ↔ 𝑥 ≤ 𝑘))
249	248	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑥 ≤ (𝑘 · 1) ↔ 𝑥 ≤ 𝑘))
250	245, 249	bitrd 267	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑥 / 𝑘) ≤ 1 ↔ 𝑥 ≤ 𝑘))
251	242, 250	mpbird 246	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑥 / 𝑘) ≤ 1)
252	39, 17	elicc2i 12110	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 / 𝑘) ∈ (0[,]1) ↔ ((𝑥 / 𝑘) ∈ ℝ ∧ 0 ≤ (𝑥 / 𝑘) ∧ (𝑥 / 𝑘) ≤ 1))
253	234, 240, 251, 252	syl3anbrc 1239	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑥 / 𝑘) ∈ (0[,]1))
254	253	ancoms 468	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ (0...𝑘)) → (𝑥 / 𝑘) ∈ (0[,]1))
255		elsni 4142	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ {𝑘} → 𝑦 = 𝑘)
256	255	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ {𝑘} → (𝑥 / 𝑦) = (𝑥 / 𝑘))
257	256	eleq1d 2672	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ {𝑘} → ((𝑥 / 𝑦) ∈ (0[,]1) ↔ (𝑥 / 𝑘) ∈ (0[,]1)))
258	254, 257	syl5ibrcom 236	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℕ ∧ 𝑥 ∈ (0...𝑘)) → (𝑦 ∈ {𝑘} → (𝑥 / 𝑦) ∈ (0[,]1)))
259	258	impr 647	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ ∧ (𝑥 ∈ (0...𝑘) ∧ 𝑦 ∈ {𝑘})) → (𝑥 / 𝑦) ∈ (0[,]1))
260	226, 259	sylan 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ (0...𝑘) ∧ 𝑦 ∈ {𝑘})) → (𝑥 / 𝑦) ∈ (0[,]1))
261		elun 3715	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ ({1} ∪ {0}) ↔ (𝑦 ∈ {1} ∨ 𝑦 ∈ {0}))
262		fzofzp1 12431	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ (0..^𝑘) → (𝑥 + 1) ∈ (0...𝑘))
263		elsni 4142	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 ∈ {1} → 𝑦 = 1)
264	263	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ {1} → (𝑥 + 𝑦) = (𝑥 + 1))
265	264	eleq1d 2672	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ {1} → ((𝑥 + 𝑦) ∈ (0...𝑘) ↔ (𝑥 + 1) ∈ (0...𝑘)))
266	262, 265	syl5ibrcom 236	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ (0..^𝑘) → (𝑦 ∈ {1} → (𝑥 + 𝑦) ∈ (0...𝑘)))
267		elfzonn0 12380	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 ∈ (0..^𝑘) → 𝑥 ∈ ℕ₀)
268	267	nn0cnd 11230	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∈ (0..^𝑘) → 𝑥 ∈ ℂ)
269	268	addid1d 10115	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ (0..^𝑘) → (𝑥 + 0) = 𝑥)
270		elfzofz 12354	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ (0..^𝑘) → 𝑥 ∈ (0...𝑘))
271	269, 270	eqeltrd 2688	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ (0..^𝑘) → (𝑥 + 0) ∈ (0...𝑘))
272		elsni 4142	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 ∈ {0} → 𝑦 = 0)
273	272	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ {0} → (𝑥 + 𝑦) = (𝑥 + 0))
274	273	eleq1d 2672	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ {0} → ((𝑥 + 𝑦) ∈ (0...𝑘) ↔ (𝑥 + 0) ∈ (0...𝑘)))
275	271, 274	syl5ibrcom 236	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ (0..^𝑘) → (𝑦 ∈ {0} → (𝑥 + 𝑦) ∈ (0...𝑘)))
276	266, 275	jaod 394	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ (0..^𝑘) → ((𝑦 ∈ {1} ∨ 𝑦 ∈ {0}) → (𝑥 + 𝑦) ∈ (0...𝑘)))
277	261, 276	syl5bi 231	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ (0..^𝑘) → (𝑦 ∈ ({1} ∪ {0}) → (𝑥 + 𝑦) ∈ (0...𝑘)))
278	277	imp 444	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ (0..^𝑘) ∧ 𝑦 ∈ ({1} ∪ {0})) → (𝑥 + 𝑦) ∈ (0...𝑘))
279	278	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ (0..^𝑘) ∧ 𝑦 ∈ ({1} ∪ {0}))) → (𝑥 + 𝑦) ∈ (0...𝑘))
280		poimirlem31.3	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐺:ℕ⟶((ℕ₀ ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
281	280	ffvelrnda 6267	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ((ℕ₀ ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
282		xp1st 7089	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺‘𝑘) ∈ ((ℕ₀ ↑_𝑚 (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1^st ‘(𝐺‘𝑘)) ∈ (ℕ₀ ↑_𝑚 (1...𝑁)))
283		elmapfn 7766	. . . . . . . . . . . . . . . . . . . . . . . 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 5808	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1^st ‘(𝐺‘𝑘)):(1...𝑁)⟶(0..^𝑘) ↔ ((1^st ‘(𝐺‘𝑘)) Fn (1...𝑁) ∧ ran (1^st ‘(𝐺‘𝑘)) ⊆ (0..^𝑘)))
287	284, 285, 286	sylanbrc 695	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1^st ‘(𝐺‘𝑘)):(1...𝑁)⟶(0..^𝑘))
288	287	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (1^st ‘(𝐺‘𝑘)):(1...𝑁)⟶(0..^𝑘))
289		1ex 9914	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 ∈ V
290	289	fconst 6004	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}):((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗))⟶{1}
291	34	fconst 6004	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}):((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁))⟶{0}
292	290, 291	pm3.2i 470	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}):((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗))⟶{1} ∧ (((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}):((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁))⟶{0})
293		xp2nd 7090	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 6113	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (2^nd ‘(𝐺‘𝑘)) ∈ V
296		f1oeq1 6040	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = (2^nd ‘(𝐺‘𝑘)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2^nd ‘(𝐺‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁)))
297	295, 296	elab 3319	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((2^nd ‘(𝐺‘𝑘)) ∈ {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2^nd ‘(𝐺‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁))
298	294, 297	sylib 207	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2^nd ‘(𝐺‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁))
299		dff1o3 6056	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((2^nd ‘(𝐺‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2^nd ‘(𝐺‘𝑘)):(1...𝑁)–onto→(1...𝑁) ∧ Fun ^◡(2^nd ‘(𝐺‘𝑘))))
300	299	simprbi 479	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((2^nd ‘(𝐺‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun ^◡(2^nd ‘(𝐺‘𝑘)))
301		imain 5888	. . . . . . . . . . . . . . . . . . . . . . . . 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 12302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ₀)
304	303	nn0red 11229	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
305	304	ltp1d 10833	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1))
306		fzdisj 12239	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
307	305, 306	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
308	307	imaeq2d 5385	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 ∈ (0...𝑁) → ((2^nd ‘(𝐺‘𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((2^nd ‘(𝐺‘𝑘)) “ ∅))
309		ima0 5400	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((2^nd ‘(𝐺‘𝑘)) “ ∅) = ∅
310	308, 309	syl6eq 2660	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ (0...𝑁) → ((2^nd ‘(𝐺‘𝑘)) “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
311	302, 310	sylan9req 2665	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) ∩ ((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁))) = ∅)
312		fun 5979	. . . . . . . . . . . . . . . . . . . . . . 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 694	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) ∪ ((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
314		imaundi 5464	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((2^nd ‘(𝐺‘𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) ∪ ((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)))
315		nn0p1nn 11209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑗 ∈ ℕ₀ → (𝑗 + 1) ∈ ℕ)
316	303, 315	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ)
317		nnuz 11599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ℕ = (ℤ_≥‘1)
318	316, 317	syl6eleq 2698	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (ℤ_≥‘1))
319		elfzuz3 12210	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ_≥‘𝑗))
320		fzsplit2 12237	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑗 + 1) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ (ℤ_≥‘𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
321	318, 319, 320	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
322	321	imaeq2d 5385	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ (0...𝑁) → ((2^nd ‘(𝐺‘𝑘)) “ (1...𝑁)) = ((2^nd ‘(𝐺‘𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))))
323		f1ofo 6057	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((2^nd ‘(𝐺‘𝑘)):(1...𝑁)–1-1-onto→(1...𝑁) → (2^nd ‘(𝐺‘𝑘)):(1...𝑁)–onto→(1...𝑁))
324		foima 6033	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2665	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑗 ∈ (0...𝑁) ∧ (𝜑 ∧ 𝑘 ∈ ℕ)) → ((2^nd ‘(𝐺‘𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (1...𝑁))
327	326	ancoms 468	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((2^nd ‘(𝐺‘𝑘)) “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = (1...𝑁))
328	314, 327	syl5eqr 2658	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) ∪ ((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁))) = (1...𝑁))
329	328	feq2d 5944	. . . . . . . . . . . . . . . . . . . . . 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 221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
331		fzfid 12634	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ Fin)
332		inidm 3784	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
333	279, 288, 330, 331, 331, 332	off 6810	. . . . . . . . . . . . . . . . . . . 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 5949	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃:(1...𝑁)⟶(0...𝑘) ↔ ((1^st ‘(𝐺‘𝑘)) ∘_𝑓 + ((((2^nd ‘(𝐺‘𝑘)) “ (1...𝑗)) × {1}) ∪ (((2^nd ‘(𝐺‘𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))):(1...𝑁)⟶(0...𝑘))
336	333, 335	sylibr 223	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝑃:(1...𝑁)⟶(0...𝑘))
337		vex 3176	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑘 ∈ V
338	337	fconst 6004	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘}
339	338	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘})
340	260, 336, 339, 331, 331, 332	off 6810	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
341	212	eleq2i 2680	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑_𝑚 (1...𝑁)))
342		ovex 6577	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0[,]1) ∈ V
343		ovex 6577	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...𝑁) ∈ V
344	342, 343	elmap 7772	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑_𝑚 (1...𝑁)) ↔ (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
345	341, 344	bitri 263	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
346	340, 345	sylibr 223	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼)
347	225, 346	ffvelrnd 6268	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))) ∈ (ℝ ↑_𝑚 (1...𝑁)))
348		elmapi 7765	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))) ∈ (ℝ ↑_𝑚 (1...𝑁)) → (𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))):(1...𝑁)⟶ℝ)
349	347, 348	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → (𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))):(1...𝑁)⟶ℝ)
350	349	ffvelrnda 6267	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∈ ℝ)
351	350	an32s 842	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∈ ℝ)
352		0red 9920	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → 0 ∈ ℝ)
353	351, 352	ltnled 10063	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → (((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) < 0 ↔ ¬ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
354		ltle 10005	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∈ ℝ ∧ 0 ∈ ℝ) → (((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) < 0 → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
355	351, 39, 354	sylancl 693	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → (((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) < 0 → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
356	353, 355	sylbird 249	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → (¬ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
357	246, 232	div0d 10679	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ → (0 / 𝑘) = 0)
358		oveq1 6556	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃‘𝑛) = 0 → ((𝑃‘𝑛) / 𝑘) = (0 / 𝑘))
359	358	eqeq1d 2612	. . . . . . . . . . . . . . 15 ⊢ ((𝑃‘𝑛) = 0 → (((𝑃‘𝑛) / 𝑘) = 0 ↔ (0 / 𝑘) = 0))
360	357, 359	syl5ibrcom 236	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → ((𝑃‘𝑛) = 0 → ((𝑃‘𝑛) / 𝑘) = 0))
361	360	ad3antlr 763	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑃‘𝑛) = 0 → ((𝑃‘𝑛) / 𝑘) = 0))
362		ffn 5958	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃:(1...𝑁)⟶(0...𝑘) → 𝑃 Fn (1...𝑁))
363	336, 362	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → 𝑃 Fn (1...𝑁))
364		fnconstg 6006	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ V → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
365	337, 364	mp1i 13	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
366		eqidd 2611	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑃‘𝑛) = (𝑃‘𝑛))
367	337	fvconst2 6374	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {𝑘})‘𝑛) = 𝑘)
368	367	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {𝑘})‘𝑛) = 𝑘)
369	363, 365, 331, 331, 332, 366, 368	ofval 6804	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = ((𝑃‘𝑛) / 𝑘))
370	369	an32s 842	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = ((𝑃‘𝑛) / 𝑘))
371	370	eqeq1d 2612	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → (((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 0 ↔ ((𝑃‘𝑛) / 𝑘) = 0))
372	361, 371	sylibrd 248	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑃‘𝑛) = 0 → ((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 0))
373		simplll 794	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → 𝜑)
374		simplr 788	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → 𝑛 ∈ (1...𝑁))
375	346	adantlr 747	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼)
376		ovex 6577	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) ∈ V
377		eleq1 2676	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) → (𝑧 ∈ 𝐼 ↔ (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼))
378		fveq1 6102	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) → (𝑧‘𝑛) = ((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))‘𝑛))
379	378	eqeq1d 2612	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) → ((𝑧‘𝑛) = 0 ↔ ((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 0))
380		fveq2 6103	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) → (𝐹‘𝑧) = (𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))))
381	380	fveq1d 6105	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) → ((𝐹‘𝑧)‘𝑛) = ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))
382	381	breq1d 4593	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) → (((𝐹‘𝑧)‘𝑛) ≤ 0 ↔ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
383	379, 382	imbi12d 333	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) → (((𝑧‘𝑛) = 0 → ((𝐹‘𝑧)‘𝑛) ≤ 0) ↔ (((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 0 → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0)))
384	377, 383	imbi12d 333	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) → ((𝑧 ∈ 𝐼 → ((𝑧‘𝑛) = 0 → ((𝐹‘𝑧)‘𝑛) ≤ 0)) ↔ ((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 → (((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 0 → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))))
385	384	imbi2d 329	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) → ((𝑛 ∈ (1...𝑁) → (𝑧 ∈ 𝐼 → ((𝑧‘𝑛) = 0 → ((𝐹‘𝑧)‘𝑛) ≤ 0))) ↔ (𝑛 ∈ (1...𝑁) → ((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 → (((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 0 → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0)))))
386	385	imbi2d 329	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) → ((𝜑 → (𝑛 ∈ (1...𝑁) → (𝑧 ∈ 𝐼 → ((𝑧‘𝑛) = 0 → ((𝐹‘𝑧)‘𝑛) ≤ 0)))) ↔ (𝜑 → (𝑛 ∈ (1...𝑁) → ((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 → (((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 0 → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))))))
387		poimir.2	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧 ∈ 𝐼 ∧ (𝑧‘𝑛) = 0)) → ((𝐹‘𝑧)‘𝑛) ≤ 0)
388	387	3exp2 1277	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑛 ∈ (1...𝑁) → (𝑧 ∈ 𝐼 → ((𝑧‘𝑛) = 0 → ((𝐹‘𝑧)‘𝑛) ≤ 0))))
389	376, 386, 388	vtocl 3232	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑛 ∈ (1...𝑁) → ((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 → (((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 0 → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))))
390	373, 374, 375, 389	syl3c 64	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → (((𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 0 → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
391	372, 390	syld 46	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑃‘𝑛) = 0 → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
392	356, 391	jaod 394	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → ((¬ 0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∨ (𝑃‘𝑛) = 0) → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
393	204, 392	syld 46	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
394	393	reximdva 3000	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑁)) → (∃𝑗 ∈ (0...𝑁)(𝑛 − 1) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑃‘𝑏) ≠ 0)}), ℝ, < ) → ∃𝑗 ∈ (0...𝑁)((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
395	394	anasss 677	. . . . . . 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 4585	. . . . . . . 8 ⊢ (𝑟 = ^◡ ≤ → (0𝑟((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ↔ 0^◡ ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
398		fvex 6113	. . . . . . . . 9 ⊢ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∈ V
399	34, 398	brcnv 5227	. . . . . . . 8 ⊢ (0^◡ ≤ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ↔ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0)
400	397, 399	syl6bb 275	. . . . . . 7 ⊢ (𝑟 = ^◡ ≤ → (0𝑟((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ↔ ((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
401	400	rexbidv 3034	. . . . . 6 ⊢ (𝑟 = ^◡ ≤ → (∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ↔ ∃𝑗 ∈ (0...𝑁)((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ≤ 0))
402	396, 401	syl5ibrcom 236	. . . . 5 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → (𝑟 = ^◡ ≤ → ∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
403	78, 402	jaod 394	. . . 4 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → ((𝑟 = ≤ ∨ 𝑟 = ^◡ ≤ ) → ∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
404	1, 403	syl5 33	. . 3 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁))) → (𝑟 ∈ { ≤ , ^◡ ≤ } → ∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
405	404	exp32 629	. 2 ⊢ (𝜑 → (𝑘 ∈ ℕ → (𝑛 ∈ (1...𝑁) → (𝑟 ∈ { ≤ , ^◡ ≤ } → ∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))))
406	405	3imp2 1274	1 ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ^◡ ≤ })) → ∃𝑗 ∈ (0...𝑁)0𝑟((𝐹‘(𝑃 ∘_𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∨ wo 382 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 {cab 2596 ≠ wne 2780 ∀wral 2896 ∃wrex 2897 {crab 2900 Vcvv 3173 ∪ cun 3538 ∩ cin 3539 ⊆ wss 3540 ∅c0 3874 {csn 4125 {cpr 4127 ∪ cuni 4372 class class class wbr 4583 Or wor 4958 × cxp 5036 ^◡ccnv 5037 ran crn 5039 “ cima 5041 Fun wfun 5798 Fn wfn 5799 ⟶wf 5800 –onto→wfo 5802 –1-1-onto→wf1o 5803 ‘cfv 5804 (class class class)co 6549 ∘_𝑓 cof 6793 1^st c1st 7057 2^nd c2nd 7058 ↑_𝑚 cmap 7744 Fincfn 7841 supcsup 8229 ℂcc 9813 ℝcr 9814 0cc0 9815 1c1 9816 + caddc 9818 · cmul 9820 < clt 9953 ≤ cle 9954 − cmin 10145 / cdiv 10563 ℕcn 10897 ℕ₀cn0 11169 ℤcz 11254 ℤ_≥cuz 11563 ℝ⁺crp 11708 (,)cioo 12046 [,]cicc 12049 ...cfz 12197 ..^cfzo 12334 ↾_t crest 15904 topGenctg 15921 ∏_tcpt 15922 Topctop 20517 Cn ccn 20838

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-of 6795 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-map 7746 df-ixp 7795 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-fi 8200 df-sup 8231 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-n0 11170 df-z 11255 df-uz 11564 df-rp 11709 df-ioo 12050 df-icc 12053 df-fz 12198 df-fzo 12335 df-rest 15906 df-topgen 15927 df-pt 15928 df-top 20521 df-bases 20522 df-topon 20523 df-cn 20841

This theorem is referenced by: poimirlem32 32611

W3C validator