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	$⊢ (A \in (1 ..^B) \land B \in (1 ..^N)) \to A B ∥ (N - 1)!$

Proof

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

Metamath Proof Explorer

Theorem muldvdsfacm1

Proof