Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
/-
Copyright (c) 2018 Chris Hughes. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Hughes

! This file was ported from Lean 3 source module data.int.modeq
! leanprover-community/mathlib commit 47a1a73351de8dd6c8d3d32b569c8e434b03ca47
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Std.Data.Int.DivMod
import Mathlib.Data.Nat.ModEq
import Mathlib.Tactic.Ring

/-!

# Congruences modulo an integer

This file defines the equivalence relation `a ≡ b [ZMOD n]` on the integers, similarly to how
`Data.Nat.ModEq` defines them for the natural numbers. The notation is short for `n.ModEq a b`,
which is defined to be `a % n = b % n` for integers `a b n`.

## Tags

modeq, congruence, mod, MOD, modulo, integers

-/


namespace Int

/-- `a ≡ b [ZMOD n]` when `a % n = b % n`. -/
def 
ModEq: (n a b : ℤ) → ?m.9 n a b
ModEq
(n a b :
ℤ: Type
ℤ
) := a % n = b % n #align int.modeq
Int.ModEq: ℤ → ℤ → ℤ → Prop
Int.ModEq
@[inherit_doc] notation:50
a: ?m.2411
a
" ≡ "
b: ?m.2402
b
" [ZMOD "
n: ?m.2418
n
"]" =>
ModEq: ℤ → ℤ → ℤ → Prop
ModEq
n: ?m.3160
n
a: ?m.3153
a
b: ?m.2402
b
variable {m n a b c d :
ℤ: Type
ℤ
} -- Porting note: This instance should be derivable automatically
instance: {n a b : ℤ} → Decidable (a ≡ b [ZMOD n])
instance
:
Decidable: Prop → Type
Decidable
(
ModEq: ℤ → ℤ → ℤ → Prop
ModEq
n a b) :=
decEq: {α : Sort ?u.8789} → [inst : DecidableEq α] → (a b : α) → Decidable (a = b)
decEq
(a % n) (b % n) namespace ModEq @[refl] protected theorem
refl: ∀ {n : ℤ} (a : ℤ), a ≡ a [ZMOD n]
refl
(a :
ℤ: Type
ℤ
) : a ≡ a [ZMOD n] := @
rfl: ∀ {α : Sort ?u.8988} {a : α}, a = a
rfl
_: Sort ?u.8988
_
_: ?m.8989
_
#align int.modeq.refl
Int.ModEq.refl: ∀ {n : ℤ} (a : ℤ), a ≡ a [ZMOD n]
Int.ModEq.refl
protected theorem
rfl: a ≡ a [ZMOD n]
rfl
: a ≡ a [ZMOD n] :=
ModEq.refl: ∀ {n : ℤ} (a : ℤ), a ≡ a [ZMOD n]
ModEq.refl
_ #align int.modeq.rfl
Int.ModEq.rfl: ∀ {n a : ℤ}, a ≡ a [ZMOD n]
Int.ModEq.rfl
instance: ∀ {n : ℤ}, IsRefl ℤ (ModEq n)
instance
:
IsRefl: (α : Type ?u.9033) → (α → α → Prop) → Prop
IsRefl
_: Type ?u.9033
_
(
ModEq: ℤ → ℤ → ℤ → Prop
ModEq
n) := ⟨
ModEq.refl: ∀ {n : ℤ} (a : ℤ), a ≡ a [ZMOD n]
ModEq.refl
⟩ @[symm] protected theorem
symm: a ≡ b [ZMOD n] → b ≡ a [ZMOD n]
symm
: a ≡ b [ZMOD n] → b ≡ a [ZMOD n] :=
Eq.symm: ∀ {α : Sort ?u.9094} {a b : α}, a = b → b = a
Eq.symm
#align int.modeq.symm
Int.ModEq.symm: ∀ {n a b : ℤ}, a ≡ b [ZMOD n] → b ≡ a [ZMOD n]
Int.ModEq.symm
@[trans] protected theorem
trans: a ≡ b [ZMOD n] → b ≡ c [ZMOD n] → a ≡ c [ZMOD n]
trans
: a ≡ b [ZMOD n] → b ≡ c [ZMOD n] → a ≡ c [ZMOD n] :=
Eq.trans: ∀ {α : Sort ?u.9132} {a b c : α}, a = b → b = c → a = c
Eq.trans
#align int.modeq.trans
Int.ModEq.trans: ∀ {n a b c : ℤ}, a ≡ b [ZMOD n] → b ≡ c [ZMOD n] → a ≡ c [ZMOD n]
Int.ModEq.trans
instance: ∀ {n : ℤ}, IsTrans ℤ (ModEq n)
instance
:
IsTrans: (α : Type ?u.9170) → (α → α → Prop) → Prop
IsTrans
ℤ: Type
ℤ
(
ModEq: ℤ → ℤ → ℤ → Prop
ModEq
n) where trans := @
Int.ModEq.trans: ∀ {n a b c : ℤ}, a ≡ b [ZMOD n] → b ≡ c [ZMOD n] → a ≡ c [ZMOD n]
Int.ModEq.trans
n protected theorem
eq: a ≡ b [ZMOD n] → a % n = b % n
eq
: a ≡ b [ZMOD n] → a % n = b % n :=
id: ∀ {α : Sort ?u.9280}, α → α
id
#align int.modeq.eq
Int.ModEq.eq: ∀ {n a b : ℤ}, a ≡ b [ZMOD n] → a % n = b % n
Int.ModEq.eq
end ModEq theorem
modEq_comm: a ≡ b [ZMOD n] ↔ b ≡ a [ZMOD n]
modEq_comm
: a ≡ b [ZMOD n] ↔ b ≡ a [ZMOD n] := ⟨
ModEq.symm: ∀ {n a b : ℤ}, a ≡ b [ZMOD n] → b ≡ a [ZMOD n]
ModEq.symm
,
ModEq.symm: ∀ {n a b : ℤ}, a ≡ b [ZMOD n] → b ≡ a [ZMOD n]
ModEq.symm
⟩ #align int.modeq_comm
Int.modEq_comm: ∀ {n a b : ℤ}, a ≡ b [ZMOD n] ↔ b ≡ a [ZMOD n]
Int.modEq_comm
theorem
coe_nat_modEq_iff: ∀ {a b n : ℕ}, ↑a ≡ ↑b [ZMOD ↑n] ↔ a ≡ b [MOD n]
coe_nat_modEq_iff
{a b n :
ℕ: Type
ℕ
} : a ≡ b [ZMOD n] ↔ a ≡ b [MOD n] :=

Goals accomplished! 🐙
m, n✝, a✝, b✝, c, d: ℤ

a, b, n: ℕ


↑a ≡ ↑b [ZMOD ↑n] ↔ a ≡ b [MOD n]
m, n✝, a✝, b✝, c, d: ℤ

a, b, n: ℕ


↑a % ↑n = ↑b % ↑n ↔ a % n = b % n
m, n✝, a✝, b✝, c, d: ℤ

a, b, n: ℕ


↑a % ↑n = ↑b % ↑n ↔ a % n = b % n
m, n✝, a✝, b✝, c, d: ℤ

a, b, n: ℕ


↑a ≡ ↑b [ZMOD ↑n] ↔ a ≡ b [MOD n]
m, n✝, a✝, b✝, c, d: ℤ

a, b, n: ℕ


↑a % ↑n = ↑b % ↑n ↔ a % n = b % n
m, n✝, a✝, b✝, c, d: ℤ

a, b, n: ℕ


↑a % ↑n = ↑b % ↑n ↔ ↑(a % n) = ↑(b % n)
m, n✝, a✝, b✝, c, d: ℤ

a, b, n: ℕ


