Nuprl - Proof: prime factorization includes prime divisors 1 2 1 1 1

(12steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: prime factorization includes prime divisors 1 2 1 1 1

1. a :

2. b :

3. f : {a..b

}

4. p :

5. is_prime_factorization(a; b; f)
6. prime(p)
7. p | (

i:{a..b

}. i

f(i))
8. i : {a..b

}
9. p | i

f(i)
10. f(i)

0
11. p | i
12. prime(i)

p

{a..b

} & 0<f(p)

By:	FwdThru: Thm* x:{2...}, y:. prime(y) x \| y x = y on [ p \| i ] ...

Generated subgoals:

1 p {2...}
1 step

2 13. p = i
p {a..b} & 0<f(p)
2 steps

About:

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

(12steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc