[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ 1 ∈
    { carrier := {x | ‖x‖ ≤ 1},
        mul_mem' := (_ : ∀ {a b : ℚ_[p]}, a ∈ {x | ‖x‖ ≤ 1} → b ∈ {x | ‖x‖ ≤ 1} → ‖a * b‖ ≤ 1) }.carrier
[PROOFSTEP]
norm_num
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ 0 ∈
    {
          toSubsemigroup :=
            { carrier := {x | ‖x‖ ≤ 1},
              mul_mem' := (_ : ∀ {a b : ℚ_[p]}, a ∈ {x | ‖x‖ ≤ 1} → b ∈ {x | ‖x‖ ≤ 1} → ‖a * b‖ ≤ 1) },
          one_mem' := (_ : ‖1‖ ≤ 1) }.toSubsemigroup.carrier
[PROOFSTEP]
norm_num
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ Add { x // x ∈ subring p }
[PROOFSTEP]
infer_instance
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ Mul { x // x ∈ subring p }
[PROOFSTEP]
infer_instance
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ Neg { x // x ∈ subring p }
[PROOFSTEP]
infer_instance
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ Sub { x // x ∈ subring p }
[PROOFSTEP]
infer_instance
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ Zero { x // x ∈ subring p }
[PROOFSTEP]
infer_instance
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ‖1‖ ≤ 1
[PROOFSTEP]
norm_num
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ ↑z = 0 ↔ z = 0
[PROOFSTEP]
rw [← coe_zero, Subtype.coe_inj]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ AddCommGroup { x // x ∈ subring p }
[PROOFSTEP]
infer_instance
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ CommRing { x // x ∈ subring p }
[PROOFSTEP]
infer_instance
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖k‖ = 1
⊢ ‖k⁻¹‖ ≤ 1
[PROOFSTEP]
simp [h]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
m n : ℕ
h : ↑m = ↑n
⊢ ↑m = ↑n
[PROOFSTEP]
rw [Subtype.ext_iff] at h
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
m n : ℕ
h✝ : ↑m = ↑n
h : ↑↑m = ↑↑n
⊢ ↑m = ↑n
[PROOFSTEP]
norm_cast at h
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
z1 z2 : ℤ
⊢ ↑z1 = ↑z2 ↔ z1 = z2
[PROOFSTEP]
suffices (z1 : ℚ_[p]) = z2 ↔ z1 = z2 from Iff.trans (by norm_cast) this
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
z1 z2 : ℤ
this : ↑z1 = ↑z2 ↔ z1 = z2
⊢ ↑z1 = ↑z2 ↔ ↑z1 = ↑z2
[PROOFSTEP]
norm_cast
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
z1 z2 : ℤ
⊢ ↑z1 = ↑z2 ↔ z1 = z2
[PROOFSTEP]
norm_cast
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
seq : ℕ → ℤ
h : IsCauSeq (padicNorm p) fun n => ↑(seq n)
⊢ ↑(PadicSeq.norm { val := fun n => ↑(seq n), property := h }) ≤ 1
[PROOFSTEP]
rw [PadicSeq.norm]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
seq : ℕ → ℤ
h : IsCauSeq (padicNorm p) fun n => ↑(seq n)
⊢ ↑(if hf : { val := fun n => ↑(seq n), property := h } ≈ 0 then 0
      else padicNorm p (↑{ val := fun n => ↑(seq n), property := h } (PadicSeq.stationaryPoint hf))) ≤
    1
[PROOFSTEP]
split_ifs with hne
[GOAL]
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
seq : ℕ → ℤ
h : IsCauSeq (padicNorm p) fun n => ↑(seq n)
hne : { val := fun n => ↑(seq n), property := h } ≈ 0
⊢ ↑0 ≤ 1
[PROOFSTEP]
norm_cast
[GOAL]
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
seq : ℕ → ℤ
h : IsCauSeq (padicNorm p) fun n => ↑(seq n)
hne : ¬{ val := fun n => ↑(seq n), property := h } ≈ 0
⊢ ↑(padicNorm p (↑{ val := fun n => ↑(seq n), property := h } (PadicSeq.stationaryPoint hne))) ≤ 1
[PROOFSTEP]
norm_cast
[GOAL]
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
seq : ℕ → ℤ
h : IsCauSeq (padicNorm p) fun n => ↑(seq n)
hne : ¬{ val := fun n => ↑(seq n), property := h } ≈ 0
⊢ padicNorm p (↑{ val := fun n => ↑(seq n), property := h } (PadicSeq.stationaryPoint hne)) ≤ 1
[PROOFSTEP]
apply padicNorm.of_int
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
src✝ : CommRing ℤ_[p] := instCommRing
⊢ ∀ (a b : ℤ_[p]), ‖a * b‖ ≤ ‖a‖ * ‖b‖
[PROOFSTEP]
simp [norm_def]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∀ {x : ℤ_[p]}, ‖x‖ = 0 ↔ x = 0
[PROOFSTEP]
simp [norm_eq_zero]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝¹ x✝ : ℤ_[p]
⊢ ‖x✝¹ * x✝‖ = ‖x✝¹‖ * ‖x✝‖
[PROOFSTEP]
simp only [norm_def, padicNormE.mul, PadicInt.coe_mul]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
⊢ ‖z1 * z2‖ = ‖z1‖ * ‖z2‖
[PROOFSTEP]
simp [norm_def]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ ‖z ^ 0‖ = ‖z‖ ^ 0
[PROOFSTEP]
simp
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
z : ℤ_[p]
k : ℕ
⊢ ‖z ^ (k + 1)‖ = ‖z‖ ^ (k + 1)
[PROOFSTEP]
rw [pow_succ, pow_succ, norm_mul]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
z : ℤ_[p]
k : ℕ
⊢ ‖z‖ * ‖z ^ k‖ = ‖z‖ * ‖z‖ ^ k
[PROOFSTEP]
congr
[GOAL]
case e_a
p : ℕ
inst✝ : Fact (Nat.Prime p)
z : ℤ_[p]
k : ℕ
⊢ ‖z ^ k‖ = ‖z‖ ^ k
[PROOFSTEP]
apply norm_pow
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
h : ‖z1 + z2‖ < ‖z2‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z1 + z2‖ ≥ ‖z2‖
[PROOFSTEP]
rw [norm_add_eq_max_of_ne hne]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
h : ‖z1 + z2‖ < ‖z2‖
hne : ¬‖z1‖ = ‖z2‖
⊢ max ‖z1‖ ‖z2‖ ≥ ‖z2‖
[PROOFSTEP]
apply le_max_right
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
h : ‖z1 + z2‖ < ‖z1‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z1 + z2‖ ≥ ‖z1‖
[PROOFSTEP]
rw [norm_add_eq_max_of_ne hne]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
h : ‖z1 + z2‖ < ‖z1‖
hne : ¬‖z1‖ = ‖z2‖
⊢ max ‖z1‖ ‖z2‖ ≥ ‖z1‖
[PROOFSTEP]
apply le_max_left
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ ‖↑z‖ = ‖z‖
[PROOFSTEP]
simp [norm_def]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
z : ℤ
⊢ ‖↑z‖ = ‖↑z‖
[PROOFSTEP]
simp [norm_def]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℤ_[p] norm
x✝ : ℝ
hε : x✝ > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → (fun a => ‖a‖) ((fun n => ↑(↑f n)) j - (fun n => ↑(↑f n)) i) < x✝
[PROOFSTEP]
simpa [norm, norm_def] using f.cauchy hε
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℤ_[p] norm
hqn : ‖CauSeq.lim (PadicInt.cauSeq_to_rat_cauSeq f)‖ ≤ 1
ε : ℝ
⊢ ε > 0 →
    ∃ i,
      ∀ (j : ℕ),
        j ≥ i →
          ‖↑(f - CauSeq.const norm { val := CauSeq.lim (PadicInt.cauSeq_to_rat_cauSeq f), property := hqn }) j‖ < ε
[PROOFSTEP]
simpa [norm, norm_def] using CauSeq.equiv_lim (cauSeq_to_rat_cauSeq f) ε
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
⊢ ∃ k, ↑p ^ (-↑k) < ε
[PROOFSTEP]
obtain ⟨k, hk⟩ := exists_nat_gt ε⁻¹
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ∃ k, ↑p ^ (-↑k) < ε
[PROOFSTEP]
use k
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ↑p ^ (-↑k) < ε
[PROOFSTEP]
rw [← inv_lt_inv hε (_root_.zpow_pos_of_pos _ _)]
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ε⁻¹ < (↑p ^ (-↑k))⁻¹
[PROOFSTEP]
rw [zpow_neg, inv_inv, zpow_ofNat]
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ε⁻¹ < ↑p ^ k
[PROOFSTEP]
apply lt_of_lt_of_le hk
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ↑k ≤ ↑p ^ k
[PROOFSTEP]
norm_cast
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ k ≤ p ^ k
[PROOFSTEP]
apply le_of_lt
[GOAL]
case h.a
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ k < p ^ k
[PROOFSTEP]
convert Nat.lt_pow_self _ _ using 1
[GOAL]
case h.a.convert_2
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ 1 < p
[PROOFSTEP]
exact hp.1.one_lt
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ 0 < ↑p
[PROOFSTEP]
exact_mod_cast hp.1.pos
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℚ
hε : 0 < ε
⊢ ∃ k, ↑p ^ (-↑k) < ε
[PROOFSTEP]
obtain ⟨k, hk⟩ := @exists_pow_neg_lt p _ ε (by exact_mod_cast hε)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℚ
hε : 0 < ε
⊢ 0 < ↑ε
[PROOFSTEP]
exact_mod_cast hε
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℚ
hε : 0 < ε
k : ℕ
hk : ↑p ^ (-↑k) < ↑ε
⊢ ∃ k, ↑p ^ (-↑k) < ε
[PROOFSTEP]
use k
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℚ
hε : 0 < ε
k : ℕ
hk : ↑p ^ (-↑k) < ↑ε
⊢ ↑p ^ (-↑k) < ε
[PROOFSTEP]
rw [show (p : ℝ) = (p : ℚ) by simp] at hk
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℚ
hε : 0 < ε
k : ℕ
hk : ↑p ^ (-↑k) < ↑ε
⊢ ↑p = ↑↑p
[PROOFSTEP]
simp
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℚ
hε : 0 < ε
k : ℕ
hk : ↑↑p ^ (-↑k) < ↑ε
⊢ ↑p ^ (-↑k) < ε
[PROOFSTEP]
exact_mod_cast hk
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
this : ‖↑k‖ < 1 ↔ ↑p ∣ k
⊢ ‖↑k‖ < 1 ↔ ↑p ∣ k
[PROOFSTEP]
rwa [norm_int_cast_eq_padic_norm]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑(p ^ n) ∣ k
⊢ ‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑(p ^ n) ∣ k
[PROOFSTEP]
simpa [norm_int_cast_eq_padic_norm]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ‖x‖ = ↑p ^ (-valuation x)
[PROOFSTEP]
refine @Padic.norm_eq_pow_val p hp x ?_
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ↑x ≠ 0
[PROOFSTEP]
contrapose! hx
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ↑x = 0
⊢ x = 0
[PROOFSTEP]
exact Subtype.val_injective hx
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ valuation ↑p = 1
[PROOFSTEP]
simp [valuation]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ 0 ≤ valuation x
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x = 0
⊢ 0 ≤ valuation x
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ¬x = 0
⊢ 0 ≤ valuation x
[PROOFSTEP]
have h : (1 : ℝ) < p := by exact_mod_cast hp.1.one_lt
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ¬x = 0
⊢ 1 < ↑p
[PROOFSTEP]
exact_mod_cast hp.1.one_lt
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ¬x = 0
h : 1 < ↑p
⊢ 0 ≤ valuation x
[PROOFSTEP]
rw [← neg_nonpos, ← (zpow_strictMono h).le_iff_le]
[GOAL]
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
[PROOFSTEP]
show (p : ℝ) ^ (-valuation x) ≤ (p : ℝ) ^ (0 : ℤ)
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ¬x = 0
h : 1 < ↑p
⊢ ↑p ^ (-valuation x) ≤ ↑p ^ 0
[PROOFSTEP]
rw [← norm_eq_pow_val hx]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ¬x = 0
h : 1 < ↑p
⊢ ‖x‖ ≤ ↑p ^ 0
[PROOFSTEP]
simpa using x.property
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hc : c ≠ 0
⊢ valuation (↑p ^ n * c) = ↑n + valuation c
[PROOFSTEP]
have : ‖(p : ℤ_[p]) ^ n * c‖ = ‖(p : ℤ_[p]) ^ n‖ * ‖c‖ := norm_mul _ _
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hc : c ≠ 0
this : ‖↑p ^ n * c‖ = ‖↑p ^ n‖ * ‖c‖
⊢ valuation (↑p ^ n * c) = ↑n + valuation c
[PROOFSTEP]
have aux : (p : ℤ_[p]) ^ n * c ≠ 0 := by
  contrapose! hc
  rw [mul_eq_zero] at hc
  cases' hc with hc hc
  · refine (hp.1.ne_zero ?_).elim
    exact_mod_cast pow_eq_zero hc
  · exact hc
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hc : c ≠ 0
this : ‖↑p ^ n * c‖ = ‖↑p ^ n‖ * ‖c‖
⊢ ↑p ^ n * c ≠ 0
[PROOFSTEP]
contrapose! hc
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
this : ‖↑p ^ n * c‖ = ‖↑p ^ n‖ * ‖c‖
hc : ↑p ^ n * c = 0
⊢ c = 0
[PROOFSTEP]
rw [mul_eq_zero] at hc
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
this : ‖↑p ^ n * c‖ = ‖↑p ^ n‖ * ‖c‖
hc : ↑p ^ n = 0 ∨ c = 0
⊢ c = 0
[PROOFSTEP]
cases' hc with hc hc
[GOAL]
case inl
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
this : ‖↑p ^ n * c‖ = ‖↑p ^ n‖ * ‖c‖
hc : ↑p ^ n = 0
⊢ c = 0
[PROOFSTEP]
refine (hp.1.ne_zero ?_).elim
[GOAL]
case inl
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
this : ‖↑p ^ n * c‖ = ‖↑p ^ n‖ * ‖c‖
hc : ↑p ^ n = 0
⊢ p = 0
[PROOFSTEP]
exact_mod_cast pow_eq_zero hc
[GOAL]
case inr
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
this : ‖↑p ^ n * c‖ = ‖↑p ^ n‖ * ‖c‖
hc : c = 0
⊢ c = 0
[PROOFSTEP]
exact hc
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hc : c ≠ 0
this : ‖↑p ^ n * c‖ = ‖↑p ^ n‖ * ‖c‖
aux : ↑p ^ n * c ≠ 0
⊢ valuation (↑p ^ n * c) = ↑n + valuation c
[PROOFSTEP]
rwa [norm_eq_pow_val aux, norm_p_pow, norm_eq_pow_val hc, ← zpow_add₀, ← neg_add, zpow_inj, neg_inj] at this
[GOAL]
case h₀
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hc : c ≠ 0
this : ↑p ^ (-valuation (↑p ^ n * c)) = ↑p ^ (-(↑n + valuation c))
aux : ↑p ^ n * c ≠ 0
⊢ 0 < ↑p
[PROOFSTEP]
exact_mod_cast hp.1.pos
[GOAL]
case h₁
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hc : c ≠ 0
this : ↑p ^ (-valuation (↑p ^ n * c)) = ↑p ^ (-(↑n + valuation c))
aux : ↑p ^ n * c ≠ 0
⊢ ↑p ≠ 1
[PROOFSTEP]
exact_mod_cast hp.1.ne_one
[GOAL]
case ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hc : c ≠ 0
this : ↑p ^ (-valuation (↑p ^ n * c)) = ↑p ^ (-↑n) * ↑p ^ (-valuation c)
aux : ↑p ^ n * c ≠ 0
⊢ ↑p ≠ 0
[PROOFSTEP]
exact_mod_cast hp.1.ne_zero
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖{ val := k, property := property✝ }‖ = 1
⊢ { val := k, property := property✝ } * inv { val := k, property := property✝ } = 1
[PROOFSTEP]
have hk : k ≠ 0 := fun h' => zero_ne_one' ℚ_[p] (by simp [h'] at h )
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖{ val := k, property := property✝ }‖ = 1
h' : k = 0
⊢ 0 = 1
[PROOFSTEP]
simp [h'] at h
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖{ val := k, property := property✝ }‖ = 1
hk : k ≠ 0
⊢ { val := k, property := property✝ } * inv { val := k, property := property✝ } = 1
[PROOFSTEP]
unfold PadicInt.inv
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖{ val := k, property := property✝ }‖ = 1
hk : k ≠ 0
⊢ ({ val := k, property := property✝ } *
      match { val := k, property := property✝ } with
      | { val := k, property := property } => if h : ‖k‖ = 1 then { val := k⁻¹, property := (_ : ‖k⁻¹‖ ≤ 1) } else 0) =
    1
[PROOFSTEP]
rw [norm_eq_padic_norm] at h
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖k‖ = 1
hk : k ≠ 0
⊢ ({ val := k, property := property✝ } *
      match { val := k, property := property✝ } with
      | { val := k, property := property } => if h : ‖k‖ = 1 then { val := k⁻¹, property := (_ : ‖k⁻¹‖ ≤ 1) } else 0) =
    1
[PROOFSTEP]
dsimp only
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖k‖ = 1
hk : k ≠ 0
⊢ ({ val := k, property := property✝ } * if h : ‖k‖ = 1 then { val := k⁻¹, property := (_ : ‖k⁻¹‖ ≤ 1) } else 0) = 1
[PROOFSTEP]
rw [dif_pos h]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖k‖ = 1
hk : k ≠ 0
⊢ { val := k, property := property✝ } * { val := k⁻¹, property := (_ : ‖k⁻¹‖ ≤ 1) } = 1
[PROOFSTEP]
apply Subtype.ext_iff_val.2
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖k‖ = 1
hk : k ≠ 0
⊢ ↑({ val := k, property := property✝ } * { val := k⁻¹, property := (_ : ‖k⁻¹‖ ≤ 1) }) = ↑1
[PROOFSTEP]
simp [mul_inv_cancel hk]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
hz : ‖z‖ = 1
⊢ inv z * z = 1
[PROOFSTEP]
rw [mul_comm, mul_inv hz]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
⊢ ‖z‖ = 1
[PROOFSTEP]
rcases isUnit_iff_dvd_one.1 h with ⟨w, eq⟩
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
w : ℤ_[p]
eq : 1 = z * w
⊢ ‖z‖ = 1
[PROOFSTEP]
refine' le_antisymm (norm_le_one _) _
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
w : ℤ_[p]
eq : 1 = z * w
⊢ 1 ≤ ‖z‖
[PROOFSTEP]
have := mul_le_mul_of_nonneg_left (norm_le_one w) (norm_nonneg z)
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
w : ℤ_[p]
eq : 1 = z * w
this : ‖z‖ * ‖w‖ ≤ ‖z‖ * 1
⊢ 1 ≤ ‖z‖
[PROOFSTEP]
rwa [mul_one, ← norm_mul, ← eq, norm_one] at this
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
hz2 : ‖z2‖ < 1
⊢ ‖z1 * z2‖ = ‖z1‖ * ‖z2‖
[PROOFSTEP]
simp
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ z ∈ nonunits ℤ_[p] ↔ ‖z‖ < 1
[PROOFSTEP]
rw [lt_iff_le_and_ne]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ z ∈ nonunits ℤ_[p] ↔ ‖z‖ ≤ 1 ∧ ‖z‖ ≠ 1
[PROOFSTEP]
simp [norm_le_one z, nonunits, isUnit_iff]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
u : ℤ_[p]ˣ
⊢ IsUnit ↑u
[PROOFSTEP]
simp
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
u : ℚ_[p] := ↑x * ↑p ^ (-valuation x)
⊢ ‖u‖ = 1
[PROOFSTEP]
simp [hx, Nat.zpow_ne_zero_of_pos (by exact_mod_cast hp.1.pos) x.valuation, norm_eq_pow_val, zpow_neg, inv_mul_cancel]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
u : ℚ_[p] := ↑x * ↑p ^ (-valuation x)
⊢ 0 < ?m.493673
[PROOFSTEP]
exact_mod_cast hp.1.pos
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ x = ↑(unitCoeff hx) * ↑p ^ Int.natAbs (valuation x)
[PROOFSTEP]
apply Subtype.coe_injective
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ (fun a => ↑a) x = (fun a => ↑a) (↑(unitCoeff hx) * ↑p ^ Int.natAbs (valuation x))
[PROOFSTEP]
push_cast
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ↑x = ↑↑(unitCoeff hx) * ↑p ^ Int.natAbs (valuation x)
[PROOFSTEP]
have repr : (x : ℚ_[p]) = unitCoeff hx * (p : ℚ_[p]) ^ x.valuation :=
  by
  rw [unitCoeff_coe, mul_assoc, ← zpow_add₀]
  · simp
  · exact_mod_cast hp.1.ne_zero
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ↑x = ↑↑(unitCoeff hx) * ↑p ^ valuation x
[PROOFSTEP]
rw [unitCoeff_coe, mul_assoc, ← zpow_add₀]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ↑x = ↑x * ↑p ^ (-valuation x + valuation x)
[PROOFSTEP]
simp
[GOAL]
case ha
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ↑p ≠ 0
[PROOFSTEP]
exact_mod_cast hp.1.ne_zero
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
repr : ↑x = ↑↑(unitCoeff hx) * ↑p ^ valuation x
⊢ ↑x = ↑↑(unitCoeff hx) * ↑p ^ Int.natAbs (valuation x)
[PROOFSTEP]
convert repr using 2
[GOAL]
case h.e'_3.h.e'_6
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
repr : ↑x = ↑↑(unitCoeff hx) * ↑p ^ valuation x
⊢ ↑p ^ Int.natAbs (valuation x) = ↑p ^ valuation x
[PROOFSTEP]
rw [← zpow_ofNat, Int.natAbs_of_nonneg (valuation_nonneg x)]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ ‖x‖ ≤ ↑p ^ (-↑n) ↔ ↑n ≤ valuation x
[PROOFSTEP]
rw [norm_eq_pow_val hx]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ ↑p ^ (-valuation x) ≤ ↑p ^ (-↑n) ↔ ↑n ≤ valuation x
[PROOFSTEP]
lift x.valuation to ℕ using x.valuation_nonneg with k
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
⊢ ↑p ^ (-↑k) ≤ ↑p ^ (-↑n) ↔ ↑n ≤ ↑k
[PROOFSTEP]
simp only [Int.ofNat_le, zpow_neg, zpow_ofNat]
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
⊢ (↑p ^ k)⁻¹ ≤ (↑p ^ n)⁻¹ ↔ n ≤ k
[PROOFSTEP]
have aux : ∀ m : ℕ, 0 < (p : ℝ) ^ m := by
  intro m
  refine pow_pos ?_ m
  exact_mod_cast hp.1.pos
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
⊢ ∀ (m : ℕ), 0 < ↑p ^ m
[PROOFSTEP]
intro m
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k m : ℕ
⊢ 0 < ↑p ^ m
[PROOFSTEP]
refine pow_pos ?_ m
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k m : ℕ
⊢ 0 < ↑p
[PROOFSTEP]
exact_mod_cast hp.1.pos
[GOAL]
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
[PROOFSTEP]
rw [inv_le_inv (aux _) (aux _)]
[GOAL]
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
[PROOFSTEP]
have : p ^ n ≤ p ^ k ↔ n ≤ k := (pow_strictMono_right hp.1.one_lt).le_iff_le
[GOAL]
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
[PROOFSTEP]
rw [← this]
[GOAL]
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
[PROOFSTEP]
norm_cast
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ x ∈ Ideal.span {↑p ^ n} ↔ ↑n ≤ valuation x
[PROOFSTEP]
rw [Ideal.mem_span_singleton]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ ↑p ^ n ∣ x ↔ ↑n ≤ valuation x
[PROOFSTEP]
constructor
[GOAL]
case mp
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ ↑p ^ n ∣ x → ↑n ≤ valuation x
[PROOFSTEP]
rintro ⟨c, rfl⟩
[GOAL]
case mp.intro
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : ↑p ^ n * c ≠ 0
⊢ ↑n ≤ valuation (↑p ^ n * c)
[PROOFSTEP]
suffices c ≠ 0 by
  rw [valuation_p_pow_mul _ _ this, le_add_iff_nonneg_right]
  apply valuation_nonneg
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : ↑p ^ n * c ≠ 0
this : c ≠ 0
⊢ ↑n ≤ valuation (↑p ^ n * c)
[PROOFSTEP]
rw [valuation_p_pow_mul _ _ this, le_add_iff_nonneg_right]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : ↑p ^ n * c ≠ 0
this : c ≠ 0
⊢ 0 ≤ valuation c
[PROOFSTEP]
apply valuation_nonneg
[GOAL]
case mp.intro
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : ↑p ^ n * c ≠ 0
⊢ c ≠ 0
[PROOFSTEP]
contrapose! hx
[GOAL]
case mp.intro
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : c = 0
⊢ ↑p ^ n * c = 0
[PROOFSTEP]
rw [hx, mul_zero]
[GOAL]
case mpr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ ↑n ≤ valuation x → ↑p ^ n ∣ x
[PROOFSTEP]
nth_rewrite 2 [unitCoeff_spec hx]
[GOAL]
case mpr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ ↑n ≤ valuation x → ↑p ^ n ∣ ↑(unitCoeff hx) * ↑p ^ Int.natAbs (valuation x)
[PROOFSTEP]
lift x.valuation to ℕ using x.valuation_nonneg with k
[GOAL]
case mpr.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
⊢ ↑n ≤ ↑k → ↑p ^ n ∣ ↑(unitCoeff hx) * ↑p ^ Int.natAbs ↑k
[PROOFSTEP]
simp only [Int.natAbs_ofNat, Units.isUnit, IsUnit.dvd_mul_left, Int.ofNat_le]
[GOAL]
case mpr.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
⊢ n ≤ k → ↑p ^ n ∣ ↑p ^ k
[PROOFSTEP]
intro H
[GOAL]
case mpr.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
H : n ≤ k
⊢ ↑p ^ n ∣ ↑p ^ k
[PROOFSTEP]
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le H
[GOAL]
case mpr.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
H : n ≤ n + k
⊢ ↑p ^ n ∣ ↑p ^ (n + k)
[PROOFSTEP]
simp only [pow_add, dvd_mul_right]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
⊢ ‖x‖ ≤ ↑p ^ (-↑n) ↔ x ∈ Ideal.span {↑p ^ n}
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
hx : x = 0
⊢ ‖x‖ ≤ ↑p ^ (-↑n) ↔ x ∈ Ideal.span {↑p ^ n}
[PROOFSTEP]
subst hx
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ‖0‖ ≤ ↑p ^ (-↑n) ↔ 0 ∈ Ideal.span {↑p ^ n}
[PROOFSTEP]
simp only [norm_zero, zpow_neg, zpow_ofNat, inv_nonneg, iff_true_iff, Submodule.zero_mem]
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ 0 ≤ ↑p ^ n
[PROOFSTEP]
exact_mod_cast Nat.zero_le _
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
hx : ¬x = 0
⊢ ‖x‖ ≤ ↑p ^ (-↑n) ↔ x ∈ Ideal.span {↑p ^ n}
[PROOFSTEP]
rw [norm_le_pow_iff_le_valuation x hx, mem_span_pow_iff_le_valuation x hx]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℤ
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)
[PROOFSTEP]
rw [norm_def]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℤ
⊢ ‖↑x‖ ≤ ↑p ^ n ↔ ‖↑x‖ < ↑p ^ (n + 1)
[PROOFSTEP]
exact Padic.norm_le_pow_iff_norm_lt_pow_add_one _ _
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℤ
⊢ ‖x‖ < ↑p ^ n ↔ ‖x‖ ≤ ↑p ^ (n - 1)
[PROOFSTEP]
rw [norm_le_pow_iff_norm_lt_pow_add_one, sub_add_cancel]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ‖x‖ < 1 ↔ ↑p ∣ x
[PROOFSTEP]
have := norm_le_pow_iff_mem_span_pow x 1
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
this : ‖x‖ ≤ ↑p ^ (-↑1) ↔ x ∈ Ideal.span {↑p ^ 1}
⊢ ‖x‖ < 1 ↔ ↑p ∣ x
[PROOFSTEP]
rw [Ideal.mem_span_singleton, pow_one] at this
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
this : ‖x‖ ≤ ↑p ^ (-↑1) ↔ ↑p ∣ x
⊢ ‖x‖ < 1 ↔ ↑p ∣ x
[PROOFSTEP]
rw [← this, norm_le_pow_iff_norm_lt_pow_add_one]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
this : ‖x‖ ≤ ↑p ^ (-↑1) ↔ ↑p ∣ x
⊢ ‖x‖ < 1 ↔ ‖x‖ < ↑p ^ (-↑1 + 1)
[PROOFSTEP]
simp only [zpow_zero, Int.ofNat_zero, Int.ofNat_succ, add_left_neg, zero_add]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
a : ℤ
⊢ ↑p ^ n ∣ ↑a ↔ ↑(p ^ n) ∣ a
[PROOFSTEP]
rw [← Nat.cast_pow, ← norm_int_le_pow_iff_dvd, norm_le_pow_iff_mem_span_pow, Ideal.mem_span_singleton, Nat.cast_pow]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∀ (a b : ℤ_[p]), a ∈ nonunits ℤ_[p] → b ∈ nonunits ℤ_[p] → a + b ∈ nonunits ℤ_[p]
[PROOFSTEP]
simp only [mem_nonunits]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∀ (a b : ℤ_[p]), ‖a‖ < 1 → ‖b‖ < 1 → ‖a + b‖ < 1
[PROOFSTEP]
exact fun x y => norm_lt_one_add
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑p ∈ nonunits ℤ_[p]
[PROOFSTEP]
have : (p : ℝ)⁻¹ < 1 := inv_lt_one <| by exact_mod_cast hp.1.one_lt
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ 1 < ↑p
[PROOFSTEP]
exact_mod_cast hp.1.one_lt
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
this : (↑p)⁻¹ < 1
⊢ ↑p ∈ nonunits ℤ_[p]
[PROOFSTEP]
rwa [← norm_p, ← mem_nonunits] at this
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ maximalIdeal ℤ_[p] = Ideal.span {↑p}
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ maximalIdeal ℤ_[p] ≤ Ideal.span {↑p}
[PROOFSTEP]
intro x hx
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ∈ maximalIdeal ℤ_[p]
⊢ x ∈ Ideal.span {↑p}
[PROOFSTEP]
simp only [LocalRing.mem_maximalIdeal, mem_nonunits] at hx
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ‖x‖ < 1
⊢ x ∈ Ideal.span {↑p}
[PROOFSTEP]
rwa [Ideal.mem_span_singleton, ← norm_lt_one_iff_dvd]
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Ideal.span {↑p} ≤ maximalIdeal ℤ_[p]
[PROOFSTEP]
rw [Ideal.span_le, Set.singleton_subset_iff]
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑p ∈ ↑(maximalIdeal ℤ_[p])
[PROOFSTEP]
exact p_nonnunit
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Prime ↑p
[PROOFSTEP]
rw [← Ideal.span_singleton_prime, ← maximalIdeal_eq_span_p]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Ideal.IsPrime (maximalIdeal ℤ_[p])
[PROOFSTEP]
infer_instance
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑p ≠ 0
[PROOFSTEP]
exact_mod_cast hp.1.ne_zero
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ↑p ^ Int.natAbs (valuation x) * ↑(unitCoeff hx) = x
[PROOFSTEP]
rw [mul_comm, ← unitCoeff_spec hx]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → x m ≡ x n [SMOD maximalIdeal ℤ_[p] ^ m • ⊤]
⊢ ∃ L, ∀ (n : ℕ), x n ≡ L [SMOD maximalIdeal ℤ_[p] ^ n • ⊤]
[PROOFSTEP]
simp only [← Ideal.one_eq_top, smul_eq_mul, mul_one, SModEq.sub_mem, maximalIdeal_eq_span_p, Ideal.span_singleton_pow, ←
  norm_le_pow_iff_mem_span_pow] at hx ⊢
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
⊢ ∃ L, ∀ (n : ℕ), ‖x n - L‖ ≤ ↑p ^ (-↑n)
[PROOFSTEP]
let x' : CauSeq ℤ_[p] norm := ⟨x, ?_⟩
[GOAL]
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
x' : CauSeq ℤ_[p] norm := { val := x, property := ?refine_1 }
⊢ ∃ L, ∀ (n : ℕ), ‖x n - L‖ ≤ ↑p ^ (-↑n)
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
⊢ IsCauSeq norm x
[PROOFSTEP]
swap
[GOAL]
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
⊢ IsCauSeq norm x
[PROOFSTEP]
intro ε hε
[GOAL]
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
ε : ℝ
hε : ε > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → ‖x j - x i‖ < ε
[PROOFSTEP]
obtain ⟨m, hm⟩ := exists_pow_neg_lt p hε
[GOAL]
case refine_1.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
ε : ℝ
hε : ε > 0
m : ℕ
hm : ↑p ^ (-↑m) < ε
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → ‖x j - x i‖ < ε
[PROOFSTEP]
refine ⟨m, fun n hn => lt_of_le_of_lt ?_ hm⟩
[GOAL]
case refine_1.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
ε : ℝ
hε : ε > 0
m : ℕ
hm : ↑p ^ (-↑m) < ε
n : ℕ
hn : n ≥ m
⊢ ‖x n - x m‖ ≤ ↑p ^ (-↑m)
[PROOFSTEP]
rw [← neg_sub, norm_neg]
[GOAL]
case refine_1.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
ε : ℝ
hε : ε > 0
m : ℕ
hm : ↑p ^ (-↑m) < ε
n : ℕ
hn : n ≥ m
⊢ ‖x m - x n‖ ≤ ↑p ^ (-↑m)
[PROOFSTEP]
exact hx hn
[GOAL]
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
x' : CauSeq ℤ_[p] norm := { val := x, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → ‖x j - x i‖ < ε) }
⊢ ∃ L, ∀ (n : ℕ), ‖x n - L‖ ≤ ↑p ^ (-↑n)
[PROOFSTEP]
refine ⟨x'.lim, fun n => ?_⟩
[GOAL]
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
x' : CauSeq ℤ_[p] norm := { val := x, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → ‖x j - x i‖ < ε) }
n : ℕ
⊢ ‖x n - CauSeq.lim x'‖ ≤ ↑p ^ (-↑n)
[PROOFSTEP]
have : (0 : ℝ) < (p : ℝ) ^ (-n : ℤ) := by
  apply zpow_pos_of_pos
  exact_mod_cast hp.1.pos
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
x' : CauSeq ℤ_[p] norm := { val := x, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → ‖x j - x i‖ < ε) }
n : ℕ
⊢ 0 < ↑p ^ (-↑n)
[PROOFSTEP]
apply zpow_pos_of_pos
[GOAL]
case ha
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
x' : CauSeq ℤ_[p] norm := { val := x, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → ‖x j - x i‖ < ε) }
n : ℕ
⊢ 0 < ↑p
[PROOFSTEP]
exact_mod_cast hp.1.pos
[GOAL]
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
x' : CauSeq ℤ_[p] norm := { val := x, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → ‖x j - x i‖ < ε) }
n : ℕ
this : 0 < ↑p ^ (-↑n)
⊢ ‖x n - CauSeq.lim x'‖ ≤ ↑p ^ (-↑n)
[PROOFSTEP]
obtain ⟨i, hi⟩ := equiv_def₃ (equiv_lim x') this
[GOAL]
case refine_2.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
x' : CauSeq ℤ_[p] norm := { val := x, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → ‖x j - x i‖ < ε) }
n : ℕ
this : 0 < ↑p ^ (-↑n)
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → ∀ (k : ℕ), k ≥ j → ‖↑x' k - ↑(const norm (CauSeq.lim x')) j‖ < ↑p ^ (-↑n)
⊢ ‖x n - CauSeq.lim x'‖ ≤ ↑p ^ (-↑n)
[PROOFSTEP]
by_cases hin : i ≤ n
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
x' : CauSeq ℤ_[p] norm := { val := x, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → ‖x j - x i‖ < ε) }
n : ℕ
this : 0 < ↑p ^ (-↑n)
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → ∀ (k : ℕ), k ≥ j → ‖↑x' k - ↑(const norm (CauSeq.lim x')) j‖ < ↑p ^ (-↑n)
hin : i ≤ n
⊢ ‖x n - CauSeq.lim x'‖ ≤ ↑p ^ (-↑n)
[PROOFSTEP]
exact (hi i le_rfl n hin).le
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
x' : CauSeq ℤ_[p] norm := { val := x, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → ‖x j - x i‖ < ε) }
n : ℕ
this : 0 < ↑p ^ (-↑n)
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → ∀ (k : ℕ), k ≥ j → ‖↑x' k - ↑(const norm (CauSeq.lim x')) j‖ < ↑p ^ (-↑n)
hin : ¬i ≤ n
⊢ ‖x n - CauSeq.lim x'‖ ≤ ↑p ^ (-↑n)
[PROOFSTEP]
push_neg at hin
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
x' : CauSeq ℤ_[p] norm := { val := x, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → ‖x j - x i‖ < ε) }
n : ℕ
this : 0 < ↑p ^ (-↑n)
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → ∀ (k : ℕ), k ≥ j → ‖↑x' k - ↑(const norm (CauSeq.lim x')) j‖ < ↑p ^ (-↑n)
hin : n < i
⊢ ‖x n - CauSeq.lim x'‖ ≤ ↑p ^ (-↑n)
[PROOFSTEP]
specialize hi i le_rfl i le_rfl
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
x' : CauSeq ℤ_[p] norm := { val := x, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → ‖x j - x i‖ < ε) }
n : ℕ
this : 0 < ↑p ^ (-↑n)
i : ℕ
hin : n < i
hi : ‖↑x' i - ↑(const norm (CauSeq.lim x')) i‖ < ↑p ^ (-↑n)
⊢ ‖x n - CauSeq.lim x'‖ ≤ ↑p ^ (-↑n)
[PROOFSTEP]
specialize hx hin.le
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ_[p]
hx✝ : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
x' : CauSeq ℤ_[p] norm := { val := x, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → ‖x j - x i‖ < ε) }
n : ℕ
this : 0 < ↑p ^ (-↑n)
i : ℕ
hin : n < i
hi : ‖↑x' i - ↑(const norm (CauSeq.lim x')) i‖ < ↑p ^ (-↑n)
hx : ‖x n - x i‖ ≤ ↑p ^ (-↑n)
⊢ ‖x n - CauSeq.lim x'‖ ≤ ↑p ^ (-↑n)
[PROOFSTEP]
have := nonarchimedean (x n - x i : ℤ_[p]) (x i - x'.lim)
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ_[p]
hx✝ : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
x' : CauSeq ℤ_[p] norm := { val := x, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → ‖x j - x i‖ < ε) }
n : ℕ
this✝ : 0 < ↑p ^ (-↑n)
i : ℕ
hin : n < i
hi : ‖↑x' i - ↑(const norm (CauSeq.lim x')) i‖ < ↑p ^ (-↑n)
hx : ‖x n - x i‖ ≤ ↑p ^ (-↑n)
this : ‖x n - x i + (x i - CauSeq.lim x')‖ ≤ max ‖x n - x i‖ ‖x i - CauSeq.lim x'‖
⊢ ‖x n - CauSeq.lim x'‖ ≤ ↑p ^ (-↑n)
[PROOFSTEP]
rw [sub_add_sub_cancel] at this
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ_[p]
hx✝ : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
x' : CauSeq ℤ_[p] norm := { val := x, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ i, ∀ (j : ℕ), j ≥ i → ‖x j - x i‖ < ε) }
n : ℕ
this✝ : 0 < ↑p ^ (-↑n)
i : ℕ
hin : n < i
hi : ‖↑x' i - ↑(const norm (CauSeq.lim x')) i‖ < ↑p ^ (-↑n)
hx : ‖x n - x i‖ ≤ ↑p ^ (-↑n)
this : ‖x n - CauSeq.lim x'‖ ≤ max ‖x n - x i‖ ‖x i - CauSeq.lim x'‖
⊢ ‖x n - CauSeq.lim x'‖ ≤ ↑p ^ (-↑n)
[PROOFSTEP]
refine' this.trans (max_le_iff.mpr ⟨hx, hi.le⟩)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x✝ : { x // x ∈ nonZeroDivisors ℤ_[p] }
x : ℤ_[p]
hx : x ∈ nonZeroDivisors ℤ_[p]
⊢ IsUnit (↑(algebraMap ℤ_[p] ℚ_[p]) ↑{ val := x, property := hx })
[PROOFSTEP]
rwa [algebraMap_apply, isUnit_iff_ne_zero, PadicInt.coe_ne_zero, ← mem_nonZeroDivisors_iff_ne_zero]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ ∃ x_1, x * ↑(algebraMap ℤ_[p] ℚ_[p]) ↑x_1.snd = ↑(algebraMap ℤ_[p] ℚ_[p]) x_1.fst
[PROOFSTEP]
by_cases hx : ‖x‖ ≤ 1
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ‖x‖ ≤ 1
⊢ ∃ x_1, x * ↑(algebraMap ℤ_[p] ℚ_[p]) ↑x_1.snd = ↑(algebraMap ℤ_[p] ℚ_[p]) x_1.fst
[PROOFSTEP]
use(⟨x, hx⟩, 1)
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ‖x‖ ≤ 1
⊢ x * ↑(algebraMap ℤ_[p] ℚ_[p]) ↑({ val := x, property := hx }, 1).snd =
    ↑(algebraMap ℤ_[p] ℚ_[p]) ({ val := x, property := hx }, 1).fst
