poimirlem32

	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$
	poimir.3	$⊢ (φ \land (n \in (1 \dots N) \land z \in I \land z (n) = 1)) \to 0 \leq F (z) (n)$
Assertion	poimirlem32	$⊢ φ \to \exists c \in I \forall n \in (1 \dots N) \forall v \in (R ↾_{𝑡} I) (c \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (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		poimir.3	$⊢ (φ \land (n \in (1 \dots N) \land z \in I \land z (n) = 1)) \to 0 \leq F (z) (n)$
7	1	adantr	$⊢ (φ \land k \in ℕ) \to N \in ℕ$
8		fvoveq1	$⊢ p = 1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\})) \to F (p \div_{f} ((1 \dots N) \times \{k\})) = F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}))$
9	8	fveq1d	$⊢ p = 1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\})) \to F (p \div_{f} ((1 \dots N) \times \{k\})) (b) = F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b)$
10	9	breq2d	$⊢ p = 1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\})) \to (0 \leq F (p \div_{f} ((1 \dots N) \times \{k\})) (b) \leftrightarrow 0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b))$
11		fveq1	$⊢ p = 1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\})) \to p (b) = (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b)$
12	11	neeq1d	$⊢ p = 1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\})) \to (p (b) \neq 0 \leftrightarrow (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)$
13	10 12	anbi12d	$⊢ p = 1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\})) \to ((0 \leq F (p \div_{f} ((1 \dots N) \times \{k\})) (b) \land p (b) \neq 0) \leftrightarrow (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0))$
14	13	ralbidv	$⊢ p = 1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\})) \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 a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0))$
15	14	rabbidv	$⊢ p = 1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\})) \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)\} = \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\}$
16	15	uneq2d	$⊢ p = 1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{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)\} = \{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\}$
17	16	supeq1d	$⊢ p = 1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\})) \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)\} ℝ <) = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <)$
18	1	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
19		0elfz	$⊢ N \in ℕ_{0} \to 0 \in (0 \dots N)$
20	18 19	syl	$⊢ φ \to 0 \in (0 \dots N)$
21	20	snssd	$⊢ φ \to \{0\} \subseteq (0 \dots N)$
22		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)$
23		fz1ssfz0	$⊢ (1 \dots N) \subseteq (0 \dots N)$
24	22 23	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 (0 \dots N)$
25	24	a1i	$⊢ φ \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)\} \subseteq (0 \dots N)$
26	21 25	unssd	$⊢ φ \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)\} \subseteq (0 \dots N)$
27		ltso	$⊢ < Or ℝ$
28		snfi	$⊢ \{0\} \in Fin$
29		fzfi	$⊢ (1 \dots N) \in Fin$
30		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$
31	29 30	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$
32		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$
33	28 31 32	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$
34		c0ex	$⊢ 0 \in V$
35	34	snid	$⊢ 0 \in \{0\}$
36		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)\})$
37		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$
38	35 36 37	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$
39		0red	$⊢ (φ \to N \in ℕ) \to 0 \in ℝ$
40	39	snssd	$⊢ (φ \to N \in ℕ) \to \{0\} \subseteq ℝ$
41	1 40	ax-mp	$⊢ \{0\} \subseteq ℝ$
42		elfzelz	$⊢ n \in (1 \dots N) \to n \in ℤ$
43	42	ssriv	$⊢ (1 \dots N) \subseteq ℤ$
44		zssre	$⊢ ℤ \subseteq ℝ$
45	43 44	sstri	$⊢ (1 \dots N) \subseteq ℝ$
46	22 45	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 ℝ$
47	41 46	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 ℝ$
48	33 38 47	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 ℝ)$
49		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)\})$
50	27 48 49	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)\})$
51		ssel	$⊢ \{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 (0 \dots N) \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)\}) \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 \dots N))$
52	26 50 51	mpisyl	$⊢ φ \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 \dots N)$
53	52	ad2antrr	$⊢ ((φ \land k \in ℕ) \land p : (1 \dots N) ⟶ (0 \dots k)) \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 \dots N)$
54		elfznn	$⊢ n \in (1 \dots N) \to n \in ℕ$
55		nngt0	$⊢ n \in ℕ \to 0 < n$
56	55	adantr	$⊢ (n \in ℕ \land p (n) = 0) \to 0 < n$
57		simpr	$⊢ (0 \leq F (p \div_{f} ((1 \dots N) \times \{k\})) (b) \land p (b) \neq 0) \to p (b) \neq 0$
58	57	ralimi	$⊢ \forall b \in (1 \dots s) (0 \leq F (p \div_{f} ((1 \dots N) \times \{k\})) (b) \land p (b) \neq 0) \to \forall b \in (1 \dots s) p (b) \neq 0$
59		elfznn	$⊢ s \in (1 \dots N) \to s \in ℕ$
60		nnre	$⊢ n \in ℕ \to n \in ℝ$
61		nnre	$⊢ s \in ℕ \to s \in ℝ$
62		lenlt	$⊢ (n \in ℝ \land s \in ℝ) \to (n \leq s \leftrightarrow \neg s < n)$
63	60 61 62	syl2an	$⊢ (n \in ℕ \land s \in ℕ) \to (n \leq s \leftrightarrow \neg s < n)$
64		elfz1b	$⊢ n \in (1 \dots s) \leftrightarrow (n \in ℕ \land s \in ℕ \land n \leq s)$
65	64	biimpri	$⊢ (n \in ℕ \land s \in ℕ \land n \leq s) \to n \in (1 \dots s)$
66	65	3expia	$⊢ (n \in ℕ \land s \in ℕ) \to (n \leq s \to n \in (1 \dots s))$
67	63 66	sylbird	$⊢ (n \in ℕ \land s \in ℕ) \to (\neg s < n \to n \in (1 \dots s))$
68		fveq2	$⊢ b = n \to p (b) = p (n)$
69	68	eqeq1d	$⊢ b = n \to (p (b) = 0 \leftrightarrow p (n) = 0)$
70	69	rspcev	$⊢ (n \in (1 \dots s) \land p (n) = 0) \to \exists b \in (1 \dots s) p (b) = 0$
71	70	expcom	$⊢ p (n) = 0 \to (n \in (1 \dots s) \to \exists b \in (1 \dots s) p (b) = 0)$
72	67 71	sylan9	$⊢ ((n \in ℕ \land s \in ℕ) \land p (n) = 0) \to (\neg s < n \to \exists b \in (1 \dots s) p (b) = 0)$
73	72	an32s	$⊢ ((n \in ℕ \land p (n) = 0) \land s \in ℕ) \to (\neg s < n \to \exists b \in (1 \dots s) p (b) = 0)$
74		nne	$⊢ \neg p (b) \neq 0 \leftrightarrow p (b) = 0$
75	74	rexbii	$⊢ \exists b \in (1 \dots s) \neg p (b) \neq 0 \leftrightarrow \exists b \in (1 \dots s) p (b) = 0$
76		rexnal	$⊢ \exists b \in (1 \dots s) \neg p (b) \neq 0 \leftrightarrow \neg \forall b \in (1 \dots s) p (b) \neq 0$
77	75 76	bitr3i	$⊢ \exists b \in (1 \dots s) p (b) = 0 \leftrightarrow \neg \forall b \in (1 \dots s) p (b) \neq 0$
78	73 77	syl6ib	$⊢ ((n \in ℕ \land p (n) = 0) \land s \in ℕ) \to (\neg s < n \to \neg \forall b \in (1 \dots s) p (b) \neq 0)$
79	78	con4d	$⊢ ((n \in ℕ \land p (n) = 0) \land s \in ℕ) \to (\forall b \in (1 \dots s) p (b) \neq 0 \to s < n)$
80	59 79	sylan2	$⊢ ((n \in ℕ \land p (n) = 0) \land s \in (1 \dots N)) \to (\forall b \in (1 \dots s) p (b) \neq 0 \to s < n)$
81	58 80	syl5	$⊢ ((n \in ℕ \land p (n) = 0) \land s \in (1 \dots N)) \to (\forall b \in (1 \dots s) (0 \leq F (p \div_{f} ((1 \dots N) \times \{k\})) (b) \land p (b) \neq 0) \to s < n)$
82	81	ralrimiva	$⊢ (n \in ℕ \land p (n) = 0) \to \forall s \in (1 \dots N) (\forall b \in (1 \dots s) (0 \leq F (p \div_{f} ((1 \dots N) \times \{k\})) (b) \land p (b) \neq 0) \to s < n)$
83		ralunb	$⊢ \forall s \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)\}) s < n \leftrightarrow (\forall s \in \{0\} s < n \land \forall s \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)\} s < n)$
84		breq1	$⊢ s = 0 \to (s < n \leftrightarrow 0 < n)$
85	34 84	ralsn	$⊢ \forall s \in \{0\} s < n \leftrightarrow 0 < n$
86		oveq2	$⊢ a = s \to (1 \dots a) = (1 \dots s)$
87	86	raleqdv	$⊢ a = s \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 s) (0 \leq F (p \div_{f} ((1 \dots N) \times \{k\})) (b) \land p (b) \neq 0))$
88	87	ralrab	$⊢ \forall s \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)\} s < n \leftrightarrow \forall s \in (1 \dots N) (\forall b \in (1 \dots s) (0 \leq F (p \div_{f} ((1 \dots N) \times \{k\})) (b) \land p (b) \neq 0) \to s < n)$
89	85 88	anbi12i	$⊢ (\forall s \in \{0\} s < n \land \forall s \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)\} s < n) \leftrightarrow (0 < n \land \forall s \in (1 \dots N) (\forall b \in (1 \dots s) (0 \leq F (p \div_{f} ((1 \dots N) \times \{k\})) (b) \land p (b) \neq 0) \to s < n))$
90	83 89	bitri	$⊢ \forall s \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)\}) s < n \leftrightarrow (0 < n \land \forall s \in (1 \dots N) (\forall b \in (1 \dots s) (0 \leq F (p \div_{f} ((1 \dots N) \times \{k\})) (b) \land p (b) \neq 0) \to s < n))$
91	56 82 90	sylanbrc	$⊢ (n \in ℕ \land p (n) = 0) \to \forall s \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)\}) s < n$
92		breq1	$⊢ s = 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 (s < n \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)\} ℝ <) < n)$
93	92	rspcva	$⊢ (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)\}) \land \forall s \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)\}) s < n) \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)\} ℝ <) < n$
94	50 91 93	sylancr	$⊢ (n \in ℕ \land p (n) = 0) \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)\} ℝ <) < n$
95	54 94	sylan	$⊢ (n \in (1 \dots N) \land p (n) = 0) \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)\} ℝ <) < n$
96	95	3adant2	$⊢ (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = 0) \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)\} ℝ <) < n$
97	96	adantl	$⊢ ((φ \land k \in ℕ) \land (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = 0)) \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)\} ℝ <) < n$
98	42	zred	$⊢ n \in (1 \dots N) \to n \in ℝ$
99	98	3ad2ant1	$⊢ (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k) \to n \in ℝ$
100	99	adantl	$⊢ ((φ \land k \in ℕ) \land (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k)) \to n \in ℝ$
101		simpr1	$⊢ ((φ \land k \in ℕ) \land (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k)) \to n \in (1 \dots N)$
102		simpll	$⊢ ((φ \land k \in ℕ) \land (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k)) \to φ$
103		simplr	$⊢ ((φ \land k \in ℕ) \land (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k))) \to k \in ℕ$
104		elfzelz	$⊢ i \in (0 \dots k) \to i \in ℤ$
105	104	zred	$⊢ i \in (0 \dots k) \to i \in ℝ$
106		nndivre	$⊢ (i \in ℝ \land k \in ℕ) \to \frac{i}{k} \in ℝ$
107	105 106	sylan	$⊢ (i \in (0 \dots k) \land k \in ℕ) \to \frac{i}{k} \in ℝ$
108		elfzle1	$⊢ i \in (0 \dots k) \to 0 \leq i$
109	105 108	jca	$⊢ i \in (0 \dots k) \to (i \in ℝ \land 0 \leq i)$
110		nnrp	$⊢ k \in ℕ \to k \in ℝ^{+}$
111	110	rpregt0d	$⊢ k \in ℕ \to (k \in ℝ \land 0 < k)$
112		divge0	$⊢ ((i \in ℝ \land 0 \leq i) \land (k \in ℝ \land 0 < k)) \to 0 \leq \frac{i}{k}$
113	109 111 112	syl2an	$⊢ (i \in (0 \dots k) \land k \in ℕ) \to 0 \leq \frac{i}{k}$
114		elfzle2	$⊢ i \in (0 \dots k) \to i \leq k$
115	114	adantr	$⊢ (i \in (0 \dots k) \land k \in ℕ) \to i \leq k$
116	105	adantr	$⊢ (i \in (0 \dots k) \land k \in ℕ) \to i \in ℝ$
117		1red	$⊢ (i \in (0 \dots k) \land k \in ℕ) \to 1 \in ℝ$
118	110	adantl	$⊢ (i \in (0 \dots k) \land k \in ℕ) \to k \in ℝ^{+}$
119	116 117 118	ledivmuld	$⊢ (i \in (0 \dots k) \land k \in ℕ) \to (\frac{i}{k} \leq 1 \leftrightarrow i \leq k \cdot 1)$
120		nncn	$⊢ k \in ℕ \to k \in ℂ$
121	120	mulid1d	$⊢ k \in ℕ \to k \cdot 1 = k$
122	121	breq2d	$⊢ k \in ℕ \to (i \leq k \cdot 1 \leftrightarrow i \leq k)$
123	122	adantl	$⊢ (i \in (0 \dots k) \land k \in ℕ) \to (i \leq k \cdot 1 \leftrightarrow i \leq k)$
124	119 123	bitrd	$⊢ (i \in (0 \dots k) \land k \in ℕ) \to (\frac{i}{k} \leq 1 \leftrightarrow i \leq k)$
125	115 124	mpbird	$⊢ (i \in (0 \dots k) \land k \in ℕ) \to \frac{i}{k} \leq 1$
126		elicc01	$⊢ \frac{i}{k} \in [0, 1] \leftrightarrow (\frac{i}{k} \in ℝ \land 0 \leq \frac{i}{k} \land \frac{i}{k} \leq 1)$
127	107 113 125 126	syl3anbrc	$⊢ (i \in (0 \dots k) \land k \in ℕ) \to \frac{i}{k} \in [0, 1]$
128	127	ancoms	$⊢ (k \in ℕ \land i \in (0 \dots k)) \to \frac{i}{k} \in [0, 1]$
129		elsni	$⊢ j \in \{k\} \to j = k$
130	129	oveq2d	$⊢ j \in \{k\} \to \frac{i}{j} = \frac{i}{k}$
131	130	eleq1d	$⊢ j \in \{k\} \to (\frac{i}{j} \in [0, 1] \leftrightarrow \frac{i}{k} \in [0, 1])$
132	128 131	syl5ibrcom	$⊢ (k \in ℕ \land i \in (0 \dots k)) \to (j \in \{k\} \to \frac{i}{j} \in [0, 1])$
133	132	impr	$⊢ (k \in ℕ \land (i \in (0 \dots k) \land j \in \{k\})) \to \frac{i}{j} \in [0, 1]$
134	103 133	sylan	$⊢ (((φ \land k \in ℕ) \land (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k))) \land (i \in (0 \dots k) \land j \in \{k\})) \to \frac{i}{j} \in [0, 1]$
135		simprr	$⊢ ((φ \land k \in ℕ) \land (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k))) \to p : (1 \dots N) ⟶ (0 \dots k)$
136		vex	$⊢ k \in V$
137	136	fconst	$⊢ ((1 \dots N) \times \{k\}) : (1 \dots N) ⟶ \{k\}$
138	137	a1i	$⊢ ((φ \land k \in ℕ) \land (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k))) \to ((1 \dots N) \times \{k\}) : (1 \dots N) ⟶ \{k\}$
139		fzfid	$⊢ ((φ \land k \in ℕ) \land (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k))) \to (1 \dots N) \in Fin$
140		inidm	$⊢ (1 \dots N) \cap (1 \dots N) = (1 \dots N)$
141	134 135 138 139 139 140	off	$⊢ ((φ \land k \in ℕ) \land (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k))) \to (p \div_{f} ((1 \dots N) \times \{k\})) : (1 \dots N) ⟶ [0, 1]$
142	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)})$
143		ovex	$⊢ [0, 1] \in V$
144		ovex	$⊢ (1 \dots N) \in V$
145	143 144	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]$
146	142 145	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]$
147	141 146	sylibr	$⊢ ((φ \land k \in ℕ) \land (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k))) \to p \div_{f} ((1 \dots N) \times \{k\}) \in I$
148	147	3adantr3	$⊢ ((φ \land k \in ℕ) \land (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k)) \to p \div_{f} ((1 \dots N) \times \{k\}) \in I$
149		3anass	$⊢ (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k) \leftrightarrow (n \in (1 \dots N) \land (p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k))$
150		ancom	$⊢ (n \in (1 \dots N) \land (p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k)) \leftrightarrow ((p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k) \land n \in (1 \dots N))$
151	149 150	bitri	$⊢ (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k) \leftrightarrow ((p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k) \land n \in (1 \dots N))$
152		ffn	$⊢ p : (1 \dots N) ⟶ (0 \dots k) \to p Fn (1 \dots N)$
153	152	ad2antrl	$⊢ ((φ \land k \in ℕ) \land (p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k)) \to p Fn (1 \dots N)$
154		fnconstg	$⊢ k \in V \to ((1 \dots N) \times \{k\}) Fn (1 \dots N)$
155	136 154	mp1i	$⊢ ((φ \land k \in ℕ) \land (p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k)) \to ((1 \dots N) \times \{k\}) Fn (1 \dots N)$
156		fzfid	$⊢ ((φ \land k \in ℕ) \land (p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k)) \to (1 \dots N) \in Fin$
157		simplrr	$⊢ (((φ \land k \in ℕ) \land (p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k)) \land n \in (1 \dots N)) \to p (n) = k$
158	136	fvconst2	$⊢ n \in (1 \dots N) \to ((1 \dots N) \times \{k\}) (n) = k$
159	158	adantl	$⊢ (((φ \land k \in ℕ) \land (p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k)) \land n \in (1 \dots N)) \to ((1 \dots N) \times \{k\}) (n) = k$
160	153 155 156 156 140 157 159	ofval	$⊢ (((φ \land k \in ℕ) \land (p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k)) \land n \in (1 \dots N)) \to (p \div_{f} ((1 \dots N) \times \{k\})) (n) = \frac{k}{k}$
161	160	anasss	$⊢ ((φ \land k \in ℕ) \land ((p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k) \land n \in (1 \dots N))) \to (p \div_{f} ((1 \dots N) \times \{k\})) (n) = \frac{k}{k}$
162	151 161	sylan2b	$⊢ ((φ \land k \in ℕ) \land (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k)) \to (p \div_{f} ((1 \dots N) \times \{k\})) (n) = \frac{k}{k}$
163		nnne0	$⊢ k \in ℕ \to k \neq 0$
164	120 163	dividd	$⊢ k \in ℕ \to \frac{k}{k} = 1$
165	164	ad2antlr	$⊢ ((φ \land k \in ℕ) \land (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k)) \to \frac{k}{k} = 1$
166	162 165	eqtrd	$⊢ ((φ \land k \in ℕ) \land (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k)) \to (p \div_{f} ((1 \dots N) \times \{k\})) (n) = 1$
167		ovex	$⊢ p \div_{f} ((1 \dots N) \times \{k\}) \in V$
168		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)$
169		fveq1	$⊢ z = p \div_{f} ((1 \dots N) \times \{k\}) \to z (n) = (p \div_{f} ((1 \dots N) \times \{k\})) (n)$
170	169	eqeq1d	$⊢ z = p \div_{f} ((1 \dots N) \times \{k\}) \to (z (n) = 1 \leftrightarrow (p \div_{f} ((1 \dots N) \times \{k\})) (n) = 1)$
171	168 170	3anbi23d	$⊢ z = p \div_{f} ((1 \dots N) \times \{k\}) \to ((n \in (1 \dots N) \land z \in I \land z (n) = 1) \leftrightarrow (n \in (1 \dots N) \land p \div_{f} ((1 \dots N) \times \{k\}) \in I \land (p \div_{f} ((1 \dots N) \times \{k\})) (n) = 1))$
172	171	anbi2d	$⊢ z = p \div_{f} ((1 \dots N) \times \{k\}) \to ((φ \land (n \in (1 \dots N) \land z \in I \land z (n) = 1)) \leftrightarrow (φ \land (n \in (1 \dots N) \land p \div_{f} ((1 \dots N) \times \{k\}) \in I \land (p \div_{f} ((1 \dots N) \times \{k\})) (n) = 1)))$
173		fveq2	$⊢ z = p \div_{f} ((1 \dots N) \times \{k\}) \to F (z) = F (p \div_{f} ((1 \dots N) \times \{k\}))$
174	173	fveq1d	$⊢ z = p \div_{f} ((1 \dots N) \times \{k\}) \to F (z) (n) = F (p \div_{f} ((1 \dots N) \times \{k\})) (n)$
175	174	breq2d	$⊢ z = p \div_{f} ((1 \dots N) \times \{k\}) \to (0 \leq F (z) (n) \leftrightarrow 0 \leq F (p \div_{f} ((1 \dots N) \times \{k\})) (n))$
176	172 175	imbi12d	$⊢ z = p \div_{f} ((1 \dots N) \times \{k\}) \to (((φ \land (n \in (1 \dots N) \land z \in I \land z (n) = 1)) \to 0 \leq F (z) (n)) \leftrightarrow ((φ \land (n \in (1 \dots N) \land p \div_{f} ((1 \dots N) \times \{k\}) \in I \land (p \div_{f} ((1 \dots N) \times \{k\})) (n) = 1)) \to 0 \leq F (p \div_{f} ((1 \dots N) \times \{k\})) (n)))$
177	167 176 6	vtocl	$⊢ (φ \land (n \in (1 \dots N) \land p \div_{f} ((1 \dots N) \times \{k\}) \in I \land (p \div_{f} ((1 \dots N) \times \{k\})) (n) = 1)) \to 0 \leq F (p \div_{f} ((1 \dots N) \times \{k\})) (n)$
178	102 101 148 166 177	syl13anc	$⊢ ((φ \land k \in ℕ) \land (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k)) \to 0 \leq F (p \div_{f} ((1 \dots N) \times \{k\})) (n)$
179		simpr	$⊢ (φ \land k \in ℕ) \to k \in ℕ$
180		simp3	$⊢ (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k) \to p (n) = k$
181		neeq1	$⊢ p (n) = k \to (p (n) \neq 0 \leftrightarrow k \neq 0)$
182	163 181	syl5ibrcom	$⊢ k \in ℕ \to (p (n) = k \to p (n) \neq 0)$
183	182	imp	$⊢ (k \in ℕ \land p (n) = k) \to p (n) \neq 0$
184	179 180 183	syl2an	$⊢ ((φ \land k \in ℕ) \land (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k)) \to p (n) \neq 0$
185		vex	$⊢ n \in V$
186		fveq2	$⊢ b = n \to F (p \div_{f} ((1 \dots N) \times \{k\})) (b) = F (p \div_{f} ((1 \dots N) \times \{k\})) (n)$
187	186	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))$
188	68	neeq1d	$⊢ b = n \to (p (b) \neq 0 \leftrightarrow p (n) \neq 0)$
189	187 188	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))$
190	185 189	ralsn	$⊢ \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)$
191	178 184 190	sylanbrc	$⊢ ((φ \land k \in ℕ) \land (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k)) \to \forall b \in \{n\} (0 \leq F (p \div_{f} ((1 \dots N) \times \{k\})) (b) \land p (b) \neq 0)$
192	42	zcnd	$⊢ n \in (1 \dots N) \to n \in ℂ$
193		1cnd	$⊢ n \in (1 \dots N) \to 1 \in ℂ$
194	192 193	subeq0ad	$⊢ n \in (1 \dots N) \to (n - 1 = 0 \leftrightarrow n = 1)$
195	194	biimpcd	$⊢ n - 1 = 0 \to (n \in (1 \dots N) \to n = 1)$
196		1z	$⊢ 1 \in ℤ$
197		fzsn	$⊢ 1 \in ℤ \to (1 \dots 1) = \{1\}$
198	196 197	ax-mp	$⊢ (1 \dots 1) = \{1\}$
199		oveq2	$⊢ n = 1 \to (1 \dots n) = (1 \dots 1)$
200		sneq	$⊢ n = 1 \to \{n\} = \{1\}$
201	198 199 200	3eqtr4a	$⊢ n = 1 \to (1 \dots n) = \{n\}$
202	201	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))$
203	202	biimprd	$⊢ n = 1 \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))$
204	195 203	syl6	$⊢ n - 1 = 0 \to (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) \to \forall b \in (1 \dots n) (0 \leq F (p \div_{f} ((1 \dots N) \times \{k\})) (b) \land p (b) \neq 0)))$
205		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)$
206		npcan1	$⊢ n \in ℂ \to n - 1 + 1 = n$
207	192 206	syl	$⊢ n \in (1 \dots N) \to n - 1 + 1 = n$
208		elfzuz	$⊢ n \in (1 \dots N) \to n \in ℤ_{\geq 1}$
209	207 208	eqeltrd	$⊢ n \in (1 \dots N) \to n - 1 + 1 \in ℤ_{\geq 1}$
210		peano2zm	$⊢ n \in ℤ \to n - 1 \in ℤ$
211		uzid	$⊢ n - 1 \in ℤ \to n - 1 \in ℤ_{\geq (n - 1)}$
212		peano2uz	$⊢ n - 1 \in ℤ_{\geq (n - 1)} \to n - 1 + 1 \in ℤ_{\geq (n - 1)}$
213	42 210 211 212	4syl	$⊢ n \in (1 \dots N) \to n - 1 + 1 \in ℤ_{\geq (n - 1)}$
214	207 213	eqeltrrd	$⊢ n \in (1 \dots N) \to n \in ℤ_{\geq (n - 1)}$
215		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)$
216	209 214 215	syl2anc	$⊢ n \in (1 \dots N) \to (1 \dots n) = (1 \dots n - 1) \cup (n - 1 + 1 \dots n)$
217	207	oveq1d	$⊢ n \in (1 \dots N) \to (n - 1 + 1 \dots n) = (n \dots n)$
218		fzsn	$⊢ n \in ℤ \to (n \dots n) = \{n\}$
219	42 218	syl	$⊢ n \in (1 \dots N) \to (n \dots n) = \{n\}$
220	217 219	eqtrd	$⊢ n \in (1 \dots N) \to (n - 1 + 1 \dots n) = \{n\}$
221	220	uneq2d	$⊢ n \in (1 \dots N) \to (1 \dots n - 1) \cup (n - 1 + 1 \dots n) = (1 \dots n - 1) \cup \{n\}$
222	216 221	eqtrd	$⊢ n \in (1 \dots N) \to (1 \dots n) = (1 \dots n - 1) \cup \{n\}$
223	222	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))$
224	205 223	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))$
225	224	expd	$⊢ 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) \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)))$
226	225	com12	$⊢ \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 (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) \to \forall b \in (1 \dots n) (0 \leq F (p \div_{f} ((1 \dots N) \times \{k\})) (b) \land p (b) \neq 0)))$
227	226	adantl	$⊢ (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 (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) \to \forall b \in (1 \dots n) (0 \leq F (p \div_{f} ((1 \dots N) \times \{k\})) (b) \land p (b) \neq 0)))$
228	204 227	jaoi	$⊢ (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))) \to (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) \to \forall b \in (1 \dots n) (0 \leq F (p \div_{f} ((1 \dots N) \times \{k\})) (b) \land p (b) \neq 0)))$
229	228	imdistand	$⊢ (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))) \to ((n \in (1 \dots N) \land \forall b \in \{n\} (0 \leq F (p \div_{f} ((1 \dots N) \times \{k\})) (b) \land p (b) \neq 0)) \to (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)))$
230	229	com12	$⊢ (n \in (1 \dots N) \land \forall b \in \{n\} (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))) \to (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)))$
231		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)\})$
232		ovex	$⊢ n - 1 \in V$
233	232	elsn	$⊢ n - 1 \in \{0\} \leftrightarrow n - 1 = 0$
234		oveq2	$⊢ a = n - 1 \to (1 \dots a) = (1 \dots n - 1)$
235	234	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))$
236	235	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))$
237	233 236	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)))$
238	231 237	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)))$
239		oveq2	$⊢ a = n \to (1 \dots a) = (1 \dots n)$
240	239	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))$
241	240	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))$
242	230 238 241	3imtr4g	$⊢ (n \in (1 \dots N) \land \forall b \in \{n\} (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)\}) \to 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)\})$
243		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)\})$
244	242 243	syl6	$⊢ (n \in (1 \dots N) \land \forall b \in \{n\} (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)\}) \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)\}))$
245	101 191 244	syl2anc	$⊢ ((φ \land k \in ℕ) \land (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k)) \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)\}) \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)\}))$
246		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 i \in ℝ \forall j \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)\}) j \leq i$
247	47 33 246	mp2an	$⊢ \exists i \in ℝ \forall j \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)\}) j \leq i$
248	47 38 247	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 i \in ℝ \forall j \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)\}) j \leq i)$
249	248	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)\} ℝ <)$
250	245 249	syl6	$⊢ ((φ \land k \in ℕ) \land (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k)) \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)\}) \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)\} ℝ <))$
251		ltm1	$⊢ n \in ℝ \to n - 1 < n$
252		peano2rem	$⊢ n \in ℝ \to n - 1 \in ℝ$
253	47 50	sselii	$⊢ 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 ℝ$
254		ltletr	$⊢ (n - 1 \in ℝ \land n \in ℝ \land 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 ℝ) \to ((n - 1 < n \land 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 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)\} ℝ <))$
255	253 254	mp3an3	$⊢ (n - 1 \in ℝ \land n \in ℝ) \to ((n - 1 < n \land 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 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)\} ℝ <))$
256	252 255	mpancom	$⊢ n \in ℝ \to ((n - 1 < n \land 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 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)\} ℝ <))$
257	251 256	mpand	$⊢ n \in ℝ \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)\} ℝ <) \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)\} ℝ <))$
258	100 250 257	sylsyld	$⊢ ((φ \land k \in ℕ) \land (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k)) \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)\}) \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)\} ℝ <))$
259	253	ltnri	$⊢ \neg 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)\} ℝ <) < 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)\} ℝ <)$
260		breq1	$⊢ 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)\} ℝ <) = n - 1 \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)\} ℝ <) < 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)\} ℝ <))$
261	259 260	mtbii	$⊢ 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)\} ℝ <) = n - 1 \to \neg 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)\} ℝ <)$
262	261	necon2ai	$⊢ 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 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)\} ℝ <) \neq n - 1$
263	258 262	syl6	$⊢ ((φ \land k \in ℕ) \land (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k)) \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)\}) \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)\} ℝ <) \neq n - 1)$
264		eleq1	$⊢ 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)\} ℝ <) = n - 1 \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)\}) \leftrightarrow 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)\}))$
265	50 264	mpbii	$⊢ 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)\} ℝ <) = n - 1 \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)\})$
266	265	necon3bi	$⊢ \neg 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)\}) \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)\} ℝ <) \neq n - 1$
267	263 266	pm2.61d1	$⊢ ((φ \land k \in ℕ) \land (n \in (1 \dots N) \land p : (1 \dots N) ⟶ (0 \dots k) \land p (n) = k)) \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)\} ℝ <) \neq n - 1$
268	7 17 53 97 267 179	poimirlem28	$⊢ (φ \land k \in ℕ) \to \exists s \in (({(0 ..^k)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <)$
269		nn0ex	$⊢ ℕ_{0} \in V$
270		fzo0ssnn0	$⊢ (0 ..^k) \subseteq ℕ_{0}$
271		mapss	$⊢ (ℕ_{0} \in V \land (0 ..^k) \subseteq ℕ_{0}) \to {(0 ..^k)}^{(1 \dots N)} \subseteq {ℕ_{0}}^{(1 \dots N)}$
272	269 270 271	mp2an	$⊢ {(0 ..^k)}^{(1 \dots N)} \subseteq {ℕ_{0}}^{(1 \dots N)}$
273		xpss1	$⊢ {(0 ..^k)}^{(1 \dots N)} \subseteq {ℕ_{0}}^{(1 \dots N)} \to ({(0 ..^k)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \subseteq ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
274	272 273	ax-mp	$⊢ ({(0 ..^k)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \subseteq ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
275	274	sseli	$⊢ s \in (({(0 ..^k)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to s \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
276		xp1st	$⊢ s \in (({(0 ..^k)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 1^{st} (s) \in ({(0 ..^k)}^{(1 \dots N)})$
277		elmapi	$⊢ 1^{st} (s) \in ({(0 ..^k)}^{(1 \dots N)}) \to 1^{st} (s) : (1 \dots N) ⟶ (0 ..^k)$
278		frn	$⊢ 1^{st} (s) : (1 \dots N) ⟶ (0 ..^k) \to ran 1^{st} (s) \subseteq (0 ..^k)$
279	276 277 278	3syl	$⊢ s \in (({(0 ..^k)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to ran 1^{st} (s) \subseteq (0 ..^k)$
280	275 279	jca	$⊢ s \in (({(0 ..^k)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to (s \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land ran 1^{st} (s) \subseteq (0 ..^k))$
281	280	anim1i	$⊢ (s \in (({(0 ..^k)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <)) \to ((s \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land ran 1^{st} (s) \subseteq (0 ..^k)) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <))$
282		anass	$⊢ ((s \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land ran 1^{st} (s) \subseteq (0 ..^k)) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <)) \leftrightarrow (s \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land (ran 1^{st} (s) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <)))$
283	281 282	sylib	$⊢ (s \in (({(0 ..^k)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <)) \to (s \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land (ran 1^{st} (s) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <)))$
284	283	reximi2	$⊢ \exists s \in (({(0 ..^k)}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <) \to \exists s \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) (ran 1^{st} (s) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <))$
285	268 284	syl	$⊢ (φ \land k \in ℕ) \to \exists s \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) (ran 1^{st} (s) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <))$
286	285	ralrimiva	$⊢ φ \to \forall k \in ℕ \exists s \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) (ran 1^{st} (s) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <))$
287		nnex	$⊢ ℕ \in V$
288	144 269	ixpconst	$⊢ ⨉_{n = 1}^{N} ℕ_{0} = {ℕ_{0}}^{(1 \dots N)}$
289		omelon	$⊢ ω \in On$
290		nn0ennn	$⊢ ℕ_{0} \approx ℕ$
291		nnenom	$⊢ ℕ \approx ω$
292	290 291	entr2i	$⊢ ω \approx ℕ_{0}$
293		isnumi	$⊢ (ω \in On \land ω \approx ℕ_{0}) \to ℕ_{0} \in dom card$
294	289 292 293	mp2an	$⊢ ℕ_{0} \in dom card$
295	294	rgenw	$⊢ \forall n \in (1 \dots N) ℕ_{0} \in dom card$
296		finixpnum	$⊢ ((1 \dots N) \in Fin \land \forall n \in (1 \dots N) ℕ_{0} \in dom card) \to ⨉_{n = 1}^{N} ℕ_{0} \in dom card$
297	29 295 296	mp2an	$⊢ ⨉_{n = 1}^{N} ℕ_{0} \in dom card$
298	288 297	eqeltrri	$⊢ {ℕ_{0}}^{(1 \dots N)} \in dom card$
299	144 144	mapval	$⊢ {(1 \dots N)}^{(1 \dots N)} = \{f \| f : (1 \dots N) ⟶ (1 \dots N)\}$
300		mapfi	$⊢ ((1 \dots N) \in Fin \land (1 \dots N) \in Fin) \to {(1 \dots N)}^{(1 \dots N)} \in Fin$
301	29 29 300	mp2an	$⊢ {(1 \dots N)}^{(1 \dots N)} \in Fin$
302	299 301	eqeltrri	$⊢ \{f \| f : (1 \dots N) ⟶ (1 \dots N)\} \in Fin$
303		f1of	$⊢ f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to f : (1 \dots N) ⟶ (1 \dots N)$
304	303	ss2abi	$⊢ \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \subseteq \{f \| f : (1 \dots N) ⟶ (1 \dots N)\}$
305		ssfi	$⊢ (\{f \| f : (1 \dots N) ⟶ (1 \dots N)\} \in Fin \land \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \subseteq \{f \| f : (1 \dots N) ⟶ (1 \dots N)\}) \to \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \in Fin$
306	302 304 305	mp2an	$⊢ \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \in Fin$
307		finnum	$⊢ \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \in Fin \to \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \in dom card$
308	306 307	ax-mp	$⊢ \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \in dom card$
309		xpnum	$⊢ ({ℕ_{0}}^{(1 \dots N)} \in dom card \land \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \in dom card) \to ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \in dom card$
310	298 308 309	mp2an	$⊢ ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \in dom card$
311		ssrab2	$⊢ \{s \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \| (ran 1^{st} (s) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <))\} \subseteq ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
312	311	rgenw	$⊢ \forall k \in ℕ \{s \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \| (ran 1^{st} (s) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <))\} \subseteq ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
313		ss2iun	$⊢ \forall k \in ℕ \{s \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \| (ran 1^{st} (s) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <))\} \subseteq ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \to ⋃_{k \in ℕ} \{s \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \| (ran 1^{st} (s) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <))\} \subseteq ⋃_{k \in ℕ} (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
314	312 313	ax-mp	$⊢ ⋃_{k \in ℕ} \{s \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \| (ran 1^{st} (s) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <))\} \subseteq ⋃_{k \in ℕ} (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
315		1nn	$⊢ 1 \in ℕ$
316		ne0i	$⊢ 1 \in ℕ \to ℕ \neq \emptyset$
317		iunconst	$⊢ ℕ \neq \emptyset \to ⋃_{k \in ℕ} (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) = ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
318	315 316 317	mp2b	$⊢ ⋃_{k \in ℕ} (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) = ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
319	314 318	sseqtri	$⊢ ⋃_{k \in ℕ} \{s \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \| (ran 1^{st} (s) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <))\} \subseteq ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
320		ssnum	$⊢ (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \in dom card \land ⋃_{k \in ℕ} \{s \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \| (ran 1^{st} (s) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <))\} \subseteq ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to ⋃_{k \in ℕ} \{s \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \| (ran 1^{st} (s) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <))\} \in dom card$
321	310 319 320	mp2an	$⊢ ⋃_{k \in ℕ} \{s \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \| (ran 1^{st} (s) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <))\} \in dom card$
322		fveq2	$⊢ s = g (k) \to 1^{st} (s) = 1^{st} (g (k))$
323	322	rneqd	$⊢ s = g (k) \to ran 1^{st} (s) = ran 1^{st} (g (k))$
324	323	sseq1d	$⊢ s = g (k) \to (ran 1^{st} (s) \subseteq (0 ..^k) \leftrightarrow ran 1^{st} (g (k)) \subseteq (0 ..^k))$
325		fveq2	$⊢ s = g (k) \to 2^{nd} (s) = 2^{nd} (g (k))$
326	325	imaeq1d	$⊢ s = g (k) \to 2^{nd} (s) [(1 \dots j)] = 2^{nd} (g (k)) [(1 \dots j)]$
327	326	xpeq1d	$⊢ s = g (k) \to 2^{nd} (s) [(1 \dots j)] \times \{1\} = 2^{nd} (g (k)) [(1 \dots j)] \times \{1\}$
328	325	imaeq1d	$⊢ s = g (k) \to 2^{nd} (s) [(j + 1 \dots N)] = 2^{nd} (g (k)) [(j + 1 \dots N)]$
329	328	xpeq1d	$⊢ s = g (k) \to 2^{nd} (s) [(j + 1 \dots N)] \times \{0\} = 2^{nd} (g (k)) [(j + 1 \dots N)] \times \{0\}$
330	327 329	uneq12d	$⊢ s = g (k) \to (2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}) = (2^{nd} (g (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (k)) [(j + 1 \dots N)] \times \{0\})$
331	322 330	oveq12d	$⊢ s = g (k) \to 1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\})) = 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\}))$
332	331	fvoveq1d	$⊢ s = g (k) \to F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) = F ((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\}))) \div_{f} ((1 \dots N) \times \{k\}))$
333	332	fveq1d	$⊢ s = g (k) \to F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) = F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b)$
334	333	breq2d	$⊢ s = g (k) \to (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \leftrightarrow 0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b))$
335	331	fveq1d	$⊢ s = g (k) \to (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) = (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\}))) (b)$
336	335	neeq1d	$⊢ s = g (k) \to ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0 \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\}))) (b) \neq 0)$
337	334 336	anbi12d	$⊢ s = g (k) \to ((0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0) \leftrightarrow (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0))$
338	337	ralbidv	$⊢ s = g (k) \to (\forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0) \leftrightarrow \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0))$
339	338	rabbidv	$⊢ s = g (k) \to \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} = \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\}$
340	339	uneq2d	$⊢ s = g (k) \to \{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} = \{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\}$
341	340	supeq1d	$⊢ s = g (k) \to sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <) = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <)$
342	341	eqeq2d	$⊢ s = g (k) \to (i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <) \leftrightarrow i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <))$
343	342	rexbidv	$⊢ s = g (k) \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 ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <) \leftrightarrow \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <))$
344	343	ralbidv	$⊢ s = g (k) \to (\forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <) \leftrightarrow \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <))$
345	324 344	anbi12d	$⊢ s = g (k) \to ((ran 1^{st} (s) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <)) \leftrightarrow (ran 1^{st} (g (k)) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <)))$
346	345	ac6num	$⊢ (ℕ \in V \land ⋃_{k \in ℕ} \{s \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \| (ran 1^{st} (s) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <))\} \in dom card \land \forall k \in ℕ \exists s \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) (ran 1^{st} (s) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <))) \to \exists g (g : ℕ ⟶ ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \land \forall k \in ℕ (ran 1^{st} (g (k)) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <)))$
347	287 321 346	mp3an12	$⊢ \forall k \in ℕ \exists s \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) (ran 1^{st} (s) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (1^{st} (s) +_{f} ((2^{nd} (s) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (s) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <)) \to \exists g (g : ℕ ⟶ ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \land \forall k \in ℕ (ran 1^{st} (g (k)) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <)))$
348	286 347	syl	$⊢ φ \to \exists g (g : ℕ ⟶ ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \land \forall k \in ℕ (ran 1^{st} (g (k)) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <)))$
349	1	ad2antrr	$⊢ ((φ \land g : ℕ ⟶ ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land \forall k \in ℕ (ran 1^{st} (g (k)) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <))) \to N \in ℕ$
350	4	ad2antrr	$⊢ ((φ \land g : ℕ ⟶ ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land \forall k \in ℕ (ran 1^{st} (g (k)) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <))) \to F \in ((R ↾_{𝑡} I) Cn R)$
351		eqid	$⊢ F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (n) = F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (n)$
352		simplr	$⊢ ((φ \land g : ℕ ⟶ ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land \forall k \in ℕ (ran 1^{st} (g (k)) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <))) \to g : ℕ ⟶ ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
353		simpl	$⊢ (ran 1^{st} (g (k)) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <)) \to ran 1^{st} (g (k)) \subseteq (0 ..^k)$
354	353	ralimi	$⊢ \forall k \in ℕ (ran 1^{st} (g (k)) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <)) \to \forall k \in ℕ ran 1^{st} (g (k)) \subseteq (0 ..^k)$
355	354	adantl	$⊢ ((φ \land g : ℕ ⟶ ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land \forall k \in ℕ (ran 1^{st} (g (k)) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <))) \to \forall k \in ℕ ran 1^{st} (g (k)) \subseteq (0 ..^k)$
356		2fveq3	$⊢ k = p \to 1^{st} (g (k)) = 1^{st} (g (p))$
357	356	rneqd	$⊢ k = p \to ran 1^{st} (g (k)) = ran 1^{st} (g (p))$
358		oveq2	$⊢ k = p \to (0 ..^k) = (0 ..^p)$
359	357 358	sseq12d	$⊢ k = p \to (ran 1^{st} (g (k)) \subseteq (0 ..^k) \leftrightarrow ran 1^{st} (g (p)) \subseteq (0 ..^p))$
360	359	rspccva	$⊢ (\forall k \in ℕ ran 1^{st} (g (k)) \subseteq (0 ..^k) \land p \in ℕ) \to ran 1^{st} (g (p)) \subseteq (0 ..^p)$
361	355 360	sylan	$⊢ (((φ \land g : ℕ ⟶ ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land \forall k \in ℕ (ran 1^{st} (g (k)) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <))) \land p \in ℕ) \to ran 1^{st} (g (p)) \subseteq (0 ..^p)$
362		simpll	$⊢ ((φ \land g : ℕ ⟶ ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land \forall k \in ℕ (ran 1^{st} (g (k)) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <))) \to φ$
363	362 5	sylan	$⊢ (((φ \land g : ℕ ⟶ ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land \forall k \in ℕ (ran 1^{st} (g (k)) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <))) \land (n \in (1 \dots N) \land z \in I \land z (n) = 0)) \to F (z) (n) \leq 0$
364		eqid	$⊢ 1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\})) = 1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))$
365		simpr	$⊢ (ran 1^{st} (g (k)) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <)) \to \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <)$
366	365	ralimi	$⊢ \forall k \in ℕ (ran 1^{st} (g (k)) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <)) \to \forall k \in ℕ \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <)$
367	366	adantl	$⊢ ((φ \land g : ℕ ⟶ ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land \forall k \in ℕ (ran 1^{st} (g (k)) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <))) \to \forall k \in ℕ \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <)$
368		2fveq3	$⊢ k = p \to 2^{nd} (g (k)) = 2^{nd} (g (p))$
369	368	imaeq1d	$⊢ k = p \to 2^{nd} (g (k)) [(1 \dots j)] = 2^{nd} (g (p)) [(1 \dots j)]$
370	369	xpeq1d	$⊢ k = p \to 2^{nd} (g (k)) [(1 \dots j)] \times \{1\} = 2^{nd} (g (p)) [(1 \dots j)] \times \{1\}$
371	368	imaeq1d	$⊢ k = p \to 2^{nd} (g (k)) [(j + 1 \dots N)] = 2^{nd} (g (p)) [(j + 1 \dots N)]$
372	371	xpeq1d	$⊢ k = p \to 2^{nd} (g (k)) [(j + 1 \dots N)] \times \{0\} = 2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}$
373	370 372	uneq12d	$⊢ k = p \to (2^{nd} (g (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (k)) [(j + 1 \dots N)] \times \{0\}) = (2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\})$
374	356 373	oveq12d	$⊢ k = p \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^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))$
375		sneq	$⊢ k = p \to \{k\} = \{p\}$
376	375	xpeq2d	$⊢ k = p \to (1 \dots N) \times \{k\} = (1 \dots N) \times \{p\}$
377	374 376	oveq12d	$⊢ k = p \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\}))) \div_{f} ((1 \dots N) \times \{k\}) = (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})$
378	377	fveq2d	$⊢ k = p \to F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) = F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\}))$
379	378	fveq1d	$⊢ k = p \to F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) = F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b)$
380	379	breq2d	$⊢ k = p \to (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \leftrightarrow 0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b))$
381	374	fveq1d	$⊢ k = p \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\}))) (b) = (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) (b)$
382	381	neeq1d	$⊢ k = p \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\}))) (b) \neq 0 \leftrightarrow (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)$
383	380 382	anbi12d	$⊢ k = p \to ((0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0) \leftrightarrow (0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0))$
384	383	ralbidv	$⊢ k = p \to (\forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0) \leftrightarrow \forall b \in (1 \dots a) (0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0))$
385	384	rabbidv	$⊢ k = p \to \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} = \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\}$
386	385	uneq2d	$⊢ k = p \to \{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} = \{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\}$
387	386	supeq1d	$⊢ k = p \to sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <) = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <)$
388	387	eqeq2d	$⊢ k = p \to (i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <) \leftrightarrow i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <))$
389	388	rexbidv	$⊢ k = p \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 ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <) \leftrightarrow \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <))$
390		eqeq1	$⊢ i = q \to (i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <) \leftrightarrow q = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <))$
391	390	rexbidv	$⊢ i = q \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 ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <) \leftrightarrow \exists j \in (0 \dots N) q = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <))$
392		oveq2	$⊢ j = m \to (1 \dots j) = (1 \dots m)$
393	392	imaeq2d	$⊢ j = m \to 2^{nd} (g (p)) [(1 \dots j)] = 2^{nd} (g (p)) [(1 \dots m)]$
394	393	xpeq1d	$⊢ j = m \to 2^{nd} (g (p)) [(1 \dots j)] \times \{1\} = 2^{nd} (g (p)) [(1 \dots m)] \times \{1\}$
395		oveq1	$⊢ j = m \to j + 1 = m + 1$
396	395	oveq1d	$⊢ j = m \to (j + 1 \dots N) = (m + 1 \dots N)$
397	396	imaeq2d	$⊢ j = m \to 2^{nd} (g (p)) [(j + 1 \dots N)] = 2^{nd} (g (p)) [(m + 1 \dots N)]$
398	397	xpeq1d	$⊢ j = m \to 2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\} = 2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}$
399	394 398	uneq12d	$⊢ j = m \to (2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}) = (2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\})$
400	399	oveq2d	$⊢ j = m \to 1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\})) = 1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))$
401	400	fvoveq1d	$⊢ j = m \to F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) = F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\}))$
402	401	fveq1d	$⊢ j = m \to F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) = F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b)$
403	402	breq2d	$⊢ j = m \to (0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \leftrightarrow 0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b))$
404	400	fveq1d	$⊢ j = m \to (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) (b) = (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) (b)$
405	404	neeq1d	$⊢ j = m \to ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0 \leftrightarrow (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) (b) \neq 0)$
406	403 405	anbi12d	$⊢ j = m \to ((0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0) \leftrightarrow (0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) (b) \neq 0))$
407	406	ralbidv	$⊢ j = m \to (\forall b \in (1 \dots a) (0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0) \leftrightarrow \forall b \in (1 \dots a) (0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) (b) \neq 0))$
408	407	rabbidv	$⊢ j = m \to \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} = \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) (b) \neq 0)\}$
409	408	uneq2d	$⊢ j = m \to \{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} = \{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) (b) \neq 0)\}$
410	409	supeq1d	$⊢ j = m \to sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <) = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <)$
411	410	eqeq2d	$⊢ j = m \to (q = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <) \leftrightarrow q = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <))$
412	411	cbvrexvw	$⊢ \exists j \in (0 \dots N) q = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <) \leftrightarrow \exists m \in (0 \dots N) q = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <)$
413	391 412	bitrdi	$⊢ i = q \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 ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (g (p)) [(j + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <) \leftrightarrow \exists m \in (0 \dots N) q = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <))$
414	389 413	rspc2v	$⊢ (p \in ℕ \land q \in (0 \dots N)) \to (\forall k \in ℕ \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <) \to \exists m \in (0 \dots N) q = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <))$
415	367 414	mpan9	$⊢ (((φ \land g : ℕ ⟶ ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land \forall k \in ℕ (ran 1^{st} (g (k)) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <))) \land (p \in ℕ \land q \in (0 \dots N))) \to \exists m \in (0 \dots N) q = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (b) \land (1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) (b) \neq 0)\} ℝ <)$
416	349 2 3 350 363 364 352 361 415	poimirlem31	$⊢ (((φ \land g : ℕ ⟶ ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land \forall k \in ℕ (ran 1^{st} (g (k)) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <))) \land (p \in ℕ \land n \in (1 \dots N) \land r \in \{\leq \leq^{-1}\})) \to \exists m \in (0 \dots N) 0 r F ((1^{st} (g (p)) +_{f} ((2^{nd} (g (p)) [(1 \dots m)] \times \{1\}) \cup (2^{nd} (g (p)) [(m + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{p\})) (n)$
417	349 2 3 350 351 352 361 416	poimirlem30	$⊢ ((φ \land g : ℕ ⟶ ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \land \forall k \in ℕ (ran 1^{st} (g (k)) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <))) \to \exists c \in I \forall n \in (1 \dots N) \forall v \in (R ↾_{𝑡} I) (c \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n))$
418	417	anasss	$⊢ (φ \land (g : ℕ ⟶ ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \land \forall k \in ℕ (ran 1^{st} (g (k)) \subseteq (0 ..^k) \land \forall i \in (0 \dots N) \exists j \in (0 \dots N) i = sup (\{0\} \cup \{a \in (1 \dots N) \| \forall b \in (1 \dots a) (0 \leq F ((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\}))) \div_{f} ((1 \dots N) \times \{k\})) (b) \land (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\}))) (b) \neq 0)\} ℝ <)))) \to \exists c \in I \forall n \in (1 \dots N) \forall v \in (R ↾_{𝑡} I) (c \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n))$
419	348 418	exlimddv	$⊢ φ \to \exists c \in I \forall n \in (1 \dots N) \forall v \in (R ↾_{𝑡} I) (c \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n))$

Metamath Proof Explorer

Theorem poimirlem32

Proof