prmdvdsprmo

Description: The primorial of a number is divisible by each prime less then or equal to the number. (Contributed by AV, 15-Aug-2020) (Revised by AV, 28-Aug-2020)

		Ref	Expression
	Assertion	prmdvdsprmo	$⊢ N \in ℕ \to \forall p \in ℙ (p \leq N \to p ∥ #_{p} (N))$

Proof

Step	Hyp	Ref	Expression
1		fzfi	$⊢ (1 \dots N) \in Fin$
2		diffi	$⊢ (1 \dots N) \in Fin \to (1 \dots N) ∖ \{p\} \in Fin$
3	1 2	mp1i	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq N) \to (1 \dots N) ∖ \{p\} \in Fin$
4		eldifi	$⊢ k \in ((1 \dots N) ∖ \{p\}) \to k \in (1 \dots N)$
5		elfzelz	$⊢ k \in (1 \dots N) \to k \in ℤ$
6	4 5	syl	$⊢ k \in ((1 \dots N) ∖ \{p\}) \to k \in ℤ$
7		1zzd	$⊢ k \in ((1 \dots N) ∖ \{p\}) \to 1 \in ℤ$
8	6 7	ifcld	$⊢ k \in ((1 \dots N) ∖ \{p\}) \to if (k \in ℙ, k, 1) \in ℤ$
9	8	adantl	$⊢ (((N \in ℕ \land p \in ℙ) \land p \leq N) \land k \in ((1 \dots N) ∖ \{p\})) \to if (k \in ℙ, k, 1) \in ℤ$
10	3 9	fprodzcl	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq N) \to \prod_{k \in (1 \dots N) ∖ \{p\}} if (k \in ℙ, k, 1) \in ℤ$
11		prmz	$⊢ p \in ℙ \to p \in ℤ$
12	11	adantl	$⊢ (N \in ℕ \land p \in ℙ) \to p \in ℤ$
13	12	adantr	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq N) \to p \in ℤ$
14		dvdsmul2	$⊢ (\prod_{k \in (1 \dots N) ∖ \{p\}} if (k \in ℙ, k, 1) \in ℤ \land p \in ℤ) \to p ∥ \prod_{k \in (1 \dots N) ∖ \{p\}} if (k \in ℙ, k, 1) p$
15	10 13 14	syl2anc	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq N) \to p ∥ \prod_{k \in (1 \dots N) ∖ \{p\}} if (k \in ℙ, k, 1) p$
16		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
17		prmoval	$⊢ N \in ℕ_{0} \to #_{p} (N) = \prod_{k = 1}^{N} if (k \in ℙ, k, 1)$
18	16 17	syl	$⊢ N \in ℕ \to #_{p} (N) = \prod_{k = 1}^{N} if (k \in ℙ, k, 1)$
19	18	ad2antrr	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq N) \to #_{p} (N) = \prod_{k = 1}^{N} if (k \in ℙ, k, 1)$
20	19	breq2d	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq N) \to (p ∥ #_{p} (N) \leftrightarrow p ∥ \prod_{k = 1}^{N} if (k \in ℙ, k, 1))$
21		neldifsnd	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq N) \to \neg p \in ((1 \dots N) ∖ \{p\})$
22		disjsn	$⊢ ((1 \dots N) ∖ \{p\}) \cap \{p\} = \emptyset \leftrightarrow \neg p \in ((1 \dots N) ∖ \{p\})$
23	21 22	sylibr	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq N) \to ((1 \dots N) ∖ \{p\}) \cap \{p\} = \emptyset$
24		prmnn	$⊢ p \in ℙ \to p \in ℕ$
25	24	adantl	$⊢ (N \in ℕ \land p \in ℙ) \to p \in ℕ$
26	25	anim1i	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq N) \to (p \in ℕ \land p \leq N)$
27		nnz	$⊢ N \in ℕ \to N \in ℤ$
28		fznn	$⊢ N \in ℤ \to (p \in (1 \dots N) \leftrightarrow (p \in ℕ \land p \leq N))$
29	27 28	syl	$⊢ N \in ℕ \to (p \in (1 \dots N) \leftrightarrow (p \in ℕ \land p \leq N))$
30	29	ad2antrr	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq N) \to (p \in (1 \dots N) \leftrightarrow (p \in ℕ \land p \leq N))$
31	26 30	mpbird	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq N) \to p \in (1 \dots N)$
32		difsnid	$⊢ p \in (1 \dots N) \to ((1 \dots N) ∖ \{p\}) \cup \{p\} = (1 \dots N)$
33	32	eqcomd	$⊢ p \in (1 \dots N) \to (1 \dots N) = ((1 \dots N) ∖ \{p\}) \cup \{p\}$
34	31 33	syl	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq N) \to (1 \dots N) = ((1 \dots N) ∖ \{p\}) \cup \{p\}$
35		fzfid	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq N) \to (1 \dots N) \in Fin$
36		1zzd	$⊢ k \in (1 \dots N) \to 1 \in ℤ$
37	5 36	ifcld	$⊢ k \in (1 \dots N) \to if (k \in ℙ, k, 1) \in ℤ$
38	37	zcnd	$⊢ k \in (1 \dots N) \to if (k \in ℙ, k, 1) \in ℂ$
39	38	adantl	$⊢ (((N \in ℕ \land p \in ℙ) \land p \leq N) \land k \in (1 \dots N)) \to if (k \in ℙ, k, 1) \in ℂ$
40	23 34 35 39	fprodsplit	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq N) \to \prod_{k = 1}^{N} if (k \in ℙ, k, 1) = \prod_{k \in (1 \dots N) ∖ \{p\}} if (k \in ℙ, k, 1) \prod_{k \in \{p\}} if (k \in ℙ, k, 1)$
41		simplr	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq N) \to p \in ℙ$
42	25	adantr	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq N) \to p \in ℕ$
43	42	nncnd	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq N) \to p \in ℂ$
44		1cnd	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq N) \to 1 \in ℂ$
45	43 44	ifcld	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq N) \to if (p \in ℙ, p, 1) \in ℂ$
46		eleq1w	$⊢ k = p \to (k \in ℙ \leftrightarrow p \in ℙ)$
47		id	$⊢ k = p \to k = p$
48	46 47	ifbieq1d	$⊢ k = p \to if (k \in ℙ, k, 1) = if (p \in ℙ, p, 1)$
49	48	prodsn	$⊢ (p \in ℙ \land if (p \in ℙ, p, 1) \in ℂ) \to \prod_{k \in \{p\}} if (k \in ℙ, k, 1) = if (p \in ℙ, p, 1)$
50	41 45 49	syl2anc	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq N) \to \prod_{k \in \{p\}} if (k \in ℙ, k, 1) = if (p \in ℙ, p, 1)$
51		simpr	$⊢ (N \in ℕ \land p \in ℙ) \to p \in ℙ$
52	51	iftrued	$⊢ (N \in ℕ \land p \in ℙ) \to if (p \in ℙ, p, 1) = p$
53	52	adantr	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq N) \to if (p \in ℙ, p, 1) = p$
54	50 53	eqtrd	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq N) \to \prod_{k \in \{p\}} if (k \in ℙ, k, 1) = p$
55	54	oveq2d	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq N) \to \prod_{k \in (1 \dots N) ∖ \{p\}} if (k \in ℙ, k, 1) \prod_{k \in \{p\}} if (k \in ℙ, k, 1) = \prod_{k \in (1 \dots N) ∖ \{p\}} if (k \in ℙ, k, 1) p$
56	40 55	eqtrd	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq N) \to \prod_{k = 1}^{N} if (k \in ℙ, k, 1) = \prod_{k \in (1 \dots N) ∖ \{p\}} if (k \in ℙ, k, 1) p$
57	56	breq2d	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq N) \to (p ∥ \prod_{k = 1}^{N} if (k \in ℙ, k, 1) \leftrightarrow p ∥ \prod_{k \in (1 \dots N) ∖ \{p\}} if (k \in ℙ, k, 1) p)$
58	20 57	bitrd	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq N) \to (p ∥ #_{p} (N) \leftrightarrow p ∥ \prod_{k \in (1 \dots N) ∖ \{p\}} if (k \in ℙ, k, 1) p)$
59	15 58	mpbird	$⊢ ((N \in ℕ \land p \in ℙ) \land p \leq N) \to p ∥ #_{p} (N)$
60	59	ex	$⊢ (N \in ℕ \land p \in ℙ) \to (p \leq N \to p ∥ #_{p} (N))$
61	60	ralrimiva	$⊢ N \in ℕ \to \forall p \in ℙ (p \leq N \to p ∥ #_{p} (N))$

Metamath Proof Explorer

Theorem prmdvdsprmo

Proof