# Metamath Proof Explorer

## 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 $⊢ M ∈ ℤ ∧ N ∈ ℕ → M ∥ N → M ≤ N$

### Proof

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