Theorem rmbaserp

Description: The base of exponentiation for the X and Y sequences is a positive real. (Contributed by Stefan O'Rear, 22-Sep-2014)

	Ref	Expression
Assertion	rmbaserp	|- ( A e. ( ZZ>= ` 2 ) -> ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) e. RR+ )

Proof

Step	Hyp	Ref	Expression
1		rmspecfund	|- ( A e. ( ZZ>= ` 2 ) -> ( PellFund ` ( ( A ^ 2 ) - 1 ) ) = ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) )
2		rmspecnonsq	|- ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. ( NN \ []NN ) )
3		pellfundrp	|- ( ( ( A ^ 2 ) - 1 ) e. ( NN \ []NN ) -> ( PellFund ` ( ( A ^ 2 ) - 1 ) ) e. RR+ )
4	2 3	syl	|- ( A e. ( ZZ>= ` 2 ) -> ( PellFund ` ( ( A ^ 2 ) - 1 ) ) e. RR+ )
5	1 4	eqeltrrd	|- ( A e. ( ZZ>= ` 2 ) -> ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) e. RR+ )