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 /\ ( -u 3 ^ -u 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 e. CC
4 binom21 
 |-  ( 4 e. CC -> ( ( 4 + 1 ) ^ 2 ) = ( ( ( 4 ^ 2 ) + ( 2 x. 4 ) ) + 1 ) )
5 3 4 ax-mp 
 |-  ( ( 4 + 1 ) ^ 2 ) = ( ( ( 4 ^ 2 ) + ( 2 x. 4 ) ) + 1 )
6 2nn0 
 |-  2 e. NN0
7 4nn0 
 |-  4 e. NN0
8 4p1e5 
 |-  ( 4 + 1 ) = 5
9 sq4e2t8 
 |-  ( 4 ^ 2 ) = ( 2 x. 8 )
10 8cn 
 |-  8 e. CC
11 2cn 
 |-  2 e. CC
12 8t2e16 
 |-  ( 8 x. 2 ) = ; 1 6
13 10 11 12 mulcomli 
 |-  ( 2 x. 8 ) = ; 1 6
14 9 13 eqtri 
 |-  ( 4 ^ 2 ) = ; 1 6
15 4t2e8 
 |-  ( 4 x. 2 ) = 8
16 3 11 15 mulcomli 
 |-  ( 2 x. 4 ) = 8
17 14 16 oveq12i 
 |-  ( ( 4 ^ 2 ) + ( 2 x. 4 ) ) = ( ; 1 6 + 8 )
18 1nn0 
 |-  1 e. NN0
19 6nn0 
 |-  6 e. NN0
20 8nn0 
 |-  8 e. NN0
21 eqid 
 |-  ; 1 6 = ; 1 6
22 1p1e2 
 |-  ( 1 + 1 ) = 2
23 6cn 
 |-  6 e. CC
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 x. 4 ) ) = ; 2 4
28 6 7 8 27 decsuc 
 |-  ( ( ( 4 ^ 2 ) + ( 2 x. 4 ) ) + 1 ) = ; 2 5
29 5 28 eqtri 
 |-  ( ( 4 + 1 ) ^ 2 ) = ; 2 5
30 2 29 eqtri 
 |-  ( 5 ^ 2 ) = ; 2 5
31 3cn 
 |-  3 e. CC
32 31 negcli 
 |-  -u 3 e. CC
33 expneg 
 |-  ( ( -u 3 e. CC /\ 2 e. NN0 ) -> ( -u 3 ^ -u 2 ) = ( 1 / ( -u 3 ^ 2 ) ) )
34 32 6 33 mp2an 
 |-  ( -u 3 ^ -u 2 ) = ( 1 / ( -u 3 ^ 2 ) )
35 sqneg 
 |-  ( 3 e. CC -> ( -u 3 ^ 2 ) = ( 3 ^ 2 ) )
36 31 35 ax-mp 
 |-  ( -u 3 ^ 2 ) = ( 3 ^ 2 )
37 sq3 
 |-  ( 3 ^ 2 ) = 9
38 36 37 eqtri 
 |-  ( -u 3 ^ 2 ) = 9
39 38 oveq2i 
 |-  ( 1 / ( -u 3 ^ 2 ) ) = ( 1 / 9 )
40 34 39 eqtri 
 |-  ( -u 3 ^ -u 2 ) = ( 1 / 9 )
41 30 40 pm3.2i 
 |-  ( ( 5 ^ 2 ) = ; 2 5 /\ ( -u 3 ^ -u 2 ) = ( 1 / 9 ) )