---

Step * of Lemma product-eq-0-mod-prime

∀p,a,b:ℤ.  (prime(p) ⇒ ((a * b) ≡ 0 mod p) ⇒ ((a ≡ 0 mod p) ∨ (b ≡ 0 mod p)))
BY
{ xxx((Auto THEN D -1) THEN (Assert p | (a * b) BY (D 0 With ⌜c⌝  THEN Auto)))xxx }

1
1. p : ℤ
2. a : ℤ
3. b : ℤ
4. prime(p)
5. c : ℤ
6. ((a * b) - 0) = (p * c) ∈ ℤ
7. p | (a * b)
⊢ (a ≡ 0 mod p) ∨ (b ≡ 0 mod p)

---

Latex:

---

Latex:
\mforall{}p,a,b:\mBbbZ{}.    (prime(p)  {}\mRightarrow{}  ((a  *  b)  \mequiv{}  0  mod  p)  {}\mRightarrow{}  ((a  \mequiv{}  0  mod  p)  \mvee{}  (b  \mequiv{}  0  mod  p)))


By

---

Latex:
xxx((Auto  THEN  D  -1)  THEN  (Assert  p  |  (a  *  b)  BY  (D  0  With  \mkleeneopen{}c\mkleeneclose{}    THEN  Auto)))xxx

---

Home Index