| Step |
Hyp |
Ref |
Expression |
| 1 |
|
3p2e5 |
|- ( 3 + 2 ) = 5 |
| 2 |
1
|
eqcomi |
|- 5 = ( 3 + 2 ) |
| 3 |
2
|
oveq2i |
|- ( 2 ^ 5 ) = ( 2 ^ ( 3 + 2 ) ) |
| 4 |
|
2cn |
|- 2 e. CC |
| 5 |
|
3nn0 |
|- 3 e. NN0 |
| 6 |
|
2nn0 |
|- 2 e. NN0 |
| 7 |
|
expadd |
|- ( ( 2 e. CC /\ 3 e. NN0 /\ 2 e. NN0 ) -> ( 2 ^ ( 3 + 2 ) ) = ( ( 2 ^ 3 ) x. ( 2 ^ 2 ) ) ) |
| 8 |
4 5 6 7
|
mp3an |
|- ( 2 ^ ( 3 + 2 ) ) = ( ( 2 ^ 3 ) x. ( 2 ^ 2 ) ) |
| 9 |
|
cu2 |
|- ( 2 ^ 3 ) = 8 |
| 10 |
|
sq2 |
|- ( 2 ^ 2 ) = 4 |
| 11 |
9 10
|
oveq12i |
|- ( ( 2 ^ 3 ) x. ( 2 ^ 2 ) ) = ( 8 x. 4 ) |
| 12 |
8 11
|
eqtri |
|- ( 2 ^ ( 3 + 2 ) ) = ( 8 x. 4 ) |
| 13 |
3 12
|
eqtri |
|- ( 2 ^ 5 ) = ( 8 x. 4 ) |
| 14 |
|
8t4e32 |
|- ( 8 x. 4 ) = ; 3 2 |
| 15 |
13 14
|
eqtri |
|- ( 2 ^ 5 ) = ; 3 2 |