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 ) / 𝑁 ) ∈ ℤ )