p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : n = 0
this : Rat.mk' n d = 0
⊢ ‖↑(Rat.mk' n d)‖ ≤ 1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : n = 0
⊢ ‖↑(Rat.mk' n d)‖ ≤ 1
have : (⟨n, d, hn, hd⟩ : ℚ) = 0 := Rat.zero_iff_num_zero.mpr hnz
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : n = 0
this : Rat.mk' n d = 0
⊢ ‖↑0‖ ≤ 1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : n = 0
this : Rat.mk' n d = 0
⊢ ‖↑(Rat.mk' n d)‖ ≤ 1
rw [this]
no goals
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : n = 0
this : Rat.mk' n d = 0
⊢ ‖↑0‖ ≤ 1
norm_num
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : Rat.mk' n d ≠ 0
⊢ ‖↑(Rat.mk' n d)‖ ≤ 1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : ¬n = 0
⊢ ‖↑(Rat.mk' n d)‖ ≤ 1
have hnz' : (⟨n, d, hn, hd⟩ : ℚ) ≠ 0 := mt Rat.zero_iff_num_zero.1 hnz
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : Rat.mk' n d ≠ 0
⊢ ↑(padicNorm p (Rat.mk' n d)) ≤ 1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : Rat.mk' n d ≠ 0
⊢ ‖↑(Rat.mk' n d)‖ ≤ 1
rw [padicNormE.eq_padicNorm]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : Rat.mk' n d ≠ 0
⊢ padicNorm p (Rat.mk' n d) ≤ 1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : Rat.mk' n d ≠ 0
⊢ ↑(padicNorm p (Rat.mk' n d)) ≤ 1
norm_cast
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : Rat.mk' n d ≠ 0
⊢ (↑p ^ padicValInt p (Rat.mk' n d).num)⁻¹ ≤ 1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : Rat.mk' n d ≠ 0
⊢ padicNorm p (Rat.mk' n d) ≤ 1
rw [padicNorm.eq_zpow_of_nonzero hnz', padicValRat, neg_sub,
  padicValNat.eq_zero_of_not_dvd hq, Nat.cast_zero, zero_sub, zpow_neg, zpow_ofNat]
case ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : Rat.mk' n d ≠ 0
⊢ 1 ≤ ↑p ^ padicValInt p (Rat.mk' n d).num
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : Rat.mk' n d ≠ 0
⊢ (↑p ^ padicValInt p (Rat.mk' n d).num)⁻¹ ≤ 1
apply inv_le_one
case ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : Rat.mk' n d ≠ 0
⊢ 1 ≤ p ^ padicValInt p (Rat.mk' n d).num
case ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : Rat.mk' n d ≠ 0
⊢ 1 ≤ ↑p ^ padicValInt p (Rat.mk' n d).num
norm_cast
case ha.h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : Rat.mk' n d ≠ 0
⊢ 0 < p
case ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : Rat.mk' n d ≠ 0
⊢ 1 ≤ p ^ padicValInt p (Rat.mk' n d).num
apply one_le_pow
no goals
case ha.h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : Rat.mk' n d ≠ 0
⊢ 0 < p
exact hp.1.pos