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 \in ℕ_{0} \land N \in ℕ) \land (1 < N \land N \leq M)) \to \neg \frac{M! + 1}{N} \in ℤ$

Proof

Step	Hyp	Ref	Expression
1		nnre	$⊢ N \in ℕ \to N \in ℝ$
2		recnz	$⊢ (N \in ℝ \land 1 < N) \to \neg \frac{1}{N} \in ℤ$
3	1 2	sylan	$⊢ (N \in ℕ \land 1 < N) \to \neg \frac{1}{N} \in ℤ$
4	3	ad2ant2lr	$⊢ ((M \in ℕ_{0} \land N \in ℕ) \land (1 < N \land N \leq M)) \to \neg \frac{1}{N} \in ℤ$
5		facdiv	$⊢ (M \in ℕ_{0} \land N \in ℕ \land N \leq M) \to \frac{M!}{N} \in ℕ$
6	5	3expa	$⊢ ((M \in ℕ_{0} \land N \in ℕ) \land N \leq M) \to \frac{M!}{N} \in ℕ$
7	6	nnzd	$⊢ ((M \in ℕ_{0} \land N \in ℕ) \land N \leq M) \to \frac{M!}{N} \in ℤ$
8	7	adantrl	$⊢ ((M \in ℕ_{0} \land N \in ℕ) \land (1 < N \land N \leq M)) \to \frac{M!}{N} \in ℤ$
9		zsubcl	$⊢ (\frac{M! + 1}{N} \in ℤ \land \frac{M!}{N} \in ℤ) \to (\frac{M! + 1}{N}) - (\frac{M!}{N}) \in ℤ$
10	9	ex	$⊢ \frac{M! + 1}{N} \in ℤ \to (\frac{M!}{N} \in ℤ \to (\frac{M! + 1}{N}) - (\frac{M!}{N}) \in ℤ)$
11	8 10	syl5com	$⊢ ((M \in ℕ_{0} \land N \in ℕ) \land (1 < N \land N \leq M)) \to (\frac{M! + 1}{N} \in ℤ \to (\frac{M! + 1}{N}) - (\frac{M!}{N}) \in ℤ)$
12		faccl	$⊢ M \in ℕ_{0} \to M! \in ℕ$
13	12	nncnd	$⊢ M \in ℕ_{0} \to M! \in ℂ$
14		peano2cn	$⊢ M! \in ℂ \to M! + 1 \in ℂ$
15	13 14	syl	$⊢ M \in ℕ_{0} \to M! + 1 \in ℂ$
16	15	ad2antrr	$⊢ ((M \in ℕ_{0} \land N \in ℕ) \land (1 < N \land N \leq M)) \to M! + 1 \in ℂ$
17	13	ad2antrr	$⊢ ((M \in ℕ_{0} \land N \in ℕ) \land (1 < N \land N \leq M)) \to M! \in ℂ$
18		nncn	$⊢ N \in ℕ \to N \in ℂ$
19		nnne0	$⊢ N \in ℕ \to N \neq 0$
20	18 19	jca	$⊢ N \in ℕ \to (N \in ℂ \land N \neq 0)$
21	20	ad2antlr	$⊢ ((M \in ℕ_{0} \land N \in ℕ) \land (1 < N \land N \leq M)) \to (N \in ℂ \land N \neq 0)$
22		divsubdir	$⊢ (M! + 1 \in ℂ \land M! \in ℂ \land (N \in ℂ \land N \neq 0)) \to \frac{M! + 1 - M!}{N} = (\frac{M! + 1}{N}) - (\frac{M!}{N})$
23	16 17 21 22	syl3anc	$⊢ ((M \in ℕ_{0} \land N \in ℕ) \land (1 < N \land N \leq M)) \to \frac{M! + 1 - M!}{N} = (\frac{M! + 1}{N}) - (\frac{M!}{N})$
24		ax-1cn	$⊢ 1 \in ℂ$
25		pncan2	$⊢ (M! \in ℂ \land 1 \in ℂ) \to M! + 1 - M! = 1$
26	13 24 25	sylancl	$⊢ M \in ℕ_{0} \to M! + 1 - M! = 1$
27	26	oveq1d	$⊢ M \in ℕ_{0} \to \frac{M! + 1 - M!}{N} = \frac{1}{N}$
28	27	ad2antrr	$⊢ ((M \in ℕ_{0} \land N \in ℕ) \land (1 < N \land N \leq M)) \to \frac{M! + 1 - M!}{N} = \frac{1}{N}$
29	23 28	eqtr3d	$⊢ ((M \in ℕ_{0} \land N \in ℕ) \land (1 < N \land N \leq M)) \to (\frac{M! + 1}{N}) - (\frac{M!}{N}) = \frac{1}{N}$
30	29	eleq1d	$⊢ ((M \in ℕ_{0} \land N \in ℕ) \land (1 < N \land N \leq M)) \to ((\frac{M! + 1}{N}) - (\frac{M!}{N}) \in ℤ \leftrightarrow \frac{1}{N} \in ℤ)$
31	11 30	sylibd	$⊢ ((M \in ℕ_{0} \land N \in ℕ) \land (1 < N \land N \leq M)) \to (\frac{M! + 1}{N} \in ℤ \to \frac{1}{N} \in ℤ)$
32	4 31	mtod	$⊢ ((M \in ℕ_{0} \land N \in ℕ) \land (1 < N \land N \leq M)) \to \neg \frac{M! + 1}{N} \in ℤ$

Metamath Proof Explorer

Theorem facndiv

Proof