Theorem ex-exp

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

	Ref	Expression
Assertion	ex-exp	$$⊢\left(5^2=25\wedge {\left(-3\right)}^{-2}=\frac{1}{9}\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-5	$$⊢5=4+1$$
2	1	oveq1i	$$⊢5^2={\left(4+1\right)}^2$$
3		4cn	$$⊢4\in ℂ$$
4		binom21	$$⊢4\in ℂ\to {\left(4+1\right)}^2=4^2+2\cdot 4+1$$
5	3 4	ax-mp	$$⊢{\left(4+1\right)}^2=4^2+2\cdot 4+1$$
6		2nn0	$$⊢2\in {\mathbb{N}}_0$$
7		4nn0	$$⊢4\in {\mathbb{N}}_0$$
8		4p1e5	$$⊢4+1=5$$
9		sq4e2t8	$$⊢4^2=2\cdot 8$$
10		8cn	$$⊢8\in ℂ$$
11		2cn	$$⊢2\in ℂ$$
12		8t2e16	$$⊢8\cdot 2=16$$
13	10 11 12	mulcomli	$$⊢2\cdot 8=16$$
14	9 13	eqtri	$$⊢4^2=16$$
15		4t2e8	$$⊢4\cdot 2=8$$
16	3 11 15	mulcomli	$$⊢2\cdot 4=8$$
17	14 16	oveq12i	$$⊢4^2+2\cdot 4=16+8$$
18		1nn0	$$⊢1\in {\mathbb{N}}_0$$
19		6nn0	$$⊢6\in {\mathbb{N}}_0$$
20		8nn0	$$⊢8\in {\mathbb{N}}_0$$
21		eqid	$$⊢16=16$$
22		1p1e2	$$⊢1+1=2$$
23		6cn	$$⊢6\in ℂ$$
24		8p6e14	$$⊢8+6=14$$
25	10 23 24	addcomli	$$⊢6+8=14$$
26	18 19 20 21 22 7 25	decaddci	$$⊢16+8=24$$
27	17 26	eqtri	$$⊢4^2+2\cdot 4=24$$
28	6 7 8 27	decsuc	$$⊢4^2+2\cdot 4+1=25$$
29	5 28	eqtri	$$⊢{\left(4+1\right)}^2=25$$
30	2 29	eqtri	$$⊢5^2=25$$
31		3cn	$$⊢3\in ℂ$$
32	31	negcli	$$⊢-3\in ℂ$$
33		expneg	$$⊢\left(-3\in ℂ\wedge 2\in {\mathbb{N}}_0\right)\to {\left(-3\right)}^{-2}=\frac{1}{{\left(-3\right)}^2}$$
34	32 6 33	mp2an	$$⊢{\left(-3\right)}^{-2}=\frac{1}{{\left(-3\right)}^2}$$
35		sqneg	$$⊢3\in ℂ\to {\left(-3\right)}^2=3^2$$
36	31 35	ax-mp	$$⊢{\left(-3\right)}^2=3^2$$
37		sq3	$$⊢3^2=9$$
38	36 37	eqtri	$$⊢{\left(-3\right)}^2=9$$
39	38	oveq2i	$$⊢\frac{1}{{\left(-3\right)}^2}=\frac{1}{9}$$
40	34 39	eqtri	$$⊢{\left(-3\right)}^{-2}=\frac{1}{9}$$
41	30 40	pm3.2i	$$⊢\left(5^2=25\wedge {\left(-3\right)}^{-2}=\frac{1}{9}\right)$$