Theorem sqrtqaa

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

	Ref	Expression
Assertion	sqrtqaa	$$⊢A\in \mathbb{Q}\to \sqrt{A}\in 𝔸$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢A=0\to \sqrt{A}=\sqrt{0}$$
2		sqrt0	$$⊢\sqrt{0}=0$$
3	1 2	eqtrdi	$$⊢A=0\to \sqrt{A}=0$$
4		0aa	$$⊢0\in 𝔸$$
5	3 4	eqeltrdi	$$⊢A=0\to \sqrt{A}\in 𝔸$$
6	5	adantl	$$⊢\left(A\in \mathbb{Q}\wedge A=0\right)\to \sqrt{A}\in 𝔸$$
7		sqrtnzqaa	$$⊢\left(A\in \mathbb{Q}\wedge A\ne 0\right)\to \sqrt{A}\in 𝔸$$
8	6 7	pm2.61dane	$$⊢A\in \mathbb{Q}\to \sqrt{A}\in 𝔸$$