Metamath Proof Explorer

Theorem dvdslelem

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

Ref Expression
Hypotheses dvdslelem.1 ⊢ M ∈ ℤ
dvdslelem.2 ⊢ N ∈ ℕ
dvdslelem.3 ⊢ K ∈ ℤ
Assertion dvdslelem ⊢ N < M → K ⋅ M ≠ N

Proof

Step Hyp Ref Expression
1 dvdslelem.1 ⊢ M ∈ ℤ
2 dvdslelem.2 ⊢ N ∈ ℕ
3 dvdslelem.3 ⊢ K ∈ ℤ
4 3 zrei ⊢ K ∈ ℝ
5 0re ⊢ 0 ∈ ℝ
6 lelttric ⊢ K ∈ ℝ ∧ 0 ∈ ℝ → K ≤ 0 ∨ 0 < K
7 4 5 6 mp2an ⊢ K ≤ 0 ∨ 0 < K
8 zgt0ge1 ⊢ K ∈ ℤ → 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 ∈ ℝ → K ≤ 0 ↔ 0 ≤ − K
13 4 12 ax-mp ⊢ K ≤ 0 ↔ 0 ≤ − K
14 2 nngt0i ⊢ 0 < N
15 2 nnrei ⊢ N ∈ ℝ
16 1 zrei ⊢ M ∈ ℝ
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 ⊢ − K ∈ ℝ
22 21 16 mulge0i ⊢ 0 ≤ − K ∧ 0 ≤ M → 0 ≤ − K ⋅ M
23 20 22 sylan2 ⊢ 0 ≤ − K ∧ N < M → 0 ≤ − K ⋅ M
24 13 23 sylanb ⊢ K ≤ 0 ∧ N < M → 0 ≤ − K ⋅ M
25 24 expcom ⊢ N < M → K ≤ 0 → 0 ≤ − K ⋅ M
26 4 16 remulcli ⊢ K ⋅ M ∈ ℝ
27 le0neg1 ⊢ K ⋅ M ∈ ℝ → K ⋅ M ≤ 0 ↔ 0 ≤ − K ⋅ M
28 26 27 ax-mp ⊢ K ⋅ M ≤ 0 ↔ 0 ≤ − K ⋅ M
29 4 recni ⊢ K ∈ ℂ
30 16 recni ⊢ M ∈ ℂ
31 29 30 mulneg1i ⊢ − K ⋅ M = − K ⋅ M
32 31 breq2i ⊢ 0 ≤ − K ⋅ M ↔ 0 ≤ − K ⋅ M
33 28 32 bitr4i ⊢ K ⋅ M ≤ 0 ↔ 0 ≤ − K ⋅ M
34 25 33 imbitrrdi ⊢ N < M → K ≤ 0 → K ⋅ M ≤ 0
35 26 5 15 lelttri ⊢ K ⋅ M ≤ 0 ∧ 0 < N → K ⋅ M < N
36 14 35 mpan2 ⊢ K ⋅ M ≤ 0 → K ⋅ M < N
37 34 36 syl6 ⊢ N < M → K ≤ 0 → K ⋅ M < N
38 lemulge12 ⊢ M ∈ ℝ ∧ K ∈ ℝ ∧ 0 ≤ M ∧ 1 ≤ K → M ≤ K ⋅ M
39 16 4 38 mpanl12 ⊢ 0 ≤ M ∧ 1 ≤ K → M ≤ K ⋅ M
40 20 39 sylan ⊢ N < M ∧ 1 ≤ K → M ≤ K ⋅ M
41 40 ex ⊢ N < M → 1 ≤ K → M ≤ K ⋅ M
42 15 16 26 ltletri ⊢ N < M ∧ M ≤ K ⋅ M → N < K ⋅ M
43 42 ex ⊢ N < M → M ≤ K ⋅ M → N < K ⋅ M
44 41 43 syld ⊢ N < M → 1 ≤ K → N < K ⋅ M
45 37 44 orim12d ⊢ N < M → K ≤ 0 ∨ 1 ≤ K → K ⋅ M < N ∨ N < K ⋅ M
46 11 45 mpi ⊢ N < M → K ⋅ M < N ∨ N < K ⋅ M
47 26 15 lttri2i ⊢ K ⋅ M ≠ N ↔ K ⋅ M < N ∨ N < K ⋅ M
48 46 47 sylibr ⊢ N < M → K ⋅ M ≠ N