theorem proved term proof

`pow_le_pow_iff_of_one_lt`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 650private theorem pow_le_pow_iff_of_one_lt {γ : ℝ} (hγ : 1 < γ) (n m : Nat) :
 651    γ ^ n ≤ γ ^ m ↔ n ≤ m := by

proof body

Term-mode proof.

 652  constructor
 653  · intro h
 654    by_contra hlt
 655    push_neg at hlt
 656    have : γ ^ m < γ ^ n := pow_lt_pow_right₀ hγ hlt
 657    linarith
 658  · intro h
 659    exact pow_le_pow_right₀ (le_of_lt hγ) h
 660
 661/-- For `γ > 1`, `γⁿ < γᵐ ↔ n < m` on `Nat`. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

embed_le_iff_of_one_lt in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use