Theorem pellfundrp

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

	Ref	Expression
Assertion	pellfundrp	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( PellFund ‘ 𝐷 ) ∈ ℝ+ )

Proof

Step	Hyp	Ref	Expression
1		pellfundre	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( PellFund ‘ 𝐷 ) ∈ ℝ )
2		0red	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 0 ∈ ℝ )
3		1red	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 1 ∈ ℝ )
4		0lt1	⊢ 0 < 1
5	4	a1i	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 0 < 1 )
6		pellfundgt1	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 1 < ( PellFund ‘ 𝐷 ) )
7	2 3 1 5 6	lttrd	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 0 < ( PellFund ‘ 𝐷 ) )
8	1 7	elrpd	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( PellFund ‘ 𝐷 ) ∈ ℝ+ )