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 ) )