This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvdslelem

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

Ref Expression
Hypotheses dvdslelem.1 ⊢ 𝑀 ∈ ℤ
dvdslelem.2 ⊢ 𝑁 ∈ ℕ
dvdslelem.3 ⊢ 𝐾 ∈ ℤ
Assertion dvdslelem ( 𝑁 < 𝑀 → ( 𝐾 · 𝑀 ) ≠ 𝑁 )

Proof

Step Hyp Ref Expression
1 dvdslelem.1 ⊢ 𝑀 ∈ ℤ
2 dvdslelem.2 ⊢ 𝑁 ∈ ℕ
3 dvdslelem.3 ⊢ 𝐾 ∈ ℤ
4 3 zrei ⊢ 𝐾 ∈ ℝ
5 0re ⊢ 0 ∈ ℝ
6 lelttric ⊢ ( ( 𝐾 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐾 ≤ 0 ∨ 0 < 𝐾 ) )
7 4 5 6 mp2an ⊢ ( 𝐾 ≤ 0 ∨ 0 < 𝐾 )
8 zgt0ge1 ⊢ ( 𝐾 ∈ ℤ → ( 0 < 𝐾 ↔ 1 ≤ 𝐾 ) )
9 3 8 ax-mp ⊢ ( 0 < 𝐾 ↔ 1 ≤ 𝐾 )
10 9 orbi2i ⊢ ( ( 𝐾 ≤ 0 ∨ 0 < 𝐾 ) ↔ ( 𝐾 ≤ 0 ∨ 1 ≤ 𝐾 ) )
11 7 10 mpbi ⊢ ( 𝐾 ≤ 0 ∨ 1 ≤ 𝐾 )
12 le0neg1 ⊢ ( 𝐾 ∈ ℝ → ( 𝐾 ≤ 0 ↔ 0 ≤ - 𝐾 ) )
13 4 12 ax-mp ⊢ ( 𝐾 ≤ 0 ↔ 0 ≤ - 𝐾 )
14 2 nngt0i ⊢ 0 < 𝑁
15 2 nnrei ⊢ 𝑁 ∈ ℝ
16 1 zrei ⊢ 𝑀 ∈ ℝ
17 5 15 16 lttri ⊢ ( ( 0 < 𝑁 ∧ 𝑁 < 𝑀 ) → 0 < 𝑀 )
18 14 17 mpan ⊢ ( 𝑁 < 𝑀 → 0 < 𝑀 )
19 5 16 ltlei ⊢ ( 0 < 𝑀 → 0 ≤ 𝑀 )
20 18 19 syl ⊢ ( 𝑁 < 𝑀 → 0 ≤ 𝑀 )
21 4 renegcli ⊢ - 𝐾 ∈ ℝ
22 21 16 mulge0i ⊢ ( ( 0 ≤ - 𝐾 ∧ 0 ≤ 𝑀 ) → 0 ≤ ( - 𝐾 · 𝑀 ) )
23 20 22 sylan2 ⊢ ( ( 0 ≤ - 𝐾 ∧ 𝑁 < 𝑀 ) → 0 ≤ ( - 𝐾 · 𝑀 ) )
24 13 23 sylanb ⊢ ( ( 𝐾 ≤ 0 ∧ 𝑁 < 𝑀 ) → 0 ≤ ( - 𝐾 · 𝑀 ) )
25 24 expcom ⊢ ( 𝑁 < 𝑀 → ( 𝐾 ≤ 0 → 0 ≤ ( - 𝐾 · 𝑀 ) ) )
26 4 16 remulcli ⊢ ( 𝐾 · 𝑀 ) ∈ ℝ
27 le0neg1 ⊢ ( ( 𝐾 · 𝑀 ) ∈ ℝ → ( ( 𝐾 · 𝑀 ) ≤ 0 ↔ 0 ≤ - ( 𝐾 · 𝑀 ) ) )
28 26 27 ax-mp ⊢ ( ( 𝐾 · 𝑀 ) ≤ 0 ↔ 0 ≤ - ( 𝐾 · 𝑀 ) )
29 4 recni ⊢ 𝐾 ∈ ℂ
30 16 recni ⊢ 𝑀 ∈ ℂ
31 29 30 mulneg1i ⊢ ( - 𝐾 · 𝑀 ) = - ( 𝐾 · 𝑀 )
32 31 breq2i ⊢ ( 0 ≤ ( - 𝐾 · 𝑀 ) ↔ 0 ≤ - ( 𝐾 · 𝑀 ) )
33 28 32 bitr4i ⊢ ( ( 𝐾 · 𝑀 ) ≤ 0 ↔ 0 ≤ ( - 𝐾 · 𝑀 ) )
34 25 33 imbitrrdi ⊢ ( 𝑁 < 𝑀 → ( 𝐾 ≤ 0 → ( 𝐾 · 𝑀 ) ≤ 0 ) )
35 26 5 15 lelttri ⊢ ( ( ( 𝐾 · 𝑀 ) ≤ 0 ∧ 0 < 𝑁 ) → ( 𝐾 · 𝑀 ) < 𝑁 )
36 14 35 mpan2 ⊢ ( ( 𝐾 · 𝑀 ) ≤ 0 → ( 𝐾 · 𝑀 ) < 𝑁 )
37 34 36 syl6 ⊢ ( 𝑁 < 𝑀 → ( 𝐾 ≤ 0 → ( 𝐾 · 𝑀 ) < 𝑁 ) )
38 lemulge12 ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ) ∧ ( 0 ≤ 𝑀 ∧ 1 ≤ 𝐾 ) ) → 𝑀 ≤ ( 𝐾 · 𝑀 ) )
39 16 4 38 mpanl12 ⊢ ( ( 0 ≤ 𝑀 ∧ 1 ≤ 𝐾 ) → 𝑀 ≤ ( 𝐾 · 𝑀 ) )
40 20 39 sylan ⊢ ( ( 𝑁 < 𝑀 ∧ 1 ≤ 𝐾 ) → 𝑀 ≤ ( 𝐾 · 𝑀 ) )
41 40 ex ⊢ ( 𝑁 < 𝑀 → ( 1 ≤ 𝐾 → 𝑀 ≤ ( 𝐾 · 𝑀 ) ) )
42 15 16 26 ltletri ⊢ ( ( 𝑁 < 𝑀 ∧ 𝑀 ≤ ( 𝐾 · 𝑀 ) ) → 𝑁 < ( 𝐾 · 𝑀 ) )
43 42 ex ⊢ ( 𝑁 < 𝑀 → ( 𝑀 ≤ ( 𝐾 · 𝑀 ) → 𝑁 < ( 𝐾 · 𝑀 ) ) )
44 41 43 syld ⊢ ( 𝑁 < 𝑀 → ( 1 ≤ 𝐾 → 𝑁 < ( 𝐾 · 𝑀 ) ) )
45 37 44 orim12d ⊢ ( 𝑁 < 𝑀 → ( ( 𝐾 ≤ 0 ∨ 1 ≤ 𝐾 ) → ( ( 𝐾 · 𝑀 ) < 𝑁 ∨ 𝑁 < ( 𝐾 · 𝑀 ) ) ) )
46 11 45 mpi ⊢ ( 𝑁 < 𝑀 → ( ( 𝐾 · 𝑀 ) < 𝑁 ∨ 𝑁 < ( 𝐾 · 𝑀 ) ) )
47 26 15 lttri2i ⊢ ( ( 𝐾 · 𝑀 ) ≠ 𝑁 ↔ ( ( 𝐾 · 𝑀 ) < 𝑁 ∨ 𝑁 < ( 𝐾 · 𝑀 ) ) )
48 46 47 sylibr ⊢ ( 𝑁 < 𝑀 → ( 𝐾 · 𝑀 ) ≠ 𝑁 )