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