prmdvdsbc

Description: Condition for a prime number to divide a binomial coefficient. (Contributed by Thierry Arnoux, 17-Sep-2023)

		Ref	Expression
	Assertion	prmdvdsbc	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to P ∥ (\binom{P}{N})$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ \frac{P!}{(P - N)! N!} = \frac{P!}{(P - N)! N!}$
2		simpl	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to P \in ℙ$
3		prmnn	$⊢ P \in ℙ \to P \in ℕ$
4	3	nnzd	$⊢ P \in ℙ \to P \in ℤ$
5		1nn0	$⊢ 1 \in ℕ_{0}$
6		eluzmn	$⊢ (P \in ℤ \land 1 \in ℕ_{0}) \to P \in ℤ_{\geq (P - 1)}$
7	4 5 6	sylancl	$⊢ P \in ℙ \to P \in ℤ_{\geq (P - 1)}$
8		fzss2	$⊢ P \in ℤ_{\geq (P - 1)} \to (1 \dots P - 1) \subseteq (1 \dots P)$
9	7 8	syl	$⊢ P \in ℙ \to (1 \dots P - 1) \subseteq (1 \dots P)$
10		fz1ssfz0	$⊢ (1 \dots P) \subseteq (0 \dots P)$
11	9 10	sstrdi	$⊢ P \in ℙ \to (1 \dots P - 1) \subseteq (0 \dots P)$
12	11	sselda	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N \in (0 \dots P)$
13		bcval2	$⊢ N \in (0 \dots P) \to (\binom{P}{N}) = \frac{P!}{(P - N)! N!}$
14	12 13	syl	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (\binom{P}{N}) = \frac{P!}{(P - N)! N!}$
15	3	nnnn0d	$⊢ P \in ℙ \to P \in ℕ_{0}$
16	15	adantr	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to P \in ℕ_{0}$
17		elfzelz	$⊢ N \in (1 \dots P - 1) \to N \in ℤ$
18	17	adantl	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N \in ℤ$
19		bccl	$⊢ (P \in ℕ_{0} \land N \in ℤ) \to (\binom{P}{N}) \in ℕ_{0}$
20	16 18 19	syl2anc	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (\binom{P}{N}) \in ℕ_{0}$
21	20	nn0zd	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (\binom{P}{N}) \in ℤ$
22	14 21	eqeltrrd	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to \frac{P!}{(P - N)! N!} \in ℤ$
23		elfznn	$⊢ N \in (1 \dots P - 1) \to N \in ℕ$
24	23	adantl	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N \in ℕ$
25	24	nnnn0d	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N \in ℕ_{0}$
26		1zzd	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to 1 \in ℤ$
27	4	adantr	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to P \in ℤ$
28		simpr	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N \in (1 \dots P - 1)$
29		elfzm11	$⊢ (1 \in ℤ \land P \in ℤ) \to (N \in (1 \dots P - 1) \leftrightarrow (N \in ℤ \land 1 \leq N \land N < P))$
30	29	biimpa	$⊢ ((1 \in ℤ \land P \in ℤ) \land N \in (1 \dots P - 1)) \to (N \in ℤ \land 1 \leq N \land N < P)$
31	30	simp3d	$⊢ ((1 \in ℤ \land P \in ℤ) \land N \in (1 \dots P - 1)) \to N < P$
32	26 27 28 31	syl21anc	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N < P$
33		ltsubnn0	$⊢ (P \in ℕ_{0} \land N \in ℕ_{0}) \to (N < P \to P - N \in ℕ_{0})$
34	33	imp	$⊢ ((P \in ℕ_{0} \land N \in ℕ_{0}) \land N < P) \to P - N \in ℕ_{0}$
35	16 25 32 34	syl21anc	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to P - N \in ℕ_{0}$
36	35	faccld	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (P - N)! \in ℕ$
37	36	nnzd	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (P - N)! \in ℤ$
38	25	faccld	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N! \in ℕ$
39	38	nnzd	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N! \in ℤ$
40	37 39	zmulcld	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (P - N)! N! \in ℤ$
41	37	zcnd	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (P - N)! \in ℂ$
42	39	zcnd	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N! \in ℂ$
43		facne0	$⊢ P - N \in ℕ_{0} \to (P - N)! \neq 0$
44	35 43	syl	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (P - N)! \neq 0$
45		facne0	$⊢ N \in ℕ_{0} \to N! \neq 0$
46	25 45	syl	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N! \neq 0$
47	41 42 44 46	mulne0d	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to (P - N)! N! \neq 0$
48		uzid	$⊢ P \in ℤ \to P \in ℤ_{\geq P}$
49	4 48	syl	$⊢ P \in ℙ \to P \in ℤ_{\geq P}$
50		dvdsfac	$⊢ (P \in ℕ \land P \in ℤ_{\geq P}) \to P ∥ P!$
51	3 49 50	syl2anc	$⊢ P \in ℙ \to P ∥ P!$
52	51	adantr	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to P ∥ P!$
53	16	nn0red	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to P \in ℝ$
54	24	nnrpd	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to N \in ℝ^{+}$
55	53 54	ltsubrpd	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to P - N < P$
56		prmndvdsfaclt	$⊢ (P \in ℙ \land P - N \in ℕ_{0}) \to (P - N < P \to \neg P ∥ (P - N)!)$
57	56	imp	$⊢ ((P \in ℙ \land P - N \in ℕ_{0}) \land P - N < P) \to \neg P ∥ (P - N)!$
58	2 35 55 57	syl21anc	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to \neg P ∥ (P - N)!$
59		prmndvdsfaclt	$⊢ (P \in ℙ \land N \in ℕ_{0}) \to (N < P \to \neg P ∥ N!)$
60	59	imp	$⊢ ((P \in ℙ \land N \in ℕ_{0}) \land N < P) \to \neg P ∥ N!$
61	2 25 32 60	syl21anc	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to \neg P ∥ N!$
62		ioran	$⊢ \neg (P ∥ (P - N)! \lor P ∥ N!) \leftrightarrow (\neg P ∥ (P - N)! \land \neg P ∥ N!)$
63		euclemma	$⊢ (P \in ℙ \land (P - N)! \in ℤ \land N! \in ℤ) \to (P ∥ (P - N)! N! \leftrightarrow (P ∥ (P - N)! \lor P ∥ N!))$
64	63	biimpd	$⊢ (P \in ℙ \land (P - N)! \in ℤ \land N! \in ℤ) \to (P ∥ (P - N)! N! \to (P ∥ (P - N)! \lor P ∥ N!))$
65	64	con3d	$⊢ (P \in ℙ \land (P - N)! \in ℤ \land N! \in ℤ) \to (\neg (P ∥ (P - N)! \lor P ∥ N!) \to \neg P ∥ (P - N)! N!)$
66	62 65	syl5bir	$⊢ (P \in ℙ \land (P - N)! \in ℤ \land N! \in ℤ) \to ((\neg P ∥ (P - N)! \land \neg P ∥ N!) \to \neg P ∥ (P - N)! N!)$
67	66	imp	$⊢ ((P \in ℙ \land (P - N)! \in ℤ \land N! \in ℤ) \land (\neg P ∥ (P - N)! \land \neg P ∥ N!)) \to \neg P ∥ (P - N)! N!$
68	2 37 39 58 61 67	syl32anc	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to \neg P ∥ (P - N)! N!$
69	1 2 22 40 47 52 68	dvdszzq	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to P ∥ (\frac{P!}{(P - N)! N!})$
70	69 14	breqtrrd	$⊢ (P \in ℙ \land N \in (1 \dots P - 1)) \to P ∥ (\binom{P}{N})$

Metamath Proof Explorer

Theorem prmdvdsbc

Proof