rmydioph

Description: jm2.27 restated in terms of Diophantine sets. (Contributed by Stefan O'Rear, 11-Oct-2014) (Revised by Stefan O'Rear, 6-May-2015)

		Ref	Expression
	Assertion	rmydioph	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (1) \in ℤ_{\geq 2} \land a (3) = a (1) Y_{rm} a (2))\} \in Dioph (3)$

Proof

Step	Hyp	Ref	Expression
1		elmapi	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to a : (1 \dots 3) ⟶ ℕ_{0}$
2		2nn	$⊢ 2 \in ℕ$
3	2	jm2.27dlem3	$⊢ 2 \in (1 \dots 2)$
4		df-3	$⊢ 3 = 2 + 1$
5	3 4 2	jm2.27dlem2	$⊢ 2 \in (1 \dots 3)$
6		ffvelcdm	$⊢ (a : (1 \dots 3) ⟶ ℕ_{0} \land 2 \in (1 \dots 3)) \to a (2) \in ℕ_{0}$
7	1 5 6	sylancl	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to a (2) \in ℕ_{0}$
8		elnn0	$⊢ a (2) \in ℕ_{0} \leftrightarrow (a (2) \in ℕ \lor a (2) = 0)$
9	7 8	sylib	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to (a (2) \in ℕ \lor a (2) = 0)$
10		iba	$⊢ (a (2) \in ℕ \lor a (2) = 0) \to (a (3) = a (1) Y_{rm} a (2) \leftrightarrow (a (3) = a (1) Y_{rm} a (2) \land (a (2) \in ℕ \lor a (2) = 0)))$
11		andi	$⊢ (a (3) = a (1) Y_{rm} a (2) \land (a (2) \in ℕ \lor a (2) = 0)) \leftrightarrow ((a (3) = a (1) Y_{rm} a (2) \land a (2) \in ℕ) \lor (a (3) = a (1) Y_{rm} a (2) \land a (2) = 0))$
12	10 11	bitrdi	$⊢ (a (2) \in ℕ \lor a (2) = 0) \to (a (3) = a (1) Y_{rm} a (2) \leftrightarrow ((a (3) = a (1) Y_{rm} a (2) \land a (2) \in ℕ) \lor (a (3) = a (1) Y_{rm} a (2) \land a (2) = 0)))$
13	12	anbi2d	$⊢ (a (2) \in ℕ \lor a (2) = 0) \to ((a (1) \in ℤ_{\geq 2} \land a (3) = a (1) Y_{rm} a (2)) \leftrightarrow (a (1) \in ℤ_{\geq 2} \land ((a (3) = a (1) Y_{rm} a (2) \land a (2) \in ℕ) \lor (a (3) = a (1) Y_{rm} a (2) \land a (2) = 0))))$
14	9 13	syl	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to ((a (1) \in ℤ_{\geq 2} \land a (3) = a (1) Y_{rm} a (2)) \leftrightarrow (a (1) \in ℤ_{\geq 2} \land ((a (3) = a (1) Y_{rm} a (2) \land a (2) \in ℕ) \lor (a (3) = a (1) Y_{rm} a (2) \land a (2) = 0))))$
15		simplr	$⊢ ((a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \land a (2) \in ℕ) \to a (1) \in ℤ_{\geq 2}$
16		nnz	$⊢ a (2) \in ℕ \to a (2) \in ℤ$
17	16	adantl	$⊢ ((a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \land a (2) \in ℕ) \to a (2) \in ℤ$
18		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
19	18	fovcl	$⊢ (a (1) \in ℤ_{\geq 2} \land a (2) \in ℤ) \to a (1) Y_{rm} a (2) \in ℤ$
20	15 17 19	syl2anc	$⊢ ((a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \land a (2) \in ℕ) \to a (1) Y_{rm} a (2) \in ℤ$
21		rmy0	$⊢ a (1) \in ℤ_{\geq 2} \to a (1) Y_{rm} 0 = 0$
22	21	ad2antlr	$⊢ ((a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \land a (2) \in ℕ) \to a (1) Y_{rm} 0 = 0$
23		nngt0	$⊢ a (2) \in ℕ \to 0 < a (2)$
24	23	adantl	$⊢ ((a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \land a (2) \in ℕ) \to 0 < a (2)$
25		0zd	$⊢ ((a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \land a (2) \in ℕ) \to 0 \in ℤ$
26		ltrmy	$⊢ (a (1) \in ℤ_{\geq 2} \land 0 \in ℤ \land a (2) \in ℤ) \to (0 < a (2) \leftrightarrow a (1) Y_{rm} 0 < a (1) Y_{rm} a (2))$
27	15 25 17 26	syl3anc	$⊢ ((a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \land a (2) \in ℕ) \to (0 < a (2) \leftrightarrow a (1) Y_{rm} 0 < a (1) Y_{rm} a (2))$
28	24 27	mpbid	$⊢ ((a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \land a (2) \in ℕ) \to a (1) Y_{rm} 0 < a (1) Y_{rm} a (2)$
29	22 28	eqbrtrrd	$⊢ ((a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \land a (2) \in ℕ) \to 0 < a (1) Y_{rm} a (2)$
30		elnnz	$⊢ a (1) Y_{rm} a (2) \in ℕ \leftrightarrow (a (1) Y_{rm} a (2) \in ℤ \land 0 < a (1) Y_{rm} a (2))$
31	20 29 30	sylanbrc	$⊢ ((a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \land a (2) \in ℕ) \to a (1) Y_{rm} a (2) \in ℕ$
32		eleq1	$⊢ a (3) = a (1) Y_{rm} a (2) \to (a (3) \in ℕ \leftrightarrow a (1) Y_{rm} a (2) \in ℕ)$
33	31 32	syl5ibrcom	$⊢ ((a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \land a (2) \in ℕ) \to (a (3) = a (1) Y_{rm} a (2) \to a (3) \in ℕ)$
34	33	pm4.71rd	$⊢ ((a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \land a (2) \in ℕ) \to (a (3) = a (1) Y_{rm} a (2) \leftrightarrow (a (3) \in ℕ \land a (3) = a (1) Y_{rm} a (2)))$
35		simpllr	$⊢ (((a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \land a (2) \in ℕ) \land a (3) \in ℕ) \to a (1) \in ℤ_{\geq 2}$
36		simplr	$⊢ (((a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \land a (2) \in ℕ) \land a (3) \in ℕ) \to a (2) \in ℕ$
37		simpr	$⊢ (((a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \land a (2) \in ℕ) \land a (3) \in ℕ) \to a (3) \in ℕ$
38		jm2.27	$⊢ (a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ \land a (3) \in ℕ) \to (a (3) = a (1) Y_{rm} a (2) \leftrightarrow \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3)))))$
39	35 36 37 38	syl3anc	$⊢ (((a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \land a (2) \in ℕ) \land a (3) \in ℕ) \to (a (3) = a (1) Y_{rm} a (2) \leftrightarrow \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3)))))$
40	39	pm5.32da	$⊢ ((a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \land a (2) \in ℕ) \to ((a (3) \in ℕ \land a (3) = a (1) Y_{rm} a (2)) \leftrightarrow (a (3) \in ℕ \land \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3))))))$
41	34 40	bitrd	$⊢ ((a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \land a (2) \in ℕ) \to (a (3) = a (1) Y_{rm} a (2) \leftrightarrow (a (3) \in ℕ \land \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3))))))$
42	41	ex	$⊢ (a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \to (a (2) \in ℕ \to (a (3) = a (1) Y_{rm} a (2) \leftrightarrow (a (3) \in ℕ \land \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3)))))))$
43	42	pm5.32rd	$⊢ (a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \to ((a (3) = a (1) Y_{rm} a (2) \land a (2) \in ℕ) \leftrightarrow ((a (3) \in ℕ \land \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3))))) \land a (2) \in ℕ))$
44		oveq2	$⊢ a (2) = 0 \to a (1) Y_{rm} a (2) = a (1) Y_{rm} 0$
45	44	adantl	$⊢ ((a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \land a (2) = 0) \to a (1) Y_{rm} a (2) = a (1) Y_{rm} 0$
46	21	ad2antlr	$⊢ ((a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \land a (2) = 0) \to a (1) Y_{rm} 0 = 0$
47	45 46	eqtrd	$⊢ ((a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \land a (2) = 0) \to a (1) Y_{rm} a (2) = 0$
48	47	eqeq2d	$⊢ ((a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \land a (2) = 0) \to (a (3) = a (1) Y_{rm} a (2) \leftrightarrow a (3) = 0)$
49	48	ex	$⊢ (a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \to (a (2) = 0 \to (a (3) = a (1) Y_{rm} a (2) \leftrightarrow a (3) = 0))$
50	49	pm5.32rd	$⊢ (a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \to ((a (3) = a (1) Y_{rm} a (2) \land a (2) = 0) \leftrightarrow (a (3) = 0 \land a (2) = 0))$
51	43 50	orbi12d	$⊢ (a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \to (((a (3) = a (1) Y_{rm} a (2) \land a (2) \in ℕ) \lor (a (3) = a (1) Y_{rm} a (2) \land a (2) = 0)) \leftrightarrow (((a (3) \in ℕ \land \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3))))) \land a (2) \in ℕ) \lor (a (3) = 0 \land a (2) = 0)))$
52	51	pm5.32da	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to ((a (1) \in ℤ_{\geq 2} \land ((a (3) = a (1) Y_{rm} a (2) \land a (2) \in ℕ) \lor (a (3) = a (1) Y_{rm} a (2) \land a (2) = 0))) \leftrightarrow (a (1) \in ℤ_{\geq 2} \land (((a (3) \in ℕ \land \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3))))) \land a (2) \in ℕ) \lor (a (3) = 0 \land a (2) = 0))))$
53	14 52	bitrd	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to ((a (1) \in ℤ_{\geq 2} \land a (3) = a (1) Y_{rm} a (2)) \leftrightarrow (a (1) \in ℤ_{\geq 2} \land (((a (3) \in ℕ \land \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3))))) \land a (2) \in ℕ) \lor (a (3) = 0 \land a (2) = 0))))$
54	53	rabbiia	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (1) \in ℤ_{\geq 2} \land a (3) = a (1) Y_{rm} a (2))\} = \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (1) \in ℤ_{\geq 2} \land (((a (3) \in ℕ \land \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3))))) \land a (2) \in ℕ) \lor (a (3) = 0 \land a (2) = 0)))\}$
55		3nn0	$⊢ 3 \in ℕ_{0}$
56		2z	$⊢ 2 \in ℤ$
57		ovex	$⊢ (1 \dots 3) \in V$
58		1nn	$⊢ 1 \in ℕ$
59	58	jm2.27dlem3	$⊢ 1 \in (1 \dots 1)$
60		df-2	$⊢ 2 = 1 + 1$
61	59 60 58	jm2.27dlem2	$⊢ 1 \in (1 \dots 2)$
62	61 4 2	jm2.27dlem2	$⊢ 1 \in (1 \dots 3)$
63		mzpproj	$⊢ ((1 \dots 3) \in V \land 1 \in (1 \dots 3)) \to (a \in (ℤ^{(1 \dots 3)}) ⟼ a (1)) \in mzPoly ((1 \dots 3))$
64	57 62 63	mp2an	$⊢ (a \in (ℤ^{(1 \dots 3)}) ⟼ a (1)) \in mzPoly ((1 \dots 3))$
65		eluzrabdioph	$⊢ (3 \in ℕ_{0} \land 2 \in ℤ \land (a \in (ℤ^{(1 \dots 3)}) ⟼ a (1)) \in mzPoly ((1 \dots 3))) \to \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (1) \in ℤ_{\geq 2}\} \in Dioph (3)$
66	55 56 64 65	mp3an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (1) \in ℤ_{\geq 2}\} \in Dioph (3)$
67		3nn	$⊢ 3 \in ℕ$
68	67	jm2.27dlem3	$⊢ 3 \in (1 \dots 3)$
69		mzpproj	$⊢ ((1 \dots 3) \in V \land 3 \in (1 \dots 3)) \to (a \in (ℤ^{(1 \dots 3)}) ⟼ a (3)) \in mzPoly ((1 \dots 3))$
70	57 68 69	mp2an	$⊢ (a \in (ℤ^{(1 \dots 3)}) ⟼ a (3)) \in mzPoly ((1 \dots 3))$
71		elnnrabdioph	$⊢ (3 \in ℕ_{0} \land (a \in (ℤ^{(1 \dots 3)}) ⟼ a (3)) \in mzPoly ((1 \dots 3))) \to \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (3) \in ℕ\} \in Dioph (3)$
72	55 70 71	mp2an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (3) \in ℕ\} \in Dioph (3)$
73		fvex	$⊢ i (8) \in V$
74		fvex	$⊢ i (9) \in V$
75		fvex	$⊢ i (10) \in V$
76		oveq1	$⊢ g = i (9) \to g^{2} = {i (9)}^{2}$
77		oveq1	$⊢ f = i (8) \to f^{2} = {i (8)}^{2}$
78	77	oveq2d	$⊢ f = i (8) \to (e^{2} - 1) f^{2} = (e^{2} - 1) {i (8)}^{2}$
79	76 78	oveqan12rd	$⊢ (f = i (8) \land g = i (9)) \to g^{2} - (e^{2} - 1) f^{2} = {i (9)}^{2} - (e^{2} - 1) {i (8)}^{2}$
80	79	eqeq1d	$⊢ (f = i (8) \land g = i (9)) \to (g^{2} - (e^{2} - 1) f^{2} = 1 \leftrightarrow {i (9)}^{2} - (e^{2} - 1) {i (8)}^{2} = 1)$
81	80	3adant3	$⊢ (f = i (8) \land g = i (9) \land h = i (10)) \to (g^{2} - (e^{2} - 1) f^{2} = 1 \leftrightarrow {i (9)}^{2} - (e^{2} - 1) {i (8)}^{2} = 1)$
82		oveq1	$⊢ h = i (10) \to h + 1 = i (10) + 1$
83	82	oveq1d	$⊢ h = i (10) \to (h + 1) 2 {a (3)}^{2} = (i (10) + 1) 2 {a (3)}^{2}$
84	83	eqeq2d	$⊢ h = i (10) \to (c = (h + 1) 2 {a (3)}^{2} \leftrightarrow c = (i (10) + 1) 2 {a (3)}^{2})$
85	84	3ad2ant3	$⊢ (f = i (8) \land g = i (9) \land h = i (10)) \to (c = (h + 1) 2 {a (3)}^{2} \leftrightarrow c = (i (10) + 1) 2 {a (3)}^{2})$
86	81 85	3anbi12d	$⊢ (f = i (8) \land g = i (9) \land h = i (10)) \to ((g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1))) \leftrightarrow ({i (9)}^{2} - (e^{2} - 1) {i (8)}^{2} = 1 \land c = (i (10) + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1))))$
87	86	anbi2d	$⊢ (f = i (8) \land g = i (9) \land h = i (10)) \to (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \leftrightarrow ((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land ({i (9)}^{2} - (e^{2} - 1) {i (8)}^{2} = 1 \land c = (i (10) + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))))$
88		oveq1	$⊢ f = i (8) \to f - a (3) = i (8) - a (3)$
89	88	breq2d	$⊢ f = i (8) \to (d ∥ (f - a (3)) \leftrightarrow d ∥ (i (8) - a (3)))$
90	89	anbi2d	$⊢ f = i (8) \to ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \leftrightarrow (2 a (3) ∥ (e - 1) \land d ∥ (i (8) - a (3))))$
91		oveq1	$⊢ f = i (8) \to f - a (2) = i (8) - a (2)$
92	91	breq2d	$⊢ f = i (8) \to (2 a (3) ∥ (f - a (2)) \leftrightarrow 2 a (3) ∥ (i (8) - a (2)))$
93	92	anbi1d	$⊢ f = i (8) \to ((2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3)) \leftrightarrow (2 a (3) ∥ (i (8) - a (2)) \land a (2) \leq a (3)))$
94	90 93	anbi12d	$⊢ f = i (8) \to (((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3))) \leftrightarrow ((2 a (3) ∥ (e - 1) \land d ∥ (i (8) - a (3))) \land (2 a (3) ∥ (i (8) - a (2)) \land a (2) \leq a (3))))$
95	94	3ad2ant1	$⊢ (f = i (8) \land g = i (9) \land h = i (10)) \to (((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3))) \leftrightarrow ((2 a (3) ∥ (e - 1) \land d ∥ (i (8) - a (3))) \land (2 a (3) ∥ (i (8) - a (2)) \land a (2) \leq a (3))))$
96	87 95	anbi12d	$⊢ (f = i (8) \land g = i (9) \land h = i (10)) \to ((((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3)))) \leftrightarrow (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land ({i (9)}^{2} - (e^{2} - 1) {i (8)}^{2} = 1 \land c = (i (10) + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (i (8) - a (3))) \land (2 a (3) ∥ (i (8) - a (2)) \land a (2) \leq a (3)))))$
97	73 74 75 96	sbc3ie	$⊢ \underset{˙}{[} i (8) / f \underset{˙}{]} \underset{˙}{[} i (9) / g \underset{˙}{]} \underset{˙}{[} i (10) / h \underset{˙}{]} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3)))) \leftrightarrow (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land ({i (9)}^{2} - (e^{2} - 1) {i (8)}^{2} = 1 \land c = (i (10) + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (i (8) - a (3))) \land (2 a (3) ∥ (i (8) - a (2)) \land a (2) \leq a (3))))$
98	97	sbcbii	$⊢ \underset{˙}{[} i (7) / e \underset{˙}{]} \underset{˙}{[} i (8) / f \underset{˙}{]} \underset{˙}{[} i (9) / g \underset{˙}{]} \underset{˙}{[} i (10) / h \underset{˙}{]} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3)))) \leftrightarrow \underset{˙}{[} i (7) / e \underset{˙}{]} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land ({i (9)}^{2} - (e^{2} - 1) {i (8)}^{2} = 1 \land c = (i (10) + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (i (8) - a (3))) \land (2 a (3) ∥ (i (8) - a (2)) \land a (2) \leq a (3))))$
99	98	sbcbii	$⊢ \underset{˙}{[} i (6) / d \underset{˙}{]} \underset{˙}{[} i (7) / e \underset{˙}{]} \underset{˙}{[} i (8) / f \underset{˙}{]} \underset{˙}{[} i (9) / g \underset{˙}{]} \underset{˙}{[} i (10) / h \underset{˙}{]} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3)))) \leftrightarrow \underset{˙}{[} i (6) / d \underset{˙}{]} \underset{˙}{[} i (7) / e \underset{˙}{]} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land ({i (9)}^{2} - (e^{2} - 1) {i (8)}^{2} = 1 \land c = (i (10) + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (i (8) - a (3))) \land (2 a (3) ∥ (i (8) - a (2)) \land a (2) \leq a (3))))$
100	99	sbcbii	$⊢ \underset{˙}{[} i (5) / c \underset{˙}{]} \underset{˙}{[} i (6) / d \underset{˙}{]} \underset{˙}{[} i (7) / e \underset{˙}{]} \underset{˙}{[} i (8) / f \underset{˙}{]} \underset{˙}{[} i (9) / g \underset{˙}{]} \underset{˙}{[} i (10) / h \underset{˙}{]} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3)))) \leftrightarrow \underset{˙}{[} i (5) / c \underset{˙}{]} \underset{˙}{[} i (6) / d \underset{˙}{]} \underset{˙}{[} i (7) / e \underset{˙}{]} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land ({i (9)}^{2} - (e^{2} - 1) {i (8)}^{2} = 1 \land c = (i (10) + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (i (8) - a (3))) \land (2 a (3) ∥ (i (8) - a (2)) \land a (2) \leq a (3))))$
101	100	sbcbii	$⊢ \underset{˙}{[} i (4) / b \underset{˙}{]} \underset{˙}{[} i (5) / c \underset{˙}{]} \underset{˙}{[} i (6) / d \underset{˙}{]} \underset{˙}{[} i (7) / e \underset{˙}{]} \underset{˙}{[} i (8) / f \underset{˙}{]} \underset{˙}{[} i (9) / g \underset{˙}{]} \underset{˙}{[} i (10) / h \underset{˙}{]} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3)))) \leftrightarrow \underset{˙}{[} i (4) / b \underset{˙}{]} \underset{˙}{[} i (5) / c \underset{˙}{]} \underset{˙}{[} i (6) / d \underset{˙}{]} \underset{˙}{[} i (7) / e \underset{˙}{]} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land ({i (9)}^{2} - (e^{2} - 1) {i (8)}^{2} = 1 \land c = (i (10) + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (i (8) - a (3))) \land (2 a (3) ∥ (i (8) - a (2)) \land a (2) \leq a (3))))$
102	101	sbcbii	$⊢ \underset{˙}{[} ({i ↾}_{(1 \dots 3)}) / a \underset{˙}{]} \underset{˙}{[} i (4) / b \underset{˙}{]} \underset{˙}{[} i (5) / c \underset{˙}{]} \underset{˙}{[} i (6) / d \underset{˙}{]} \underset{˙}{[} i (7) / e \underset{˙}{]} \underset{˙}{[} i (8) / f \underset{˙}{]} \underset{˙}{[} i (9) / g \underset{˙}{]} \underset{˙}{[} i (10) / h \underset{˙}{]} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3)))) \leftrightarrow \underset{˙}{[} ({i ↾}_{(1 \dots 3)}) / a \underset{˙}{]} \underset{˙}{[} i (4) / b \underset{˙}{]} \underset{˙}{[} i (5) / c \underset{˙}{]} \underset{˙}{[} i (6) / d \underset{˙}{]} \underset{˙}{[} i (7) / e \underset{˙}{]} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land ({i (9)}^{2} - (e^{2} - 1) {i (8)}^{2} = 1 \land c = (i (10) + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (i (8) - a (3))) \land (2 a (3) ∥ (i (8) - a (2)) \land a (2) \leq a (3))))$
103		fvex	$⊢ i (5) \in V$
104		fvex	$⊢ i (6) \in V$
105		fvex	$⊢ i (7) \in V$
106		oveq1	$⊢ d = i (6) \to d^{2} = {i (6)}^{2}$
107	106	3ad2ant2	$⊢ (c = i (5) \land d = i (6) \land e = i (7)) \to d^{2} = {i (6)}^{2}$
108		oveq1	$⊢ c = i (5) \to c^{2} = {i (5)}^{2}$
109	108	oveq2d	$⊢ c = i (5) \to ({a (1)}^{2} - 1) c^{2} = ({a (1)}^{2} - 1) {i (5)}^{2}$
110	109	3ad2ant1	$⊢ (c = i (5) \land d = i (6) \land e = i (7)) \to ({a (1)}^{2} - 1) c^{2} = ({a (1)}^{2} - 1) {i (5)}^{2}$
111	107 110	oveq12d	$⊢ (c = i (5) \land d = i (6) \land e = i (7)) \to d^{2} - ({a (1)}^{2} - 1) c^{2} = {i (6)}^{2} - ({a (1)}^{2} - 1) {i (5)}^{2}$
112	111	eqeq1d	$⊢ (c = i (5) \land d = i (6) \land e = i (7)) \to (d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \leftrightarrow {i (6)}^{2} - ({a (1)}^{2} - 1) {i (5)}^{2} = 1)$
113		eleq1	$⊢ e = i (7) \to (e \in ℤ_{\geq 2} \leftrightarrow i (7) \in ℤ_{\geq 2})$
114	113	3ad2ant3	$⊢ (c = i (5) \land d = i (6) \land e = i (7)) \to (e \in ℤ_{\geq 2} \leftrightarrow i (7) \in ℤ_{\geq 2})$
115	112 114	3anbi23d	$⊢ (c = i (5) \land d = i (6) \land e = i (7)) \to ((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \leftrightarrow (b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land {i (6)}^{2} - ({a (1)}^{2} - 1) {i (5)}^{2} = 1 \land i (7) \in ℤ_{\geq 2}))$
116		oveq1	$⊢ e = i (7) \to e^{2} = {i (7)}^{2}$
117	116	oveq1d	$⊢ e = i (7) \to e^{2} - 1 = {i (7)}^{2} - 1$
118	117	oveq1d	$⊢ e = i (7) \to (e^{2} - 1) {i (8)}^{2} = ({i (7)}^{2} - 1) {i (8)}^{2}$
119	118	oveq2d	$⊢ e = i (7) \to {i (9)}^{2} - (e^{2} - 1) {i (8)}^{2} = {i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2}$
120	119	eqeq1d	$⊢ e = i (7) \to ({i (9)}^{2} - (e^{2} - 1) {i (8)}^{2} = 1 \leftrightarrow {i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1)$
121	120	3ad2ant3	$⊢ (c = i (5) \land d = i (6) \land e = i (7)) \to ({i (9)}^{2} - (e^{2} - 1) {i (8)}^{2} = 1 \leftrightarrow {i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1)$
122		eqeq1	$⊢ c = i (5) \to (c = (i (10) + 1) 2 {a (3)}^{2} \leftrightarrow i (5) = (i (10) + 1) 2 {a (3)}^{2})$
123	122	3ad2ant1	$⊢ (c = i (5) \land d = i (6) \land e = i (7)) \to (c = (i (10) + 1) 2 {a (3)}^{2} \leftrightarrow i (5) = (i (10) + 1) 2 {a (3)}^{2})$
124		simp2	$⊢ (c = i (5) \land d = i (6) \land e = i (7)) \to d = i (6)$
125		oveq1	$⊢ e = i (7) \to e - a (1) = i (7) - a (1)$
126	125	3ad2ant3	$⊢ (c = i (5) \land d = i (6) \land e = i (7)) \to e - a (1) = i (7) - a (1)$
127	124 126	breq12d	$⊢ (c = i (5) \land d = i (6) \land e = i (7)) \to (d ∥ (e - a (1)) \leftrightarrow i (6) ∥ (i (7) - a (1)))$
128	121 123 127	3anbi123d	$⊢ (c = i (5) \land d = i (6) \land e = i (7)) \to (({i (9)}^{2} - (e^{2} - 1) {i (8)}^{2} = 1 \land c = (i (10) + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1))) \leftrightarrow ({i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1 \land i (5) = (i (10) + 1) 2 {a (3)}^{2} \land i (6) ∥ (i (7) - a (1))))$
129	115 128	anbi12d	$⊢ (c = i (5) \land d = i (6) \land e = i (7)) \to (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land ({i (9)}^{2} - (e^{2} - 1) {i (8)}^{2} = 1 \land c = (i (10) + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \leftrightarrow ((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land {i (6)}^{2} - ({a (1)}^{2} - 1) {i (5)}^{2} = 1 \land i (7) \in ℤ_{\geq 2}) \land ({i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1 \land i (5) = (i (10) + 1) 2 {a (3)}^{2} \land i (6) ∥ (i (7) - a (1)))))$
130		oveq1	$⊢ e = i (7) \to e - 1 = i (7) - 1$
131	130	breq2d	$⊢ e = i (7) \to (2 a (3) ∥ (e - 1) \leftrightarrow 2 a (3) ∥ (i (7) - 1))$
132		breq1	$⊢ d = i (6) \to (d ∥ (i (8) - a (3)) \leftrightarrow i (6) ∥ (i (8) - a (3)))$
133	131 132	bi2anan9r	$⊢ (d = i (6) \land e = i (7)) \to ((2 a (3) ∥ (e - 1) \land d ∥ (i (8) - a (3))) \leftrightarrow (2 a (3) ∥ (i (7) - 1) \land i (6) ∥ (i (8) - a (3))))$
134	133	anbi1d	$⊢ (d = i (6) \land e = i (7)) \to (((2 a (3) ∥ (e - 1) \land d ∥ (i (8) - a (3))) \land (2 a (3) ∥ (i (8) - a (2)) \land a (2) \leq a (3))) \leftrightarrow ((2 a (3) ∥ (i (7) - 1) \land i (6) ∥ (i (8) - a (3))) \land (2 a (3) ∥ (i (8) - a (2)) \land a (2) \leq a (3))))$
135	134	3adant1	$⊢ (c = i (5) \land d = i (6) \land e = i (7)) \to (((2 a (3) ∥ (e - 1) \land d ∥ (i (8) - a (3))) \land (2 a (3) ∥ (i (8) - a (2)) \land a (2) \leq a (3))) \leftrightarrow ((2 a (3) ∥ (i (7) - 1) \land i (6) ∥ (i (8) - a (3))) \land (2 a (3) ∥ (i (8) - a (2)) \land a (2) \leq a (3))))$
136	129 135	anbi12d	$⊢ (c = i (5) \land d = i (6) \land e = i (7)) \to ((((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land ({i (9)}^{2} - (e^{2} - 1) {i (8)}^{2} = 1 \land c = (i (10) + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (i (8) - a (3))) \land (2 a (3) ∥ (i (8) - a (2)) \land a (2) \leq a (3)))) \leftrightarrow (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land {i (6)}^{2} - ({a (1)}^{2} - 1) {i (5)}^{2} = 1 \land i (7) \in ℤ_{\geq 2}) \land ({i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1 \land i (5) = (i (10) + 1) 2 {a (3)}^{2} \land i (6) ∥ (i (7) - a (1)))) \land ((2 a (3) ∥ (i (7) - 1) \land i (6) ∥ (i (8) - a (3))) \land (2 a (3) ∥ (i (8) - a (2)) \land a (2) \leq a (3)))))$
137	103 104 105 136	sbc3ie	$⊢ \underset{˙}{[} i (5) / c \underset{˙}{]} \underset{˙}{[} i (6) / d \underset{˙}{]} \underset{˙}{[} i (7) / e \underset{˙}{]} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land ({i (9)}^{2} - (e^{2} - 1) {i (8)}^{2} = 1 \land c = (i (10) + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (i (8) - a (3))) \land (2 a (3) ∥ (i (8) - a (2)) \land a (2) \leq a (3)))) \leftrightarrow (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land {i (6)}^{2} - ({a (1)}^{2} - 1) {i (5)}^{2} = 1 \land i (7) \in ℤ_{\geq 2}) \land ({i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1 \land i (5) = (i (10) + 1) 2 {a (3)}^{2} \land i (6) ∥ (i (7) - a (1)))) \land ((2 a (3) ∥ (i (7) - 1) \land i (6) ∥ (i (8) - a (3))) \land (2 a (3) ∥ (i (8) - a (2)) \land a (2) \leq a (3))))$
138	137	sbcbii	$⊢ \underset{˙}{[} i (4) / b \underset{˙}{]} \underset{˙}{[} i (5) / c \underset{˙}{]} \underset{˙}{[} i (6) / d \underset{˙}{]} \underset{˙}{[} i (7) / e \underset{˙}{]} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land ({i (9)}^{2} - (e^{2} - 1) {i (8)}^{2} = 1 \land c = (i (10) + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (i (8) - a (3))) \land (2 a (3) ∥ (i (8) - a (2)) \land a (2) \leq a (3)))) \leftrightarrow \underset{˙}{[} i (4) / b \underset{˙}{]} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land {i (6)}^{2} - ({a (1)}^{2} - 1) {i (5)}^{2} = 1 \land i (7) \in ℤ_{\geq 2}) \land ({i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1 \land i (5) = (i (10) + 1) 2 {a (3)}^{2} \land i (6) ∥ (i (7) - a (1)))) \land ((2 a (3) ∥ (i (7) - 1) \land i (6) ∥ (i (8) - a (3))) \land (2 a (3) ∥ (i (8) - a (2)) \land a (2) \leq a (3))))$
139	138	sbcbii	$⊢ \underset{˙}{[} ({i ↾}_{(1 \dots 3)}) / a \underset{˙}{]} \underset{˙}{[} i (4) / b \underset{˙}{]} \underset{˙}{[} i (5) / c \underset{˙}{]} \underset{˙}{[} i (6) / d \underset{˙}{]} \underset{˙}{[} i (7) / e \underset{˙}{]} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land ({i (9)}^{2} - (e^{2} - 1) {i (8)}^{2} = 1 \land c = (i (10) + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (i (8) - a (3))) \land (2 a (3) ∥ (i (8) - a (2)) \land a (2) \leq a (3)))) \leftrightarrow \underset{˙}{[} ({i ↾}_{(1 \dots 3)}) / a \underset{˙}{]} \underset{˙}{[} i (4) / b \underset{˙}{]} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land {i (6)}^{2} - ({a (1)}^{2} - 1) {i (5)}^{2} = 1 \land i (7) \in ℤ_{\geq 2}) \land ({i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1 \land i (5) = (i (10) + 1) 2 {a (3)}^{2} \land i (6) ∥ (i (7) - a (1)))) \land ((2 a (3) ∥ (i (7) - 1) \land i (6) ∥ (i (8) - a (3))) \land (2 a (3) ∥ (i (8) - a (2)) \land a (2) \leq a (3))))$
140		vex	$⊢ i \in V$
141	140	resex	$⊢ {i ↾}_{(1 \dots 3)} \in V$
142		fvex	$⊢ i (4) \in V$
143		oveq1	$⊢ b = i (4) \to b^{2} = {i (4)}^{2}$
144	62	jm2.27dlem1	$⊢ a = {i ↾}_{(1 \dots 3)} \to a (1) = i (1)$
145	144	oveq1d	$⊢ a = {i ↾}_{(1 \dots 3)} \to {a (1)}^{2} = {i (1)}^{2}$
146	145	oveq1d	$⊢ a = {i ↾}_{(1 \dots 3)} \to {a (1)}^{2} - 1 = {i (1)}^{2} - 1$
147	68	jm2.27dlem1	$⊢ a = {i ↾}_{(1 \dots 3)} \to a (3) = i (3)$
148	147	oveq1d	$⊢ a = {i ↾}_{(1 \dots 3)} \to {a (3)}^{2} = {i (3)}^{2}$
149	146 148	oveq12d	$⊢ a = {i ↾}_{(1 \dots 3)} \to ({a (1)}^{2} - 1) {a (3)}^{2} = ({i (1)}^{2} - 1) {i (3)}^{2}$
150	143 149	oveqan12rd	$⊢ (a = {i ↾}_{(1 \dots 3)} \land b = i (4)) \to b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = {i (4)}^{2} - ({i (1)}^{2} - 1) {i (3)}^{2}$
151	150	eqeq1d	$⊢ (a = {i ↾}_{(1 \dots 3)} \land b = i (4)) \to (b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \leftrightarrow {i (4)}^{2} - ({i (1)}^{2} - 1) {i (3)}^{2} = 1)$
152	146	oveq1d	$⊢ a = {i ↾}_{(1 \dots 3)} \to ({a (1)}^{2} - 1) {i (5)}^{2} = ({i (1)}^{2} - 1) {i (5)}^{2}$
153	152	oveq2d	$⊢ a = {i ↾}_{(1 \dots 3)} \to {i (6)}^{2} - ({a (1)}^{2} - 1) {i (5)}^{2} = {i (6)}^{2} - ({i (1)}^{2} - 1) {i (5)}^{2}$
154	153	eqeq1d	$⊢ a = {i ↾}_{(1 \dots 3)} \to ({i (6)}^{2} - ({a (1)}^{2} - 1) {i (5)}^{2} = 1 \leftrightarrow {i (6)}^{2} - ({i (1)}^{2} - 1) {i (5)}^{2} = 1)$
155	154	adantr	$⊢ (a = {i ↾}_{(1 \dots 3)} \land b = i (4)) \to ({i (6)}^{2} - ({a (1)}^{2} - 1) {i (5)}^{2} = 1 \leftrightarrow {i (6)}^{2} - ({i (1)}^{2} - 1) {i (5)}^{2} = 1)$
156	151 155	3anbi12d	$⊢ (a = {i ↾}_{(1 \dots 3)} \land b = i (4)) \to ((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land {i (6)}^{2} - ({a (1)}^{2} - 1) {i (5)}^{2} = 1 \land i (7) \in ℤ_{\geq 2}) \leftrightarrow ({i (4)}^{2} - ({i (1)}^{2} - 1) {i (3)}^{2} = 1 \land {i (6)}^{2} - ({i (1)}^{2} - 1) {i (5)}^{2} = 1 \land i (7) \in ℤ_{\geq 2}))$
157	148	oveq2d	$⊢ a = {i ↾}_{(1 \dots 3)} \to 2 {a (3)}^{2} = 2 {i (3)}^{2}$
158	157	oveq2d	$⊢ a = {i ↾}_{(1 \dots 3)} \to (i (10) + 1) 2 {a (3)}^{2} = (i (10) + 1) 2 {i (3)}^{2}$
159	158	eqeq2d	$⊢ a = {i ↾}_{(1 \dots 3)} \to (i (5) = (i (10) + 1) 2 {a (3)}^{2} \leftrightarrow i (5) = (i (10) + 1) 2 {i (3)}^{2})$
160	144	oveq2d	$⊢ a = {i ↾}_{(1 \dots 3)} \to i (7) - a (1) = i (7) - i (1)$
161	160	breq2d	$⊢ a = {i ↾}_{(1 \dots 3)} \to (i (6) ∥ (i (7) - a (1)) \leftrightarrow i (6) ∥ (i (7) - i (1)))$
162	159 161	3anbi23d	$⊢ a = {i ↾}_{(1 \dots 3)} \to (({i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1 \land i (5) = (i (10) + 1) 2 {a (3)}^{2} \land i (6) ∥ (i (7) - a (1))) \leftrightarrow ({i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1 \land i (5) = (i (10) + 1) 2 {i (3)}^{2} \land i (6) ∥ (i (7) - i (1))))$
163	162	adantr	$⊢ (a = {i ↾}_{(1 \dots 3)} \land b = i (4)) \to (({i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1 \land i (5) = (i (10) + 1) 2 {a (3)}^{2} \land i (6) ∥ (i (7) - a (1))) \leftrightarrow ({i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1 \land i (5) = (i (10) + 1) 2 {i (3)}^{2} \land i (6) ∥ (i (7) - i (1))))$
164	156 163	anbi12d	$⊢ (a = {i ↾}_{(1 \dots 3)} \land b = i (4)) \to (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land {i (6)}^{2} - ({a (1)}^{2} - 1) {i (5)}^{2} = 1 \land i (7) \in ℤ_{\geq 2}) \land ({i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1 \land i (5) = (i (10) + 1) 2 {a (3)}^{2} \land i (6) ∥ (i (7) - a (1)))) \leftrightarrow (({i (4)}^{2} - ({i (1)}^{2} - 1) {i (3)}^{2} = 1 \land {i (6)}^{2} - ({i (1)}^{2} - 1) {i (5)}^{2} = 1 \land i (7) \in ℤ_{\geq 2}) \land ({i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1 \land i (5) = (i (10) + 1) 2 {i (3)}^{2} \land i (6) ∥ (i (7) - i (1)))))$
165	147	oveq2d	$⊢ a = {i ↾}_{(1 \dots 3)} \to 2 a (3) = 2 i (3)$
166	165	breq1d	$⊢ a = {i ↾}_{(1 \dots 3)} \to (2 a (3) ∥ (i (7) - 1) \leftrightarrow 2 i (3) ∥ (i (7) - 1))$
167	147	oveq2d	$⊢ a = {i ↾}_{(1 \dots 3)} \to i (8) - a (3) = i (8) - i (3)$
168	167	breq2d	$⊢ a = {i ↾}_{(1 \dots 3)} \to (i (6) ∥ (i (8) - a (3)) \leftrightarrow i (6) ∥ (i (8) - i (3)))$
169	166 168	anbi12d	$⊢ a = {i ↾}_{(1 \dots 3)} \to ((2 a (3) ∥ (i (7) - 1) \land i (6) ∥ (i (8) - a (3))) \leftrightarrow (2 i (3) ∥ (i (7) - 1) \land i (6) ∥ (i (8) - i (3))))$
170	5	jm2.27dlem1	$⊢ a = {i ↾}_{(1 \dots 3)} \to a (2) = i (2)$
171	170	oveq2d	$⊢ a = {i ↾}_{(1 \dots 3)} \to i (8) - a (2) = i (8) - i (2)$
172	165 171	breq12d	$⊢ a = {i ↾}_{(1 \dots 3)} \to (2 a (3) ∥ (i (8) - a (2)) \leftrightarrow 2 i (3) ∥ (i (8) - i (2)))$
173	170 147	breq12d	$⊢ a = {i ↾}_{(1 \dots 3)} \to (a (2) \leq a (3) \leftrightarrow i (2) \leq i (3))$
174	172 173	anbi12d	$⊢ a = {i ↾}_{(1 \dots 3)} \to ((2 a (3) ∥ (i (8) - a (2)) \land a (2) \leq a (3)) \leftrightarrow (2 i (3) ∥ (i (8) - i (2)) \land i (2) \leq i (3)))$
175	169 174	anbi12d	$⊢ a = {i ↾}_{(1 \dots 3)} \to (((2 a (3) ∥ (i (7) - 1) \land i (6) ∥ (i (8) - a (3))) \land (2 a (3) ∥ (i (8) - a (2)) \land a (2) \leq a (3))) \leftrightarrow ((2 i (3) ∥ (i (7) - 1) \land i (6) ∥ (i (8) - i (3))) \land (2 i (3) ∥ (i (8) - i (2)) \land i (2) \leq i (3))))$
176	175	adantr	$⊢ (a = {i ↾}_{(1 \dots 3)} \land b = i (4)) \to (((2 a (3) ∥ (i (7) - 1) \land i (6) ∥ (i (8) - a (3))) \land (2 a (3) ∥ (i (8) - a (2)) \land a (2) \leq a (3))) \leftrightarrow ((2 i (3) ∥ (i (7) - 1) \land i (6) ∥ (i (8) - i (3))) \land (2 i (3) ∥ (i (8) - i (2)) \land i (2) \leq i (3))))$
177	164 176	anbi12d	$⊢ (a = {i ↾}_{(1 \dots 3)} \land b = i (4)) \to ((((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land {i (6)}^{2} - ({a (1)}^{2} - 1) {i (5)}^{2} = 1 \land i (7) \in ℤ_{\geq 2}) \land ({i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1 \land i (5) = (i (10) + 1) 2 {a (3)}^{2} \land i (6) ∥ (i (7) - a (1)))) \land ((2 a (3) ∥ (i (7) - 1) \land i (6) ∥ (i (8) - a (3))) \land (2 a (3) ∥ (i (8) - a (2)) \land a (2) \leq a (3)))) \leftrightarrow ((({i (4)}^{2} - ({i (1)}^{2} - 1) {i (3)}^{2} = 1 \land {i (6)}^{2} - ({i (1)}^{2} - 1) {i (5)}^{2} = 1 \land i (7) \in ℤ_{\geq 2}) \land ({i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1 \land i (5) = (i (10) + 1) 2 {i (3)}^{2} \land i (6) ∥ (i (7) - i (1)))) \land ((2 i (3) ∥ (i (7) - 1) \land i (6) ∥ (i (8) - i (3))) \land (2 i (3) ∥ (i (8) - i (2)) \land i (2) \leq i (3)))))$
178	141 142 177	sbc2ie	$⊢ \underset{˙}{[} ({i ↾}_{(1 \dots 3)}) / a \underset{˙}{]} \underset{˙}{[} i (4) / b \underset{˙}{]} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land {i (6)}^{2} - ({a (1)}^{2} - 1) {i (5)}^{2} = 1 \land i (7) \in ℤ_{\geq 2}) \land ({i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1 \land i (5) = (i (10) + 1) 2 {a (3)}^{2} \land i (6) ∥ (i (7) - a (1)))) \land ((2 a (3) ∥ (i (7) - 1) \land i (6) ∥ (i (8) - a (3))) \land (2 a (3) ∥ (i (8) - a (2)) \land a (2) \leq a (3)))) \leftrightarrow ((({i (4)}^{2} - ({i (1)}^{2} - 1) {i (3)}^{2} = 1 \land {i (6)}^{2} - ({i (1)}^{2} - 1) {i (5)}^{2} = 1 \land i (7) \in ℤ_{\geq 2}) \land ({i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1 \land i (5) = (i (10) + 1) 2 {i (3)}^{2} \land i (6) ∥ (i (7) - i (1)))) \land ((2 i (3) ∥ (i (7) - 1) \land i (6) ∥ (i (8) - i (3))) \land (2 i (3) ∥ (i (8) - i (2)) \land i (2) \leq i (3))))$
179	102 139 178	3bitri	$⊢ \underset{˙}{[} ({i ↾}_{(1 \dots 3)}) / a \underset{˙}{]} \underset{˙}{[} i (4) / b \underset{˙}{]} \underset{˙}{[} i (5) / c \underset{˙}{]} \underset{˙}{[} i (6) / d \underset{˙}{]} \underset{˙}{[} i (7) / e \underset{˙}{]} \underset{˙}{[} i (8) / f \underset{˙}{]} \underset{˙}{[} i (9) / g \underset{˙}{]} \underset{˙}{[} i (10) / h \underset{˙}{]} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3)))) \leftrightarrow ((({i (4)}^{2} - ({i (1)}^{2} - 1) {i (3)}^{2} = 1 \land {i (6)}^{2} - ({i (1)}^{2} - 1) {i (5)}^{2} = 1 \land i (7) \in ℤ_{\geq 2}) \land ({i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1 \land i (5) = (i (10) + 1) 2 {i (3)}^{2} \land i (6) ∥ (i (7) - i (1)))) \land ((2 i (3) ∥ (i (7) - 1) \land i (6) ∥ (i (8) - i (3))) \land (2 i (3) ∥ (i (8) - i (2)) \land i (2) \leq i (3))))$
180	179	rabbii	$⊢ \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| \underset{˙}{[} ({i ↾}_{(1 \dots 3)}) / a \underset{˙}{]} \underset{˙}{[} i (4) / b \underset{˙}{]} \underset{˙}{[} i (5) / c \underset{˙}{]} \underset{˙}{[} i (6) / d \underset{˙}{]} \underset{˙}{[} i (7) / e \underset{˙}{]} \underset{˙}{[} i (8) / f \underset{˙}{]} \underset{˙}{[} i (9) / g \underset{˙}{]} \underset{˙}{[} i (10) / h \underset{˙}{]} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3))))\} = \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| ((({i (4)}^{2} - ({i (1)}^{2} - 1) {i (3)}^{2} = 1 \land {i (6)}^{2} - ({i (1)}^{2} - 1) {i (5)}^{2} = 1 \land i (7) \in ℤ_{\geq 2}) \land ({i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1 \land i (5) = (i (10) + 1) 2 {i (3)}^{2} \land i (6) ∥ (i (7) - i (1)))) \land ((2 i (3) ∥ (i (7) - 1) \land i (6) ∥ (i (8) - i (3))) \land (2 i (3) ∥ (i (8) - i (2)) \land i (2) \leq i (3))))\}$
181		10nn0	$⊢ 10 \in ℕ_{0}$
182		ovex	$⊢ (1 \dots 10) \in V$
183		df-5	$⊢ 5 = 4 + 1$
184		df-6	$⊢ 6 = 5 + 1$
185		df-7	$⊢ 7 = 6 + 1$
186		df-8	$⊢ 8 = 7 + 1$
187		df-9	$⊢ 9 = 8 + 1$
188		9p1e10	$⊢ 9 + 1 = 10$
189	188	eqcomi	$⊢ 10 = 9 + 1$
190		ssid	$⊢ (1 \dots 10) \subseteq (1 \dots 10)$
191	189 190	jm2.27dlem5	$⊢ (1 \dots 9) \subseteq (1 \dots 10)$
192	187 191	jm2.27dlem5	$⊢ (1 \dots 8) \subseteq (1 \dots 10)$
193	186 192	jm2.27dlem5	$⊢ (1 \dots 7) \subseteq (1 \dots 10)$
194	185 193	jm2.27dlem5	$⊢ (1 \dots 6) \subseteq (1 \dots 10)$
195	184 194	jm2.27dlem5	$⊢ (1 \dots 5) \subseteq (1 \dots 10)$
196	183 195	jm2.27dlem5	$⊢ (1 \dots 4) \subseteq (1 \dots 10)$
197		4nn	$⊢ 4 \in ℕ$
198	197	jm2.27dlem3	$⊢ 4 \in (1 \dots 4)$
199	196 198	sselii	$⊢ 4 \in (1 \dots 10)$
200		mzpproj	$⊢ ((1 \dots 10) \in V \land 4 \in (1 \dots 10)) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ i (4)) \in mzPoly ((1 \dots 10))$
201	182 199 200	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ i (4)) \in mzPoly ((1 \dots 10))$
202		2nn0	$⊢ 2 \in ℕ_{0}$
203		mzpexpmpt	$⊢ ((i \in (ℤ^{(1 \dots 10)}) ⟼ i (4)) \in mzPoly ((1 \dots 10)) \land 2 \in ℕ_{0}) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (4)}^{2}) \in mzPoly ((1 \dots 10))$
204	201 202 203	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (4)}^{2}) \in mzPoly ((1 \dots 10))$
205		df-4	$⊢ 4 = 3 + 1$
206	205 196	jm2.27dlem5	$⊢ (1 \dots 3) \subseteq (1 \dots 10)$
207	4 206	jm2.27dlem5	$⊢ (1 \dots 2) \subseteq (1 \dots 10)$
208	60 207	jm2.27dlem5	$⊢ (1 \dots 1) \subseteq (1 \dots 10)$
209	208 59	sselii	$⊢ 1 \in (1 \dots 10)$
210		mzpproj	$⊢ ((1 \dots 10) \in V \land 1 \in (1 \dots 10)) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ i (1)) \in mzPoly ((1 \dots 10))$
211	182 209 210	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ i (1)) \in mzPoly ((1 \dots 10))$
212		mzpexpmpt	$⊢ ((i \in (ℤ^{(1 \dots 10)}) ⟼ i (1)) \in mzPoly ((1 \dots 10)) \land 2 \in ℕ_{0}) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (1)}^{2}) \in mzPoly ((1 \dots 10))$
213	211 202 212	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (1)}^{2}) \in mzPoly ((1 \dots 10))$
214		1z	$⊢ 1 \in ℤ$
215		mzpconstmpt	$⊢ ((1 \dots 10) \in V \land 1 \in ℤ) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ 1) \in mzPoly ((1 \dots 10))$
216	182 214 215	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ 1) \in mzPoly ((1 \dots 10))$
217		mzpsubmpt	$⊢ ((i \in (ℤ^{(1 \dots 10)}) ⟼ {i (1)}^{2}) \in mzPoly ((1 \dots 10)) \land (i \in (ℤ^{(1 \dots 10)}) ⟼ 1) \in mzPoly ((1 \dots 10))) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (1)}^{2} - 1) \in mzPoly ((1 \dots 10))$
218	213 216 217	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (1)}^{2} - 1) \in mzPoly ((1 \dots 10))$
219	206 68	sselii	$⊢ 3 \in (1 \dots 10)$
220		mzpproj	$⊢ ((1 \dots 10) \in V \land 3 \in (1 \dots 10)) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ i (3)) \in mzPoly ((1 \dots 10))$
221	182 219 220	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ i (3)) \in mzPoly ((1 \dots 10))$
222		mzpexpmpt	$⊢ ((i \in (ℤ^{(1 \dots 10)}) ⟼ i (3)) \in mzPoly ((1 \dots 10)) \land 2 \in ℕ_{0}) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (3)}^{2}) \in mzPoly ((1 \dots 10))$
223	221 202 222	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (3)}^{2}) \in mzPoly ((1 \dots 10))$
224		mzpmulmpt	$⊢ ((i \in (ℤ^{(1 \dots 10)}) ⟼ {i (1)}^{2} - 1) \in mzPoly ((1 \dots 10)) \land (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (3)}^{2}) \in mzPoly ((1 \dots 10))) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ ({i (1)}^{2} - 1) {i (3)}^{2}) \in mzPoly ((1 \dots 10))$
225	218 223 224	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ ({i (1)}^{2} - 1) {i (3)}^{2}) \in mzPoly ((1 \dots 10))$
226		mzpsubmpt	$⊢ ((i \in (ℤ^{(1 \dots 10)}) ⟼ {i (4)}^{2}) \in mzPoly ((1 \dots 10)) \land (i \in (ℤ^{(1 \dots 10)}) ⟼ ({i (1)}^{2} - 1) {i (3)}^{2}) \in mzPoly ((1 \dots 10))) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (4)}^{2} - ({i (1)}^{2} - 1) {i (3)}^{2}) \in mzPoly ((1 \dots 10))$
227	204 225 226	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (4)}^{2} - ({i (1)}^{2} - 1) {i (3)}^{2}) \in mzPoly ((1 \dots 10))$
228		eqrabdioph	$⊢ (10 \in ℕ_{0} \land (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (4)}^{2} - ({i (1)}^{2} - 1) {i (3)}^{2}) \in mzPoly ((1 \dots 10)) \land (i \in (ℤ^{(1 \dots 10)}) ⟼ 1) \in mzPoly ((1 \dots 10))) \to \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| {i (4)}^{2} - ({i (1)}^{2} - 1) {i (3)}^{2} = 1\} \in Dioph (10)$
229	181 227 216 228	mp3an	$⊢ \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| {i (4)}^{2} - ({i (1)}^{2} - 1) {i (3)}^{2} = 1\} \in Dioph (10)$
230		6nn	$⊢ 6 \in ℕ$
231	230	jm2.27dlem3	$⊢ 6 \in (1 \dots 6)$
232	194 231	sselii	$⊢ 6 \in (1 \dots 10)$
233		mzpproj	$⊢ ((1 \dots 10) \in V \land 6 \in (1 \dots 10)) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ i (6)) \in mzPoly ((1 \dots 10))$
234	182 232 233	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ i (6)) \in mzPoly ((1 \dots 10))$
235		mzpexpmpt	$⊢ ((i \in (ℤ^{(1 \dots 10)}) ⟼ i (6)) \in mzPoly ((1 \dots 10)) \land 2 \in ℕ_{0}) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (6)}^{2}) \in mzPoly ((1 \dots 10))$
236	234 202 235	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (6)}^{2}) \in mzPoly ((1 \dots 10))$
237		5nn	$⊢ 5 \in ℕ$
238	237	jm2.27dlem3	$⊢ 5 \in (1 \dots 5)$
239	195 238	sselii	$⊢ 5 \in (1 \dots 10)$
240		mzpproj	$⊢ ((1 \dots 10) \in V \land 5 \in (1 \dots 10)) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ i (5)) \in mzPoly ((1 \dots 10))$
241	182 239 240	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ i (5)) \in mzPoly ((1 \dots 10))$
242		mzpexpmpt	$⊢ ((i \in (ℤ^{(1 \dots 10)}) ⟼ i (5)) \in mzPoly ((1 \dots 10)) \land 2 \in ℕ_{0}) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (5)}^{2}) \in mzPoly ((1 \dots 10))$
243	241 202 242	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (5)}^{2}) \in mzPoly ((1 \dots 10))$
244		mzpmulmpt	$⊢ ((i \in (ℤ^{(1 \dots 10)}) ⟼ {i (1)}^{2} - 1) \in mzPoly ((1 \dots 10)) \land (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (5)}^{2}) \in mzPoly ((1 \dots 10))) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ ({i (1)}^{2} - 1) {i (5)}^{2}) \in mzPoly ((1 \dots 10))$
245	218 243 244	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ ({i (1)}^{2} - 1) {i (5)}^{2}) \in mzPoly ((1 \dots 10))$
246		mzpsubmpt	$⊢ ((i \in (ℤ^{(1 \dots 10)}) ⟼ {i (6)}^{2}) \in mzPoly ((1 \dots 10)) \land (i \in (ℤ^{(1 \dots 10)}) ⟼ ({i (1)}^{2} - 1) {i (5)}^{2}) \in mzPoly ((1 \dots 10))) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (6)}^{2} - ({i (1)}^{2} - 1) {i (5)}^{2}) \in mzPoly ((1 \dots 10))$
247	236 245 246	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (6)}^{2} - ({i (1)}^{2} - 1) {i (5)}^{2}) \in mzPoly ((1 \dots 10))$
248		eqrabdioph	$⊢ (10 \in ℕ_{0} \land (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (6)}^{2} - ({i (1)}^{2} - 1) {i (5)}^{2}) \in mzPoly ((1 \dots 10)) \land (i \in (ℤ^{(1 \dots 10)}) ⟼ 1) \in mzPoly ((1 \dots 10))) \to \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| {i (6)}^{2} - ({i (1)}^{2} - 1) {i (5)}^{2} = 1\} \in Dioph (10)$
249	181 247 216 248	mp3an	$⊢ \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| {i (6)}^{2} - ({i (1)}^{2} - 1) {i (5)}^{2} = 1\} \in Dioph (10)$
250		7nn	$⊢ 7 \in ℕ$
251	250	jm2.27dlem3	$⊢ 7 \in (1 \dots 7)$
252	193 251	sselii	$⊢ 7 \in (1 \dots 10)$
253		mzpproj	$⊢ ((1 \dots 10) \in V \land 7 \in (1 \dots 10)) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ i (7)) \in mzPoly ((1 \dots 10))$
254	182 252 253	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ i (7)) \in mzPoly ((1 \dots 10))$
255		eluzrabdioph	$⊢ (10 \in ℕ_{0} \land 2 \in ℤ \land (i \in (ℤ^{(1 \dots 10)}) ⟼ i (7)) \in mzPoly ((1 \dots 10))) \to \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| i (7) \in ℤ_{\geq 2}\} \in Dioph (10)$
256	181 56 254 255	mp3an	$⊢ \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| i (7) \in ℤ_{\geq 2}\} \in Dioph (10)$
257		3anrabdioph	$⊢ (\{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| {i (4)}^{2} - ({i (1)}^{2} - 1) {i (3)}^{2} = 1\} \in Dioph (10) \land \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| {i (6)}^{2} - ({i (1)}^{2} - 1) {i (5)}^{2} = 1\} \in Dioph (10) \land \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| i (7) \in ℤ_{\geq 2}\} \in Dioph (10)) \to \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| ({i (4)}^{2} - ({i (1)}^{2} - 1) {i (3)}^{2} = 1 \land {i (6)}^{2} - ({i (1)}^{2} - 1) {i (5)}^{2} = 1 \land i (7) \in ℤ_{\geq 2})\} \in Dioph (10)$
258	229 249 256 257	mp3an	$⊢ \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| ({i (4)}^{2} - ({i (1)}^{2} - 1) {i (3)}^{2} = 1 \land {i (6)}^{2} - ({i (1)}^{2} - 1) {i (5)}^{2} = 1 \land i (7) \in ℤ_{\geq 2})\} \in Dioph (10)$
259		9nn	$⊢ 9 \in ℕ$
260	259	jm2.27dlem3	$⊢ 9 \in (1 \dots 9)$
261	260 189 259	jm2.27dlem2	$⊢ 9 \in (1 \dots 10)$
262		mzpproj	$⊢ ((1 \dots 10) \in V \land 9 \in (1 \dots 10)) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ i (9)) \in mzPoly ((1 \dots 10))$
263	182 261 262	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ i (9)) \in mzPoly ((1 \dots 10))$
264		mzpexpmpt	$⊢ ((i \in (ℤ^{(1 \dots 10)}) ⟼ i (9)) \in mzPoly ((1 \dots 10)) \land 2 \in ℕ_{0}) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (9)}^{2}) \in mzPoly ((1 \dots 10))$
265	263 202 264	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (9)}^{2}) \in mzPoly ((1 \dots 10))$
266		mzpexpmpt	$⊢ ((i \in (ℤ^{(1 \dots 10)}) ⟼ i (7)) \in mzPoly ((1 \dots 10)) \land 2 \in ℕ_{0}) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (7)}^{2}) \in mzPoly ((1 \dots 10))$
267	254 202 266	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (7)}^{2}) \in mzPoly ((1 \dots 10))$
268		mzpsubmpt	$⊢ ((i \in (ℤ^{(1 \dots 10)}) ⟼ {i (7)}^{2}) \in mzPoly ((1 \dots 10)) \land (i \in (ℤ^{(1 \dots 10)}) ⟼ 1) \in mzPoly ((1 \dots 10))) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (7)}^{2} - 1) \in mzPoly ((1 \dots 10))$
269	267 216 268	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (7)}^{2} - 1) \in mzPoly ((1 \dots 10))$
270		8nn	$⊢ 8 \in ℕ$
271	270	jm2.27dlem3	$⊢ 8 \in (1 \dots 8)$
272	192 271	sselii	$⊢ 8 \in (1 \dots 10)$
273		mzpproj	$⊢ ((1 \dots 10) \in V \land 8 \in (1 \dots 10)) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ i (8)) \in mzPoly ((1 \dots 10))$
274	182 272 273	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ i (8)) \in mzPoly ((1 \dots 10))$
275		mzpexpmpt	$⊢ ((i \in (ℤ^{(1 \dots 10)}) ⟼ i (8)) \in mzPoly ((1 \dots 10)) \land 2 \in ℕ_{0}) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (8)}^{2}) \in mzPoly ((1 \dots 10))$
276	274 202 275	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (8)}^{2}) \in mzPoly ((1 \dots 10))$
277		mzpmulmpt	$⊢ ((i \in (ℤ^{(1 \dots 10)}) ⟼ {i (7)}^{2} - 1) \in mzPoly ((1 \dots 10)) \land (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (8)}^{2}) \in mzPoly ((1 \dots 10))) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ ({i (7)}^{2} - 1) {i (8)}^{2}) \in mzPoly ((1 \dots 10))$
278	269 276 277	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ ({i (7)}^{2} - 1) {i (8)}^{2}) \in mzPoly ((1 \dots 10))$
279		mzpsubmpt	$⊢ ((i \in (ℤ^{(1 \dots 10)}) ⟼ {i (9)}^{2}) \in mzPoly ((1 \dots 10)) \land (i \in (ℤ^{(1 \dots 10)}) ⟼ ({i (7)}^{2} - 1) {i (8)}^{2}) \in mzPoly ((1 \dots 10))) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2}) \in mzPoly ((1 \dots 10))$
280	265 278 279	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2}) \in mzPoly ((1 \dots 10))$
281		eqrabdioph	$⊢ (10 \in ℕ_{0} \land (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2}) \in mzPoly ((1 \dots 10)) \land (i \in (ℤ^{(1 \dots 10)}) ⟼ 1) \in mzPoly ((1 \dots 10))) \to \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| {i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1\} \in Dioph (10)$
282	181 280 216 281	mp3an	$⊢ \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| {i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1\} \in Dioph (10)$
283		10nn	$⊢ 10 \in ℕ$
284	283	jm2.27dlem3	$⊢ 10 \in (1 \dots 10)$
285		mzpproj	$⊢ ((1 \dots 10) \in V \land 10 \in (1 \dots 10)) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ i (10)) \in mzPoly ((1 \dots 10))$
286	182 284 285	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ i (10)) \in mzPoly ((1 \dots 10))$
287		mzpaddmpt	$⊢ ((i \in (ℤ^{(1 \dots 10)}) ⟼ i (10)) \in mzPoly ((1 \dots 10)) \land (i \in (ℤ^{(1 \dots 10)}) ⟼ 1) \in mzPoly ((1 \dots 10))) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ i (10) + 1) \in mzPoly ((1 \dots 10))$
288	286 216 287	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ i (10) + 1) \in mzPoly ((1 \dots 10))$
289		mzpconstmpt	$⊢ ((1 \dots 10) \in V \land 2 \in ℤ) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ 2) \in mzPoly ((1 \dots 10))$
290	182 56 289	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ 2) \in mzPoly ((1 \dots 10))$
291		mzpmulmpt	$⊢ ((i \in (ℤ^{(1 \dots 10)}) ⟼ 2) \in mzPoly ((1 \dots 10)) \land (i \in (ℤ^{(1 \dots 10)}) ⟼ {i (3)}^{2}) \in mzPoly ((1 \dots 10))) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ 2 {i (3)}^{2}) \in mzPoly ((1 \dots 10))$
292	290 223 291	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ 2 {i (3)}^{2}) \in mzPoly ((1 \dots 10))$
293		mzpmulmpt	$⊢ ((i \in (ℤ^{(1 \dots 10)}) ⟼ i (10) + 1) \in mzPoly ((1 \dots 10)) \land (i \in (ℤ^{(1 \dots 10)}) ⟼ 2 {i (3)}^{2}) \in mzPoly ((1 \dots 10))) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ (i (10) + 1) 2 {i (3)}^{2}) \in mzPoly ((1 \dots 10))$
294	288 292 293	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ (i (10) + 1) 2 {i (3)}^{2}) \in mzPoly ((1 \dots 10))$
295		eqrabdioph	$⊢ (10 \in ℕ_{0} \land (i \in (ℤ^{(1 \dots 10)}) ⟼ i (5)) \in mzPoly ((1 \dots 10)) \land (i \in (ℤ^{(1 \dots 10)}) ⟼ (i (10) + 1) 2 {i (3)}^{2}) \in mzPoly ((1 \dots 10))) \to \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| i (5) = (i (10) + 1) 2 {i (3)}^{2}\} \in Dioph (10)$
296	181 241 294 295	mp3an	$⊢ \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| i (5) = (i (10) + 1) 2 {i (3)}^{2}\} \in Dioph (10)$
297		mzpsubmpt	$⊢ ((i \in (ℤ^{(1 \dots 10)}) ⟼ i (7)) \in mzPoly ((1 \dots 10)) \land (i \in (ℤ^{(1 \dots 10)}) ⟼ i (1)) \in mzPoly ((1 \dots 10))) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ i (7) - i (1)) \in mzPoly ((1 \dots 10))$
298	254 211 297	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ i (7) - i (1)) \in mzPoly ((1 \dots 10))$
299		dvdsrabdioph	$⊢ (10 \in ℕ_{0} \land (i \in (ℤ^{(1 \dots 10)}) ⟼ i (6)) \in mzPoly ((1 \dots 10)) \land (i \in (ℤ^{(1 \dots 10)}) ⟼ i (7) - i (1)) \in mzPoly ((1 \dots 10))) \to \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| i (6) ∥ (i (7) - i (1))\} \in Dioph (10)$
300	181 234 298 299	mp3an	$⊢ \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| i (6) ∥ (i (7) - i (1))\} \in Dioph (10)$
301		3anrabdioph	$⊢ (\{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| {i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1\} \in Dioph (10) \land \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| i (5) = (i (10) + 1) 2 {i (3)}^{2}\} \in Dioph (10) \land \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| i (6) ∥ (i (7) - i (1))\} \in Dioph (10)) \to \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| ({i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1 \land i (5) = (i (10) + 1) 2 {i (3)}^{2} \land i (6) ∥ (i (7) - i (1)))\} \in Dioph (10)$
302	282 296 300 301	mp3an	$⊢ \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| ({i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1 \land i (5) = (i (10) + 1) 2 {i (3)}^{2} \land i (6) ∥ (i (7) - i (1)))\} \in Dioph (10)$
303		anrabdioph	$⊢ (\{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| ({i (4)}^{2} - ({i (1)}^{2} - 1) {i (3)}^{2} = 1 \land {i (6)}^{2} - ({i (1)}^{2} - 1) {i (5)}^{2} = 1 \land i (7) \in ℤ_{\geq 2})\} \in Dioph (10) \land \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| ({i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1 \land i (5) = (i (10) + 1) 2 {i (3)}^{2} \land i (6) ∥ (i (7) - i (1)))\} \in Dioph (10)) \to \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| (({i (4)}^{2} - ({i (1)}^{2} - 1) {i (3)}^{2} = 1 \land {i (6)}^{2} - ({i (1)}^{2} - 1) {i (5)}^{2} = 1 \land i (7) \in ℤ_{\geq 2}) \land ({i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1 \land i (5) = (i (10) + 1) 2 {i (3)}^{2} \land i (6) ∥ (i (7) - i (1))))\} \in Dioph (10)$
304	258 302 303	mp2an	$⊢ \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| (({i (4)}^{2} - ({i (1)}^{2} - 1) {i (3)}^{2} = 1 \land {i (6)}^{2} - ({i (1)}^{2} - 1) {i (5)}^{2} = 1 \land i (7) \in ℤ_{\geq 2}) \land ({i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1 \land i (5) = (i (10) + 1) 2 {i (3)}^{2} \land i (6) ∥ (i (7) - i (1))))\} \in Dioph (10)$
305		mzpmulmpt	$⊢ ((i \in (ℤ^{(1 \dots 10)}) ⟼ 2) \in mzPoly ((1 \dots 10)) \land (i \in (ℤ^{(1 \dots 10)}) ⟼ i (3)) \in mzPoly ((1 \dots 10))) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ 2 i (3)) \in mzPoly ((1 \dots 10))$
306	290 221 305	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ 2 i (3)) \in mzPoly ((1 \dots 10))$
307		mzpsubmpt	$⊢ ((i \in (ℤ^{(1 \dots 10)}) ⟼ i (7)) \in mzPoly ((1 \dots 10)) \land (i \in (ℤ^{(1 \dots 10)}) ⟼ 1) \in mzPoly ((1 \dots 10))) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ i (7) - 1) \in mzPoly ((1 \dots 10))$
308	254 216 307	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ i (7) - 1) \in mzPoly ((1 \dots 10))$
309		dvdsrabdioph	$⊢ (10 \in ℕ_{0} \land (i \in (ℤ^{(1 \dots 10)}) ⟼ 2 i (3)) \in mzPoly ((1 \dots 10)) \land (i \in (ℤ^{(1 \dots 10)}) ⟼ i (7) - 1) \in mzPoly ((1 \dots 10))) \to \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| 2 i (3) ∥ (i (7) - 1)\} \in Dioph (10)$
310	181 306 308 309	mp3an	$⊢ \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| 2 i (3) ∥ (i (7) - 1)\} \in Dioph (10)$
311		mzpsubmpt	$⊢ ((i \in (ℤ^{(1 \dots 10)}) ⟼ i (8)) \in mzPoly ((1 \dots 10)) \land (i \in (ℤ^{(1 \dots 10)}) ⟼ i (3)) \in mzPoly ((1 \dots 10))) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ i (8) - i (3)) \in mzPoly ((1 \dots 10))$
312	274 221 311	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ i (8) - i (3)) \in mzPoly ((1 \dots 10))$
313		dvdsrabdioph	$⊢ (10 \in ℕ_{0} \land (i \in (ℤ^{(1 \dots 10)}) ⟼ i (6)) \in mzPoly ((1 \dots 10)) \land (i \in (ℤ^{(1 \dots 10)}) ⟼ i (8) - i (3)) \in mzPoly ((1 \dots 10))) \to \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| i (6) ∥ (i (8) - i (3))\} \in Dioph (10)$
314	181 234 312 313	mp3an	$⊢ \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| i (6) ∥ (i (8) - i (3))\} \in Dioph (10)$
315		anrabdioph	$⊢ (\{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| 2 i (3) ∥ (i (7) - 1)\} \in Dioph (10) \land \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| i (6) ∥ (i (8) - i (3))\} \in Dioph (10)) \to \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| (2 i (3) ∥ (i (7) - 1) \land i (6) ∥ (i (8) - i (3)))\} \in Dioph (10)$
316	310 314 315	mp2an	$⊢ \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| (2 i (3) ∥ (i (7) - 1) \land i (6) ∥ (i (8) - i (3)))\} \in Dioph (10)$
317	207 3	sselii	$⊢ 2 \in (1 \dots 10)$
318		mzpproj	$⊢ ((1 \dots 10) \in V \land 2 \in (1 \dots 10)) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ i (2)) \in mzPoly ((1 \dots 10))$
319	182 317 318	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ i (2)) \in mzPoly ((1 \dots 10))$
320		mzpsubmpt	$⊢ ((i \in (ℤ^{(1 \dots 10)}) ⟼ i (8)) \in mzPoly ((1 \dots 10)) \land (i \in (ℤ^{(1 \dots 10)}) ⟼ i (2)) \in mzPoly ((1 \dots 10))) \to (i \in (ℤ^{(1 \dots 10)}) ⟼ i (8) - i (2)) \in mzPoly ((1 \dots 10))$
321	274 319 320	mp2an	$⊢ (i \in (ℤ^{(1 \dots 10)}) ⟼ i (8) - i (2)) \in mzPoly ((1 \dots 10))$
322		dvdsrabdioph	$⊢ (10 \in ℕ_{0} \land (i \in (ℤ^{(1 \dots 10)}) ⟼ 2 i (3)) \in mzPoly ((1 \dots 10)) \land (i \in (ℤ^{(1 \dots 10)}) ⟼ i (8) - i (2)) \in mzPoly ((1 \dots 10))) \to \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| 2 i (3) ∥ (i (8) - i (2))\} \in Dioph (10)$
323	181 306 321 322	mp3an	$⊢ \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| 2 i (3) ∥ (i (8) - i (2))\} \in Dioph (10)$
324		lerabdioph	$⊢ (10 \in ℕ_{0} \land (i \in (ℤ^{(1 \dots 10)}) ⟼ i (2)) \in mzPoly ((1 \dots 10)) \land (i \in (ℤ^{(1 \dots 10)}) ⟼ i (3)) \in mzPoly ((1 \dots 10))) \to \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| i (2) \leq i (3)\} \in Dioph (10)$
325	181 319 221 324	mp3an	$⊢ \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| i (2) \leq i (3)\} \in Dioph (10)$
326		anrabdioph	$⊢ (\{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| 2 i (3) ∥ (i (8) - i (2))\} \in Dioph (10) \land \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| i (2) \leq i (3)\} \in Dioph (10)) \to \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| (2 i (3) ∥ (i (8) - i (2)) \land i (2) \leq i (3))\} \in Dioph (10)$
327	323 325 326	mp2an	$⊢ \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| (2 i (3) ∥ (i (8) - i (2)) \land i (2) \leq i (3))\} \in Dioph (10)$
328		anrabdioph	$⊢ (\{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| (2 i (3) ∥ (i (7) - 1) \land i (6) ∥ (i (8) - i (3)))\} \in Dioph (10) \land \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| (2 i (3) ∥ (i (8) - i (2)) \land i (2) \leq i (3))\} \in Dioph (10)) \to \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| ((2 i (3) ∥ (i (7) - 1) \land i (6) ∥ (i (8) - i (3))) \land (2 i (3) ∥ (i (8) - i (2)) \land i (2) \leq i (3)))\} \in Dioph (10)$
329	316 327 328	mp2an	$⊢ \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| ((2 i (3) ∥ (i (7) - 1) \land i (6) ∥ (i (8) - i (3))) \land (2 i (3) ∥ (i (8) - i (2)) \land i (2) \leq i (3)))\} \in Dioph (10)$
330		anrabdioph	$⊢ (\{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| (({i (4)}^{2} - ({i (1)}^{2} - 1) {i (3)}^{2} = 1 \land {i (6)}^{2} - ({i (1)}^{2} - 1) {i (5)}^{2} = 1 \land i (7) \in ℤ_{\geq 2}) \land ({i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1 \land i (5) = (i (10) + 1) 2 {i (3)}^{2} \land i (6) ∥ (i (7) - i (1))))\} \in Dioph (10) \land \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| ((2 i (3) ∥ (i (7) - 1) \land i (6) ∥ (i (8) - i (3))) \land (2 i (3) ∥ (i (8) - i (2)) \land i (2) \leq i (3)))\} \in Dioph (10)) \to \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| ((({i (4)}^{2} - ({i (1)}^{2} - 1) {i (3)}^{2} = 1 \land {i (6)}^{2} - ({i (1)}^{2} - 1) {i (5)}^{2} = 1 \land i (7) \in ℤ_{\geq 2}) \land ({i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1 \land i (5) = (i (10) + 1) 2 {i (3)}^{2} \land i (6) ∥ (i (7) - i (1)))) \land ((2 i (3) ∥ (i (7) - 1) \land i (6) ∥ (i (8) - i (3))) \land (2 i (3) ∥ (i (8) - i (2)) \land i (2) \leq i (3))))\} \in Dioph (10)$
331	304 329 330	mp2an	$⊢ \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| ((({i (4)}^{2} - ({i (1)}^{2} - 1) {i (3)}^{2} = 1 \land {i (6)}^{2} - ({i (1)}^{2} - 1) {i (5)}^{2} = 1 \land i (7) \in ℤ_{\geq 2}) \land ({i (9)}^{2} - ({i (7)}^{2} - 1) {i (8)}^{2} = 1 \land i (5) = (i (10) + 1) 2 {i (3)}^{2} \land i (6) ∥ (i (7) - i (1)))) \land ((2 i (3) ∥ (i (7) - 1) \land i (6) ∥ (i (8) - i (3))) \land (2 i (3) ∥ (i (8) - i (2)) \land i (2) \leq i (3))))\} \in Dioph (10)$
332	180 331	eqeltri	$⊢ \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| \underset{˙}{[} ({i ↾}_{(1 \dots 3)}) / a \underset{˙}{]} \underset{˙}{[} i (4) / b \underset{˙}{]} \underset{˙}{[} i (5) / c \underset{˙}{]} \underset{˙}{[} i (6) / d \underset{˙}{]} \underset{˙}{[} i (7) / e \underset{˙}{]} \underset{˙}{[} i (8) / f \underset{˙}{]} \underset{˙}{[} i (9) / g \underset{˙}{]} \underset{˙}{[} i (10) / h \underset{˙}{]} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3))))\} \in Dioph (10)$
333	205 183 184 185 186 187 189	7rexfrabdioph	$⊢ (3 \in ℕ_{0} \land \{i \in ({ℕ_{0}}^{(1 \dots 10)}) \| \underset{˙}{[} ({i ↾}_{(1 \dots 3)}) / a \underset{˙}{]} \underset{˙}{[} i (4) / b \underset{˙}{]} \underset{˙}{[} i (5) / c \underset{˙}{]} \underset{˙}{[} i (6) / d \underset{˙}{]} \underset{˙}{[} i (7) / e \underset{˙}{]} \underset{˙}{[} i (8) / f \underset{˙}{]} \underset{˙}{[} i (9) / g \underset{˙}{]} \underset{˙}{[} i (10) / h \underset{˙}{]} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3))))\} \in Dioph (10)) \to \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3))))\} \in Dioph (3)$
334	55 332 333	mp2an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3))))\} \in Dioph (3)$
335		anrabdioph	$⊢ (\{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (3) \in ℕ\} \in Dioph (3) \land \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3))))\} \in Dioph (3)) \to \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (3) \in ℕ \land \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3)))))\} \in Dioph (3)$
336	72 334 335	mp2an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (3) \in ℕ \land \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3)))))\} \in Dioph (3)$
337		mzpproj	$⊢ ((1 \dots 3) \in V \land 2 \in (1 \dots 3)) \to (a \in (ℤ^{(1 \dots 3)}) ⟼ a (2)) \in mzPoly ((1 \dots 3))$
338	57 5 337	mp2an	$⊢ (a \in (ℤ^{(1 \dots 3)}) ⟼ a (2)) \in mzPoly ((1 \dots 3))$
339		elnnrabdioph	$⊢ (3 \in ℕ_{0} \land (a \in (ℤ^{(1 \dots 3)}) ⟼ a (2)) \in mzPoly ((1 \dots 3))) \to \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (2) \in ℕ\} \in Dioph (3)$
340	55 338 339	mp2an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (2) \in ℕ\} \in Dioph (3)$
341		anrabdioph	$⊢ (\{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (3) \in ℕ \land \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3)))))\} \in Dioph (3) \land \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (2) \in ℕ\} \in Dioph (3)) \to \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| ((a (3) \in ℕ \land \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3))))) \land a (2) \in ℕ)\} \in Dioph (3)$
342	336 340 341	mp2an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| ((a (3) \in ℕ \land \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3))))) \land a (2) \in ℕ)\} \in Dioph (3)$
343		eq0rabdioph	$⊢ (3 \in ℕ_{0} \land (a \in (ℤ^{(1 \dots 3)}) ⟼ a (3)) \in mzPoly ((1 \dots 3))) \to \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (3) = 0\} \in Dioph (3)$
344	55 70 343	mp2an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (3) = 0\} \in Dioph (3)$
345		eq0rabdioph	$⊢ (3 \in ℕ_{0} \land (a \in (ℤ^{(1 \dots 3)}) ⟼ a (2)) \in mzPoly ((1 \dots 3))) \to \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (2) = 0\} \in Dioph (3)$
346	55 338 345	mp2an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (2) = 0\} \in Dioph (3)$
347		anrabdioph	$⊢ (\{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (3) = 0\} \in Dioph (3) \land \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (2) = 0\} \in Dioph (3)) \to \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (3) = 0 \land a (2) = 0)\} \in Dioph (3)$
348	344 346 347	mp2an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (3) = 0 \land a (2) = 0)\} \in Dioph (3)$
349		orrabdioph	$⊢ (\{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| ((a (3) \in ℕ \land \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3))))) \land a (2) \in ℕ)\} \in Dioph (3) \land \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (3) = 0 \land a (2) = 0)\} \in Dioph (3)) \to \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (((a (3) \in ℕ \land \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3))))) \land a (2) \in ℕ) \lor (a (3) = 0 \land a (2) = 0))\} \in Dioph (3)$
350	342 348 349	mp2an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (((a (3) \in ℕ \land \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3))))) \land a (2) \in ℕ) \lor (a (3) = 0 \land a (2) = 0))\} \in Dioph (3)$
351		anrabdioph	$⊢ (\{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| a (1) \in ℤ_{\geq 2}\} \in Dioph (3) \land \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (((a (3) \in ℕ \land \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3))))) \land a (2) \in ℕ) \lor (a (3) = 0 \land a (2) = 0))\} \in Dioph (3)) \to \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (1) \in ℤ_{\geq 2} \land (((a (3) \in ℕ \land \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3))))) \land a (2) \in ℕ) \lor (a (3) = 0 \land a (2) = 0)))\} \in Dioph (3)$
352	66 350 351	mp2an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (1) \in ℤ_{\geq 2} \land (((a (3) \in ℕ \land \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} \exists g \in ℕ_{0} \exists h \in ℕ_{0} (((b^{2} - ({a (1)}^{2} - 1) {a (3)}^{2} = 1 \land d^{2} - ({a (1)}^{2} - 1) c^{2} = 1 \land e \in ℤ_{\geq 2}) \land (g^{2} - (e^{2} - 1) f^{2} = 1 \land c = (h + 1) 2 {a (3)}^{2} \land d ∥ (e - a (1)))) \land ((2 a (3) ∥ (e - 1) \land d ∥ (f - a (3))) \land (2 a (3) ∥ (f - a (2)) \land a (2) \leq a (3))))) \land a (2) \in ℕ) \lor (a (3) = 0 \land a (2) = 0)))\} \in Dioph (3)$
353	54 352	eqeltri	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (1) \in ℤ_{\geq 2} \land a (3) = a (1) Y_{rm} a (2))\} \in Dioph (3)$

Metamath Proof Explorer

Theorem rmydioph

Proof