# Metamath Proof Explorer

## 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 {ℕ}_{0}$
7 4nn0 ${⊢}4\in {ℕ}_{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 {ℕ}_{0}$
19 6nn0 ${⊢}6\in {ℕ}_{0}$
20 8nn0 ${⊢}8\in {ℕ}_{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 {ℕ}_{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)$