[PROOFSTEP]
rw [Submonoid.coe_one, map_one, mul_one, PadicInt.algebraMap_apply, Subtype.coe_mk]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
⊢ ∃ x_1, x * ↑(algebraMap ℤ_[p] ℚ_[p]) ↑x_1.snd = ↑(algebraMap ℤ_[p] ℚ_[p]) x_1.fst
[PROOFSTEP]
set n := Int.toNat (-x.valuation) with hn
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := Int.toNat (-Padic.valuation x)
hn : n = Int.toNat (-Padic.valuation x)
⊢ ∃ x_1, x * ↑(algebraMap ℤ_[p] ℚ_[p]) ↑x_1.snd = ↑(algebraMap ℤ_[p] ℚ_[p]) x_1.fst
[PROOFSTEP]
have hn_coe : (n : ℤ) = -x.valuation := by
  rw [hn, Int.toNat_of_nonneg]
  rw [Right.nonneg_neg_iff]
  rw [Padic.norm_le_one_iff_val_nonneg, not_le] at hx
  exact hx.le
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := Int.toNat (-Padic.valuation x)
hn : n = Int.toNat (-Padic.valuation x)
⊢ ↑n = -Padic.valuation x
[PROOFSTEP]
rw [hn, Int.toNat_of_nonneg]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := Int.toNat (-Padic.valuation x)
hn : n = Int.toNat (-Padic.valuation x)
⊢ 0 ≤ -Padic.valuation x
[PROOFSTEP]
rw [Right.nonneg_neg_iff]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := Int.toNat (-Padic.valuation x)
hn : n = Int.toNat (-Padic.valuation x)
⊢ Padic.valuation x ≤ 0
[PROOFSTEP]
rw [Padic.norm_le_one_iff_val_nonneg, not_le] at hx
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : Padic.valuation x < 0
n : ℕ := Int.toNat (-Padic.valuation x)
hn : n = Int.toNat (-Padic.valuation x)
⊢ Padic.valuation x ≤ 0
[PROOFSTEP]
exact hx.le
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := Int.toNat (-Padic.valuation x)
hn : n = Int.toNat (-Padic.valuation x)
hn_coe : ↑n = -Padic.valuation x
⊢ ∃ x_1, x * ↑(algebraMap ℤ_[p] ℚ_[p]) ↑x_1.snd = ↑(algebraMap ℤ_[p] ℚ_[p]) x_1.fst
[PROOFSTEP]
set a := x * (p : ℚ_[p]) ^ n with ha
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := Int.toNat (-Padic.valuation x)
hn : n = Int.toNat (-Padic.valuation x)
hn_coe : ↑n = -Padic.valuation x
a : ℚ_[p] := x * ↑p ^ n
ha : a = x * ↑p ^ n
⊢ ∃ x_1, x * ↑(algebraMap ℤ_[p] ℚ_[p]) ↑x_1.snd = ↑(algebraMap ℤ_[p] ℚ_[p]) x_1.fst
[PROOFSTEP]
have ha_norm : ‖a‖ = 1 :=
  by
  have hx : x ≠ 0 := by
    intro h0
    rw [h0, norm_zero] at hx
    exact hx zero_le_one
  rw [ha, padicNormE.mul, padicNormE.norm_p_pow, Padic.norm_eq_pow_val hx, ← zpow_add', hn_coe, neg_neg, add_left_neg,
    zpow_zero]
  exact Or.inl (Nat.cast_ne_zero.mpr (NeZero.ne p))
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := Int.toNat (-Padic.valuation x)
hn : n = Int.toNat (-Padic.valuation x)
hn_coe : ↑n = -Padic.valuation x
a : ℚ_[p] := x * ↑p ^ n
ha : a = x * ↑p ^ n
⊢ ‖a‖ = 1
[PROOFSTEP]
have hx : x ≠ 0 := by
  intro h0
  rw [h0, norm_zero] at hx
  exact hx zero_le_one
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := Int.toNat (-Padic.valuation x)
hn : n = Int.toNat (-Padic.valuation x)
hn_coe : ↑n = -Padic.valuation x
a : ℚ_[p] := x * ↑p ^ n
ha : a = x * ↑p ^ n
⊢ x ≠ 0
[PROOFSTEP]
intro h0
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := Int.toNat (-Padic.valuation x)
hn : n = Int.toNat (-Padic.valuation x)
hn_coe : ↑n = -Padic.valuation x
a : ℚ_[p] := x * ↑p ^ n
ha : a = x * ↑p ^ n
h0 : x = 0
⊢ False
[PROOFSTEP]
rw [h0, norm_zero] at hx
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬0 ≤ 1
n : ℕ := Int.toNat (-Padic.valuation x)
hn : n = Int.toNat (-Padic.valuation x)
hn_coe : ↑n = -Padic.valuation x
a : ℚ_[p] := x * ↑p ^ n
ha : a = x * ↑p ^ n
h0 : x = 0
⊢ False
[PROOFSTEP]
exact hx zero_le_one
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx✝ : ¬‖x‖ ≤ 1
n : ℕ := Int.toNat (-Padic.valuation x)
hn : n = Int.toNat (-Padic.valuation x)
hn_coe : ↑n = -Padic.valuation x
a : ℚ_[p] := x * ↑p ^ n
ha : a = x * ↑p ^ n
hx : x ≠ 0
⊢ ‖a‖ = 1
[PROOFSTEP]
rw [ha, padicNormE.mul, padicNormE.norm_p_pow, Padic.norm_eq_pow_val hx, ← zpow_add', hn_coe, neg_neg, add_left_neg,
  zpow_zero]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx✝ : ¬‖x‖ ≤ 1
