Metamath Proof Explorer


Theorem msqsqrtd

Description: Square root theorem. Theorem I.35 of Apostol p. 29. (Contributed by Mario Carneiro, 29-May-2016)

Ref Expression
Hypothesis abscld.1 φA
Assertion msqsqrtd φAA=A

Proof

Step Hyp Ref Expression
1 abscld.1 φA
2 1 sqrtcld φA
3 2 sqvald φA2=AA
4 1 sqsqrtd φA2=A
5 3 4 eqtr3d φAA=A