Step |
Hyp |
Ref |
Expression |
1 |
|
3ancomb |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ↔ ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) |
2 |
|
ltexp2 |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ 1 < 𝐴 ) → ( 𝑁 < 𝑀 ↔ ( 𝐴 ↑ 𝑁 ) < ( 𝐴 ↑ 𝑀 ) ) ) |
3 |
1 2
|
sylanb |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → ( 𝑁 < 𝑀 ↔ ( 𝐴 ↑ 𝑁 ) < ( 𝐴 ↑ 𝑀 ) ) ) |
4 |
3
|
notbid |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → ( ¬ 𝑁 < 𝑀 ↔ ¬ ( 𝐴 ↑ 𝑁 ) < ( 𝐴 ↑ 𝑀 ) ) ) |
5 |
|
simpl2 |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → 𝑀 ∈ ℤ ) |
6 |
|
simpl3 |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → 𝑁 ∈ ℤ ) |
7 |
|
zre |
⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ ) |
8 |
|
zre |
⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ ) |
9 |
|
lenlt |
⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 ≤ 𝑁 ↔ ¬ 𝑁 < 𝑀 ) ) |
10 |
7 8 9
|
syl2an |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ≤ 𝑁 ↔ ¬ 𝑁 < 𝑀 ) ) |
11 |
5 6 10
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → ( 𝑀 ≤ 𝑁 ↔ ¬ 𝑁 < 𝑀 ) ) |
12 |
|
simpl1 |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → 𝐴 ∈ ℝ ) |
13 |
|
0red |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → 0 ∈ ℝ ) |
14 |
|
1red |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → 1 ∈ ℝ ) |
15 |
|
0lt1 |
⊢ 0 < 1 |
16 |
15
|
a1i |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → 0 < 1 ) |
17 |
|
simpr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → 1 < 𝐴 ) |
18 |
13 14 12 16 17
|
lttrd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → 0 < 𝐴 ) |
19 |
18
|
gt0ne0d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → 𝐴 ≠ 0 ) |
20 |
|
reexpclz |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ∧ 𝑀 ∈ ℤ ) → ( 𝐴 ↑ 𝑀 ) ∈ ℝ ) |
21 |
12 19 5 20
|
syl3anc |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → ( 𝐴 ↑ 𝑀 ) ∈ ℝ ) |
22 |
|
reexpclz |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℝ ) |
23 |
12 19 6 22
|
syl3anc |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℝ ) |
24 |
21 23
|
lenltd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → ( ( 𝐴 ↑ 𝑀 ) ≤ ( 𝐴 ↑ 𝑁 ) ↔ ¬ ( 𝐴 ↑ 𝑁 ) < ( 𝐴 ↑ 𝑀 ) ) ) |
25 |
4 11 24
|
3bitr4d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝐴 ↑ 𝑀 ) ≤ ( 𝐴 ↑ 𝑁 ) ) ) |