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}}$

Step	Hyp	Ref	Expression
1		3cn	$⊢ 3 \in ℂ$
2		3nn0	$⊢ 3 \in ℕ_{0}$
3		expmul	$⊢ (3 \in ℂ \land 3 \in ℕ_{0} \land 3 \in ℕ_{0}) \to 3^{3 \cdot 3} = {(3^{3})}^{3}$
4	1 2 2 3	mp3an	$⊢ 3^{3 \cdot 3} = {(3^{3})}^{3}$
5		3re	$⊢ 3 \in ℝ$
6	2 2	nn0mulcli	$⊢ 3 \cdot 3 \in ℕ_{0}$
7	6	nn0zi	$⊢ 3 \cdot 3 \in ℤ$
8	2 2	nn0expcli	$⊢ 3^{3} \in ℕ_{0}$
9	8	nn0zi	$⊢ 3^{3} \in ℤ$
10		1lt3	$⊢ 1 < 3$
11	1	sqvali	$⊢ 3^{2} = 3 \cdot 3$
12		2z	$⊢ 2 \in ℤ$
13		3z	$⊢ 3 \in ℤ$
14		2lt3	$⊢ 2 < 3$
15		ltexp2a	$⊢ ((3 \in ℝ \land 2 \in ℤ \land 3 \in ℤ) \land (1 < 3 \land 2 < 3)) \to 3^{2} < 3^{3}$
16	10 14 15	mpanr12	$⊢ (3 \in ℝ \land 2 \in ℤ \land 3 \in ℤ) \to 3^{2} < 3^{3}$
17	5 12 13 16	mp3an	$⊢ 3^{2} < 3^{3}$
18	11 17	eqbrtrri	$⊢ 3 \cdot 3 < 3^{3}$
19		ltexp2a	$⊢ ((3 \in ℝ \land 3 \cdot 3 \in ℤ \land 3^{3} \in ℤ) \land (1 < 3 \land 3 \cdot 3 < 3^{3})) \to 3^{3 \cdot 3} < 3^{3^{3}}$
20	10 18 19	mpanr12	$⊢ (3 \in ℝ \land 3 \cdot 3 \in ℤ \land 3^{3} \in ℤ) \to 3^{3 \cdot 3} < 3^{3^{3}}$
21	5 7 9 20	mp3an	$⊢ 3^{3 \cdot 3} < 3^{3^{3}}$
22	4 21	eqbrtrri	$⊢ {(3^{3})}^{3} < 3^{3^{3}}$

Metamath Proof Explorer