---

Step * of Lemma divisor_of_sum

∀a,b1,b2:ℤ.  ((a | b1) ⇒ (a | b2) ⇒ (a | (b1 + b2)))
BY
{ (UnivCD THENA Auto) }

1
1. a : ℤ@i
2. b1 : ℤ@i
3. b2 : ℤ@i
4. a | b1@i
5. a | b2@i
⊢ a | (b1 + b2)

---

Latex:

---

Latex:
\mforall{}a,b1,b2:\mBbbZ{}.    ((a  |  b1)  {}\mRightarrow{}  (a  |  b2)  {}\mRightarrow{}  (a  |  (b1  +  b2)))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index