Theorem muldvdsfacm1

Description: The product of two different positive integers less than a third integer divides the factorial of the third integer decreased by 1. By assumption, the third integer must be greater than 3. (Contributed by AV, 6-Apr-2026)

	Ref	Expression
Assertion	muldvdsfacm1	⊢ ( ( 𝐴 ∈ ( 1 ..^ 𝐵 ) ∧ 𝐵 ∈ ( 1 ..^ 𝑁 ) ) → ( 𝐴 · 𝐵 ) ∥ ( ! ‘ ( 𝑁 − 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elfzoelz	⊢ ( 𝐴 ∈ ( 1 ..^ 𝐵 ) → 𝐴 ∈ ℤ )
2		elfzoelz	⊢ ( 𝐵 ∈ ( 1 ..^ 𝑁 ) → 𝐵 ∈ ℤ )
3		zmulcl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 · 𝐵 ) ∈ ℤ )
4	1 2 3	syl2an	⊢ ( ( 𝐴 ∈ ( 1 ..^ 𝐵 ) ∧ 𝐵 ∈ ( 1 ..^ 𝑁 ) ) → ( 𝐴 · 𝐵 ) ∈ ℤ )
5		elfzo2	⊢ ( 𝐵 ∈ ( 1 ..^ 𝑁 ) ↔ ( 𝐵 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ℤ ∧ 𝐵 < 𝑁 ) )
6		elnnuz	⊢ ( 𝐵 ∈ ℕ ↔ 𝐵 ∈ ( ℤ≥ ‘ 1 ) )
7		nnnn0	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℕ0 )
8	6 7	sylbir	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 1 ) → 𝐵 ∈ ℕ0 )
9	8	3ad2ant1	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ℤ ∧ 𝐵 < 𝑁 ) → 𝐵 ∈ ℕ0 )
10	5 9	sylbi	⊢ ( 𝐵 ∈ ( 1 ..^ 𝑁 ) → 𝐵 ∈ ℕ0 )
11	10	adantl	⊢ ( ( 𝐴 ∈ ( 1 ..^ 𝐵 ) ∧ 𝐵 ∈ ( 1 ..^ 𝑁 ) ) → 𝐵 ∈ ℕ0 )
12	11	faccld	⊢ ( ( 𝐴 ∈ ( 1 ..^ 𝐵 ) ∧ 𝐵 ∈ ( 1 ..^ 𝑁 ) ) → ( ! ‘ 𝐵 ) ∈ ℕ )
13	12	nnzd	⊢ ( ( 𝐴 ∈ ( 1 ..^ 𝐵 ) ∧ 𝐵 ∈ ( 1 ..^ 𝑁 ) ) → ( ! ‘ 𝐵 ) ∈ ℤ )
14		simp2	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ℤ ∧ 𝐵 < 𝑁 ) → 𝑁 ∈ ℤ )
15		eluz2	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 1 ) ↔ ( 1 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 1 ≤ 𝐵 ) )
16		1red	⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 1 ∈ ℝ )
17		zre	⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℝ )
18	17	adantr	⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝐵 ∈ ℝ )
19		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
20	19	adantl	⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℝ )
21		lelttr	⊢ ( ( 1 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 1 ≤ 𝐵 ∧ 𝐵 < 𝑁 ) → 1 < 𝑁 ) )
22	16 18 20 21	syl3anc	⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 1 ≤ 𝐵 ∧ 𝐵 < 𝑁 ) → 1 < 𝑁 ) )
23		0lt1	⊢ 0 < 1
24		0red	⊢ ( 𝑁 ∈ ℤ → 0 ∈ ℝ )
25		1red	⊢ ( 𝑁 ∈ ℤ → 1 ∈ ℝ )
26		lttr	⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 0 < 1 ∧ 1 < 𝑁 ) → 0 < 𝑁 ) )
27	24 25 19 26	syl3anc	⊢ ( 𝑁 ∈ ℤ → ( ( 0 < 1 ∧ 1 < 𝑁 ) → 0 < 𝑁 ) )
28	23 27	mpani	⊢ ( 𝑁 ∈ ℤ → ( 1 < 𝑁 → 0 < 𝑁 ) )
29	28	adantl	⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 1 < 𝑁 → 0 < 𝑁 ) )
30	22 29	syld	⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 1 ≤ 𝐵 ∧ 𝐵 < 𝑁 ) → 0 < 𝑁 ) )
31	30	exp4b	⊢ ( 𝐵 ∈ ℤ → ( 𝑁 ∈ ℤ → ( 1 ≤ 𝐵 → ( 𝐵 < 𝑁 → 0 < 𝑁 ) ) ) )
32	31	com23	⊢ ( 𝐵 ∈ ℤ → ( 1 ≤ 𝐵 → ( 𝑁 ∈ ℤ → ( 𝐵 < 𝑁 → 0 < 𝑁 ) ) ) )
33	32	a1i	⊢ ( 1 ∈ ℤ → ( 𝐵 ∈ ℤ → ( 1 ≤ 𝐵 → ( 𝑁 ∈ ℤ → ( 𝐵 < 𝑁 → 0 < 𝑁 ) ) ) ) )
34	33	3imp	⊢ ( ( 1 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 1 ≤ 𝐵 ) → ( 𝑁 ∈ ℤ → ( 𝐵 < 𝑁 → 0 < 𝑁 ) ) )
35	15 34	sylbi	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 1 ) → ( 𝑁 ∈ ℤ → ( 𝐵 < 𝑁 → 0 < 𝑁 ) ) )
36	35	3imp	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ℤ ∧ 𝐵 < 𝑁 ) → 0 < 𝑁 )
37		elnnz	⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) )
38	14 36 37	sylanbrc	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ℤ ∧ 𝐵 < 𝑁 ) → 𝑁 ∈ ℕ )
39		nnm1nn0	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
40	38 39	syl	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ℤ ∧ 𝐵 < 𝑁 ) → ( 𝑁 − 1 ) ∈ ℕ0 )
41	5 40	sylbi	⊢ ( 𝐵 ∈ ( 1 ..^ 𝑁 ) → ( 𝑁 − 1 ) ∈ ℕ0 )
42	41	adantl	⊢ ( ( 𝐴 ∈ ( 1 ..^ 𝐵 ) ∧ 𝐵 ∈ ( 1 ..^ 𝑁 ) ) → ( 𝑁 − 1 ) ∈ ℕ0 )
43	42	faccld	⊢ ( ( 𝐴 ∈ ( 1 ..^ 𝐵 ) ∧ 𝐵 ∈ ( 1 ..^ 𝑁 ) ) → ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℕ )
44	43	nnzd	⊢ ( ( 𝐴 ∈ ( 1 ..^ 𝐵 ) ∧ 𝐵 ∈ ( 1 ..^ 𝑁 ) ) → ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℤ )
45		muldvdsfacgt	⊢ ( 𝐴 ∈ ( 1 ..^ 𝐵 ) → ( 𝐴 · 𝐵 ) ∥ ( ! ‘ 𝐵 ) )
46	45	adantr	⊢ ( ( 𝐴 ∈ ( 1 ..^ 𝐵 ) ∧ 𝐵 ∈ ( 1 ..^ 𝑁 ) ) → ( 𝐴 · 𝐵 ) ∥ ( ! ‘ 𝐵 ) )
47		1eluzge0	⊢ 1 ∈ ( ℤ≥ ‘ 0 )
48		fzoss1	⊢ ( 1 ∈ ( ℤ≥ ‘ 0 ) → ( 1 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝑁 ) )
49	48	sseld	⊢ ( 1 ∈ ( ℤ≥ ‘ 0 ) → ( 𝐵 ∈ ( 1 ..^ 𝑁 ) → 𝐵 ∈ ( 0 ..^ 𝑁 ) ) )
50	47 49	ax-mp	⊢ ( 𝐵 ∈ ( 1 ..^ 𝑁 ) → 𝐵 ∈ ( 0 ..^ 𝑁 ) )
51		elfzoel2	⊢ ( 𝐵 ∈ ( 1 ..^ 𝑁 ) → 𝑁 ∈ ℤ )
52		fzoval	⊢ ( 𝑁 ∈ ℤ → ( 0 ..^ 𝑁 ) = ( 0 ... ( 𝑁 − 1 ) ) )
53	52	eleq2d	⊢ ( 𝑁 ∈ ℤ → ( 𝐵 ∈ ( 0 ..^ 𝑁 ) ↔ 𝐵 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )
54	51 53	syl	⊢ ( 𝐵 ∈ ( 1 ..^ 𝑁 ) → ( 𝐵 ∈ ( 0 ..^ 𝑁 ) ↔ 𝐵 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )
55	50 54	mpbid	⊢ ( 𝐵 ∈ ( 1 ..^ 𝑁 ) → 𝐵 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
56	55	adantl	⊢ ( ( 𝐴 ∈ ( 1 ..^ 𝐵 ) ∧ 𝐵 ∈ ( 1 ..^ 𝑁 ) ) → 𝐵 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
57		facnn0dvdsfac	⊢ ( 𝐵 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ! ‘ 𝐵 ) ∥ ( ! ‘ ( 𝑁 − 1 ) ) )
58	56 57	syl	⊢ ( ( 𝐴 ∈ ( 1 ..^ 𝐵 ) ∧ 𝐵 ∈ ( 1 ..^ 𝑁 ) ) → ( ! ‘ 𝐵 ) ∥ ( ! ‘ ( 𝑁 − 1 ) ) )
59	4 13 44 46 58	dvdstrd	⊢ ( ( 𝐴 ∈ ( 1 ..^ 𝐵 ) ∧ 𝐵 ∈ ( 1 ..^ 𝑁 ) ) → ( 𝐴 · 𝐵 ) ∥ ( ! ‘ ( 𝑁 − 1 ) ) )