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 e. ( ZZ>= ` 2 ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) )

Proof

Step Hyp Ref Expression
1 eluzelcn 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. CC )
2 1 sqcld 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A ^ 2 ) e. CC )
3 ax-1cn 
 |-  1 e. CC
4 subcl 
 |-  ( ( ( A ^ 2 ) e. CC /\ 1 e. CC ) -> ( ( A ^ 2 ) - 1 ) e. CC )
5 2 3 4 sylancl 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. CC )
6 5 sqrtcld 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. CC )
7 eluz2nn 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. NN )
8 7 nnsqcld 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A ^ 2 ) e. NN )
9 nnm1nn0 
 |-  ( ( A ^ 2 ) e. NN -> ( ( A ^ 2 ) - 1 ) e. NN0 )
10 8 9 syl 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. NN0 )
11 nnm1nn0 
 |-  ( A e. NN -> ( A - 1 ) e. NN0 )
12 7 11 syl 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A - 1 ) e. NN0 )
13 binom2sub1 
 |-  ( A e. CC -> ( ( A - 1 ) ^ 2 ) = ( ( ( A ^ 2 ) - ( 2 x. A ) ) + 1 ) )
14 1 13 syl 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A - 1 ) ^ 2 ) = ( ( ( A ^ 2 ) - ( 2 x. A ) ) + 1 ) )
15 2cnd 
 |-  ( A e. ( ZZ>= ` 2 ) -> 2 e. CC )
16 15 1 mulcld 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( 2 x. A ) e. CC )
17 3 a1i 
 |-  ( A e. ( ZZ>= ` 2 ) -> 1 e. CC )
18 2 16 17 subsubd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - ( ( 2 x. A ) - 1 ) ) = ( ( ( A ^ 2 ) - ( 2 x. A ) ) + 1 ) )
19 14 18 eqtr4d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A - 1 ) ^ 2 ) = ( ( A ^ 2 ) - ( ( 2 x. A ) - 1 ) ) )
20 1red 
 |-  ( A e. ( ZZ>= ` 2 ) -> 1 e. RR )
21 2re 
 |-  2 e. RR
22 21 a1i 
 |-  ( A e. ( ZZ>= ` 2 ) -> 2 e. RR )
23 eluzelre 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. RR )
24 22 23 remulcld 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( 2 x. A ) e. RR )
25 24 20 resubcld 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( 2 x. A ) - 1 ) e. RR )
26 8 nnred 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A ^ 2 ) e. RR )
27 eluz2gt1 
 |-  ( A e. ( ZZ>= ` 2 ) -> 1 < A )
28 20 20 23 27 27 lt2addmuld 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( 1 + 1 ) < ( 2 x. A ) )
29 remulcl 
 |-  ( ( 2 e. RR /\ A e. RR ) -> ( 2 x. A ) e. RR )
30 21 23 29 sylancr 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( 2 x. A ) e. RR )
31 20 20 30 ltaddsubd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( 1 + 1 ) < ( 2 x. A ) <-> 1 < ( ( 2 x. A ) - 1 ) ) )
32 28 31 mpbid 
 |-  ( A e. ( ZZ>= ` 2 ) -> 1 < ( ( 2 x. A ) - 1 ) )
33 20 25 26 32 ltsub2dd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - ( ( 2 x. A ) - 1 ) ) < ( ( A ^ 2 ) - 1 ) )
34 19 33 eqbrtrd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A - 1 ) ^ 2 ) < ( ( A ^ 2 ) - 1 ) )
35 26 ltm1d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) < ( A ^ 2 ) )
36 npcan 
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( ( A - 1 ) + 1 ) = A )
37 1 3 36 sylancl 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A - 1 ) + 1 ) = A )
38 37 oveq1d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( ( A - 1 ) + 1 ) ^ 2 ) = ( A ^ 2 ) )
39 35 38 breqtrrd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) < ( ( ( A - 1 ) + 1 ) ^ 2 ) )
40 nonsq 
 |-  ( ( ( ( ( A ^ 2 ) - 1 ) e. NN0 /\ ( A - 1 ) e. NN0 ) /\ ( ( ( A - 1 ) ^ 2 ) < ( ( A ^ 2 ) - 1 ) /\ ( ( A ^ 2 ) - 1 ) < ( ( ( A - 1 ) + 1 ) ^ 2 ) ) ) -> -. ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. QQ )
41 10 12 34 39 40 syl22anc 
 |-  ( A e. ( ZZ>= ` 2 ) -> -. ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. QQ )
42 6 41 eldifd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) )