Step |
Hyp |
Ref |
Expression |
1 |
|
neg1cn |
|- -u 1 e. CC |
2 |
|
neg1ne0 |
|- -u 1 =/= 0 |
3 |
|
prmdvdsfi |
|- ( A e. NN -> { p e. Prime | p || A } e. Fin ) |
4 |
|
hashcl |
|- ( { p e. Prime | p || A } e. Fin -> ( # ` { p e. Prime | p || A } ) e. NN0 ) |
5 |
3 4
|
syl |
|- ( A e. NN -> ( # ` { p e. Prime | p || A } ) e. NN0 ) |
6 |
5
|
nn0zd |
|- ( A e. NN -> ( # ` { p e. Prime | p || A } ) e. ZZ ) |
7 |
|
expne0i |
|- ( ( -u 1 e. CC /\ -u 1 =/= 0 /\ ( # ` { p e. Prime | p || A } ) e. ZZ ) -> ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) =/= 0 ) |
8 |
1 2 6 7
|
mp3an12i |
|- ( A e. NN -> ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) =/= 0 ) |
9 |
|
iffalse |
|- ( -. E. p e. Prime ( p ^ 2 ) || A -> if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) = ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) |
10 |
9
|
neeq1d |
|- ( -. E. p e. Prime ( p ^ 2 ) || A -> ( if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) =/= 0 <-> ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) =/= 0 ) ) |
11 |
8 10
|
syl5ibrcom |
|- ( A e. NN -> ( -. E. p e. Prime ( p ^ 2 ) || A -> if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) =/= 0 ) ) |
12 |
|
muval |
|- ( A e. NN -> ( mmu ` A ) = if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) ) |
13 |
12
|
neeq1d |
|- ( A e. NN -> ( ( mmu ` A ) =/= 0 <-> if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) =/= 0 ) ) |
14 |
11 13
|
sylibrd |
|- ( A e. NN -> ( -. E. p e. Prime ( p ^ 2 ) || A -> ( mmu ` A ) =/= 0 ) ) |
15 |
14
|
necon4bd |
|- ( A e. NN -> ( ( mmu ` A ) = 0 -> E. p e. Prime ( p ^ 2 ) || A ) ) |
16 |
|
iftrue |
|- ( E. p e. Prime ( p ^ 2 ) || A -> if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) = 0 ) |
17 |
12
|
eqeq1d |
|- ( A e. NN -> ( ( mmu ` A ) = 0 <-> if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) = 0 ) ) |
18 |
16 17
|
syl5ibr |
|- ( A e. NN -> ( E. p e. Prime ( p ^ 2 ) || A -> ( mmu ` A ) = 0 ) ) |
19 |
15 18
|
impbid |
|- ( A e. NN -> ( ( mmu ` A ) = 0 <-> E. p e. Prime ( p ^ 2 ) || A ) ) |