[GOAL]
m n✝ a✝ b✝ c d : ℤ
a b n : ℕ
⊢ ↑a ≡ ↑b [ZMOD ↑n] ↔ a ≡ b [MOD n]
[PROOFSTEP]
unfold ModEq Nat.ModEq
[GOAL]
m n✝ a✝ b✝ c d : ℤ
a b n : ℕ
⊢ ↑a % ↑n = ↑b % ↑n ↔ a % n = b % n
[PROOFSTEP]
rw [← Int.ofNat_inj]
[GOAL]
m n✝ a✝ b✝ c d : ℤ
a b n : ℕ
⊢ ↑a % ↑n = ↑b % ↑n ↔ ↑(a % n) = ↑(b % n)
[PROOFSTEP]
simp [coe_nat_mod]
[GOAL]
m n a b c d : ℤ
⊢ a ≡ 0 [ZMOD n] ↔ n ∣ a
[PROOFSTEP]
rw [ModEq, zero_emod, dvd_iff_emod_eq_zero]
[GOAL]
m n a b c d : ℤ
⊢ a ≡ b [ZMOD n] ↔ n ∣ b - a
[PROOFSTEP]
rw [ModEq, eq_comm]
[GOAL]
m n a b c d : ℤ
⊢ b % n = a % n ↔ n ∣ b - a
[PROOFSTEP]
simp [emod_eq_emod_iff_emod_sub_eq_zero, dvd_iff_emod_eq_zero]
[GOAL]
m n✝ a✝ b✝ c d a b n : ℤ
⊢ a ≡ b [ZMOD n] ↔ ∃ t, b = a + n * t
[PROOFSTEP]
rw [modEq_iff_dvd]
[GOAL]
m n✝ a✝ b✝ c d a b n : ℤ
⊢ n ∣ b - a ↔ ∃ t, b = a + n * t
[PROOFSTEP]
exact exists_congr fun t => sub_eq_iff_eq_add'
[GOAL]
m n a b c d : ℤ
⊢ -a ≡ -b [ZMOD n] ↔ a ≡ b [ZMOD n]
[PROOFSTEP]
simp [-sub_neg_eq_add, neg_sub_neg, modEq_iff_dvd, dvd_sub_comm]
[GOAL]
m n a b c d : ℤ
⊢ a ≡ b [ZMOD -n] ↔ a ≡ b [ZMOD n]
[PROOFSTEP]
simp [modEq_iff_dvd]
[GOAL]
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
⊢ c * a ≡ c * b [ZMOD c * n]
[PROOFSTEP]
obtain hc | rfl | hc := lt_trichotomy c 0
[GOAL]
case inl
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
hc : c < 0
⊢ c * a ≡ c * b [ZMOD c * n]
[PROOFSTEP]
rw [← neg_modEq_neg, ← modEq_neg, ← neg_mul, ← neg_mul, ← neg_mul]
[GOAL]
case inl
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
hc : c < 0
⊢ -c * a ≡ -c * b [ZMOD -c * n]
[PROOFSTEP]
simp only [ModEq, mul_emod_mul_of_pos _ _ (neg_pos.2 hc), h.eq]
[GOAL]
case inr.inl
m n a b d : ℤ
h : a ≡ b [ZMOD n]
⊢ 0 * a ≡ 0 * b [ZMOD 0 * n]
[PROOFSTEP]
simp
[GOAL]
case inr.inr
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
hc : 0 < c
⊢ c * a ≡ c * b [ZMOD c * n]
[PROOFSTEP]
simp only [ModEq, mul_emod_mul_of_pos _ _ hc, h.eq]
[GOAL]
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
⊢ a * c ≡ b * c [ZMOD n * c]
[PROOFSTEP]
rw [mul_comm a, mul_comm b, mul_comm n]
[GOAL]
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
⊢ c * a ≡ c * b [ZMOD c * n]
[PROOFSTEP]
exact h.mul_left'
[GOAL]
m n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : c ≡ d [ZMOD n]
⊢ n ∣ b + d - (a + c)
[PROOFSTEP]
convert dvd_add h₁.dvd h₂.dvd using 1
[GOAL]
case h.e'_4
m n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : c ≡ d [ZMOD n]
⊢ b + d - (a + c) = b - a + (d - c)
[PROOFSTEP]
ring
[GOAL]
m n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : a + c ≡ b + d [ZMOD n]
⊢ d - c = b + d - (a + c) - (b - a)
[PROOFSTEP]
ring
[GOAL]
m n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : a + c ≡ b + d [ZMOD n]
this : d - c = b + d - (a + c) - (b - a)
⊢ n ∣ d - c
[PROOFSTEP]
rw [this]
[GOAL]
m n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : a + c ≡ b + d [ZMOD n]
this : d - c = b + d - (a + c) - (b - a)
⊢ n ∣ b + d - (a + c) - (b - a)
[PROOFSTEP]
exact dvd_sub h₂.dvd h₁.dvd
[GOAL]
m n a b c d : ℤ
h₁ : c ≡ d [ZMOD n]
h₂ : a + c ≡ b + d [ZMOD n]
⊢ a ≡ b [ZMOD n]
[PROOFSTEP]
rw [add_comm a, add_comm b] at h₂ 
[GOAL]
m n a b c d : ℤ
h₁ : c ≡ d [ZMOD n]
h₂ : c + a ≡ d + b [ZMOD n]
⊢ a ≡ b [ZMOD n]
[PROOFSTEP]
exact h₁.add_left_cancel h₂
[GOAL]
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
⊢ a + -a ≡ b + -b [ZMOD n]
[PROOFSTEP]
simp_rw [← sub_eq_add_neg, sub_self]
[GOAL]
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
⊢ 0 ≡ 0 [ZMOD n]
[PROOFSTEP]
rfl
[GOAL]
m n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : c ≡ d [ZMOD n]
⊢ a - c ≡ b - d [ZMOD n]
[PROOFSTEP]
rw [sub_eq_add_neg, sub_eq_add_neg]
[GOAL]
m n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : c ≡ d [ZMOD n]
⊢ a + -c ≡ b + -d [ZMOD n]
[PROOFSTEP]
exact h₁.add h₂.neg
[GOAL]
m✝ n a b c d : ℤ
m : ℕ
h : a ≡ b [ZMOD n]
⊢ a ^ m ≡ b ^ m [ZMOD n]
[PROOFSTEP]
induction' m with d hd
[GOAL]
case zero
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
⊢ a ^ Nat.zero ≡ b ^ Nat.zero [ZMOD n]
[PROOFSTEP]
rfl
[GOAL]
case succ
m n a b c d✝ : ℤ
h : a ≡ b [ZMOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [ZMOD n]
⊢ a ^ Nat.succ d ≡ b ^ Nat.succ d [ZMOD n]
[PROOFSTEP]
rw [pow_succ, pow_succ]
[GOAL]
case succ
m n a b c d✝ : ℤ
h : a ≡ b [ZMOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [ZMOD n]
⊢ a * a ^ d ≡ b * b ^ d [ZMOD n]
[PROOFSTEP]
exact h.mul hd
[GOAL]
m✝ n a b c d m : ℤ
h : a ≡ b [ZMOD m * n]
⊢ a ≡ b [ZMOD n]
[PROOFSTEP]
rw [modEq_iff_dvd] at *
[GOAL]
m✝ n a b c d m : ℤ
h : m * n ∣ b - a
⊢ n ∣ b - a
[PROOFSTEP]
exact (dvd_mul_left n m).trans h
[GOAL]
m n a b c d : ℤ
hm : 0 < m
h : a * c ≡ b * c [ZMOD m]
⊢ a ≡ b [ZMOD m / ↑(gcd m c)]
[PROOFSTEP]
letI d := gcd m c
[GOAL]
m n a b c d✝ : ℤ
hm : 0 < m
h : a * c ≡ b * c [ZMOD m]
d : ℕ := gcd m c
⊢ a ≡ b [ZMOD m / ↑(gcd m c)]
[PROOFSTEP]
have hmd := gcd_dvd_left m c
[GOAL]
m n a b c d✝ : ℤ
hm : 0 < m
h : a * c ≡ b * c [ZMOD m]
d : ℕ := gcd m c
hmd : ↑(gcd m c) ∣ m
⊢ a ≡ b [ZMOD m / ↑(gcd m c)]
[PROOFSTEP]
have hcd := gcd_dvd_right m c
[GOAL]
m n a b c d✝ : ℤ
hm : 0 < m
h : a * c ≡ b * c [ZMOD m]
d : ℕ := gcd m c
hmd : ↑(gcd m c) ∣ m
hcd : ↑(gcd m c) ∣ c
⊢ a ≡ b [ZMOD m / ↑(gcd m c)]
[PROOFSTEP]
rw [modEq_iff_dvd] at h ⊢
  -- porting note: removed `show` due to leanprover-community/mathlib4#3305
[GOAL]
m n a b c d✝ : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := gcd m c
hmd : ↑(gcd m c) ∣ m
hcd : ↑(gcd m c) ∣ c
⊢ m / ↑(gcd m c) ∣ b - a
[PROOFSTEP]
refine Int.dvd_of_dvd_mul_right_of_gcd_one (?_ : m / d ∣ c / d * (b - a)) ?_
[GOAL]
case refine_1
m n a b c d✝ : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := gcd m c
hmd : ↑(gcd m c) ∣ m
hcd : ↑(gcd m c) ∣ c
⊢ m / ↑d ∣ c / ↑d * (b - a)
[PROOFSTEP]
rw [mul_comm, ← Int.mul_ediv_assoc (b - a) hcd, sub_mul]
[GOAL]
case refine_1
m n a b c d✝ : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := gcd m c
hmd : ↑(gcd m c) ∣ m
hcd : ↑(gcd m c) ∣ c
⊢ m / ↑d ∣ (b * c - a * c) / ↑(gcd m c)
[PROOFSTEP]
exact Int.ediv_dvd_ediv hmd h
[GOAL]
case refine_2
m n a b c d✝ : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := gcd m c
hmd : ↑(gcd m c) ∣ m
hcd : ↑(gcd m c) ∣ c
⊢ gcd (m / ↑(gcd m c)) (c / ↑d) = 1
[PROOFSTEP]
rw [gcd_div hmd hcd, natAbs_ofNat, Nat.div_self (gcd_pos_of_ne_zero_left c hm.ne')]
[GOAL]
m n a b c d : ℤ
hm : 0 < m
h : c * a ≡ c * b [ZMOD m]
⊢ a * c ≡ b * c [ZMOD m]
[PROOFSTEP]
simpa [mul_comm] using h
[GOAL]
m n a b c d : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ a ≡ b [ZMOD m]
[PROOFSTEP]
convert h.mul_left'
[GOAL]
case h.e'_1
m n a b c d : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ m = ?m.21777 * (m / c)
[PROOFSTEP]
rwa [Int.mul_ediv_cancel']
[GOAL]
case h.e'_2
m n a b c d : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ a = c * (a / c)
[PROOFSTEP]
rwa [Int.mul_ediv_cancel']
[GOAL]
case h.e'_3
m n a b c d : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ b = c * (b / c)
[PROOFSTEP]
rwa [Int.mul_ediv_cancel']
[GOAL]
m n a b c d : ℤ
⊢ a ≡ b [ZMOD 0] ↔ a = b
[PROOFSTEP]
rw [ModEq, emod_zero, emod_zero]
[GOAL]
m n a b c d : ℤ
⊢ n ∣ n + a - a
[PROOFSTEP]
simp
[GOAL]
m n a b c d : ℤ
⊢ n ∣ a + n - a
[PROOFSTEP]
simp
[GOAL]
m✝ n✝ a✝ b✝ c d a b m n : ℤ
hmn : Nat.coprime (natAbs m) (natAbs n)
h : a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n]
⊢ a ≡ b [ZMOD m * n]
[PROOFSTEP]
rw [modEq_iff_dvd, modEq_iff_dvd] at h 
[GOAL]
m✝ n✝ a✝ b✝ c d a b m n : ℤ
hmn : Nat.coprime (natAbs m) (natAbs n)
h : m ∣ b - a ∧ n ∣ b - a
⊢ a ≡ b [ZMOD m * n]
[PROOFSTEP]
rw [modEq_iff_dvd, ← natAbs_dvd, ← dvd_natAbs, coe_nat_dvd, natAbs_mul]
[GOAL]
m✝ n✝ a✝ b✝ c d a b m n : ℤ
hmn : Nat.coprime (natAbs m) (natAbs n)
h : m ∣ b - a ∧ n ∣ b - a
⊢ natAbs m * natAbs n ∣ natAbs (b - a)
[PROOFSTEP]
refine' hmn.mul_dvd_of_dvd_of_dvd _ _
[GOAL]
case refine'_1
m✝ n✝ a✝ b✝ c d a b m n : ℤ
hmn : Nat.coprime (natAbs m) (natAbs n)
h : m ∣ b - a ∧ n ∣ b - a
⊢ natAbs m ∣ natAbs (b - a)
[PROOFSTEP]
rw [← coe_nat_dvd, natAbs_dvd, dvd_natAbs]
[GOAL]
case refine'_2
m✝ n✝ a✝ b✝ c d a b m n : ℤ
hmn : Nat.coprime (natAbs m) (natAbs n)
h : m ∣ b - a ∧ n ∣ b - a
⊢ natAbs n ∣ natAbs (b - a)
[PROOFSTEP]
rw [← coe_nat_dvd, natAbs_dvd, dvd_natAbs]
[GOAL]
case refine'_1
m✝ n✝ a✝ b✝ c d a b m n : ℤ
hmn : Nat.coprime (natAbs m) (natAbs n)
h : m ∣ b - a ∧ n ∣ b - a
⊢ m ∣ b - a
[PROOFSTEP]
tauto
[GOAL]
case refine'_2
m✝ n✝ a✝ b✝ c d a b m n : ℤ
hmn : Nat.coprime (natAbs m) (natAbs n)
h : m ∣ b - a ∧ n ∣ b - a
⊢ n ∣ b - a
[PROOFSTEP]
tauto
[GOAL]
m n a✝ b✝ c d : ℤ
a b : ℕ
⊢ ↑a * Nat.gcdA a b ≡ ↑(Nat.gcd a b) [ZMOD ↑b]
[PROOFSTEP]
rw [← add_zero ((a : ℤ) * _), Nat.gcd_eq_gcd_ab]
[GOAL]
m n a✝ b✝ c d : ℤ
a b : ℕ
⊢ ↑a * Nat.gcdA a b + 0 ≡ ↑a * Nat.gcdA a b + ↑b * Nat.gcdB a b [ZMOD ↑b]
[PROOFSTEP]
exact (dvd_mul_right _ _).zero_modEq_int.add_left _
[GOAL]
m n✝ a✝ b✝ c✝ d a b n c : ℤ
ha : a ≡ b [ZMOD n]
⊢ b + 0 ≡ b [ZMOD n]
[PROOFSTEP]
rw [add_zero]
[GOAL]
m n✝ a✝ b✝ c✝ d a b n c : ℤ
ha : a ≡ b [ZMOD n]
⊢ a - n * c ≡ b [ZMOD n]
[PROOFSTEP]
convert Int.modEq_add_fac (-c) ha using 1
[GOAL]
case h.e'_2
m n✝ a✝ b✝ c✝ d a b n c : ℤ
ha : a ≡ b [ZMOD n]
⊢ a - n * c = a + n * -c
[PROOFSTEP]
ring
[GOAL]
m n a✝ b✝ c d : ℤ
a b : ℕ
hab : Nat.coprime a b
hgcd : Nat.gcd a b = 1
⊢ ↑a * Nat.gcdA a b + ↑b * Nat.gcdB a b ≡ 1 [ZMOD ↑b]
[PROOFSTEP]
rw [← Nat.gcd_eq_gcd_ab, hgcd]
[GOAL]
m n a✝ b✝ c d : ℤ
a b : ℕ
hab : Nat.coprime a b
hgcd : Nat.gcd a b = 1
⊢ ↑1 ≡ 1 [ZMOD ↑b]
[PROOFSTEP]
rfl
[GOAL]
m n a✝ b✝ c d a b : ℤ
hb : 0 < b
⊢ a % b < b
[PROOFSTEP]
have : a % b < |b| := emod_lt _ (ne_of_gt hb)
[GOAL]
m n a✝ b✝ c d a b : ℤ
hb : 0 < b
this : a % b < |b|
⊢ a % b < b
[PROOFSTEP]
rwa [abs_of_pos hb] at this 
[GOAL]
m n a✝ b✝ c d a b : ℤ
hb : 0 < b
⊢ a % b ≡ a [ZMOD b]
[PROOFSTEP]
simp [ModEq]
[GOAL]
m n a✝ b✝ c d a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ ↑(natAbs z) < b ∧ ↑(natAbs z) ≡ a [ZMOD b]
[PROOFSTEP]
constructor
[GOAL]
case left
m n a✝ b✝ c d a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ ↑(natAbs z) < b
[PROOFSTEP]
rw [ofNat_natAbs_eq_of_nonneg z hz1]
[GOAL]
case right
m n a✝ b✝ c d a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ ↑(natAbs z) ≡ a [ZMOD b]
[PROOFSTEP]
rw [ofNat_natAbs_eq_of_nonneg z hz1]
[GOAL]
case left
m n a✝ b✝ c d a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ z < b
[PROOFSTEP]
assumption
[GOAL]
case right
m n a✝ b✝ c d a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ z ≡ a [ZMOD b]
[PROOFSTEP]
assumption