↑a % ↑n = ↑b % ↑n ↔ ↑(a % n) = ↑(b % n)
m, n✝, a✝, b✝, c, d: ℤ

a, b, n: ℕ


↑a % ↑n = ↑b % ↑n ↔ ↑(a % n) = ↑(b % n)
m, n✝, a✝, b✝, c, d: ℤ

a, b, n: ℕ


↑a ≡ ↑b [ZMOD ↑n] ↔ a ≡ b [MOD n]

Goals accomplished! 🐙
#align int.coe_nat_modeq_iff
Int.coe_nat_modEq_iff: ∀ {a b n : ℕ}, ↑a ≡ ↑b [ZMOD ↑n] ↔ a ≡ b [MOD n]
Int.coe_nat_modEq_iff
theorem
modEq_zero_iff_dvd: a ≡ 0 [ZMOD n] ↔ n ∣ a
modEq_zero_iff_dvd
: a ≡
0: ?m.9709
0
[ZMOD n] ↔ n ∣ a :=

Goals accomplished! 🐙
m, n, a, b, c, d: ℤ


m, n, a, b, c, d: ℤ


m, n, a, b, c, d: ℤ


a % n = 0 % n ↔ n ∣ a
m, n, a, b, c, d: ℤ


m, n, a, b, c, d: ℤ


a % n = 0 ↔ n ∣ a
m, n, a, b, c, d: ℤ


m, n, a, b, c, d: ℤ


a % n = 0 ↔ a % n = 0

Goals accomplished! 🐙
#align int.modeq_zero_iff_dvd
Int.modEq_zero_iff_dvd: ∀ {n a : ℤ}, a ≡ 0 [ZMOD n] ↔ n ∣ a
Int.modEq_zero_iff_dvd
theorem
_root_.Dvd.dvd.modEq_zero_int: n ∣ a → a ≡ 0 [ZMOD n]
_root_.Dvd.dvd.modEq_zero_int
(
h: n ∣ a
h
: n ∣ a) : a ≡
0: ?m.9806
0
[ZMOD n] :=
modEq_zero_iff_dvd: ∀ {n a : ℤ}, a ≡ 0 [ZMOD n] ↔ n ∣ a
modEq_zero_iff_dvd
.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
h: n ∣ a
h
#align has_dvd.dvd.modeq_zero_int
Dvd.dvd.modEq_zero_int: ∀ {n a : ℤ}, n ∣ a → a ≡ 0 [ZMOD n]
Dvd.dvd.modEq_zero_int
theorem
_root_.Dvd.dvd.zero_modEq_int: n ∣ a → 0 ≡ a [ZMOD n]
_root_.Dvd.dvd.zero_modEq_int
(
h: n ∣ a
h
: n ∣ a) :
0: ?m.9856
0
≡ a [ZMOD n] :=
h: n ∣ a
h
.
modEq_zero_int: ∀ {n a : ℤ}, n ∣ a → a ≡ 0 [ZMOD n]
modEq_zero_int
.
symm: ∀ {n a b : ℤ}, a ≡ b [ZMOD n] → b ≡ a [ZMOD n]
symm
#align has_dvd.dvd.zero_modeq_int
Dvd.dvd.zero_modEq_int: ∀ {n a : ℤ}, n ∣ a → 0 ≡ a [ZMOD n]
Dvd.dvd.zero_modEq_int
theorem
modEq_iff_dvd: ∀ {n a b : ℤ}, a ≡ b [ZMOD n] ↔ n ∣ b - a
modEq_iff_dvd
: a ≡ b [ZMOD n] ↔ n ∣ b - a :=

Goals accomplished! 🐙
m, n, a, b, c, d: ℤ


m, n, a, b, c, d: ℤ


m, n, a, b, c, d: ℤ


a % n = b % n ↔ n ∣ b - a
m, n, a, b, c, d: ℤ


m, n, a, b, c, d: ℤ


b % n = a % n ↔ n ∣ b - a
m, n, a, b, c, d: ℤ


b % n = a % n ↔ n ∣ b - a
m, n, a, b, c, d: ℤ



Goals accomplished! 🐙
#align int.modeq_iff_dvd
Int.modEq_iff_dvd: ∀ {n a b : ℤ}, a ≡ b [ZMOD n] ↔ n ∣ b - a
Int.modEq_iff_dvd
theorem
modEq_iff_add_fac: ∀ {a b n : ℤ}, a ≡ b [ZMOD n] ↔ ∃ t, b = a + n * t
modEq_iff_add_fac
{a b n :
ℤ: Type
ℤ
} : a ≡ b [ZMOD n] ↔ ∃
t: ?m.10300
t
, b = a + n *
t: ?m.10300
t
:=

Goals accomplished! 🐙
m, n✝, a✝, b✝, c, d, a, b, n: ℤ


a ≡ b [ZMOD n] ↔ ∃ t, b = a + n * t
m, n✝, a✝, b✝, c, d, a, b, n: ℤ


a ≡ b [ZMOD n] ↔ ∃ t, b = a + n * t
m, n✝, a✝, b✝, c, d, a, b, n: ℤ


n ∣ b - a ↔ ∃ t, b = a + n * t
m, n✝, a✝, b✝, c, d, a, b, n: ℤ


n ∣ b - a ↔ ∃ t, b = a + n * t
m, n✝, a✝, b✝, c, d, a, b, n: ℤ


a ≡ b [ZMOD n] ↔ ∃ t, b = a + n * t

Goals accomplished! 🐙
#align int.modeq_iff_add_fac
Int.modEq_iff_add_fac: ∀ {a b n : ℤ}, a ≡ b [ZMOD n] ↔ ∃ t, b = a + n * t
Int.modEq_iff_add_fac
alias
modEq_iff_dvd: ∀ {n a b : ℤ}, a ≡ b [ZMOD n] ↔ n ∣ b - a
modEq_iff_dvd
↔
ModEq.dvd: ∀ {n a b : ℤ}, a ≡ b [ZMOD n] → n ∣ b - a
ModEq.dvd
modEq_of_dvd: ∀ {n a b : ℤ}, n ∣ b - a → a ≡ b [ZMOD n]
modEq_of_dvd
#align int.modeq.dvd
Int.ModEq.dvd: ∀ {n a b : ℤ}, a ≡ b [ZMOD n] → n ∣ b - a
Int.ModEq.dvd
#align int.modeq_of_dvd
Int.modEq_of_dvd: ∀ {n a b : ℤ}, n ∣ b - a → a ≡ b [ZMOD n]
Int.modEq_of_dvd
theorem
mod_modEq: ∀ (a n : ℤ), a % n ≡ a [ZMOD n]
mod_modEq
(
a: ?m.10509
a
n: ?m.10512
n
) :
a: ?m.10509
a
%
n: ?m.10512
n
≡
a: ?m.10509
a
[ZMOD
n: ?m.10512
n
] :=
emod_emod: ∀ (a b : ℤ), a % b % b = a % b
emod_emod
_ _ #align int.mod_modeq
Int.mod_modEq: ∀ (a n : ℤ), a % n ≡ a [ZMOD n]
Int.mod_modEq
@[simp] theorem
neg_modEq_neg: ∀ {n a b : ℤ}, -a ≡ -b [ZMOD n] ↔ a ≡ b [ZMOD n]
neg_modEq_neg
: -a ≡ -b [ZMOD n] ↔ a ≡ b [ZMOD n] :=

Goals accomplished! 🐙
m, n, a, b, c, d: ℤ



