pell1234qrval

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

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

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

Metamath Proof Explorer