poimirlem31

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

	Ref	Expression
Hypotheses	poimir.0	$⊢ φ \to N \in ℕ$
	poimir.i	$⊢ I = {[0, 1]}^{(1 \dots N)}$
	poimir.r	$⊢ R = \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.))\})$
	poimir.1	$⊢ φ \to F \in ((R ↾_{𝑡} I) Cn R)$
	poimir.2	$⊢ (φ \land (n \in (1 \dots N) \land z \in I \land z (n) = 0)) \to F (z) (n) \leq 0$
	poimirlem31.p	$⊢ P = 1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))$
	poimirlem31.3	$⊢ φ \to G : ℕ ⟶ ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
	poimirlem31.4	$⊢ (φ \land k \in ℕ) \to ran 1^{st} (G (k)) \subseteq (0 ..^k)$
	poimirlem31.5	$⊢ (φ \land (k \in ℕ \land i \in (0 \dots N))) \to \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <)$
Assertion	poimirlem31	$⊢ (φ \land (k \in ℕ \land n \in (1 \dots N) \land r \in \{\leq \leq^{-1}\})) \to \exists j \in (0 \dots N) 0 r F (P \div_{f} ((1 \dots N) \times \{k\})) (n)$

Proof

Step	Hyp	Ref	Expression
1		poimir.0	$⊢ φ \to N \in ℕ$
2		poimir.i	$⊢ I = {[0, 1]}^{(1 \dots N)}$
3		poimir.r	$⊢ R = \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.))\})$
4		poimir.1	$⊢ φ \to F \in ((R ↾_{𝑡} I) Cn R)$
5		poimir.2	$⊢ (φ \land (n \in (1 \dots N) \land z \in I \land z (n) = 0)) \to F (z) (n) \leq 0$
6		poimirlem31.p	$⊢ P = 1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))$
7		poimirlem31.3	$⊢ φ \to G : ℕ ⟶ ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
8		poimirlem31.4	$⊢ (φ \land k \in ℕ) \to ran 1^{st} (G (k)) \subseteq (0 ..^k)$
9		poimirlem31.5	$⊢ (φ \land (k \in ℕ \land i \in (0 \dots N))) \to \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <)$
10		elpri	$⊢ r \in \{\leq \leq^{-1}\} \to (r = \leq \lor r = \leq^{-1})$
11		simprr	$⊢ (φ \land (k \in ℕ \land n \in (1 \dots N))) \to n \in (1 \dots N)$
12		fz1ssfz0	$⊢ (1 \dots N) \subseteq (0 \dots N)$
13	12	sseli	$⊢ n \in (1 \dots N) \to n \in (0 \dots N)$
14	13	anim2i	$⊢ (k \in ℕ \land n \in (1 \dots N)) \to (k \in ℕ \land n \in (0 \dots N))$
15		eleq1	$⊢ i = n \to (i \in (0 \dots N) \leftrightarrow n \in (0 \dots N))$
16	15	anbi2d	$⊢ i = n \to ((k \in ℕ \land i \in (0 \dots N)) \leftrightarrow (k \in ℕ \land n \in (0 \dots N)))$
17	16	anbi2d	$⊢ i = n \to ((φ \land (k \in ℕ \land i \in (0 \dots N))) \leftrightarrow (φ \land (k \in ℕ \land n \in (0 \dots N))))$
18		eqeq1	$⊢ i = n \to (i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \leftrightarrow n = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <))$
19	18	rexbidv	$⊢ i = n \to (\exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \leftrightarrow \exists j \in (0 \dots N) n = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <))$
20	17 19	imbi12d	$⊢ i = n \to (((φ \land (k \in ℕ \land i \in (0 \dots N))) \to \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <)) \leftrightarrow ((φ \land (k \in ℕ \land n \in (0 \dots N))) \to \exists j \in (0 \dots N) n = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <)))$
21	20 9	chvarvv	$⊢ (φ \land (k \in ℕ \land n \in (0 \dots N))) \to \exists j \in (0 \dots N) n = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <)$
22		elfzle1	$⊢ n \in (1 \dots N) \to 1 \leq n$
23		1re	$⊢ 1 \in ℝ$
24		elfzelz	$⊢ n \in (1 \dots N) \to n \in ℤ$
25	24	zred	$⊢ n \in (1 \dots N) \to n \in ℝ$
26		lenlt	$⊢ (1 \in ℝ \land n \in ℝ) \to (1 \leq n \leftrightarrow \neg n < 1)$
27	23 25 26	sylancr	$⊢ n \in (1 \dots N) \to (1 \leq n \leftrightarrow \neg n < 1)$
28	22 27	mpbid	$⊢ n \in (1 \dots N) \to \neg n < 1$
29		elsni	$⊢ n \in \{0\} \to n = 0$
30		0lt1	$⊢ 0 < 1$
31	29 30	eqbrtrdi	$⊢ n \in \{0\} \to n < 1$
32	28 31	nsyl	$⊢ n \in (1 \dots N) \to \neg n \in \{0\}$
33		ltso	$⊢ < Or ℝ$
34		snfi	$⊢ \{0\} \in Fin$
35		fzfi	$⊢ (1 \dots N) \in Fin$
36		rabfi	$⊢ (1 \dots N) \in Fin \to \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} \in Fin$
37	35 36	ax-mp	$⊢ \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} \in Fin$
38		unfi	$⊢ (\{0\} \in Fin \land \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} \in Fin) \to \{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} \in Fin$
39	34 37 38	mp2an	$⊢ \{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} \in Fin$
40		c0ex	$⊢ 0 \in V$
41	40	snid	$⊢ 0 \in \{0\}$
42		elun1	$⊢ 0 \in \{0\} \to 0 \in (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\})$
43		ne0i	$⊢ 0 \in (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\}) \to \{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} \neq \emptyset$
44	41 42 43	mp2b	$⊢ \{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} \neq \emptyset$
45		0re	$⊢ 0 \in ℝ$
46		snssi	$⊢ 0 \in ℝ \to \{0\} \subseteq ℝ$
47	45 46	ax-mp	$⊢ \{0\} \subseteq ℝ$
48		ssrab2	$⊢ \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} \subseteq (1 \dots N)$
49	24	ssriv	$⊢ (1 \dots N) \subseteq ℤ$
50		zssre	$⊢ ℤ \subseteq ℝ$
51	49 50	sstri	$⊢ (1 \dots N) \subseteq ℝ$
52	48 51	sstri	$⊢ \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} \subseteq ℝ$
53	47 52	unssi	$⊢ \{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} \subseteq ℝ$
54	39 44 53	3pm3.2i	$⊢ (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} \in Fin \land \{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} \neq \emptyset \land \{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} \subseteq ℝ)$
55		fisupcl	$⊢ (< Or ℝ \land (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} \in Fin \land \{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} \neq \emptyset \land \{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} \subseteq ℝ)) \to sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \in (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\})$
56	33 54 55	mp2an	$⊢ sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \in (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\})$
57		eleq1	$⊢ n = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \to (n \in (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\}) \leftrightarrow sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \in (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\}))$
58	56 57	mpbiri	$⊢ n = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \to n \in (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\})$
59		elun	$⊢ n \in (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\}) \leftrightarrow (n \in \{0\} \lor n \in \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\})$
60	58 59	sylib	$⊢ n = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \to (n \in \{0\} \lor n \in \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\})$
61		oveq2	$⊢ a = n \to (1 \dots a) = (1 \dots n)$
62	61	raleqdv	$⊢ a = n \to (\forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0) \leftrightarrow \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))$
63	62	elrab	$⊢ n \in \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} \leftrightarrow (n \in (1 \dots N) \land \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))$
64		elfzuz	$⊢ n \in (1 \dots N) \to n \in ℤ_{\geq 1}$
65		eluzfz2	$⊢ n \in ℤ_{\geq 1} \to n \in (1 \dots n)$
66	64 65	syl	$⊢ n \in (1 \dots N) \to n \in (1 \dots n)$
67		simpl	$⊢ (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0) \to 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b)$
68	67	ralimi	$⊢ \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0) \to \forall b \in (1 \dots n) 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b)$
69		fveq2	$⊢ b = n \to F (P \div_{f} ((1 \dots N) \times \{k\})) (b) = F (P \div_{f} ((1 \dots N) \times \{k\})) (n)$
70	69	breq2d	$⊢ b = n \to (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \leftrightarrow 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n))$
71	70	rspcva	$⊢ (n \in (1 \dots n) \land \forall b \in (1 \dots n) 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b)) \to 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n)$
72	66 68 71	syl2an	$⊢ (n \in (1 \dots N) \land \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)) \to 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n)$
73	63 72	sylbi	$⊢ n \in \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} \to 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n)$
74	73	orim2i	$⊢ (n \in \{0\} \lor n \in \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\}) \to (n \in \{0\} \lor 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n))$
75	60 74	syl	$⊢ n = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \to (n \in \{0\} \lor 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n))$
76		orel1	$⊢ \neg n \in \{0\} \to ((n \in \{0\} \lor 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n)) \to 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n))$
77	32 75 76	syl2im	$⊢ n \in (1 \dots N) \to (n = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \to 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n))$
78	77	reximdv	$⊢ n \in (1 \dots N) \to (\exists j \in (0 \dots N) n = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \to \exists j \in (0 \dots N) 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n))$
79	21 78	syl5	$⊢ n \in (1 \dots N) \to ((φ \land (k \in ℕ \land n \in (0 \dots N))) \to \exists j \in (0 \dots N) 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n))$
80	14 79	sylan2i	$⊢ n \in (1 \dots N) \to ((φ \land (k \in ℕ \land n \in (1 \dots N))) \to \exists j \in (0 \dots N) 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n))$
81	11 80	mpcom	$⊢ (φ \land (k \in ℕ \land n \in (1 \dots N))) \to \exists j \in (0 \dots N) 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n)$
82		breq	$⊢ r = \leq \to (0 r F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \leftrightarrow 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n))$
83	82	rexbidv	$⊢ r = \leq \to (\exists j \in (0 \dots N) 0 r F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \leftrightarrow \exists j \in (0 \dots N) 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n))$
84	81 83	syl5ibrcom	$⊢ (φ \land (k \in ℕ \land n \in (1 \dots N))) \to (r = \leq \to \exists j \in (0 \dots N) 0 r F (P \div_{f} ((1 \dots N) \times \{k\})) (n))$
85	1	nnzd	$⊢ φ \to N \in ℤ$
86		elfzm1b	$⊢ (n \in ℤ \land N \in ℤ) \to (n \in (1 \dots N) \leftrightarrow n - 1 \in (0 \dots N - 1))$
87	24 85 86	syl2anr	$⊢ (φ \land n \in (1 \dots N)) \to (n \in (1 \dots N) \leftrightarrow n - 1 \in (0 \dots N - 1))$
88	87	biimpd	$⊢ (φ \land n \in (1 \dots N)) \to (n \in (1 \dots N) \to n - 1 \in (0 \dots N - 1))$
89	88	ex	$⊢ φ \to (n \in (1 \dots N) \to (n \in (1 \dots N) \to n - 1 \in (0 \dots N - 1)))$
90	89	pm2.43d	$⊢ φ \to (n \in (1 \dots N) \to n - 1 \in (0 \dots N - 1))$
91	1	nncnd	$⊢ φ \to N \in ℂ$
92		npcan1	$⊢ N \in ℂ \to N - 1 + 1 = N$
93	91 92	syl	$⊢ φ \to N - 1 + 1 = N$
94		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
95	1 94	syl	$⊢ φ \to N - 1 \in ℕ_{0}$
96	95	nn0zd	$⊢ φ \to N - 1 \in ℤ$
97		uzid	$⊢ N - 1 \in ℤ \to N - 1 \in ℤ_{\geq (N - 1)}$
98		peano2uz	$⊢ N - 1 \in ℤ_{\geq (N - 1)} \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
99	96 97 98	3syl	$⊢ φ \to N - 1 + 1 \in ℤ_{\geq (N - 1)}$
100	93 99	eqeltrrd	$⊢ φ \to N \in ℤ_{\geq (N - 1)}$
101		fzss2	$⊢ N \in ℤ_{\geq (N - 1)} \to (0 \dots N - 1) \subseteq (0 \dots N)$
102	100 101	syl	$⊢ φ \to (0 \dots N - 1) \subseteq (0 \dots N)$
103	102	sseld	$⊢ φ \to (n - 1 \in (0 \dots N - 1) \to n - 1 \in (0 \dots N))$
104	90 103	syld	$⊢ φ \to (n \in (1 \dots N) \to n - 1 \in (0 \dots N))$
105	104	anim2d	$⊢ φ \to ((k \in ℕ \land n \in (1 \dots N)) \to (k \in ℕ \land n - 1 \in (0 \dots N)))$
106	105	imp	$⊢ (φ \land (k \in ℕ \land n \in (1 \dots N))) \to (k \in ℕ \land n - 1 \in (0 \dots N))$
107		ovex	$⊢ n - 1 \in V$
108		eleq1	$⊢ i = n - 1 \to (i \in (0 \dots N) \leftrightarrow n - 1 \in (0 \dots N))$
109	108	anbi2d	$⊢ i = n - 1 \to ((k \in ℕ \land i \in (0 \dots N)) \leftrightarrow (k \in ℕ \land n - 1 \in (0 \dots N)))$
110	109	anbi2d	$⊢ i = n - 1 \to ((φ \land (k \in ℕ \land i \in (0 \dots N))) \leftrightarrow (φ \land (k \in ℕ \land n - 1 \in (0 \dots N))))$
111		eqeq1	$⊢ i = n - 1 \to (i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \leftrightarrow n - 1 = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <))$
112	111	rexbidv	$⊢ i = n - 1 \to (\exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \leftrightarrow \exists j \in (0 \dots N) n - 1 = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <))$
113	110 112	imbi12d	$⊢ i = n - 1 \to (((φ \land (k \in ℕ \land i \in (0 \dots N))) \to \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <)) \leftrightarrow ((φ \land (k \in ℕ \land n - 1 \in (0 \dots N))) \to \exists j \in (0 \dots N) n - 1 = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <)))$
114	107 113 9	vtocl	$⊢ (φ \land (k \in ℕ \land n - 1 \in (0 \dots N))) \to \exists j \in (0 \dots N) n - 1 = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <)$
115	106 114	syldan	$⊢ (φ \land (k \in ℕ \land n \in (1 \dots N))) \to \exists j \in (0 \dots N) n - 1 = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <)$
116		eleq1	$⊢ n - 1 = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \to (n - 1 \in (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\}) \leftrightarrow sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \in (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\}))$
117	56 116	mpbiri	$⊢ n - 1 = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \to n - 1 \in (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\})$
118		elun	$⊢ n - 1 \in (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\}) \leftrightarrow (n - 1 \in \{0\} \lor n - 1 \in \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\})$
119	107	elsn	$⊢ n - 1 \in \{0\} \leftrightarrow n - 1 = 0$
120		oveq2	$⊢ a = n - 1 \to (1 \dots a) = (1 \dots n - 1)$
121	120	raleqdv	$⊢ a = n - 1 \to (\forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0) \leftrightarrow \forall b \in (1 \dots n - 1) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))$
122	121	elrab	$⊢ n - 1 \in \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} \leftrightarrow (n - 1 \in (1 \dots N) \land \forall b \in (1 \dots n - 1) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))$
123	119 122	orbi12i	$⊢ (n - 1 \in \{0\} \lor n - 1 \in \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\}) \leftrightarrow (n - 1 = 0 \lor (n - 1 \in (1 \dots N) \land \forall b \in (1 \dots n - 1) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)))$
124	118 123	bitri	$⊢ n - 1 \in (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\}) \leftrightarrow (n - 1 = 0 \lor (n - 1 \in (1 \dots N) \land \forall b \in (1 \dots n - 1) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)))$
125	117 124	sylib	$⊢ n - 1 = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \to (n - 1 = 0 \lor (n - 1 \in (1 \dots N) \land \forall b \in (1 \dots n - 1) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)))$
126	125	a1i	$⊢ n \in (1 \dots N) \to (n - 1 = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \to (n - 1 = 0 \lor (n - 1 \in (1 \dots N) \land \forall b \in (1 \dots n - 1) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))))$
127		ltm1	$⊢ n \in ℝ \to n - 1 < n$
128		peano2rem	$⊢ n \in ℝ \to n - 1 \in ℝ$
129		ltnle	$⊢ (n - 1 \in ℝ \land n \in ℝ) \to (n - 1 < n \leftrightarrow \neg n \leq n - 1)$
130	128 129	mpancom	$⊢ n \in ℝ \to (n - 1 < n \leftrightarrow \neg n \leq n - 1)$
131	127 130	mpbid	$⊢ n \in ℝ \to \neg n \leq n - 1$
132	25 131	syl	$⊢ n \in (1 \dots N) \to \neg n \leq n - 1$
133		breq2	$⊢ n - 1 = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \to (n \leq n - 1 \leftrightarrow n \leq sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <))$
134	133	notbid	$⊢ n - 1 = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \to (\neg n \leq n - 1 \leftrightarrow \neg n \leq sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <))$
135	132 134	syl5ibcom	$⊢ n \in (1 \dots N) \to (n - 1 = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \to \neg n \leq sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <))$
136		elun2	$⊢ n \in \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} \to n \in (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\})$
137		fimaxre2	$⊢ (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} \subseteq ℝ \land \{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} \in Fin) \to \exists x \in ℝ \forall y \in (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\}) y \leq x$
138	53 39 137	mp2an	$⊢ \exists x \in ℝ \forall y \in (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\}) y \leq x$
139	53 44 138	3pm3.2i	$⊢ (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} \subseteq ℝ \land \{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} \neq \emptyset \land \exists x \in ℝ \forall y \in (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\}) y \leq x)$
140	139	suprubii	$⊢ n \in (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\}) \to n \leq sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <)$
141	136 140	syl	$⊢ n \in \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} \to n \leq sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <)$
142	141	con3i	$⊢ \neg n \leq sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \to \neg n \in \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\}$
143		ianor	$⊢ \neg (n \in (1 \dots N) \land \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)) \leftrightarrow (\neg n \in (1 \dots N) \lor \neg \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))$
144	143 63	xchnxbir	$⊢ \neg n \in \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} \leftrightarrow (\neg n \in (1 \dots N) \lor \neg \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))$
145	142 144	sylib	$⊢ \neg n \leq sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \to (\neg n \in (1 \dots N) \lor \neg \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))$
146	135 145	syl6	$⊢ n \in (1 \dots N) \to (n - 1 = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \to (\neg n \in (1 \dots N) \lor \neg \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)))$
147		pm2.63	$⊢ (n \in (1 \dots N) \lor \neg \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)) \to ((\neg n \in (1 \dots N) \lor \neg \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)) \to \neg \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))$
148	147	orcs	$⊢ n \in (1 \dots N) \to ((\neg n \in (1 \dots N) \lor \neg \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)) \to \neg \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))$
149	146 148	syld	$⊢ n \in (1 \dots N) \to (n - 1 = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \to \neg \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))$
150	126 149	jcad	$⊢ n \in (1 \dots N) \to (n - 1 = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \to ((n - 1 = 0 \lor (n - 1 \in (1 \dots N) \land \forall b \in (1 \dots n - 1) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))) \land \neg \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)))$
151		andir	$⊢ ((n - 1 = 0 \lor (n - 1 \in (1 \dots N) \land \forall b \in (1 \dots n - 1) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))) \land \neg \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)) \leftrightarrow ((n - 1 = 0 \land \neg \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)) \lor ((n - 1 \in (1 \dots N) \land \forall b \in (1 \dots n - 1) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)) \land \neg \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)))$
152	24	zcnd	$⊢ n \in (1 \dots N) \to n \in ℂ$
153		ax-1cn	$⊢ 1 \in ℂ$
154		0cn	$⊢ 0 \in ℂ$
155		subadd	$⊢ (n \in ℂ \land 1 \in ℂ \land 0 \in ℂ) \to (n - 1 = 0 \leftrightarrow 1 + 0 = n)$
156	153 154 155	mp3an23	$⊢ n \in ℂ \to (n - 1 = 0 \leftrightarrow 1 + 0 = n)$
157	152 156	syl	$⊢ n \in (1 \dots N) \to (n - 1 = 0 \leftrightarrow 1 + 0 = n)$
158	157	biimpa	$⊢ (n \in (1 \dots N) \land n - 1 = 0) \to 1 + 0 = n$
159		1p0e1	$⊢ 1 + 0 = 1$
160	158 159	eqtr3di	$⊢ (n \in (1 \dots N) \land n - 1 = 0) \to n = 1$
161		1z	$⊢ 1 \in ℤ$
162		fzsn	$⊢ 1 \in ℤ \to (1 \dots 1) = \{1\}$
163	161 162	ax-mp	$⊢ (1 \dots 1) = \{1\}$
164		oveq2	$⊢ n = 1 \to (1 \dots n) = (1 \dots 1)$
165		sneq	$⊢ n = 1 \to \{n\} = \{1\}$
166	163 164 165	3eqtr4a	$⊢ n = 1 \to (1 \dots n) = \{n\}$
167	166	raleqdv	$⊢ n = 1 \to (\forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0) \leftrightarrow \forall b \in \{n\} (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))$
168	167	notbid	$⊢ n = 1 \to (\neg \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0) \leftrightarrow \neg \forall b \in \{n\} (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))$
169	168	biimpd	$⊢ n = 1 \to (\neg \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0) \to \neg \forall b \in \{n\} (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))$
170	160 169	syl	$⊢ (n \in (1 \dots N) \land n - 1 = 0) \to (\neg \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0) \to \neg \forall b \in \{n\} (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))$
171	170	expimpd	$⊢ n \in (1 \dots N) \to ((n - 1 = 0 \land \neg \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)) \to \neg \forall b \in \{n\} (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))$
172		ralun	$⊢ (\forall b \in (1 \dots n - 1) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0) \land \forall b \in \{n\} (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)) \to \forall b \in ((1 \dots n - 1) \cup \{n\}) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)$
173		npcan1	$⊢ n \in ℂ \to n - 1 + 1 = n$
174	152 173	syl	$⊢ n \in (1 \dots N) \to n - 1 + 1 = n$
175	174 64	eqeltrd	$⊢ n \in (1 \dots N) \to n - 1 + 1 \in ℤ_{\geq 1}$
176		peano2zm	$⊢ n \in ℤ \to n - 1 \in ℤ$
177		uzid	$⊢ n - 1 \in ℤ \to n - 1 \in ℤ_{\geq (n - 1)}$
178		peano2uz	$⊢ n - 1 \in ℤ_{\geq (n - 1)} \to n - 1 + 1 \in ℤ_{\geq (n - 1)}$
179	24 176 177 178	4syl	$⊢ n \in (1 \dots N) \to n - 1 + 1 \in ℤ_{\geq (n - 1)}$
180	174 179	eqeltrrd	$⊢ n \in (1 \dots N) \to n \in ℤ_{\geq (n - 1)}$
181		fzsplit2	$⊢ (n - 1 + 1 \in ℤ_{\geq 1} \land n \in ℤ_{\geq (n - 1)}) \to (1 \dots n) = (1 \dots n - 1) \cup (n - 1 + 1 \dots n)$
182	175 180 181	syl2anc	$⊢ n \in (1 \dots N) \to (1 \dots n) = (1 \dots n - 1) \cup (n - 1 + 1 \dots n)$
183	174	oveq1d	$⊢ n \in (1 \dots N) \to (n - 1 + 1 \dots n) = (n \dots n)$
184		fzsn	$⊢ n \in ℤ \to (n \dots n) = \{n\}$
185	24 184	syl	$⊢ n \in (1 \dots N) \to (n \dots n) = \{n\}$
186	183 185	eqtrd	$⊢ n \in (1 \dots N) \to (n - 1 + 1 \dots n) = \{n\}$
187	186	uneq2d	$⊢ n \in (1 \dots N) \to (1 \dots n - 1) \cup (n - 1 + 1 \dots n) = (1 \dots n - 1) \cup \{n\}$
188	182 187	eqtrd	$⊢ n \in (1 \dots N) \to (1 \dots n) = (1 \dots n - 1) \cup \{n\}$
189	188	raleqdv	$⊢ n \in (1 \dots N) \to (\forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0) \leftrightarrow \forall b \in ((1 \dots n - 1) \cup \{n\}) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))$
190	172 189	syl5ibr	$⊢ n \in (1 \dots N) \to ((\forall b \in (1 \dots n - 1) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0) \land \forall b \in \{n\} (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)) \to \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))$
191	190	expdimp	$⊢ (n \in (1 \dots N) \land \forall b \in (1 \dots n - 1) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)) \to (\forall b \in \{n\} (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0) \to \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))$
192	191	con3d	$⊢ (n \in (1 \dots N) \land \forall b \in (1 \dots n - 1) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)) \to (\neg \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0) \to \neg \forall b \in \{n\} (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))$
193	192	adantrl	$⊢ (n \in (1 \dots N) \land (n - 1 \in (1 \dots N) \land \forall b \in (1 \dots n - 1) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))) \to (\neg \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0) \to \neg \forall b \in \{n\} (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))$
194	193	expimpd	$⊢ n \in (1 \dots N) \to (((n - 1 \in (1 \dots N) \land \forall b \in (1 \dots n - 1) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)) \land \neg \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)) \to \neg \forall b \in \{n\} (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))$
195	171 194	jaod	$⊢ n \in (1 \dots N) \to (((n - 1 = 0 \land \neg \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)) \lor ((n - 1 \in (1 \dots N) \land \forall b \in (1 \dots n - 1) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)) \land \neg \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))) \to \neg \forall b \in \{n\} (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))$
196	151 195	syl5bi	$⊢ n \in (1 \dots N) \to (((n - 1 = 0 \lor (n - 1 \in (1 \dots N) \land \forall b \in (1 \dots n - 1) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))) \land \neg \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)) \to \neg \forall b \in \{n\} (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))$
197		fveq2	$⊢ b = n \to P (b) = P (n)$
198	197	neeq1d	$⊢ b = n \to (P (b) \neq 0 \leftrightarrow P (n) \neq 0)$
199	70 198	anbi12d	$⊢ b = n \to ((0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0) \leftrightarrow (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \land P (n) \neq 0))$
200	199	ralsng	$⊢ n \in (1 \dots N) \to (\forall b \in \{n\} (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0) \leftrightarrow (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \land P (n) \neq 0))$
201	200	notbid	$⊢ n \in (1 \dots N) \to (\neg \forall b \in \{n\} (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0) \leftrightarrow \neg (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \land P (n) \neq 0))$
202		ianor	$⊢ \neg (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \land P (n) \neq 0) \leftrightarrow (\neg 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \lor \neg P (n) \neq 0)$
203		nne	$⊢ \neg P (n) \neq 0 \leftrightarrow P (n) = 0$
204	203	orbi2i	$⊢ (\neg 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \lor \neg P (n) \neq 0) \leftrightarrow (\neg 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \lor P (n) = 0)$
205	202 204	bitri	$⊢ \neg (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \land P (n) \neq 0) \leftrightarrow (\neg 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \lor P (n) = 0)$
206	201 205	bitrdi	$⊢ n \in (1 \dots N) \to (\neg \forall b \in \{n\} (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0) \leftrightarrow (\neg 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \lor P (n) = 0))$
207	196 206	sylibd	$⊢ n \in (1 \dots N) \to (((n - 1 = 0 \lor (n - 1 \in (1 \dots N) \land \forall b \in (1 \dots n - 1) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0))) \land \neg \forall b \in (1 \dots n) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)) \to (\neg 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \lor P (n) = 0))$
208	150 207	syld	$⊢ n \in (1 \dots N) \to (n - 1 = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \to (\neg 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \lor P (n) = 0))$
209	208	ad2antlr	$⊢ (((φ \land k \in ℕ) \land n \in (1 \dots N)) \land j \in (0 \dots N)) \to (n - 1 = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \to (\neg 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \lor P (n) = 0))$
210		retop	$⊢ topGen (ran (.)) \in Top$
211	210	fconst6	$⊢ ((1 \dots N) \times \{topGen (ran (.))\}) : (1 \dots N) ⟶ Top$
212		pttop	$⊢ ((1 \dots N) \in Fin \land ((1 \dots N) \times \{topGen (ran (.))\}) : (1 \dots N) ⟶ Top) \to \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.))\}) \in Top$
213	35 211 212	mp2an	$⊢ \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.))\}) \in Top$
214	3 213	eqeltri	$⊢ R \in Top$
215		reex	$⊢ ℝ \in V$
216		unitssre	$⊢ [0, 1] \subseteq ℝ$
217		mapss	$⊢ (ℝ \in V \land [0, 1] \subseteq ℝ) \to {[0, 1]}^{(1 \dots N)} \subseteq ℝ^{(1 \dots N)}$
218	215 216 217	mp2an	$⊢ {[0, 1]}^{(1 \dots N)} \subseteq ℝ^{(1 \dots N)}$
219	2 218	eqsstri	$⊢ I \subseteq ℝ^{(1 \dots N)}$
220		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
221	3 220	ptuniconst	$⊢ ((1 \dots N) \in Fin \land topGen (ran (.)) \in Top) \to ℝ^{(1 \dots N)} = ⋃ R$
222	35 210 221	mp2an	$⊢ ℝ^{(1 \dots N)} = ⋃ R$
223	222	restuni	$⊢ (R \in Top \land I \subseteq ℝ^{(1 \dots N)}) \to I = ⋃ (R ↾_{𝑡} I)$
224	214 219 223	mp2an	$⊢ I = ⋃ (R ↾_{𝑡} I)$
225	224 222	cnf	$⊢ F \in ((R ↾_{𝑡} I) Cn R) \to F : I ⟶ ℝ^{(1 \dots N)}$
226	4 225	syl	$⊢ φ \to F : I ⟶ ℝ^{(1 \dots N)}$
227	226	ad2antrr	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to F : I ⟶ ℝ^{(1 \dots N)}$
228		simplr	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to k \in ℕ$
229		elfzelz	$⊢ x \in (0 \dots k) \to x \in ℤ$
230	229	zred	$⊢ x \in (0 \dots k) \to x \in ℝ$
231	230	adantr	$⊢ (x \in (0 \dots k) \land k \in ℕ) \to x \in ℝ$
232		nnre	$⊢ k \in ℕ \to k \in ℝ$
233	232	adantl	$⊢ (x \in (0 \dots k) \land k \in ℕ) \to k \in ℝ$
234		nnne0	$⊢ k \in ℕ \to k \neq 0$
235	234	adantl	$⊢ (x \in (0 \dots k) \land k \in ℕ) \to k \neq 0$
236	231 233 235	redivcld	$⊢ (x \in (0 \dots k) \land k \in ℕ) \to \frac{x}{k} \in ℝ$
237		elfzle1	$⊢ x \in (0 \dots k) \to 0 \leq x$
238	230 237	jca	$⊢ x \in (0 \dots k) \to (x \in ℝ \land 0 \leq x)$
239		nnrp	$⊢ k \in ℕ \to k \in ℝ^{+}$
240	239	rpregt0d	$⊢ k \in ℕ \to (k \in ℝ \land 0 < k)$
241		divge0	$⊢ ((x \in ℝ \land 0 \leq x) \land (k \in ℝ \land 0 < k)) \to 0 \leq \frac{x}{k}$
242	238 240 241	syl2an	$⊢ (x \in (0 \dots k) \land k \in ℕ) \to 0 \leq \frac{x}{k}$
243		elfzle2	$⊢ x \in (0 \dots k) \to x \leq k$
244	243	adantr	$⊢ (x \in (0 \dots k) \land k \in ℕ) \to x \leq k$
245		1red	$⊢ (x \in (0 \dots k) \land k \in ℕ) \to 1 \in ℝ$
246	239	adantl	$⊢ (x \in (0 \dots k) \land k \in ℕ) \to k \in ℝ^{+}$
247	231 245 246	ledivmuld	$⊢ (x \in (0 \dots k) \land k \in ℕ) \to (\frac{x}{k} \leq 1 \leftrightarrow x \leq k \cdot 1)$
248		nncn	$⊢ k \in ℕ \to k \in ℂ$
249	248	mulid1d	$⊢ k \in ℕ \to k \cdot 1 = k$
250	249	breq2d	$⊢ k \in ℕ \to (x \leq k \cdot 1 \leftrightarrow x \leq k)$
251	250	adantl	$⊢ (x \in (0 \dots k) \land k \in ℕ) \to (x \leq k \cdot 1 \leftrightarrow x \leq k)$
252	247 251	bitrd	$⊢ (x \in (0 \dots k) \land k \in ℕ) \to (\frac{x}{k} \leq 1 \leftrightarrow x \leq k)$
253	244 252	mpbird	$⊢ (x \in (0 \dots k) \land k \in ℕ) \to \frac{x}{k} \leq 1$
254		elicc01	$⊢ \frac{x}{k} \in [0, 1] \leftrightarrow (\frac{x}{k} \in ℝ \land 0 \leq \frac{x}{k} \land \frac{x}{k} \leq 1)$
255	236 242 253 254	syl3anbrc	$⊢ (x \in (0 \dots k) \land k \in ℕ) \to \frac{x}{k} \in [0, 1]$
256	255	ancoms	$⊢ (k \in ℕ \land x \in (0 \dots k)) \to \frac{x}{k} \in [0, 1]$
257		elsni	$⊢ y \in \{k\} \to y = k$
258	257	oveq2d	$⊢ y \in \{k\} \to \frac{x}{y} = \frac{x}{k}$
259	258	eleq1d	$⊢ y \in \{k\} \to (\frac{x}{y} \in [0, 1] \leftrightarrow \frac{x}{k} \in [0, 1])$
260	256 259	syl5ibrcom	$⊢ (k \in ℕ \land x \in (0 \dots k)) \to (y \in \{k\} \to \frac{x}{y} \in [0, 1])$
261	260	impr	$⊢ (k \in ℕ \land (x \in (0 \dots k) \land y \in \{k\})) \to \frac{x}{y} \in [0, 1]$
262	228 261	sylan	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land (x \in (0 \dots k) \land y \in \{k\})) \to \frac{x}{y} \in [0, 1]$
263		elun	$⊢ y \in (\{1\} \cup \{0\}) \leftrightarrow (y \in \{1\} \lor y \in \{0\})$
264		fzofzp1	$⊢ x \in (0 ..^k) \to x + 1 \in (0 \dots k)$
265		elsni	$⊢ y \in \{1\} \to y = 1$
266	265	oveq2d	$⊢ y \in \{1\} \to x + y = x + 1$
267	266	eleq1d	$⊢ y \in \{1\} \to (x + y \in (0 \dots k) \leftrightarrow x + 1 \in (0 \dots k))$
268	264 267	syl5ibrcom	$⊢ x \in (0 ..^k) \to (y \in \{1\} \to x + y \in (0 \dots k))$
269		elfzonn0	$⊢ x \in (0 ..^k) \to x \in ℕ_{0}$
270	269	nn0cnd	$⊢ x \in (0 ..^k) \to x \in ℂ$
271	270	addid1d	$⊢ x \in (0 ..^k) \to x + 0 = x$
272		elfzofz	$⊢ x \in (0 ..^k) \to x \in (0 \dots k)$
273	271 272	eqeltrd	$⊢ x \in (0 ..^k) \to x + 0 \in (0 \dots k)$
274		elsni	$⊢ y \in \{0\} \to y = 0$
275	274	oveq2d	$⊢ y \in \{0\} \to x + y = x + 0$
276	275	eleq1d	$⊢ y \in \{0\} \to (x + y \in (0 \dots k) \leftrightarrow x + 0 \in (0 \dots k))$
277	273 276	syl5ibrcom	$⊢ x \in (0 ..^k) \to (y \in \{0\} \to x + y \in (0 \dots k))$
278	268 277	jaod	$⊢ x \in (0 ..^k) \to ((y \in \{1\} \lor y \in \{0\}) \to x + y \in (0 \dots k))$
279	263 278	syl5bi	$⊢ x \in (0 ..^k) \to (y \in (\{1\} \cup \{0\}) \to x + y \in (0 \dots k))$
280	279	imp	$⊢ (x \in (0 ..^k) \land y \in (\{1\} \cup \{0\})) \to x + y \in (0 \dots k)$
281	280	adantl	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land (x \in (0 ..^k) \land y \in (\{1\} \cup \{0\}))) \to x + y \in (0 \dots k)$
282	7	ffvelrnda	$⊢ (φ \land k \in ℕ) \to G (k) \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
283		xp1st	$⊢ G (k) \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 1^{st} (G (k)) \in ({ℕ_{0}}^{(1 \dots N)})$
284		elmapfn	$⊢ 1^{st} (G (k)) \in ({ℕ_{0}}^{(1 \dots N)}) \to 1^{st} (G (k)) Fn (1 \dots N)$
285	282 283 284	3syl	$⊢ (φ \land k \in ℕ) \to 1^{st} (G (k)) Fn (1 \dots N)$
286		df-f	$⊢ 1^{st} (G (k)) : (1 \dots N) ⟶ (0 ..^k) \leftrightarrow (1^{st} (G (k)) Fn (1 \dots N) \land ran 1^{st} (G (k)) \subseteq (0 ..^k))$
287	285 8 286	sylanbrc	$⊢ (φ \land k \in ℕ) \to 1^{st} (G (k)) : (1 \dots N) ⟶ (0 ..^k)$
288	287	adantr	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to 1^{st} (G (k)) : (1 \dots N) ⟶ (0 ..^k)$
289		1ex	$⊢ 1 \in V$
290	289	fconst	$⊢ (2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) : 2^{nd} (G (k)) [(1 \dots j)] ⟶ \{1\}$
291	40	fconst	$⊢ (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}) : 2^{nd} (G (k)) [(j + 1 \dots N)] ⟶ \{0\}$
292	290 291	pm3.2i	$⊢ ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) : 2^{nd} (G (k)) [(1 \dots j)] ⟶ \{1\} \land (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}) : 2^{nd} (G (k)) [(j + 1 \dots N)] ⟶ \{0\})$
293		xp2nd	$⊢ G (k) \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 2^{nd} (G (k)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
294	282 293	syl	$⊢ (φ \land k \in ℕ) \to 2^{nd} (G (k)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
295		fvex	$⊢ 2^{nd} (G (k)) \in V$
296		f1oeq1	$⊢ f = 2^{nd} (G (k)) \to (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow 2^{nd} (G (k)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N))$
297	295 296	elab	$⊢ 2^{nd} (G (k)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \leftrightarrow 2^{nd} (G (k)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
298	294 297	sylib	$⊢ (φ \land k \in ℕ) \to 2^{nd} (G (k)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
299		dff1o3	$⊢ 2^{nd} (G (k)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow (2^{nd} (G (k)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \land Fun {2^{nd} (G (k))}^{-1})$
300	299	simprbi	$⊢ 2^{nd} (G (k)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to Fun {2^{nd} (G (k))}^{-1}$
301		imain	$⊢ Fun {2^{nd} (G (k))}^{-1} \to 2^{nd} (G (k)) [(1 \dots j) \cap (j + 1 \dots N)] = 2^{nd} (G (k)) [(1 \dots j)] \cap 2^{nd} (G (k)) [(j + 1 \dots N)]$
302	298 300 301	3syl	$⊢ (φ \land k \in ℕ) \to 2^{nd} (G (k)) [(1 \dots j) \cap (j + 1 \dots N)] = 2^{nd} (G (k)) [(1 \dots j)] \cap 2^{nd} (G (k)) [(j + 1 \dots N)]$
303		elfznn0	$⊢ j \in (0 \dots N) \to j \in ℕ_{0}$
304	303	nn0red	$⊢ j \in (0 \dots N) \to j \in ℝ$
305	304	ltp1d	$⊢ j \in (0 \dots N) \to j < j + 1$
306		fzdisj	$⊢ j < j + 1 \to (1 \dots j) \cap (j + 1 \dots N) = \emptyset$
307	305 306	syl	$⊢ j \in (0 \dots N) \to (1 \dots j) \cap (j + 1 \dots N) = \emptyset$
308	307	imaeq2d	$⊢ j \in (0 \dots N) \to 2^{nd} (G (k)) [(1 \dots j) \cap (j + 1 \dots N)] = 2^{nd} (G (k)) [\emptyset]$
309		ima0	$⊢ 2^{nd} (G (k)) [\emptyset] = \emptyset$
310	308 309	eqtrdi	$⊢ j \in (0 \dots N) \to 2^{nd} (G (k)) [(1 \dots j) \cap (j + 1 \dots N)] = \emptyset$
311	302 310	sylan9req	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to 2^{nd} (G (k)) [(1 \dots j)] \cap 2^{nd} (G (k)) [(j + 1 \dots N)] = \emptyset$
312		fun	$⊢ (((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) : 2^{nd} (G (k)) [(1 \dots j)] ⟶ \{1\} \land (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}) : 2^{nd} (G (k)) [(j + 1 \dots N)] ⟶ \{0\}) \land 2^{nd} (G (k)) [(1 \dots j)] \cap 2^{nd} (G (k)) [(j + 1 \dots N)] = \emptyset) \to ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) : 2^{nd} (G (k)) [(1 \dots j)] \cup 2^{nd} (G (k)) [(j + 1 \dots N)] ⟶ \{1\} \cup \{0\}$
313	292 311 312	sylancr	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) : 2^{nd} (G (k)) [(1 \dots j)] \cup 2^{nd} (G (k)) [(j + 1 \dots N)] ⟶ \{1\} \cup \{0\}$
314		imaundi	$⊢ 2^{nd} (G (k)) [(1 \dots j) \cup (j + 1 \dots N)] = 2^{nd} (G (k)) [(1 \dots j)] \cup 2^{nd} (G (k)) [(j + 1 \dots N)]$
315		nn0p1nn	$⊢ j \in ℕ_{0} \to j + 1 \in ℕ$
316	303 315	syl	$⊢ j \in (0 \dots N) \to j + 1 \in ℕ$
317		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
318	316 317	eleqtrdi	$⊢ j \in (0 \dots N) \to j + 1 \in ℤ_{\geq 1}$
319		elfzuz3	$⊢ j \in (0 \dots N) \to N \in ℤ_{\geq j}$
320		fzsplit2	$⊢ (j + 1 \in ℤ_{\geq 1} \land N \in ℤ_{\geq j}) \to (1 \dots N) = (1 \dots j) \cup (j + 1 \dots N)$
321	318 319 320	syl2anc	$⊢ j \in (0 \dots N) \to (1 \dots N) = (1 \dots j) \cup (j + 1 \dots N)$
322	321	imaeq2d	$⊢ j \in (0 \dots N) \to 2^{nd} (G (k)) [(1 \dots N)] = 2^{nd} (G (k)) [(1 \dots j) \cup (j + 1 \dots N)]$
323		f1ofo	$⊢ 2^{nd} (G (k)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (G (k)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N)$
324		foima	$⊢ 2^{nd} (G (k)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \to 2^{nd} (G (k)) [(1 \dots N)] = (1 \dots N)$
325	298 323 324	3syl	$⊢ (φ \land k \in ℕ) \to 2^{nd} (G (k)) [(1 \dots N)] = (1 \dots N)$
326	322 325	sylan9req	$⊢ (j \in (0 \dots N) \land (φ \land k \in ℕ)) \to 2^{nd} (G (k)) [(1 \dots j) \cup (j + 1 \dots N)] = (1 \dots N)$
327	326	ancoms	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to 2^{nd} (G (k)) [(1 \dots j) \cup (j + 1 \dots N)] = (1 \dots N)$
328	314 327	eqtr3id	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to 2^{nd} (G (k)) [(1 \dots j)] \cup 2^{nd} (G (k)) [(j + 1 \dots N)] = (1 \dots N)$
329	328	feq2d	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to (((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) : 2^{nd} (G (k)) [(1 \dots j)] \cup 2^{nd} (G (k)) [(j + 1 \dots N)] ⟶ \{1\} \cup \{0\} \leftrightarrow ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) : (1 \dots N) ⟶ \{1\} \cup \{0\})$
330	313 329	mpbid	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) : (1 \dots N) ⟶ \{1\} \cup \{0\}$
331		fzfid	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to (1 \dots N) \in Fin$
332		inidm	$⊢ (1 \dots N) \cap (1 \dots N) = (1 \dots N)$
333	281 288 330 331 331 332	off	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots k)$
334	6	feq1i	$⊢ P : (1 \dots N) ⟶ (0 \dots k) \leftrightarrow (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots k)$
335	333 334	sylibr	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to P : (1 \dots N) ⟶ (0 \dots k)$
336		vex	$⊢ k \in V$
337	336	fconst	$⊢ ((1 \dots N) \times \{k\}) : (1 \dots N) ⟶ \{k\}$
338	337	a1i	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to ((1 \dots N) \times \{k\}) : (1 \dots N) ⟶ \{k\}$
339	262 335 338 331 331 332	off	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to (P \div_{f} ((1 \dots N) \times \{k\})) : (1 \dots N) ⟶ [0, 1]$
340	2	eleq2i	$⊢ P \div_{f} ((1 \dots N) \times \{k\}) \in I \leftrightarrow P \div_{f} ((1 \dots N) \times \{k\}) \in ({[0, 1]}^{(1 \dots N)})$
341		ovex	$⊢ [0, 1] \in V$
342		ovex	$⊢ (1 \dots N) \in V$
343	341 342	elmap	$⊢ P \div_{f} ((1 \dots N) \times \{k\}) \in ({[0, 1]}^{(1 \dots N)}) \leftrightarrow (P \div_{f} ((1 \dots N) \times \{k\})) : (1 \dots N) ⟶ [0, 1]$
344	340 343	bitri	$⊢ P \div_{f} ((1 \dots N) \times \{k\}) \in I \leftrightarrow (P \div_{f} ((1 \dots N) \times \{k\})) : (1 \dots N) ⟶ [0, 1]$
345	339 344	sylibr	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to P \div_{f} ((1 \dots N) \times \{k\}) \in I$
346	227 345	ffvelrnd	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to F (P \div_{f} ((1 \dots N) \times \{k\})) \in (ℝ^{(1 \dots N)})$
347		elmapi	$⊢ F (P \div_{f} ((1 \dots N) \times \{k\})) \in (ℝ^{(1 \dots N)}) \to F (P \div_{f} ((1 \dots N) \times \{k\})) : (1 \dots N) ⟶ ℝ$
348	346 347	syl	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to F (P \div_{f} ((1 \dots N) \times \{k\})) : (1 \dots N) ⟶ ℝ$
349	348	ffvelrnda	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land n \in (1 \dots N)) \to F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \in ℝ$
350	349	an32s	$⊢ (((φ \land k \in ℕ) \land n \in (1 \dots N)) \land j \in (0 \dots N)) \to F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \in ℝ$
351		0red	$⊢ (((φ \land k \in ℕ) \land n \in (1 \dots N)) \land j \in (0 \dots N)) \to 0 \in ℝ$
352	350 351	ltnled	$⊢ (((φ \land k \in ℕ) \land n \in (1 \dots N)) \land j \in (0 \dots N)) \to (F (P \div_{f} ((1 \dots N) \times \{k\})) (n) < 0 \leftrightarrow \neg 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n))$
353		ltle	$⊢ (F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \in ℝ \land 0 \in ℝ) \to (F (P \div_{f} ((1 \dots N) \times \{k\})) (n) < 0 \to F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \leq 0)$
354	350 45 353	sylancl	$⊢ (((φ \land k \in ℕ) \land n \in (1 \dots N)) \land j \in (0 \dots N)) \to (F (P \div_{f} ((1 \dots N) \times \{k\})) (n) < 0 \to F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \leq 0)$
355	352 354	sylbird	$⊢ (((φ \land k \in ℕ) \land n \in (1 \dots N)) \land j \in (0 \dots N)) \to (\neg 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \to F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \leq 0)$
356	248 234	div0d	$⊢ k \in ℕ \to \frac{0}{k} = 0$
357		oveq1	$⊢ P (n) = 0 \to \frac{P (n)}{k} = \frac{0}{k}$
358	357	eqeq1d	$⊢ P (n) = 0 \to (\frac{P (n)}{k} = 0 \leftrightarrow \frac{0}{k} = 0)$
359	356 358	syl5ibrcom	$⊢ k \in ℕ \to (P (n) = 0 \to \frac{P (n)}{k} = 0)$
360	359	ad3antlr	$⊢ (((φ \land k \in ℕ) \land n \in (1 \dots N)) \land j \in (0 \dots N)) \to (P (n) = 0 \to \frac{P (n)}{k} = 0)$
361	335	ffnd	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to P Fn (1 \dots N)$
362		fnconstg	$⊢ k \in V \to ((1 \dots N) \times \{k\}) Fn (1 \dots N)$
363	336 362	mp1i	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to ((1 \dots N) \times \{k\}) Fn (1 \dots N)$
364		eqidd	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land n \in (1 \dots N)) \to P (n) = P (n)$
365	336	fvconst2	$⊢ n \in (1 \dots N) \to ((1 \dots N) \times \{k\}) (n) = k$
366	365	adantl	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land n \in (1 \dots N)) \to ((1 \dots N) \times \{k\}) (n) = k$
367	361 363 331 331 332 364 366	ofval	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land n \in (1 \dots N)) \to (P \div_{f} ((1 \dots N) \times \{k\})) (n) = \frac{P (n)}{k}$
368	367	an32s	$⊢ (((φ \land k \in ℕ) \land n \in (1 \dots N)) \land j \in (0 \dots N)) \to (P \div_{f} ((1 \dots N) \times \{k\})) (n) = \frac{P (n)}{k}$
369	368	eqeq1d	$⊢ (((φ \land k \in ℕ) \land n \in (1 \dots N)) \land j \in (0 \dots N)) \to ((P \div_{f} ((1 \dots N) \times \{k\})) (n) = 0 \leftrightarrow \frac{P (n)}{k} = 0)$
370	360 369	sylibrd	$⊢ (((φ \land k \in ℕ) \land n \in (1 \dots N)) \land j \in (0 \dots N)) \to (P (n) = 0 \to (P \div_{f} ((1 \dots N) \times \{k\})) (n) = 0)$
371		simplll	$⊢ (((φ \land k \in ℕ) \land n \in (1 \dots N)) \land j \in (0 \dots N)) \to φ$
372		simplr	$⊢ (((φ \land k \in ℕ) \land n \in (1 \dots N)) \land j \in (0 \dots N)) \to n \in (1 \dots N)$
373	345	adantlr	$⊢ (((φ \land k \in ℕ) \land n \in (1 \dots N)) \land j \in (0 \dots N)) \to P \div_{f} ((1 \dots N) \times \{k\}) \in I$
374		ovex	$⊢ P \div_{f} ((1 \dots N) \times \{k\}) \in V$
375		eleq1	$⊢ z = P \div_{f} ((1 \dots N) \times \{k\}) \to (z \in I \leftrightarrow P \div_{f} ((1 \dots N) \times \{k\}) \in I)$
376		fveq1	$⊢ z = P \div_{f} ((1 \dots N) \times \{k\}) \to z (n) = (P \div_{f} ((1 \dots N) \times \{k\})) (n)$
377	376	eqeq1d	$⊢ z = P \div_{f} ((1 \dots N) \times \{k\}) \to (z (n) = 0 \leftrightarrow (P \div_{f} ((1 \dots N) \times \{k\})) (n) = 0)$
378		fveq2	$⊢ z = P \div_{f} ((1 \dots N) \times \{k\}) \to F (z) = F (P \div_{f} ((1 \dots N) \times \{k\}))$
379	378	fveq1d	$⊢ z = P \div_{f} ((1 \dots N) \times \{k\}) \to F (z) (n) = F (P \div_{f} ((1 \dots N) \times \{k\})) (n)$
380	379	breq1d	$⊢ z = P \div_{f} ((1 \dots N) \times \{k\}) \to (F (z) (n) \leq 0 \leftrightarrow F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \leq 0)$
381	377 380	imbi12d	$⊢ z = P \div_{f} ((1 \dots N) \times \{k\}) \to ((z (n) = 0 \to F (z) (n) \leq 0) \leftrightarrow ((P \div_{f} ((1 \dots N) \times \{k\})) (n) = 0 \to F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \leq 0))$
382	375 381	imbi12d	$⊢ z = P \div_{f} ((1 \dots N) \times \{k\}) \to ((z \in I \to (z (n) = 0 \to F (z) (n) \leq 0)) \leftrightarrow (P \div_{f} ((1 \dots N) \times \{k\}) \in I \to ((P \div_{f} ((1 \dots N) \times \{k\})) (n) = 0 \to F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \leq 0)))$
383	382	imbi2d	$⊢ z = P \div_{f} ((1 \dots N) \times \{k\}) \to ((n \in (1 \dots N) \to (z \in I \to (z (n) = 0 \to F (z) (n) \leq 0))) \leftrightarrow (n \in (1 \dots N) \to (P \div_{f} ((1 \dots N) \times \{k\}) \in I \to ((P \div_{f} ((1 \dots N) \times \{k\})) (n) = 0 \to F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \leq 0))))$
384	383	imbi2d	$⊢ z = P \div_{f} ((1 \dots N) \times \{k\}) \to ((φ \to (n \in (1 \dots N) \to (z \in I \to (z (n) = 0 \to F (z) (n) \leq 0)))) \leftrightarrow (φ \to (n \in (1 \dots N) \to (P \div_{f} ((1 \dots N) \times \{k\}) \in I \to ((P \div_{f} ((1 \dots N) \times \{k\})) (n) = 0 \to F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \leq 0)))))$
385	5	3exp2	$⊢ φ \to (n \in (1 \dots N) \to (z \in I \to (z (n) = 0 \to F (z) (n) \leq 0)))$
386	374 384 385	vtocl	$⊢ φ \to (n \in (1 \dots N) \to (P \div_{f} ((1 \dots N) \times \{k\}) \in I \to ((P \div_{f} ((1 \dots N) \times \{k\})) (n) = 0 \to F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \leq 0)))$
387	371 372 373 386	syl3c	$⊢ (((φ \land k \in ℕ) \land n \in (1 \dots N)) \land j \in (0 \dots N)) \to ((P \div_{f} ((1 \dots N) \times \{k\})) (n) = 0 \to F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \leq 0)$
388	370 387	syld	$⊢ (((φ \land k \in ℕ) \land n \in (1 \dots N)) \land j \in (0 \dots N)) \to (P (n) = 0 \to F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \leq 0)$
389	355 388	jaod	$⊢ (((φ \land k \in ℕ) \land n \in (1 \dots N)) \land j \in (0 \dots N)) \to ((\neg 0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \lor P (n) = 0) \to F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \leq 0)$
390	209 389	syld	$⊢ (((φ \land k \in ℕ) \land n \in (1 \dots N)) \land j \in (0 \dots N)) \to (n - 1 = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \to F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \leq 0)$
391	390	reximdva	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots N)) \to (\exists j \in (0 \dots N) n - 1 = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \to \exists j \in (0 \dots N) F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \leq 0)$
392	391	anasss	$⊢ (φ \land (k \in ℕ \land n \in (1 \dots N))) \to (\exists j \in (0 \dots N) n - 1 = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F (P \div_{f} ((1 \dots N) \times \{k\})) (b) \land P (b) \neq 0)\} ℝ <) \to \exists j \in (0 \dots N) F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \leq 0)$
393	115 392	mpd	$⊢ (φ \land (k \in ℕ \land n \in (1 \dots N))) \to \exists j \in (0 \dots N) F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \leq 0$
394		breq	$⊢ r = \leq^{-1} \to (0 r F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \leftrightarrow 0 \leq^{-1} F (P \div_{f} ((1 \dots N) \times \{k\})) (n))$
395		fvex	$⊢ F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \in V$
396	40 395	brcnv	$⊢ 0 \leq^{-1} F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \leftrightarrow F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \leq 0$
397	394 396	bitrdi	$⊢ r = \leq^{-1} \to (0 r F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \leftrightarrow F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \leq 0)$
398	397	rexbidv	$⊢ r = \leq^{-1} \to (\exists j \in (0 \dots N) 0 r F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \leftrightarrow \exists j \in (0 \dots N) F (P \div_{f} ((1 \dots N) \times \{k\})) (n) \leq 0)$
399	393 398	syl5ibrcom	$⊢ (φ \land (k \in ℕ \land n \in (1 \dots N))) \to (r = \leq^{-1} \to \exists j \in (0 \dots N) 0 r F (P \div_{f} ((1 \dots N) \times \{k\})) (n))$
400	84 399	jaod	$⊢ (φ \land (k \in ℕ \land n \in (1 \dots N))) \to ((r = \leq \lor r = \leq^{-1}) \to \exists j \in (0 \dots N) 0 r F (P \div_{f} ((1 \dots N) \times \{k\})) (n))$
401	10 400	syl5	$⊢ (φ \land (k \in ℕ \land n \in (1 \dots N))) \to (r \in \{\leq \leq^{-1}\} \to \exists j \in (0 \dots N) 0 r F (P \div_{f} ((1 \dots N) \times \{k\})) (n))$
402	401	exp32	$⊢ φ \to (k \in ℕ \to (n \in (1 \dots N) \to (r \in \{\leq \leq^{-1}\} \to \exists j \in (0 \dots N) 0 r F (P \div_{f} ((1 \dots N) \times \{k\})) (n))))$
403	402	3imp2	$⊢ (φ \land (k \in ℕ \land n \in (1 \dots N) \land r \in \{\leq \leq^{-1}\})) \to \exists j \in (0 \dots N) 0 r F (P \div_{f} ((1 \dots N) \times \{k\})) (n)$

Metamath Proof Explorer

Theorem poimirlem31

Proof