# Metamath Proof Explorer

## 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 {ℤ}_{\ge 2}\to {{A}}^{2}-1\in \left(ℕ\setminus {◻}_{ℕ}\right)$

### Proof

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