# Metamath Proof Explorer

## 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+ )`