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