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

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ¬x = 0
⊢ 0 ≤ valuation x
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ 0 ≤ valuation x
by_cases hx : x = 0
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ¬x = 0
h : 1 < ↑p
⊢ 0 ≤ valuation x
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ¬x = 0
⊢ 0 ≤ valuation x
have h : (1 : ℝ) < p := by exact_mod_cast hp.1.one_lt
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ¬x = 0
h : 1 < ↑p
⊢ (fun x x_1 => x ^ x_1) (↑p) (-valuation x) ≤ (fun x x_1 => x ^ x_1) (↑p) 0
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ¬x = 0
h : 1 < ↑p
⊢ 0 ≤ valuation x
rw [← neg_nonpos, ← (zpow_strictMono h).le_iff_le]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ¬x = 0
h : 1 < ↑p
⊢ ↑p ^ (-valuation x) ≤ ↑p ^ 0
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ¬x = 0
h : 1 < ↑p
⊢ (fun x x_1 => x ^ x_1) (↑p) (-valuation x) ≤ (fun x x_1 => x ^ x_1) (↑p) 0
show (p : ℝ) ^ (-valuation x) ≤ (p : ℝ) ^ (0 : ℤ)
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ¬x = 0
h : 1 < ↑p
⊢ ‖x‖ ≤ ↑p ^ 0
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ¬x = 0
h : 1 < ↑p
⊢ ↑p ^ (-valuation x) ≤ ↑p ^ 0
rw [← norm_eq_pow_val hx]
no goals
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ¬x = 0
h : 1 < ↑p
⊢ ‖x‖ ≤ ↑p ^ 0
simpa using x.property
no goals
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x = 0
⊢ 0 ≤ valuation x
simp [hx]
no goals
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ¬x = 0
⊢ 1 < ↑p
exact_mod_cast hp.1.one_lt