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 ( 𝐴 ∈ ℕ → ( √ ‘ 𝐴 ) ∈ 𝔸 )

Proof

Step Hyp Ref Expression
1 nncn ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℂ )
2 sqrtcl ⊢ ( 𝐴 ∈ ℂ → ( √ ‘ 𝐴 ) ∈ ℂ )
3 1 2 syl ⊢ ( 𝐴 ∈ ℕ → ( √ ‘ 𝐴 ) ∈ ℂ )
4 zsscn ⊢ ℤ ⊆ ℂ
5 1z ⊢ 1 ∈ ℤ
6 2nn0 ⊢ 2 ∈ ℕ0
7 plypow ⊢ ( ( ℤ ⊆ ℂ ∧ 1 ∈ ℤ ∧ 2 ∈ ℕ0 ) → ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∈ ( Poly ‘ ℤ ) )
8 4 5 6 7 mp3an ⊢ ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∈ ( Poly ‘ ℤ )
9 8 a1i ⊢ ( 𝐴 ∈ ℕ → ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∈ ( Poly ‘ ℤ ) )
10 4 a1i ⊢ ( 𝐴 ∈ ℕ → ℤ ⊆ ℂ )
11 nnz ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ )
12 plyconst ⊢ ( ( ℤ ⊆ ℂ ∧ 𝐴 ∈ ℤ ) → ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℤ ) )
13 10 11 12 syl2anc ⊢ ( 𝐴 ∈ ℕ → ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℤ ) )
14 zaddcl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑝 ∈ ℤ ) → ( 𝑥 + 𝑝 ) ∈ ℤ )
15 14 adantl ⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝑥 ∈ ℤ ∧ 𝑝 ∈ ℤ ) ) → ( 𝑥 + 𝑝 ) ∈ ℤ )
16 zmulcl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑝 ∈ ℤ ) → ( 𝑥 · 𝑝 ) ∈ ℤ )
17 16 adantl ⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝑥 ∈ ℤ ∧ 𝑝 ∈ ℤ ) ) → ( 𝑥 · 𝑝 ) ∈ ℤ )
18 neg1z ⊢ - 1 ∈ ℤ
19 18 a1i ⊢ ( 𝐴 ∈ ℕ → - 1 ∈ ℤ )
20 9 13 15 17 19 plysub ⊢ ( 𝐴 ∈ ℕ → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ∈ ( Poly ‘ ℤ ) )
21 0cnd ⊢ ( 𝐴 ∈ ℕ → 0 ∈ ℂ )
22 ovex ⊢ ( 𝑡 ↑ 2 ) ∈ V
23 22 rgenw ⊢ ∀ 𝑡 ∈ ℂ ( 𝑡 ↑ 2 ) ∈ V
24 23 a1i ⊢ ( 𝐴 ∈ ℕ → ∀ 𝑡 ∈ ℂ ( 𝑡 ↑ 2 ) ∈ V )
25 nfcv ⊢ Ⅎ 𝑡 ℂ
26 25 mptfnf ⊢ ( ∀ 𝑡 ∈ ℂ ( 𝑡 ↑ 2 ) ∈ V ↔ ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) Fn ℂ )
27 24 26 sylib ⊢ ( 𝐴 ∈ ℕ → ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) Fn ℂ )
28 fnconstg ⊢ ( 𝐴 ∈ ℕ → ( ℂ × { 𝐴 } ) Fn ℂ )
29 27 28 jca ⊢ ( 𝐴 ∈ ℕ → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) Fn ℂ ∧ ( ℂ × { 𝐴 } ) Fn ℂ ) )
30 cnex ⊢ ℂ ∈ V
31 30 a1i ⊢ ( 𝐴 ∈ ℕ → ℂ ∈ V )
32 31 21 jca ⊢ ( 𝐴 ∈ ℕ → ( ℂ ∈ V ∧ 0 ∈ ℂ ) )
33 fnfvof ⊢ ( ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) Fn ℂ ∧ ( ℂ × { 𝐴 } ) Fn ℂ ) ∧ ( ℂ ∈ V ∧ 0 ∈ ℂ ) ) → ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ‘ 0 ) = ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ‘ 0 ) − ( ( ℂ × { 𝐴 } ) ‘ 0 ) ) )
34 29 32 33 syl2anc ⊢ ( 𝐴 ∈ ℕ → ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ‘ 0 ) = ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ‘ 0 ) − ( ( ℂ × { 𝐴 } ) ‘ 0 ) ) )
35 0cn ⊢ 0 ∈ ℂ
36 oveq1 ⊢ ( 𝑡 = 0 → ( 𝑡 ↑ 2 ) = ( 0 ↑ 2 ) )
37 eqid ⊢ ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) = ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) )
38 ovex ⊢ ( 0 ↑ 2 ) ∈ V
39 36 37 38 fvmpt ⊢ ( 0 ∈ ℂ → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ‘ 0 ) = ( 0 ↑ 2 ) )
40 35 39 ax-mp ⊢ ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ‘ 0 ) = ( 0 ↑ 2 )
41 sq0 ⊢ ( 0 ↑ 2 ) = 0
42 40 41 eqtri ⊢ ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ‘ 0 ) = 0
43 42 a1i ⊢ ( 𝐴 ∈ ℕ → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ‘ 0 ) = 0 )
44 id ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℕ )
45 fvconst2g ⊢ ( ( 𝐴 ∈ ℕ ∧ 0 ∈ ℂ ) → ( ( ℂ × { 𝐴 } ) ‘ 0 ) = 𝐴 )
46 44 21 45 syl2anc ⊢ ( 𝐴 ∈ ℕ → ( ( ℂ × { 𝐴 } ) ‘ 0 ) = 𝐴 )
47 43 46 oveq12d ⊢ ( 𝐴 ∈ ℕ → ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ‘ 0 ) − ( ( ℂ × { 𝐴 } ) ‘ 0 ) ) = ( 0 − 𝐴 ) )
48 34 47 eqtrd ⊢ ( 𝐴 ∈ ℕ → ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ‘ 0 ) = ( 0 − 𝐴 ) )
49 nnne0 ⊢ ( 𝐴 ∈ ℕ → 𝐴 ≠ 0 )
50 49 necomd ⊢ ( 𝐴 ∈ ℕ → 0 ≠ 𝐴 )
51 21 1 50 subne0d ⊢ ( 𝐴 ∈ ℕ → ( 0 − 𝐴 ) ≠ 0 )
52 48 51 eqnetrd ⊢ ( 𝐴 ∈ ℕ → ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ‘ 0 ) ≠ 0 )
53 ne0p ⊢ ( ( 0 ∈ ℂ ∧ ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ‘ 0 ) ≠ 0 ) → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ≠ 0𝑝 )
54 21 52 53 syl2anc ⊢ ( 𝐴 ∈ ℕ → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ≠ 0𝑝 )
55 eldifsn ⊢ ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ↔ ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ∈ ( Poly ‘ ℤ ) ∧ ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ≠ 0𝑝 ) )
56 20 54 55 sylanbrc ⊢ ( 𝐴 ∈ ℕ → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) )
57 31 3 jca ⊢ ( 𝐴 ∈ ℕ → ( ℂ ∈ V ∧ ( √ ‘ 𝐴 ) ∈ ℂ ) )
58 fnfvof ⊢ ( ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) Fn ℂ ∧ ( ℂ × { 𝐴 } ) Fn ℂ ) ∧ ( ℂ ∈ V ∧ ( √ ‘ 𝐴 ) ∈ ℂ ) ) → ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ‘ ( √ ‘ 𝐴 ) ) = ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ‘ ( √ ‘ 𝐴 ) ) − ( ( ℂ × { 𝐴 } ) ‘ ( √ ‘ 𝐴 ) ) ) )
59 29 57 58 syl2anc ⊢ ( 𝐴 ∈ ℕ → ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ‘ ( √ ‘ 𝐴 ) ) = ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ‘ ( √ ‘ 𝐴 ) ) − ( ( ℂ × { 𝐴 } ) ‘ ( √ ‘ 𝐴 ) ) ) )
60 oveq1 ⊢ ( 𝑡 = ( √ ‘ 𝐴 ) → ( 𝑡 ↑ 2 ) = ( ( √ ‘ 𝐴 ) ↑ 2 ) )
61 ovex ⊢ ( ( √ ‘ 𝐴 ) ↑ 2 ) ∈ V
62 60 37 61 fvmpt ⊢ ( ( √ ‘ 𝐴 ) ∈ ℂ → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ‘ ( √ ‘ 𝐴 ) ) = ( ( √ ‘ 𝐴 ) ↑ 2 ) )
63 3 62 syl ⊢ ( 𝐴 ∈ ℕ → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ‘ ( √ ‘ 𝐴 ) ) = ( ( √ ‘ 𝐴 ) ↑ 2 ) )
64 sqrtth ⊢ ( 𝐴 ∈ ℂ → ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 )
65 1 64 syl ⊢ ( 𝐴 ∈ ℕ → ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 )
66 63 65 eqtrd ⊢ ( 𝐴 ∈ ℕ → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ‘ ( √ ‘ 𝐴 ) ) = 𝐴 )
67 fvconst2g ⊢ ( ( 𝐴 ∈ ℕ ∧ ( √ ‘ 𝐴 ) ∈ ℂ ) → ( ( ℂ × { 𝐴 } ) ‘ ( √ ‘ 𝐴 ) ) = 𝐴 )
68 44 3 67 syl2anc ⊢ ( 𝐴 ∈ ℕ → ( ( ℂ × { 𝐴 } ) ‘ ( √ ‘ 𝐴 ) ) = 𝐴 )
69 66 68 oveq12d ⊢ ( 𝐴 ∈ ℕ → ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ‘ ( √ ‘ 𝐴 ) ) − ( ( ℂ × { 𝐴 } ) ‘ ( √ ‘ 𝐴 ) ) ) = ( 𝐴 − 𝐴 ) )
70 59 69 eqtrd ⊢ ( 𝐴 ∈ ℕ → ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ‘ ( √ ‘ 𝐴 ) ) = ( 𝐴 − 𝐴 ) )
71 subid ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 − 𝐴 ) = 0 )
72 1 71 syl ⊢ ( 𝐴 ∈ ℕ → ( 𝐴 − 𝐴 ) = 0 )
73 70 72 eqtrd ⊢ ( 𝐴 ∈ ℕ → ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ‘ ( √ ‘ 𝐴 ) ) = 0 )
74 fveq1 ⊢ ( 𝑥 = ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) → ( 𝑥 ‘ ( √ ‘ 𝐴 ) ) = ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ‘ ( √ ‘ 𝐴 ) ) )
75 74 eqeq1d ⊢ ( 𝑥 = ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) → ( ( 𝑥 ‘ ( √ ‘ 𝐴 ) ) = 0 ↔ ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ‘ ( √ ‘ 𝐴 ) ) = 0 ) )
76 75 rspcev ⊢ ( ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ∧ ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ‘ ( √ ‘ 𝐴 ) ) = 0 ) → ∃ 𝑥 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑥 ‘ ( √ ‘ 𝐴 ) ) = 0 )
77 56 73 76 syl2anc ⊢ ( 𝐴 ∈ ℕ → ∃ 𝑥 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑥 ‘ ( √ ‘ 𝐴 ) ) = 0 )
78 3 77 jca ⊢ ( 𝐴 ∈ ℕ → ( ( √ ‘ 𝐴 ) ∈ ℂ ∧ ∃ 𝑥 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑥 ‘ ( √ ‘ 𝐴 ) ) = 0 ) )
79 elaa ⊢ ( ( √ ‘ 𝐴 ) ∈ 𝔸 ↔ ( ( √ ‘ 𝐴 ) ∈ ℂ ∧ ∃ 𝑥 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑥 ‘ ( √ ‘ 𝐴 ) ) = 0 ) )
80 78 79 sylibr ⊢ ( 𝐴 ∈ ℕ → ( √ ‘ 𝐴 ) ∈ 𝔸 )