Goals accomplished! 🐙
#align int.neg_modeq_neg
Int.neg_modEq_neg: ∀ {n a b : ℤ}, -a ≡ -b [ZMOD n] ↔ a ≡ b [ZMOD n]
Int.neg_modEq_neg
@[simp] theorem
modEq_neg: ∀ {n a b : ℤ}, a ≡ b [ZMOD -n] ↔ a ≡ b [ZMOD n]
modEq_neg
: a ≡ b [ZMOD -n] ↔ a ≡ b [ZMOD n] :=

Goals accomplished! 🐙
m, n, a, b, c, d: ℤ



Goals accomplished! 🐙
#align int.modeq_neg
Int.modEq_neg: ∀ {n a b : ℤ}, a ≡ b [ZMOD -n] ↔ a ≡ b [ZMOD n]
Int.modEq_neg
namespace ModEq protected theorem
of_dvd: m ∣ n → a ≡ b [ZMOD n] → a ≡ b [ZMOD m]
of_dvd
(
d: m ∣ n
d
: m ∣ n) (
h: a ≡ b [ZMOD n]
h
: a ≡ b [ZMOD n]) : a ≡ b [ZMOD m] :=
modEq_iff_dvd: ∀ {n a b : ℤ}, a ≡ b [ZMOD n] ↔ n ∣ b - a
modEq_iff_dvd
.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
<|
d: m ∣ n
d
.
trans: ∀ {α : Type ?u.14056} [inst : Semigroup α] {a b c : α}, a ∣ b → b ∣ c → a ∣ c
trans
h: a ≡ b [ZMOD n]
h
.
dvd: ∀ {n a b : ℤ}, a ≡ b [ZMOD n] → n ∣ b - a
dvd
#align int.modeq.of_dvd
Int.ModEq.of_dvd: ∀ {m n a b : ℤ}, m ∣ n → a ≡ b [ZMOD n] → a ≡ b [ZMOD m]
Int.ModEq.of_dvd
protected theorem
mul_left': ∀ {n a b c : ℤ}, a ≡ b [ZMOD n] → c * a ≡ c * b [ZMOD c * n]
mul_left'
(
h: a ≡ b [ZMOD n]
h
: a ≡ b [ZMOD n]) : c * a ≡ c * b [ZMOD c * n] :=

Goals accomplished! 🐙
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]


c * a ≡ c * b [ZMOD c * n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]

hc: c < 0


inl
c * a ≡ c * b [ZMOD c * n]
m, n, a, b, d: ℤ

h: a ≡ b [ZMOD n]


inr.inl
0 * a ≡ 0 * b [ZMOD 0 * n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]

hc: 0 < c


inr.inr
c * a ≡ c * b [ZMOD c * n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]


c * a ≡ c * b [ZMOD c * n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]

hc: c < 0


inl
c * a ≡ c * b [ZMOD c * n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]

hc: c < 0


inl
c * a ≡ c * b [ZMOD c * n]
m, n, a, b, d: ℤ

h: a ≡ b [ZMOD n]


inr.inl
0 * a ≡ 0 * b [ZMOD 0 * n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]

hc: 0 < c


inr.inr
c * a ≡ c * b [ZMOD c * n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]

hc: c < 0


inl
c * a ≡ c * b [ZMOD c * n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]

hc: c < 0


inl
-(c * a) ≡ -(c * b) [ZMOD c * n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]

hc: c < 0


inl
c * a ≡ c * b [ZMOD c * n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]

hc: c < 0


inl
-(c * a) ≡ -(c * b) [ZMOD -(c * n)]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]

hc: c < 0


inl
c * a ≡ c * b [ZMOD c * n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]

hc: c < 0


inl
-(c * a) ≡ -(c * b) [ZMOD -c * n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]

hc: c < 0


inl
c * a ≡ c * b [ZMOD c * n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]

hc: c < 0


inl
-c * a ≡ -(c * b) [ZMOD -c * n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]

hc: c < 0


inl
c * a ≡ c * b [ZMOD c * n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]

hc: c < 0


inl
-c * a ≡ -c * b [ZMOD -c * n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]

hc: c < 0


inl
-c * a ≡ -c * b [ZMOD -c * n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]

hc: c < 0


inl
c * a ≡ c * b [ZMOD c * n]

Goals accomplished! 🐙
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]


c * a ≡ c * b [ZMOD c * n]
m, n, a, b, d: ℤ

h: a ≡ b [ZMOD n]


inr.inl
0 * a ≡ 0 * b [ZMOD 0 * n]
m, n, a, b, d: ℤ

h: a ≡ b [ZMOD n]


inr.inl
0 * a ≡ 0 * b [ZMOD 0 * n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]

hc: 0 < c


inr.inr
c * a ≡ c * b [ZMOD c * n]

Goals accomplished! 🐙
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]


c * a ≡ c * b [ZMOD c * n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]

hc: 0 < c


inr.inr
c * a ≡ c * b [ZMOD c * n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]

hc: 0 < c


inr.inr
c * a ≡ c * b [ZMOD c * n]

Goals accomplished! 🐙
#align int.modeq.mul_left'
Int.ModEq.mul_left': ∀ {n a b c : ℤ}, a ≡ b [ZMOD n] → c * a ≡ c * b [ZMOD c * n]
Int.ModEq.mul_left'
protected theorem
mul_right': ∀ {n a b c : ℤ}, a ≡ b [ZMOD n] → a * c ≡ b * c [ZMOD n * c]
mul_right'
(
h: a ≡ b [ZMOD n]
h
: a ≡ b [ZMOD n]) : a * c ≡ b * c [ZMOD n * c] :=

Goals accomplished! 🐙
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]


a * c ≡ b * c [ZMOD n * c]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]


a * c ≡ b * c [ZMOD n * c]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]


c * a ≡ b * c [ZMOD n * c]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]


a * c ≡ b * c [ZMOD n * c]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]


c * a ≡ c * b [ZMOD n * c]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]


a * c ≡ b * c [ZMOD n * c]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]


c * a ≡ c * b [ZMOD c * n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]


c * a ≡ c * b [ZMOD c * n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]


c * a ≡ c * b [ZMOD c * n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]


a * c ≡ b * c [ZMOD n * c]

Goals accomplished! 🐙
#align int.modeq.mul_right'
Int.ModEq.mul_right': ∀ {n a b c : ℤ}, a ≡ b [ZMOD n] → a * c ≡ b * c [ZMOD n * c]
Int.ModEq.mul_right'
protected theorem
add: ∀ {n a b c d : ℤ}, a ≡ b [ZMOD n] → c ≡ d [ZMOD n] → a + c ≡ b + d [ZMOD n]
add
(
h₁: a ≡ b [ZMOD n]
h₁
: a ≡ b [ZMOD n]) (
h₂: c ≡ d [ZMOD n]
h₂
: c ≡ d [ZMOD n]) : a + c ≡ b + d [ZMOD n] :=
modEq_iff_dvd: ∀ {n a b : ℤ}, a ≡ b [ZMOD n] ↔ n ∣ b - a
modEq_iff_dvd
.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
<|

Goals accomplished! 🐙
m, n, a, b, c, d: ℤ

h₁: a ≡ b [ZMOD n]

h₂: c ≡ d [ZMOD n]


n ∣ b + d - (a + c)
m, n, a, b, c, d: ℤ

h₁: a ≡ b [ZMOD n]

h₂: c ≡ d [ZMOD n]


h.e'_4
b + d - (a + c) = b - a + (d - c)
m, n, a, b, c, d: ℤ

h₁: a ≡ b [ZMOD n]

h₂: c ≡ d [ZMOD n]


n ∣ b + d - (a + c)

