This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ¬ 𝑀 ∥ 𝑁 )

Proof

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