𝕜 : Type u_1
B : Type ?u.36107
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
x : 𝕜
hx : 0 < x
⊢ (∃ n, n • p = x) ↔ ∃ n, n • p = x
𝕜 : Type u_1
B : Type ?u.36107
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
x : 𝕜
hx : 0 < x
⊢ ↑x = 0 ↔ ∃ n, n • p = x
rw [coe_eq_zero_iff]
case mp.intro
𝕜 : Type u_1
B : Type ?u.36107
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n • p
⊢ ∃ n_1, n_1 • p = n • p

case mpr.intro
𝕜 : Type u_1
B : Type ?u.36107
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
n : ℕ
hx : 0 < n • p
⊢ ∃ n_1, n_1 • p = n • p
𝕜 : Type u_1
B : Type ?u.36107
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
x : 𝕜
hx : 0 < x
⊢ (∃ n, n • p = x) ↔ ∃ n, n • p = x
constructor <;> rintro ⟨n, rfl⟩
case hx
𝕜 : Type u_1
B : Type ?u.36107
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n • p
⊢ 0 < n

case mp.intro
𝕜 : Type u_1
B : Type ?u.36107
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n
⊢ ∃ n_1, n_1 • p = n • p
case mp.intro
𝕜 : Type u_1
B : Type ?u.36107
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n • p
⊢ ∃ n_1, n_1 • p = n • p
replace hx : 0 < n
no goals
case mp.intro
𝕜 : Type u_1
B : Type ?u.36107
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n
⊢ ∃ n_1, n_1 • p = n • p
exact ⟨n.toNat, by rw [← coe_nat_zsmul, Int.toNat_of_nonneg hx.le]⟩
case hx
𝕜 : Type u_1
B : Type ?u.36107
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
n : ℤ
hx : n ≤ 0
⊢ n • p ≤ 0
case hx
𝕜 : Type u_1
B : Type ?u.36107
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n • p
⊢ 0 < n
contrapose! hx
no goals
case hx
𝕜 : Type u_1
B : Type ?u.36107
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
n : ℤ
hx : n ≤ 0
⊢ n • p ≤ 0
simpa only [← neg_nonneg, ← zsmul_neg, zsmul_neg'] using zsmul_nonneg hp.le (neg_nonneg.2 hx)
no goals
𝕜 : Type u_1
B : Type ?u.36107
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
n : ℤ
hx : 0 < n
⊢ Int.toNat n • p = n • p
rw [← coe_nat_zsmul, Int.toNat_of_nonneg hx.le]
no goals
case mpr.intro
𝕜 : Type u_1
B : Type ?u.36107
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
n : ℕ
hx : 0 < n • p
⊢ ∃ n_1, n_1 • p = n • p
exact ⟨(n : ℤ), by simp⟩
no goals
𝕜 : Type u_1
B : Type ?u.36107
inst✝² : LinearOrderedAddCommGroup 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
n : ℕ
hx : 0 < n • p
⊢ ↑n • p = n • p
simp