# 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 ( 𝐴 ∈ ( ℤ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ( ℕ ∖ ◻NN ) )

### Proof

Step Hyp Ref Expression
1 eluzelz ( 𝐴 ∈ ( ℤ ‘ 2 ) → 𝐴 ∈ ℤ )
2 zsqcl ( 𝐴 ∈ ℤ → ( 𝐴 ↑ 2 ) ∈ ℤ )
3 1 2 syl ( 𝐴 ∈ ( ℤ ‘ 2 ) → ( 𝐴 ↑ 2 ) ∈ ℤ )
4 1zzd ( 𝐴 ∈ ( ℤ ‘ 2 ) → 1 ∈ ℤ )
5 3 4 zsubcld ( 𝐴 ∈ ( ℤ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℤ )
6 sq1 ( 1 ↑ 2 ) = 1
7 eluz2b2 ( 𝐴 ∈ ( ℤ ‘ 2 ) ↔ ( 𝐴 ∈ ℕ ∧ 1 < 𝐴 ) )
8 7 simprbi ( 𝐴 ∈ ( ℤ ‘ 2 ) → 1 < 𝐴 )
9 1red ( 𝐴 ∈ ( ℤ ‘ 2 ) → 1 ∈ ℝ )
10 eluzelre ( 𝐴 ∈ ( ℤ ‘ 2 ) → 𝐴 ∈ ℝ )
11 0le1 0 ≤ 1
12 11 a1i ( 𝐴 ∈ ( ℤ ‘ 2 ) → 0 ≤ 1 )
13 eluzge2nn0 ( 𝐴 ∈ ( ℤ ‘ 2 ) → 𝐴 ∈ ℕ0 )
14 13 nn0ge0d ( 𝐴 ∈ ( ℤ ‘ 2 ) → 0 ≤ 𝐴 )
15 9 10 12 14 lt2sqd ( 𝐴 ∈ ( ℤ ‘ 2 ) → ( 1 < 𝐴 ↔ ( 1 ↑ 2 ) < ( 𝐴 ↑ 2 ) ) )
16 8 15 mpbid ( 𝐴 ∈ ( ℤ ‘ 2 ) → ( 1 ↑ 2 ) < ( 𝐴 ↑ 2 ) )
17 6 16 eqbrtrrid ( 𝐴 ∈ ( ℤ ‘ 2 ) → 1 < ( 𝐴 ↑ 2 ) )
18 10 resqcld ( 𝐴 ∈ ( ℤ ‘ 2 ) → ( 𝐴 ↑ 2 ) ∈ ℝ )
19 9 18 posdifd ( 𝐴 ∈ ( ℤ ‘ 2 ) → ( 1 < ( 𝐴 ↑ 2 ) ↔ 0 < ( ( 𝐴 ↑ 2 ) − 1 ) ) )
20 17 19 mpbid ( 𝐴 ∈ ( ℤ ‘ 2 ) → 0 < ( ( 𝐴 ↑ 2 ) − 1 ) )
21 elnnz ( ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℕ ↔ ( ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℤ ∧ 0 < ( ( 𝐴 ↑ 2 ) − 1 ) ) )
22 5 20 21 sylanbrc ( 𝐴 ∈ ( ℤ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℕ )
23 rmspecsqrtnq ( 𝐴 ∈ ( ℤ ‘ 2 ) → ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ( ℂ ∖ ℚ ) )
24 23 eldifbd ( 𝐴 ∈ ( ℤ ‘ 2 ) → ¬ ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ℚ )
25 24 intnand ( 𝐴 ∈ ( ℤ ‘ 2 ) → ¬ ( ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℕ ∧ ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ℚ ) )
26 df-squarenn NN = { 𝑎 ∈ ℕ ∣ ( √ ‘ 𝑎 ) ∈ ℚ }
27 26 eleq2i ( ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ◻NN ↔ ( ( 𝐴 ↑ 2 ) − 1 ) ∈ { 𝑎 ∈ ℕ ∣ ( √ ‘ 𝑎 ) ∈ ℚ } )
28 fveq2 ( 𝑎 = ( ( 𝐴 ↑ 2 ) − 1 ) → ( √ ‘ 𝑎 ) = ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) )
29 28 eleq1d ( 𝑎 = ( ( 𝐴 ↑ 2 ) − 1 ) → ( ( √ ‘ 𝑎 ) ∈ ℚ ↔ ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ℚ ) )
30 29 elrab ( ( ( 𝐴 ↑ 2 ) − 1 ) ∈ { 𝑎 ∈ ℕ ∣ ( √ ‘ 𝑎 ) ∈ ℚ } ↔ ( ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℕ ∧ ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ℚ ) )
31 27 30 bitr2i ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℕ ∧ ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ℚ ) ↔ ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ◻NN )
32 25 31 sylnib ( 𝐴 ∈ ( ℤ ‘ 2 ) → ¬ ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ◻NN )
33 22 32 eldifd ( 𝐴 ∈ ( ℤ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ( ℕ ∖ ◻NN ) )