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		4t2e8	⊢ ( 4 · 2 ) = 8
16	3 11 15	mulcomli	⊢ ( 2 · 4 ) = 8
17	14 16	oveq12i	⊢ ( ( 4 ↑ 2 ) + ( 2 · 4 ) ) = ( ; 1 6 + 8 )
18		1nn0	⊢ 1 ∈ ℕ0
19		6nn0	⊢ 6 ∈ ℕ0
20		8nn0	⊢ 8 ∈ ℕ0
21		eqid	⊢ ; 1 6 = ; 1 6
22		1p1e2	⊢ ( 1 + 1 ) = 2
23		6cn	⊢ 6 ∈ ℂ
24		8p6e14	⊢ ( 8 + 6 ) = ; 1 4
25	10 23 24	addcomli	⊢ ( 6 + 8 ) = ; 1 4
26	18 19 20 21 22 7 25	decaddci	⊢ ( ; 1 6 + 8 ) = ; 2 4
27	17 26	eqtri	⊢ ( ( 4 ↑ 2 ) + ( 2 · 4 ) ) = ; 2 4
28	6 7 8 27	decsuc	⊢ ( ( ( 4 ↑ 2 ) + ( 2 · 4 ) ) + 1 ) = ; 2 5
29	5 28	eqtri	⊢ ( ( 4 + 1 ) ↑ 2 ) = ; 2 5
30	2 29	eqtri	⊢ ( 5 ↑ 2 ) = ; 2 5
31		3cn	⊢ 3 ∈ ℂ
32	31	negcli	⊢ - 3 ∈ ℂ
33		expneg	⊢ ( ( - 3 ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( - 3 ↑ - 2 ) = ( 1 / ( - 3 ↑ 2 ) ) )
34	32 6 33	mp2an	⊢ ( - 3 ↑ - 2 ) = ( 1 / ( - 3 ↑ 2 ) )
35		sqneg	⊢ ( 3 ∈ ℂ → ( - 3 ↑ 2 ) = ( 3 ↑ 2 ) )
36	31 35	ax-mp	⊢ ( - 3 ↑ 2 ) = ( 3 ↑ 2 )
37		sq3	⊢ ( 3 ↑ 2 ) = 9
38	36 37	eqtri	⊢ ( - 3 ↑ 2 ) = 9
39	38	oveq2i	⊢ ( 1 / ( - 3 ↑ 2 ) ) = ( 1 / 9 )
40	34 39	eqtri	⊢ ( - 3 ↑ - 2 ) = ( 1 / 9 )
41	30 40	pm3.2i	⊢ ( ( 5 ↑ 2 ) = ; 2 5 ∧ ( - 3 ↑ - 2 ) = ( 1 / 9 ) )