Goals accomplished! 🐙
#align int.modeq.add
Int.ModEq.add: ∀ {n a b c d : ℤ}, a ≡ b [ZMOD n] → c ≡ d [ZMOD n] → a + c ≡ b + d [ZMOD n]
Int.ModEq.add
protected theorem
add_left: ∀ (c : ℤ), a ≡ b [ZMOD n] → c + a ≡ c + b [ZMOD n]
add_left
(c :
ℤ: Type
ℤ
) (
h: a ≡ b [ZMOD n]
h
: a ≡ b [ZMOD n]) : c + a ≡ c + b [ZMOD n] :=
ModEq.rfl: ∀ {n a : ℤ}, a ≡ a [ZMOD n]
ModEq.rfl
.
add: ∀ {n a b c d : ℤ}, a ≡ b [ZMOD n] → c ≡ d [ZMOD n] → a + c ≡ b + d [ZMOD n]
add
h: a ≡ b [ZMOD n]
h
#align int.modeq.add_left
Int.ModEq.add_left: ∀ {n a b : ℤ} (c : ℤ), a ≡ b [ZMOD n] → c + a ≡ c + b [ZMOD n]
Int.ModEq.add_left
protected theorem
add_right: ∀ {n a b : ℤ} (c : ℤ), a ≡ b [ZMOD n] → a + c ≡ b + c [ZMOD n]
add_right
(c :
ℤ: Type
ℤ
) (
h: a ≡ b [ZMOD n]
h
: a ≡ b [ZMOD n]) : a + c ≡ b + c [ZMOD n] :=
h: a ≡ b [ZMOD n]
h
.
add: ∀ {n a b c d : ℤ}, a ≡ b [ZMOD n] → c ≡ d [ZMOD n] → a + c ≡ b + d [ZMOD n]
add
ModEq.rfl: ∀ {n a : ℤ}, a ≡ a [ZMOD n]
ModEq.rfl
#align int.modeq.add_right
Int.ModEq.add_right: ∀ {n a b : ℤ} (c : ℤ), a ≡ b [ZMOD n] → a + c ≡ b + c [ZMOD n]
Int.ModEq.add_right
protected theorem
add_left_cancel: ∀ {n a b c d : ℤ}, a ≡ b [ZMOD n] → a + c ≡ b + d [ZMOD n] → c ≡ d [ZMOD n]
add_left_cancel
(
h₁: a ≡ b [ZMOD n]
h₁
: a ≡ b [ZMOD n]) (
h₂: a + c ≡ b + d [ZMOD n]
h₂
: a + c ≡ b + d [ZMOD n]) : c ≡ d [ZMOD n] := have : d - c = b + d - (a + c) - (b - a) :=

Goals accomplished! 🐙
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)

Goals accomplished! 🐙
modEq_iff_dvd: ∀ {n a b : ℤ}, a ≡ b [ZMOD n] ↔ n ∣ b - a
modEq_iff_dvd
.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
<|

Goals accomplished! 🐙
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
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
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)
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)
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

Goals accomplished! 🐙
#align int.modeq.add_left_cancel
Int.ModEq.add_left_cancel: ∀ {n a b c d : ℤ}, a ≡ b [ZMOD n] → a + c ≡ b + d [ZMOD n] → c ≡ d [ZMOD n]
Int.ModEq.add_left_cancel
protected theorem
add_left_cancel': ∀ {n a b : ℤ} (c : ℤ), c + a ≡ c + b [ZMOD n] → a ≡ b [ZMOD n]
add_left_cancel'
(c :
ℤ: Type
ℤ
) (
h: c + a ≡ c + b [ZMOD n]
h
: c + a ≡ c + b [ZMOD n]) : a ≡ b [ZMOD n] :=
ModEq.rfl: ∀ {n a : ℤ}, a ≡ a [ZMOD n]
ModEq.rfl
.
add_left_cancel: ∀ {n a b c d : ℤ}, a ≡ b [ZMOD n] → a + c ≡ b + d [ZMOD n] → c ≡ d [ZMOD n]
add_left_cancel
h: c + a ≡ c + b [ZMOD n]
h
#align int.modeq.add_left_cancel'
Int.ModEq.add_left_cancel': ∀ {n a b : ℤ} (c : ℤ), c + a ≡ c + b [ZMOD n] → a ≡ b [ZMOD n]
Int.ModEq.add_left_cancel'
protected theorem
add_right_cancel: ∀ {n a b c d : ℤ}, c ≡ d [ZMOD n] → a + c ≡ b + d [ZMOD n] → a ≡ b [ZMOD n]
add_right_cancel
(
h₁: c ≡ d [ZMOD n]
h₁
: c ≡ d [ZMOD n]) (
h₂: a + c ≡ b + d [ZMOD n]
h₂
: a + c ≡ b + d [ZMOD n]) : a ≡ b [ZMOD n] :=

Goals accomplished! 🐙
m, n, a, b, c, d: ℤ

h₁: c ≡ d [ZMOD n]

h₂: a + c ≡ b + d [ZMOD n]


m, n, a, b, c, d: ℤ

h₁: c ≡ d [ZMOD n]

h₂: a + c ≡ b + d [ZMOD n]


m, n, a, b, c, d: ℤ

h₁: c ≡ d [ZMOD n]

h₂: c + a ≡ b + d [ZMOD n]


m, n, a, b, c, d: ℤ

h₁: c ≡ d [ZMOD n]

h₂: a + c ≡ b + d [ZMOD n]


m, n, a, b, c, d: ℤ

h₁: c ≡ d [ZMOD n]

h₂: c + a ≡ d + b [ZMOD n]


m, n, a, b, c, d: ℤ

h₁: c ≡ d [ZMOD n]

h₂: c + a ≡ d + b [ZMOD n]


m, n, a, b, c, d: ℤ

h₁: c ≡ d [ZMOD n]

h₂: c + a ≡ d + b [ZMOD n]


m, n, a, b, c, d: ℤ

h₁: c ≡ d [ZMOD n]

h₂: a + c ≡ b + d [ZMOD n]



Goals accomplished! 🐙
#align int.modeq.add_right_cancel
Int.ModEq.add_right_cancel: ∀ {n a b c d : ℤ}, c ≡ d [ZMOD n] → a + c ≡ b + d [ZMOD n] → a ≡ b [ZMOD n]
Int.ModEq.add_right_cancel
protected theorem
add_right_cancel': ∀ (c : ℤ), a + c ≡ b + c [ZMOD n] → a ≡ b [ZMOD n]
add_right_cancel'
(c :
ℤ: Type
ℤ
) (
h: a + c ≡ b + c [ZMOD n]
h
: a + c ≡ b + c [ZMOD n]) : a ≡ b [ZMOD n] :=
ModEq.rfl: ∀ {n a : ℤ}, a ≡ a [ZMOD n]
ModEq.rfl
.
add_right_cancel: ∀ {n a b c d : ℤ}, c ≡ d [ZMOD n] → a + c ≡ b + d [ZMOD n] → a ≡ b [ZMOD n]
add_right_cancel
h: a + c ≡ b + c [ZMOD n]
h
#align int.modeq.add_right_cancel'
Int.ModEq.add_right_cancel': ∀ {n a b : ℤ} (c : ℤ), a + c ≡ b + c [ZMOD n] → a ≡ b [ZMOD n]
Int.ModEq.add_right_cancel'
protected theorem
neg: a ≡ b [ZMOD n] → -a ≡ -b [ZMOD n]
neg
(
h: a ≡ b [ZMOD n]
h
: a ≡ b [ZMOD n]) : -a ≡ -b [ZMOD n] :=
h: a ≡ b [ZMOD n]
h
.
add_left_cancel: ∀ {n a b c d : ℤ}, a ≡ b [ZMOD n] → a + c ≡ b + d [ZMOD n] → c ≡ d [ZMOD n]
add_left_cancel
(

Goals accomplished! 🐙
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]


