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	⊢ ( 𝑁 < 𝑀 → ( 𝐾 · 𝑀 ) ≠ 𝑁 )