Metamath Proof Explorer

Theorem dvdslelem

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

Ref Expression
Hypotheses dvdslelem.1 ${⊢}{M}\in ℤ$
dvdslelem.2 ${⊢}{N}\in ℕ$
dvdslelem.3 ${⊢}{K}\in ℤ$
Assertion dvdslelem ${⊢}{N}<{M}\to {K}\cdot {M}\ne {N}$

Proof

Step Hyp Ref Expression
1 dvdslelem.1 ${⊢}{M}\in ℤ$
2 dvdslelem.2 ${⊢}{N}\in ℕ$
3 dvdslelem.3 ${⊢}{K}\in ℤ$
4 3 zrei ${⊢}{K}\in ℝ$
5 0re ${⊢}0\in ℝ$
6 lelttric ${⊢}\left({K}\in ℝ\wedge 0\in ℝ\right)\to \left({K}\le 0\vee 0<{K}\right)$
7 4 5 6 mp2an ${⊢}\left({K}\le 0\vee 0<{K}\right)$
8 zgt0ge1 ${⊢}{K}\in ℤ\to \left(0<{K}↔1\le {K}\right)$
9 3 8 ax-mp ${⊢}0<{K}↔1\le {K}$
10 9 orbi2i ${⊢}\left({K}\le 0\vee 0<{K}\right)↔\left({K}\le 0\vee 1\le {K}\right)$
11 7 10 mpbi ${⊢}\left({K}\le 0\vee 1\le {K}\right)$
12 le0neg1 ${⊢}{K}\in ℝ\to \left({K}\le 0↔0\le -{K}\right)$
13 4 12 ax-mp ${⊢}{K}\le 0↔0\le -{K}$
14 2 nngt0i ${⊢}0<{N}$
15 2 nnrei ${⊢}{N}\in ℝ$
16 1 zrei ${⊢}{M}\in ℝ$
17 5 15 16 lttri ${⊢}\left(0<{N}\wedge {N}<{M}\right)\to 0<{M}$
18 14 17 mpan ${⊢}{N}<{M}\to 0<{M}$
19 5 16 ltlei ${⊢}0<{M}\to 0\le {M}$
20 18 19 syl ${⊢}{N}<{M}\to 0\le {M}$
21 4 renegcli ${⊢}-{K}\in ℝ$
22 21 16 mulge0i ${⊢}\left(0\le -{K}\wedge 0\le {M}\right)\to 0\le \left(-{K}\right)\cdot {M}$
23 20 22 sylan2 ${⊢}\left(0\le -{K}\wedge {N}<{M}\right)\to 0\le \left(-{K}\right)\cdot {M}$
24 13 23 sylanb ${⊢}\left({K}\le 0\wedge {N}<{M}\right)\to 0\le \left(-{K}\right)\cdot {M}$
25 24 expcom ${⊢}{N}<{M}\to \left({K}\le 0\to 0\le \left(-{K}\right)\cdot {M}\right)$
26 4 16 remulcli ${⊢}{K}\cdot {M}\in ℝ$
27 le0neg1 ${⊢}{K}\cdot {M}\in ℝ\to \left({K}\cdot {M}\le 0↔0\le -{K}\cdot {M}\right)$
28 26 27 ax-mp ${⊢}{K}\cdot {M}\le 0↔0\le -{K}\cdot {M}$
29 4 recni ${⊢}{K}\in ℂ$
30 16 recni ${⊢}{M}\in ℂ$
31 29 30 mulneg1i ${⊢}\left(-{K}\right)\cdot {M}=-{K}\cdot {M}$
32 31 breq2i ${⊢}0\le \left(-{K}\right)\cdot {M}↔0\le -{K}\cdot {M}$
33 28 32 bitr4i ${⊢}{K}\cdot {M}\le 0↔0\le \left(-{K}\right)\cdot {M}$
34 25 33 syl6ibr ${⊢}{N}<{M}\to \left({K}\le 0\to {K}\cdot {M}\le 0\right)$
35 26 5 15 lelttri ${⊢}\left({K}\cdot {M}\le 0\wedge 0<{N}\right)\to {K}\cdot {M}<{N}$
36 14 35 mpan2 ${⊢}{K}\cdot {M}\le 0\to {K}\cdot {M}<{N}$
37 34 36 syl6 ${⊢}{N}<{M}\to \left({K}\le 0\to {K}\cdot {M}<{N}\right)$
38 lemulge12 ${⊢}\left(\left({M}\in ℝ\wedge {K}\in ℝ\right)\wedge \left(0\le {M}\wedge 1\le {K}\right)\right)\to {M}\le {K}\cdot {M}$
39 16 4 38 mpanl12 ${⊢}\left(0\le {M}\wedge 1\le {K}\right)\to {M}\le {K}\cdot {M}$
40 20 39 sylan ${⊢}\left({N}<{M}\wedge 1\le {K}\right)\to {M}\le {K}\cdot {M}$
41 40 ex ${⊢}{N}<{M}\to \left(1\le {K}\to {M}\le {K}\cdot {M}\right)$
42 15 16 26 ltletri ${⊢}\left({N}<{M}\wedge {M}\le {K}\cdot {M}\right)\to {N}<{K}\cdot {M}$
43 42 ex ${⊢}{N}<{M}\to \left({M}\le {K}\cdot {M}\to {N}<{K}\cdot {M}\right)$
44 41 43 syld ${⊢}{N}<{M}\to \left(1\le {K}\to {N}<{K}\cdot {M}\right)$
45 37 44 orim12d ${⊢}{N}<{M}\to \left(\left({K}\le 0\vee 1\le {K}\right)\to \left({K}\cdot {M}<{N}\vee {N}<{K}\cdot {M}\right)\right)$
46 11 45 mpi ${⊢}{N}<{M}\to \left({K}\cdot {M}<{N}\vee {N}<{K}\cdot {M}\right)$
47 26 15 lttri2i ${⊢}{K}\cdot {M}\ne {N}↔\left({K}\cdot {M}<{N}\vee {N}<{K}\cdot {M}\right)$
48 46 47 sylibr ${⊢}{N}<{M}\to {K}\cdot {M}\ne {N}$