a + -a ≡ b + -b [ZMOD n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]


a + -a ≡ b + -b [ZMOD n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]


a - a ≡ b - b [ZMOD n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]


a + -a ≡ b + -b [ZMOD n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]


m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]


m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]


m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]


a + -a ≡ b + -b [ZMOD n]

Goals accomplished! 🐙
) #align int.modeq.neg
Int.ModEq.neg: ∀ {n a b : ℤ}, a ≡ b [ZMOD n] → -a ≡ -b [ZMOD n]
Int.ModEq.neg
protected theorem
sub: a ≡ b [ZMOD n] → c ≡ d [ZMOD n] → a - c ≡ b - d [ZMOD n]
sub
(
h₁: a ≡ b [ZMOD n]
h₁
: a ≡ b [ZMOD n]) (
h₂: c ≡ d [ZMOD n]
h₂
: c ≡ d [ZMOD n]) : a - c ≡ b - d [ZMOD n] :=

Goals accomplished! 🐙
m, n, a, b, c, d: ℤ

h₁: a ≡ b [ZMOD n]

h₂: c ≡ d [ZMOD n]


a - c ≡ b - d [ZMOD n]
m, n, a, b, c, d: ℤ

h₁: a ≡ b [ZMOD n]

h₂: c ≡ d [ZMOD n]


a - c ≡ b - d [ZMOD n]
m, n, a, b, c, d: ℤ

h₁: a ≡ b [ZMOD n]

h₂: c ≡ d [ZMOD n]


a + -c ≡ b - d [ZMOD n]
m, n, a, b, c, d: ℤ

h₁: a ≡ b [ZMOD n]

h₂: c ≡ d [ZMOD n]


a - c ≡ b - d [ZMOD n]
m, n, a, b, c, d: ℤ

h₁: a ≡ b [ZMOD n]

h₂: c ≡ d [ZMOD n]


a + -c ≡ b + -d [ZMOD n]
m, n, a, b, c, d: ℤ

h₁: a ≡ b [ZMOD n]

h₂: c ≡ d [ZMOD n]


a + -c ≡ b + -d [ZMOD n]
m, n, a, b, c, d: ℤ

h₁: a ≡ b [ZMOD n]

h₂: c ≡ d [ZMOD n]


a - c ≡ b - d [ZMOD n]

Goals accomplished! 🐙
#align int.modeq.sub
Int.ModEq.sub: ∀ {n a b c d : ℤ}, a ≡ b [ZMOD n] → c ≡ d [ZMOD n] → a - c ≡ b - d [ZMOD n]
Int.ModEq.sub
protected theorem
sub_left: ∀ (c : ℤ), a ≡ b [ZMOD n] → c - a ≡ c - b [ZMOD n]
sub_left
(c :
ℤ: Type
ℤ
) (
h: a ≡ b [ZMOD n]
h
: a ≡ b [ZMOD n]) : c - a ≡ c - b [ZMOD n] :=
ModEq.rfl: ∀ {n a : ℤ}, a ≡ a [ZMOD n]
ModEq.rfl
.
sub: ∀ {n a b c d : ℤ}, a ≡ b [ZMOD n] → c ≡ d [ZMOD n] → a - c ≡ b - d [ZMOD n]
sub
h: a ≡ b [ZMOD n]
h
#align int.modeq.sub_left
Int.ModEq.sub_left: ∀ {n a b : ℤ} (c : ℤ), a ≡ b [ZMOD n] → c - a ≡ c - b [ZMOD n]
Int.ModEq.sub_left
protected theorem
sub_right: ∀ {n a b : ℤ} (c : ℤ), a ≡ b [ZMOD n] → a - c ≡ b - c [ZMOD n]
sub_right
(c :
ℤ: Type
ℤ
) (
h: a ≡ b [ZMOD n]
h
: a ≡ b [ZMOD n]) : a - c ≡ b - c [ZMOD n] :=
h: a ≡ b [ZMOD n]
h
.
sub: ∀ {n a b c d : ℤ}, a ≡ b [ZMOD n] → c ≡ d [ZMOD n] → a - c ≡ b - d [ZMOD n]
sub
ModEq.rfl: ∀ {n a : ℤ}, a ≡ a [ZMOD n]
ModEq.rfl
#align int.modeq.sub_right
Int.ModEq.sub_right: ∀ {n a b : ℤ} (c : ℤ), a ≡ b [ZMOD n] → a - c ≡ b - c [ZMOD n]
Int.ModEq.sub_right
protected theorem
mul_left: ∀ {n a b : ℤ} (c : ℤ), a ≡ b [ZMOD n] → c * a ≡ c * b [ZMOD n]
mul_left
(c :
ℤ: Type
ℤ
) (
h: a ≡ b [ZMOD n]
h
: a ≡ b [ZMOD n]) : c * a ≡ c * b [ZMOD n] :=
h: a ≡ b [ZMOD n]
h
.
mul_left': ∀ {n a b c : ℤ}, a ≡ b [ZMOD n] → c * a ≡ c * b [ZMOD c * n]
mul_left'
.
of_dvd: ∀ {m n a b : ℤ}, m ∣ n → a ≡ b [ZMOD n] → a ≡ b [ZMOD m]
of_dvd
<|
dvd_mul_left: ∀ {α : Type ?u.18736} [inst : CommSemigroup α] (a b : α), a ∣ b * a
dvd_mul_left
_: ?m.18737
_
_: ?m.18737
_
#align int.modeq.mul_left
Int.ModEq.mul_left: ∀ {n a b : ℤ} (c : ℤ), a ≡ b [ZMOD n] → c * a ≡ c * b [ZMOD n]
Int.ModEq.mul_left
protected theorem
mul_right: ∀ (c : ℤ), a ≡ b [ZMOD n] → a * c ≡ b * c [ZMOD n]
mul_right
(c :
ℤ: Type
ℤ
) (
h: a ≡ b [ZMOD n]
h
: a ≡ b [ZMOD n]) : a * c ≡ b * c [ZMOD n] :=
h: a ≡ b [ZMOD n]
h
.
mul_right': ∀ {n a b c : ℤ}, a ≡ b [ZMOD n] → a * c ≡ b * c [ZMOD n * c]
mul_right'
.
of_dvd: ∀ {m n a b : ℤ}, m ∣ n → a ≡ b [ZMOD n] → a ≡ b [ZMOD m]
of_dvd
<|
dvd_mul_right: ∀ {α : Type ?u.18906} [inst : Semigroup α] (a b : α), a ∣ a * b
dvd_mul_right
_: ?m.18907
_
_: ?m.18907
_
#align int.modeq.mul_right
Int.ModEq.mul_right: ∀ {n a b : ℤ} (c : ℤ), a ≡ b [ZMOD n] → a * c ≡ b * c [ZMOD n]
Int.ModEq.mul_right
protected theorem
mul: a ≡ b [ZMOD n] → c ≡ d [ZMOD n] → a * c ≡ b * d [ZMOD n]
mul
(
h₁: a ≡ b [ZMOD n]
h₁
: a ≡ b [ZMOD n]) (
h₂: c ≡ d [ZMOD n]
h₂
: c ≡ d [ZMOD n]) : a * c ≡ b * d [ZMOD n] := (
h₂: c ≡ d [ZMOD n]
h₂
.
mul_left: ∀ {n a b : ℤ} (c : ℤ), a ≡ b [ZMOD n] → c * a ≡ c * b [ZMOD n]
mul_left
_).
trans: ∀ {n a b c : ℤ}, a ≡ b [ZMOD n] → b ≡ c [ZMOD n] → a ≡ c [ZMOD n]
trans
(
h₁: a ≡ b [ZMOD n]
h₁
.
mul_right: ∀ {n a b : ℤ} (c : ℤ), a ≡ b [ZMOD n] → a * c ≡ b * c [ZMOD n]
mul_right
_) #align int.modeq.mul
Int.ModEq.mul: ∀ {n a b c d : ℤ}, a ≡ b [ZMOD n] → c ≡ d [ZMOD n] → a * c ≡ b * d [ZMOD n]
Int.ModEq.mul
protected theorem
pow: ∀ {n a b : ℤ} (m : ℕ), a ≡ b [ZMOD n] → a ^ m ≡ b ^ m [ZMOD n]
pow
(m :
ℕ: Type
ℕ
) (
h: a ≡ b [ZMOD n]
h
: a ≡ b [ZMOD n]) : a ^ m ≡ b ^ m [ZMOD n] :=

