Metamath Proof Explorer


Theorem expnass

Description: A counterexample showing that exponentiation is not associative. (Contributed by Stefan Allan and Gérard Lang, 21-Sep-2010)

Ref Expression
Assertion expnass
|- ( ( 3 ^ 3 ) ^ 3 ) < ( 3 ^ ( 3 ^ 3 ) )

Proof

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