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 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 ∥ 𝑁 → 𝑀 ≤ 𝑁 ) )

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 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 ∥ 𝑁 → 𝑀 ≤ 𝑁 ) )