Metamath Proof Explorer

Theorem ltexp2r

Description: The integer powers of a fixed positive real smaller than 1 decrease as the exponent increases. (Contributed by NM, 2-Aug-2006) (Revised by Mario Carneiro, 5-Jun-2014)

Ref Expression
Assertion ltexp2r ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐴 < 1 ) → ( 𝑀 < 𝑁 ↔ ( 𝐴 ↑ 𝑁 ) < ( 𝐴 ↑ 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 simpl1 ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐴 < 1 ) → 𝐴 ∈ ℝ+ )
2 1 rpcnd ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐴 < 1 ) → 𝐴 ∈ ℂ )
3 1 rpne0d ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐴 < 1 ) → 𝐴 ≠ 0 )
4 simpl2 ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐴 < 1 ) → 𝑀 ∈ ℤ )
5 exprec ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑀 ∈ ℤ ) → ( ( 1 / 𝐴 ) ↑ 𝑀 ) = ( 1 / ( 𝐴 ↑ 𝑀 ) ) )
6 2 3 4 5 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐴 < 1 ) → ( ( 1 / 𝐴 ) ↑ 𝑀 ) = ( 1 / ( 𝐴 ↑ 𝑀 ) ) )
7 simpl3 ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐴 < 1 ) → 𝑁 ∈ ℤ )
8 exprec ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( ( 1 / 𝐴 ) ↑ 𝑁 ) = ( 1 / ( 𝐴 ↑ 𝑁 ) ) )
9 2 3 7 8 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐴 < 1 ) → ( ( 1 / 𝐴 ) ↑ 𝑁 ) = ( 1 / ( 𝐴 ↑ 𝑁 ) ) )
10 6 9 breq12d ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐴 < 1 ) → ( ( ( 1 / 𝐴 ) ↑ 𝑀 ) < ( ( 1 / 𝐴 ) ↑ 𝑁 ) ↔ ( 1 / ( 𝐴 ↑ 𝑀 ) ) < ( 1 / ( 𝐴 ↑ 𝑁 ) ) ) )
11 1 rprecred ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐴 < 1 ) → ( 1 / 𝐴 ) ∈ ℝ )
12 simpr ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐴 < 1 ) → 𝐴 < 1 )
13 1 reclt1d ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐴 < 1 ) → ( 𝐴 < 1 ↔ 1 < ( 1 / 𝐴 ) ) )
14 12 13 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐴 < 1 ) → 1 < ( 1 / 𝐴 ) )
15 ltexp2 ⊢ ( ( ( ( 1 / 𝐴 ) ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < ( 1 / 𝐴 ) ) → ( 𝑀 < 𝑁 ↔ ( ( 1 / 𝐴 ) ↑ 𝑀 ) < ( ( 1 / 𝐴 ) ↑ 𝑁 ) ) )
16 11 4 7 14 15 syl31anc ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐴 < 1 ) → ( 𝑀 < 𝑁 ↔ ( ( 1 / 𝐴 ) ↑ 𝑀 ) < ( ( 1 / 𝐴 ) ↑ 𝑁 ) ) )
17 rpexpcl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℝ+ )
18 1 7 17 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐴 < 1 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℝ+ )
19 rpexpcl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑀 ∈ ℤ ) → ( 𝐴 ↑ 𝑀 ) ∈ ℝ+ )
20 1 4 19 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐴 < 1 ) → ( 𝐴 ↑ 𝑀 ) ∈ ℝ+ )
21 18 20 ltrecd ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐴 < 1 ) → ( ( 𝐴 ↑ 𝑁 ) < ( 𝐴 ↑ 𝑀 ) ↔ ( 1 / ( 𝐴 ↑ 𝑀 ) ) < ( 1 / ( 𝐴 ↑ 𝑁 ) ) ) )
22 10 16 21 3bitr4d ⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐴 < 1 ) → ( 𝑀 < 𝑁 ↔ ( 𝐴 ↑ 𝑁 ) < ( 𝐴 ↑ 𝑀 ) ) )