Metamath Proof Explorer

Theorem sqrtnzqaa

Description: Square root of a nonzero rational is algebraic. (Contributed by Ender Ting, 22-Jul-2026)

Ref Expression
Assertion sqrtnzqaa 
|- ( ( A e. QQ /\ A =/= 0 ) -> ( sqrt ` A ) e. AA )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> A e. QQ )
2 qcn 
 |-  ( A e. QQ -> A e. CC )
3 sqrtcl 
 |-  ( A e. CC -> ( sqrt ` A ) e. CC )
4 1 2 3 3syl 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( sqrt ` A ) e. CC )
5 fveq1 
 |-  ( x = ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) -> ( x ` ( sqrt ` A ) ) = ( ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) ` ( sqrt ` A ) ) )
6 5 eqeq1d 
 |-  ( x = ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) -> ( ( x ` ( sqrt ` A ) ) = 0 <-> ( ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) ` ( sqrt ` A ) ) = 0 ) )
7 qsscn 
 |-  QQ C_ CC
8 1z 
 |-  1 e. ZZ
9 zq 
 |-  ( 1 e. ZZ -> 1 e. QQ )
10 8 9 ax-mp 
 |-  1 e. QQ
11 2nn0 
 |-  2 e. NN0
12 plypow 
 |-  ( ( QQ C_ CC /\ 1 e. QQ /\ 2 e. NN0 ) -> ( t e. CC |-> ( t ^ 2 ) ) e. ( Poly ` QQ ) )
13 7 10 11 12 mp3an 
 |-  ( t e. CC |-> ( t ^ 2 ) ) e. ( Poly ` QQ )
14 13 a1i 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( t e. CC |-> ( t ^ 2 ) ) e. ( Poly ` QQ ) )
15 7 a1i 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> QQ C_ CC )
16 plyconst 
 |-  ( ( QQ C_ CC /\ A e. QQ ) -> ( CC X. { A } ) e. ( Poly ` QQ ) )
17 15 1 16 syl2anc 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( CC X. { A } ) e. ( Poly ` QQ ) )
18 qaddcl 
 |-  ( ( x e. QQ /\ p e. QQ ) -> ( x + p ) e. QQ )
19 18 adantl 
 |-  ( ( ( A e. QQ /\ A =/= 0 ) /\ ( x e. QQ /\ p e. QQ ) ) -> ( x + p ) e. QQ )
20 qmulcl 
 |-  ( ( x e. QQ /\ p e. QQ ) -> ( x x. p ) e. QQ )
21 20 adantl 
 |-  ( ( ( A e. QQ /\ A =/= 0 ) /\ ( x e. QQ /\ p e. QQ ) ) -> ( x x. p ) e. QQ )
22 neg1z 
 |-  -u 1 e. ZZ
23 zq 
 |-  ( -u 1 e. ZZ -> -u 1 e. QQ )
24 22 23 ax-mp 
 |-  -u 1 e. QQ
25 24 a1i 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> -u 1 e. QQ )
26 14 17 19 21 25 plysub 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) e. ( Poly ` QQ ) )
27 0cnd 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> 0 e. CC )
28 fnconstg 
 |-  ( A e. QQ -> ( CC X. { A } ) Fn CC )
29 28 adantr 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( CC X. { A } ) Fn CC )
30 ovex 
 |-  ( t ^ 2 ) e. _V
31 30 rgenw 
 |-  A. t e. CC ( t ^ 2 ) e. _V
32 nfcv 
 |-  F/_ t CC
33 32 mptfnf 
 |-  ( A. t e. CC ( t ^ 2 ) e. _V <-> ( t e. CC |-> ( t ^ 2 ) ) Fn CC )
34 31 33 mpbi 
 |-  ( t e. CC |-> ( t ^ 2 ) ) Fn CC
35 29 34 jctil 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( ( t e. CC |-> ( t ^ 2 ) ) Fn CC /\ ( CC X. { A } ) Fn CC ) )
36 cnex 
 |-  CC e. _V
37 0cn 
 |-  0 e. CC
38 36 37 pm3.2i 
 |-  ( CC e. _V /\ 0 e. CC )
39 38 a1i 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( CC e. _V /\ 0 e. CC ) )
40 fnfvof 
 |-  ( ( ( ( t e. CC |-> ( t ^ 2 ) ) Fn CC /\ ( CC X. { A } ) Fn CC ) /\ ( CC e. _V /\ 0 e. CC ) ) -> ( ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) ` 0 ) = ( ( ( t e. CC |-> ( t ^ 2 ) ) ` 0 ) - ( ( CC X. { A } ) ` 0 ) ) )
41 35 39 40 syl2anc 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) ` 0 ) = ( ( ( t e. CC |-> ( t ^ 2 ) ) ` 0 ) - ( ( CC X. { A } ) ` 0 ) ) )
42 oveq1 
 |-  ( t = 0 -> ( t ^ 2 ) = ( 0 ^ 2 ) )
43 eqid 
 |-  ( t e. CC |-> ( t ^ 2 ) ) = ( t e. CC |-> ( t ^ 2 ) )
44 ovex 
 |-  ( 0 ^ 2 ) e. _V
45 42 43 44 fvmpt 
 |-  ( 0 e. CC -> ( ( t e. CC |-> ( t ^ 2 ) ) ` 0 ) = ( 0 ^ 2 ) )
