Metamath Proof Explorer

Theorem divalglem1

Description: Lemma for divalg . (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Hypotheses divalglem0.1 
|- N e. ZZ
divalglem0.2 
|- D e. ZZ
divalglem1.3 
|- D =/= 0
Assertion divalglem1 
|- 0 <_ ( N + ( abs ` ( N x. D ) ) )

Proof

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 syl5eq 
 |-  ( 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 ) ) )