sqrtnnaa

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

		Ref	Expression
	Assertion	sqrtnnaa	$⊢ A \in ℕ \to \sqrt{A} \in 𝔸$

Proof

Step	Hyp	Ref	Expression
1		nncn	$⊢ A \in ℕ \to A \in ℂ$
2	1	sqrtcld	$⊢ A \in ℕ \to \sqrt{A} \in ℂ$
3		fveq1	$⊢ x = (t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\}) \to x (\sqrt{A}) = ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (\sqrt{A})$
4	3	eqeq1d	$⊢ x = (t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\}) \to (x (\sqrt{A}) = 0 \leftrightarrow ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (\sqrt{A}) = 0)$
5		zsscn	$⊢ ℤ \subseteq ℂ$
6		1z	$⊢ 1 \in ℤ$
7		2nn0	$⊢ 2 \in ℕ_{0}$
8		plypow	$⊢ (ℤ \subseteq ℂ \land 1 \in ℤ \land 2 \in ℕ_{0}) \to (t \in ℂ ⟼ t^{2}) \in Poly (ℤ)$
9	5 6 7 8	mp3an	$⊢ (t \in ℂ ⟼ t^{2}) \in Poly (ℤ)$
10	9	a1i	$⊢ A \in ℕ \to (t \in ℂ ⟼ t^{2}) \in Poly (ℤ)$
11		nnz	$⊢ A \in ℕ \to A \in ℤ$
12		plyconst	$⊢ (ℤ \subseteq ℂ \land A \in ℤ) \to ℂ \times \{A\} \in Poly (ℤ)$
13	5 11 12	sylancr	$⊢ A \in ℕ \to ℂ \times \{A\} \in Poly (ℤ)$
14		zaddcl	$⊢ (x \in ℤ \land p \in ℤ) \to x + p \in ℤ$
15	14	adantl	$⊢ (A \in ℕ \land (x \in ℤ \land p \in ℤ)) \to x + p \in ℤ$
16		zmulcl	$⊢ (x \in ℤ \land p \in ℤ) \to x p \in ℤ$
17	16	adantl	$⊢ (A \in ℕ \land (x \in ℤ \land p \in ℤ)) \to x p \in ℤ$
18		neg1z	$⊢ - 1 \in ℤ$
19	18	a1i	$⊢ A \in ℕ \to - 1 \in ℤ$
20	10 13 15 17 19	plysub	$⊢ A \in ℕ \to (t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\}) \in Poly (ℤ)$
21		0cn	$⊢ 0 \in ℂ$
22		ovex	$⊢ t^{2} \in V$
23	22	rgenw	$⊢ \forall t \in ℂ t^{2} \in V$
24	23	a1i	$⊢ A \in ℕ \to \forall t \in ℂ t^{2} \in V$
25		nfcv	$⊢ \underline{Ⅎ} t ℂ$
26	25	mptfnf	$⊢ \forall t \in ℂ t^{2} \in V \leftrightarrow (t \in ℂ ⟼ t^{2}) Fn ℂ$
27	24 26	sylib	$⊢ A \in ℕ \to (t \in ℂ ⟼ t^{2}) Fn ℂ$
28		fnconstg	$⊢ A \in ℕ \to (ℂ \times \{A\}) Fn ℂ$
29		cnex	$⊢ ℂ \in V$
30	29	a1i	$⊢ A \in ℕ \to ℂ \in V$
31		0cnd	$⊢ A \in ℕ \to 0 \in ℂ$
32		fnfvof	$⊢ (((t \in ℂ ⟼ t^{2}) Fn ℂ \land (ℂ \times \{A\}) Fn ℂ) \land (ℂ \in V \land 0 \in ℂ)) \to ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (0) = (t \in ℂ ⟼ t^{2}) (0) - (ℂ \times \{A\}) (0)$
33	27 28 30 31 32	syl22anc	$⊢ A \in ℕ \to ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (0) = (t \in ℂ ⟼ t^{2}) (0) - (ℂ \times \{A\}) (0)$
34		oveq1	$⊢ t = 0 \to t^{2} = 0^{2}$
35		eqid	$⊢ (t \in ℂ ⟼ t^{2}) = (t \in ℂ ⟼ t^{2})$
36		ovex	$⊢ 0^{2} \in V$
37	34 35 36	fvmpt	$⊢ 0 \in ℂ \to (t \in ℂ ⟼ t^{2}) (0) = 0^{2}$
38	21 37	ax-mp	$⊢ (t \in ℂ ⟼ t^{2}) (0) = 0^{2}$
39		sq0	$⊢ 0^{2} = 0$
40	38 39	eqtri	$⊢ (t \in ℂ ⟼ t^{2}) (0) = 0$
41	40	a1i	$⊢ A \in ℕ \to (t \in ℂ ⟼ t^{2}) (0) = 0$
42		fvconst2g	$⊢ (A \in ℕ \land 0 \in ℂ) \to (ℂ \times \{A\}) (0) = A$
43	31 42	mpdan	$⊢ A \in ℕ \to (ℂ \times \{A\}) (0) = A$
44	41 43	oveq12d	$⊢ A \in ℕ \to (t \in ℂ ⟼ t^{2}) (0) - (ℂ \times \{A\}) (0) = 0 - A$
45	33 44	eqtrd	$⊢ A \in ℕ \to ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (0) = 0 - A$
46		nnne0	$⊢ A \in ℕ \to A \neq 0$
47	46	necomd	$⊢ A \in ℕ \to 0 \neq A$
48	31 1 47	subne0d	$⊢ A \in ℕ \to 0 - A \neq 0$
49	45 48	eqnetrd	$⊢ A \in ℕ \to ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (0) \neq 0$
50		ne0p	$⊢ (0 \in ℂ \land ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (0) \neq 0) \to (t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\}) \neq 0_{𝑝}$
51	21 49 50	sylancr	$⊢ A \in ℕ \to (t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\}) \neq 0_{𝑝}$
52	20 51	eldifsnd	$⊢ A \in ℕ \to (t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\}) \in (Poly (ℤ) ∖ \{0_{𝑝}\})$
53		fnfvof	$⊢ (((t \in ℂ ⟼ t^{2}) Fn ℂ \land (ℂ \times \{A\}) Fn ℂ) \land (ℂ \in V \land \sqrt{A} \in ℂ)) \to ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (\sqrt{A}) = (t \in ℂ ⟼ t^{2}) (\sqrt{A}) - (ℂ \times \{A\}) (\sqrt{A})$
54	27 28 30 2 53	syl22anc	$⊢ A \in ℕ \to ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (\sqrt{A}) = (t \in ℂ ⟼ t^{2}) (\sqrt{A}) - (ℂ \times \{A\}) (\sqrt{A})$
55		oveq1	$⊢ t = \sqrt{A} \to t^{2} = {\sqrt{A}}^{2}$
56		ovex	$⊢ {\sqrt{A}}^{2} \in V$
57	55 35 56	fvmpt	$⊢ \sqrt{A} \in ℂ \to (t \in ℂ ⟼ t^{2}) (\sqrt{A}) = {\sqrt{A}}^{2}$
58	2 57	syl	$⊢ A \in ℕ \to (t \in ℂ ⟼ t^{2}) (\sqrt{A}) = {\sqrt{A}}^{2}$
59	1	sqsqrtd	$⊢ A \in ℕ \to {\sqrt{A}}^{2} = A$
60	58 59	eqtrd	$⊢ A \in ℕ \to (t \in ℂ ⟼ t^{2}) (\sqrt{A}) = A$
61		fvconst2g	$⊢ (A \in ℕ \land \sqrt{A} \in ℂ) \to (ℂ \times \{A\}) (\sqrt{A}) = A$
62	2 61	mpdan	$⊢ A \in ℕ \to (ℂ \times \{A\}) (\sqrt{A}) = A$
63	60 62	oveq12d	$⊢ A \in ℕ \to (t \in ℂ ⟼ t^{2}) (\sqrt{A}) - (ℂ \times \{A\}) (\sqrt{A}) = A - A$
64	54 63	eqtrd	$⊢ A \in ℕ \to ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (\sqrt{A}) = A - A$
65	1	subidd	$⊢ A \in ℕ \to A - A = 0$
66	64 65	eqtrd	$⊢ A \in ℕ \to ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (\sqrt{A}) = 0$
67	4 52 66	rspcedvdw	$⊢ A \in ℕ \to \exists x \in (Poly (ℤ) ∖ \{0_{𝑝}\}) x (\sqrt{A}) = 0$
68		elaa	$⊢ \sqrt{A} \in 𝔸 \leftrightarrow (\sqrt{A} \in ℂ \land \exists x \in (Poly (ℤ) ∖ \{0_{𝑝}\}) x (\sqrt{A}) = 0)$
69	2 67 68	sylanbrc	$⊢ A \in ℕ \to \sqrt{A} \in 𝔸$

Metamath Proof Explorer

Theorem sqrtnnaa

Proof