| Step |
Hyp |
Ref |
Expression |
| 1 |
|
divalglem0.1 |
|- N e. ZZ |
| 2 |
|
divalglem0.2 |
|- D e. ZZ |
| 3 |
|
divalglem1.3 |
|- D =/= 0 |
| 4 |
1
|
zrei |
|- N e. RR |
| 5 |
|
0re |
|- 0 e. RR |
| 6 |
4 5
|
letrii |
|- ( N <_ 0 \/ 0 <_ N ) |
| 7 |
|
nnabscl |
|- ( ( D e. ZZ /\ D =/= 0 ) -> ( abs ` D ) e. NN ) |
| 8 |
2 3 7
|
mp2an |
|- ( abs ` D ) e. NN |
| 9 |
|
nnge1 |
|- ( ( abs ` D ) e. NN -> 1 <_ ( abs ` D ) ) |
| 10 |
8 9
|
ax-mp |
|- 1 <_ ( abs ` D ) |
| 11 |
|
le0neg1 |
|- ( N e. RR -> ( N <_ 0 <-> 0 <_ -u N ) ) |
| 12 |
4 11
|
ax-mp |
|- ( N <_ 0 <-> 0 <_ -u N ) |
| 13 |
4
|
renegcli |
|- -u N e. RR |
| 14 |
2
|
zrei |
|- D e. RR |
| 15 |
14
|
recni |
|- D e. CC |
| 16 |
15
|
abscli |
|- ( abs ` D ) e. RR |
| 17 |
|
lemulge11 |
|- ( ( ( -u N e. RR /\ ( abs ` D ) e. RR ) /\ ( 0 <_ -u N /\ 1 <_ ( abs ` D ) ) ) -> -u N <_ ( -u N x. ( abs ` D ) ) ) |
| 18 |
13 16 17
|
mpanl12 |
|- ( ( 0 <_ -u N /\ 1 <_ ( abs ` D ) ) -> -u N <_ ( -u N x. ( abs ` D ) ) ) |
| 19 |
12 18
|
sylanb |
|- ( ( N <_ 0 /\ 1 <_ ( abs ` D ) ) -> -u N <_ ( -u N x. ( abs ` D ) ) ) |
| 20 |
10 19
|
mpan2 |
|- ( N <_ 0 -> -u N <_ ( -u N x. ( abs ` D ) ) ) |
| 21 |
4
|
recni |
|- N e. CC |
| 22 |
21 15
|
absmuli |
|- ( abs ` ( N x. D ) ) = ( ( abs ` N ) x. ( abs ` D ) ) |
| 23 |
4
|
absnidi |
|- ( N <_ 0 -> ( abs ` N ) = -u N ) |
| 24 |
23
|
oveq1d |
|- ( N <_ 0 -> ( ( abs ` N ) x. ( abs ` D ) ) = ( -u N x. ( abs ` D ) ) ) |
| 25 |
22 24
|
eqtrid |
|- ( N <_ 0 -> ( abs ` ( N x. D ) ) = ( -u N x. ( abs ` D ) ) ) |
| 26 |
20 25
|
breqtrrd |
|- ( N <_ 0 -> -u N <_ ( abs ` ( N x. D ) ) ) |
| 27 |
|
le0neg2 |
|- ( N e. RR -> ( 0 <_ N <-> -u N <_ 0 ) ) |
| 28 |
4 27
|
ax-mp |
|- ( 0 <_ N <-> -u N <_ 0 ) |
| 29 |
4 14
|
remulcli |
|- ( N x. D ) e. RR |
| 30 |
29
|
recni |
|- ( N x. D ) e. CC |
| 31 |
30
|
absge0i |
|- 0 <_ ( abs ` ( N x. D ) ) |
| 32 |
30
|
abscli |
|- ( abs ` ( N x. D ) ) e. RR |
| 33 |
13 5 32
|
letri |
|- ( ( -u N <_ 0 /\ 0 <_ ( abs ` ( N x. D ) ) ) -> -u N <_ ( abs ` ( N x. D ) ) ) |
| 34 |
31 33
|
mpan2 |
|- ( -u N <_ 0 -> -u N <_ ( abs ` ( N x. D ) ) ) |
| 35 |
28 34
|
sylbi |
|- ( 0 <_ N -> -u N <_ ( abs ` ( N x. D ) ) ) |
| 36 |
26 35
|
jaoi |
|- ( ( N <_ 0 \/ 0 <_ N ) -> -u N <_ ( abs ` ( N x. D ) ) ) |
| 37 |
6 36
|
ax-mp |
|- -u N <_ ( abs ` ( N x. D ) ) |
| 38 |
|
df-neg |
|- -u N = ( 0 - N ) |
| 39 |
38
|
breq1i |
|- ( -u N <_ ( abs ` ( N x. D ) ) <-> ( 0 - N ) <_ ( abs ` ( N x. D ) ) ) |
| 40 |
5 4 32
|
lesubadd2i |
|- ( ( 0 - N ) <_ ( abs ` ( N x. D ) ) <-> 0 <_ ( N + ( abs ` ( N x. D ) ) ) ) |
| 41 |
39 40
|
bitri |
|- ( -u N <_ ( abs ` ( N x. D ) ) <-> 0 <_ ( N + ( abs ` ( N x. D ) ) ) ) |
| 42 |
37 41
|
mpbi |
|- 0 <_ ( N + ( abs ` ( N x. D ) ) ) |