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