Nuprl - Proof: prime factorization includes prime divisors 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 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. b

a

False

By:	Rewrite7 by Thm* f:(AAA), u:A, a,b:, e:({a..b}A). Thm* ba (Iter(f;u) i:{a..b}. e(i)) = u

Generated subgoal:

1 9. p | 1
False
1 step

About:

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

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