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

### Proof

Step Hyp Ref Expression
1 eluzelcn ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}\in ℂ$
2 1 sqcld ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}\in ℂ$
3 ax-1cn ${⊢}1\in ℂ$
4 subcl ${⊢}\left({{A}}^{2}\in ℂ\wedge 1\in ℂ\right)\to {{A}}^{2}-1\in ℂ$
5 2 3 4 sylancl ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}-1\in ℂ$
6 5 sqrtcld ${⊢}{A}\in {ℤ}_{\ge 2}\to \sqrt{{{A}}^{2}-1}\in ℂ$
7 eluz2nn ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}\in ℕ$
8 7 nnsqcld ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}\in ℕ$
9 nnm1nn0 ${⊢}{{A}}^{2}\in ℕ\to {{A}}^{2}-1\in {ℕ}_{0}$
10 8 9 syl ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}-1\in {ℕ}_{0}$
11 nnm1nn0 ${⊢}{A}\in ℕ\to {A}-1\in {ℕ}_{0}$
12 7 11 syl ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}-1\in {ℕ}_{0}$
13 binom2sub1 ${⊢}{A}\in ℂ\to {\left({A}-1\right)}^{2}={{A}}^{2}-2{A}+1$
14 1 13 syl ${⊢}{A}\in {ℤ}_{\ge 2}\to {\left({A}-1\right)}^{2}={{A}}^{2}-2{A}+1$
15 2cnd ${⊢}{A}\in {ℤ}_{\ge 2}\to 2\in ℂ$
16 15 1 mulcld ${⊢}{A}\in {ℤ}_{\ge 2}\to 2{A}\in ℂ$
17 3 a1i ${⊢}{A}\in {ℤ}_{\ge 2}\to 1\in ℂ$
18 2 16 17 subsubd ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}-\left(2{A}-1\right)={{A}}^{2}-2{A}+1$
19 14 18 eqtr4d ${⊢}{A}\in {ℤ}_{\ge 2}\to {\left({A}-1\right)}^{2}={{A}}^{2}-\left(2{A}-1\right)$
20 1red ${⊢}{A}\in {ℤ}_{\ge 2}\to 1\in ℝ$
21 2re ${⊢}2\in ℝ$
22 21 a1i ${⊢}{A}\in {ℤ}_{\ge 2}\to 2\in ℝ$
23 eluzelre ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}\in ℝ$
24 22 23 remulcld ${⊢}{A}\in {ℤ}_{\ge 2}\to 2{A}\in ℝ$
25 24 20 resubcld ${⊢}{A}\in {ℤ}_{\ge 2}\to 2{A}-1\in ℝ$
26 8 nnred ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}\in ℝ$
27 eluz2gt1 ${⊢}{A}\in {ℤ}_{\ge 2}\to 1<{A}$
28 20 20 23 27 27 lt2addmuld ${⊢}{A}\in {ℤ}_{\ge 2}\to 1+1<2{A}$
29 remulcl ${⊢}\left(2\in ℝ\wedge {A}\in ℝ\right)\to 2{A}\in ℝ$
30 21 23 29 sylancr ${⊢}{A}\in {ℤ}_{\ge 2}\to 2{A}\in ℝ$
31 20 20 30 ltaddsubd ${⊢}{A}\in {ℤ}_{\ge 2}\to \left(1+1<2{A}↔1<2{A}-1\right)$
32 28 31 mpbid ${⊢}{A}\in {ℤ}_{\ge 2}\to 1<2{A}-1$
33 20 25 26 32 ltsub2dd ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}-\left(2{A}-1\right)<{{A}}^{2}-1$
34 19 33 eqbrtrd ${⊢}{A}\in {ℤ}_{\ge 2}\to {\left({A}-1\right)}^{2}<{{A}}^{2}-1$
35 26 ltm1d ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}-1<{{A}}^{2}$
36 npcan ${⊢}\left({A}\in ℂ\wedge 1\in ℂ\right)\to {A}-1+1={A}$
37 1 3 36 sylancl ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}-1+1={A}$
38 37 oveq1d ${⊢}{A}\in {ℤ}_{\ge 2}\to {\left({A}-1+1\right)}^{2}={{A}}^{2}$
39 35 38 breqtrrd ${⊢}{A}\in {ℤ}_{\ge 2}\to {{A}}^{2}-1<{\left({A}-1+1\right)}^{2}$
40 nonsq ${⊢}\left(\left({{A}}^{2}-1\in {ℕ}_{0}\wedge {A}-1\in {ℕ}_{0}\right)\wedge \left({\left({A}-1\right)}^{2}<{{A}}^{2}-1\wedge {{A}}^{2}-1<{\left({A}-1+1\right)}^{2}\right)\right)\to ¬\sqrt{{{A}}^{2}-1}\in ℚ$
41 10 12 34 39 40 syl22anc ${⊢}{A}\in {ℤ}_{\ge 2}\to ¬\sqrt{{{A}}^{2}-1}\in ℚ$
42 6 41 eldifd ${⊢}{A}\in {ℤ}_{\ge 2}\to \sqrt{{{A}}^{2}-1}\in \left(ℂ\setminus ℚ\right)$