IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
prime factorization limit11 1. n : 2. f : Prime 3. g : Prime 4. f is a factorization of n 5. g is a factorization of n 6. x:{2..(n+1)}. prime_mset_complete(f)(x) = prime_mset_complete(g)(x)
7. x : 8. prime(x)
9. n<x f(x) = g(x)
By:
FwdThru: Hyp:4 on [ n<x ] THEN FwdThru: Hyp:5 on [ n<x ]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html