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

Proof

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