ι : Type ?u.12689
α : Type u_1
β : Type ?u.12695
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n✝ : ℤ
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ n
ι : Type ?u.12689
α : Type u_1
β : Type ?u.12695
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n✝ : ℤ
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ ↑n
rw [zpow_ofNat]
no goals
ι : Type ?u.12689
α : Type u_1
β : Type ?u.12695
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n✝ : ℤ
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ n
exact pow_nonneg ha _
ι : Type ?u.12689
α : Type u_1
β : Type ?u.12695
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n✝ : ℤ
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ (n + 1)
ι : Type ?u.12689
α : Type u_1
β : Type ?u.12695
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n✝ : ℤ
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ (-↑(n + 1))
rw [zpow_neg, inv_nonneg, zpow_ofNat]
no goals
ι : Type ?u.12689
α : Type u_1
β : Type ?u.12695
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n✝ : ℤ
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ (n + 1)
exact pow_nonneg ha _