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

(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 1 1 1 1 2 1 1 1

1. x :

2.

x1:

. x1<x

2

x1

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

j
8.

prime(i)
9. n : {2..i

}
10. m : {2..i

}
11. i = n

m
12. prime(n)
13. x = n

m

j

j:{2..x

}. x = n

j & prime(n)

By:	Witness: mj ...

Generated subgoal:

1 mj {2..x}
4 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