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=ifM∈ℤM1→N<M↔N<ifM∈ℤM1
2 oveq2 ⊢M=ifM∈ℤM1→n⋅ M=n⁢ifM∈ℤM1
3 2 neeq1d ⊢M=ifM∈ℤM1→n⋅ M≠N↔n⁢ifM∈ℤM1≠N
4 1 3 imbi12d ⊢M=ifM∈ℤM1→N<M→n⋅ M≠N↔N<ifM∈ℤM1→n⁢ifM∈ℤM1≠N
5 breq1 ⊢N=ifN∈ℕN1→N<ifM∈ℤM1↔ifN∈ℕN1<ifM∈ℤM1
6 neeq2 ⊢N=ifN∈ℕN1→n⁢ifM∈ℤM1≠N↔n⁢ifM∈ℤM1≠ifN∈ℕN1
7 5 6 imbi12d ⊢N=ifN∈ℕN1→N<ifM∈ℤM1→n⁢ifM∈ℤM1≠N↔ifN∈ℕN1<ifM∈ℤM1→n⁢ifM∈ℤM1≠ifN∈ℕN1
8 oveq1 ⊢n=ifn∈ℤn1→n⁢ifM∈ℤM1=ifn∈ℤn1⁢ifM∈ℤM1
9 8 neeq1d ⊢n=ifn∈ℤn1→n⁢ifM∈ℤM1≠ifN∈ℕN1↔ifn∈ℤn1⁢ifM∈ℤM1≠ifN∈ℕN1
10 9 imbi2d ⊢n=ifn∈ℤn1→ifN∈ℕN1<ifM∈ℤM1→n⁢ifM∈ℤM1≠ifN∈ℕN1↔ifN∈ℕN1<ifM∈ℤM1→ifn∈ℤn1⁢ifM∈ℤM1≠ifN∈ℕN1
11 1z ⊢1∈ℤ
12 11 elimel ⊢ifM∈ℤM1∈ℤ
13 1nn ⊢1∈ℕ
14 13 elimel ⊢ifN∈ℕN1∈ℕ
15 11 elimel ⊢ifn∈ℤn1∈ℤ
16 12 14 15 dvdslelem ⊢ifN∈ℕN1<ifM∈ℤM1→ifn∈ℤn1⁢ifM∈ℤM1≠ifN∈ℕN1
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