Step |
Hyp |
Ref |
Expression |
1 |
|
eldmgm |
|- ( A e. ( CC \ ( ZZ \ NN ) ) <-> ( A e. CC /\ -. -u A e. NN0 ) ) |
2 |
1
|
simprbi |
|- ( A e. ( CC \ ( ZZ \ NN ) ) -> -. -u A e. NN0 ) |
3 |
2
|
adantr |
|- ( ( A e. ( CC \ ( ZZ \ NN ) ) /\ N e. NN0 ) -> -. -u A e. NN0 ) |
4 |
|
df-neg |
|- -u A = ( 0 - A ) |
5 |
4
|
eqeq1i |
|- ( -u A = N <-> ( 0 - A ) = N ) |
6 |
|
0cnd |
|- ( ( A e. ( CC \ ( ZZ \ NN ) ) /\ N e. NN0 ) -> 0 e. CC ) |
7 |
|
eldifi |
|- ( A e. ( CC \ ( ZZ \ NN ) ) -> A e. CC ) |
8 |
7
|
adantr |
|- ( ( A e. ( CC \ ( ZZ \ NN ) ) /\ N e. NN0 ) -> A e. CC ) |
9 |
|
nn0cn |
|- ( N e. NN0 -> N e. CC ) |
10 |
9
|
adantl |
|- ( ( A e. ( CC \ ( ZZ \ NN ) ) /\ N e. NN0 ) -> N e. CC ) |
11 |
6 8 10
|
subaddd |
|- ( ( A e. ( CC \ ( ZZ \ NN ) ) /\ N e. NN0 ) -> ( ( 0 - A ) = N <-> ( A + N ) = 0 ) ) |
12 |
5 11
|
syl5bb |
|- ( ( A e. ( CC \ ( ZZ \ NN ) ) /\ N e. NN0 ) -> ( -u A = N <-> ( A + N ) = 0 ) ) |
13 |
|
simpr |
|- ( ( A e. ( CC \ ( ZZ \ NN ) ) /\ N e. NN0 ) -> N e. NN0 ) |
14 |
|
eleq1 |
|- ( -u A = N -> ( -u A e. NN0 <-> N e. NN0 ) ) |
15 |
13 14
|
syl5ibrcom |
|- ( ( A e. ( CC \ ( ZZ \ NN ) ) /\ N e. NN0 ) -> ( -u A = N -> -u A e. NN0 ) ) |
16 |
12 15
|
sylbird |
|- ( ( A e. ( CC \ ( ZZ \ NN ) ) /\ N e. NN0 ) -> ( ( A + N ) = 0 -> -u A e. NN0 ) ) |
17 |
16
|
necon3bd |
|- ( ( A e. ( CC \ ( ZZ \ NN ) ) /\ N e. NN0 ) -> ( -. -u A e. NN0 -> ( A + N ) =/= 0 ) ) |
18 |
3 17
|
mpd |
|- ( ( A e. ( CC \ ( ZZ \ NN ) ) /\ N e. NN0 ) -> ( A + N ) =/= 0 ) |