Theorem sqrtqaa

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

	Ref	Expression
Assertion	sqrtqaa	⊢ ( 𝐴 ∈ ℚ → ( √ ‘ 𝐴 ) ∈ 𝔸 )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝐴 = 0 → ( √ ‘ 𝐴 ) = ( √ ‘ 0 ) )
2		sqrt0	⊢ ( √ ‘ 0 ) = 0
3	1 2	eqtrdi	⊢ ( 𝐴 = 0 → ( √ ‘ 𝐴 ) = 0 )
4		0aa	⊢ 0 ∈ 𝔸
5	3 4	eqeltrdi	⊢ ( 𝐴 = 0 → ( √ ‘ 𝐴 ) ∈ 𝔸 )
6	5	adantl	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐴 = 0 ) → ( √ ‘ 𝐴 ) ∈ 𝔸 )
7		sqrtnzqaa	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ) → ( √ ‘ 𝐴 ) ∈ 𝔸 )
8	6 7	pm2.61dane	⊢ ( 𝐴 ∈ ℚ → ( √ ‘ 𝐴 ) ∈ 𝔸 )