Theorem ex-exp

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

	Ref	Expression
Assertion	ex-exp	⊢ ( ( 5 ↑ 2 ) = ; 2 5 ∧ ( - 3 ↑ - 2 ) = ( 1 / 9 ) )

Proof

Step	Hyp	Ref	Expression
1		df-5	⊢ 5 = ( 4 + 1 )
2	1	oveq1i	⊢ ( 5 ↑ 2 ) = ( ( 4 + 1 ) ↑ 2 )
3		4cn	⊢ 4 ∈ ℂ
4		binom21	⊢ ( 4 ∈ ℂ → ( ( 4 + 1 ) ↑ 2 ) = ( ( ( 4 ↑ 2 ) + ( 2 · 4 ) ) + 1 ) )
5	3 4	ax-mp	⊢ ( ( 4 + 1 ) ↑ 2 ) = ( ( ( 4 ↑ 2 ) + ( 2 · 4 ) ) + 1 )
6		2nn0	⊢ 2 ∈ ℕ0
7		4nn0	⊢ 4 ∈ ℕ0
8		4p1e5	⊢ ( 4 + 1 ) = 5
9		sq4e2t8	⊢ ( 4 ↑ 2 ) = ( 2 · 8 )
10		8cn	⊢ 8 ∈ ℂ
11		2cn	⊢ 2 ∈ ℂ
12		8t2e16	⊢ ( 8 · 2 ) = ; 1 6
13	10 11 12	mulcomli	⊢ ( 2 · 8 ) = ; 1 6
14	9 13	eqtri	⊢ ( 4 ↑ 2 ) = ; 1 6
15		2t4e8	⊢ ( 2 · 4 ) = 8
16	14 15	oveq12i	⊢ ( ( 4 ↑ 2 ) + ( 2 · 4 ) ) = ( ; 1 6 + 8 )
17		1nn0	⊢ 1 ∈ ℕ0
18		6nn0	⊢ 6 ∈ ℕ0
19		8nn0	⊢ 8 ∈ ℕ0
20		eqid	⊢ ; 1 6 = ; 1 6
21		1p1e2	⊢ ( 1 + 1 ) = 2
22		6cn	⊢ 6 ∈ ℂ
23		8p6e14	⊢ ( 8 + 6 ) = ; 1 4
24	10 22 23	addcomli	⊢ ( 6 + 8 ) = ; 1 4
25	17 18 19 20 21 7 24	decaddci	⊢ ( ; 1 6 + 8 ) = ; 2 4
26	16 25	eqtri	⊢ ( ( 4 ↑ 2 ) + ( 2 · 4 ) ) = ; 2 4
27	6 7 8 26	decsuc	⊢ ( ( ( 4 ↑ 2 ) + ( 2 · 4 ) ) + 1 ) = ; 2 5
28	5 27	eqtri	⊢ ( ( 4 + 1 ) ↑ 2 ) = ; 2 5
29	2 28	eqtri	⊢ ( 5 ↑ 2 ) = ; 2 5
30		3cn	⊢ 3 ∈ ℂ
31	30	negcli	⊢ - 3 ∈ ℂ
32		expneg	⊢ ( ( - 3 ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( - 3 ↑ - 2 ) = ( 1 / ( - 3 ↑ 2 ) ) )
33	31 6 32	mp2an	⊢ ( - 3 ↑ - 2 ) = ( 1 / ( - 3 ↑ 2 ) )
34		sqneg	⊢ ( 3 ∈ ℂ → ( - 3 ↑ 2 ) = ( 3 ↑ 2 ) )
35	30 34	ax-mp	⊢ ( - 3 ↑ 2 ) = ( 3 ↑ 2 )
36		sq3	⊢ ( 3 ↑ 2 ) = 9
37	35 36	eqtri	⊢ ( - 3 ↑ 2 ) = 9
38	37	oveq2i	⊢ ( 1 / ( - 3 ↑ 2 ) ) = ( 1 / 9 )
39	33 38	eqtri	⊢ ( - 3 ↑ - 2 ) = ( 1 / 9 )
40	29 39	pm3.2i	⊢ ( ( 5 ↑ 2 ) = ; 2 5 ∧ ( - 3 ↑ - 2 ) = ( 1 / 9 ) )