n:
, f,g:(Prime
).
f is a factorization of n 
g is a factorization of n f = gAt: prime factorization mset unique
n:, f,g:(Prime).
f is a factorization of n g is a factorization of n f = g| By: |
Thm* n:, f,g:(Prime).
Thm* f is a factorization of n Thm*
Thm* g is a factorization of n Thm*
Thm* ( x:{2..(n+1) }. prime_mset_complete(f)(x) = prime_mset_complete(g)(x))
Thm*
Thm* f = g THEN BackThru: Hyp:-1 |
| 1 |
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))
6.
6. f = g 7. x : {2..(n+1) }
prime_mset_complete(f)(x) = prime_mset_complete(g)(x) | 3 steps |
About:
 |  |  |  |  |  |  |  |