rmxycomplete

Description: The X and Y sequences taken together enumerate all solutions to the corresponding Pell equation in the right half-plane. This is Metamath 100 proof #39. (Contributed by Stefan O'Rear, 22-Sep-2014)

		Ref	Expression
	Assertion	rmxycomplete	$⊢ (A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \to (X^{2} - (A^{2} - 1) Y^{2} = 1 \leftrightarrow \exists n \in ℤ (X = A X_{rm} n \land Y = A Y_{rm} n))$

Proof

Step	Hyp	Ref	Expression
1		rmspecnonsq	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in (ℕ ∖ ◻_{ℕ})$
2	1	3ad2ant1	$⊢ (A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \to A^{2} - 1 \in (ℕ ∖ ◻_{ℕ})$
3		pellfund14b	$⊢ A^{2} - 1 \in (ℕ ∖ ◻_{ℕ}) \to (X + \sqrt{A^{2} - 1} Y \in Pell14QR (A^{2} - 1) \leftrightarrow \exists n \in ℤ X + \sqrt{A^{2} - 1} Y = {PellFund (A^{2} - 1)}^{n})$
4	2 3	syl	$⊢ (A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \to (X + \sqrt{A^{2} - 1} Y \in Pell14QR (A^{2} - 1) \leftrightarrow \exists n \in ℤ X + \sqrt{A^{2} - 1} Y = {PellFund (A^{2} - 1)}^{n})$
5		nn0re	$⊢ X \in ℕ_{0} \to X \in ℝ$
6	5	3ad2ant2	$⊢ (A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \to X \in ℝ$
7		rmspecpos	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in ℝ^{+}$
8	7	rpsqrtcld	$⊢ A \in ℤ_{\geq 2} \to \sqrt{A^{2} - 1} \in ℝ^{+}$
9	8	rpred	$⊢ A \in ℤ_{\geq 2} \to \sqrt{A^{2} - 1} \in ℝ$
10	9	3ad2ant1	$⊢ (A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \to \sqrt{A^{2} - 1} \in ℝ$
11		zre	$⊢ Y \in ℤ \to Y \in ℝ$
12	11	3ad2ant3	$⊢ (A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \to Y \in ℝ$
13	10 12	remulcld	$⊢ (A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \to \sqrt{A^{2} - 1} Y \in ℝ$
14	6 13	readdcld	$⊢ (A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \to X + \sqrt{A^{2} - 1} Y \in ℝ$
15	14	biantrurd	$⊢ (A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \to (\exists x \in ℕ_{0} \exists y \in ℤ (X + \sqrt{A^{2} - 1} Y = x + \sqrt{A^{2} - 1} y \land x^{2} - (A^{2} - 1) y^{2} = 1) \leftrightarrow (X + \sqrt{A^{2} - 1} Y \in ℝ \land \exists x \in ℕ_{0} \exists y \in ℤ (X + \sqrt{A^{2} - 1} Y = x + \sqrt{A^{2} - 1} y \land x^{2} - (A^{2} - 1) y^{2} = 1)))$
16		simpl2	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land X^{2} - (A^{2} - 1) Y^{2} = 1) \to X \in ℕ_{0}$
17		simpl3	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land X^{2} - (A^{2} - 1) Y^{2} = 1) \to Y \in ℤ$
18		eqidd	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land X^{2} - (A^{2} - 1) Y^{2} = 1) \to X + \sqrt{A^{2} - 1} Y = X + \sqrt{A^{2} - 1} Y$
19		simpr	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land X^{2} - (A^{2} - 1) Y^{2} = 1) \to X^{2} - (A^{2} - 1) Y^{2} = 1$
20		oveq1	$⊢ x = X \to x + \sqrt{A^{2} - 1} y = X + \sqrt{A^{2} - 1} y$
21	20	eqeq2d	$⊢ x = X \to (X + \sqrt{A^{2} - 1} Y = x + \sqrt{A^{2} - 1} y \leftrightarrow X + \sqrt{A^{2} - 1} Y = X + \sqrt{A^{2} - 1} y)$
22		oveq1	$⊢ x = X \to x^{2} = X^{2}$
23	22	oveq1d	$⊢ x = X \to x^{2} - (A^{2} - 1) y^{2} = X^{2} - (A^{2} - 1) y^{2}$
24	23	eqeq1d	$⊢ x = X \to (x^{2} - (A^{2} - 1) y^{2} = 1 \leftrightarrow X^{2} - (A^{2} - 1) y^{2} = 1)$
25	21 24	anbi12d	$⊢ x = X \to ((X + \sqrt{A^{2} - 1} Y = x + \sqrt{A^{2} - 1} y \land x^{2} - (A^{2} - 1) y^{2} = 1) \leftrightarrow (X + \sqrt{A^{2} - 1} Y = X + \sqrt{A^{2} - 1} y \land X^{2} - (A^{2} - 1) y^{2} = 1))$
26		oveq2	$⊢ y = Y \to \sqrt{A^{2} - 1} y = \sqrt{A^{2} - 1} Y$
27	26	oveq2d	$⊢ y = Y \to X + \sqrt{A^{2} - 1} y = X + \sqrt{A^{2} - 1} Y$
28	27	eqeq2d	$⊢ y = Y \to (X + \sqrt{A^{2} - 1} Y = X + \sqrt{A^{2} - 1} y \leftrightarrow X + \sqrt{A^{2} - 1} Y = X + \sqrt{A^{2} - 1} Y)$
29		oveq1	$⊢ y = Y \to y^{2} = Y^{2}$
30	29	oveq2d	$⊢ y = Y \to (A^{2} - 1) y^{2} = (A^{2} - 1) Y^{2}$
31	30	oveq2d	$⊢ y = Y \to X^{2} - (A^{2} - 1) y^{2} = X^{2} - (A^{2} - 1) Y^{2}$
32	31	eqeq1d	$⊢ y = Y \to (X^{2} - (A^{2} - 1) y^{2} = 1 \leftrightarrow X^{2} - (A^{2} - 1) Y^{2} = 1)$
33	28 32	anbi12d	$⊢ y = Y \to ((X + \sqrt{A^{2} - 1} Y = X + \sqrt{A^{2} - 1} y \land X^{2} - (A^{2} - 1) y^{2} = 1) \leftrightarrow (X + \sqrt{A^{2} - 1} Y = X + \sqrt{A^{2} - 1} Y \land X^{2} - (A^{2} - 1) Y^{2} = 1))$
34	25 33	rspc2ev	$⊢ (X \in ℕ_{0} \land Y \in ℤ \land (X + \sqrt{A^{2} - 1} Y = X + \sqrt{A^{2} - 1} Y \land X^{2} - (A^{2} - 1) Y^{2} = 1)) \to \exists x \in ℕ_{0} \exists y \in ℤ (X + \sqrt{A^{2} - 1} Y = x + \sqrt{A^{2} - 1} y \land x^{2} - (A^{2} - 1) y^{2} = 1)$
35	16 17 18 19 34	syl112anc	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land X^{2} - (A^{2} - 1) Y^{2} = 1) \to \exists x \in ℕ_{0} \exists y \in ℤ (X + \sqrt{A^{2} - 1} Y = x + \sqrt{A^{2} - 1} y \land x^{2} - (A^{2} - 1) y^{2} = 1)$
36	35	ex	$⊢ (A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \to (X^{2} - (A^{2} - 1) Y^{2} = 1 \to \exists x \in ℕ_{0} \exists y \in ℤ (X + \sqrt{A^{2} - 1} Y = x + \sqrt{A^{2} - 1} y \land x^{2} - (A^{2} - 1) y^{2} = 1))$
37		rmspecsqrtnq	$⊢ A \in ℤ_{\geq 2} \to \sqrt{A^{2} - 1} \in (ℂ ∖ ℚ)$
38	37	3ad2ant1	$⊢ (A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \to \sqrt{A^{2} - 1} \in (ℂ ∖ ℚ)$
39	38	adantr	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land (x \in ℕ_{0} \land y \in ℤ)) \to \sqrt{A^{2} - 1} \in (ℂ ∖ ℚ)$
40		nn0ssq	$⊢ ℕ_{0} \subseteq ℚ$
41		simp2	$⊢ (A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \to X \in ℕ_{0}$
42	40 41	sselid	$⊢ (A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \to X \in ℚ$
43	42	adantr	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land (x \in ℕ_{0} \land y \in ℤ)) \to X \in ℚ$
44		zq	$⊢ Y \in ℤ \to Y \in ℚ$
45	44	3ad2ant3	$⊢ (A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \to Y \in ℚ$
46	45	adantr	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land (x \in ℕ_{0} \land y \in ℤ)) \to Y \in ℚ$
47	40	sseli	$⊢ x \in ℕ_{0} \to x \in ℚ$
48	47	ad2antrl	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land (x \in ℕ_{0} \land y \in ℤ)) \to x \in ℚ$
49		zq	$⊢ y \in ℤ \to y \in ℚ$
50	49	ad2antll	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land (x \in ℕ_{0} \land y \in ℤ)) \to y \in ℚ$
51		qirropth	$⊢ (\sqrt{A^{2} - 1} \in (ℂ ∖ ℚ) \land (X \in ℚ \land Y \in ℚ) \land (x \in ℚ \land y \in ℚ)) \to (X + \sqrt{A^{2} - 1} Y = x + \sqrt{A^{2} - 1} y \leftrightarrow (X = x \land Y = y))$
52	39 43 46 48 50 51	syl122anc	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land (x \in ℕ_{0} \land y \in ℤ)) \to (X + \sqrt{A^{2} - 1} Y = x + \sqrt{A^{2} - 1} y \leftrightarrow (X = x \land Y = y))$
53	52	biimpd	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land (x \in ℕ_{0} \land y \in ℤ)) \to (X + \sqrt{A^{2} - 1} Y = x + \sqrt{A^{2} - 1} y \to (X = x \land Y = y))$
54	53	anim1d	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land (x \in ℕ_{0} \land y \in ℤ)) \to ((X + \sqrt{A^{2} - 1} Y = x + \sqrt{A^{2} - 1} y \land x^{2} - (A^{2} - 1) y^{2} = 1) \to ((X = x \land Y = y) \land x^{2} - (A^{2} - 1) y^{2} = 1))$
55		oveq1	$⊢ X = x \to X^{2} = x^{2}$
56		oveq1	$⊢ Y = y \to Y^{2} = y^{2}$
57	56	oveq2d	$⊢ Y = y \to (A^{2} - 1) Y^{2} = (A^{2} - 1) y^{2}$
58	55 57	oveqan12d	$⊢ (X = x \land Y = y) \to X^{2} - (A^{2} - 1) Y^{2} = x^{2} - (A^{2} - 1) y^{2}$
59	58	eqcomd	$⊢ (X = x \land Y = y) \to x^{2} - (A^{2} - 1) y^{2} = X^{2} - (A^{2} - 1) Y^{2}$
60	59	eqeq1d	$⊢ (X = x \land Y = y) \to (x^{2} - (A^{2} - 1) y^{2} = 1 \leftrightarrow X^{2} - (A^{2} - 1) Y^{2} = 1)$
61	60	biimpa	$⊢ ((X = x \land Y = y) \land x^{2} - (A^{2} - 1) y^{2} = 1) \to X^{2} - (A^{2} - 1) Y^{2} = 1$
62	54 61	syl6	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land (x \in ℕ_{0} \land y \in ℤ)) \to ((X + \sqrt{A^{2} - 1} Y = x + \sqrt{A^{2} - 1} y \land x^{2} - (A^{2} - 1) y^{2} = 1) \to X^{2} - (A^{2} - 1) Y^{2} = 1)$
63	62	rexlimdvva	$⊢ (A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \to (\exists x \in ℕ_{0} \exists y \in ℤ (X + \sqrt{A^{2} - 1} Y = x + \sqrt{A^{2} - 1} y \land x^{2} - (A^{2} - 1) y^{2} = 1) \to X^{2} - (A^{2} - 1) Y^{2} = 1)$
64	36 63	impbid	$⊢ (A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \to (X^{2} - (A^{2} - 1) Y^{2} = 1 \leftrightarrow \exists x \in ℕ_{0} \exists y \in ℤ (X + \sqrt{A^{2} - 1} Y = x + \sqrt{A^{2} - 1} y \land x^{2} - (A^{2} - 1) y^{2} = 1))$
65		elpell14qr	$⊢ A^{2} - 1 \in (ℕ ∖ ◻_{ℕ}) \to (X + \sqrt{A^{2} - 1} Y \in Pell14QR (A^{2} - 1) \leftrightarrow (X + \sqrt{A^{2} - 1} Y \in ℝ \land \exists x \in ℕ_{0} \exists y \in ℤ (X + \sqrt{A^{2} - 1} Y = x + \sqrt{A^{2} - 1} y \land x^{2} - (A^{2} - 1) y^{2} = 1)))$
66	2 65	syl	$⊢ (A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \to (X + \sqrt{A^{2} - 1} Y \in Pell14QR (A^{2} - 1) \leftrightarrow (X + \sqrt{A^{2} - 1} Y \in ℝ \land \exists x \in ℕ_{0} \exists y \in ℤ (X + \sqrt{A^{2} - 1} Y = x + \sqrt{A^{2} - 1} y \land x^{2} - (A^{2} - 1) y^{2} = 1)))$
67	15 64 66	3bitr4d	$⊢ (A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \to (X^{2} - (A^{2} - 1) Y^{2} = 1 \leftrightarrow X + \sqrt{A^{2} - 1} Y \in Pell14QR (A^{2} - 1))$
68	38	adantr	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land n \in ℤ) \to \sqrt{A^{2} - 1} \in (ℂ ∖ ℚ)$
69	42	adantr	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land n \in ℤ) \to X \in ℚ$
70	45	adantr	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land n \in ℤ) \to Y \in ℚ$
71		frmx	$⊢ X_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℕ_{0}$
72	71	a1i	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land n \in ℤ) \to X_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℕ_{0}$
73		simpl1	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land n \in ℤ) \to A \in ℤ_{\geq 2}$
74		simpr	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land n \in ℤ) \to n \in ℤ$
75	72 73 74	fovcdmd	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land n \in ℤ) \to A X_{rm} n \in ℕ_{0}$
76	40 75	sselid	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land n \in ℤ) \to A X_{rm} n \in ℚ$
77		zssq	$⊢ ℤ \subseteq ℚ$
78		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
79	78	a1i	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land n \in ℤ) \to Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
80	79 73 74	fovcdmd	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land n \in ℤ) \to A Y_{rm} n \in ℤ$
81	77 80	sselid	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land n \in ℤ) \to A Y_{rm} n \in ℚ$
82		qirropth	$⊢ (\sqrt{A^{2} - 1} \in (ℂ ∖ ℚ) \land (X \in ℚ \land Y \in ℚ) \land (A X_{rm} n \in ℚ \land A Y_{rm} n \in ℚ)) \to (X + \sqrt{A^{2} - 1} Y = (A X_{rm} n) + \sqrt{A^{2} - 1} (A Y_{rm} n) \leftrightarrow (X = A X_{rm} n \land Y = A Y_{rm} n))$
83	68 69 70 76 81 82	syl122anc	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land n \in ℤ) \to (X + \sqrt{A^{2} - 1} Y = (A X_{rm} n) + \sqrt{A^{2} - 1} (A Y_{rm} n) \leftrightarrow (X = A X_{rm} n \land Y = A Y_{rm} n))$
84		rmxyval	$⊢ (A \in ℤ_{\geq 2} \land n \in ℤ) \to (A X_{rm} n) + \sqrt{A^{2} - 1} (A Y_{rm} n) = {(A + \sqrt{A^{2} - 1})}^{n}$
85	84	3ad2antl1	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land n \in ℤ) \to (A X_{rm} n) + \sqrt{A^{2} - 1} (A Y_{rm} n) = {(A + \sqrt{A^{2} - 1})}^{n}$
86		rmspecfund	$⊢ A \in ℤ_{\geq 2} \to PellFund (A^{2} - 1) = A + \sqrt{A^{2} - 1}$
87	86	3ad2ant1	$⊢ (A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \to PellFund (A^{2} - 1) = A + \sqrt{A^{2} - 1}$
88	87	adantr	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land n \in ℤ) \to PellFund (A^{2} - 1) = A + \sqrt{A^{2} - 1}$
89	88	oveq1d	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land n \in ℤ) \to {PellFund (A^{2} - 1)}^{n} = {(A + \sqrt{A^{2} - 1})}^{n}$
90	85 89	eqtr4d	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land n \in ℤ) \to (A X_{rm} n) + \sqrt{A^{2} - 1} (A Y_{rm} n) = {PellFund (A^{2} - 1)}^{n}$
91	90	eqeq2d	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land n \in ℤ) \to (X + \sqrt{A^{2} - 1} Y = (A X_{rm} n) + \sqrt{A^{2} - 1} (A Y_{rm} n) \leftrightarrow X + \sqrt{A^{2} - 1} Y = {PellFund (A^{2} - 1)}^{n})$
92	83 91	bitr3d	$⊢ ((A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \land n \in ℤ) \to ((X = A X_{rm} n \land Y = A Y_{rm} n) \leftrightarrow X + \sqrt{A^{2} - 1} Y = {PellFund (A^{2} - 1)}^{n})$
93	92	rexbidva	$⊢ (A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \to (\exists n \in ℤ (X = A X_{rm} n \land Y = A Y_{rm} n) \leftrightarrow \exists n \in ℤ X + \sqrt{A^{2} - 1} Y = {PellFund (A^{2} - 1)}^{n})$
94	4 67 93	3bitr4d	$⊢ (A \in ℤ_{\geq 2} \land X \in ℕ_{0} \land Y \in ℤ) \to (X^{2} - (A^{2} - 1) Y^{2} = 1 \leftrightarrow \exists n \in ℤ (X = A X_{rm} n \land Y = A Y_{rm} n))$

Metamath Proof Explorer

Theorem rmxycomplete

Proof