[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a✝ a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
a : α
⊢ a - a = 0 • p
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
⊢ (∃ b_1, b - a = ↑(Equiv.neg ℤ).symm b_1 • p) ↔ b ≡ a [PMOD p]
[PROOFSTEP]
simp [ModEq, ← neg_eq_iff_eq_neg]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n✝ : ℕ
z : ℤ
x✝¹ : a ≡ b [PMOD p]
x✝ : b ≡ c [PMOD p]
m : ℤ
hm : b - a = m • p
n : ℤ
hn : c - b = n • p
⊢ c - a = (m + n) • p
[PROOFSTEP]
simp [add_smul, ← hm, ← hn]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
⊢ -b ≡ -a [PMOD p] ↔ a ≡ b [PMOD p]
[PROOFSTEP]
simp [ModEq, neg_add_eq_sub]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
⊢ b ≡ a [PMOD -p] ↔ a ≡ b [PMOD p]
[PROOFSTEP]
simp [ModEq, ← neg_eq_iff_eq_neg]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
⊢ a ≡ b [PMOD 0] ↔ a = b
[PROOFSTEP]
simp [ModEq, sub_eq_zero, eq_comm]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
⊢ 0 - p = -1 • p
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z✝ z : ℤ
⊢ 0 - z • p = -z • p
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z✝ z : ℤ
⊢ a - (a + z • p) = -z • p
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z✝ z : ℤ
⊢ a - (z • p + a) = -z • p
[PROOFSTEP]
simp [← sub_sub]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n✝ : ℕ
z : ℤ
n : ℕ
⊢ a - (a + n • p) = -↑n • p
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n✝ : ℕ
z : ℤ
n : ℕ
⊢ a - (n • p + a) = -↑n • p
[PROOFSTEP]
simp [← sub_sub]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
x✝ : a ≡ b [PMOD z • p]
m : ℤ
hm : b - a = m • z • p
⊢ b - a = (m * z) • p
[PROOFSTEP]
rwa [mul_smul]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
x✝ : a ≡ b [PMOD n • p]
m : ℤ
hm : b - a = m • n • p
⊢ b - a = (m * ↑n) • p
[PROOFSTEP]
rwa [mul_smul, coe_nat_zsmul]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z m : ℤ
hm : b - a = m • p
⊢ z • b - z • a = m • z • p
[PROOFSTEP]
rw [← smul_sub, hm, smul_comm]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z m : ℤ
hm : b - a = m • p
⊢ n • b - n • a = m • n • p
[PROOFSTEP]
rw [← smul_sub, hm, smul_comm]
[GOAL]
α : Type u_1
inst✝¹ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
inst✝ : NoZeroSMulDivisors ℤ α
hn : z ≠ 0
m : ℤ
⊢ z • b - z • a = m • z • p ↔ b - a = m • p
[PROOFSTEP]
rw [← smul_sub, smul_comm, smul_right_inj hn]
[GOAL]
α : Type u_1
inst✝¹ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
inst✝ : NoZeroSMulDivisors ℕ α
hn : n ≠ 0
m : ℤ
⊢ n • b - n • a = m • n • p ↔ b - a = m • p
[PROOFSTEP]
rw [← smul_sub, smul_comm, smul_right_inj hn]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
x✝ : a₁ ≡ b₁ [PMOD p]
m : ℤ
hm : b₁ - a₁ = m • p
⊢ (∃ b, b₁ + b₂ - (a₁ + a₂) = ↑(Equiv.addLeft m).symm.symm b • p) ↔ a₂ ≡ b₂ [PMOD p]
[PROOFSTEP]
simp [add_sub_add_comm, hm, add_smul, ModEq]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
x✝ : a₂ ≡ b₂ [PMOD p]
m : ℤ
hm : b₂ - a₂ = m • p
⊢ (∃ b, b₁ + b₂ - (a₁ + a₂) = ↑(Equiv.addRight m).symm.symm b • p) ↔ a₁ ≡ b₁ [PMOD p]
[PROOFSTEP]
simp [add_sub_add_comm, hm, add_smul, ModEq]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
x✝ : a₁ ≡ b₁ [PMOD p]
m : ℤ
hm : b₁ - a₁ = m • p
⊢ (∃ b, b₁ - b₂ - (a₁ - a₂) = ↑(Equiv.subLeft m).symm.symm b • p) ↔ a₂ ≡ b₂ [PMOD p]
[PROOFSTEP]
simp [sub_sub_sub_comm, hm, sub_smul, ModEq]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
x✝ : a₂ ≡ b₂ [PMOD p]
m : ℤ
hm : b₂ - a₂ = m • p
⊢ (∃ b, b₁ - b₂ - (a₁ - a₂) = ↑(Equiv.subRight m).symm.symm b • p) ↔ a₁ ≡ b₁ [PMOD p]
[PROOFSTEP]
simp [sub_sub_sub_comm, hm, sub_smul, ModEq]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
⊢ a ≡ b - c [PMOD p] ↔ c + a ≡ b [PMOD p]
[PROOFSTEP]
simp [ModEq, sub_sub]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
⊢ c + a ≡ b [PMOD p] ↔ a + c ≡ b [PMOD p]
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
⊢ a - b ≡ 0 [PMOD p] ↔ a ≡ b [PMOD p]
[PROOFSTEP]
simp [sub_modEq_iff_modEq_add]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
⊢ a + b ≡ a [PMOD p] ↔ b ≡ 0 [PMOD p]
[PROOFSTEP]
simp [← modEq_sub_iff_add_modEq']
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
⊢ a + b ≡ b [PMOD p] ↔ a ≡ 0 [PMOD p]
[PROOFSTEP]
simp [← modEq_sub_iff_add_modEq]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
⊢ a ≡ b [PMOD p] ↔ ∃ z, b = a + z • p
[PROOFSTEP]
simp_rw [ModEq, sub_eq_iff_eq_add']
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
⊢ ¬a ≡ b [PMOD p] ↔ ∀ (z : ℤ), b ≠ a + z • p
[PROOFSTEP]
rw [modEq_iff_eq_add_zsmul, not_exists]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
⊢ a ≡ b [PMOD p] ↔ ↑b = ↑a
[PROOFSTEP]
simp_rw [modEq_iff_eq_add_zsmul, QuotientAddGroup.eq_iff_sub_mem, AddSubgroup.mem_zmultiples_iff, eq_sub_iff_add_eq',
  eq_comm]
[GOAL]
α : Type u_1
a b z : ℤ
⊢ a ≡ b [PMOD z] ↔ a ≡ b [ZMOD z]
[PROOFSTEP]
simp [ModEq, dvd_iff_exists_eq_mul_left, Int.modEq_iff_dvd]
[GOAL]
α : Type u_1
inst✝¹ : AddCommGroupWithOne α
inst✝ : CharZero α
a b z : ℤ
⊢ ↑a ≡ ↑b [PMOD ↑z] ↔ a ≡ b [PMOD z]
[PROOFSTEP]
simp_rw [ModEq, ← Int.cast_mul_eq_zsmul_cast]
[GOAL]
α : Type u_1
inst✝¹ : AddCommGroupWithOne α
inst✝ : CharZero α
a b z : ℤ
⊢ (∃ z_1, ↑b - ↑a = ↑(z_1 * z)) ↔ ∃ z_1, b - a = z_1 • z
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
inst✝¹ : AddCommGroupWithOne α
inst✝ : CharZero α
a b n : ℕ
⊢ ↑a ≡ ↑b [PMOD ↑n] ↔ a ≡ b [MOD n]
[PROOFSTEP]
simp_rw [← Int.coe_nat_modEq_iff, ← modEq_iff_int_modEq, ← @int_cast_modEq_int_cast α, Int.cast_ofNat]
