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 1 sqrtcld 
 |-  ( A e. NN -> ( sqrt ` A ) e. CC )
3 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 ) ) )
4 3 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 ) )
5 zsscn 
 |-  ZZ C_ CC
6 1z 
 |-  1 e. ZZ
7 2nn0 
 |-  2 e. NN0
8 plypow 
 |-  ( ( ZZ C_ CC /\ 1 e. ZZ /\ 2 e. NN0 ) -> ( t e. CC |-> ( t ^ 2 ) ) e. ( Poly ` ZZ ) )
9 5 6 7 8 mp3an 
 |-  ( t e. CC |-> ( t ^ 2 ) ) e. ( Poly ` ZZ )
10 9 a1i 
 |-  ( A e. NN -> ( t e. CC |-> ( t ^ 2 ) ) e. ( Poly ` ZZ ) )
11 nnz 
 |-  ( A e. NN -> A e. ZZ )
12 plyconst 
 |-  ( ( ZZ C_ CC /\ A e. ZZ ) -> ( CC X. { A } ) e. ( Poly ` ZZ ) )
13 5 11 12 sylancr 
 |-  ( 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 10 13 15 17 19 plysub 
 |-  ( A e. NN -> ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) e. ( Poly ` ZZ ) )
21 0cn 
 |-  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 cnex 
 |-  CC e. _V
30 29 a1i 
 |-  ( A e. NN -> CC e. _V )
31 0cnd 
 |-  ( A e. NN -> 0 e. CC )
32 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 ) ) )
33 27 28 30 31 32 syl22anc 
 |-  ( A e. NN -> ( ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) ` 0 ) = ( ( ( t e. CC |-> ( t ^ 2 ) ) ` 0 ) - ( ( CC X. { A } ) ` 0 ) ) )
34 oveq1 
 |-  ( t = 0 -> ( t ^ 2 ) = ( 0 ^ 2 ) )
35 eqid 
 |-  ( t e. CC |-> ( t ^ 2 ) ) = ( t e. CC |-> ( t ^ 2 ) )
36 ovex 
 |-  ( 0 ^ 2 ) e. _V
37 34 35 36 fvmpt 
 |-  ( 0 e. CC -> ( ( t e. CC |-> ( t ^ 2 ) ) ` 0 ) = ( 0 ^ 2 ) )
38 21 37 ax-mp 
 |-  ( ( t e. CC |-> ( t ^ 2 ) ) ` 0 ) = ( 0 ^ 2 )
39 sq0 
 |-  ( 0 ^ 2 ) = 0
40 38 39 eqtri 
 |-  ( ( t e. CC |-> ( t ^ 2 ) ) ` 0 ) = 0
41 40 a1i 
 |-  ( A e. NN -> ( ( t e. CC |-> ( t ^ 2 ) ) ` 0 ) = 0 )
42 fvconst2g 
 |-  ( ( A e. NN /\ 0 e. CC ) -> ( ( CC X. { A } ) ` 0 ) = A )
43 31 42 mpdan 
 |-  ( A e. NN -> ( ( CC X. { A } ) ` 0 ) = A )
44 41 43 oveq12d 
 |-  ( A e. NN -> ( ( ( t e. CC |-> ( t ^ 2 ) ) ` 0 ) - ( ( CC X. { A } ) ` 0 ) ) = ( 0 - A ) )
45 33 44 eqtrd 
 |-  ( A e. NN -> ( ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) ` 0 ) = ( 0 - A ) )
46 nnne0 
 |-  ( A e. NN -> A =/= 0 )
47 46 necomd 
 |-  ( A e. NN -> 0 =/= A )
48 31 1 47 subne0d 
 |-  ( A e. NN -> ( 0 - A ) =/= 0 )
49 45 48 eqnetrd 
 |-  ( A e. NN -> ( ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) ` 0 ) =/= 0 )
50 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 )
51 21 49 50 sylancr 
 |-  ( A e. NN -> ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) =/= 0p )
52 20 51 eldifsnd 
 |-  ( A e. NN -> ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) e. ( ( Poly ` ZZ ) \ { 0p } ) )
53 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 ) ) ) )
54 27 28 30 2 53 syl22anc 
 |-  ( 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 ) ) ) )
55 oveq1 
 |-  ( t = ( sqrt ` A ) -> ( t ^ 2 ) = ( ( sqrt ` A ) ^ 2 ) )
56 ovex 
 |-  ( ( sqrt ` A ) ^ 2 ) e. _V
57 55 35 56 fvmpt 
 |-  ( ( sqrt ` A ) e. CC -> ( ( t e. CC |-> ( t ^ 2 ) ) ` ( sqrt ` A ) ) = ( ( sqrt ` A ) ^ 2 ) )
58 2 57 syl 
 |-  ( A e. NN -> ( ( t e. CC |-> ( t ^ 2 ) ) ` ( sqrt ` A ) ) = ( ( sqrt ` A ) ^ 2 ) )
59 1 sqsqrtd 
 |-  ( A e. NN -> ( ( sqrt ` A ) ^ 2 ) = A )
60 58 59 eqtrd 
 |-  ( A e. NN -> ( ( t e. CC |-> ( t ^ 2 ) ) ` ( sqrt ` A ) ) = A )
61 fvconst2g 
 |-  ( ( A e. NN /\ ( sqrt ` A ) e. CC ) -> ( ( CC X. { A } ) ` ( sqrt ` A ) ) = A )
62 2 61 mpdan 
 |-  ( A e. NN -> ( ( CC X. { A } ) ` ( sqrt ` A ) ) = A )
63 60 62 oveq12d 
 |-  ( A e. NN -> ( ( ( t e. CC |-> ( t ^ 2 ) ) ` ( sqrt ` A ) ) - ( ( CC X. { A } ) ` ( sqrt ` A ) ) ) = ( A - A ) )
64 54 63 eqtrd 
 |-  ( A e. NN -> ( ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) ` ( sqrt ` A ) ) = ( A - A ) )
65 1 subidd 
 |-  ( A e. NN -> ( A - A ) = 0 )
66 64 65 eqtrd 
 |-  ( A e. NN -> ( ( ( t e. CC |-> ( t ^ 2 ) ) oF - ( CC X. { A } ) ) ` ( sqrt ` A ) ) = 0 )
67 4 52 66 rspcedvdw 
 |-  ( A e. NN -> E. x e. ( ( Poly ` ZZ ) \ { 0p } ) ( x ` ( sqrt ` A ) ) = 0 )
68 elaa 
 |-  ( ( sqrt ` A ) e. AA <-> ( ( sqrt ` A ) e. CC /\ E. x e. ( ( Poly ` ZZ ) \ { 0p } ) ( x ` ( sqrt ` A ) ) = 0 ) )
69 2 67 68 sylanbrc 
 |-  ( A e. NN -> ( sqrt ` A ) e. AA )