---

Step * 1 of Lemma rat2real-qadd


1. a : ℚ
2. b : ℚ
3. p : ℤ
4. q : ℤ
5. 0 < q
6. ¬(q = 0 ∈ ℚ)
7. b = (p/q) ∈ ℚ
8. ¬↑qeq(q;0)
9. p1 : ℤ
10. q1 : ℤ
11. 0 < q1
12. ¬(q1 = 0 ∈ ℚ)
13. a = (p1/q1) ∈ ℚ
14. ¬↑qeq(q1;0)
⊢ (r((p1 * q) + (p * q1)))/q1 * q = ((r(p1))/q1 + (r(p))/q)
BY
{ (RWO "int-rdiv-req" 0 THEN Auto THEN RWO "radd-int-fractions" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbQ{}
2.  b  :  \mBbbQ{}
3.  p  :  \mBbbZ{}
4.  q  :  \mBbbZ{}
5.  0  <  q
6.  \mneg{}(q  =  0)
7.  b  =  (p/q)
8.  \mneg{}\muparrow{}qeq(q;0)
9.  p1  :  \mBbbZ{}
10.  q1  :  \mBbbZ{}
11.  0  <  q1
12.  \mneg{}(q1  =  0)
13.  a  =  (p1/q1)
14.  \mneg{}\muparrow{}qeq(q1;0)
\mvdash{}  (r((p1  *  q)  +  (p  *  q1)))/q1  *  q  =  ((r(p1))/q1  +  (r(p))/q)


By

---

Latex:
(RWO  "int-rdiv-req"  0  THEN  Auto  THEN  RWO  "radd-int-fractions"  0  THEN  Auto)

---

Home Index