Metamath Proof Explorer

Theorem pell14qrrp

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

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

Step	Hyp	Ref	Expression
1		pell14qrre	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to A \in ℝ$
2		pell14qrgt0	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to 0 < A$
3	1 2	elrpd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to A \in ℝ^{+}$