Metamath Proof Explorer

Theorem facndiv

Description: No positive integer (greater than one) divides the factorial plus one of an equal or larger number. (Contributed by NM, 3-May-2005)

Ref Expression
Assertion facndiv ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ ∧ 1 < N ∧ N ≤ M → ¬ M ! + 1 N ∈ ℤ

Proof

Step Hyp Ref Expression
1 nnre ⊢ N ∈ ℕ → N ∈ ℝ
2 recnz ⊢ N ∈ ℝ ∧ 1 < N → ¬ 1 N ∈ ℤ
3 1 2 sylan ⊢ N ∈ ℕ ∧ 1 < N → ¬ 1 N ∈ ℤ
4 3 ad2ant2lr ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ ∧ 1 < N ∧ N ≤ M → ¬ 1 N ∈ ℤ
5 facdiv ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ ∧ N ≤ M → M ! N ∈ ℕ
6 5 3expa ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ ∧ N ≤ M → M ! N ∈ ℕ
7 6 nnzd ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ ∧ N ≤ M → M ! N ∈ ℤ
8 7 adantrl ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ ∧ 1 < N ∧ N ≤ M → M ! N ∈ ℤ
9 zsubcl ⊢ M ! + 1 N ∈ ℤ ∧ M ! N ∈ ℤ → M ! + 1 N − M ! N ∈ ℤ
10 9 ex ⊢ M ! + 1 N ∈ ℤ → M ! N ∈ ℤ → M ! + 1 N − M ! N ∈ ℤ
11 8 10 syl5com ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ ∧ 1 < N ∧ N ≤ M → M ! + 1 N ∈ ℤ → M ! + 1 N − M ! N ∈ ℤ
12 faccl ⊢ M ∈ ℕ 0 → M ! ∈ ℕ
13 12 nncnd ⊢ M ∈ ℕ 0 → M ! ∈ ℂ
14 peano2cn ⊢ M ! ∈ ℂ → M ! + 1 ∈ ℂ
15 13 14 syl ⊢ M ∈ ℕ 0 → M ! + 1 ∈ ℂ
16 15 ad2antrr ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ ∧ 1 < N ∧ N ≤ M → M ! + 1 ∈ ℂ
17 13 ad2antrr ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ ∧ 1 < N ∧ N ≤ M → M ! ∈ ℂ
18 nncn ⊢ N ∈ ℕ → N ∈ ℂ
19 nnne0 ⊢ N ∈ ℕ → N ≠ 0
20 18 19 jca ⊢ N ∈ ℕ → N ∈ ℂ ∧ N ≠ 0
21 20 ad2antlr ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ ∧ 1 < N ∧ N ≤ M → N ∈ ℂ ∧ N ≠ 0
22 divsubdir ⊢ M ! + 1 ∈ ℂ ∧ M ! ∈ ℂ ∧ N ∈ ℂ ∧ N ≠ 0 → M ! + 1 - M ! N = M ! + 1 N − M ! N
23 16 17 21 22 syl3anc ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ ∧ 1 < N ∧ N ≤ M → M ! + 1 - M ! N = M ! + 1 N − M ! N
24 ax-1cn ⊢ 1 ∈ ℂ
25 pncan2 ⊢ M ! ∈ ℂ ∧ 1 ∈ ℂ → M ! + 1 - M ! = 1
26 13 24 25 sylancl ⊢ M ∈ ℕ 0 → M ! + 1 - M ! = 1
27 26 oveq1d ⊢ M ∈ ℕ 0 → M ! + 1 - M ! N = 1 N
28 27 ad2antrr ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ ∧ 1 < N ∧ N ≤ M → M ! + 1 - M ! N = 1 N
29 23 28 eqtr3d ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ ∧ 1 < N ∧ N ≤ M → M ! + 1 N − M ! N = 1 N
30 29 eleq1d ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ ∧ 1 < N ∧ N ≤ M → M ! + 1 N − M ! N ∈ ℤ ↔ 1 N ∈ ℤ
31 11 30 sylibd ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ ∧ 1 < N ∧ N ≤ M → M ! + 1 N ∈ ℤ → 1 N ∈ ℤ
32 4 31 mtod ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ ∧ 1 < N ∧ N ≤ M → ¬ M ! + 1 N ∈ ℤ