[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 1 ≤ a
h : m ≤ n
⊢ a ^ m ≤ a ^ n
[PROOFSTEP]
have ha₀ : 0 < a := one_pos.trans_le ha
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 1 ≤ a
h : m ≤ n
ha₀ : 0 < a
⊢ a ^ m ≤ a ^ n
[PROOFSTEP]
lift n - m to ℕ using sub_nonneg.2 h with k hk
[GOAL]
case intro
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 1 ≤ a
h : m ≤ n
ha₀ : 0 < a
k : ℕ
hk : ↑k = n - m
⊢ a ^ m ≤ a ^ n
[PROOFSTEP]
calc
  a ^ m = a ^ m * 1 := (mul_one _).symm
  _ ≤ a ^ m * a ^ k := (mul_le_mul_of_nonneg_left (one_le_pow_of_one_le ha _) (zpow_nonneg ha₀.le _))
  _ = a ^ n := by rw [← zpow_ofNat, ← zpow_add₀ ha₀.ne', hk, add_sub_cancel'_right]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 1 ≤ a
h : m ≤ n
ha₀ : 0 < a
k : ℕ
hk : ↑k = n - m
⊢ a ^ m * a ^ k = a ^ n
[PROOFSTEP]
rw [← zpow_ofNat, ← zpow_add₀ ha₀.ne', hk, add_sub_cancel'_right]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
a✝ b c d e : α
m n✝ : ℤ
a : ℕ
h : 0 < a
n : ℤ
⊢ 0 < ↑a ^ n
[PROOFSTEP]
apply zpow_pos_of_pos
[GOAL]
case ha
α : Type u_1
inst✝ : LinearOrderedSemifield α
a✝ b c d e : α
m n✝ : ℤ
a : ℕ
h : 0 < a
n : ℤ
⊢ 0 < ↑a
[PROOFSTEP]
exact_mod_cast h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h₀ : 0 < a
h₁ : a ≠ 1
⊢ Injective ((fun x x_1 => x ^ x_1) a)
[PROOFSTEP]
rcases h₁.lt_or_lt with (H | H)
[GOAL]
case inl
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h₀ : 0 < a
h₁ : a ≠ 1
H : a < 1
⊢ Injective ((fun x x_1 => x ^ x_1) a)
[PROOFSTEP]
exact (zpow_strictAnti h₀ H).injective
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h₀ : 0 < a
h₁ : a ≠ 1
H : 1 < a
⊢ Injective ((fun x x_1 => x ^ x_1) a)
[PROOFSTEP]
exact (zpow_strictMono H).injective
[GOAL]
α : Type u_1
inst✝ : LinearOrderedSemifield α
a✝ b✝ c✝ d e : α
m n : ℤ
x : α
hx : 1 < x
a b c : ℤ
⊢ x ^ (-c) ≤ max (x ^ (-a)) (x ^ (-b)) ↔ min a b ≤ c
[PROOFSTEP]
simp_rw [le_max_iff, min_le_iff, zpow_le_iff_le hx, neg_le_neg_iff]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ b c d : α
n : ℤ
a : α
⊢ 0 ≤ a ^ 2
[PROOFSTEP]
convert zpow_bit0_nonneg a 1
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
h : a ≠ 0
⊢ 0 < a ^ 2
[PROOFSTEP]
convert zpow_bit0_pos h 1
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hn : n ≠ 0
⊢ 0 < a ^ bit0 n → a ≠ 0
[PROOFSTEP]
rintro h rfl
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
b c d : α
n : ℤ
hn : n ≠ 0
h : 0 < 0 ^ bit0 n
⊢ False
[PROOFSTEP]
refine' (zero_zpow _ _).not_gt h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
b c d : α
n : ℤ
hn : n ≠ 0
h : 0 < 0 ^ bit0 n
⊢ bit0 n ≠ 0
[PROOFSTEP]
rwa [bit0_ne_zero]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
h : a < 0
⊢ a ^ bit1 n < 0
[PROOFSTEP]
rw [bit1, zpow_add_one₀ h.ne]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
h : a < 0
⊢ a ^ bit0 n * a < 0
[PROOFSTEP]
exact mul_neg_of_pos_of_neg (zpow_bit0_pos h.ne _) h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
⊢ a ^ bit1 n ≤ 0 ↔ a ≤ 0
[PROOFSTEP]
rw [le_iff_lt_or_eq, le_iff_lt_or_eq, zpow_bit1_neg_iff, zpow_eq_zero_iff (Int.bit1_ne_zero n)]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ b c d : α
n : ℤ
hn : Even n
a : α
⊢ 0 ≤ a ^ n
[PROOFSTEP]
obtain ⟨k, rfl⟩ := hn
[GOAL]
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a✝ b c d a : α
k : ℤ
⊢ 0 ≤ a ^ (k + k)
[PROOFSTEP]
exact zpow_bit0_nonneg _ _
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hn : Even n
h : n ≠ 0
⊢ 0 < a ^ n ↔ a ≠ 0
[PROOFSTEP]
obtain ⟨k, rfl⟩ := hn
[GOAL]
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
k : ℤ
h : k + k ≠ 0
⊢ 0 < a ^ (k + k) ↔ a ≠ 0
[PROOFSTEP]
exact zpow_bit0_pos_iff (by rintro rfl; simp at h )
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
k : ℤ
h : k + k ≠ 0
⊢ k ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
h : 0 + 0 ≠ 0
⊢ False
[PROOFSTEP]
simp at h 
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hn : Odd n
⊢ a ^ n < 0 ↔ a < 0
[PROOFSTEP]
cases' hn with k hk
[GOAL]
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n k : ℤ
hk : n = 2 * k + 1
⊢ a ^ n < 0 ↔ a < 0
[PROOFSTEP]
simpa only [hk, two_mul] using zpow_bit1_neg_iff
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hn : Odd n
⊢ 0 ≤ a ^ n ↔ 0 ≤ a
[PROOFSTEP]
cases' hn with k hk
[GOAL]
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n k : ℤ
hk : n = 2 * k + 1
⊢ 0 ≤ a ^ n ↔ 0 ≤ a
[PROOFSTEP]
simpa only [hk, two_mul] using zpow_bit1_nonneg_iff
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hn : Odd n
⊢ a ^ n ≤ 0 ↔ a ≤ 0
[PROOFSTEP]
cases' hn with k hk
[GOAL]
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n k : ℤ
hk : n = 2 * k + 1
⊢ a ^ n ≤ 0 ↔ a ≤ 0
[PROOFSTEP]
simpa only [hk, two_mul] using zpow_bit1_nonpos_iff
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hn : Odd n
⊢ 0 < a ^ n ↔ 0 < a
[PROOFSTEP]
cases' hn with k hk
[GOAL]
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c d : α
n k : ℤ
hk : n = 2 * k + 1
⊢ 0 < a ^ n ↔ 0 < a
[PROOFSTEP]
simpa only [hk, two_mul] using zpow_bit1_pos_iff
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
a✝ b c d : α
n p : ℤ
hp : Even p
a : α
⊢ |a| ^ p = a ^ p
[PROOFSTEP]
cases' abs_choice a with h h
[GOAL]
case inl
α : Type u_1
inst✝ : LinearOrderedField α
a✝ b c d : α
n p : ℤ
hp : Even p
a : α
h : |a| = a
⊢ |a| ^ p = a ^ p
[PROOFSTEP]
simp only [h, hp.neg_zpow _]
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a✝ b c d : α
n p : ℤ
hp : Even p
a : α
h : |a| = -a
⊢ |a| ^ p = a ^ p
[PROOFSTEP]
simp only [h, hp.neg_zpow _]
