Theorem rmspecpos

Description: The discriminant used to define the X and Y sequences is a positive real. (Contributed by Stefan O'Rear, 22-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		eluzelre	|- ( A e. ( ZZ>= ` 2 ) -> A e. RR )
2	1	resqcld	|- ( A e. ( ZZ>= ` 2 ) -> ( A ^ 2 ) e. RR )
3		1red	|- ( A e. ( ZZ>= ` 2 ) -> 1 e. RR )
4	2 3	resubcld	|- ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. RR )
5		sq1	|- ( 1 ^ 2 ) = 1
6		eluz2b1	|- ( A e. ( ZZ>= ` 2 ) <-> ( A e. ZZ /\ 1 < A ) )
7	6	simprbi	|- ( A e. ( ZZ>= ` 2 ) -> 1 < A )
8		0le1	|- 0 <_ 1
9	8	a1i	|- ( A e. ( ZZ>= ` 2 ) -> 0 <_ 1 )
10		eluzge2nn0	|- ( A e. ( ZZ>= ` 2 ) -> A e. NN0 )
11	10	nn0ge0d	|- ( A e. ( ZZ>= ` 2 ) -> 0 <_ A )
12	3 1 9 11	lt2sqd	|- ( A e. ( ZZ>= ` 2 ) -> ( 1 < A <-> ( 1 ^ 2 ) < ( A ^ 2 ) ) )
13	7 12	mpbid	|- ( A e. ( ZZ>= ` 2 ) -> ( 1 ^ 2 ) < ( A ^ 2 ) )
14	5 13	eqbrtrrid	|- ( A e. ( ZZ>= ` 2 ) -> 1 < ( A ^ 2 ) )
15	3 2	posdifd	|- ( A e. ( ZZ>= ` 2 ) -> ( 1 < ( A ^ 2 ) <-> 0 < ( ( A ^ 2 ) - 1 ) ) )
16	14 15	mpbid	|- ( A e. ( ZZ>= ` 2 ) -> 0 < ( ( A ^ 2 ) - 1 ) )
17	4 16	elrpd	|- ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. RR+ )