n : ℕ := Int.toNat (-Padic.valuation x)
hn : n = Int.toNat (-Padic.valuation x)
hn_coe : ↑n = -Padic.valuation x
a : ℚ_[p] := x * ↑p ^ n
ha : a = x * ↑p ^ n
hx : x ≠ 0
⊢ ↑p ≠ 0 ∨ -Padic.valuation x + -↑n ≠ 0 ∨ -Padic.valuation x = 0 ∧ -↑n = 0
[PROOFSTEP]
exact Or.inl (Nat.cast_ne_zero.mpr (NeZero.ne p))
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := Int.toNat (-Padic.valuation x)
hn : n = Int.toNat (-Padic.valuation x)
hn_coe : ↑n = -Padic.valuation x
a : ℚ_[p] := x * ↑p ^ n
ha : a = x * ↑p ^ n
ha_norm : ‖a‖ = 1
⊢ ∃ x_1, x * ↑(algebraMap ℤ_[p] ℚ_[p]) ↑x_1.snd = ↑(algebraMap ℤ_[p] ℚ_[p]) x_1.fst
[PROOFSTEP]
use(⟨a, le_of_eq ha_norm⟩, ⟨(p ^ n : ℤ_[p]), mem_nonZeroDivisors_iff_ne_zero.mpr (NeZero.ne _)⟩)
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := Int.toNat (-Padic.valuation x)
hn : n = Int.toNat (-Padic.valuation x)
hn_coe : ↑n = -Padic.valuation x
a : ℚ_[p] := x * ↑p ^ n
ha : a = x * ↑p ^ n
ha_norm : ‖a‖ = 1
⊢ x *
      ↑(algebraMap ℤ_[p] ℚ_[p])
        ↑({ val := a, property := (_ : ‖a‖ ≤ 1) },
              { val := ↑(p ^ n), property := (_ : ↑(p ^ n) ∈ nonZeroDivisors ℤ_[p]) }).snd =
    ↑(algebraMap ℤ_[p] ℚ_[p])
      ({ val := a, property := (_ : ‖a‖ ≤ 1) },
          { val := ↑(p ^ n), property := (_ : ↑(p ^ n) ∈ nonZeroDivisors ℤ_[p]) }).fst
