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