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		sqrtcl	$⊢ A \in ℂ \to \sqrt{A} \in ℂ$
3	1 2	syl	$⊢ A \in ℕ \to \sqrt{A} \in ℂ$
4		zsscn	$⊢ ℤ \subseteq ℂ$
5		1z	$⊢ 1 \in ℤ$
6		2nn0	$⊢ 2 \in ℕ_{0}$
7		plypow	$⊢ (ℤ \subseteq ℂ \land 1 \in ℤ \land 2 \in ℕ_{0}) \to (t \in ℂ ⟼ t^{2}) \in Poly (ℤ)$
8	4 5 6 7	mp3an	$⊢ (t \in ℂ ⟼ t^{2}) \in Poly (ℤ)$
9	8	a1i	$⊢ A \in ℕ \to (t \in ℂ ⟼ t^{2}) \in Poly (ℤ)$
10	4	a1i	$⊢ A \in ℕ \to ℤ \subseteq ℂ$
11		nnz	$⊢ A \in ℕ \to A \in ℤ$
12		plyconst	$⊢ (ℤ \subseteq ℂ \land A \in ℤ) \to ℂ \times \{A\} \in Poly (ℤ)$
13	10 11 12	syl2anc	$⊢ 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	9 13 15 17 19	plysub	$⊢ A \in ℕ \to (t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\}) \in Poly (ℤ)$
21		0cnd	$⊢ A \in ℕ \to 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	27 28	jca	$⊢ A \in ℕ \to ((t \in ℂ ⟼ t^{2}) Fn ℂ \land (ℂ \times \{A\}) Fn ℂ)$
30		cnex	$⊢ ℂ \in V$
31	30	a1i	$⊢ A \in ℕ \to ℂ \in V$
32	31 21	jca	$⊢ A \in ℕ \to (ℂ \in V \land 0 \in ℂ)$
33		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)$
34	29 32 33	syl2anc	$⊢ A \in ℕ \to ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (0) = (t \in ℂ ⟼ t^{2}) (0) - (ℂ \times \{A\}) (0)$
35		0cn	$⊢ 0 \in ℂ$
36		oveq1	$⊢ t = 0 \to t^{2} = 0^{2}$
37		eqid	$⊢ (t \in ℂ ⟼ t^{2}) = (t \in ℂ ⟼ t^{2})$
38		ovex	$⊢ 0^{2} \in V$
39	36 37 38	fvmpt	$⊢ 0 \in ℂ \to (t \in ℂ ⟼ t^{2}) (0) = 0^{2}$
40	35 39	ax-mp	$⊢ (t \in ℂ ⟼ t^{2}) (0) = 0^{2}$
41		sq0	$⊢ 0^{2} = 0$
42	40 41	eqtri	$⊢ (t \in ℂ ⟼ t^{2}) (0) = 0$
43	42	a1i	$⊢ A \in ℕ \to (t \in ℂ ⟼ t^{2}) (0) = 0$
44		id	$⊢ A \in ℕ \to A \in ℕ$
45		fvconst2g	$⊢ (A \in ℕ \land 0 \in ℂ) \to (ℂ \times \{A\}) (0) = A$
46	44 21 45	syl2anc	$⊢ A \in ℕ \to (ℂ \times \{A\}) (0) = A$
47	43 46	oveq12d	$⊢ A \in ℕ \to (t \in ℂ ⟼ t^{2}) (0) - (ℂ \times \{A\}) (0) = 0 - A$
48	34 47	eqtrd	$⊢ A \in ℕ \to ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (0) = 0 - A$
49		nnne0	$⊢ A \in ℕ \to A \neq 0$
50	49	necomd	$⊢ A \in ℕ \to 0 \neq A$
51	21 1 50	subne0d	$⊢ A \in ℕ \to 0 - A \neq 0$
52	48 51	eqnetrd	$⊢ A \in ℕ \to ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (0) \neq 0$
53		ne0p	$⊢ (0 \in ℂ \land ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (0) \neq 0) \to (t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\}) \neq 0_{𝑝}$
54	21 52 53	syl2anc	$⊢ A \in ℕ \to (t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\}) \neq 0_{𝑝}$
55		eldifsn	$⊢ (t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\}) \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \leftrightarrow ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\}) \in Poly (ℤ) \land (t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\}) \neq 0_{𝑝})$
56	20 54 55	sylanbrc	$⊢ A \in ℕ \to (t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\}) \in (Poly (ℤ) ∖ \{0_{𝑝}\})$
57	31 3	jca	$⊢ A \in ℕ \to (ℂ \in V \land \sqrt{A} \in ℂ)$
58		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})$
59	29 57 58	syl2anc	$⊢ A \in ℕ \to ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (\sqrt{A}) = (t \in ℂ ⟼ t^{2}) (\sqrt{A}) - (ℂ \times \{A\}) (\sqrt{A})$
60		oveq1	$⊢ t = \sqrt{A} \to t^{2} = {\sqrt{A}}^{2}$
61		ovex	$⊢ {\sqrt{A}}^{2} \in V$
62	60 37 61	fvmpt	$⊢ \sqrt{A} \in ℂ \to (t \in ℂ ⟼ t^{2}) (\sqrt{A}) = {\sqrt{A}}^{2}$
63	3 62	syl	$⊢ A \in ℕ \to (t \in ℂ ⟼ t^{2}) (\sqrt{A}) = {\sqrt{A}}^{2}$
64		sqrtth	$⊢ A \in ℂ \to {\sqrt{A}}^{2} = A$
65	1 64	syl	$⊢ A \in ℕ \to {\sqrt{A}}^{2} = A$
66	63 65	eqtrd	$⊢ A \in ℕ \to (t \in ℂ ⟼ t^{2}) (\sqrt{A}) = A$
67		fvconst2g	$⊢ (A \in ℕ \land \sqrt{A} \in ℂ) \to (ℂ \times \{A\}) (\sqrt{A}) = A$
68	44 3 67	syl2anc	$⊢ A \in ℕ \to (ℂ \times \{A\}) (\sqrt{A}) = A$
69	66 68	oveq12d	$⊢ A \in ℕ \to (t \in ℂ ⟼ t^{2}) (\sqrt{A}) - (ℂ \times \{A\}) (\sqrt{A}) = A - A$
70	59 69	eqtrd	$⊢ A \in ℕ \to ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (\sqrt{A}) = A - A$
71		subid	$⊢ A \in ℂ \to A - A = 0$
72	1 71	syl	$⊢ A \in ℕ \to A - A = 0$
73	70 72	eqtrd	$⊢ A \in ℕ \to ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (\sqrt{A}) = 0$
74		fveq1	$⊢ x = (t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\}) \to x (\sqrt{A}) = ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (\sqrt{A})$
75	74	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)$
76	75	rspcev	$⊢ ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\}) \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \land ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (\sqrt{A}) = 0) \to \exists x \in (Poly (ℤ) ∖ \{0_{𝑝}\}) x (\sqrt{A}) = 0$
77	56 73 76	syl2anc	$⊢ A \in ℕ \to \exists x \in (Poly (ℤ) ∖ \{0_{𝑝}\}) x (\sqrt{A}) = 0$
78	3 77	jca	$⊢ A \in ℕ \to (\sqrt{A} \in ℂ \land \exists x \in (Poly (ℤ) ∖ \{0_{𝑝}\}) x (\sqrt{A}) = 0)$
79		elaa	$⊢ \sqrt{A} \in 𝔸 \leftrightarrow (\sqrt{A} \in ℂ \land \exists x \in (Poly (ℤ) ∖ \{0_{𝑝}\}) x (\sqrt{A}) = 0)$
80	78 79	sylibr	$⊢ A \in ℕ \to \sqrt{A} \in 𝔸$

Metamath Proof Explorer

Theorem sqrtnnaa

Proof