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\in {\mathbb{Z}}_{\ge 2}\to A+\sqrt{A^2-1}\in {ℝ}^{+}$$

Proof

Step	Hyp	Ref	Expression
1		rmspecfund	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \mathrm{PellFund}\left(A^2-1\right)=A+\sqrt{A^2-1}$$
2		rmspecnonsq	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A^2-1\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)$$
3		pellfundrp	$$⊢A^2-1\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \mathrm{PellFund}\left(A^2-1\right)\in {ℝ}^{+}$$
4	2 3	syl	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \mathrm{PellFund}\left(A^2-1\right)\in {ℝ}^{+}$$
5	1 4	eqeltrrd	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A+\sqrt{A^2-1}\in {ℝ}^{+}$$