Metamath Proof Explorer

Theorem rmspecsqrtnq

Description: The discriminant used to define the X and Y sequences has an irrational square root. (Contributed by Stefan O'Rear, 21-Sep-2014) (Proof shortened by AV, 2-Aug-2021)

Ref Expression
Assertion rmspecsqrtnq ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ( ℂ ∖ ℚ ) )

Proof

Step Hyp Ref Expression
1 eluzelcn ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℂ )
2 1 sqcld ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
3 ax-1cn ⊢ 1 ∈ ℂ
4 subcl ⊢ ( ( ( 𝐴 ↑ 2 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℂ )
5 2 3 4 sylancl ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℂ )
6 5 sqrtcld ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ℂ )
7 eluz2nn ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℕ )
8 7 nnsqcld ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 ↑ 2 ) ∈ ℕ )
9 nnm1nn0 ⊢ ( ( 𝐴 ↑ 2 ) ∈ ℕ → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℕ0 )
10 8 9 syl ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℕ0 )
11 nnm1nn0 ⊢ ( 𝐴 ∈ ℕ → ( 𝐴 − 1 ) ∈ ℕ0 )
12 7 11 syl ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 − 1 ) ∈ ℕ0 )
13 binom2sub1 ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 − 1 ) ↑ 2 ) = ( ( ( 𝐴 ↑ 2 ) − ( 2 · 𝐴 ) ) + 1 ) )
14 1 13 syl ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 − 1 ) ↑ 2 ) = ( ( ( 𝐴 ↑ 2 ) − ( 2 · 𝐴 ) ) + 1 ) )
15 2cnd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ℂ )
16 15 1 mulcld ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · 𝐴 ) ∈ ℂ )
17 3 a1i ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 1 ∈ ℂ )
18 2 16 17 subsubd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − ( ( 2 · 𝐴 ) − 1 ) ) = ( ( ( 𝐴 ↑ 2 ) − ( 2 · 𝐴 ) ) + 1 ) )
19 14 18 eqtr4d ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 − 1 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) − ( ( 2 · 𝐴 ) − 1 ) ) )
20 1red ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 1 ∈ ℝ )
21 2re ⊢ 2 ∈ ℝ
22 21 a1i ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ℝ )
23 eluzelre ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℝ )
24 22 23 remulcld ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · 𝐴 ) ∈ ℝ )
25 24 20 resubcld ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 · 𝐴 ) − 1 ) ∈ ℝ )
26 8 nnred ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 ↑ 2 ) ∈ ℝ )
27 eluz2gt1 ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝐴 )
28 20 20 23 27 27 lt2addmuld ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 1 + 1 ) < ( 2 · 𝐴 ) )
29 remulcl ⊢ ( ( 2 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 2 · 𝐴 ) ∈ ℝ )
30 21 23 29 sylancr ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · 𝐴 ) ∈ ℝ )
31 20 20 30 ltaddsubd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 1 + 1 ) < ( 2 · 𝐴 ) ↔ 1 < ( ( 2 · 𝐴 ) − 1 ) ) )
32 28 31 mpbid ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 1 < ( ( 2 · 𝐴 ) − 1 ) )
33 20 25 26 32 ltsub2dd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − ( ( 2 · 𝐴 ) − 1 ) ) < ( ( 𝐴 ↑ 2 ) − 1 ) )
34 19 33 eqbrtrd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 − 1 ) ↑ 2 ) < ( ( 𝐴 ↑ 2 ) − 1 ) )
35 26 ltm1d ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) < ( 𝐴 ↑ 2 ) )
36 npcan ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐴 − 1 ) + 1 ) = 𝐴 )
37 1 3 36 sylancl ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 − 1 ) + 1 ) = 𝐴 )
38 37 oveq1d ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 𝐴 − 1 ) + 1 ) ↑ 2 ) = ( 𝐴 ↑ 2 ) )
39 35 38 breqtrrd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) < ( ( ( 𝐴 − 1 ) + 1 ) ↑ 2 ) )
40 nonsq ⊢ ( ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℕ0 ∧ ( 𝐴 − 1 ) ∈ ℕ0 ) ∧ ( ( ( 𝐴 − 1 ) ↑ 2 ) < ( ( 𝐴 ↑ 2 ) − 1 ) ∧ ( ( 𝐴 ↑ 2 ) − 1 ) < ( ( ( 𝐴 − 1 ) + 1 ) ↑ 2 ) ) ) → ¬ ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ℚ )
41 10 12 34 39 40 syl22anc ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ¬ ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ℚ )
42 6 41 eldifd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ( ℂ ∖ ℚ ) )