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

Metamath Proof Explorer

Theorem ltexp2rd

Description: The power of a positive number less than 1 decreases as its exponent increases. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses rpexpcld.1 ⊢ φ → A ∈ ℝ +
rpexpcld.2 ⊢ φ → N ∈ ℤ
ltexp2rd.3 ⊢ φ → M ∈ ℤ
ltexp2rd.4 ⊢ φ → A < 1
Assertion ltexp2rd ⊢ φ → M < N ↔ A N < A M

Proof

Step Hyp Ref Expression
1 rpexpcld.1 ⊢ φ → A ∈ ℝ +
2 rpexpcld.2 ⊢ φ → N ∈ ℤ
3 ltexp2rd.3 ⊢ φ → M ∈ ℤ
4 ltexp2rd.4 ⊢ φ → A < 1
5 ltexp2r ⊢ A ∈ ℝ + ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ A < 1 → M < N ↔ A N < A M
6 1 3 2 4 5 syl31anc ⊢ φ → M < N ↔ A N < A M