expdiophlem2

Description: Lemma for expdioph . Exponentiation on a restricted domain is Diophantine. (Contributed by Stefan O'Rear, 17-Oct-2014)

		Ref	Expression
	Assertion	expdiophlem2	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{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		3nn	$⊢ 3 \in ℕ$
3	2	jm2.27dlem3	$⊢ 3 \in (1 \dots 3)$
4		ffvelcdm	$⊢ (a : (1 \dots 3) ⟶ ℕ_{0} \land 3 \in (1 \dots 3)) \to a (3) \in ℕ_{0}$
5	1 3 4	sylancl	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to a (3) \in ℕ_{0}$
6		expdiophlem1	$⊢ a (3) \in ℕ_{0} \to (((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{a (2)}) \leftrightarrow \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} (a (2) + 1)) \land ((b \in ℤ_{\geq 2} \land c = b Y_{rm} a (2)) \land ((b \in ℤ_{\geq 2} \land d = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (d - (b - a (1)) c - a (3))))))))$
7	5 6	syl	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to (((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{a (2)}) \leftrightarrow \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} (a (2) + 1)) \land ((b \in ℤ_{\geq 2} \land c = b Y_{rm} a (2)) \land ((b \in ℤ_{\geq 2} \land d = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (d - (b - a (1)) c - a (3))))))))$
8	7	rabbiia	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{a (2)})\} = \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} (a (2) + 1)) \land ((b \in ℤ_{\geq 2} \land c = b Y_{rm} a (2)) \land ((b \in ℤ_{\geq 2} \land d = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (d - (b - a (1)) c - a (3)))))))\}$
9		3nn0	$⊢ 3 \in ℕ_{0}$
10		fvex	$⊢ e (5) \in V$
11		fvex	$⊢ e (6) \in V$
12		eqeq1	$⊢ c = e (5) \to (c = b Y_{rm} a (2) \leftrightarrow e (5) = b Y_{rm} a (2))$
13	12	anbi2d	$⊢ c = e (5) \to ((b \in ℤ_{\geq 2} \land c = b Y_{rm} a (2)) \leftrightarrow (b \in ℤ_{\geq 2} \land e (5) = b Y_{rm} a (2)))$
14	13	adantr	$⊢ (c = e (5) \land d = e (6)) \to ((b \in ℤ_{\geq 2} \land c = b Y_{rm} a (2)) \leftrightarrow (b \in ℤ_{\geq 2} \land e (5) = b Y_{rm} a (2)))$
15		eqeq1	$⊢ d = e (6) \to (d = b X_{rm} a (2) \leftrightarrow e (6) = b X_{rm} a (2))$
16	15	anbi2d	$⊢ d = e (6) \to ((b \in ℤ_{\geq 2} \land d = b X_{rm} a (2)) \leftrightarrow (b \in ℤ_{\geq 2} \land e (6) = b X_{rm} a (2)))$
17	16	adantl	$⊢ (c = e (5) \land d = e (6)) \to ((b \in ℤ_{\geq 2} \land d = b X_{rm} a (2)) \leftrightarrow (b \in ℤ_{\geq 2} \land e (6) = b X_{rm} a (2)))$
18		simpr	$⊢ (c = e (5) \land d = e (6)) \to d = e (6)$
19		oveq2	$⊢ c = e (5) \to (b - a (1)) c = (b - a (1)) e (5)$
20	19	adantr	$⊢ (c = e (5) \land d = e (6)) \to (b - a (1)) c = (b - a (1)) e (5)$
21	18 20	oveq12d	$⊢ (c = e (5) \land d = e (6)) \to d - (b - a (1)) c = e (6) - (b - a (1)) e (5)$
22	21	oveq1d	$⊢ (c = e (5) \land d = e (6)) \to d - (b - a (1)) c - a (3) = e (6) - (b - a (1)) e (5) - a (3)$
23	22	breq2d	$⊢ (c = e (5) \land d = e (6)) \to ((2 b a (1) - {a (1)}^{2} - 1) ∥ (d - (b - a (1)) c - a (3)) \leftrightarrow (2 b a (1) - {a (1)}^{2} - 1) ∥ (e (6) - (b - a (1)) e (5) - a (3)))$
24	23	anbi2d	$⊢ (c = e (5) \land d = e (6)) \to ((a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (d - (b - a (1)) c - a (3))) \leftrightarrow (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (e (6) - (b - a (1)) e (5) - a (3))))$
25	17 24	anbi12d	$⊢ (c = e (5) \land d = e (6)) \to (((b \in ℤ_{\geq 2} \land d = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (d - (b - a (1)) c - a (3)))) \leftrightarrow ((b \in ℤ_{\geq 2} \land e (6) = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (e (6) - (b - a (1)) e (5) - a (3)))))$
26	14 25	anbi12d	$⊢ (c = e (5) \land d = e (6)) \to (((b \in ℤ_{\geq 2} \land c = b Y_{rm} a (2)) \land ((b \in ℤ_{\geq 2} \land d = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (d - (b - a (1)) c - a (3))))) \leftrightarrow ((b \in ℤ_{\geq 2} \land e (5) = b Y_{rm} a (2)) \land ((b \in ℤ_{\geq 2} \land e (6) = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (e (6) - (b - a (1)) e (5) - a (3))))))$
27	26	anbi2d	$⊢ (c = e (5) \land d = e (6)) \to (((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} (a (2) + 1)) \land ((b \in ℤ_{\geq 2} \land c = b Y_{rm} a (2)) \land ((b \in ℤ_{\geq 2} \land d = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (d - (b - a (1)) c - a (3)))))) \leftrightarrow ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} (a (2) + 1)) \land ((b \in ℤ_{\geq 2} \land e (5) = b Y_{rm} a (2)) \land ((b \in ℤ_{\geq 2} \land e (6) = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (e (6) - (b - a (1)) e (5) - a (3)))))))$
28	27	anbi2d	$⊢ (c = e (5) \land d = e (6)) \to (((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} (a (2) + 1)) \land ((b \in ℤ_{\geq 2} \land c = b Y_{rm} a (2)) \land ((b \in ℤ_{\geq 2} \land d = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (d - (b - a (1)) c - a (3))))))) \leftrightarrow ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} (a (2) + 1)) \land ((b \in ℤ_{\geq 2} \land e (5) = b Y_{rm} a (2)) \land ((b \in ℤ_{\geq 2} \land e (6) = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (e (6) - (b - a (1)) e (5) - a (3))))))))$
29	10 11 28	sbc2ie	$⊢ \underset{˙}{[} e (5) / c \underset{˙}{]} \underset{˙}{[} e (6) / d \underset{˙}{]} ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} (a (2) + 1)) \land ((b \in ℤ_{\geq 2} \land c = b Y_{rm} a (2)) \land ((b \in ℤ_{\geq 2} \land d = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (d - (b - a (1)) c - a (3))))))) \leftrightarrow ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} (a (2) + 1)) \land ((b \in ℤ_{\geq 2} \land e (5) = b Y_{rm} a (2)) \land ((b \in ℤ_{\geq 2} \land e (6) = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (e (6) - (b - a (1)) e (5) - a (3)))))))$
30	29	sbcbii	$⊢ \underset{˙}{[} e (4) / b \underset{˙}{]} \underset{˙}{[} e (5) / c \underset{˙}{]} \underset{˙}{[} e (6) / d \underset{˙}{]} ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} (a (2) + 1)) \land ((b \in ℤ_{\geq 2} \land c = b Y_{rm} a (2)) \land ((b \in ℤ_{\geq 2} \land d = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (d - (b - a (1)) c - a (3))))))) \leftrightarrow \underset{˙}{[} e (4) / b \underset{˙}{]} ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} (a (2) + 1)) \land ((b \in ℤ_{\geq 2} \land e (5) = b Y_{rm} a (2)) \land ((b \in ℤ_{\geq 2} \land e (6) = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (e (6) - (b - a (1)) e (5) - a (3)))))))$
31	30	sbcbii	$⊢ \underset{˙}{[} ({e ↾}_{(1 \dots 3)}) / a \underset{˙}{]} \underset{˙}{[} e (4) / b \underset{˙}{]} \underset{˙}{[} e (5) / c \underset{˙}{]} \underset{˙}{[} e (6) / d \underset{˙}{]} ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} (a (2) + 1)) \land ((b \in ℤ_{\geq 2} \land c = b Y_{rm} a (2)) \land ((b \in ℤ_{\geq 2} \land d = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (d - (b - a (1)) c - a (3))))))) \leftrightarrow \underset{˙}{[} ({e ↾}_{(1 \dots 3)}) / a \underset{˙}{]} \underset{˙}{[} e (4) / b \underset{˙}{]} ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} (a (2) + 1)) \land ((b \in ℤ_{\geq 2} \land e (5) = b Y_{rm} a (2)) \land ((b \in ℤ_{\geq 2} \land e (6) = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (e (6) - (b - a (1)) e (5) - a (3)))))))$
32		vex	$⊢ e \in V$
33	32	resex	$⊢ {e ↾}_{(1 \dots 3)} \in V$
34		fvex	$⊢ e (4) \in V$
35		df-2	$⊢ 2 = 1 + 1$
36		df-3	$⊢ 3 = 2 + 1$
37		ssid	$⊢ (1 \dots 3) \subseteq (1 \dots 3)$
38	36 37	jm2.27dlem5	$⊢ (1 \dots 2) \subseteq (1 \dots 3)$
39	35 38	jm2.27dlem5	$⊢ (1 \dots 1) \subseteq (1 \dots 3)$
40		1nn	$⊢ 1 \in ℕ$
41	40	jm2.27dlem3	$⊢ 1 \in (1 \dots 1)$
42	39 41	sselii	$⊢ 1 \in (1 \dots 3)$
43	42	jm2.27dlem1	$⊢ a = {e ↾}_{(1 \dots 3)} \to a (1) = e (1)$
44	43	eleq1d	$⊢ a = {e ↾}_{(1 \dots 3)} \to (a (1) \in ℤ_{\geq 2} \leftrightarrow e (1) \in ℤ_{\geq 2})$
45		2nn	$⊢ 2 \in ℕ$
46	45	jm2.27dlem3	$⊢ 2 \in (1 \dots 2)$
47	46 36 45	jm2.27dlem2	$⊢ 2 \in (1 \dots 3)$
48	47	jm2.27dlem1	$⊢ a = {e ↾}_{(1 \dots 3)} \to a (2) = e (2)$
49	48	eleq1d	$⊢ a = {e ↾}_{(1 \dots 3)} \to (a (2) \in ℕ \leftrightarrow e (2) \in ℕ)$
50	44 49	anbi12d	$⊢ a = {e ↾}_{(1 \dots 3)} \to ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \leftrightarrow (e (1) \in ℤ_{\geq 2} \land e (2) \in ℕ))$
51	50	adantr	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \leftrightarrow (e (1) \in ℤ_{\geq 2} \land e (2) \in ℕ))$
52	44	adantr	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to (a (1) \in ℤ_{\geq 2} \leftrightarrow e (1) \in ℤ_{\geq 2})$
53		id	$⊢ b = e (4) \to b = e (4)$
54	48	oveq1d	$⊢ a = {e ↾}_{(1 \dots 3)} \to a (2) + 1 = e (2) + 1$
55	43 54	oveq12d	$⊢ a = {e ↾}_{(1 \dots 3)} \to a (1) Y_{rm} (a (2) + 1) = e (1) Y_{rm} (e (2) + 1)$
56	53 55	eqeqan12rd	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to (b = a (1) Y_{rm} (a (2) + 1) \leftrightarrow e (4) = e (1) Y_{rm} (e (2) + 1))$
57	52 56	anbi12d	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} (a (2) + 1)) \leftrightarrow (e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} (e (2) + 1)))$
58		eleq1	$⊢ b = e (4) \to (b \in ℤ_{\geq 2} \leftrightarrow e (4) \in ℤ_{\geq 2})$
59	58	adantl	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to (b \in ℤ_{\geq 2} \leftrightarrow e (4) \in ℤ_{\geq 2})$
60	53 48	oveqan12rd	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to b Y_{rm} a (2) = e (4) Y_{rm} e (2)$
61	60	eqeq2d	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to (e (5) = b Y_{rm} a (2) \leftrightarrow e (5) = e (4) Y_{rm} e (2))$
62	59 61	anbi12d	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to ((b \in ℤ_{\geq 2} \land e (5) = b Y_{rm} a (2)) \leftrightarrow (e (4) \in ℤ_{\geq 2} \land e (5) = e (4) Y_{rm} e (2)))$
63	53 48	oveqan12rd	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to b X_{rm} a (2) = e (4) X_{rm} e (2)$
64	63	eqeq2d	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to (e (6) = b X_{rm} a (2) \leftrightarrow e (6) = e (4) X_{rm} e (2))$
65	59 64	anbi12d	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to ((b \in ℤ_{\geq 2} \land e (6) = b X_{rm} a (2)) \leftrightarrow (e (4) \in ℤ_{\geq 2} \land e (6) = e (4) X_{rm} e (2)))$
66	3	jm2.27dlem1	$⊢ a = {e ↾}_{(1 \dots 3)} \to a (3) = e (3)$
67	66	adantr	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to a (3) = e (3)$
68		oveq2	$⊢ b = e (4) \to 2 b = 2 e (4)$
69	68 43	oveqan12rd	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to 2 b a (1) = 2 e (4) e (1)$
70	43	oveq1d	$⊢ a = {e ↾}_{(1 \dots 3)} \to {a (1)}^{2} = {e (1)}^{2}$
71	70	adantr	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to {a (1)}^{2} = {e (1)}^{2}$
72	69 71	oveq12d	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to 2 b a (1) - {a (1)}^{2} = 2 e (4) e (1) - {e (1)}^{2}$
73	72	oveq1d	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to 2 b a (1) - {a (1)}^{2} - 1 = 2 e (4) e (1) - {e (1)}^{2} - 1$
74	67 73	breq12d	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \leftrightarrow e (3) < 2 e (4) e (1) - {e (1)}^{2} - 1)$
75		simpr	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to b = e (4)$
76	43	adantr	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to a (1) = e (1)$
77	75 76	oveq12d	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to b - a (1) = e (4) - e (1)$
78	77	oveq1d	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to (b - a (1)) e (5) = (e (4) - e (1)) e (5)$
79	78	oveq2d	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to e (6) - (b - a (1)) e (5) = e (6) - (e (4) - e (1)) e (5)$
80	79 67	oveq12d	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to e (6) - (b - a (1)) e (5) - a (3) = e (6) - (e (4) - e (1)) e (5) - e (3)$
81	73 80	breq12d	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to ((2 b a (1) - {a (1)}^{2} - 1) ∥ (e (6) - (b - a (1)) e (5) - a (3)) \leftrightarrow (2 e (4) e (1) - {e (1)}^{2} - 1) ∥ (e (6) - (e (4) - e (1)) e (5) - e (3)))$
82	74 81	anbi12d	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to ((a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (e (6) - (b - a (1)) e (5) - a (3))) \leftrightarrow (e (3) < 2 e (4) e (1) - {e (1)}^{2} - 1 \land (2 e (4) e (1) - {e (1)}^{2} - 1) ∥ (e (6) - (e (4) - e (1)) e (5) - e (3))))$
83	65 82	anbi12d	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to (((b \in ℤ_{\geq 2} \land e (6) = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (e (6) - (b - a (1)) e (5) - a (3)))) \leftrightarrow ((e (4) \in ℤ_{\geq 2} \land e (6) = e (4) X_{rm} e (2)) \land (e (3) < 2 e (4) e (1) - {e (1)}^{2} - 1 \land (2 e (4) e (1) - {e (1)}^{2} - 1) ∥ (e (6) - (e (4) - e (1)) e (5) - e (3)))))$
84	62 83	anbi12d	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to (((b \in ℤ_{\geq 2} \land e (5) = b Y_{rm} a (2)) \land ((b \in ℤ_{\geq 2} \land e (6) = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (e (6) - (b - a (1)) e (5) - a (3))))) \leftrightarrow ((e (4) \in ℤ_{\geq 2} \land e (5) = e (4) Y_{rm} e (2)) \land ((e (4) \in ℤ_{\geq 2} \land e (6) = e (4) X_{rm} e (2)) \land (e (3) < 2 e (4) e (1) - {e (1)}^{2} - 1 \land (2 e (4) e (1) - {e (1)}^{2} - 1) ∥ (e (6) - (e (4) - e (1)) e (5) - e (3))))))$
85	57 84	anbi12d	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to (((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} (a (2) + 1)) \land ((b \in ℤ_{\geq 2} \land e (5) = b Y_{rm} a (2)) \land ((b \in ℤ_{\geq 2} \land e (6) = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (e (6) - (b - a (1)) e (5) - a (3)))))) \leftrightarrow ((e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} (e (2) + 1)) \land ((e (4) \in ℤ_{\geq 2} \land e (5) = e (4) Y_{rm} e (2)) \land ((e (4) \in ℤ_{\geq 2} \land e (6) = e (4) X_{rm} e (2)) \land (e (3) < 2 e (4) e (1) - {e (1)}^{2} - 1 \land (2 e (4) e (1) - {e (1)}^{2} - 1) ∥ (e (6) - (e (4) - e (1)) e (5) - e (3)))))))$
86	51 85	anbi12d	$⊢ (a = {e ↾}_{(1 \dots 3)} \land b = e (4)) \to (((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} (a (2) + 1)) \land ((b \in ℤ_{\geq 2} \land e (5) = b Y_{rm} a (2)) \land ((b \in ℤ_{\geq 2} \land e (6) = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (e (6) - (b - a (1)) e (5) - a (3))))))) \leftrightarrow ((e (1) \in ℤ_{\geq 2} \land e (2) \in ℕ) \land ((e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} (e (2) + 1)) \land ((e (4) \in ℤ_{\geq 2} \land e (5) = e (4) Y_{rm} e (2)) \land ((e (4) \in ℤ_{\geq 2} \land e (6) = e (4) X_{rm} e (2)) \land (e (3) < 2 e (4) e (1) - {e (1)}^{2} - 1 \land (2 e (4) e (1) - {e (1)}^{2} - 1) ∥ (e (6) - (e (4) - e (1)) e (5) - e (3))))))))$
87	33 34 86	sbc2ie	$⊢ \underset{˙}{[} ({e ↾}_{(1 \dots 3)}) / a \underset{˙}{]} \underset{˙}{[} e (4) / b \underset{˙}{]} ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} (a (2) + 1)) \land ((b \in ℤ_{\geq 2} \land e (5) = b Y_{rm} a (2)) \land ((b \in ℤ_{\geq 2} \land e (6) = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (e (6) - (b - a (1)) e (5) - a (3))))))) \leftrightarrow ((e (1) \in ℤ_{\geq 2} \land e (2) \in ℕ) \land ((e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} (e (2) + 1)) \land ((e (4) \in ℤ_{\geq 2} \land e (5) = e (4) Y_{rm} e (2)) \land ((e (4) \in ℤ_{\geq 2} \land e (6) = e (4) X_{rm} e (2)) \land (e (3) < 2 e (4) e (1) - {e (1)}^{2} - 1 \land (2 e (4) e (1) - {e (1)}^{2} - 1) ∥ (e (6) - (e (4) - e (1)) e (5) - e (3)))))))$
88	31 87	bitri	$⊢ \underset{˙}{[} ({e ↾}_{(1 \dots 3)}) / a \underset{˙}{]} \underset{˙}{[} e (4) / b \underset{˙}{]} \underset{˙}{[} e (5) / c \underset{˙}{]} \underset{˙}{[} e (6) / d \underset{˙}{]} ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} (a (2) + 1)) \land ((b \in ℤ_{\geq 2} \land c = b Y_{rm} a (2)) \land ((b \in ℤ_{\geq 2} \land d = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (d - (b - a (1)) c - a (3))))))) \leftrightarrow ((e (1) \in ℤ_{\geq 2} \land e (2) \in ℕ) \land ((e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} (e (2) + 1)) \land ((e (4) \in ℤ_{\geq 2} \land e (5) = e (4) Y_{rm} e (2)) \land ((e (4) \in ℤ_{\geq 2} \land e (6) = e (4) X_{rm} e (2)) \land (e (3) < 2 e (4) e (1) - {e (1)}^{2} - 1 \land (2 e (4) e (1) - {e (1)}^{2} - 1) ∥ (e (6) - (e (4) - e (1)) e (5) - e (3)))))))$
89	88	rabbii	$⊢ \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| \underset{˙}{[} ({e ↾}_{(1 \dots 3)}) / a \underset{˙}{]} \underset{˙}{[} e (4) / b \underset{˙}{]} \underset{˙}{[} e (5) / c \underset{˙}{]} \underset{˙}{[} e (6) / d \underset{˙}{]} ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} (a (2) + 1)) \land ((b \in ℤ_{\geq 2} \land c = b Y_{rm} a (2)) \land ((b \in ℤ_{\geq 2} \land d = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (d - (b - a (1)) c - a (3)))))))\} = \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| ((e (1) \in ℤ_{\geq 2} \land e (2) \in ℕ) \land ((e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} (e (2) + 1)) \land ((e (4) \in ℤ_{\geq 2} \land e (5) = e (4) Y_{rm} e (2)) \land ((e (4) \in ℤ_{\geq 2} \land e (6) = e (4) X_{rm} e (2)) \land (e (3) < 2 e (4) e (1) - {e (1)}^{2} - 1 \land (2 e (4) e (1) - {e (1)}^{2} - 1) ∥ (e (6) - (e (4) - e (1)) e (5) - e (3)))))))\}$
90		6nn0	$⊢ 6 \in ℕ_{0}$
91		2z	$⊢ 2 \in ℤ$
92		ovex	$⊢ (1 \dots 6) \in V$
93		df-4	$⊢ 4 = 3 + 1$
94		df-5	$⊢ 5 = 4 + 1$
95		df-6	$⊢ 6 = 5 + 1$
96		ssid	$⊢ (1 \dots 6) \subseteq (1 \dots 6)$
97	95 96	jm2.27dlem5	$⊢ (1 \dots 5) \subseteq (1 \dots 6)$
98	94 97	jm2.27dlem5	$⊢ (1 \dots 4) \subseteq (1 \dots 6)$
99	93 98	jm2.27dlem5	$⊢ (1 \dots 3) \subseteq (1 \dots 6)$
100	36 99	jm2.27dlem5	$⊢ (1 \dots 2) \subseteq (1 \dots 6)$
101	35 100	jm2.27dlem5	$⊢ (1 \dots 1) \subseteq (1 \dots 6)$
102	101 41	sselii	$⊢ 1 \in (1 \dots 6)$
103		mzpproj	$⊢ ((1 \dots 6) \in V \land 1 \in (1 \dots 6)) \to (e \in (ℤ^{(1 \dots 6)}) ⟼ e (1)) \in mzPoly ((1 \dots 6))$
104	92 102 103	mp2an	$⊢ (e \in (ℤ^{(1 \dots 6)}) ⟼ e (1)) \in mzPoly ((1 \dots 6))$
105		eluzrabdioph	$⊢ (6 \in ℕ_{0} \land 2 \in ℤ \land (e \in (ℤ^{(1 \dots 6)}) ⟼ e (1)) \in mzPoly ((1 \dots 6))) \to \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| e (1) \in ℤ_{\geq 2}\} \in Dioph (6)$
106	90 91 104 105	mp3an	$⊢ \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| e (1) \in ℤ_{\geq 2}\} \in Dioph (6)$
107	100 46	sselii	$⊢ 2 \in (1 \dots 6)$
108		mzpproj	$⊢ ((1 \dots 6) \in V \land 2 \in (1 \dots 6)) \to (e \in (ℤ^{(1 \dots 6)}) ⟼ e (2)) \in mzPoly ((1 \dots 6))$
109	92 107 108	mp2an	$⊢ (e \in (ℤ^{(1 \dots 6)}) ⟼ e (2)) \in mzPoly ((1 \dots 6))$
110		elnnrabdioph	$⊢ (6 \in ℕ_{0} \land (e \in (ℤ^{(1 \dots 6)}) ⟼ e (2)) \in mzPoly ((1 \dots 6))) \to \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| e (2) \in ℕ\} \in Dioph (6)$
111	90 109 110	mp2an	$⊢ \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| e (2) \in ℕ\} \in Dioph (6)$
112		anrabdioph	$⊢ (\{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| e (1) \in ℤ_{\geq 2}\} \in Dioph (6) \land \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| e (2) \in ℕ\} \in Dioph (6)) \to \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| (e (1) \in ℤ_{\geq 2} \land e (2) \in ℕ)\} \in Dioph (6)$
113	106 111 112	mp2an	$⊢ \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| (e (1) \in ℤ_{\geq 2} \land e (2) \in ℕ)\} \in Dioph (6)$
114		elmapi	$⊢ e \in ({ℕ_{0}}^{(1 \dots 6)}) \to e : (1 \dots 6) ⟶ ℕ_{0}$
115		ffvelcdm	$⊢ (e : (1 \dots 6) ⟶ ℕ_{0} \land 2 \in (1 \dots 6)) \to e (2) \in ℕ_{0}$
116	114 107 115	sylancl	$⊢ e \in ({ℕ_{0}}^{(1 \dots 6)}) \to e (2) \in ℕ_{0}$
117		peano2nn0	$⊢ e (2) \in ℕ_{0} \to e (2) + 1 \in ℕ_{0}$
118		oveq2	$⊢ b = e (2) + 1 \to e (1) Y_{rm} b = e (1) Y_{rm} (e (2) + 1)$
119	118	eqeq2d	$⊢ b = e (2) + 1 \to (e (4) = e (1) Y_{rm} b \leftrightarrow e (4) = e (1) Y_{rm} (e (2) + 1))$
120	119	anbi2d	$⊢ b = e (2) + 1 \to ((e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} b) \leftrightarrow (e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} (e (2) + 1)))$
121	120	ceqsrexv	$⊢ e (2) + 1 \in ℕ_{0} \to (\exists b \in ℕ_{0} (b = e (2) + 1 \land (e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} b)) \leftrightarrow (e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} (e (2) + 1)))$
122	116 117 121	3syl	$⊢ e \in ({ℕ_{0}}^{(1 \dots 6)}) \to (\exists b \in ℕ_{0} (b = e (2) + 1 \land (e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} b)) \leftrightarrow (e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} (e (2) + 1)))$
123	122	bicomd	$⊢ e \in ({ℕ_{0}}^{(1 \dots 6)}) \to ((e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} (e (2) + 1)) \leftrightarrow \exists b \in ℕ_{0} (b = e (2) + 1 \land (e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} b)))$
124	123	rabbiia	$⊢ \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| (e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} (e (2) + 1))\} = \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| \exists b \in ℕ_{0} (b = e (2) + 1 \land (e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} b))\}$
125		vex	$⊢ a \in V$
126	125	resex	$⊢ {a ↾}_{(1 \dots 6)} \in V$
127		fvex	$⊢ a (7) \in V$
128		id	$⊢ b = a (7) \to b = a (7)$
129	107	jm2.27dlem1	$⊢ e = {a ↾}_{(1 \dots 6)} \to e (2) = a (2)$
130	129	oveq1d	$⊢ e = {a ↾}_{(1 \dots 6)} \to e (2) + 1 = a (2) + 1$
131	128 130	eqeqan12rd	$⊢ (e = {a ↾}_{(1 \dots 6)} \land b = a (7)) \to (b = e (2) + 1 \leftrightarrow a (7) = a (2) + 1)$
132	102	jm2.27dlem1	$⊢ e = {a ↾}_{(1 \dots 6)} \to e (1) = a (1)$
133	132	adantr	$⊢ (e = {a ↾}_{(1 \dots 6)} \land b = a (7)) \to e (1) = a (1)$
134	133	eleq1d	$⊢ (e = {a ↾}_{(1 \dots 6)} \land b = a (7)) \to (e (1) \in ℤ_{\geq 2} \leftrightarrow a (1) \in ℤ_{\geq 2})$
135		4nn	$⊢ 4 \in ℕ$
136	135	jm2.27dlem3	$⊢ 4 \in (1 \dots 4)$
137	98 136	sselii	$⊢ 4 \in (1 \dots 6)$
138	137	jm2.27dlem1	$⊢ e = {a ↾}_{(1 \dots 6)} \to e (4) = a (4)$
139	138	adantr	$⊢ (e = {a ↾}_{(1 \dots 6)} \land b = a (7)) \to e (4) = a (4)$
140	132 128	oveqan12d	$⊢ (e = {a ↾}_{(1 \dots 6)} \land b = a (7)) \to e (1) Y_{rm} b = a (1) Y_{rm} a (7)$
141	139 140	eqeq12d	$⊢ (e = {a ↾}_{(1 \dots 6)} \land b = a (7)) \to (e (4) = e (1) Y_{rm} b \leftrightarrow a (4) = a (1) Y_{rm} a (7))$
142	134 141	anbi12d	$⊢ (e = {a ↾}_{(1 \dots 6)} \land b = a (7)) \to ((e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} b) \leftrightarrow (a (1) \in ℤ_{\geq 2} \land a (4) = a (1) Y_{rm} a (7)))$
143	131 142	anbi12d	$⊢ (e = {a ↾}_{(1 \dots 6)} \land b = a (7)) \to ((b = e (2) + 1 \land (e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} b)) \leftrightarrow (a (7) = a (2) + 1 \land (a (1) \in ℤ_{\geq 2} \land a (4) = a (1) Y_{rm} a (7))))$
144	126 127 143	sbc2ie	$⊢ \underset{˙}{[} ({a ↾}_{(1 \dots 6)}) / e \underset{˙}{]} \underset{˙}{[} a (7) / b \underset{˙}{]} (b = e (2) + 1 \land (e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} b)) \leftrightarrow (a (7) = a (2) + 1 \land (a (1) \in ℤ_{\geq 2} \land a (4) = a (1) Y_{rm} a (7)))$
145	144	rabbii	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 7)}) \| \underset{˙}{[} ({a ↾}_{(1 \dots 6)}) / e \underset{˙}{]} \underset{˙}{[} a (7) / b \underset{˙}{]} (b = e (2) + 1 \land (e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} b))\} = \{a \in ({ℕ_{0}}^{(1 \dots 7)}) \| (a (7) = a (2) + 1 \land (a (1) \in ℤ_{\geq 2} \land a (4) = a (1) Y_{rm} a (7)))\}$
146		7nn0	$⊢ 7 \in ℕ_{0}$
147		ovex	$⊢ (1 \dots 7) \in V$
148		7nn	$⊢ 7 \in ℕ$
149	148	jm2.27dlem3	$⊢ 7 \in (1 \dots 7)$
150		mzpproj	$⊢ ((1 \dots 7) \in V \land 7 \in (1 \dots 7)) \to (a \in (ℤ^{(1 \dots 7)}) ⟼ a (7)) \in mzPoly ((1 \dots 7))$
151	147 149 150	mp2an	$⊢ (a \in (ℤ^{(1 \dots 7)}) ⟼ a (7)) \in mzPoly ((1 \dots 7))$
152		df-7	$⊢ 7 = 6 + 1$
153		6nn	$⊢ 6 \in ℕ$
154	107 152 153	jm2.27dlem2	$⊢ 2 \in (1 \dots 7)$
155		mzpproj	$⊢ ((1 \dots 7) \in V \land 2 \in (1 \dots 7)) \to (a \in (ℤ^{(1 \dots 7)}) ⟼ a (2)) \in mzPoly ((1 \dots 7))$
156	147 154 155	mp2an	$⊢ (a \in (ℤ^{(1 \dots 7)}) ⟼ a (2)) \in mzPoly ((1 \dots 7))$
157		1z	$⊢ 1 \in ℤ$
158		mzpconstmpt	$⊢ ((1 \dots 7) \in V \land 1 \in ℤ) \to (a \in (ℤ^{(1 \dots 7)}) ⟼ 1) \in mzPoly ((1 \dots 7))$
159	147 157 158	mp2an	$⊢ (a \in (ℤ^{(1 \dots 7)}) ⟼ 1) \in mzPoly ((1 \dots 7))$
160		mzpaddmpt	$⊢ ((a \in (ℤ^{(1 \dots 7)}) ⟼ a (2)) \in mzPoly ((1 \dots 7)) \land (a \in (ℤ^{(1 \dots 7)}) ⟼ 1) \in mzPoly ((1 \dots 7))) \to (a \in (ℤ^{(1 \dots 7)}) ⟼ a (2) + 1) \in mzPoly ((1 \dots 7))$
161	156 159 160	mp2an	$⊢ (a \in (ℤ^{(1 \dots 7)}) ⟼ a (2) + 1) \in mzPoly ((1 \dots 7))$
162		eqrabdioph	$⊢ (7 \in ℕ_{0} \land (a \in (ℤ^{(1 \dots 7)}) ⟼ a (7)) \in mzPoly ((1 \dots 7)) \land (a \in (ℤ^{(1 \dots 7)}) ⟼ a (2) + 1) \in mzPoly ((1 \dots 7))) \to \{a \in ({ℕ_{0}}^{(1 \dots 7)}) \| a (7) = a (2) + 1\} \in Dioph (7)$
163	146 151 161 162	mp3an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 7)}) \| a (7) = a (2) + 1\} \in Dioph (7)$
164		rmydioph	$⊢ \{b \in ({ℕ_{0}}^{(1 \dots 3)}) \| (b (1) \in ℤ_{\geq 2} \land b (3) = b (1) Y_{rm} b (2))\} \in Dioph (3)$
165		simp1	$⊢ (b (1) = a (1) \land b (2) = a (7) \land b (3) = a (4)) \to b (1) = a (1)$
166	165	eleq1d	$⊢ (b (1) = a (1) \land b (2) = a (7) \land b (3) = a (4)) \to (b (1) \in ℤ_{\geq 2} \leftrightarrow a (1) \in ℤ_{\geq 2})$
167		simp3	$⊢ (b (1) = a (1) \land b (2) = a (7) \land b (3) = a (4)) \to b (3) = a (4)$
168		simp2	$⊢ (b (1) = a (1) \land b (2) = a (7) \land b (3) = a (4)) \to b (2) = a (7)$
169	165 168	oveq12d	$⊢ (b (1) = a (1) \land b (2) = a (7) \land b (3) = a (4)) \to b (1) Y_{rm} b (2) = a (1) Y_{rm} a (7)$
170	167 169	eqeq12d	$⊢ (b (1) = a (1) \land b (2) = a (7) \land b (3) = a (4)) \to (b (3) = b (1) Y_{rm} b (2) \leftrightarrow a (4) = a (1) Y_{rm} a (7))$
171	166 170	anbi12d	$⊢ (b (1) = a (1) \land b (2) = a (7) \land b (3) = a (4)) \to ((b (1) \in ℤ_{\geq 2} \land b (3) = b (1) Y_{rm} b (2)) \leftrightarrow (a (1) \in ℤ_{\geq 2} \land a (4) = a (1) Y_{rm} a (7)))$
172	102 152 153	jm2.27dlem2	$⊢ 1 \in (1 \dots 7)$
173	137 152 153	jm2.27dlem2	$⊢ 4 \in (1 \dots 7)$
174	171 172 149 173	rabren3dioph	$⊢ (7 \in ℕ_{0} \land \{b \in ({ℕ_{0}}^{(1 \dots 3)}) \| (b (1) \in ℤ_{\geq 2} \land b (3) = b (1) Y_{rm} b (2))\} \in Dioph (3)) \to \{a \in ({ℕ_{0}}^{(1 \dots 7)}) \| (a (1) \in ℤ_{\geq 2} \land a (4) = a (1) Y_{rm} a (7))\} \in Dioph (7)$
175	146 164 174	mp2an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 7)}) \| (a (1) \in ℤ_{\geq 2} \land a (4) = a (1) Y_{rm} a (7))\} \in Dioph (7)$
176		anrabdioph	$⊢ (\{a \in ({ℕ_{0}}^{(1 \dots 7)}) \| a (7) = a (2) + 1\} \in Dioph (7) \land \{a \in ({ℕ_{0}}^{(1 \dots 7)}) \| (a (1) \in ℤ_{\geq 2} \land a (4) = a (1) Y_{rm} a (7))\} \in Dioph (7)) \to \{a \in ({ℕ_{0}}^{(1 \dots 7)}) \| (a (7) = a (2) + 1 \land (a (1) \in ℤ_{\geq 2} \land a (4) = a (1) Y_{rm} a (7)))\} \in Dioph (7)$
177	163 175 176	mp2an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 7)}) \| (a (7) = a (2) + 1 \land (a (1) \in ℤ_{\geq 2} \land a (4) = a (1) Y_{rm} a (7)))\} \in Dioph (7)$
178	145 177	eqeltri	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 7)}) \| \underset{˙}{[} ({a ↾}_{(1 \dots 6)}) / e \underset{˙}{]} \underset{˙}{[} a (7) / b \underset{˙}{]} (b = e (2) + 1 \land (e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} b))\} \in Dioph (7)$
179	152	rexfrabdioph	$⊢ (6 \in ℕ_{0} \land \{a \in ({ℕ_{0}}^{(1 \dots 7)}) \| \underset{˙}{[} ({a ↾}_{(1 \dots 6)}) / e \underset{˙}{]} \underset{˙}{[} a (7) / b \underset{˙}{]} (b = e (2) + 1 \land (e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} b))\} \in Dioph (7)) \to \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| \exists b \in ℕ_{0} (b = e (2) + 1 \land (e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} b))\} \in Dioph (6)$
180	90 178 179	mp2an	$⊢ \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| \exists b \in ℕ_{0} (b = e (2) + 1 \land (e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} b))\} \in Dioph (6)$
181	124 180	eqeltri	$⊢ \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| (e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} (e (2) + 1))\} \in Dioph (6)$
182		rmydioph	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (1) \in ℤ_{\geq 2} \land a (3) = a (1) Y_{rm} a (2))\} \in Dioph (3)$
183		simp1	$⊢ (a (1) = e (4) \land a (2) = e (2) \land a (3) = e (5)) \to a (1) = e (4)$
184	183	eleq1d	$⊢ (a (1) = e (4) \land a (2) = e (2) \land a (3) = e (5)) \to (a (1) \in ℤ_{\geq 2} \leftrightarrow e (4) \in ℤ_{\geq 2})$
185		simp3	$⊢ (a (1) = e (4) \land a (2) = e (2) \land a (3) = e (5)) \to a (3) = e (5)$
186		simp2	$⊢ (a (1) = e (4) \land a (2) = e (2) \land a (3) = e (5)) \to a (2) = e (2)$
187	183 186	oveq12d	$⊢ (a (1) = e (4) \land a (2) = e (2) \land a (3) = e (5)) \to a (1) Y_{rm} a (2) = e (4) Y_{rm} e (2)$
188	185 187	eqeq12d	$⊢ (a (1) = e (4) \land a (2) = e (2) \land a (3) = e (5)) \to (a (3) = a (1) Y_{rm} a (2) \leftrightarrow e (5) = e (4) Y_{rm} e (2))$
189	184 188	anbi12d	$⊢ (a (1) = e (4) \land a (2) = e (2) \land a (3) = e (5)) \to ((a (1) \in ℤ_{\geq 2} \land a (3) = a (1) Y_{rm} a (2)) \leftrightarrow (e (4) \in ℤ_{\geq 2} \land e (5) = e (4) Y_{rm} e (2)))$
190		5nn	$⊢ 5 \in ℕ$
191	190	jm2.27dlem3	$⊢ 5 \in (1 \dots 5)$
192	191 95 190	jm2.27dlem2	$⊢ 5 \in (1 \dots 6)$
193	189 137 107 192	rabren3dioph	$⊢ (6 \in ℕ_{0} \land \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (1) \in ℤ_{\geq 2} \land a (3) = a (1) Y_{rm} a (2))\} \in Dioph (3)) \to \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| (e (4) \in ℤ_{\geq 2} \land e (5) = e (4) Y_{rm} e (2))\} \in Dioph (6)$
194	90 182 193	mp2an	$⊢ \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| (e (4) \in ℤ_{\geq 2} \land e (5) = e (4) Y_{rm} e (2))\} \in Dioph (6)$
195		rmxdioph	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (1) \in ℤ_{\geq 2} \land a (3) = a (1) X_{rm} a (2))\} \in Dioph (3)$
196		simp1	$⊢ (a (1) = e (4) \land a (2) = e (2) \land a (3) = e (6)) \to a (1) = e (4)$
197	196	eleq1d	$⊢ (a (1) = e (4) \land a (2) = e (2) \land a (3) = e (6)) \to (a (1) \in ℤ_{\geq 2} \leftrightarrow e (4) \in ℤ_{\geq 2})$
198		simp3	$⊢ (a (1) = e (4) \land a (2) = e (2) \land a (3) = e (6)) \to a (3) = e (6)$
199		simp2	$⊢ (a (1) = e (4) \land a (2) = e (2) \land a (3) = e (6)) \to a (2) = e (2)$
200	196 199	oveq12d	$⊢ (a (1) = e (4) \land a (2) = e (2) \land a (3) = e (6)) \to a (1) X_{rm} a (2) = e (4) X_{rm} e (2)$
201	198 200	eqeq12d	$⊢ (a (1) = e (4) \land a (2) = e (2) \land a (3) = e (6)) \to (a (3) = a (1) X_{rm} a (2) \leftrightarrow e (6) = e (4) X_{rm} e (2))$
202	197 201	anbi12d	$⊢ (a (1) = e (4) \land a (2) = e (2) \land a (3) = e (6)) \to ((a (1) \in ℤ_{\geq 2} \land a (3) = a (1) X_{rm} a (2)) \leftrightarrow (e (4) \in ℤ_{\geq 2} \land e (6) = e (4) X_{rm} e (2)))$
203	153	jm2.27dlem3	$⊢ 6 \in (1 \dots 6)$
204	202 137 107 203	rabren3dioph	$⊢ (6 \in ℕ_{0} \land \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (1) \in ℤ_{\geq 2} \land a (3) = a (1) X_{rm} a (2))\} \in Dioph (3)) \to \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| (e (4) \in ℤ_{\geq 2} \land e (6) = e (4) X_{rm} e (2))\} \in Dioph (6)$
205	90 195 204	mp2an	$⊢ \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| (e (4) \in ℤ_{\geq 2} \land e (6) = e (4) X_{rm} e (2))\} \in Dioph (6)$
206	99 3	sselii	$⊢ 3 \in (1 \dots 6)$
207		mzpproj	$⊢ ((1 \dots 6) \in V \land 3 \in (1 \dots 6)) \to (e \in (ℤ^{(1 \dots 6)}) ⟼ e (3)) \in mzPoly ((1 \dots 6))$
208	92 206 207	mp2an	$⊢ (e \in (ℤ^{(1 \dots 6)}) ⟼ e (3)) \in mzPoly ((1 \dots 6))$
209		mzpconstmpt	$⊢ ((1 \dots 6) \in V \land 2 \in ℤ) \to (e \in (ℤ^{(1 \dots 6)}) ⟼ 2) \in mzPoly ((1 \dots 6))$
210	92 91 209	mp2an	$⊢ (e \in (ℤ^{(1 \dots 6)}) ⟼ 2) \in mzPoly ((1 \dots 6))$
211		mzpproj	$⊢ ((1 \dots 6) \in V \land 4 \in (1 \dots 6)) \to (e \in (ℤ^{(1 \dots 6)}) ⟼ e (4)) \in mzPoly ((1 \dots 6))$
212	92 137 211	mp2an	$⊢ (e \in (ℤ^{(1 \dots 6)}) ⟼ e (4)) \in mzPoly ((1 \dots 6))$
213		mzpmulmpt	$⊢ ((e \in (ℤ^{(1 \dots 6)}) ⟼ 2) \in mzPoly ((1 \dots 6)) \land (e \in (ℤ^{(1 \dots 6)}) ⟼ e (4)) \in mzPoly ((1 \dots 6))) \to (e \in (ℤ^{(1 \dots 6)}) ⟼ 2 e (4)) \in mzPoly ((1 \dots 6))$
214	210 212 213	mp2an	$⊢ (e \in (ℤ^{(1 \dots 6)}) ⟼ 2 e (4)) \in mzPoly ((1 \dots 6))$
215		mzpmulmpt	$⊢ ((e \in (ℤ^{(1 \dots 6)}) ⟼ 2 e (4)) \in mzPoly ((1 \dots 6)) \land (e \in (ℤ^{(1 \dots 6)}) ⟼ e (1)) \in mzPoly ((1 \dots 6))) \to (e \in (ℤ^{(1 \dots 6)}) ⟼ 2 e (4) e (1)) \in mzPoly ((1 \dots 6))$
216	214 104 215	mp2an	$⊢ (e \in (ℤ^{(1 \dots 6)}) ⟼ 2 e (4) e (1)) \in mzPoly ((1 \dots 6))$
217		2nn0	$⊢ 2 \in ℕ_{0}$
218		mzpexpmpt	$⊢ ((e \in (ℤ^{(1 \dots 6)}) ⟼ e (1)) \in mzPoly ((1 \dots 6)) \land 2 \in ℕ_{0}) \to (e \in (ℤ^{(1 \dots 6)}) ⟼ {e (1)}^{2}) \in mzPoly ((1 \dots 6))$
219	104 217 218	mp2an	$⊢ (e \in (ℤ^{(1 \dots 6)}) ⟼ {e (1)}^{2}) \in mzPoly ((1 \dots 6))$
220		mzpsubmpt	$⊢ ((e \in (ℤ^{(1 \dots 6)}) ⟼ 2 e (4) e (1)) \in mzPoly ((1 \dots 6)) \land (e \in (ℤ^{(1 \dots 6)}) ⟼ {e (1)}^{2}) \in mzPoly ((1 \dots 6))) \to (e \in (ℤ^{(1 \dots 6)}) ⟼ 2 e (4) e (1) - {e (1)}^{2}) \in mzPoly ((1 \dots 6))$
221	216 219 220	mp2an	$⊢ (e \in (ℤ^{(1 \dots 6)}) ⟼ 2 e (4) e (1) - {e (1)}^{2}) \in mzPoly ((1 \dots 6))$
222		mzpconstmpt	$⊢ ((1 \dots 6) \in V \land 1 \in ℤ) \to (e \in (ℤ^{(1 \dots 6)}) ⟼ 1) \in mzPoly ((1 \dots 6))$
223	92 157 222	mp2an	$⊢ (e \in (ℤ^{(1 \dots 6)}) ⟼ 1) \in mzPoly ((1 \dots 6))$
224		mzpsubmpt	$⊢ ((e \in (ℤ^{(1 \dots 6)}) ⟼ 2 e (4) e (1) - {e (1)}^{2}) \in mzPoly ((1 \dots 6)) \land (e \in (ℤ^{(1 \dots 6)}) ⟼ 1) \in mzPoly ((1 \dots 6))) \to (e \in (ℤ^{(1 \dots 6)}) ⟼ 2 e (4) e (1) - {e (1)}^{2} - 1) \in mzPoly ((1 \dots 6))$
225	221 223 224	mp2an	$⊢ (e \in (ℤ^{(1 \dots 6)}) ⟼ 2 e (4) e (1) - {e (1)}^{2} - 1) \in mzPoly ((1 \dots 6))$
226		ltrabdioph	$⊢ (6 \in ℕ_{0} \land (e \in (ℤ^{(1 \dots 6)}) ⟼ e (3)) \in mzPoly ((1 \dots 6)) \land (e \in (ℤ^{(1 \dots 6)}) ⟼ 2 e (4) e (1) - {e (1)}^{2} - 1) \in mzPoly ((1 \dots 6))) \to \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| e (3) < 2 e (4) e (1) - {e (1)}^{2} - 1\} \in Dioph (6)$
227	90 208 225 226	mp3an	$⊢ \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| e (3) < 2 e (4) e (1) - {e (1)}^{2} - 1\} \in Dioph (6)$
228		mzpproj	$⊢ ((1 \dots 6) \in V \land 6 \in (1 \dots 6)) \to (e \in (ℤ^{(1 \dots 6)}) ⟼ e (6)) \in mzPoly ((1 \dots 6))$
229	92 203 228	mp2an	$⊢ (e \in (ℤ^{(1 \dots 6)}) ⟼ e (6)) \in mzPoly ((1 \dots 6))$
230		mzpsubmpt	$⊢ ((e \in (ℤ^{(1 \dots 6)}) ⟼ e (4)) \in mzPoly ((1 \dots 6)) \land (e \in (ℤ^{(1 \dots 6)}) ⟼ e (1)) \in mzPoly ((1 \dots 6))) \to (e \in (ℤ^{(1 \dots 6)}) ⟼ e (4) - e (1)) \in mzPoly ((1 \dots 6))$
231	212 104 230	mp2an	$⊢ (e \in (ℤ^{(1 \dots 6)}) ⟼ e (4) - e (1)) \in mzPoly ((1 \dots 6))$
232		mzpproj	$⊢ ((1 \dots 6) \in V \land 5 \in (1 \dots 6)) \to (e \in (ℤ^{(1 \dots 6)}) ⟼ e (5)) \in mzPoly ((1 \dots 6))$
233	92 192 232	mp2an	$⊢ (e \in (ℤ^{(1 \dots 6)}) ⟼ e (5)) \in mzPoly ((1 \dots 6))$
234		mzpmulmpt	$⊢ ((e \in (ℤ^{(1 \dots 6)}) ⟼ e (4) - e (1)) \in mzPoly ((1 \dots 6)) \land (e \in (ℤ^{(1 \dots 6)}) ⟼ e (5)) \in mzPoly ((1 \dots 6))) \to (e \in (ℤ^{(1 \dots 6)}) ⟼ (e (4) - e (1)) e (5)) \in mzPoly ((1 \dots 6))$
235	231 233 234	mp2an	$⊢ (e \in (ℤ^{(1 \dots 6)}) ⟼ (e (4) - e (1)) e (5)) \in mzPoly ((1 \dots 6))$
236		mzpsubmpt	$⊢ ((e \in (ℤ^{(1 \dots 6)}) ⟼ e (6)) \in mzPoly ((1 \dots 6)) \land (e \in (ℤ^{(1 \dots 6)}) ⟼ (e (4) - e (1)) e (5)) \in mzPoly ((1 \dots 6))) \to (e \in (ℤ^{(1 \dots 6)}) ⟼ e (6) - (e (4) - e (1)) e (5)) \in mzPoly ((1 \dots 6))$
237	229 235 236	mp2an	$⊢ (e \in (ℤ^{(1 \dots 6)}) ⟼ e (6) - (e (4) - e (1)) e (5)) \in mzPoly ((1 \dots 6))$
238		mzpsubmpt	$⊢ ((e \in (ℤ^{(1 \dots 6)}) ⟼ e (6) - (e (4) - e (1)) e (5)) \in mzPoly ((1 \dots 6)) \land (e \in (ℤ^{(1 \dots 6)}) ⟼ e (3)) \in mzPoly ((1 \dots 6))) \to (e \in (ℤ^{(1 \dots 6)}) ⟼ e (6) - (e (4) - e (1)) e (5) - e (3)) \in mzPoly ((1 \dots 6))$
239	237 208 238	mp2an	$⊢ (e \in (ℤ^{(1 \dots 6)}) ⟼ e (6) - (e (4) - e (1)) e (5) - e (3)) \in mzPoly ((1 \dots 6))$
240		dvdsrabdioph	$⊢ (6 \in ℕ_{0} \land (e \in (ℤ^{(1 \dots 6)}) ⟼ 2 e (4) e (1) - {e (1)}^{2} - 1) \in mzPoly ((1 \dots 6)) \land (e \in (ℤ^{(1 \dots 6)}) ⟼ e (6) - (e (4) - e (1)) e (5) - e (3)) \in mzPoly ((1 \dots 6))) \to \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| (2 e (4) e (1) - {e (1)}^{2} - 1) ∥ (e (6) - (e (4) - e (1)) e (5) - e (3))\} \in Dioph (6)$
241	90 225 239 240	mp3an	$⊢ \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| (2 e (4) e (1) - {e (1)}^{2} - 1) ∥ (e (6) - (e (4) - e (1)) e (5) - e (3))\} \in Dioph (6)$
242		anrabdioph	$⊢ (\{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| e (3) < 2 e (4) e (1) - {e (1)}^{2} - 1\} \in Dioph (6) \land \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| (2 e (4) e (1) - {e (1)}^{2} - 1) ∥ (e (6) - (e (4) - e (1)) e (5) - e (3))\} \in Dioph (6)) \to \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| (e (3) < 2 e (4) e (1) - {e (1)}^{2} - 1 \land (2 e (4) e (1) - {e (1)}^{2} - 1) ∥ (e (6) - (e (4) - e (1)) e (5) - e (3)))\} \in Dioph (6)$
243	227 241 242	mp2an	$⊢ \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| (e (3) < 2 e (4) e (1) - {e (1)}^{2} - 1 \land (2 e (4) e (1) - {e (1)}^{2} - 1) ∥ (e (6) - (e (4) - e (1)) e (5) - e (3)))\} \in Dioph (6)$
244		anrabdioph	$⊢ (\{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| (e (4) \in ℤ_{\geq 2} \land e (6) = e (4) X_{rm} e (2))\} \in Dioph (6) \land \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| (e (3) < 2 e (4) e (1) - {e (1)}^{2} - 1 \land (2 e (4) e (1) - {e (1)}^{2} - 1) ∥ (e (6) - (e (4) - e (1)) e (5) - e (3)))\} \in Dioph (6)) \to \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| ((e (4) \in ℤ_{\geq 2} \land e (6) = e (4) X_{rm} e (2)) \land (e (3) < 2 e (4) e (1) - {e (1)}^{2} - 1 \land (2 e (4) e (1) - {e (1)}^{2} - 1) ∥ (e (6) - (e (4) - e (1)) e (5) - e (3))))\} \in Dioph (6)$
245	205 243 244	mp2an	$⊢ \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| ((e (4) \in ℤ_{\geq 2} \land e (6) = e (4) X_{rm} e (2)) \land (e (3) < 2 e (4) e (1) - {e (1)}^{2} - 1 \land (2 e (4) e (1) - {e (1)}^{2} - 1) ∥ (e (6) - (e (4) - e (1)) e (5) - e (3))))\} \in Dioph (6)$
246		anrabdioph	$⊢ (\{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| (e (4) \in ℤ_{\geq 2} \land e (5) = e (4) Y_{rm} e (2))\} \in Dioph (6) \land \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| ((e (4) \in ℤ_{\geq 2} \land e (6) = e (4) X_{rm} e (2)) \land (e (3) < 2 e (4) e (1) - {e (1)}^{2} - 1 \land (2 e (4) e (1) - {e (1)}^{2} - 1) ∥ (e (6) - (e (4) - e (1)) e (5) - e (3))))\} \in Dioph (6)) \to \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| ((e (4) \in ℤ_{\geq 2} \land e (5) = e (4) Y_{rm} e (2)) \land ((e (4) \in ℤ_{\geq 2} \land e (6) = e (4) X_{rm} e (2)) \land (e (3) < 2 e (4) e (1) - {e (1)}^{2} - 1 \land (2 e (4) e (1) - {e (1)}^{2} - 1) ∥ (e (6) - (e (4) - e (1)) e (5) - e (3)))))\} \in Dioph (6)$
247	194 245 246	mp2an	$⊢ \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| ((e (4) \in ℤ_{\geq 2} \land e (5) = e (4) Y_{rm} e (2)) \land ((e (4) \in ℤ_{\geq 2} \land e (6) = e (4) X_{rm} e (2)) \land (e (3) < 2 e (4) e (1) - {e (1)}^{2} - 1 \land (2 e (4) e (1) - {e (1)}^{2} - 1) ∥ (e (6) - (e (4) - e (1)) e (5) - e (3)))))\} \in Dioph (6)$
248		anrabdioph	$⊢ (\{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| (e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} (e (2) + 1))\} \in Dioph (6) \land \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| ((e (4) \in ℤ_{\geq 2} \land e (5) = e (4) Y_{rm} e (2)) \land ((e (4) \in ℤ_{\geq 2} \land e (6) = e (4) X_{rm} e (2)) \land (e (3) < 2 e (4) e (1) - {e (1)}^{2} - 1 \land (2 e (4) e (1) - {e (1)}^{2} - 1) ∥ (e (6) - (e (4) - e (1)) e (5) - e (3)))))\} \in Dioph (6)) \to \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| ((e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} (e (2) + 1)) \land ((e (4) \in ℤ_{\geq 2} \land e (5) = e (4) Y_{rm} e (2)) \land ((e (4) \in ℤ_{\geq 2} \land e (6) = e (4) X_{rm} e (2)) \land (e (3) < 2 e (4) e (1) - {e (1)}^{2} - 1 \land (2 e (4) e (1) - {e (1)}^{2} - 1) ∥ (e (6) - (e (4) - e (1)) e (5) - e (3))))))\} \in Dioph (6)$
249	181 247 248	mp2an	$⊢ \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| ((e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} (e (2) + 1)) \land ((e (4) \in ℤ_{\geq 2} \land e (5) = e (4) Y_{rm} e (2)) \land ((e (4) \in ℤ_{\geq 2} \land e (6) = e (4) X_{rm} e (2)) \land (e (3) < 2 e (4) e (1) - {e (1)}^{2} - 1 \land (2 e (4) e (1) - {e (1)}^{2} - 1) ∥ (e (6) - (e (4) - e (1)) e (5) - e (3))))))\} \in Dioph (6)$
250		anrabdioph	$⊢ (\{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| (e (1) \in ℤ_{\geq 2} \land e (2) \in ℕ)\} \in Dioph (6) \land \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| ((e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} (e (2) + 1)) \land ((e (4) \in ℤ_{\geq 2} \land e (5) = e (4) Y_{rm} e (2)) \land ((e (4) \in ℤ_{\geq 2} \land e (6) = e (4) X_{rm} e (2)) \land (e (3) < 2 e (4) e (1) - {e (1)}^{2} - 1 \land (2 e (4) e (1) - {e (1)}^{2} - 1) ∥ (e (6) - (e (4) - e (1)) e (5) - e (3))))))\} \in Dioph (6)) \to \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| ((e (1) \in ℤ_{\geq 2} \land e (2) \in ℕ) \land ((e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} (e (2) + 1)) \land ((e (4) \in ℤ_{\geq 2} \land e (5) = e (4) Y_{rm} e (2)) \land ((e (4) \in ℤ_{\geq 2} \land e (6) = e (4) X_{rm} e (2)) \land (e (3) < 2 e (4) e (1) - {e (1)}^{2} - 1 \land (2 e (4) e (1) - {e (1)}^{2} - 1) ∥ (e (6) - (e (4) - e (1)) e (5) - e (3)))))))\} \in Dioph (6)$
251	113 249 250	mp2an	$⊢ \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| ((e (1) \in ℤ_{\geq 2} \land e (2) \in ℕ) \land ((e (1) \in ℤ_{\geq 2} \land e (4) = e (1) Y_{rm} (e (2) + 1)) \land ((e (4) \in ℤ_{\geq 2} \land e (5) = e (4) Y_{rm} e (2)) \land ((e (4) \in ℤ_{\geq 2} \land e (6) = e (4) X_{rm} e (2)) \land (e (3) < 2 e (4) e (1) - {e (1)}^{2} - 1 \land (2 e (4) e (1) - {e (1)}^{2} - 1) ∥ (e (6) - (e (4) - e (1)) e (5) - e (3)))))))\} \in Dioph (6)$
252	89 251	eqeltri	$⊢ \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| \underset{˙}{[} ({e ↾}_{(1 \dots 3)}) / a \underset{˙}{]} \underset{˙}{[} e (4) / b \underset{˙}{]} \underset{˙}{[} e (5) / c \underset{˙}{]} \underset{˙}{[} e (6) / d \underset{˙}{]} ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} (a (2) + 1)) \land ((b \in ℤ_{\geq 2} \land c = b Y_{rm} a (2)) \land ((b \in ℤ_{\geq 2} \land d = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (d - (b - a (1)) c - a (3)))))))\} \in Dioph (6)$
253	93 94 95	3rexfrabdioph	$⊢ (3 \in ℕ_{0} \land \{e \in ({ℕ_{0}}^{(1 \dots 6)}) \| \underset{˙}{[} ({e ↾}_{(1 \dots 3)}) / a \underset{˙}{]} \underset{˙}{[} e (4) / b \underset{˙}{]} \underset{˙}{[} e (5) / c \underset{˙}{]} \underset{˙}{[} e (6) / d \underset{˙}{]} ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} (a (2) + 1)) \land ((b \in ℤ_{\geq 2} \land c = b Y_{rm} a (2)) \land ((b \in ℤ_{\geq 2} \land d = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (d - (b - a (1)) c - a (3)))))))\} \in Dioph (6)) \to \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} (a (2) + 1)) \land ((b \in ℤ_{\geq 2} \land c = b Y_{rm} a (2)) \land ((b \in ℤ_{\geq 2} \land d = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (d - (b - a (1)) c - a (3)))))))\} \in Dioph (3)$
254	9 252 253	mp2an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| \exists b \in ℕ_{0} \exists c \in ℕ_{0} \exists d \in ℕ_{0} ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} (a (2) + 1)) \land ((b \in ℤ_{\geq 2} \land c = b Y_{rm} a (2)) \land ((b \in ℤ_{\geq 2} \land d = b X_{rm} a (2)) \land (a (3) < 2 b a (1) - {a (1)}^{2} - 1 \land (2 b a (1) - {a (1)}^{2} - 1) ∥ (d - (b - a (1)) c - a (3)))))))\} \in Dioph (3)$
255	8 254	eqeltri	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| ((a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ) \land a (3) = {a (1)}^{a (2)})\} \in Dioph (3)$

Metamath Proof Explorer

Theorem expdiophlem2

Proof