sqrtnzqaa

Description: Square root of a nonzero rational is algebraic. (Contributed by Ender Ting, 22-Jul-2026)

		Ref	Expression
	Assertion	sqrtnzqaa	$⊢ (A \in ℚ \land A \neq 0) \to \sqrt{A} \in 𝔸$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \in ℚ \land A \neq 0) \to A \in ℚ$
2		qcn	$⊢ A \in ℚ \to A \in ℂ$
3		sqrtcl	$⊢ A \in ℂ \to \sqrt{A} \in ℂ$
4	1 2 3	3syl	$⊢ (A \in ℚ \land A \neq 0) \to \sqrt{A} \in ℂ$
5		fveq1	$⊢ x = (t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\}) \to x (\sqrt{A}) = ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (\sqrt{A})$
6	5	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)$
7		qsscn	$⊢ ℚ \subseteq ℂ$
8		1z	$⊢ 1 \in ℤ$
9		zq	$⊢ 1 \in ℤ \to 1 \in ℚ$
10	8 9	ax-mp	$⊢ 1 \in ℚ$
11		2nn0	$⊢ 2 \in ℕ_{0}$
12		plypow	$⊢ (ℚ \subseteq ℂ \land 1 \in ℚ \land 2 \in ℕ_{0}) \to (t \in ℂ ⟼ t^{2}) \in Poly (ℚ)$
13	7 10 11 12	mp3an	$⊢ (t \in ℂ ⟼ t^{2}) \in Poly (ℚ)$
14	13	a1i	$⊢ (A \in ℚ \land A \neq 0) \to (t \in ℂ ⟼ t^{2}) \in Poly (ℚ)$
15	7	a1i	$⊢ (A \in ℚ \land A \neq 0) \to ℚ \subseteq ℂ$
16		plyconst	$⊢ (ℚ \subseteq ℂ \land A \in ℚ) \to ℂ \times \{A\} \in Poly (ℚ)$
17	15 1 16	syl2anc	$⊢ (A \in ℚ \land A \neq 0) \to ℂ \times \{A\} \in Poly (ℚ)$
18		qaddcl	$⊢ (x \in ℚ \land p \in ℚ) \to x + p \in ℚ$
19	18	adantl	$⊢ ((A \in ℚ \land A \neq 0) \land (x \in ℚ \land p \in ℚ)) \to x + p \in ℚ$
20		qmulcl	$⊢ (x \in ℚ \land p \in ℚ) \to x p \in ℚ$
21	20	adantl	$⊢ ((A \in ℚ \land A \neq 0) \land (x \in ℚ \land p \in ℚ)) \to x p \in ℚ$
22		neg1z	$⊢ - 1 \in ℤ$
23		zq	$⊢ - 1 \in ℤ \to - 1 \in ℚ$
24	22 23	ax-mp	$⊢ - 1 \in ℚ$
25	24	a1i	$⊢ (A \in ℚ \land A \neq 0) \to - 1 \in ℚ$
26	14 17 19 21 25	plysub	$⊢ (A \in ℚ \land A \neq 0) \to (t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\}) \in Poly (ℚ)$
27		0cnd	$⊢ (A \in ℚ \land A \neq 0) \to 0 \in ℂ$
28		fnconstg	$⊢ A \in ℚ \to (ℂ \times \{A\}) Fn ℂ$
29	28	adantr	$⊢ (A \in ℚ \land A \neq 0) \to (ℂ \times \{A\}) Fn ℂ$
30		ovex	$⊢ t^{2} \in V$
31	30	rgenw	$⊢ \forall t \in ℂ t^{2} \in V$
32		nfcv	$⊢ \underline{Ⅎ} t ℂ$
33	32	mptfnf	$⊢ \forall t \in ℂ t^{2} \in V \leftrightarrow (t \in ℂ ⟼ t^{2}) Fn ℂ$
34	31 33	mpbi	$⊢ (t \in ℂ ⟼ t^{2}) Fn ℂ$
35	29 34	jctil	$⊢ (A \in ℚ \land A \neq 0) \to ((t \in ℂ ⟼ t^{2}) Fn ℂ \land (ℂ \times \{A\}) Fn ℂ)$
36		cnex	$⊢ ℂ \in V$
37		0cn	$⊢ 0 \in ℂ$
38	36 37	pm3.2i	$⊢ (ℂ \in V \land 0 \in ℂ)$
39	38	a1i	$⊢ (A \in ℚ \land A \neq 0) \to (ℂ \in V \land 0 \in ℂ)$
40		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)$
41	35 39 40	syl2anc	$⊢ (A \in ℚ \land A \neq 0) \to ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (0) = (t \in ℂ ⟼ t^{2}) (0) - (ℂ \times \{A\}) (0)$
42		oveq1	$⊢ t = 0 \to t^{2} = 0^{2}$
43		eqid	$⊢ (t \in ℂ ⟼ t^{2}) = (t \in ℂ ⟼ t^{2})$
44		ovex	$⊢ 0^{2} \in V$
45	42 43 44	fvmpt	$⊢ 0 \in ℂ \to (t \in ℂ ⟼ t^{2}) (0) = 0^{2}$
46	37 45	ax-mp	$⊢ (t \in ℂ ⟼ t^{2}) (0) = 0^{2}$
47		sq0	$⊢ 0^{2} = 0$
48	46 47	eqtri	$⊢ (t \in ℂ ⟼ t^{2}) (0) = 0$
49	48	a1i	$⊢ (A \in ℚ \land A \neq 0) \to (t \in ℂ ⟼ t^{2}) (0) = 0$
50		fvconst2g	$⊢ (A \in ℚ \land 0 \in ℂ) \to (ℂ \times \{A\}) (0) = A$
51	1 27 50	syl2anc	$⊢ (A \in ℚ \land A \neq 0) \to (ℂ \times \{A\}) (0) = A$
52	49 51	oveq12d	$⊢ (A \in ℚ \land A \neq 0) \to (t \in ℂ ⟼ t^{2}) (0) - (ℂ \times \{A\}) (0) = 0 - A$
53	41 52	eqtrd	$⊢ (A \in ℚ \land A \neq 0) \to ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (0) = 0 - A$
54	2	adantr	$⊢ (A \in ℚ \land A \neq 0) \to A \in ℂ$
55		necom	$⊢ A \neq 0 \leftrightarrow 0 \neq A$
56	55	biimpi	$⊢ A \neq 0 \to 0 \neq A$
57	56	adantl	$⊢ (A \in ℚ \land A \neq 0) \to 0 \neq A$
58	27 54 57	subne0d	$⊢ (A \in ℚ \land A \neq 0) \to 0 - A \neq 0$
59	53 58	eqnetrd	$⊢ (A \in ℚ \land A \neq 0) \to ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (0) \neq 0$
60		ne0p	$⊢ (0 \in ℂ \land ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (0) \neq 0) \to (t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\}) \neq 0_{𝑝}$
61	27 59 60	syl2anc	$⊢ (A \in ℚ \land A \neq 0) \to (t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\}) \neq 0_{𝑝}$
62	26 61	eldifsnd	$⊢ (A \in ℚ \land A \neq 0) \to (t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\}) \in (Poly (ℚ) ∖ \{0_{𝑝}\})$
63	4 36	jctil	$⊢ (A \in ℚ \land A \neq 0) \to (ℂ \in V \land \sqrt{A} \in ℂ)$
64		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})$
65	35 63 64	syl2anc	$⊢ (A \in ℚ \land A \neq 0) \to ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (\sqrt{A}) = (t \in ℂ ⟼ t^{2}) (\sqrt{A}) - (ℂ \times \{A\}) (\sqrt{A})$
66		oveq1	$⊢ t = \sqrt{A} \to t^{2} = {\sqrt{A}}^{2}$
67		ovex	$⊢ {\sqrt{A}}^{2} \in V$
68	66 43 67	fvmpt	$⊢ \sqrt{A} \in ℂ \to (t \in ℂ ⟼ t^{2}) (\sqrt{A}) = {\sqrt{A}}^{2}$
69	54 3 68	3syl	$⊢ (A \in ℚ \land A \neq 0) \to (t \in ℂ ⟼ t^{2}) (\sqrt{A}) = {\sqrt{A}}^{2}$
70		sqrtth	$⊢ A \in ℂ \to {\sqrt{A}}^{2} = A$
71	1 2 70	3syl	$⊢ (A \in ℚ \land A \neq 0) \to {\sqrt{A}}^{2} = A$
72	69 71	eqtrd	$⊢ (A \in ℚ \land A \neq 0) \to (t \in ℂ ⟼ t^{2}) (\sqrt{A}) = A$
73		fvconst2g	$⊢ (A \in ℚ \land \sqrt{A} \in ℂ) \to (ℂ \times \{A\}) (\sqrt{A}) = A$
74	1 4 73	syl2anc	$⊢ (A \in ℚ \land A \neq 0) \to (ℂ \times \{A\}) (\sqrt{A}) = A$
75	72 74	oveq12d	$⊢ (A \in ℚ \land A \neq 0) \to (t \in ℂ ⟼ t^{2}) (\sqrt{A}) - (ℂ \times \{A\}) (\sqrt{A}) = A - A$
76	65 75	eqtrd	$⊢ (A \in ℚ \land A \neq 0) \to ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (\sqrt{A}) = A - A$
77		subid	$⊢ A \in ℂ \to A - A = 0$
78	1 2 77	3syl	$⊢ (A \in ℚ \land A \neq 0) \to A - A = 0$
79	76 78	eqtrd	$⊢ (A \in ℚ \land A \neq 0) \to ((t \in ℂ ⟼ t^{2}) -_{f} (ℂ \times \{A\})) (\sqrt{A}) = 0$
80	6 62 79	rspcedvdw	$⊢ (A \in ℚ \land A \neq 0) \to \exists x \in (Poly (ℚ) ∖ \{0_{𝑝}\}) x (\sqrt{A}) = 0$
81		elqaa	$⊢ \sqrt{A} \in 𝔸 \leftrightarrow (\sqrt{A} \in ℂ \land \exists x \in (Poly (ℚ) ∖ \{0_{𝑝}\}) x (\sqrt{A}) = 0)$
82	4 80 81	sylanbrc	$⊢ (A \in ℚ \land A \neq 0) \to \sqrt{A} \in 𝔸$

Metamath Proof Explorer

Theorem sqrtnzqaa

Proof