prmodvdslcmf

Description: The primorial of a nonnegative integer divides the least common multiple of all positive integers less than or equal to the integer. (Contributed by AV, 19-Aug-2020) (Revised by AV, 29-Aug-2020)

		Ref	Expression
	Assertion	prmodvdslcmf	$⊢ N \in ℕ_{0} \to #_{p} (N) ∥ \underline{lcm} ((1 \dots N))$

Proof

Step	Hyp	Ref	Expression
1		prmoval	$⊢ N \in ℕ_{0} \to #_{p} (N) = \prod_{k = 1}^{N} if (k \in ℙ, k, 1)$
2		eqidd	$⊢ k \in (1 \dots N) \to (m \in ℕ ⟼ if (m \in ℙ, m, 1)) = (m \in ℕ ⟼ if (m \in ℙ, m, 1))$
3		simpr	$⊢ (k \in (1 \dots N) \land m = k) \to m = k$
4	3	eleq1d	$⊢ (k \in (1 \dots N) \land m = k) \to (m \in ℙ \leftrightarrow k \in ℙ)$
5	4 3	ifbieq1d	$⊢ (k \in (1 \dots N) \land m = k) \to if (m \in ℙ, m, 1) = if (k \in ℙ, k, 1)$
6		elfznn	$⊢ k \in (1 \dots N) \to k \in ℕ$
7		1nn	$⊢ 1 \in ℕ$
8	7	a1i	$⊢ k \in (1 \dots N) \to 1 \in ℕ$
9	6 8	ifcld	$⊢ k \in (1 \dots N) \to if (k \in ℙ, k, 1) \in ℕ$
10	2 5 6 9	fvmptd	$⊢ k \in (1 \dots N) \to (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k) = if (k \in ℙ, k, 1)$
11	10	eqcomd	$⊢ k \in (1 \dots N) \to if (k \in ℙ, k, 1) = (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k)$
12	11	prodeq2i	$⊢ \prod_{k = 1}^{N} if (k \in ℙ, k, 1) = \prod_{k = 1}^{N} (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k)$
13	1 12	eqtrdi	$⊢ N \in ℕ_{0} \to #_{p} (N) = \prod_{k = 1}^{N} (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k)$
14		fzfid	$⊢ N \in ℕ_{0} \to (1 \dots N) \in Fin$
15		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
16	14 15	jctil	$⊢ N \in ℕ_{0} \to ((1 \dots N) \subseteq ℕ \land (1 \dots N) \in Fin)$
17		fzssz	$⊢ (1 \dots N) \subseteq ℤ$
18	17	a1i	$⊢ N \in ℕ_{0} \to (1 \dots N) \subseteq ℤ$
19		0nelfz1	$⊢ 0 \notin (1 \dots N)$
20	19	a1i	$⊢ N \in ℕ_{0} \to 0 \notin (1 \dots N)$
21		lcmfn0cl	$⊢ ((1 \dots N) \subseteq ℤ \land (1 \dots N) \in Fin \land 0 \notin (1 \dots N)) \to \underline{lcm} ((1 \dots N)) \in ℕ$
22	18 14 20 21	syl3anc	$⊢ N \in ℕ_{0} \to \underline{lcm} ((1 \dots N)) \in ℕ$
23		id	$⊢ m \in ℕ \to m \in ℕ$
24	7	a1i	$⊢ m \in ℕ \to 1 \in ℕ$
25	23 24	ifcld	$⊢ m \in ℕ \to if (m \in ℙ, m, 1) \in ℕ$
26	25	adantl	$⊢ (N \in ℕ_{0} \land m \in ℕ) \to if (m \in ℙ, m, 1) \in ℕ$
27	26	fmpttd	$⊢ N \in ℕ_{0} \to (m \in ℕ ⟼ if (m \in ℙ, m, 1)) : ℕ ⟶ ℕ$
28		simpr	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N)) \to k \in (1 \dots N)$
29	28	adantr	$⊢ ((N \in ℕ_{0} \land k \in (1 \dots N)) \land x \in ((1 \dots N) ∖ \{k\})) \to k \in (1 \dots N)$
30		eldifi	$⊢ x \in ((1 \dots N) ∖ \{k\}) \to x \in (1 \dots N)$
31	30	adantl	$⊢ ((N \in ℕ_{0} \land k \in (1 \dots N)) \land x \in ((1 \dots N) ∖ \{k\})) \to x \in (1 \dots N)$
32		eldif	$⊢ x \in ((1 \dots N) ∖ \{k\}) \leftrightarrow (x \in (1 \dots N) \land \neg x \in \{k\})$
33		velsn	$⊢ x \in \{k\} \leftrightarrow x = k$
34	33	biimpri	$⊢ x = k \to x \in \{k\}$
35	34	equcoms	$⊢ k = x \to x \in \{k\}$
36	35	necon3bi	$⊢ \neg x \in \{k\} \to k \neq x$
37	32 36	simplbiim	$⊢ x \in ((1 \dots N) ∖ \{k\}) \to k \neq x$
38	37	adantl	$⊢ ((N \in ℕ_{0} \land k \in (1 \dots N)) \land x \in ((1 \dots N) ∖ \{k\})) \to k \neq x$
39		eqid	$⊢ (m \in ℕ ⟼ if (m \in ℙ, m, 1)) = (m \in ℕ ⟼ if (m \in ℙ, m, 1))$
40	39	fvprmselgcd1	$⊢ (k \in (1 \dots N) \land x \in (1 \dots N) \land k \neq x) \to (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k) \gcd (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (x) = 1$
41	29 31 38 40	syl3anc	$⊢ ((N \in ℕ_{0} \land k \in (1 \dots N)) \land x \in ((1 \dots N) ∖ \{k\})) \to (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k) \gcd (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (x) = 1$
42	41	ralrimiva	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N)) \to \forall x \in ((1 \dots N) ∖ \{k\}) (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k) \gcd (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (x) = 1$
43	42	ralrimiva	$⊢ N \in ℕ_{0} \to \forall k \in (1 \dots N) \forall x \in ((1 \dots N) ∖ \{k\}) (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k) \gcd (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (x) = 1$
44		eqidd	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N)) \to (m \in ℕ ⟼ if (m \in ℙ, m, 1)) = (m \in ℕ ⟼ if (m \in ℙ, m, 1))$
45		simpr	$⊢ ((N \in ℕ_{0} \land k \in (1 \dots N)) \land m = k) \to m = k$
46	45	eleq1d	$⊢ ((N \in ℕ_{0} \land k \in (1 \dots N)) \land m = k) \to (m \in ℙ \leftrightarrow k \in ℙ)$
47	46 45	ifbieq1d	$⊢ ((N \in ℕ_{0} \land k \in (1 \dots N)) \land m = k) \to if (m \in ℙ, m, 1) = if (k \in ℙ, k, 1)$
48	15 28	sselid	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N)) \to k \in ℕ$
49	17 28	sselid	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N)) \to k \in ℤ$
50		1zzd	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N)) \to 1 \in ℤ$
51	49 50	ifcld	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N)) \to if (k \in ℙ, k, 1) \in ℤ$
52	44 47 48 51	fvmptd	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N)) \to (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k) = if (k \in ℙ, k, 1)$
53		breq1	$⊢ x = if (k \in ℙ, k, 1) \to (x ∥ \underline{lcm} ((1 \dots N)) \leftrightarrow if (k \in ℙ, k, 1) ∥ \underline{lcm} ((1 \dots N)))$
54	16	adantr	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N)) \to ((1 \dots N) \subseteq ℕ \land (1 \dots N) \in Fin)$
55	17	2a1i	$⊢ (1 \dots N) \in Fin \to ((1 \dots N) \subseteq ℕ \to (1 \dots N) \subseteq ℤ)$
56	55	imdistanri	$⊢ ((1 \dots N) \subseteq ℕ \land (1 \dots N) \in Fin) \to ((1 \dots N) \subseteq ℤ \land (1 \dots N) \in Fin)$
57		dvdslcmf	$⊢ ((1 \dots N) \subseteq ℤ \land (1 \dots N) \in Fin) \to \forall x \in (1 \dots N) x ∥ \underline{lcm} ((1 \dots N))$
58	54 56 57	3syl	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N)) \to \forall x \in (1 \dots N) x ∥ \underline{lcm} ((1 \dots N))$
59		elfzuz2	$⊢ k \in (1 \dots N) \to N \in ℤ_{\geq 1}$
60	59	adantl	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N)) \to N \in ℤ_{\geq 1}$
61		eluzfz1	$⊢ N \in ℤ_{\geq 1} \to 1 \in (1 \dots N)$
62	60 61	syl	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N)) \to 1 \in (1 \dots N)$
63	28 62	ifcld	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N)) \to if (k \in ℙ, k, 1) \in (1 \dots N)$
64	53 58 63	rspcdva	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N)) \to if (k \in ℙ, k, 1) ∥ \underline{lcm} ((1 \dots N))$
65	52 64	eqbrtrd	$⊢ (N \in ℕ_{0} \land k \in (1 \dots N)) \to (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k) ∥ \underline{lcm} ((1 \dots N))$
66	65	ralrimiva	$⊢ N \in ℕ_{0} \to \forall k \in (1 \dots N) (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k) ∥ \underline{lcm} ((1 \dots N))$
67		coprmproddvds	$⊢ (((1 \dots N) \subseteq ℕ \land (1 \dots N) \in Fin) \land (\underline{lcm} ((1 \dots N)) \in ℕ \land (m \in ℕ ⟼ if (m \in ℙ, m, 1)) : ℕ ⟶ ℕ) \land (\forall k \in (1 \dots N) \forall x \in ((1 \dots N) ∖ \{k\}) (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k) \gcd (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (x) = 1 \land \forall k \in (1 \dots N) (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k) ∥ \underline{lcm} ((1 \dots N)))) \to \prod_{k = 1}^{N} (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k) ∥ \underline{lcm} ((1 \dots N))$
68	16 22 27 43 66 67	syl122anc	$⊢ N \in ℕ_{0} \to \prod_{k = 1}^{N} (m \in ℕ ⟼ if (m \in ℙ, m, 1)) (k) ∥ \underline{lcm} ((1 \dots N))$
69	13 68	eqbrtrd	$⊢ N \in ℕ_{0} \to #_{p} (N) ∥ \underline{lcm} ((1 \dots N))$

Metamath Proof Explorer

Theorem prmodvdslcmf

Proof