This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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