Metamath Proof Explorer

Theorem sqrtnnaa

Description: Square root of a natural number is algebraic. (Contributed by Ender Ting, 21-Jul-2026)

Ref Expression
Assertion sqrtnnaa 
|- ( A e. NN -> ( sqrt ` A ) e. AA )

Proof

Step Hyp Ref Expression
1 nncn 
 |-  ( A e. NN -> A e. CC )
2 sqrtcl 
 |-  ( A e. CC -> ( sqrt ` A ) e. CC )
3 1 2 syl 
 |-  ( A e. NN -> ( sqrt ` A ) e. CC )
4 zsscn 
 |-  ZZ C_ CC
5 1z 
 |-  1 e. ZZ
6 2nn0 
 |-  2 e. NN0
7 plypow 
 |-  ( ( ZZ C_ CC /\ 1 e. ZZ /\ 2 e. NN0 ) -> ( t e. CC |-> ( t ^ 2 ) ) e. ( Poly ` ZZ ) )
8 4 5 6 7 mp3an 
 |-  ( t e. CC |-> ( t ^ 2 ) ) e. ( Poly ` ZZ )
9 8 a1i 
 |-  ( A e. NN -> ( t e. CC |-> ( t ^ 2 ) ) e. ( Poly ` ZZ ) )
10 4 a1i 
 |-  ( A e. NN -> ZZ C_ CC )
11 nnz 
 |-  ( A e. NN -> A e. ZZ )
12 plyconst 
 |-  ( ( ZZ C_ CC /\ A e. ZZ ) -> ( CC X. { A } ) e. ( Poly ` ZZ ) )
13 10 11 12 syl2anc 
 |-  ( A e. NN -> ( CC X. { A } ) e. ( Poly ` ZZ ) )
14 zaddcl 
 |-  ( ( x e. ZZ /\ p e. ZZ ) -> ( x + p ) e. ZZ )
15 14 adantl 
 |-  ( ( A e. NN /\ ( x e. ZZ /\ p e. ZZ ) ) -> ( x + p ) e. ZZ )
16 zmulcl 
 |-  ( ( x e. ZZ /\ p e. ZZ ) -> ( x x. p ) e. ZZ )
17 16 adantl 
 |-  ( ( A e. NN /\ ( x e. ZZ /\ p e. ZZ ) ) -> ( x x. p ) e. ZZ )
18 neg1z 
 |-  -u 1 e. ZZ
19 18 a1i 
 |-  ( A e. NN -> -u 1 e. ZZ )
20 9 13 15 17 19 plysub 
 |-  ( A e. NN -> ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) e. ( Poly ` ZZ ) )
21 0cnd 
 |-  ( A e. NN -> 0 e. CC )
22 ovex 
 |-  ( t ^ 2 ) e. _V
23 22 rgenw 
 |-  A. t e. CC ( t ^ 2 ) e. _V
24 23 a1i 
 |-  ( A e. NN -> A. t e. CC ( t ^ 2 ) e. _V )
25 nfcv 
 |-  F/_ t CC
26 25 mptfnf 
 |-  ( A. t e. CC ( t ^ 2 ) e. _V <-> ( t e. CC |-> ( t ^ 2 ) ) Fn CC )
27 24 26 sylib 
 |-  ( A e. NN -> ( t e. CC |-> ( t ^ 2 ) ) Fn CC )
28 fnconstg 
 |-  ( A e. NN -> ( CC X. { A } ) Fn CC )
29 27 28 jca 
 |-  ( A e. NN -> ( ( t e. CC |-> ( t ^ 2 ) ) Fn CC /\ ( CC X. { A } ) Fn CC ) )
30 cnex 
 |-  CC e. _V
31 30 a1i 
 |-  ( A e. NN -> CC e. _V )
32 31 21 jca 
 |-  ( A e. NN -> ( CC e. _V /\ 0 e. CC ) )
33 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 ) ) )
34 29 32 33 syl2anc 
 |-  ( A e. NN -> ( ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) ` 0 ) = ( ( ( t e. CC |-> ( t ^ 2 ) ) ` 0 ) - ( ( CC X. { A } ) ` 0 ) ) )
35 0cn 
 |-  0 e. CC
36 oveq1 
 |-  ( t = 0 -> ( t ^ 2 ) = ( 0 ^ 2 ) )
37 eqid 
 |-  ( t e. CC |-> ( t ^ 2 ) ) = ( t e. CC |-> ( t ^ 2 ) )
38 ovex 
 |-  ( 0 ^ 2 ) e. _V
39 36 37 38 fvmpt 
 |-  ( 0 e. CC -> ( ( t e. CC |-> ( t ^ 2 ) ) ` 0 ) = ( 0 ^ 2 ) )
40 35 39 ax-mp 
 |-  ( ( t e. CC |-> ( t ^ 2 ) ) ` 0 ) = ( 0 ^ 2 )
41 sq0 
 |-  ( 0 ^ 2 ) = 0
42 40 41 eqtri 
 |-  ( ( t e. CC |-> ( t ^ 2 ) ) ` 0 ) = 0
43 42 a1i 
 |-  ( A e. NN -> ( ( t e. CC |-> ( t ^ 2 ) ) ` 0 ) = 0 )
44 id 
 |-  ( A e. NN -> A e. NN )
