Nuprl - Proof: chrem exists aux a

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: chrem exists aux a

, s:{s':

| CoPrime(r,s') }.

. ((x = 1 mod r) & (x = 0 mod s))

By:

UnivCD

Generated subgoal:

1 1. r :
2. s : {s':| CoPrime(r,s') }
x:. ((x = 1 mod r) & (x = 0 mod s))
7 steps

About:

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