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

### Proof

Step Hyp Ref Expression
1 eluzelre ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}\in ℝ$
2 1 resqcld ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}\in ℝ$
3 1red ${⊢}{A}\in {ℤ}_{\ge 2}\to 1\in ℝ$
4 2 3 resubcld ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}-1\in ℝ$
5 sq1 ${⊢}{1}^{2}=1$
6 eluz2b1 ${⊢}{A}\in {ℤ}_{\ge 2}↔\left({A}\in ℤ\wedge 1<{A}\right)$
7 6 simprbi ${⊢}{A}\in {ℤ}_{\ge 2}\to 1<{A}$
8 0le1 ${⊢}0\le 1$
9 8 a1i ${⊢}{A}\in {ℤ}_{\ge 2}\to 0\le 1$
10 eluzge2nn0 ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}\in {ℕ}_{0}$
11 10 nn0ge0d ${⊢}{A}\in {ℤ}_{\ge 2}\to 0\le {A}$
12 3 1 9 11 lt2sqd ${⊢}{A}\in {ℤ}_{\ge 2}\to \left(1<{A}↔{1}^{2}<{{A}}^{2}\right)$
13 7 12 mpbid ${⊢}{A}\in {ℤ}_{\ge 2}\to {1}^{2}<{{A}}^{2}$
14 5 13 eqbrtrrid ${⊢}{A}\in {ℤ}_{\ge 2}\to 1<{{A}}^{2}$
15 3 2 posdifd ${⊢}{A}\in {ℤ}_{\ge 2}\to \left(1<{{A}}^{2}↔0<{{A}}^{2}-1\right)$
16 14 15 mpbid ${⊢}{A}\in {ℤ}_{\ge 2}\to 0<{{A}}^{2}-1$
17 4 16 elrpd ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}-1\in {ℝ}^{+}$