Theorem rmspecnonsq

Description: The discriminant used to define the X and Y sequences is a nonsquare positive integer and thus a valid Pell equation discriminant. (Contributed by Stefan O'Rear, 21-Sep-2014)

	Ref	Expression
Assertion	rmspecnonsq	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A^2-1\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		eluzelz	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\in \mathbb{Z}$$
2		zsqcl	$$⊢A\in \mathbb{Z}\to A^2\in \mathbb{Z}$$
3	1 2	syl	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A^2\in \mathbb{Z}$$
4		1zzd	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 1\in \mathbb{Z}$$
5	3 4	zsubcld	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A^2-1\in \mathbb{Z}$$
6		sq1	$$⊢1^2=1$$
7		eluz2b2	$$⊢A\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(A\in \mathbb{N}\wedge 1<A\right)$$
8	7	simprbi	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 1<A$$
9		1red	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 1\in ℝ$$
10		eluzelre	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\in ℝ$$
11		0le1	$$⊢0\le 1$$
12	11	a1i	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 0\le 1$$
13		eluzge2nn0	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\in {\mathbb{N}}_0$$
14	13	nn0ge0d	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 0\le A$$
15	9 10 12 14	lt2sqd	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \left(1<A\leftrightarrow 1^2<A^2\right)$$
16	8 15	mpbid	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 1^2<A^2$$
17	6 16	eqbrtrrid	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 1<A^2$$
18	10	resqcld	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A^2\in ℝ$$
19	9 18	posdifd	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \left(1<A^2\leftrightarrow 0<A^2-1\right)$$
20	17 19	mpbid	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 0<A^2-1$$
21		elnnz	$$⊢A^2-1\in \mathbb{N}\leftrightarrow \left(A^2-1\in \mathbb{Z}\wedge 0<A^2-1\right)$$
22	5 20 21	sylanbrc	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A^2-1\in \mathbb{N}$$
23		rmspecsqrtnq	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \sqrt{A^2-1}\in \left(ℂ\setminus \mathbb{Q}\right)$$
24	23	eldifbd	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \neg \sqrt{A^2-1}\in \mathbb{Q}$$
25	24	intnand	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \neg \left(A^2-1\in \mathbb{N}\wedge \sqrt{A^2-1}\in \mathbb{Q}\right)$$
26		df-squarenn	$$⊢{◻}_{\mathbb{N}}=\left\{a\in \mathbb{N}|\sqrt{a}\in \mathbb{Q}\right\}$$
27	26	eleq2i	$$⊢A^2-1\in {◻}_{\mathbb{N}}\leftrightarrow A^2-1\in \left\{a\in \mathbb{N}|\sqrt{a}\in \mathbb{Q}\right\}$$
28		fveq2	$$⊢a=A^2-1\to \sqrt{a}=\sqrt{A^2-1}$$
29	28	eleq1d	$$⊢a=A^2-1\to \left(\sqrt{a}\in \mathbb{Q}\leftrightarrow \sqrt{A^2-1}\in \mathbb{Q}\right)$$
30	29	elrab	$$⊢A^2-1\in \left\{a\in \mathbb{N}|\sqrt{a}\in \mathbb{Q}\right\}\leftrightarrow \left(A^2-1\in \mathbb{N}\wedge \sqrt{A^2-1}\in \mathbb{Q}\right)$$
31	27 30	bitr2i	$$⊢\left(A^2-1\in \mathbb{N}\wedge \sqrt{A^2-1}\in \mathbb{Q}\right)\leftrightarrow A^2-1\in {◻}_{\mathbb{N}}$$
32	25 31	sylnib	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \neg A^2-1\in {◻}_{\mathbb{N}}$$
33	22 32	eldifd	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A^2-1\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)$$