Step |
Hyp |
Ref |
Expression |
1 |
|
3cn |
|- 3 e. CC |
2 |
|
3nn0 |
|- 3 e. NN0 |
3 |
|
expmul |
|- ( ( 3 e. CC /\ 3 e. NN0 /\ 3 e. NN0 ) -> ( 3 ^ ( 3 x. 3 ) ) = ( ( 3 ^ 3 ) ^ 3 ) ) |
4 |
1 2 2 3
|
mp3an |
|- ( 3 ^ ( 3 x. 3 ) ) = ( ( 3 ^ 3 ) ^ 3 ) |
5 |
|
3re |
|- 3 e. RR |
6 |
2 2
|
nn0mulcli |
|- ( 3 x. 3 ) e. NN0 |
7 |
6
|
nn0zi |
|- ( 3 x. 3 ) e. ZZ |
8 |
2 2
|
nn0expcli |
|- ( 3 ^ 3 ) e. NN0 |
9 |
8
|
nn0zi |
|- ( 3 ^ 3 ) e. ZZ |
10 |
|
1lt3 |
|- 1 < 3 |
11 |
1
|
sqvali |
|- ( 3 ^ 2 ) = ( 3 x. 3 ) |
12 |
|
2z |
|- 2 e. ZZ |
13 |
|
3z |
|- 3 e. ZZ |
14 |
|
2lt3 |
|- 2 < 3 |
15 |
|
ltexp2a |
|- ( ( ( 3 e. RR /\ 2 e. ZZ /\ 3 e. ZZ ) /\ ( 1 < 3 /\ 2 < 3 ) ) -> ( 3 ^ 2 ) < ( 3 ^ 3 ) ) |
16 |
10 14 15
|
mpanr12 |
|- ( ( 3 e. RR /\ 2 e. ZZ /\ 3 e. ZZ ) -> ( 3 ^ 2 ) < ( 3 ^ 3 ) ) |
17 |
5 12 13 16
|
mp3an |
|- ( 3 ^ 2 ) < ( 3 ^ 3 ) |
18 |
11 17
|
eqbrtrri |
|- ( 3 x. 3 ) < ( 3 ^ 3 ) |
19 |
|
ltexp2a |
|- ( ( ( 3 e. RR /\ ( 3 x. 3 ) e. ZZ /\ ( 3 ^ 3 ) e. ZZ ) /\ ( 1 < 3 /\ ( 3 x. 3 ) < ( 3 ^ 3 ) ) ) -> ( 3 ^ ( 3 x. 3 ) ) < ( 3 ^ ( 3 ^ 3 ) ) ) |
20 |
10 18 19
|
mpanr12 |
|- ( ( 3 e. RR /\ ( 3 x. 3 ) e. ZZ /\ ( 3 ^ 3 ) e. ZZ ) -> ( 3 ^ ( 3 x. 3 ) ) < ( 3 ^ ( 3 ^ 3 ) ) ) |
21 |
5 7 9 20
|
mp3an |
|- ( 3 ^ ( 3 x. 3 ) ) < ( 3 ^ ( 3 ^ 3 ) ) |
22 |
4 21
|
eqbrtrri |
|- ( ( 3 ^ 3 ) ^ 3 ) < ( 3 ^ ( 3 ^ 3 ) ) |