Nuprl - Proof: prime among factors

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Factoring a prime always includes the prime itself.

At: prime among factors

a,b:

. prime(a

b)

a

b = a

a

b = b

By:	Auto THEN (Rewrite'2 by Thm* x:. prime(x) 2x & (i:{2..x}. i \| x) ... ; Id)

Generated subgoal:

1 1. a :
2. b :
3. prime(ab)
ab = a ab = b
8 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