Theorem 2exp5

Description: Two to the fifth power is 32. (Contributed by AV, 16-Aug-2021)

	Ref	Expression
Assertion	2exp5	⊢ ( 2 ↑ 5 ) = ; 3 2

Proof

Step	Hyp	Ref	Expression
1		3p2e5	⊢ ( 3 + 2 ) = 5
2	1	eqcomi	⊢ 5 = ( 3 + 2 )
3	2	oveq2i	⊢ ( 2 ↑ 5 ) = ( 2 ↑ ( 3 + 2 ) )
4		2cn	⊢ 2 ∈ ℂ
5		3nn0	⊢ 3 ∈ ℕ0
6		2nn0	⊢ 2 ∈ ℕ0
7		expadd	⊢ ( ( 2 ∈ ℂ ∧ 3 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) → ( 2 ↑ ( 3 + 2 ) ) = ( ( 2 ↑ 3 ) · ( 2 ↑ 2 ) ) )
8	4 5 6 7	mp3an	⊢ ( 2 ↑ ( 3 + 2 ) ) = ( ( 2 ↑ 3 ) · ( 2 ↑ 2 ) )
9		cu2	⊢ ( 2 ↑ 3 ) = 8
10		sq2	⊢ ( 2 ↑ 2 ) = 4
11	9 10	oveq12i	⊢ ( ( 2 ↑ 3 ) · ( 2 ↑ 2 ) ) = ( 8 · 4 )
12	8 11	eqtri	⊢ ( 2 ↑ ( 3 + 2 ) ) = ( 8 · 4 )
13	3 12	eqtri	⊢ ( 2 ↑ 5 ) = ( 8 · 4 )
14		8t4e32	⊢ ( 8 · 4 ) = ; 3 2
15	13 14	eqtri	⊢ ( 2 ↑ 5 ) = ; 3 2