Metamath Proof Explorer

Theorem pell14qrre

Description: A positive Pell solution is a real number. (Contributed by Stefan O'Rear, 18-Sep-2014)

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

Step	Hyp	Ref	Expression
1		pell14qrss1234	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to Pell14QR (D) \subseteq Pell1234QR (D)$
2	1	sselda	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to A \in Pell1234QR (D)$
3		pell1234qrre	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \to A \in ℝ$
4	2 3	syldan	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to A \in ℝ$