Nuprl - Proof: composite with prime factor 1 1 1 1

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

1. x :

x1:

. x1<x

prime(x1)

(

i,j:{2..x1

}. x1 = i

j & prime(i))
3. 2

x
4.

prime(x)
5. i : {2..x

}
6. j : {2..x

}
7. x = i

i,j:{2..x

}. x = i

j & prime(i)

By:	Decide: prime(i) ...

Generated subgoals:

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

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

About:

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

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