45 fvconst2g 
 |-  ( ( A e. NN /\ 0 e. CC ) -> ( ( CC X. { A } ) ` 0 ) = A )
46 44 21 45 syl2anc 
 |-  ( A e. NN -> ( ( CC X. { A } ) ` 0 ) = A )
47 43 46 oveq12d 
 |-  ( A e. NN -> ( ( ( t e. CC |-> ( t ^ 2 ) ) ` 0 ) - ( ( CC X. { A } ) ` 0 ) ) = ( 0 - A ) )
48 34 47 eqtrd 
 |-  ( A e. NN -> ( ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) ` 0 ) = ( 0 - A ) )
49 nnne0 
 |-  ( A e. NN -> A =/= 0 )
50 49 necomd 
 |-  ( A e. NN -> 0 =/= A )
51 21 1 50 subne0d 
 |-  ( A e. NN -> ( 0 - A ) =/= 0 )
52 48 51 eqnetrd 
 |-  ( A e. NN -> ( ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) ` 0 ) =/= 0 )
53 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 )
54 21 52 53 syl2anc 
 |-  ( A e. NN -> ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) =/= 0p )
55 eldifsn 
 |-  ( ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) e. ( ( Poly ` ZZ ) \ { 0p } ) <-> ( ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) e. ( Poly ` ZZ ) /\ ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) =/= 0p ) )
56 20 54 55 sylanbrc 
 |-  ( A e. NN -> ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) e. ( ( Poly ` ZZ ) \ { 0p } ) )
57 31 3 jca 
 |-  ( A e. NN -> ( CC e. _V /\ ( sqrt ` A ) e. CC ) )
58 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 ) ) ) )
59 29 57 58 syl2anc 
 |-  ( A e. NN -> ( ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) ` ( sqrt ` A ) ) = ( ( ( t e. CC |-> ( t ^ 2 ) ) ` ( sqrt ` A ) ) - ( ( CC X. { A } ) ` ( sqrt ` A ) ) ) )
60 oveq1 
 |-  ( t = ( sqrt ` A ) -> ( t ^ 2 ) = ( ( sqrt ` A ) ^ 2 ) )
61 ovex 
 |-  ( ( sqrt ` A ) ^ 2 ) e. _V
62 60 37 61 fvmpt 
 |-  ( ( sqrt ` A ) e. CC -> ( ( t e. CC |-> ( t ^ 2 ) ) ` ( sqrt ` A ) ) = ( ( sqrt ` A ) ^ 2 ) )
63 3 62 syl 
 |-  ( A e. NN -> ( ( t e. CC |-> ( t ^ 2 ) ) ` ( sqrt ` A ) ) = ( ( sqrt ` A ) ^ 2 ) )
64 sqrtth 
 |-  ( A e. CC -> ( ( sqrt ` A ) ^ 2 ) = A )
65 1 64 syl 
 |-  ( A e. NN -> ( ( sqrt ` A ) ^ 2 ) = A )
66 63 65 eqtrd 
 |-  ( A e. NN -> ( ( t e. CC |-> ( t ^ 2 ) ) ` ( sqrt ` A ) ) = A )
67 fvconst2g 
 |-  ( ( A e. NN /\ ( sqrt ` A ) e. CC ) -> ( ( CC X. { A } ) ` ( sqrt ` A ) ) = A )
68 44 3 67 syl2anc 
 |-  ( A e. NN -> ( ( CC X. { A } ) ` ( sqrt ` A ) ) = A )
69 66 68 oveq12d 
 |-  ( A e. NN -> ( ( ( t e. CC |-> ( t ^ 2 ) ) ` ( sqrt ` A ) ) - ( ( CC X. { A } ) ` ( sqrt ` A ) ) ) = ( A - A ) )
70 59 69 eqtrd 
 |-  ( A e. NN -> ( ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) ` ( sqrt ` A ) ) = ( A - A ) )
71 subid 
 |-  ( A e. CC -> ( A - A ) = 0 )
72 1 71 syl 
 |-  ( A e. NN -> ( A - A ) = 0 )
73 70 72 eqtrd 
 |-  ( A e. NN -> ( ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) ` ( sqrt ` A ) ) = 0 )
74 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 ) ) )
75 74 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 ) )
76 75 rspcev 
 |-  ( ( ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) ` ( sqrt ` A ) ) = 0 ) -> E. x e. ( ( Poly ` ZZ ) \ { 0p } ) ( x ` ( sqrt ` A ) ) = 0 )
77 56 73 76 syl2anc 
 |-  ( A e. NN -> E. x e. ( ( Poly ` ZZ ) \ { 0p } ) ( x ` ( sqrt ` A ) ) = 0 )
78 3 77 jca 
 |-  ( A e. NN -> ( ( sqrt ` A ) e. CC /\ E. x e. ( ( Poly ` ZZ ) \ { 0p } ) ( x ` ( sqrt ` A ) ) = 0 ) )
79 elaa 
 |-  ( ( sqrt ` A ) e. AA <-> ( ( sqrt ` A ) e. CC /\ E. x e. ( ( Poly ` ZZ ) \ { 0p } ) ( x ` ( sqrt ` A ) ) = 0 ) )
80 78 79 sylibr 
 |-  ( A e. NN -> ( sqrt ` A ) e. AA )