Nuprl - Proof: prime among factors 1 1

(9steps total) PrintForm Definitions Lemmas SimpleMulFacts Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: prime among factors 1 1

1. a :

2. b :

3. prime(a

b)
4. 2

a

b
5.

(

i:{2..(a

b)

}. i | a

b)

a

b = a

a

b = b

By:	Enough that (ab = a & ab = b ) (By (FwdThru: Thm* Dec(A) ((A & B) A B) on [ Hyp:-1 ] ...)

Generated subgoal:

1 (ab = a & ab = b)
6 steps

About:

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

(9steps total) PrintForm Definitions Lemmas SimpleMulFacts Sections DiscrMathExt Doc