Theorem pell14qrrp

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

	Ref	Expression
Assertion	pell14qrrp	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝐴 ∈ ℝ+ )

Proof

Step	Hyp	Ref	Expression
1		pell14qrre	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝐴 ∈ ℝ )
2		pell14qrgt0	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → 0 < 𝐴 )
3	1 2	elrpd	⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝐴 ∈ ℝ+ )