p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ ↑p ^ (-valuation x) ≤ ↑p ^ (-↑n) ↔ ↑n ≤ valuation x
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ ‖x‖ ≤ ↑p ^ (-↑n) ↔ ↑n ≤ valuation x
rw [norm_eq_pow_val hx]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
⊢ ↑p ^ (-↑k) ≤ ↑p ^ (-↑n) ↔ ↑n ≤ ↑k
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ ↑p ^ (-valuation x) ≤ ↑p ^ (-↑n) ↔ ↑n ≤ valuation x
lift x.valuation to ℕ using x.valuation_nonneg with k
case intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
⊢ (↑p ^ k)⁻¹ ≤ (↑p ^ n)⁻¹ ↔ n ≤ k
case intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
⊢ ↑p ^ (-↑k) ≤ ↑p ^ (-↑n) ↔ ↑n ≤ ↑k
simp only [Int.ofNat_le, zpow_neg, zpow_ofNat]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
aux : ∀ (m : ℕ), 0 < ↑p ^ m
⊢ (↑p ^ k)⁻¹ ≤ (↑p ^ n)⁻¹ ↔ n ≤ k
case intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
⊢ (↑p ^ k)⁻¹ ≤ (↑p ^ n)⁻¹ ↔ n ≤ k
have aux : ∀ m : ℕ, 0 < (p : ℝ) ^ m := by
  intro m
  refine pow_pos ?_ m
  exact_mod_cast hp.1.pos
case intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
aux : ∀ (m : ℕ), 0 < ↑p ^ m
⊢ ↑p ^ n ≤ ↑p ^ k ↔ n ≤ k
case intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
aux : ∀ (m : ℕ), 0 < ↑p ^ m
⊢ (↑p ^ k)⁻¹ ≤ (↑p ^ n)⁻¹ ↔ n ≤ k
rw [inv_le_inv (aux _) (aux _)]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
aux : ∀ (m : ℕ), 0 < ↑p ^ m
this : p ^ n ≤ p ^ k ↔ n ≤ k
⊢ ↑p ^ n ≤ ↑p ^ k ↔ n ≤ k
case intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
aux : ∀ (m : ℕ), 0 < ↑p ^ m
⊢ ↑p ^ n ≤ ↑p ^ k ↔ n ≤ k
have : p ^ n ≤ p ^ k ↔ n ≤ k := (pow_strictMono_right hp.1.one_lt).le_iff_le
case intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
aux : ∀ (m : ℕ), 0 < ↑p ^ m
this : p ^ n ≤ p ^ k ↔ n ≤ k
⊢ ↑p ^ n ≤ ↑p ^ k ↔ p ^ n ≤ p ^ k
case intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
aux : ∀ (m : ℕ), 0 < ↑p ^ m
this : p ^ n ≤ p ^ k ↔ n ≤ k
⊢ ↑p ^ n ≤ ↑p ^ k ↔ n ≤ k
rw [← this]
no goals
case intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
aux : ∀ (m : ℕ), 0 < ↑p ^ m
this : p ^ n ≤ p ^ k ↔ n ≤ k
⊢ ↑p ^ n ≤ ↑p ^ k ↔ p ^ n ≤ p ^ k
norm_cast
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k m : ℕ
⊢ 0 < ↑p ^ m
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
⊢ ∀ (m : ℕ), 0 < ↑p ^ m
intro m
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k m : ℕ
⊢ 0 < ↑p
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k m : ℕ
⊢ 0 < ↑p ^ m
refine pow_pos ?_ m
no goals
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k m : ℕ
⊢ 0 < ↑p
exact_mod_cast hp.1.pos