Theorem ex-sqrt

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

	Ref	Expression
Assertion	ex-sqrt	|- ( sqrt ` ; 2 5 ) = 5

Proof

Step	Hyp	Ref	Expression
1		ex-exp	|- ( ( 5 ^ 2 ) = ; 2 5 /\ ( -u 3 ^ -u 2 ) = ( 1 / 9 ) )
2	1	simpli	|- ( 5 ^ 2 ) = ; 2 5
3	2	fveq2i	|- ( sqrt ` ( 5 ^ 2 ) ) = ( sqrt ` ; 2 5 )
4		5re	|- 5 e. RR
5		0re	|- 0 e. RR
6		5pos	|- 0 < 5
7	5 4 6	ltleii	|- 0 <_ 5
8		sqrtsq	|- ( ( 5 e. RR /\ 0 <_ 5 ) -> ( sqrt ` ( 5 ^ 2 ) ) = 5 )
9	4 7 8	mp2an	|- ( sqrt ` ( 5 ^ 2 ) ) = 5
10	3 9	eqtr3i	|- ( sqrt ` ; 2 5 ) = 5