Nuprl - Proof: qadd functionality 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: qadd functionality 1 1 1

1. p1 :

2. p2 :

3. q1 :

4. q2 :

5. r1 :

6. r2 :

7. s1 :

8. s2 :

q2 = q1

s2 = s1

p1/p2 +q r1/r2.num

q1/q2 +q s1/s2.den = q1/q2 +q s1/s2.num

p1/p2 +q r1/r2.den

By:

UnivCD

Generated subgoal:

1 9. p1q2 = q1p2
10. r1s2 = s1r2
p1/p2 +q r1/r2.numq1/q2 +q s1/s2.den = q1/q2 +q s1/s2.nump1/p2 +q r1/r2.den
3 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html