Theorem dvdsle

Description: The divisors of a positive integer are bounded by it. The proof does not use / . (Contributed by Paul Chapman, 21-Mar-2011)

	Ref	Expression
Assertion	dvdsle	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 ∥ 𝑁 → 𝑀 ≤ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		breq2	⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) → ( 𝑁 < 𝑀 ↔ 𝑁 < if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) ) )
2		oveq2	⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) → ( 𝑛 · 𝑀 ) = ( 𝑛 · if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) ) )
3	2	neeq1d	⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) → ( ( 𝑛 · 𝑀 ) ≠ 𝑁 ↔ ( 𝑛 · if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) ) ≠ 𝑁 ) )
4	1 3	imbi12d	⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) → ( ( 𝑁 < 𝑀 → ( 𝑛 · 𝑀 ) ≠ 𝑁 ) ↔ ( 𝑁 < if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) → ( 𝑛 · if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) ) ≠ 𝑁 ) ) )
5		breq1	⊢ ( 𝑁 = if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) → ( 𝑁 < if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) ↔ if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) < if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) ) )
6		neeq2	⊢ ( 𝑁 = if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) → ( ( 𝑛 · if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) ) ≠ 𝑁 ↔ ( 𝑛 · if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) ) ≠ if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) ) )
7	5 6	imbi12d	⊢ ( 𝑁 = if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) → ( ( 𝑁 < if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) → ( 𝑛 · if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) ) ≠ 𝑁 ) ↔ ( if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) < if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) → ( 𝑛 · if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) ) ≠ if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) ) ) )
8		oveq1	⊢ ( 𝑛 = if ( 𝑛 ∈ ℤ , 𝑛 , 1 ) → ( 𝑛 · if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) ) = ( if ( 𝑛 ∈ ℤ , 𝑛 , 1 ) · if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) ) )
9	8	neeq1d	⊢ ( 𝑛 = if ( 𝑛 ∈ ℤ , 𝑛 , 1 ) → ( ( 𝑛 · if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) ) ≠ if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) ↔ ( if ( 𝑛 ∈ ℤ , 𝑛 , 1 ) · if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) ) ≠ if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) ) )
10	9	imbi2d	⊢ ( 𝑛 = if ( 𝑛 ∈ ℤ , 𝑛 , 1 ) → ( ( if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) < if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) → ( 𝑛 · if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) ) ≠ if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) ) ↔ ( if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) < if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) → ( if ( 𝑛 ∈ ℤ , 𝑛 , 1 ) · if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) ) ≠ if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) ) ) )
11		1z	⊢ 1 ∈ ℤ
12	11	elimel	⊢ if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) ∈ ℤ
13		1nn	⊢ 1 ∈ ℕ
14	13	elimel	⊢ if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) ∈ ℕ
15	11	elimel	⊢ if ( 𝑛 ∈ ℤ , 𝑛 , 1 ) ∈ ℤ
16	12 14 15	dvdslelem	⊢ ( if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) < if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) → ( if ( 𝑛 ∈ ℤ , 𝑛 , 1 ) · if ( 𝑀 ∈ ℤ , 𝑀 , 1 ) ) ≠ if ( 𝑁 ∈ ℕ , 𝑁 , 1 ) )
17	4 7 10 16	dedth3h	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) → ( 𝑁 < 𝑀 → ( 𝑛 · 𝑀 ) ≠ 𝑁 ) )
18	17	3expia	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑛 ∈ ℤ → ( 𝑁 < 𝑀 → ( 𝑛 · 𝑀 ) ≠ 𝑁 ) ) )
19	18	com23	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 < 𝑀 → ( 𝑛 ∈ ℤ → ( 𝑛 · 𝑀 ) ≠ 𝑁 ) ) )
20	19	3impia	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝑁 < 𝑀 ) → ( 𝑛 ∈ ℤ → ( 𝑛 · 𝑀 ) ≠ 𝑁 ) )
21	20	imp	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝑁 < 𝑀 ) ∧ 𝑛 ∈ ℤ ) → ( 𝑛 · 𝑀 ) ≠ 𝑁 )
22	21	neneqd	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝑁 < 𝑀 ) ∧ 𝑛 ∈ ℤ ) → ¬ ( 𝑛 · 𝑀 ) = 𝑁 )
23	22	nrexdv	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝑁 < 𝑀 ) → ¬ ∃ 𝑛 ∈ ℤ ( 𝑛 · 𝑀 ) = 𝑁 )
24		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
25		divides	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 𝑀 ) = 𝑁 ) )
26	24 25	sylan2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 𝑀 ) = 𝑁 ) )
27	26	3adant3	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝑁 < 𝑀 ) → ( 𝑀 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 𝑀 ) = 𝑁 ) )
28	23 27	mtbird	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 𝑁 < 𝑀 ) → ¬ 𝑀 ∥ 𝑁 )
29	28	3expia	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 < 𝑀 → ¬ 𝑀 ∥ 𝑁 ) )
30	29	con2d	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 ∥ 𝑁 → ¬ 𝑁 < 𝑀 ) )
31		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
32		nnre	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
33		lenlt	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 ≤ 𝑁 ↔ ¬ 𝑁 < 𝑀 ) )
34	31 32 33	syl2an	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 ≤ 𝑁 ↔ ¬ 𝑁 < 𝑀 ) )
35	30 34	sylibrd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 ∥ 𝑁 → 𝑀 ≤ 𝑁 ) )