Nuprl - Proof: chrem exists a 1 1

(11steps total) PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc

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

1. r :

2. s :

3. CoPrime(r,s)
4. a :

5. b :

. ((x = a mod r) & (x = b mod s))

By:	(Inst (Thm* r:, s:{s':\| CoPrime(r,s') }. x:. ((x = 1 mod r) & (x = 0 mod s)) ([r;s]) THEN (Inst (Thm* r:, s:{s':\| CoPrime(r,s') }. x:. ((x = 1 mod r) & (x = 0 mod s)) ([s;r])

Generated subgoals:

1 6. x:. ((x = 1 mod r) & (x = 0 mod s))
CoPrime(s,r)
2 steps

2 6. x:. ((x = 1 mod r) & (x = 0 mod s))
7. x:. ((x = 1 mod s) & (x = 0 mod r))
x:. ((x = a mod r) & (x = b mod s))
6 steps

About:

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

(11steps total) PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc

1	6. x:. ((x = 1 mod r) & (x = 0 mod s)) CoPrime(s,r)	2 steps
2	6. x:. ((x = 1 mod r) & (x = 0 mod s)) 7. x:. ((x = 1 mod s) & (x = 0 mod r)) x:. ((x = a mod r) & (x = b mod s))	6 steps