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

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 ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) ∧ ( 1 < 𝑁 ∧ 𝑁 ≤ 𝑀 ) ) → ¬ ( ( ( ! ‘ 𝑀 ) + 1 ) / 𝑁 ) ∈ ℤ )

Proof

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