p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)
have aux : ∀ n : ℤ, 0 < ((p : ℝ) ^ n) := by
  apply Nat.zpow_pos_of_pos
  exact hp.1.pos
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : x = 0
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)
by_cases hx0 : x = 0
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
⊢ ↑p ^ (-valuation x) ≤ ↑p ^ n ↔ ↑p ^ (-valuation x) < ↑p ^ (n + 1)
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)
rw [norm_eq_pow_val hx0]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
h1p : 1 < ↑p
⊢ ↑p ^ (-valuation x) ≤ ↑p ^ n ↔ ↑p ^ (-valuation x) < ↑p ^ (n + 1)
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
⊢ ↑p ^ (-valuation x) ≤ ↑p ^ n ↔ ↑p ^ (-valuation x) < ↑p ^ (n + 1)
have h1p : 1 < (p : ℝ) := by exact_mod_cast hp.1.one_lt
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
h1p : 1 < ↑p
H : StrictMono ((fun x x_1 => x ^ x_1) ↑p)
⊢ ↑p ^ (-valuation x) ≤ ↑p ^ n ↔ ↑p ^ (-valuation x) < ↑p ^ (n + 1)
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
h1p : 1 < ↑p
⊢ ↑p ^ (-valuation x) ≤ ↑p ^ n ↔ ↑p ^ (-valuation x) < ↑p ^ (n + 1)
have H := zpow_strictMono h1p
no goals
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
h1p : 1 < ↑p
H : StrictMono ((fun x x_1 => x ^ x_1) ↑p)
⊢ ↑p ^ (-valuation x) ≤ ↑p ^ n ↔ ↑p ^ (-valuation x) < ↑p ^ (n + 1)
rw [H.le_iff_le, H.lt_iff_lt, Int.lt_add_one_iff]
case h
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
⊢ 0 < p
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
⊢ ∀ (n : ℤ), 0 < ↑p ^ n
apply Nat.zpow_pos_of_pos
no goals
case h
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
⊢ 0 < p
exact hp.1.pos
no goals
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : x = 0
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)
simp [hx0, norm_zero, aux, le_of_lt (aux _)]
no goals
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
⊢ 1 < ↑p
exact_mod_cast hp.1.one_lt