Theorem ex-sqrt

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

	Ref	Expression
Assertion	ex-sqrt	⊢ ( √ ‘ ; 2 5 ) = 5

Proof

Step	Hyp	Ref	Expression
1		ex-exp	⊢ ( ( 5 ↑ 2 ) = ; 2 5 ∧ ( - 3 ↑ - 2 ) = ( 1 / 9 ) )
2	1	simpli	⊢ ( 5 ↑ 2 ) = ; 2 5
3	2	fveq2i	⊢ ( √ ‘ ( 5 ↑ 2 ) ) = ( √ ‘ ; 2 5 )
4		5re	⊢ 5 ∈ ℝ
5		0re	⊢ 0 ∈ ℝ
6		5pos	⊢ 0 < 5
7	5 4 6	ltleii	⊢ 0 ≤ 5
8		sqrtsq	⊢ ( ( 5 ∈ ℝ ∧ 0 ≤ 5 ) → ( √ ‘ ( 5 ↑ 2 ) ) = 5 )
9	4 7 8	mp2an	⊢ ( √ ‘ ( 5 ↑ 2 ) ) = 5
10	3 9	eqtr3i	⊢ ( √ ‘ ; 2 5 ) = 5