This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem leexp2ad

Description: Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses sqgt0d.1 ⊢ φ → A ∈ ℝ
leexp2ad.2 ⊢ φ → 1 ≤ A
leexp2ad.3 ⊢ φ → N ∈ ℤ ≥ M
Assertion leexp2ad ⊢ φ → A M ≤ A N

Proof

Step Hyp Ref Expression
1 sqgt0d.1 ⊢ φ → A ∈ ℝ
2 leexp2ad.2 ⊢ φ → 1 ≤ A
3 leexp2ad.3 ⊢ φ → N ∈ ℤ ≥ M
4 leexp2a ⊢ A ∈ ℝ ∧ 1 ≤ A ∧ N ∈ ℤ ≥ M → A M ≤ A N
5 1 2 3 4 syl3anc ⊢ φ → A M ≤ A N