[PROOFSTEP]
simp only [map_pow, map_natCast, algebraMap_apply, PadicInt.coe_pow, PadicInt.coe_nat_cast, Subtype.coe_mk,
  Nat.cast_pow]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∀ {x y : ℤ_[p]}, ↑(algebraMap ℤ_[p] ℚ_[p]) x = ↑(algebraMap ℤ_[p] ℚ_[p]) y ↔ ∃ c, ↑c * x = ↑c * y
[PROOFSTEP]
simp_rw [algebraMap_apply, Subtype.coe_inj]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∀ {x y : ℤ_[p]}, x = y ↔ ∃ c, ↑c * x = ↑c * y
[PROOFSTEP]
refine ⟨fun h => ⟨1, by rw [h]⟩, ?_⟩
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y✝ : ℤ_[p]
h : x✝ = y✝
⊢ ↑1 * x✝ = ↑1 * y✝
[PROOFSTEP]
rw [h]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y✝ : ℤ_[p]
⊢ (∃ c, ↑c * x✝ = ↑c * y✝) → x✝ = y✝
[PROOFSTEP]
rintro ⟨⟨c, hc⟩, h⟩
[GOAL]
case intro.mk
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y✝ c : ℤ_[p]
hc : c ∈ nonZeroDivisors ℤ_[p]
h : ↑{ val := c, property := hc } * x✝ = ↑{ val := c, property := hc } * y✝
⊢ x✝ = y✝
[PROOFSTEP]
exact (mul_eq_mul_left_iff.mp h).resolve_right (mem_nonZeroDivisors_iff_ne_zero.mp hc)


