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 1 sqrtcld ⊢ ( 𝐴 ∈ ℕ → ( √ ‘ 𝐴 ) ∈ ℂ )
3 fveq1 ⊢ ( 𝑥 = ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) → ( 𝑥 ‘ ( √ ‘ 𝐴 ) ) = ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ‘ ( √ ‘ 𝐴 ) ) )
4 3 eqeq1d ⊢ ( 𝑥 = ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) → ( ( 𝑥 ‘ ( √ ‘ 𝐴 ) ) = 0 ↔ ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ‘ ( √ ‘ 𝐴 ) ) = 0 ) )
5 zsscn ⊢ ℤ ⊆ ℂ
6 1z ⊢ 1 ∈ ℤ
7 2nn0 ⊢ 2 ∈ ℕ0
8 plypow ⊢ ( ( ℤ ⊆ ℂ ∧ 1 ∈ ℤ ∧ 2 ∈ ℕ0 ) → ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∈ ( Poly ‘ ℤ ) )
9 5 6 7 8 mp3an ⊢ ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∈ ( Poly ‘ ℤ )
10 9 a1i ⊢ ( 𝐴 ∈ ℕ → ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∈ ( Poly ‘ ℤ ) )
11 nnz ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ )
12 plyconst ⊢ ( ( ℤ ⊆ ℂ ∧ 𝐴 ∈ ℤ ) → ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℤ ) )
13 5 11 12 sylancr ⊢ ( 𝐴 ∈ ℕ → ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℤ ) )
14 zaddcl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑝 ∈ ℤ ) → ( 𝑥 + 𝑝 ) ∈ ℤ )
15 14 adantl ⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝑥 ∈ ℤ ∧ 𝑝 ∈ ℤ ) ) → ( 𝑥 + 𝑝 ) ∈ ℤ )
16 zmulcl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑝 ∈ ℤ ) → ( 𝑥 · 𝑝 ) ∈ ℤ )
17 16 adantl ⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝑥 ∈ ℤ ∧ 𝑝 ∈ ℤ ) ) → ( 𝑥 · 𝑝 ) ∈ ℤ )
18 neg1z ⊢ - 1 ∈ ℤ
19 18 a1i ⊢ ( 𝐴 ∈ ℕ → - 1 ∈ ℤ )
20 10 13 15 17 19 plysub ⊢ ( 𝐴 ∈ ℕ → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ∈ ( Poly ‘ ℤ ) )
21 0cn ⊢ 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 cnex ⊢ ℂ ∈ V
30 29 a1i ⊢ ( 𝐴 ∈ ℕ → ℂ ∈ V )
31 0cnd ⊢ ( 𝐴 ∈ ℕ → 0 ∈ ℂ )
32 fnfvof ⊢ ( ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) Fn ℂ ∧ ( ℂ × { 𝐴 } ) Fn ℂ ) ∧ ( ℂ ∈ V ∧ 0 ∈ ℂ ) ) → ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ‘ 0 ) = ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ‘ 0 ) − ( ( ℂ × { 𝐴 } ) ‘ 0 ) ) )
33 27 28 30 31 32 syl22anc ⊢ ( 𝐴 ∈ ℕ → ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ‘ 0 ) = ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ‘ 0 ) − ( ( ℂ × { 𝐴 } ) ‘ 0 ) ) )
34 oveq1 ⊢ ( 𝑡 = 0 → ( 𝑡 ↑ 2 ) = ( 0 ↑ 2 ) )
35 eqid ⊢ ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) = ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) )
36 ovex ⊢ ( 0 ↑ 2 ) ∈ V
37 34 35 36 fvmpt ⊢ ( 0 ∈ ℂ → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ‘ 0 ) = ( 0 ↑ 2 ) )
38 21 37 ax-mp ⊢ ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ‘ 0 ) = ( 0 ↑ 2 )
39 sq0 ⊢ ( 0 ↑ 2 ) = 0
40 38 39 eqtri ⊢ ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ‘ 0 ) = 0
41 40 a1i ⊢ ( 𝐴 ∈ ℕ → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ‘ 0 ) = 0 )
42 fvconst2g ⊢ ( ( 𝐴 ∈ ℕ ∧ 0 ∈ ℂ ) → ( ( ℂ × { 𝐴 } ) ‘ 0 ) = 𝐴 )
43 31 42 mpdan ⊢ ( 𝐴 ∈ ℕ → ( ( ℂ × { 𝐴 } ) ‘ 0 ) = 𝐴 )
44 41 43 oveq12d ⊢ ( 𝐴 ∈ ℕ → ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ‘ 0 ) − ( ( ℂ × { 𝐴 } ) ‘ 0 ) ) = ( 0 − 𝐴 ) )
45 33 44 eqtrd ⊢ ( 𝐴 ∈ ℕ → ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ‘ 0 ) = ( 0 − 𝐴 ) )
46 nnne0 ⊢ ( 𝐴 ∈ ℕ → 𝐴 ≠ 0 )
47 46 necomd ⊢ ( 𝐴 ∈ ℕ → 0 ≠ 𝐴 )
48 31 1 47 subne0d ⊢ ( 𝐴 ∈ ℕ → ( 0 − 𝐴 ) ≠ 0 )
49 45 48 eqnetrd ⊢ ( 𝐴 ∈ ℕ → ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ‘ 0 ) ≠ 0 )
50 ne0p ⊢ ( ( 0 ∈ ℂ ∧ ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ‘ 0 ) ≠ 0 ) → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ≠ 0𝑝 )
51 21 49 50 sylancr ⊢ ( 𝐴 ∈ ℕ → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ≠ 0𝑝 )
52 20 51 eldifsnd ⊢ ( 𝐴 ∈ ℕ → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) )
53 fnfvof ⊢ ( ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) Fn ℂ ∧ ( ℂ × { 𝐴 } ) Fn ℂ ) ∧ ( ℂ ∈ V ∧ ( √ ‘ 𝐴 ) ∈ ℂ ) ) → ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ‘ ( √ ‘ 𝐴 ) ) = ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ‘ ( √ ‘ 𝐴 ) ) − ( ( ℂ × { 𝐴 } ) ‘ ( √ ‘ 𝐴 ) ) ) )
54 27 28 30 2 53 syl22anc ⊢ ( 𝐴 ∈ ℕ → ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ‘ ( √ ‘ 𝐴 ) ) = ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ‘ ( √ ‘ 𝐴 ) ) − ( ( ℂ × { 𝐴 } ) ‘ ( √ ‘ 𝐴 ) ) ) )
55 oveq1 ⊢ ( 𝑡 = ( √ ‘ 𝐴 ) → ( 𝑡 ↑ 2 ) = ( ( √ ‘ 𝐴 ) ↑ 2 ) )
56 ovex ⊢ ( ( √ ‘ 𝐴 ) ↑ 2 ) ∈ V
57 55 35 56 fvmpt ⊢ ( ( √ ‘ 𝐴 ) ∈ ℂ → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ‘ ( √ ‘ 𝐴 ) ) = ( ( √ ‘ 𝐴 ) ↑ 2 ) )
58 2 57 syl ⊢ ( 𝐴 ∈ ℕ → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ‘ ( √ ‘ 𝐴 ) ) = ( ( √ ‘ 𝐴 ) ↑ 2 ) )
59 1 sqsqrtd ⊢ ( 𝐴 ∈ ℕ → ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 )
60 58 59 eqtrd ⊢ ( 𝐴 ∈ ℕ → ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ‘ ( √ ‘ 𝐴 ) ) = 𝐴 )
61 fvconst2g ⊢ ( ( 𝐴 ∈ ℕ ∧ ( √ ‘ 𝐴 ) ∈ ℂ ) → ( ( ℂ × { 𝐴 } ) ‘ ( √ ‘ 𝐴 ) ) = 𝐴 )
62 2 61 mpdan ⊢ ( 𝐴 ∈ ℕ → ( ( ℂ × { 𝐴 } ) ‘ ( √ ‘ 𝐴 ) ) = 𝐴 )
63 60 62 oveq12d ⊢ ( 𝐴 ∈ ℕ → ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ‘ ( √ ‘ 𝐴 ) ) − ( ( ℂ × { 𝐴 } ) ‘ ( √ ‘ 𝐴 ) ) ) = ( 𝐴 − 𝐴 ) )
64 54 63 eqtrd ⊢ ( 𝐴 ∈ ℕ → ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ‘ ( √ ‘ 𝐴 ) ) = ( 𝐴 − 𝐴 ) )
65 1 subidd ⊢ ( 𝐴 ∈ ℕ → ( 𝐴 − 𝐴 ) = 0 )
66 64 65 eqtrd ⊢ ( 𝐴 ∈ ℕ → ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑡 ↑ 2 ) ) ∘f − ( ℂ × { 𝐴 } ) ) ‘ ( √ ‘ 𝐴 ) ) = 0 )
67 4 52 66 rspcedvdw ⊢ ( 𝐴 ∈ ℕ → ∃ 𝑥 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑥 ‘ ( √ ‘ 𝐴 ) ) = 0 )
68 elaa ⊢ ( ( √ ‘ 𝐴 ) ∈ 𝔸 ↔ ( ( √ ‘ 𝐴 ) ∈ ℂ ∧ ∃ 𝑥 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑥 ‘ ( √ ‘ 𝐴 ) ) = 0 ) )
69 2 67 68 sylanbrc ⊢ ( 𝐴 ∈ ℕ → ( √ ‘ 𝐴 ) ∈ 𝔸 )