Metamath Proof Explorer

Theorem sqrtqaa

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

Ref Expression
Assertion sqrtqaa 
|- ( A e. QQ -> ( sqrt ` A ) e. AA )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( A = 0 -> ( sqrt ` A ) = ( sqrt ` 0 ) )
2 sqrt0 
 |-  ( sqrt ` 0 ) = 0
3 1 2 eqtrdi 
 |-  ( A = 0 -> ( sqrt ` A ) = 0 )
4 0aa 
 |-  0 e. AA
5 3 4 eqeltrdi 
 |-  ( A = 0 -> ( sqrt ` A ) e. AA )
6 5 adantl 
 |-  ( ( A e. QQ /\ A = 0 ) -> ( sqrt ` A ) e. AA )
7 sqrtnzqaa 
 |-  ( ( A e. QQ /\ A =/= 0 ) -> ( sqrt ` A ) e. AA )
8 6 7 pm2.61dane 
 |-  ( A e. QQ -> ( sqrt ` A ) e. AA )