Goals accomplished! 🐙
m✝, n, a, b, c, d: ℤ

m: ℕ

h: a ≡ b [ZMOD n]


a ^ m ≡ b ^ m [ZMOD n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]


zero
m, n, a, b, c, d✝: ℤ

h: a ≡ b [ZMOD n]

d: ℕ

hd: a ^ d ≡ b ^ d [ZMOD n]


succ
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]


zero
m, n, a, b, c, d✝: ℤ

h: a ≡ b [ZMOD n]

d: ℕ

hd: a ^ d ≡ b ^ d [ZMOD n]


succ
m✝, n, a, b, c, d: ℤ

m: ℕ

h: a ≡ b [ZMOD n]


a ^ m ≡ b ^ m [ZMOD n]
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]


zero
m, n, a, b, c, d: ℤ

h: a ≡ b [ZMOD n]


zero
m, n, a, b, c, d✝: ℤ

h: a ≡ b [ZMOD n]

d: ℕ

hd: a ^ d ≡ b ^ d [ZMOD n]


succ

Goals accomplished! 🐙
m✝, n, a, b, c, d: ℤ

m: ℕ

h: a ≡ b [ZMOD n]


a ^ m ≡ b ^ m [ZMOD n]
m, n, a, b, c, d✝: ℤ

h: a ≡ b [ZMOD n]

d: ℕ

hd: a ^ d ≡ b ^ d [ZMOD n]


succ
m, n, a, b, c, d✝: ℤ

h: a ≡ b [ZMOD n]

d: ℕ

hd: a ^ d ≡ b ^ d [ZMOD n]


succ
a * a ^ d ≡ b ^ Nat.succ d [ZMOD n]
m, n, a, b, c, d✝: ℤ

h: a ≡ b [ZMOD n]

d: ℕ

hd: a ^ d ≡ b ^ d [ZMOD n]


succ
m, n, a, b, c, d✝: ℤ

h: a ≡ b [ZMOD n]

d: ℕ

hd: a ^ d ≡ b ^ d [ZMOD n]


succ
a * a ^ d ≡ b * b ^ d [ZMOD n]
m, n, a, b, c, d✝: ℤ

h: a ≡ b [ZMOD n]

d: ℕ

hd: a ^ d ≡ b ^ d [ZMOD n]


succ
a * a ^ d ≡ b * b ^ d [ZMOD n]
m✝, n, a, b, c, d: ℤ

m: ℕ

h: a ≡ b [ZMOD n]


a ^ m ≡ b ^ m [ZMOD n]

Goals accomplished! 🐙
#align int.modeq.pow
Int.ModEq.pow: ∀ {n a b : ℤ} (m : ℕ), a ≡ b [ZMOD n] → a ^ m ≡ b ^ m [ZMOD n]
Int.ModEq.pow
lemma
of_mul_left: ∀ (m : ℤ), a ≡ b [ZMOD m * n] → a ≡ b [ZMOD n]
of_mul_left
(m :
ℤ: Type
ℤ
) (
h: a ≡ b [ZMOD m * n]
h
: a ≡ b [ZMOD m * n]) : a ≡ b [ZMOD n] :=

Goals accomplished! 🐙
m✝, n, a, b, c, d, m: ℤ

h: a ≡ b [ZMOD m * n]


m✝, n, a, b, c, d, m: ℤ

h: a ≡ b [ZMOD m * n]


m✝, n, a, b, c, d: ℤ

of_mul_left: ∀ (m : ℤ), a ≡ b [ZMOD m * n] → n ∣ b - a

m: ℤ

h: m * n ∣ b - a


n ∣ b - a
m✝, n, a, b, c, d: ℤ

of_mul_left: ∀ (m : ℤ), a ≡ b [ZMOD m * n] → n ∣ b - a

m: ℤ

h: m * n ∣ b - a


n ∣ b - a
m✝, n, a, b, c, d: ℤ

of_mul_left: ∀ (m : ℤ), a ≡ b [ZMOD m * n] → n ∣ b - a

m: ℤ

h: m * n ∣ b - a


n ∣ b - a
m✝, n, a, b, c, d: ℤ

of_mul_left: ∀ (m : ℤ), a ≡ b [ZMOD m * n] → n ∣ b - a

m: ℤ

h: m * n ∣ b - a


n ∣ b - a
m✝, n, a, b, c, d, m: ℤ

h: a ≡ b [ZMOD m * n]



Goals accomplished! 🐙
#align int.modeq.of_mul_left
Int.ModEq.of_mul_left: ∀ {n a b : ℤ} (m : ℤ), a ≡ b [ZMOD m * n] → a ≡ b [ZMOD n]
Int.ModEq.of_mul_left
lemma
of_mul_right: ∀ (m : ℤ), a ≡ b [ZMOD n * m] → a ≡ b [ZMOD n]
of_mul_right
(m :
ℤ: Type
ℤ
) : a ≡ b [ZMOD n * m] → a ≡ b [ZMOD n] :=
mul_comm: ∀ {G : Type ?u.19921} [inst : CommSemigroup G] (a b : G), a * b = b * a
mul_comm
m n ▸
of_mul_left: ∀ {n a b : ℤ} (m : ℤ), a ≡ b [ZMOD m * n] → a ≡ b [ZMOD n]
of_mul_left
_ #align int.modeq.of_mul_right
Int.ModEq.of_mul_right: ∀ {n a b : ℤ} (m : ℤ), a ≡ b [ZMOD n * m] → a ≡ b [ZMOD n]
Int.ModEq.of_mul_right
/-- To cancel a common factor `c` from a `ModEq` we must divide the modulus `m` by `gcd m c`. -/ theorem
cancel_right_div_gcd: ∀ {m a b c : ℤ}, 0 < m → a * c ≡ b * c [ZMOD m] → a ≡ b [ZMOD m / ↑(gcd m c)]
cancel_right_div_gcd
(
hm: 0 < m
hm
:
0: ?m.19978
0
< m) (
h: a * c ≡ b * c [ZMOD m]
h
: a * c ≡ b * c [ZMOD m]) : a ≡ b [ZMOD m /
gcd: ℤ → ℤ → ℕ
gcd
m c] :=

Goals accomplished! 🐙
m, n, a, b, c, d: ℤ

hm: 0 < m

h: a * c ≡ b * c [ZMOD m]


a ≡ b [ZMOD m / ↑(gcd m c)]
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)]
m, n, a, b, c, d: ℤ

hm: 0 < m

h: a * c ≡ b * c [ZMOD m]


a ≡ b [ZMOD m / ↑(gcd m c)]
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)]
m, n, a, b, c, d: ℤ

hm: 0 < m

h: a * c ≡ b * c [ZMOD m]


