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		2t4e8	$$⊢2\cdot 4=8$$
16	14 15	oveq12i	$$⊢4^2+2\cdot 4=16+8$$
17		1nn0	$$⊢1\in {\mathbb{N}}_0$$
18		6nn0	$$⊢6\in {\mathbb{N}}_0$$
19		8nn0	$$⊢8\in {\mathbb{N}}_0$$
20		eqid	$$⊢16=16$$
21		1p1e2	$$⊢1+1=2$$
22		6cn	$$⊢6\in ℂ$$
23		8p6e14	$$⊢8+6=14$$
24	10 22 23	addcomli	$$⊢6+8=14$$
25	17 18 19 20 21 7 24	decaddci	$$⊢16+8=24$$
26	16 25	eqtri	$$⊢4^2+2\cdot 4=24$$
27	6 7 8 26	decsuc	$$⊢4^2+2\cdot 4+1=25$$
28	5 27	eqtri	$$⊢{\left(4+1\right)}^2=25$$
29	2 28	eqtri	$$⊢5^2=25$$
30		3cn	$$⊢3\in ℂ$$
31	30	negcli	$$⊢-3\in ℂ$$
32		expneg	$$⊢\left(-3\in ℂ\wedge 2\in {\mathbb{N}}_0\right)\to {\left(-3\right)}^{-2}=\frac{1}{{\left(-3\right)}^2}$$
33	31 6 32	mp2an	$$⊢{\left(-3\right)}^{-2}=\frac{1}{{\left(-3\right)}^2}$$
34		sqneg	$$⊢3\in ℂ\to {\left(-3\right)}^2=3^2$$
35	30 34	ax-mp	$$⊢{\left(-3\right)}^2=3^2$$
36		sq3	$$⊢3^2=9$$
37	35 36	eqtri	$$⊢{\left(-3\right)}^2=9$$
38	37	oveq2i	$$⊢\frac{1}{{\left(-3\right)}^2}=\frac{1}{9}$$
39	33 38	eqtri	$$⊢{\left(-3\right)}^{-2}=\frac{1}{9}$$
40	29 39	pm3.2i	$$⊢\left(5^2=25\wedge {\left(-3\right)}^{-2}=\frac{1}{9}\right)$$