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 ⊢333<333

Proof

Step Hyp Ref Expression
1 3cn ⊢3∈ℂ
2 3nn0 ⊢3∈ℕ0
3 expmul ⊢3∈ℂ∧3∈ℕ0∧3∈ℕ0→33⋅3=333
4 1 2 2 3 mp3an ⊢33⋅3=333
5 3re ⊢3∈ℝ
6 2 2 nn0mulcli ⊢3⋅3∈ℕ0
7 6 nn0zi ⊢3⋅3∈ℤ
8 2 2 nn0expcli ⊢33∈ℕ0
9 8 nn0zi ⊢33∈ℤ
10 1lt3 ⊢1<3
11 1 sqvali ⊢32=3⋅3
12 2z ⊢2∈ℤ
13 3z ⊢3∈ℤ
14 2lt3 ⊢2<3
15 ltexp2a ⊢3∈ℝ∧2∈ℤ∧3∈ℤ∧1<3∧2<3→32<33
16 10 14 15 mpanr12 ⊢3∈ℝ∧2∈ℤ∧3∈ℤ→32<33
17 5 12 13 16 mp3an ⊢32<33
18 11 17 eqbrtrri ⊢3⋅3<33
19 ltexp2a ⊢3∈ℝ∧3⋅3∈ℤ∧33∈ℤ∧1<3∧3⋅3<33→33⋅3<333
20 10 18 19 mpanr12 ⊢3∈ℝ∧3⋅3∈ℤ∧33∈ℤ→33⋅3<333
21 5 7 9 20 mp3an ⊢33⋅3<333
22 4 21 eqbrtrri ⊢333<333