---

Step * 1 of Lemma divisor_of_sum


1. a : ℤ@i
2. b1 : ℤ@i
3. b2 : ℤ@i
4. a | b1@i
5. a | b2@i
⊢ a | (b1 + b2)
BY
{ (DVars [`d'] 5 THEN DVars [`c'] 4) }

1
1. a : ℤ@i
2. b1 : ℤ@i
3. b2 : ℤ@i
4. c : ℤ@i
5. b1 = (a * c) ∈ ℤ@i
6. d : ℤ@i
7. b2 = (a * d) ∈ ℤ@i
⊢ a | (b1 + b2)

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}@i
2.  b1  :  \mBbbZ{}@i
3.  b2  :  \mBbbZ{}@i
4.  a  |  b1@i
5.  a  |  b2@i
\mvdash{}  a  |  (b1  +  b2)


By

---

Latex:
(DVars  [`d']  5  THEN  DVars  [`c']  4)

---

Home Index