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))
p 
{a..b} & 0<f(p)
}
i:{a..b}. if(i))
p {a..b} & 0<f(p)| By: |
Thm*  p:.
Thm* prime(p) Thm*  
Thm* ( a,b:, e:({a..b}).
Thm* (a<b p | ( i:{a..b}. e(i)) ( i:{a..b}. p | e(i)))
on [ Hyp:-1 ] |
| 1 |
a<b | 3 steps |
| 2 |
i:{a..b}. p | if(i)
p {a..b} & 0<f(p) | 7 steps |
About:
 |  |  |  |  |  |
 |  |  |  |
 |