Metamath Proof Explorer

Theorem pell1qrval

Description: Value of the set of first-quadrant Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014)

		Ref	Expression
	Assertion	pell1qrval	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to Pell1QR (D) = \{y \in ℝ \| \exists z \in ℕ_{0} \exists w \in ℕ_{0} (y = z + \sqrt{D} w \land z^{2} - D w^{2} = 1)\}$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ a = D \to \sqrt{a} = \sqrt{D}$
2	1	oveq1d	$⊢ a = D \to \sqrt{a} w = \sqrt{D} w$
3	2	oveq2d	$⊢ a = D \to z + \sqrt{a} w = z + \sqrt{D} w$
4	3	eqeq2d	$⊢ a = D \to (y = z + \sqrt{a} w \leftrightarrow y = z + \sqrt{D} w)$
5		oveq1	$⊢ a = D \to a w^{2} = D w^{2}$
6	5	oveq2d	$⊢ a = D \to z^{2} - a w^{2} = z^{2} - D w^{2}$
7	6	eqeq1d	$⊢ a = D \to (z^{2} - a w^{2} = 1 \leftrightarrow z^{2} - D w^{2} = 1)$
8	4 7	anbi12d	$⊢ a = D \to ((y = z + \sqrt{a} w \land z^{2} - a w^{2} = 1) \leftrightarrow (y = z + \sqrt{D} w \land z^{2} - D w^{2} = 1))$
9	8	2rexbidv	$⊢ a = D \to (\exists z \in ℕ_{0} \exists w \in ℕ_{0} (y = z + \sqrt{a} w \land z^{2} - a w^{2} = 1) \leftrightarrow \exists z \in ℕ_{0} \exists w \in ℕ_{0} (y = z + \sqrt{D} w \land z^{2} - D w^{2} = 1))$
10	9	rabbidv	$⊢ a = D \to \{y \in ℝ \| \exists z \in ℕ_{0} \exists w \in ℕ_{0} (y = z + \sqrt{a} w \land z^{2} - a w^{2} = 1)\} = \{y \in ℝ \| \exists z \in ℕ_{0} \exists w \in ℕ_{0} (y = z + \sqrt{D} w \land z^{2} - D w^{2} = 1)\}$
11		df-pell1qr	$⊢ Pell1QR = (a \in (ℕ ∖ ◻_{ℕ}) ⟼ \{y \in ℝ \| \exists z \in ℕ_{0} \exists w \in ℕ_{0} (y = z + \sqrt{a} w \land z^{2} - a w^{2} = 1)\})$
12		reex	$⊢ ℝ \in V$
13	12	rabex	$⊢ \{y \in ℝ \| \exists z \in ℕ_{0} \exists w \in ℕ_{0} (y = z + \sqrt{D} w \land z^{2} - D w^{2} = 1)\} \in V$
14	10 11 13	fvmpt	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to Pell1QR (D) = \{y \in ℝ \| \exists z \in ℕ_{0} \exists w \in ℕ_{0} (y = z + \sqrt{D} w \land z^{2} - D w^{2} = 1)\}$