Theorem 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	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑁 ∉ ℙ ) → 𝑁 ∥ ( ! ‘ ( 𝑁 − 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		4z	⊢ 4 ∈ ℤ
2		6nn	⊢ 6 ∈ ℕ
3	2	nnzi	⊢ 6 ∈ ℤ
4		4re	⊢ 4 ∈ ℝ
5		6re	⊢ 6 ∈ ℝ
6		4lt6	⊢ 4 < 6
7	4 5 6	ltleii	⊢ 4 ≤ 6
8		eluz2	⊢ ( 6 ∈ ( ℤ≥ ‘ 4 ) ↔ ( 4 ∈ ℤ ∧ 6 ∈ ℤ ∧ 4 ≤ 6 ) )
9	1 3 7 8	mpbir3an	⊢ 6 ∈ ( ℤ≥ ‘ 4 )
10		uzss	⊢ ( 6 ∈ ( ℤ≥ ‘ 4 ) → ( ℤ≥ ‘ 6 ) ⊆ ( ℤ≥ ‘ 4 ) )
11	9 10	ax-mp	⊢ ( ℤ≥ ‘ 6 ) ⊆ ( ℤ≥ ‘ 4 )
12	11	sseli	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → 𝑁 ∈ ( ℤ≥ ‘ 4 ) )
13		nprmmul3	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 𝑁 ∉ ℙ ↔ ( ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ∨ ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) 𝑁 = ( 𝑎 ↑ 2 ) ) ) )
14	12 13	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → ( 𝑁 ∉ ℙ ↔ ( ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ∨ ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) 𝑁 = ( 𝑎 ↑ 2 ) ) ) )
15		elfzo2nn	⊢ ( 𝑎 ∈ ( 2 ..^ 𝑁 ) → 𝑎 ∈ ℕ )
16	15	ad2antrl	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ ( 𝑎 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑏 ∈ ( 2 ..^ 𝑁 ) ) ) → 𝑎 ∈ ℕ )
17	16	adantr	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ ( 𝑎 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑏 ∈ ( 2 ..^ 𝑁 ) ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ) → 𝑎 ∈ ℕ )
18		elfzo2nn	⊢ ( 𝑏 ∈ ( 2 ..^ 𝑁 ) → 𝑏 ∈ ℕ )
19	18	ad2antll	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ ( 𝑎 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑏 ∈ ( 2 ..^ 𝑁 ) ) ) → 𝑏 ∈ ℕ )
20	19	adantr	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ ( 𝑎 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑏 ∈ ( 2 ..^ 𝑁 ) ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ) → 𝑏 ∈ ℕ )
21		simprl	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ ( 𝑎 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑏 ∈ ( 2 ..^ 𝑁 ) ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ) → 𝑎 < 𝑏 )
22		elfzo1	⊢ ( 𝑎 ∈ ( 1 ..^ 𝑏 ) ↔ ( 𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ ∧ 𝑎 < 𝑏 ) )
23	17 20 21 22	syl3anbrc	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ ( 𝑎 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑏 ∈ ( 2 ..^ 𝑁 ) ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ) → 𝑎 ∈ ( 1 ..^ 𝑏 ) )
24		2eluzge1	⊢ 2 ∈ ( ℤ≥ ‘ 1 )
25		fzoss1	⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → ( 2 ..^ 𝑁 ) ⊆ ( 1 ..^ 𝑁 ) )
26	24 25	ax-mp	⊢ ( 2 ..^ 𝑁 ) ⊆ ( 1 ..^ 𝑁 )
27	26	sseli	⊢ ( 𝑏 ∈ ( 2 ..^ 𝑁 ) → 𝑏 ∈ ( 1 ..^ 𝑁 ) )
28	27	ad2antll	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ ( 𝑎 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑏 ∈ ( 2 ..^ 𝑁 ) ) ) → 𝑏 ∈ ( 1 ..^ 𝑁 ) )
29	28	adantr	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ ( 𝑎 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑏 ∈ ( 2 ..^ 𝑁 ) ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ) → 𝑏 ∈ ( 1 ..^ 𝑁 ) )
30		muldvdsfacm1	⊢ ( ( 𝑎 ∈ ( 1 ..^ 𝑏 ) ∧ 𝑏 ∈ ( 1 ..^ 𝑁 ) ) → ( 𝑎 · 𝑏 ) ∥ ( ! ‘ ( 𝑁 − 1 ) ) )
31	23 29 30	syl2anc	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ ( 𝑎 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑏 ∈ ( 2 ..^ 𝑁 ) ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ) → ( 𝑎 · 𝑏 ) ∥ ( ! ‘ ( 𝑁 − 1 ) ) )
32		breq1	⊢ ( 𝑁 = ( 𝑎 · 𝑏 ) → ( 𝑁 ∥ ( ! ‘ ( 𝑁 − 1 ) ) ↔ ( 𝑎 · 𝑏 ) ∥ ( ! ‘ ( 𝑁 − 1 ) ) ) )
33	32	ad2antll	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ ( 𝑎 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑏 ∈ ( 2 ..^ 𝑁 ) ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ) → ( 𝑁 ∥ ( ! ‘ ( 𝑁 − 1 ) ) ↔ ( 𝑎 · 𝑏 ) ∥ ( ! ‘ ( 𝑁 − 1 ) ) ) )
34	31 33	mpbird	⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ ( 𝑎 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑏 ∈ ( 2 ..^ 𝑁 ) ) ) ∧ ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ) → 𝑁 ∥ ( ! ‘ ( 𝑁 − 1 ) ) )
35	34	ex	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ ( 𝑎 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑏 ∈ ( 2 ..^ 𝑁 ) ) ) → ( ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) → 𝑁 ∥ ( ! ‘ ( 𝑁 − 1 ) ) ) )
36	35	rexlimdvva	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → ( ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) → 𝑁 ∥ ( ! ‘ ( 𝑁 − 1 ) ) ) )
37		nprmdvdsfacm1lem4	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝑎 ↑ 2 ) ) → 𝑁 ∥ ( ! ‘ ( 𝑁 − 1 ) ) )
38	37	3expia	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) → ( 𝑁 = ( 𝑎 ↑ 2 ) → 𝑁 ∥ ( ! ‘ ( 𝑁 − 1 ) ) ) )
39	38	rexlimdva	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → ( ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) 𝑁 = ( 𝑎 ↑ 2 ) → 𝑁 ∥ ( ! ‘ ( 𝑁 − 1 ) ) ) )
40	36 39	jaod	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → ( ( ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ∨ ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) 𝑁 = ( 𝑎 ↑ 2 ) ) → 𝑁 ∥ ( ! ‘ ( 𝑁 − 1 ) ) ) )
41	14 40	sylbid	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → ( 𝑁 ∉ ℙ → 𝑁 ∥ ( ! ‘ ( 𝑁 − 1 ) ) ) )
42	41	imp	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑁 ∉ ℙ ) → 𝑁 ∥ ( ! ‘ ( 𝑁 − 1 ) ) )