[GOAL]
x : { x // x ∈ 𝓞 ℚ }
⊢ IsUnit x ↔ ↑x = 1 ∨ ↑x = -1
[PROOFSTEP]
simp_rw [(isUnit_map_iff (Rat.ringOfIntegersEquiv : 𝓞 ℚ →+* ℤ) x).symm, Int.isUnit_iff, RingEquiv.coe_toRingHom,
  RingEquiv.map_eq_one_iff, RingEquiv.map_eq_neg_one_iff, ← Subtype.coe_injective.eq_iff]
[GOAL]
x : { x // x ∈ 𝓞 ℚ }
⊢ ↑x = ↑1 ∨ ↑x = ↑(-1) ↔ ↑x = 1 ∨ ↑x = -1
[PROOFSTEP]
rfl
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : { x // x ∈ 𝓞 K }
⊢ IsUnit x ↔ |↑(↑(RingOfIntegers.norm ℚ) x)| = 1
[PROOFSTEP]
convert (RingOfIntegers.isUnit_norm ℚ (F := K)).symm
[GOAL]
case h.e'_2.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : { x // x ∈ 𝓞 K }
⊢ |↑(↑(RingOfIntegers.norm ℚ) x)| = 1 ↔ IsUnit (↑(RingOfIntegers.norm ℚ) x)
[PROOFSTEP]
rw [← abs_one, abs_eq_abs, ← Rat.RingOfIntegers.isUnit_iff]
[GOAL]
K : Type u_1
inst✝ : Field K
x✝¹ x✝ : { x // x ∈ 𝓞 K }ˣ
h : (fun x => ↑↑x) x✝¹ = (fun x => ↑↑x) x✝
⊢ x✝¹ = x✝
[PROOFSTEP]
rwa [SetLike.coe_eq_coe, Units.eq_iff] at h
[GOAL]
K : Type u_1
inst✝ : Field K
x : { x // x ∈ 𝓞 K }ˣ
n : ℕ
⊢ ↑↑(x ^ n) = ↑↑x ^ n
[PROOFSTEP]
rw [← SubmonoidClass.coe_pow, ← val_pow_eq_pow_val]
[GOAL]
K : Type u_1
inst✝ : Field K
x : { x // x ∈ 𝓞 K }ˣ
n : ℤ
⊢ ↑↑(x ^ n) = ↑↑x ^ n
[PROOFSTEP]
change ((Units.coeHom K).comp (map (algebraMap (𝓞 K) K))) (x ^ n) = _
[GOAL]
K : Type u_1
inst✝ : Field K
x : { x // x ∈ 𝓞 K }ˣ
n : ℤ
⊢ ↑(MonoidHom.comp (coeHom K) (map ↑(algebraMap { x // x ∈ 𝓞 K } K))) (x ^ n) = ↑↑x ^ n
[PROOFSTEP]
exact map_zpow _ x n
[GOAL]
K : Type u_1
inst✝¹ : Field K
x : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
⊢ x ∈ torsion K ↔ ∀ (w : InfinitePlace K), ↑w ↑↑x = 1
[PROOFSTEP]
rw [eq_iff_eq (x : K) 1, torsion, CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one]
[GOAL]
K : Type u_1
inst✝¹ : Field K
x : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
⊢ (∃ n, 0 < n ∧ x ^ n = 1) ↔ ∀ (φ : K →+* ℂ), ‖↑φ ↑↑x‖ = 1
[PROOFSTEP]
refine ⟨fun ⟨n, h_pos, h_eq⟩ φ => ?_, fun h => ?_⟩
[GOAL]
case refine_1
K : Type u_1
inst✝¹ : Field K
x : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
x✝ : ∃ n, 0 < n ∧ x ^ n = 1
φ : K →+* ℂ
n : ℕ
h_pos : 0 < n
h_eq : x ^ n = 1
⊢ ‖↑φ ↑↑x‖ = 1
[PROOFSTEP]
refine norm_map_one_of_pow_eq_one φ.toMonoidHom (k := ⟨n, h_pos⟩) ?_
[GOAL]
case refine_1
K : Type u_1
inst✝¹ : Field K
x : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
x✝ : ∃ n, 0 < n ∧ x ^ n = 1
φ : K →+* ℂ
n : ℕ
h_pos : 0 < n
h_eq : x ^ n = 1
⊢ ↑↑x ^ ↑{ val := n, property := h_pos } = 1
[PROOFSTEP]
rw [PNat.mk_coe, ← coe_pow, h_eq, coe_one]
[GOAL]
case refine_2
K : Type u_1
inst✝¹ : Field K
x : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
h : ∀ (φ : K →+* ℂ), ‖↑φ ↑↑x‖ = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
[PROOFSTEP]
obtain ⟨n, hn, hx⟩ := Embeddings.pow_eq_one_of_norm_eq_one K ℂ x.val.prop h
[GOAL]
case refine_2.intro.intro
K : Type u_1
inst✝¹ : Field K
x : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
h : ∀ (φ : K →+* ℂ), ‖↑φ ↑↑x‖ = 1
n : ℕ
hn : 0 < n
hx : ↑↑x ^ n = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
[PROOFSTEP]
exact ⟨n, hn, by ext; rw [coe_pow, hx, coe_one]⟩
[GOAL]
K : Type u_1
inst✝¹ : Field K
x : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
h : ∀ (φ : K →+* ℂ), ‖↑φ ↑↑x‖ = 1
n : ℕ
hn : 0 < n
hx : ↑↑x ^ n = 1
⊢ x ^ n = 1
[PROOFSTEP]
ext
[GOAL]
case a.a
K : Type u_1
inst✝¹ : Field K
x : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
h : ∀ (φ : K →+* ℂ), ‖↑φ ↑↑x‖ = 1
n : ℕ
hn : 0 < n
hx : ↑↑x ^ n = 1
⊢ ↑↑(x ^ n) = ↑↑1
[PROOFSTEP]
rw [coe_pow, hx, coe_one]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Fintype { x // x ∈ torsion K }
[PROOFSTEP]
refine @Fintype.ofFinite _ (Set.finite_coe_iff.mpr ?_)
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Set.Finite ↑(torsion K)
[PROOFSTEP]
refine Set.Finite.of_finite_image ?_ ((coe_injective K).injOn _)
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Set.Finite ((fun x => ↑↑x) '' ↑(torsion K))
[PROOFSTEP]
refine (Embeddings.finite_of_norm_le K ℂ 1).subset (fun a ⟨u, ⟨h_tors, h_ua⟩⟩ => ⟨?_, fun φ => ?_⟩)
[GOAL]
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : K
x✝ : a ∈ (fun x => ↑↑x) '' ↑(torsion K)
u : { x // x ∈ 𝓞 K }ˣ
h_tors : u ∈ ↑(torsion K)
h_ua : (fun x => ↑↑x) u = a
⊢ IsIntegral ℤ a
[PROOFSTEP]
rw [← h_ua]
[GOAL]
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : K
x✝ : a ∈ (fun x => ↑↑x) '' ↑(torsion K)
u : { x // x ∈ 𝓞 K }ˣ
h_tors : u ∈ ↑(torsion K)
h_ua : (fun x => ↑↑x) u = a
⊢ IsIntegral ℤ ((fun x => ↑↑x) u)
[PROOFSTEP]
exact u.val.prop
[GOAL]
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : K
x✝ : a ∈ (fun x => ↑↑x) '' ↑(torsion K)
u : { x // x ∈ 𝓞 K }ˣ
h_tors : u ∈ ↑(torsion K)
h_ua : (fun x => ↑↑x) u = a
φ : K →+* ℂ
⊢ ‖↑φ a‖ ≤ 1
[PROOFSTEP]
rw [← h_ua]
[GOAL]
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : K
x✝ : a ∈ (fun x => ↑↑x) '' ↑(torsion K)
u : { x // x ∈ 𝓞 K }ˣ
h_tors : u ∈ ↑(torsion K)
h_ua : (fun x => ↑↑x) u = a
φ : K →+* ℂ
⊢ ‖↑φ ((fun x => ↑↑x) u)‖ ≤ 1
[PROOFSTEP]
exact
  le_of_eq
    ((eq_iff_eq _ 1).mp ((mem_torsion K).mp h_tors) φ)
      -- a shortcut instance to stop the next instance from timing out
[GOAL]
K : Type u_1
inst✝¹ : Field K
ζ : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
k : ℕ+
hc : Nat.coprime ↑k ↑(torsion_order K)
⊢ ζ ∈ rootsOfUnity k { x // x ∈ 𝓞 K } ↔ ζ = 1
[PROOFSTEP]
rw [mem_rootsOfUnity]
[GOAL]
K : Type u_1
inst✝¹ : Field K
ζ : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
k : ℕ+
hc : Nat.coprime ↑k ↑(torsion_order K)
⊢ ζ ^ ↑k = 1 ↔ ζ = 1
[PROOFSTEP]
refine ⟨fun h => ?_, fun h => by rw [h, one_pow]⟩
[GOAL]
K : Type u_1
inst✝¹ : Field K
ζ : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
k : ℕ+
hc : Nat.coprime ↑k ↑(torsion_order K)
h : ζ = 1
⊢ ζ ^ ↑k = 1
[PROOFSTEP]
rw [h, one_pow]
[GOAL]
K : Type u_1
inst✝¹ : Field K
ζ : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
k : ℕ+
hc : Nat.coprime ↑k ↑(torsion_order K)
h : ζ ^ ↑k = 1
⊢ ζ = 1
[PROOFSTEP]
refine orderOf_eq_one_iff.mp (Nat.eq_one_of_dvd_coprimes hc ?_ ?_)
[GOAL]
case refine_1
K : Type u_1
inst✝¹ : Field K
ζ : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
k : ℕ+
hc : Nat.coprime ↑k ↑(torsion_order K)
h : ζ ^ ↑k = 1
⊢ orderOf ζ ∣ ↑k
[PROOFSTEP]
exact orderOf_dvd_of_pow_eq_one h
[GOAL]
case refine_2
K : Type u_1
inst✝¹ : Field K
ζ : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
k : ℕ+
hc : Nat.coprime ↑k ↑(torsion_order K)
h : ζ ^ ↑k = 1
⊢ orderOf ζ ∣ ↑(torsion_order K)
[PROOFSTEP]
have hζ : ζ ∈ torsion K := by
  rw [torsion, CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one]
  exact ⟨k, k.prop, h⟩
[GOAL]
K : Type u_1
inst✝¹ : Field K
ζ : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
k : ℕ+
hc : Nat.coprime ↑k ↑(torsion_order K)
h : ζ ^ ↑k = 1
⊢ ζ ∈ torsion K
[PROOFSTEP]
rw [torsion, CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one]
[GOAL]
K : Type u_1
inst✝¹ : Field K
ζ : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
k : ℕ+
hc : Nat.coprime ↑k ↑(torsion_order K)
h : ζ ^ ↑k = 1
⊢ ∃ n, 0 < n ∧ ζ ^ n = 1
[PROOFSTEP]
exact ⟨k, k.prop, h⟩
[GOAL]
case refine_2
K : Type u_1
inst✝¹ : Field K
ζ : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
k : ℕ+
hc : Nat.coprime ↑k ↑(torsion_order K)
h : ζ ^ ↑k = 1
hζ : ζ ∈ torsion K
⊢ orderOf ζ ∣ ↑(torsion_order K)
[PROOFSTEP]
rw [orderOf_submonoid (⟨ζ, hζ⟩ : torsion K)]
[GOAL]
case refine_2
K : Type u_1
inst✝¹ : Field K
ζ : { x // x ∈ 𝓞 K }ˣ
inst✝ : NumberField K
k : ℕ+
hc : Nat.coprime ↑k ↑(torsion_order K)
h : ζ ^ ↑k = 1
hζ : ζ ∈ torsion K
⊢ orderOf { val := ζ, property := hζ } ∣ ↑(torsion_order K)
[PROOFSTEP]
exact orderOf_dvd_card_univ
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ rootsOfUnity (torsion_order K) { x // x ∈ 𝓞 K } = torsion K
[PROOFSTEP]
ext ζ
[GOAL]
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : { x // x ∈ 𝓞 K }ˣ
⊢ ζ ∈ rootsOfUnity (torsion_order K) { x // x ∈ 𝓞 K } ↔ ζ ∈ torsion K
[PROOFSTEP]
rw [torsion, mem_rootsOfUnity]
[GOAL]
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : { x // x ∈ 𝓞 K }ˣ
⊢ ζ ^ ↑(torsion_order K) = 1 ↔ ζ ∈ CommGroup.torsion { x // x ∈ 𝓞 K }ˣ
[PROOFSTEP]
refine ⟨fun h => ?_, fun h => ?_⟩
[GOAL]
case h.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : { x // x ∈ 𝓞 K }ˣ
h : ζ ^ ↑(torsion_order K) = 1
⊢ ζ ∈ CommGroup.torsion { x // x ∈ 𝓞 K }ˣ
[PROOFSTEP]
rw [CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one]
[GOAL]
case h.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : { x // x ∈ 𝓞 K }ˣ
h : ζ ^ ↑(torsion_order K) = 1
⊢ ∃ n, 0 < n ∧ ζ ^ n = 1
[PROOFSTEP]
exact ⟨↑(torsion_order K), (torsion_order K).prop, h⟩
[GOAL]
case h.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : { x // x ∈ 𝓞 K }ˣ
h : ζ ∈ CommGroup.torsion { x // x ∈ 𝓞 K }ˣ
⊢ ζ ^ ↑(torsion_order K) = 1
[PROOFSTEP]
exact Subtype.ext_iff.mp (@pow_card_eq_one (torsion K) _ ⟨ζ, h⟩ _)