a ≡ b [ZMOD m / ↑(gcd m c)]
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)]
m, n, a, b, c, d: ℤ

hm: 0 < m

h: a * c ≡ b * c [ZMOD m]


a ≡ b [ZMOD m / ↑(gcd m c)]
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)]
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
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
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
m, n, a, b, c, d: ℤ

hm: 0 < m

h: a * c ≡ b * c [ZMOD m]


a ≡ b [ZMOD m / ↑(gcd m c)]
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


refine_1
m / ↑d ∣ c / ↑d * (b - a)
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


refine_2
gcd (m / ↑(gcd m c)) (c / ↑d) = 1
m, n, a, b, c, d: ℤ

hm: 0 < m

h: a * c ≡ b * c [ZMOD m]


a ≡ b [ZMOD m / ↑(gcd m c)]
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


refine_1
m / ↑d ∣ c / ↑d * (b - a)
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


refine_1
m / ↑d ∣ c / ↑d * (b - a)
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


refine_2
gcd (m / ↑(gcd m c)) (c / ↑d) = 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


refine_1
m / ↑d ∣ c / ↑d * (b - a)
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


refine_1
m / ↑d ∣ (b - a) * (c / ↑d)
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


refine_1
m / ↑d ∣ c / ↑d * (b - a)
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


refine_1
m / ↑d ∣ (b - a) * c / ↑(gcd m c)
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


refine_1
m / ↑d ∣ c / ↑d * (b - a)
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


refine_1
m / ↑d ∣ (b * c - a * c) / ↑(gcd m c)
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


refine_1
m / ↑d ∣ (b * c - a * c) / ↑(gcd m c)
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


refine_1
m / ↑d ∣ c / ↑d * (b - a)

Goals accomplished! 🐙
m, n, a, b, c, d: ℤ

hm: 0 < m

h: a * c ≡ b * c [ZMOD m]


a ≡ b [ZMOD m / ↑(gcd m c)]
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


refine_2
gcd (m / ↑(gcd m c)) (c / ↑d) = 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


refine_2
gcd (m / ↑(gcd m c)) (c / ↑d) = 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


refine_2
gcd (m / ↑(gcd m c)) (c / ↑d) = 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


refine_2
gcd m c / natAbs ↑(gcd m c) = 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


refine_2
gcd (m / ↑(gcd m c)) (c / ↑d) = 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


refine_2
gcd m c / gcd m c = 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


refine_2
gcd (m / ↑(gcd m c)) (c / ↑d) = 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


refine_2
1 = 1

Goals accomplished! 🐙
#align int.modeq.cancel_right_div_gcd
Int.ModEq.cancel_right_div_gcd: ∀ {m a b c : ℤ}, 0 < m → a * c ≡ b * c [ZMOD m] → a ≡ b [ZMOD m / ↑(gcd m c)]
Int.ModEq.cancel_right_div_gcd
/-- To cancel a common factor `c` from a `ModEq` we must divide the modulus `m` by `gcd m c`. -/ theorem
cancel_left_div_gcd: ∀ {m a b c : ℤ}, 0 < m → c * a ≡ c * b [ZMOD m] → a ≡ b [ZMOD m / ↑(gcd m c)]
cancel_left_div_gcd
(
hm: 0 < m
hm
:
0: ?m.20860
0
< m) (
h: c * a ≡ c * b [ZMOD m]
h
: c * a ≡ c * b [ZMOD m]) : a ≡ b [ZMOD m /
gcd: ℤ → ℤ → ℕ
gcd
m c] :=
cancel_right_div_gcd: ∀ {m a b c : ℤ}, 0 < m → a * c ≡ b * c [ZMOD m] → a ≡ b [ZMOD m / ↑(gcd m c)]
cancel_right_div_gcd
hm: 0 < m
hm
<|

Goals accomplished! 🐙
m, n, a, b, c, d: ℤ

hm: 0 < m

h: c * a ≡ c * b [ZMOD m]


a * c ≡ b * c [ZMOD m]

Goals accomplished! 🐙
#align int.modeq.cancel_left_div_gcd
Int.ModEq.cancel_left_div_gcd: ∀ {m a b c : ℤ}, 0 < m → c * a ≡ c * b [ZMOD m] → a ≡ b [ZMOD m / ↑(gcd m c)]
Int.ModEq.cancel_left_div_gcd
theorem
of_div: ∀ {m a b c : ℤ}, a / c ≡ b / c [ZMOD m / c] → c ∣ a → c ∣ b → c ∣ m → a ≡ b [ZMOD m]
of_div
(
h: a / c ≡ b / c [ZMOD m / c]
h
: a / c ≡ b / c [ZMOD m / c]) (
ha: c ∣ a
ha
: c ∣ a) (
ha: c ∣ b
ha
: c ∣ b) (
ha: c ∣ m
ha
: c ∣ m) : a ≡ b [ZMOD m] :=

Goals accomplished! 🐙
m, n, a, b, c, d: ℤ

h: a / c ≡ b / c [ZMOD m / c]

ha✝¹: c ∣ a

ha✝: c ∣ b

ha: c ∣ m


m, n, a, b, c, d: ℤ

h: a / c ≡ b / c [ZMOD m / c]

ha✝¹: c ∣ a

ha✝: c ∣ b

ha: c ∣ m


h.e'_1
m = ?m.21477 * (m / c)
m, n, a, b, c, d: ℤ

h: a / c ≡ b / c [ZMOD m / c]

ha✝¹: c ∣ a

ha✝: c ∣ b

ha: c ∣ m


h.e'_2
a = ?m.21477 * (a / c)
m, n, a, b, c, d: ℤ

h: a / c ≡ b / c [ZMOD m / c]

ha✝¹: c ∣ a

ha✝: c ∣ b

ha: c ∣ m


h.e'_3
b = ?m.21477 * (b / c)
m, n, a, b, c, d: ℤ

h: a / c ≡ b / c [ZMOD m / c]

ha✝¹: c ∣ a

ha✝: c ∣ b

ha: c ∣ m


m, n, a, b, c, d: ℤ

h: a / c ≡ b / c [ZMOD m / c]

ha✝¹: c ∣ a

ha✝: c ∣ b

ha: c ∣ m


m, n, a, b, c, d: ℤ

h: a / c ≡ b / c [ZMOD m / c]

ha✝¹: c ∣ a

ha✝: c ∣ b

ha: c ∣ m


h.e'_1
m = ?m.21477 * (m / c)
m, n, a, b, c, d: ℤ

h: a / c ≡ b / c [ZMOD m / c]

ha✝¹: c ∣ a

ha✝: c ∣ b

ha: c ∣ m


h.e'_2
a = ?m.21477 * (a / c)
m, n, a, b, c, d: ℤ

h: a / c ≡ b / c [ZMOD m / c]

ha✝¹: c ∣ a

ha✝: c ∣ b

ha: c ∣ m


h.e'_3
b = ?m.21477 * (b / c)
m, n, a, b, c, d: ℤ

h: a / c ≡ b / c [ZMOD m / c]

ha✝¹: c ∣ a

ha✝: c ∣ b

ha: c ∣ m


m, n, a, b, c, d: ℤ

h: a / c ≡ b / c [ZMOD m / c]

ha✝¹: c ∣ a

ha✝: c ∣ b

ha: c ∣ m


m, n, a, b, c, d: ℤ

h: a / c ≡ b / c [ZMOD m / c]

ha✝¹: c ∣ a

ha✝: c ∣ b

ha: c ∣ m


h.e'_2
a = c * (a / c)
m, n, a, b, c, d: ℤ

h: a / c ≡ b / c [ZMOD m / c]

