Theorem ex-sqrt

Description: Example for df-sqrt . (Contributed by AV, 4-Sep-2021)

	Ref	Expression
Assertion	ex-sqrt	$$⊢\sqrt{25}=5$$

Proof

Step	Hyp	Ref	Expression
1		ex-exp	$$⊢\left(5^2=25\wedge {\left(-3\right)}^{-2}=\frac{1}{9}\right)$$
2	1	simpli	$$⊢5^2=25$$
3	2	fveq2i	$$⊢\sqrt{5^2}=\sqrt{25}$$
4		5re	$$⊢5\in ℝ$$
5		0re	$$⊢0\in ℝ$$
6		5pos	$$⊢0<5$$
7	5 4 6	ltleii	$$⊢0\le 5$$
8		sqrtsq	$$⊢\left(5\in ℝ\wedge 0\le 5\right)\to \sqrt{5^2}=5$$
9	4 7 8	mp2an	$$⊢\sqrt{5^2}=5$$
10	3 9	eqtr3i	$$⊢\sqrt{25}=5$$