elpell14qr

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

		Ref	Expression
	Assertion	elpell14qr	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (A \in Pell14QR (D) \leftrightarrow (A \in ℝ \land \exists z \in ℕ_{0} \exists w \in ℤ (A = z + \sqrt{D} w \land z^{2} - D w^{2} = 1)))$

Step	Hyp	Ref	Expression
1		pell14qrval	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to Pell14QR (D) = \{a \in ℝ \| \exists z \in ℕ_{0} \exists w \in ℤ (a = z + \sqrt{D} w \land z^{2} - D w^{2} = 1)\}$
2	1	eleq2d	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (A \in Pell14QR (D) \leftrightarrow A \in \{a \in ℝ \| \exists z \in ℕ_{0} \exists w \in ℤ (a = z + \sqrt{D} w \land z^{2} - D w^{2} = 1)\})$
3		eqeq1	$⊢ a = A \to (a = z + \sqrt{D} w \leftrightarrow A = z + \sqrt{D} w)$
4	3	anbi1d	$⊢ a = A \to ((a = z + \sqrt{D} w \land z^{2} - D w^{2} = 1) \leftrightarrow (A = z + \sqrt{D} w \land z^{2} - D w^{2} = 1))$
5	4	2rexbidv	$⊢ a = A \to (\exists z \in ℕ_{0} \exists w \in ℤ (a = z + \sqrt{D} w \land z^{2} - D w^{2} = 1) \leftrightarrow \exists z \in ℕ_{0} \exists w \in ℤ (A = z + \sqrt{D} w \land z^{2} - D w^{2} = 1))$
6	5	elrab	$⊢ A \in \{a \in ℝ \| \exists z \in ℕ_{0} \exists w \in ℤ (a = z + \sqrt{D} w \land z^{2} - D w^{2} = 1)\} \leftrightarrow (A \in ℝ \land \exists z \in ℕ_{0} \exists w \in ℤ (A = z + \sqrt{D} w \land z^{2} - D w^{2} = 1))$
7	2 6	bitrdi	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (A \in Pell14QR (D) \leftrightarrow (A \in ℝ \land \exists z \in ℕ_{0} \exists w \in ℤ (A = z + \sqrt{D} w \land z^{2} - D w^{2} = 1)))$

Metamath Proof Explorer