case pos
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x = 0
⊢ ‖x‖ ≤ 1 ↔ 0 ≤ valuation x

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬x = 0
⊢ ‖x‖ ≤ 1 ↔ 0 ≤ valuation x
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ ‖x‖ ≤ 1 ↔ 0 ≤ valuation x
by_cases hx : x = 0
no goals
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x = 0
⊢ ‖x‖ ≤ 1 ↔ 0 ≤ valuation x
simp only [hx, norm_zero, valuation_zero, zero_le_one, le_refl]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬x = 0
⊢ 1 < ↑p
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬x = 0
⊢ ‖x‖ ≤ 1 ↔ 0 ≤ valuation x
rw [norm_eq_pow_val hx, ← zpow_zero (p : ℝ), zpow_le_iff_le, Right.neg_nonpos_iff]
no goals
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬x = 0
⊢ 1 < ↑p
exact Nat.one_lt_cast.2 (Nat.Prime.one_lt' p).1