Theorem sq45

Description: 45 squared is 2025. (Contributed by SN, 30-Mar-2025)

	Ref	Expression
Assertion	sq45	⊢ ( ; 4 5 ↑ 2 ) = ; ; ; 2 0 2 5

Proof

Step	Hyp	Ref	Expression
1		4nn0	⊢ 4 ∈ ℕ0
2		5nn0	⊢ 5 ∈ ℕ0
3	1 2	deccl	⊢ ; 4 5 ∈ ℕ0
4	3	nn0cni	⊢ ; 4 5 ∈ ℂ
5	4	sqvali	⊢ ( ; 4 5 ↑ 2 ) = ( ; 4 5 · ; 4 5 )
6		4p1e5	⊢ ( 4 + 1 ) = 5
7		4t5e20	⊢ ( 4 · 5 ) = ; 2 0
8	1 6 7	sqn5ii	⊢ ( ; 4 5 · ; 4 5 ) = ; ; ; 2 0 2 5
9	5 8	eqtri	⊢ ( ; 4 5 ↑ 2 ) = ; ; ; 2 0 2 5