Metamath Proof Explorer

Theorem fzm1ndvds

Description: No number between 1 and M - 1 divides M . (Contributed by Mario Carneiro, 24-Jan-2015)

Ref Expression
Assertion fzm1ndvds ⊢ M ∈ ℕ ∧ N ∈ 1 … M − 1 → ¬ M ∥ N

Proof

Step Hyp Ref Expression
1 elfzle2 ⊢ N ∈ 1 … M − 1 → N ≤ M − 1
2 1 adantl ⊢ M ∈ ℕ ∧ N ∈ 1 … M − 1 → N ≤ M − 1
3 elfzelz ⊢ N ∈ 1 … M − 1 → N ∈ ℤ
4 3 adantl ⊢ M ∈ ℕ ∧ N ∈ 1 … M − 1 → N ∈ ℤ
5 nnz ⊢ M ∈ ℕ → M ∈ ℤ
6 5 adantr ⊢ M ∈ ℕ ∧ N ∈ 1 … M − 1 → M ∈ ℤ
7 zltlem1 ⊢ N ∈ ℤ ∧ M ∈ ℤ → N < M ↔ N ≤ M − 1
8 4 6 7 syl2anc ⊢ M ∈ ℕ ∧ N ∈ 1 … M − 1 → N < M ↔ N ≤ M − 1
9 2 8 mpbird ⊢ M ∈ ℕ ∧ N ∈ 1 … M − 1 → N < M
10 elfznn ⊢ N ∈ 1 … M − 1 → N ∈ ℕ
11 10 adantl ⊢ M ∈ ℕ ∧ N ∈ 1 … M − 1 → N ∈ ℕ
12 11 nnred ⊢ M ∈ ℕ ∧ N ∈ 1 … M − 1 → N ∈ ℝ
13 nnre ⊢ M ∈ ℕ → M ∈ ℝ
14 13 adantr ⊢ M ∈ ℕ ∧ N ∈ 1 … M − 1 → M ∈ ℝ
15 12 14 ltnled ⊢ M ∈ ℕ ∧ N ∈ 1 … M − 1 → N < M ↔ ¬ M ≤ N
16 9 15 mpbid ⊢ M ∈ ℕ ∧ N ∈ 1 … M − 1 → ¬ M ≤ N
17 dvdsle ⊢ M ∈ ℤ ∧ N ∈ ℕ → M ∥ N → M ≤ N
18 6 11 17 syl2anc ⊢ M ∈ ℕ ∧ N ∈ 1 … M − 1 → M ∥ N → M ≤ N
19 16 18 mtod ⊢ M ∈ ℕ ∧ N ∈ 1 … M − 1 → ¬ M ∥ N