nprmdvdsfacm1

Description: A non-prime integer greater than 5 divides the factorial of the integer decreased by 1 (see remark in Ribenboim p. 181). Note: not valid for N = 4 , but for N = 1 ! (Contributed by AV, 7-Apr-2026)

		Ref	Expression
	Assertion	nprmdvdsfacm1	$⊢ (N \in ℤ_{\geq 6} \land N \notin ℙ) \to N ∥ (N - 1)!$

Proof

Step	Hyp	Ref	Expression
1		4z	$⊢ 4 \in ℤ$
2		6nn	$⊢ 6 \in ℕ$
3	2	nnzi	$⊢ 6 \in ℤ$
4		4re	$⊢ 4 \in ℝ$
5		6re	$⊢ 6 \in ℝ$
6		4lt6	$⊢ 4 < 6$
7	4 5 6	ltleii	$⊢ 4 \leq 6$
8		eluz2	$⊢ 6 \in ℤ_{\geq 4} \leftrightarrow (4 \in ℤ \land 6 \in ℤ \land 4 \leq 6)$
9	1 3 7 8	mpbir3an	$⊢ 6 \in ℤ_{\geq 4}$
10		uzss	$⊢ 6 \in ℤ_{\geq 4} \to ℤ_{\geq 6} \subseteq ℤ_{\geq 4}$
11	9 10	ax-mp	$⊢ ℤ_{\geq 6} \subseteq ℤ_{\geq 4}$
12	11	sseli	$⊢ N \in ℤ_{\geq 6} \to N \in ℤ_{\geq 4}$
13		nprmmul3	$⊢ N \in ℤ_{\geq 4} \to (N \notin ℙ \leftrightarrow (\exists a \in (2 ..^N) \exists b \in (2 ..^N) (a < b \land N = a b) \lor \exists a \in (2 ..^N) N = a^{2}))$
14	12 13	syl	$⊢ N \in ℤ_{\geq 6} \to (N \notin ℙ \leftrightarrow (\exists a \in (2 ..^N) \exists b \in (2 ..^N) (a < b \land N = a b) \lor \exists a \in (2 ..^N) N = a^{2}))$
15		elfzo2nn	$⊢ a \in (2 ..^N) \to a \in ℕ$
16	15	ad2antrl	$⊢ (N \in ℤ_{\geq 6} \land (a \in (2 ..^N) \land b \in (2 ..^N))) \to a \in ℕ$
17	16	adantr	$⊢ ((N \in ℤ_{\geq 6} \land (a \in (2 ..^N) \land b \in (2 ..^N))) \land (a < b \land N = a b)) \to a \in ℕ$
18		elfzo2nn	$⊢ b \in (2 ..^N) \to b \in ℕ$
19	18	ad2antll	$⊢ (N \in ℤ_{\geq 6} \land (a \in (2 ..^N) \land b \in (2 ..^N))) \to b \in ℕ$
20	19	adantr	$⊢ ((N \in ℤ_{\geq 6} \land (a \in (2 ..^N) \land b \in (2 ..^N))) \land (a < b \land N = a b)) \to b \in ℕ$
21		simprl	$⊢ ((N \in ℤ_{\geq 6} \land (a \in (2 ..^N) \land b \in (2 ..^N))) \land (a < b \land N = a b)) \to a < b$
22		elfzo1	$⊢ a \in (1 ..^b) \leftrightarrow (a \in ℕ \land b \in ℕ \land a < b)$
23	17 20 21 22	syl3anbrc	$⊢ ((N \in ℤ_{\geq 6} \land (a \in (2 ..^N) \land b \in (2 ..^N))) \land (a < b \land N = a b)) \to a \in (1 ..^b)$
24		2eluzge1	$⊢ 2 \in ℤ_{\geq 1}$
25		fzoss1	$⊢ 2 \in ℤ_{\geq 1} \to (2 ..^N) \subseteq (1 ..^N)$
26	24 25	ax-mp	$⊢ (2 ..^N) \subseteq (1 ..^N)$
27	26	sseli	$⊢ b \in (2 ..^N) \to b \in (1 ..^N)$
28	27	ad2antll	$⊢ (N \in ℤ_{\geq 6} \land (a \in (2 ..^N) \land b \in (2 ..^N))) \to b \in (1 ..^N)$
29	28	adantr	$⊢ ((N \in ℤ_{\geq 6} \land (a \in (2 ..^N) \land b \in (2 ..^N))) \land (a < b \land N = a b)) \to b \in (1 ..^N)$
30		muldvdsfacm1	$⊢ (a \in (1 ..^b) \land b \in (1 ..^N)) \to a b ∥ (N - 1)!$
31	23 29 30	syl2anc	$⊢ ((N \in ℤ_{\geq 6} \land (a \in (2 ..^N) \land b \in (2 ..^N))) \land (a < b \land N = a b)) \to a b ∥ (N - 1)!$
32		breq1	$⊢ N = a b \to (N ∥ (N - 1)! \leftrightarrow a b ∥ (N - 1)!)$
33	32	ad2antll	$⊢ ((N \in ℤ_{\geq 6} \land (a \in (2 ..^N) \land b \in (2 ..^N))) \land (a < b \land N = a b)) \to (N ∥ (N - 1)! \leftrightarrow a b ∥ (N - 1)!)$
34	31 33	mpbird	$⊢ ((N \in ℤ_{\geq 6} \land (a \in (2 ..^N) \land b \in (2 ..^N))) \land (a < b \land N = a b)) \to N ∥ (N - 1)!$
35	34	ex	$⊢ (N \in ℤ_{\geq 6} \land (a \in (2 ..^N) \land b \in (2 ..^N))) \to ((a < b \land N = a b) \to N ∥ (N - 1)!)$
36	35	rexlimdvva	$⊢ N \in ℤ_{\geq 6} \to (\exists a \in (2 ..^N) \exists b \in (2 ..^N) (a < b \land N = a b) \to N ∥ (N - 1)!)$
37		nprmdvdsfacm1lem4	$⊢ (N \in ℤ_{\geq 6} \land a \in (2 ..^N) \land N = a^{2}) \to N ∥ (N - 1)!$
38	37	3expia	$⊢ (N \in ℤ_{\geq 6} \land a \in (2 ..^N)) \to (N = a^{2} \to N ∥ (N - 1)!)$
39	38	rexlimdva	$⊢ N \in ℤ_{\geq 6} \to (\exists a \in (2 ..^N) N = a^{2} \to N ∥ (N - 1)!)$
40	36 39	jaod	$⊢ N \in ℤ_{\geq 6} \to ((\exists a \in (2 ..^N) \exists b \in (2 ..^N) (a < b \land N = a b) \lor \exists a \in (2 ..^N) N = a^{2}) \to N ∥ (N - 1)!)$
41	14 40	sylbid	$⊢ N \in ℤ_{\geq 6} \to (N \notin ℙ \to N ∥ (N - 1)!)$
42	41	imp	$⊢ (N \in ℤ_{\geq 6} \land N \notin ℙ) \to N ∥ (N - 1)!$

Metamath Proof Explorer

Theorem nprmdvdsfacm1

Proof