ha✝¹: c ∣ a

ha✝: c ∣ b

ha: c ∣ m


h.e'_3
b = b
m, n, a, b, c, d: ℤ

h: a / c ≡ b / c [ZMOD m / c]

ha✝¹: c ∣ a

ha✝: c ∣ b

ha: c ∣ m


h.e'_3
c ∣ b
m, n, a, b, c, d: ℤ

h: a / c ≡ b / c [ZMOD m / c]

ha✝¹: c ∣ a

ha✝: c ∣ b

ha: c ∣ m


h.e'_1
c ∣ m
#align int.modeq.of_div
Int.ModEq.of_div: ∀ {m a b c : ℤ}, a / c ≡ b / c [ZMOD m / c] → c ∣ a → c ∣ b → c ∣ m → a ≡ b [ZMOD m]
Int.ModEq.of_div
end ModEq theorem
modEq_one: ∀ {a b : ℤ}, a ≡ b [ZMOD 1]
modEq_one
: a ≡ b [ZMOD
1: ?m.23651
1
] :=
modEq_of_dvd: ∀ {n a b : ℤ}, n ∣ b - a → a ≡ b [ZMOD n]
modEq_of_dvd
(
one_dvd: ∀ {α : Type ?u.23668} [inst : Monoid α] (a : α), 1 ∣ a
one_dvd
_: ?m.23669
_
) #align int.modeq_one
Int.modEq_one: ∀ {a b : ℤ}, a ≡ b [ZMOD 1]
Int.modEq_one
theorem
modEq_sub: ∀ (a b : ℤ), a ≡ b [ZMOD a - b]
modEq_sub
(a b :
ℤ: Type
ℤ
) : a ≡ b [ZMOD a - b] := (
modEq_of_dvd: ∀ {n a b : ℤ}, n ∣ b - a → a ≡ b [ZMOD n]
modEq_of_dvd
dvd_rfl: ∀ {α : Type ?u.23792} [inst : Monoid α] {a : α}, a ∣ a
dvd_rfl
).
symm: ∀ {n a b : ℤ}, a ≡ b [ZMOD n] → b ≡ a [ZMOD n]
symm
#align int.modeq_sub
Int.modEq_sub: ∀ (a b : ℤ), a ≡ b [ZMOD a - b]
Int.modEq_sub
@[simp] theorem
modEq_zero_iff: ∀ {a b : ℤ}, a ≡ b [ZMOD 0] ↔ a = b
modEq_zero_iff
: a ≡ b [ZMOD
0: ?m.23881
0
] ↔ a = b :=

Goals accomplished! 🐙
m, n, a, b, c, d: ℤ


a ≡ b [ZMOD 0] ↔ a = b
m, n, a, b, c, d: ℤ


a ≡ b [ZMOD 0] ↔ a = b
m, n, a, b, c, d: ℤ


a % 0 = b % 0 ↔ a = b
m, n, a, b, c, d: ℤ


a ≡ b [ZMOD 0] ↔ a = b
m, n, a, b, c, d: ℤ


a = b % 0 ↔ a = b
m, n, a, b, c, d: ℤ


a ≡ b [ZMOD 0] ↔ a = b
m, n, a, b, c, d: ℤ


a = b ↔ a = b

Goals accomplished! 🐙
#align int.modeq_zero_iff
Int.modEq_zero_iff: ∀ {a b : ℤ}, a ≡ b [ZMOD 0] ↔ a = b
Int.modEq_zero_iff
@[simp] theorem
add_modEq_left: ∀ {n a : ℤ}, n + a ≡ a [ZMOD n]
add_modEq_left
: n + a ≡ a [ZMOD n] :=
ModEq.symm: ∀ {n a b : ℤ}, a ≡ b [ZMOD n] → b ≡ a [ZMOD n]
ModEq.symm
<|
modEq_iff_dvd: ∀ {n a b : ℤ}, a ≡ b [ZMOD n] ↔ n ∣ b - a
modEq_iff_dvd
.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
<|

Goals accomplished! 🐙
m, n, a, b, c, d: ℤ


n ∣ n + a - a

Goals accomplished! 🐙
#align int.add_modeq_left
Int.add_modEq_left: ∀ {n a : ℤ}, n + a ≡ a [ZMOD n]
Int.add_modEq_left
@[simp] theorem
add_modEq_right: a + n ≡ a [ZMOD n]
add_modEq_right
: a + n ≡ a [ZMOD n] :=
ModEq.symm: ∀ {n a b : ℤ}, a ≡ b [ZMOD n] → b ≡ a [ZMOD n]
ModEq.symm
<|
modEq_iff_dvd: ∀ {n a b : ℤ}, a ≡ b [ZMOD n] ↔ n ∣ b - a
modEq_iff_dvd
.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
<|

Goals accomplished! 🐙
m, n, a, b, c, d: ℤ


n ∣ a + n - a

Goals accomplished! 🐙
#align int.add_modeq_right
Int.add_modEq_right: ∀ {n a : ℤ}, a + n ≡ a [ZMOD n]
Int.add_modEq_right
theorem
modEq_and_modEq_iff_modEq_mul: ∀ {a b m n : ℤ}, Nat.coprime (natAbs m) (natAbs n) → (a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD m * n])
modEq_and_modEq_iff_modEq_mul
{a b m n :
ℤ: Type
ℤ
} (hmn : m.
natAbs: ℤ → ℕ
natAbs
.
coprime: ℕ → ℕ → Prop
coprime
n.
natAbs: ℤ → ℕ
natAbs
) : a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD m * n] := ⟨fun
h: ?m.24657
h
=>

Goals accomplished! 🐙
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]
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]
m✝, n✝, a✝, b✝, c, d, a, b, m, n: ℤ

hmn: Nat.coprime (natAbs m) (natAbs n)

h: m ∣ b - a ∧ a ≡ b [ZMOD n]


a ≡ b [ZMOD m * n]
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]
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]
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]
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]
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]
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]
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 * n ∣ b - a
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]
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 * n)) ∣ b - a
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]
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 * n)) ∣ ↑(natAbs (b - a))
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]
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 * n) ∣ natAbs (b - a)
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]
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✝, n✝, a✝, b✝, c, d, a, b, m, n: ℤ

hmn: Nat.coprime (natAbs m) (natAbs n)

h: m ∣ b - a ∧ n ∣ b - a


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]
m✝, n✝, a✝, b✝, c, d, a, b, m, n: ℤ

hmn: Nat.coprime (natAbs m) (natAbs n)

h: m ∣ b - a ∧ n ∣ b - a


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


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


m✝, n✝, a✝, b✝, c, d, a, b, m, n: ℤ

hmn: Nat.coprime (natAbs m) (natAbs n)

h: m ∣ b - a ∧ n ∣ b - a


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


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


m✝, n✝, a✝, b✝, c, d, a, b, m, n: ℤ

hmn: Nat.coprime (natAbs m) (natAbs n)

h: m ∣ b - a ∧ n ∣ b - a


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


refine'_2
↑(natAbs n) ∣ ↑(natAbs (b - a))
m✝, n✝, a✝, b✝, c, d, a, b, m, n: ℤ

hmn: Nat.coprime (natAbs m) (natAbs n)

h: m ∣ b - a ∧ n ∣ b - a


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


refine'_1
m ∣ ↑(natAbs (b - a))
m✝, n✝, a✝, b✝, c, d, a, b, m, n: ℤ

hmn: Nat.coprime (natAbs m) (natAbs n)

h: m ∣ b - a ∧ n ∣ b - a


refine'_1
m✝, n✝, a✝, b✝, c, d, a, b, m, n: ℤ

hmn: Nat.coprime (natAbs