Metamath Proof Explorer

Theorem dvdslelem

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

Ref Expression
Hypotheses dvdslelem.1 
|- M e. ZZ
dvdslelem.2 
|- N e. NN
dvdslelem.3 
|- K e. ZZ
Assertion dvdslelem 
|- ( N < M -> ( K x. M ) =/= N )

Proof

Step Hyp Ref Expression
1 dvdslelem.1 
 |-  M e. ZZ
2 dvdslelem.2 
 |-  N e. NN
3 dvdslelem.3 
 |-  K e. ZZ
4 3 zrei 
 |-  K e. RR
5 0re 
 |-  0 e. RR
6 lelttric 
 |-  ( ( K e. RR /\ 0 e. RR ) -> ( K <_ 0 \/ 0 < K ) )
7 4 5 6 mp2an 
 |-  ( K <_ 0 \/ 0 < K )
8 zgt0ge1 
 |-  ( K e. ZZ -> ( 0 < K <-> 1 <_ K ) )
9 3 8 ax-mp 
 |-  ( 0 < K <-> 1 <_ K )
10 9 orbi2i 
 |-  ( ( K <_ 0 \/ 0 < K ) <-> ( K <_ 0 \/ 1 <_ K ) )
11 7 10 mpbi 
 |-  ( K <_ 0 \/ 1 <_ K )
12 le0neg1 
 |-  ( K e. RR -> ( K <_ 0 <-> 0 <_ -u K ) )
13 4 12 ax-mp 
 |-  ( K <_ 0 <-> 0 <_ -u K )
14 2 nngt0i 
 |-  0 < N
15 2 nnrei 
 |-  N e. RR
16 1 zrei 
 |-  M e. RR
17 5 15 16 lttri 
 |-  ( ( 0 < N /\ N < M ) -> 0 < M )
18 14 17 mpan 
 |-  ( N < M -> 0 < M )
19 5 16 ltlei 
 |-  ( 0 < M -> 0 <_ M )
20 18 19 syl 
 |-  ( N < M -> 0 <_ M )
21 4 renegcli 
 |-  -u K e. RR
22 21 16 mulge0i 
 |-  ( ( 0 <_ -u K /\ 0 <_ M ) -> 0 <_ ( -u K x. M ) )
23 20 22 sylan2 
 |-  ( ( 0 <_ -u K /\ N < M ) -> 0 <_ ( -u K x. M ) )
24 13 23 sylanb 
 |-  ( ( K <_ 0 /\ N < M ) -> 0 <_ ( -u K x. M ) )
25 24 expcom 
 |-  ( N < M -> ( K <_ 0 -> 0 <_ ( -u K x. M ) ) )
26 4 16 remulcli 
 |-  ( K x. M ) e. RR
27 le0neg1 
 |-  ( ( K x. M ) e. RR -> ( ( K x. M ) <_ 0 <-> 0 <_ -u ( K x. M ) ) )
28 26 27 ax-mp 
 |-  ( ( K x. M ) <_ 0 <-> 0 <_ -u ( K x. M ) )
29 4 recni 
 |-  K e. CC
30 16 recni 
 |-  M e. CC
31 29 30 mulneg1i 
 |-  ( -u K x. M ) = -u ( K x. M )
32 31 breq2i 
 |-  ( 0 <_ ( -u K x. M ) <-> 0 <_ -u ( K x. M ) )
33 28 32 bitr4i 
 |-  ( ( K x. M ) <_ 0 <-> 0 <_ ( -u K x. M ) )
34 25 33 syl6ibr 
 |-  ( N < M -> ( K <_ 0 -> ( K x. M ) <_ 0 ) )
35 26 5 15 lelttri 
 |-  ( ( ( K x. M ) <_ 0 /\ 0 < N ) -> ( K x. M ) < N )
36 14 35 mpan2 
 |-  ( ( K x. M ) <_ 0 -> ( K x. M ) < N )
37 34 36 syl6 
 |-  ( N < M -> ( K <_ 0 -> ( K x. M ) < N ) )
38 lemulge12 
 |-  ( ( ( M e. RR /\ K e. RR ) /\ ( 0 <_ M /\ 1 <_ K ) ) -> M <_ ( K x. M ) )
39 16 4 38 mpanl12 
 |-  ( ( 0 <_ M /\ 1 <_ K ) -> M <_ ( K x. M ) )
40 20 39 sylan 
 |-  ( ( N < M /\ 1 <_ K ) -> M <_ ( K x. M ) )
41 40 ex 
 |-  ( N < M -> ( 1 <_ K -> M <_ ( K x. M ) ) )
42 15 16 26 ltletri 
 |-  ( ( N < M /\ M <_ ( K x. M ) ) -> N < ( K x. M ) )
43 42 ex 
 |-  ( N < M -> ( M <_ ( K x. M ) -> N < ( K x. M ) ) )
44 41 43 syld 
 |-  ( N < M -> ( 1 <_ K -> N < ( K x. M ) ) )
45 37 44 orim12d 
 |-  ( N < M -> ( ( K <_ 0 \/ 1 <_ K ) -> ( ( K x. M ) < N \/ N < ( K x. M ) ) ) )
46 11 45 mpi 
 |-  ( N < M -> ( ( K x. M ) < N \/ N < ( K x. M ) ) )
47 26 15 lttri2i 
 |-  ( ( K x. M ) =/= N <-> ( ( K x. M ) < N \/ N < ( K x. M ) ) )
48 46 47 sylibr 
 |-  ( N < M -> ( K x. M ) =/= N )