This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )