rmxdioph

Description: X is a Diophantine function. (Contributed by Stefan O'Rear, 17-Oct-2014)

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

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \to a (1) \in ℤ_{\geq 2}$
2		elmapi	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to a : (1 \dots 3) ⟶ ℕ_{0}$
3		df-3	$⊢ 3 = 2 + 1$
4		ssid	$⊢ (1 \dots 3) \subseteq (1 \dots 3)$
5	3 4	jm2.27dlem5	$⊢ (1 \dots 2) \subseteq (1 \dots 3)$
6		2nn	$⊢ 2 \in ℕ$
7	6	jm2.27dlem3	$⊢ 2 \in (1 \dots 2)$
8	5 7	sselii	$⊢ 2 \in (1 \dots 3)$
9		ffvelrn	$⊢ (a : (1 \dots 3) ⟶ ℕ_{0} \land 2 \in (1 \dots 3)) \to a (2) \in ℕ_{0}$
10	2 8 9	sylancl	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to a (2) \in ℕ_{0}$
11	10	adantr	$⊢ (a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \to a (2) \in ℕ_{0}$
12		3nn	$⊢ 3 \in ℕ$
13	12	jm2.27dlem3	$⊢ 3 \in (1 \dots 3)$
14		ffvelrn	$⊢ (a : (1 \dots 3) ⟶ ℕ_{0} \land 3 \in (1 \dots 3)) \to a (3) \in ℕ_{0}$
15	2 13 14	sylancl	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to a (3) \in ℕ_{0}$
16	15	adantr	$⊢ (a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \to a (3) \in ℕ_{0}$
17		rmxdiophlem	$⊢ (a (1) \in ℤ_{\geq 2} \land a (2) \in ℕ_{0} \land a (3) \in ℕ_{0}) \to (a (3) = a (1) X_{rm} a (2) \leftrightarrow \exists b \in ℕ_{0} (b = a (1) Y_{rm} a (2) \land {a (3)}^{2} - ({a (1)}^{2} - 1) b^{2} = 1))$
18	1 11 16 17	syl3anc	$⊢ (a \in ({ℕ_{0}}^{(1 \dots 3)}) \land a (1) \in ℤ_{\geq 2}) \to (a (3) = a (1) X_{rm} a (2) \leftrightarrow \exists b \in ℕ_{0} (b = a (1) Y_{rm} a (2) \land {a (3)}^{2} - ({a (1)}^{2} - 1) b^{2} = 1))$
19	18	pm5.32da	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to ((a (1) \in ℤ_{\geq 2} \land a (3) = a (1) X_{rm} a (2)) \leftrightarrow (a (1) \in ℤ_{\geq 2} \land \exists b \in ℕ_{0} (b = a (1) Y_{rm} a (2) \land {a (3)}^{2} - ({a (1)}^{2} - 1) b^{2} = 1)))$
20		anass	$⊢ ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} a (2)) \land {a (3)}^{2} - ({a (1)}^{2} - 1) b^{2} = 1) \leftrightarrow (a (1) \in ℤ_{\geq 2} \land (b = a (1) Y_{rm} a (2) \land {a (3)}^{2} - ({a (1)}^{2} - 1) b^{2} = 1))$
21	20	rexbii	$⊢ \exists b \in ℕ_{0} ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} a (2)) \land {a (3)}^{2} - ({a (1)}^{2} - 1) b^{2} = 1) \leftrightarrow \exists b \in ℕ_{0} (a (1) \in ℤ_{\geq 2} \land (b = a (1) Y_{rm} a (2) \land {a (3)}^{2} - ({a (1)}^{2} - 1) b^{2} = 1))$
22		r19.42v	$⊢ \exists b \in ℕ_{0} (a (1) \in ℤ_{\geq 2} \land (b = a (1) Y_{rm} a (2) \land {a (3)}^{2} - ({a (1)}^{2} - 1) b^{2} = 1)) \leftrightarrow (a (1) \in ℤ_{\geq 2} \land \exists b \in ℕ_{0} (b = a (1) Y_{rm} a (2) \land {a (3)}^{2} - ({a (1)}^{2} - 1) b^{2} = 1))$
23	21 22	bitr2i	$⊢ (a (1) \in ℤ_{\geq 2} \land \exists b \in ℕ_{0} (b = a (1) Y_{rm} a (2) \land {a (3)}^{2} - ({a (1)}^{2} - 1) b^{2} = 1)) \leftrightarrow \exists b \in ℕ_{0} ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} a (2)) \land {a (3)}^{2} - ({a (1)}^{2} - 1) b^{2} = 1)$
24	19 23	bitrdi	$⊢ a \in ({ℕ_{0}}^{(1 \dots 3)}) \to ((a (1) \in ℤ_{\geq 2} \land a (3) = a (1) X_{rm} a (2)) \leftrightarrow \exists b \in ℕ_{0} ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} a (2)) \land {a (3)}^{2} - ({a (1)}^{2} - 1) b^{2} = 1))$
25	24	rabbiia	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (1) \in ℤ_{\geq 2} \land a (3) = a (1) X_{rm} a (2))\} = \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| \exists b \in ℕ_{0} ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} a (2)) \land {a (3)}^{2} - ({a (1)}^{2} - 1) b^{2} = 1)\}$
26		3nn0	$⊢ 3 \in ℕ_{0}$
27		vex	$⊢ c \in V$
28	27	resex	$⊢ {c ↾}_{(1 \dots 3)} \in V$
29		fvex	$⊢ c (4) \in V$
30		df-2	$⊢ 2 = 1 + 1$
31	30 5	jm2.27dlem5	$⊢ (1 \dots 1) \subseteq (1 \dots 3)$
32		1nn	$⊢ 1 \in ℕ$
33	32	jm2.27dlem3	$⊢ 1 \in (1 \dots 1)$
34	31 33	sselii	$⊢ 1 \in (1 \dots 3)$
35	34	jm2.27dlem1	$⊢ a = {c ↾}_{(1 \dots 3)} \to a (1) = c (1)$
36	35	eleq1d	$⊢ a = {c ↾}_{(1 \dots 3)} \to (a (1) \in ℤ_{\geq 2} \leftrightarrow c (1) \in ℤ_{\geq 2})$
37	36	adantr	$⊢ (a = {c ↾}_{(1 \dots 3)} \land b = c (4)) \to (a (1) \in ℤ_{\geq 2} \leftrightarrow c (1) \in ℤ_{\geq 2})$
38		simpr	$⊢ (a = {c ↾}_{(1 \dots 3)} \land b = c (4)) \to b = c (4)$
39	8	jm2.27dlem1	$⊢ a = {c ↾}_{(1 \dots 3)} \to a (2) = c (2)$
40	35 39	oveq12d	$⊢ a = {c ↾}_{(1 \dots 3)} \to a (1) Y_{rm} a (2) = c (1) Y_{rm} c (2)$
41	40	adantr	$⊢ (a = {c ↾}_{(1 \dots 3)} \land b = c (4)) \to a (1) Y_{rm} a (2) = c (1) Y_{rm} c (2)$
42	38 41	eqeq12d	$⊢ (a = {c ↾}_{(1 \dots 3)} \land b = c (4)) \to (b = a (1) Y_{rm} a (2) \leftrightarrow c (4) = c (1) Y_{rm} c (2))$
43	37 42	anbi12d	$⊢ (a = {c ↾}_{(1 \dots 3)} \land b = c (4)) \to ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} a (2)) \leftrightarrow (c (1) \in ℤ_{\geq 2} \land c (4) = c (1) Y_{rm} c (2)))$
44	13	jm2.27dlem1	$⊢ a = {c ↾}_{(1 \dots 3)} \to a (3) = c (3)$
45	44	oveq1d	$⊢ a = {c ↾}_{(1 \dots 3)} \to {a (3)}^{2} = {c (3)}^{2}$
46	45	adantr	$⊢ (a = {c ↾}_{(1 \dots 3)} \land b = c (4)) \to {a (3)}^{2} = {c (3)}^{2}$
47	35	oveq1d	$⊢ a = {c ↾}_{(1 \dots 3)} \to {a (1)}^{2} = {c (1)}^{2}$
48	47	oveq1d	$⊢ a = {c ↾}_{(1 \dots 3)} \to {a (1)}^{2} - 1 = {c (1)}^{2} - 1$
49		oveq1	$⊢ b = c (4) \to b^{2} = {c (4)}^{2}$
50	48 49	oveqan12d	$⊢ (a = {c ↾}_{(1 \dots 3)} \land b = c (4)) \to ({a (1)}^{2} - 1) b^{2} = ({c (1)}^{2} - 1) {c (4)}^{2}$
51	46 50	oveq12d	$⊢ (a = {c ↾}_{(1 \dots 3)} \land b = c (4)) \to {a (3)}^{2} - ({a (1)}^{2} - 1) b^{2} = {c (3)}^{2} - ({c (1)}^{2} - 1) {c (4)}^{2}$
52	51	eqeq1d	$⊢ (a = {c ↾}_{(1 \dots 3)} \land b = c (4)) \to ({a (3)}^{2} - ({a (1)}^{2} - 1) b^{2} = 1 \leftrightarrow {c (3)}^{2} - ({c (1)}^{2} - 1) {c (4)}^{2} = 1)$
53	43 52	anbi12d	$⊢ (a = {c ↾}_{(1 \dots 3)} \land b = c (4)) \to (((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} a (2)) \land {a (3)}^{2} - ({a (1)}^{2} - 1) b^{2} = 1) \leftrightarrow ((c (1) \in ℤ_{\geq 2} \land c (4) = c (1) Y_{rm} c (2)) \land {c (3)}^{2} - ({c (1)}^{2} - 1) {c (4)}^{2} = 1))$
54	28 29 53	sbc2ie	$⊢ \underset{˙}{[} ({c ↾}_{(1 \dots 3)}) / a \underset{˙}{]} \underset{˙}{[} c (4) / b \underset{˙}{]} ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} a (2)) \land {a (3)}^{2} - ({a (1)}^{2} - 1) b^{2} = 1) \leftrightarrow ((c (1) \in ℤ_{\geq 2} \land c (4) = c (1) Y_{rm} c (2)) \land {c (3)}^{2} - ({c (1)}^{2} - 1) {c (4)}^{2} = 1)$
55	54	rabbii	$⊢ \{c \in ({ℕ_{0}}^{(1 \dots 4)}) \| \underset{˙}{[} ({c ↾}_{(1 \dots 3)}) / a \underset{˙}{]} \underset{˙}{[} c (4) / b \underset{˙}{]} ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} a (2)) \land {a (3)}^{2} - ({a (1)}^{2} - 1) b^{2} = 1)\} = \{c \in ({ℕ_{0}}^{(1 \dots 4)}) \| ((c (1) \in ℤ_{\geq 2} \land c (4) = c (1) Y_{rm} c (2)) \land {c (3)}^{2} - ({c (1)}^{2} - 1) {c (4)}^{2} = 1)\}$
56		4nn0	$⊢ 4 \in ℕ_{0}$
57		rmydioph	$⊢ \{b \in ({ℕ_{0}}^{(1 \dots 3)}) \| (b (1) \in ℤ_{\geq 2} \land b (3) = b (1) Y_{rm} b (2))\} \in Dioph (3)$
58		simp1	$⊢ (b (1) = c (1) \land b (2) = c (2) \land b (3) = c (4)) \to b (1) = c (1)$
59	58	eleq1d	$⊢ (b (1) = c (1) \land b (2) = c (2) \land b (3) = c (4)) \to (b (1) \in ℤ_{\geq 2} \leftrightarrow c (1) \in ℤ_{\geq 2})$
60		simp3	$⊢ (b (1) = c (1) \land b (2) = c (2) \land b (3) = c (4)) \to b (3) = c (4)$
61		simp2	$⊢ (b (1) = c (1) \land b (2) = c (2) \land b (3) = c (4)) \to b (2) = c (2)$
62	58 61	oveq12d	$⊢ (b (1) = c (1) \land b (2) = c (2) \land b (3) = c (4)) \to b (1) Y_{rm} b (2) = c (1) Y_{rm} c (2)$
63	60 62	eqeq12d	$⊢ (b (1) = c (1) \land b (2) = c (2) \land b (3) = c (4)) \to (b (3) = b (1) Y_{rm} b (2) \leftrightarrow c (4) = c (1) Y_{rm} c (2))$
64	59 63	anbi12d	$⊢ (b (1) = c (1) \land b (2) = c (2) \land b (3) = c (4)) \to ((b (1) \in ℤ_{\geq 2} \land b (3) = b (1) Y_{rm} b (2)) \leftrightarrow (c (1) \in ℤ_{\geq 2} \land c (4) = c (1) Y_{rm} c (2)))$
65		df-4	$⊢ 4 = 3 + 1$
66		ssid	$⊢ (1 \dots 4) \subseteq (1 \dots 4)$
67	65 66	jm2.27dlem5	$⊢ (1 \dots 3) \subseteq (1 \dots 4)$
68	3 67	jm2.27dlem5	$⊢ (1 \dots 2) \subseteq (1 \dots 4)$
69	30 68	jm2.27dlem5	$⊢ (1 \dots 1) \subseteq (1 \dots 4)$
70	69 33	sselii	$⊢ 1 \in (1 \dots 4)$
71	68 7	sselii	$⊢ 2 \in (1 \dots 4)$
72		4nn	$⊢ 4 \in ℕ$
73	72	jm2.27dlem3	$⊢ 4 \in (1 \dots 4)$
74	64 70 71 73	rabren3dioph	$⊢ (4 \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 \{c \in ({ℕ_{0}}^{(1 \dots 4)}) \| (c (1) \in ℤ_{\geq 2} \land c (4) = c (1) Y_{rm} c (2))\} \in Dioph (4)$
75	56 57 74	mp2an	$⊢ \{c \in ({ℕ_{0}}^{(1 \dots 4)}) \| (c (1) \in ℤ_{\geq 2} \land c (4) = c (1) Y_{rm} c (2))\} \in Dioph (4)$
76		ovex	$⊢ (1 \dots 4) \in V$
77	67 13	sselii	$⊢ 3 \in (1 \dots 4)$
78		mzpproj	$⊢ ((1 \dots 4) \in V \land 3 \in (1 \dots 4)) \to (c \in (ℤ^{(1 \dots 4)}) ⟼ c (3)) \in mzPoly ((1 \dots 4))$
79	76 77 78	mp2an	$⊢ (c \in (ℤ^{(1 \dots 4)}) ⟼ c (3)) \in mzPoly ((1 \dots 4))$
80		2nn0	$⊢ 2 \in ℕ_{0}$
81		mzpexpmpt	$⊢ ((c \in (ℤ^{(1 \dots 4)}) ⟼ c (3)) \in mzPoly ((1 \dots 4)) \land 2 \in ℕ_{0}) \to (c \in (ℤ^{(1 \dots 4)}) ⟼ {c (3)}^{2}) \in mzPoly ((1 \dots 4))$
82	79 80 81	mp2an	$⊢ (c \in (ℤ^{(1 \dots 4)}) ⟼ {c (3)}^{2}) \in mzPoly ((1 \dots 4))$
83		mzpproj	$⊢ ((1 \dots 4) \in V \land 1 \in (1 \dots 4)) \to (c \in (ℤ^{(1 \dots 4)}) ⟼ c (1)) \in mzPoly ((1 \dots 4))$
84	76 70 83	mp2an	$⊢ (c \in (ℤ^{(1 \dots 4)}) ⟼ c (1)) \in mzPoly ((1 \dots 4))$
85		mzpexpmpt	$⊢ ((c \in (ℤ^{(1 \dots 4)}) ⟼ c (1)) \in mzPoly ((1 \dots 4)) \land 2 \in ℕ_{0}) \to (c \in (ℤ^{(1 \dots 4)}) ⟼ {c (1)}^{2}) \in mzPoly ((1 \dots 4))$
86	84 80 85	mp2an	$⊢ (c \in (ℤ^{(1 \dots 4)}) ⟼ {c (1)}^{2}) \in mzPoly ((1 \dots 4))$
87		1z	$⊢ 1 \in ℤ$
88		mzpconstmpt	$⊢ ((1 \dots 4) \in V \land 1 \in ℤ) \to (c \in (ℤ^{(1 \dots 4)}) ⟼ 1) \in mzPoly ((1 \dots 4))$
89	76 87 88	mp2an	$⊢ (c \in (ℤ^{(1 \dots 4)}) ⟼ 1) \in mzPoly ((1 \dots 4))$
90		mzpsubmpt	$⊢ ((c \in (ℤ^{(1 \dots 4)}) ⟼ {c (1)}^{2}) \in mzPoly ((1 \dots 4)) \land (c \in (ℤ^{(1 \dots 4)}) ⟼ 1) \in mzPoly ((1 \dots 4))) \to (c \in (ℤ^{(1 \dots 4)}) ⟼ {c (1)}^{2} - 1) \in mzPoly ((1 \dots 4))$
91	86 89 90	mp2an	$⊢ (c \in (ℤ^{(1 \dots 4)}) ⟼ {c (1)}^{2} - 1) \in mzPoly ((1 \dots 4))$
92		mzpproj	$⊢ ((1 \dots 4) \in V \land 4 \in (1 \dots 4)) \to (c \in (ℤ^{(1 \dots 4)}) ⟼ c (4)) \in mzPoly ((1 \dots 4))$
93	76 73 92	mp2an	$⊢ (c \in (ℤ^{(1 \dots 4)}) ⟼ c (4)) \in mzPoly ((1 \dots 4))$
94		mzpexpmpt	$⊢ ((c \in (ℤ^{(1 \dots 4)}) ⟼ c (4)) \in mzPoly ((1 \dots 4)) \land 2 \in ℕ_{0}) \to (c \in (ℤ^{(1 \dots 4)}) ⟼ {c (4)}^{2}) \in mzPoly ((1 \dots 4))$
95	93 80 94	mp2an	$⊢ (c \in (ℤ^{(1 \dots 4)}) ⟼ {c (4)}^{2}) \in mzPoly ((1 \dots 4))$
96		mzpmulmpt	$⊢ ((c \in (ℤ^{(1 \dots 4)}) ⟼ {c (1)}^{2} - 1) \in mzPoly ((1 \dots 4)) \land (c \in (ℤ^{(1 \dots 4)}) ⟼ {c (4)}^{2}) \in mzPoly ((1 \dots 4))) \to (c \in (ℤ^{(1 \dots 4)}) ⟼ ({c (1)}^{2} - 1) {c (4)}^{2}) \in mzPoly ((1 \dots 4))$
97	91 95 96	mp2an	$⊢ (c \in (ℤ^{(1 \dots 4)}) ⟼ ({c (1)}^{2} - 1) {c (4)}^{2}) \in mzPoly ((1 \dots 4))$
98		mzpsubmpt	$⊢ ((c \in (ℤ^{(1 \dots 4)}) ⟼ {c (3)}^{2}) \in mzPoly ((1 \dots 4)) \land (c \in (ℤ^{(1 \dots 4)}) ⟼ ({c (1)}^{2} - 1) {c (4)}^{2}) \in mzPoly ((1 \dots 4))) \to (c \in (ℤ^{(1 \dots 4)}) ⟼ {c (3)}^{2} - ({c (1)}^{2} - 1) {c (4)}^{2}) \in mzPoly ((1 \dots 4))$
99	82 97 98	mp2an	$⊢ (c \in (ℤ^{(1 \dots 4)}) ⟼ {c (3)}^{2} - ({c (1)}^{2} - 1) {c (4)}^{2}) \in mzPoly ((1 \dots 4))$
100		eqrabdioph	$⊢ (4 \in ℕ_{0} \land (c \in (ℤ^{(1 \dots 4)}) ⟼ {c (3)}^{2} - ({c (1)}^{2} - 1) {c (4)}^{2}) \in mzPoly ((1 \dots 4)) \land (c \in (ℤ^{(1 \dots 4)}) ⟼ 1) \in mzPoly ((1 \dots 4))) \to \{c \in ({ℕ_{0}}^{(1 \dots 4)}) \| {c (3)}^{2} - ({c (1)}^{2} - 1) {c (4)}^{2} = 1\} \in Dioph (4)$
101	56 99 89 100	mp3an	$⊢ \{c \in ({ℕ_{0}}^{(1 \dots 4)}) \| {c (3)}^{2} - ({c (1)}^{2} - 1) {c (4)}^{2} = 1\} \in Dioph (4)$
102		anrabdioph	$⊢ (\{c \in ({ℕ_{0}}^{(1 \dots 4)}) \| (c (1) \in ℤ_{\geq 2} \land c (4) = c (1) Y_{rm} c (2))\} \in Dioph (4) \land \{c \in ({ℕ_{0}}^{(1 \dots 4)}) \| {c (3)}^{2} - ({c (1)}^{2} - 1) {c (4)}^{2} = 1\} \in Dioph (4)) \to \{c \in ({ℕ_{0}}^{(1 \dots 4)}) \| ((c (1) \in ℤ_{\geq 2} \land c (4) = c (1) Y_{rm} c (2)) \land {c (3)}^{2} - ({c (1)}^{2} - 1) {c (4)}^{2} = 1)\} \in Dioph (4)$
103	75 101 102	mp2an	$⊢ \{c \in ({ℕ_{0}}^{(1 \dots 4)}) \| ((c (1) \in ℤ_{\geq 2} \land c (4) = c (1) Y_{rm} c (2)) \land {c (3)}^{2} - ({c (1)}^{2} - 1) {c (4)}^{2} = 1)\} \in Dioph (4)$
104	55 103	eqeltri	$⊢ \{c \in ({ℕ_{0}}^{(1 \dots 4)}) \| \underset{˙}{[} ({c ↾}_{(1 \dots 3)}) / a \underset{˙}{]} \underset{˙}{[} c (4) / b \underset{˙}{]} ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} a (2)) \land {a (3)}^{2} - ({a (1)}^{2} - 1) b^{2} = 1)\} \in Dioph (4)$
105	65	rexfrabdioph	$⊢ (3 \in ℕ_{0} \land \{c \in ({ℕ_{0}}^{(1 \dots 4)}) \| \underset{˙}{[} ({c ↾}_{(1 \dots 3)}) / a \underset{˙}{]} \underset{˙}{[} c (4) / b \underset{˙}{]} ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} a (2)) \land {a (3)}^{2} - ({a (1)}^{2} - 1) b^{2} = 1)\} \in Dioph (4)) \to \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| \exists b \in ℕ_{0} ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} a (2)) \land {a (3)}^{2} - ({a (1)}^{2} - 1) b^{2} = 1)\} \in Dioph (3)$
106	26 104 105	mp2an	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| \exists b \in ℕ_{0} ((a (1) \in ℤ_{\geq 2} \land b = a (1) Y_{rm} a (2)) \land {a (3)}^{2} - ({a (1)}^{2} - 1) b^{2} = 1)\} \in Dioph (3)$
107	25 106	eqeltri	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots 3)}) \| (a (1) \in ℤ_{\geq 2} \land a (3) = a (1) X_{rm} a (2))\} \in Dioph (3)$

Metamath Proof Explorer

Theorem rmxdioph

Proof