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