This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ φ → A ⁢ A = A

Proof

Step Hyp Ref Expression
1 abscld.1 ⊢ φ → A ∈ ℂ
2 1 sqrtcld ⊢ φ → A ∈ ℂ
3 2 sqvald ⊢ φ → A 2 = A ⁢ A
4 1 sqsqrtd ⊢ φ → A 2 = A
5 3 4 eqtr3d ⊢ φ → A ⁢ A = A