Metamath Proof Explorer

Theorem pell1234qrre

Description: General Pell solutions are (coded as) real numbers. (Contributed by Stefan O'Rear, 17-Sep-2014)

		Ref	Expression
	Assertion	pell1234qrre	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \to A \in ℝ$

Step	Hyp	Ref	Expression
1		elpell1234qr	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (A \in Pell1234QR (D) \leftrightarrow (A \in ℝ \land \exists a \in ℤ \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)))$
2	1	simprbda	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \to A \in ℝ$