46 37 45 ax-mp 
 |-  ( ( t e. CC |-> ( t ^ 2 ) ) ` 0 ) = ( 0 ^ 2 )
47 sq0 
 |-  ( 0 ^ 2 ) = 0
48 46 47 eqtri 
 |-  ( ( t e. CC |-> ( t ^ 2 ) ) ` 0 ) = 0
49 48 a1i 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( ( t e. CC |-> ( t ^ 2 ) ) ` 0 ) = 0 )
50 fvconst2g 
 |-  ( ( A e. QQ /\ 0 e. CC ) -> ( ( CC X. { A } ) ` 0 ) = A )
51 1 27 50 syl2anc 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( ( CC X. { A } ) ` 0 ) = A )
52 49 51 oveq12d 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( ( ( t e. CC |-> ( t ^ 2 ) ) ` 0 ) - ( ( CC X. { A } ) ` 0 ) ) = ( 0 - A ) )
53 41 52 eqtrd 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) ` 0 ) = ( 0 - A ) )
54 2 adantr 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> A e. CC )
55 necom 
 |-  ( A =/= 0 <-> 0 =/= A )
56 55 biimpi 
 |-  ( A =/= 0 -> 0 =/= A )
57 56 adantl 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> 0 =/= A )
58 27 54 57 subne0d 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( 0 - A ) =/= 0 )
59 53 58 eqnetrd 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) ` 0 ) =/= 0 )
60 ne0p 
 |-  ( ( 0 e. CC /\ ( ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) ` 0 ) =/= 0 ) -> ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) =/= 0p )
61 27 59 60 syl2anc 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) =/= 0p )
62 26 61 eldifsnd 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) e. ( ( Poly ` QQ ) \ { 0p } ) )
63 4 36 jctil 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( CC e. _V /\ ( sqrt ` A ) e. CC ) )
64 fnfvof 
 |-  ( ( ( ( t e. CC |-> ( t ^ 2 ) ) Fn CC /\ ( CC X. { A } ) Fn CC ) /\ ( CC e. _V /\ ( sqrt ` A ) e. CC ) ) -> ( ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) ` ( sqrt ` A ) ) = ( ( ( t e. CC |-> ( t ^ 2 ) ) ` ( sqrt ` A ) ) - ( ( CC X. { A } ) ` ( sqrt ` A ) ) ) )
65 35 63 64 syl2anc 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) ` ( sqrt ` A ) ) = ( ( ( t e. CC |-> ( t ^ 2 ) ) ` ( sqrt ` A ) ) - ( ( CC X. { A } ) ` ( sqrt ` A ) ) ) )
66 oveq1 
 |-  ( t = ( sqrt ` A ) -> ( t ^ 2 ) = ( ( sqrt ` A ) ^ 2 ) )
67 ovex 
 |-  ( ( sqrt ` A ) ^ 2 ) e. _V
68 66 43 67 fvmpt 
 |-  ( ( sqrt ` A ) e. CC -> ( ( t e. CC |-> ( t ^ 2 ) ) ` ( sqrt ` A ) ) = ( ( sqrt ` A ) ^ 2 ) )
69 54 3 68 3syl 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( ( t e. CC |-> ( t ^ 2 ) ) ` ( sqrt ` A ) ) = ( ( sqrt ` A ) ^ 2 ) )
70 sqrtth 
 |-  ( A e. CC -> ( ( sqrt ` A ) ^ 2 ) = A )
71 1 2 70 3syl 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( ( sqrt ` A ) ^ 2 ) = A )
72 69 71 eqtrd 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( ( t e. CC |-> ( t ^ 2 ) ) ` ( sqrt ` A ) ) = A )
73 fvconst2g 
 |-  ( ( A e. QQ /\ ( sqrt ` A ) e. CC ) -> ( ( CC X. { A } ) ` ( sqrt ` A ) ) = A )
74 1 4 73 syl2anc 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( ( CC X. { A } ) ` ( sqrt ` A ) ) = A )
75 72 74 oveq12d 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( ( ( t e. CC |-> ( t ^ 2 ) ) ` ( sqrt ` A ) ) - ( ( CC X. { A } ) ` ( sqrt ` A ) ) ) = ( A - A ) )
76 65 75 eqtrd 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) ` ( sqrt ` A ) ) = ( A - A ) )
77 subid 
 |-  ( A e. CC -> ( A - A ) = 0 )
78 1 2 77 3syl 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( A - A ) = 0 )
79 76 78 eqtrd 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) ` ( sqrt ` A ) ) = 0 )
80 6 62 79 rspcedvdw 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> E. x e. ( ( Poly ` QQ ) \ { 0p } ) ( x ` ( sqrt ` A ) ) = 0 )
81 elqaa 
 |-  ( ( sqrt ` A ) e. AA <-> ( ( sqrt ` A ) e. CC /\ E. x e. ( ( Poly ` QQ ) \ { 0p } ) ( x ` ( sqrt ` A ) ) = 0 ) )
82 4 80 81 sylanbrc 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( sqrt ` A ) e. AA )