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 ( ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) → ( √ ‘ 𝐴 ) ∈ 𝔸 )

Proof

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