Nuprl - Proof: composite with prime factor a

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: composite with prime factor a

x:{2...}.

prime(x)

(

i,j:{2..x

}. x = i

j & prime(i))

By:	x:. 2x prime(x) (i,j:{2..x}. x = ij & prime(i)) Asserted

Generated subgoals:

1   x:. 2x  prime(x)  (i,j:{2..x}. x = ij & prime(i))
PREMISE

2 1. x:. 2x  prime(x)  (i,j:{2..x}. x = ij & prime(i))
  x:{2...}. prime(x)  (i,j:{2..x}. x = ij & prime(i))
2 steps

About:

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

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

1	x:. 2x prime(x) (i,j:{2..x}. x = ij & prime(i))	PREMISE
2	1. x:. 2x prime(x) (i,j:{2..x}. x = ij & prime(i)) x:{2...}. prime(x) (i,j:{2..x}. x = ij & prime(i))	2 steps