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 ∈ ℂ
2 3nn0 3 ∈ ℕ0
3 expmul ( ( 3 ∈ ℂ ∧ 3 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) → ( 3 ↑ ( 3 · 3 ) ) = ( ( 3 ↑ 3 ) ↑ 3 ) )
4 1 2 2 3 mp3an ( 3 ↑ ( 3 · 3 ) ) = ( ( 3 ↑ 3 ) ↑ 3 )
5 3re 3 ∈ ℝ
6 2 2 nn0mulcli ( 3 · 3 ) ∈ ℕ0
7 6 nn0zi ( 3 · 3 ) ∈ ℤ
8 2 2 nn0expcli ( 3 ↑ 3 ) ∈ ℕ0
9 8 nn0zi ( 3 ↑ 3 ) ∈ ℤ
10 1lt3 1 < 3
11 1 sqvali ( 3 ↑ 2 ) = ( 3 · 3 )
12 2z 2 ∈ ℤ
13 3z 3 ∈ ℤ
14 2lt3 2 < 3
15 ltexp2a ( ( ( 3 ∈ ℝ ∧ 2 ∈ ℤ ∧ 3 ∈ ℤ ) ∧ ( 1 < 3 ∧ 2 < 3 ) ) → ( 3 ↑ 2 ) < ( 3 ↑ 3 ) )
16 10 14 15 mpanr12 ( ( 3 ∈ ℝ ∧ 2 ∈ ℤ ∧ 3 ∈ ℤ ) → ( 3 ↑ 2 ) < ( 3 ↑ 3 ) )
17 5 12 13 16 mp3an ( 3 ↑ 2 ) < ( 3 ↑ 3 )
18 11 17 eqbrtrri ( 3 · 3 ) < ( 3 ↑ 3 )
19 ltexp2a ( ( ( 3 ∈ ℝ ∧ ( 3 · 3 ) ∈ ℤ ∧ ( 3 ↑ 3 ) ∈ ℤ ) ∧ ( 1 < 3 ∧ ( 3 · 3 ) < ( 3 ↑ 3 ) ) ) → ( 3 ↑ ( 3 · 3 ) ) < ( 3 ↑ ( 3 ↑ 3 ) ) )
20 10 18 19 mpanr12 ( ( 3 ∈ ℝ ∧ ( 3 · 3 ) ∈ ℤ ∧ ( 3 ↑ 3 ) ∈ ℤ ) → ( 3 ↑ ( 3 · 3 ) ) < ( 3 ↑ ( 3 ↑ 3 ) ) )
21 5 7 9 20 mp3an ( 3 ↑ ( 3 · 3 ) ) < ( 3 ↑ ( 3 ↑ 3 ) )
22 4 21 eqbrtrri ( ( 3 ↑ 3 ) ↑ 3 ) < ( 3 ↑ ( 3 ↑ 3 ) )