| Step |
Hyp |
Ref |
Expression |
| 1 |
|
eqid |
|- ( 0 ..^ ( M x. N ) ) = ( 0 ..^ ( M x. N ) ) |
| 2 |
|
eqid |
|- ( ( 0 ..^ M ) X. ( 0 ..^ N ) ) = ( ( 0 ..^ M ) X. ( 0 ..^ N ) ) |
| 3 |
|
eqid |
|- ( x e. ( 0 ..^ ( M x. N ) ) |-> <. ( x mod M ) , ( x mod N ) >. ) = ( x e. ( 0 ..^ ( M x. N ) ) |-> <. ( x mod M ) , ( x mod N ) >. ) |
| 4 |
|
id |
|- ( ( M e. NN /\ N e. NN /\ ( M gcd N ) = 1 ) -> ( M e. NN /\ N e. NN /\ ( M gcd N ) = 1 ) ) |
| 5 |
|
eqid |
|- { y e. ( 0 ..^ M ) | ( y gcd M ) = 1 } = { y e. ( 0 ..^ M ) | ( y gcd M ) = 1 } |
| 6 |
|
eqid |
|- { y e. ( 0 ..^ N ) | ( y gcd N ) = 1 } = { y e. ( 0 ..^ N ) | ( y gcd N ) = 1 } |
| 7 |
|
eqid |
|- { y e. ( 0 ..^ ( M x. N ) ) | ( y gcd ( M x. N ) ) = 1 } = { y e. ( 0 ..^ ( M x. N ) ) | ( y gcd ( M x. N ) ) = 1 } |
| 8 |
1 2 3 4 5 6 7
|
phimullem |
|- ( ( M e. NN /\ N e. NN /\ ( M gcd N ) = 1 ) -> ( phi ` ( M x. N ) ) = ( ( phi ` M ) x. ( phi ` N ) ) ) |