Nuprl - Proof: prime nat 3 1

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

1. x :

2. 2

x
3.

(

i:{2..x

}. i | x)

atomic(x)

By:	BackThru: Thm* a:. atomic(a) (a ~ 1) & (b:. b \| a (b ~ 1) (b ~ a))

Generated subgoals:

1 (x ~ 1)
1 step

2 4. b :
5. b | x
(b ~ 1) (b ~ x)
13 steps

About:

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