Nuprl - Proof: prime mset c is prime f 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: prime mset c is prime f 1

1. f : Prime

2. b :

is_prime_factorization(2; b; prime_mset_complete(f))

By:

Analyze

Generated subgoal:

1 3. i : {2..b}
4. 0<prime_mset_complete(f)(i)
prime(i)
2 steps

About:

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