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