Nuprl - Proof: chrem exists a 1 1 2 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 2 1

1. r :

2. s :

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

5. b :

6. p :

7. (p = 1 mod r) & (p = 0 mod s) [not for witness]
8. q :

9. (q = 1 mod s) & (q = 0 mod r) [not for witness]

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

By:	SeqOnM [Witness ap+bq;Analyze 9;Analyze 7;Analyze 0]

Generated subgoals:

1 7. p = 1 mod r
8. p = 0 mod s
9. q :
10. q = 1 mod s
11. q = 0 mod r
(ap+bq) = a mod r
2 steps

2 7. p = 1 mod r
8. p = 0 mod s
9. q :
10. q = 1 mod s
11. q = 0 mod r
(ap+bq) = b mod s
2 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	7. p = 1 mod r 8. p = 0 mod s 9. q : 10. q = 1 mod s 11. q = 0 mod r (ap+bq) = a mod r	2 steps
2	7. p = 1 mod r 8. p = 0 mod s 9. q : 10. q = 1 mod s 11. q = 0 mod r (ap+bq) = b mod s	2 steps