Theorem prmdvdsbc

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

	Ref	Expression
Assertion	prmdvdsbc	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑃 ∥ ( 𝑃 C 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( ( ! ‘ 𝑃 ) / ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ) = ( ( ! ‘ 𝑃 ) / ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) )
2		simpl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑃 ∈ ℙ )
3		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
4	3	nnzd	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
5		1nn0	⊢ 1 ∈ ℕ0
6		eluzmn	⊢ ( ( 𝑃 ∈ ℤ ∧ 1 ∈ ℕ0 ) → 𝑃 ∈ ( ℤ≥ ‘ ( 𝑃 − 1 ) ) )
7	4 5 6	sylancl	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ ( 𝑃 − 1 ) ) )
8		fzss2	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ ( 𝑃 − 1 ) ) → ( 1 ... ( 𝑃 − 1 ) ) ⊆ ( 1 ... 𝑃 ) )
9	7 8	syl	⊢ ( 𝑃 ∈ ℙ → ( 1 ... ( 𝑃 − 1 ) ) ⊆ ( 1 ... 𝑃 ) )
10		fz1ssfz0	⊢ ( 1 ... 𝑃 ) ⊆ ( 0 ... 𝑃 )
11	9 10	sstrdi	⊢ ( 𝑃 ∈ ℙ → ( 1 ... ( 𝑃 − 1 ) ) ⊆ ( 0 ... 𝑃 ) )
12	11	sselda	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑁 ∈ ( 0 ... 𝑃 ) )
13		bcval2	⊢ ( 𝑁 ∈ ( 0 ... 𝑃 ) → ( 𝑃 C 𝑁 ) = ( ( ! ‘ 𝑃 ) / ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ) )
14	12 13	syl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( 𝑃 C 𝑁 ) = ( ( ! ‘ 𝑃 ) / ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ) )
15	3	nnnn0d	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ0 )
16	15	adantr	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑃 ∈ ℕ0 )
17		elfzelz	⊢ ( 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) → 𝑁 ∈ ℤ )
18	17	adantl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑁 ∈ ℤ )
19		bccl	⊢ ( ( 𝑃 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) → ( 𝑃 C 𝑁 ) ∈ ℕ0 )
20	16 18 19	syl2anc	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( 𝑃 C 𝑁 ) ∈ ℕ0 )
21	20	nn0zd	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( 𝑃 C 𝑁 ) ∈ ℤ )
22	14 21	eqeltrrd	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ( ! ‘ 𝑃 ) / ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ) ∈ ℤ )
23		elfznn	⊢ ( 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) → 𝑁 ∈ ℕ )
24	23	adantl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑁 ∈ ℕ )
25	24	nnnn0d	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑁 ∈ ℕ0 )
26		1zzd	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 1 ∈ ℤ )
27	4	adantr	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑃 ∈ ℤ )
28		simpr	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) )
29		elfzm11	⊢ ( ( 1 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ↔ ( 𝑁 ∈ ℤ ∧ 1 ≤ 𝑁 ∧ 𝑁 < 𝑃 ) ) )
30	29	biimpa	⊢ ( ( ( 1 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( 𝑁 ∈ ℤ ∧ 1 ≤ 𝑁 ∧ 𝑁 < 𝑃 ) )
31	30	simp3d	⊢ ( ( ( 1 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑁 < 𝑃 )
32	26 27 28 31	syl21anc	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑁 < 𝑃 )
33		ltsubnn0	⊢ ( ( 𝑃 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 < 𝑃 → ( 𝑃 − 𝑁 ) ∈ ℕ0 ) )
34	33	imp	⊢ ( ( ( 𝑃 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑁 < 𝑃 ) → ( 𝑃 − 𝑁 ) ∈ ℕ0 )
35	16 25 32 34	syl21anc	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( 𝑃 − 𝑁 ) ∈ ℕ0 )
36	35	faccld	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ! ‘ ( 𝑃 − 𝑁 ) ) ∈ ℕ )
37	36	nnzd	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ! ‘ ( 𝑃 − 𝑁 ) ) ∈ ℤ )
38	25	faccld	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ! ‘ 𝑁 ) ∈ ℕ )
39	38	nnzd	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ! ‘ 𝑁 ) ∈ ℤ )
40	37 39	zmulcld	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ∈ ℤ )
41	37	zcnd	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ! ‘ ( 𝑃 − 𝑁 ) ) ∈ ℂ )
42	39	zcnd	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ! ‘ 𝑁 ) ∈ ℂ )
43		facne0	⊢ ( ( 𝑃 − 𝑁 ) ∈ ℕ0 → ( ! ‘ ( 𝑃 − 𝑁 ) ) ≠ 0 )
44	35 43	syl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ! ‘ ( 𝑃 − 𝑁 ) ) ≠ 0 )
45		facne0	⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ≠ 0 )
46	25 45	syl	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ! ‘ 𝑁 ) ≠ 0 )
47	41 42 44 46	mulne0d	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ≠ 0 )
48		uzid	⊢ ( 𝑃 ∈ ℤ → 𝑃 ∈ ( ℤ≥ ‘ 𝑃 ) )
49	4 48	syl	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 𝑃 ) )
50		dvdsfac	⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 𝑃 ) ) → 𝑃 ∥ ( ! ‘ 𝑃 ) )
51	3 49 50	syl2anc	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∥ ( ! ‘ 𝑃 ) )
52	51	adantr	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑃 ∥ ( ! ‘ 𝑃 ) )
53	16	nn0red	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑃 ∈ ℝ )
54	24	nnrpd	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑁 ∈ ℝ+ )
55	53 54	ltsubrpd	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( 𝑃 − 𝑁 ) < 𝑃 )
56		prmndvdsfaclt	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 − 𝑁 ) ∈ ℕ0 ) → ( ( 𝑃 − 𝑁 ) < 𝑃 → ¬ 𝑃 ∥ ( ! ‘ ( 𝑃 − 𝑁 ) ) ) )
57	56	imp	⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 − 𝑁 ) ∈ ℕ0 ) ∧ ( 𝑃 − 𝑁 ) < 𝑃 ) → ¬ 𝑃 ∥ ( ! ‘ ( 𝑃 − 𝑁 ) ) )
58	2 35 55 57	syl21anc	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ¬ 𝑃 ∥ ( ! ‘ ( 𝑃 − 𝑁 ) ) )
59		prmndvdsfaclt	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 < 𝑃 → ¬ 𝑃 ∥ ( ! ‘ 𝑁 ) ) )
60	59	imp	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑁 < 𝑃 ) → ¬ 𝑃 ∥ ( ! ‘ 𝑁 ) )
61	2 25 32 60	syl21anc	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ¬ 𝑃 ∥ ( ! ‘ 𝑁 ) )
62		ioran	⊢ ( ¬ ( 𝑃 ∥ ( ! ‘ ( 𝑃 − 𝑁 ) ) ∨ 𝑃 ∥ ( ! ‘ 𝑁 ) ) ↔ ( ¬ 𝑃 ∥ ( ! ‘ ( 𝑃 − 𝑁 ) ) ∧ ¬ 𝑃 ∥ ( ! ‘ 𝑁 ) ) )
63		euclemma	⊢ ( ( 𝑃 ∈ ℙ ∧ ( ! ‘ ( 𝑃 − 𝑁 ) ) ∈ ℤ ∧ ( ! ‘ 𝑁 ) ∈ ℤ ) → ( 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ↔ ( 𝑃 ∥ ( ! ‘ ( 𝑃 − 𝑁 ) ) ∨ 𝑃 ∥ ( ! ‘ 𝑁 ) ) ) )
64	63	biimpd	⊢ ( ( 𝑃 ∈ ℙ ∧ ( ! ‘ ( 𝑃 − 𝑁 ) ) ∈ ℤ ∧ ( ! ‘ 𝑁 ) ∈ ℤ ) → ( 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) → ( 𝑃 ∥ ( ! ‘ ( 𝑃 − 𝑁 ) ) ∨ 𝑃 ∥ ( ! ‘ 𝑁 ) ) ) )
65	64	con3d	⊢ ( ( 𝑃 ∈ ℙ ∧ ( ! ‘ ( 𝑃 − 𝑁 ) ) ∈ ℤ ∧ ( ! ‘ 𝑁 ) ∈ ℤ ) → ( ¬ ( 𝑃 ∥ ( ! ‘ ( 𝑃 − 𝑁 ) ) ∨ 𝑃 ∥ ( ! ‘ 𝑁 ) ) → ¬ 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ) )
66	62 65	biimtrrid	⊢ ( ( 𝑃 ∈ ℙ ∧ ( ! ‘ ( 𝑃 − 𝑁 ) ) ∈ ℤ ∧ ( ! ‘ 𝑁 ) ∈ ℤ ) → ( ( ¬ 𝑃 ∥ ( ! ‘ ( 𝑃 − 𝑁 ) ) ∧ ¬ 𝑃 ∥ ( ! ‘ 𝑁 ) ) → ¬ 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ) )
67	66	imp	⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( ! ‘ ( 𝑃 − 𝑁 ) ) ∈ ℤ ∧ ( ! ‘ 𝑁 ) ∈ ℤ ) ∧ ( ¬ 𝑃 ∥ ( ! ‘ ( 𝑃 − 𝑁 ) ) ∧ ¬ 𝑃 ∥ ( ! ‘ 𝑁 ) ) ) → ¬ 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) )
68	2 37 39 58 61 67	syl32anc	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ¬ 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) )
69	1 2 22 40 47 52 68	dvdszzq	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑃 ∥ ( ( ! ‘ 𝑃 ) / ( ( ! ‘ ( 𝑃 − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ) )
70	69 14	breqtrrd	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑃 ∥ ( 𝑃 C 𝑁 ) )