lcmineqlem6

Description: Part of lcm inequality lemma, this part eventually shows that F times the least common multiple of 1 to n is an integer. (Contributed by metakunt, 10-May-2024)

	Ref	Expression
Hypotheses	lcmineqlem6.1	$⊢ F = \int_{[0, 1]} x^{M - 1} {(1 - x)}^{N - M} d x$
	lcmineqlem6.2	$⊢ φ \to N \in ℕ$
	lcmineqlem6.3	$⊢ φ \to M \in ℕ$
	lcmineqlem6.4	$⊢ φ \to M \leq N$
Assertion	lcmineqlem6	$⊢ φ \to \underline{lcm} ((1 \dots N)) F \in ℤ$

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem6.1	$⊢ F = \int_{[0, 1]} x^{M - 1} {(1 - x)}^{N - M} d x$
2		lcmineqlem6.2	$⊢ φ \to N \in ℕ$
3		lcmineqlem6.3	$⊢ φ \to M \in ℕ$
4		lcmineqlem6.4	$⊢ φ \to M \leq N$
5	1 2 3 4	lcmineqlem3	$⊢ φ \to F = \sum_{k = 0}^{N - M} {(- 1)}^{k} (\binom{N - M}{k}) (\frac{1}{M + k})$
6	5	oveq2d	$⊢ φ \to \underline{lcm} ((1 \dots N)) F = \underline{lcm} ((1 \dots N)) \sum_{k = 0}^{N - M} {(- 1)}^{k} (\binom{N - M}{k}) (\frac{1}{M + k})$
7		fzfid	$⊢ φ \to (0 \dots N - M) \in Fin$
8		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
9		fzfi	$⊢ (1 \dots N) \in Fin$
10	8 9	pm3.2i	$⊢ ((1 \dots N) \subseteq ℕ \land (1 \dots N) \in Fin)$
11		lcmfnncl	$⊢ ((1 \dots N) \subseteq ℕ \land (1 \dots N) \in Fin) \to \underline{lcm} ((1 \dots N)) \in ℕ$
12	10 11	ax-mp	$⊢ \underline{lcm} ((1 \dots N)) \in ℕ$
13	12	nncni	$⊢ \underline{lcm} ((1 \dots N)) \in ℂ$
14	13	a1i	$⊢ φ \to \underline{lcm} ((1 \dots N)) \in ℂ$
15		elfzelz	$⊢ k \in (0 \dots N - M) \to k \in ℤ$
16		m1expcl	$⊢ k \in ℤ \to {(- 1)}^{k} \in ℤ$
17	15 16	syl	$⊢ k \in (0 \dots N - M) \to {(- 1)}^{k} \in ℤ$
18	17	zcnd	$⊢ k \in (0 \dots N - M) \to {(- 1)}^{k} \in ℂ$
19	18	adantl	$⊢ (φ \land k \in (0 \dots N - M)) \to {(- 1)}^{k} \in ℂ$
20		bccl2	$⊢ k \in (0 \dots N - M) \to (\binom{N - M}{k}) \in ℕ$
21	20	nncnd	$⊢ k \in (0 \dots N - M) \to (\binom{N - M}{k}) \in ℂ$
22	21	adantl	$⊢ (φ \land k \in (0 \dots N - M)) \to (\binom{N - M}{k}) \in ℂ$
23	19 22	mulcld	$⊢ (φ \land k \in (0 \dots N - M)) \to {(- 1)}^{k} (\binom{N - M}{k}) \in ℂ$
24	3	nncnd	$⊢ φ \to M \in ℂ$
25	24	adantr	$⊢ (φ \land k \in (0 \dots N - M)) \to M \in ℂ$
26	15	zcnd	$⊢ k \in (0 \dots N - M) \to k \in ℂ$
27	26	adantl	$⊢ (φ \land k \in (0 \dots N - M)) \to k \in ℂ$
28	25 27	addcld	$⊢ (φ \land k \in (0 \dots N - M)) \to M + k \in ℂ$
29		elfznn0	$⊢ k \in (0 \dots N - M) \to k \in ℕ_{0}$
30		nnnn0addcl	$⊢ (M \in ℕ \land k \in ℕ_{0}) \to M + k \in ℕ$
31	29 30	sylan2	$⊢ (M \in ℕ \land k \in (0 \dots N - M)) \to M + k \in ℕ$
32	3 31	sylan	$⊢ (φ \land k \in (0 \dots N - M)) \to M + k \in ℕ$
33	32	nnne0d	$⊢ (φ \land k \in (0 \dots N - M)) \to M + k \neq 0$
34	28 33	reccld	$⊢ (φ \land k \in (0 \dots N - M)) \to \frac{1}{M + k} \in ℂ$
35	23 34	mulcld	$⊢ (φ \land k \in (0 \dots N - M)) \to {(- 1)}^{k} (\binom{N - M}{k}) (\frac{1}{M + k}) \in ℂ$
36	7 14 35	fsummulc2	$⊢ φ \to \underline{lcm} ((1 \dots N)) \sum_{k = 0}^{N - M} {(- 1)}^{k} (\binom{N - M}{k}) (\frac{1}{M + k}) = \sum_{k = 0}^{N - M} \underline{lcm} ((1 \dots N)) {(- 1)}^{k} (\binom{N - M}{k}) (\frac{1}{M + k})$
37	6 36	eqtrd	$⊢ φ \to \underline{lcm} ((1 \dots N)) F = \sum_{k = 0}^{N - M} \underline{lcm} ((1 \dots N)) {(- 1)}^{k} (\binom{N - M}{k}) (\frac{1}{M + k})$
38	13	a1i	$⊢ (φ \land k \in (0 \dots N - M)) \to \underline{lcm} ((1 \dots N)) \in ℂ$
39	38 23 28 33	lcmineqlem5	$⊢ (φ \land k \in (0 \dots N - M)) \to \underline{lcm} ((1 \dots N)) {(- 1)}^{k} (\binom{N - M}{k}) (\frac{1}{M + k}) = {(- 1)}^{k} (\binom{N - M}{k}) (\frac{\underline{lcm} ((1 \dots N))}{M + k})$
40	39	sumeq2dv	$⊢ φ \to \sum_{k = 0}^{N - M} \underline{lcm} ((1 \dots N)) {(- 1)}^{k} (\binom{N - M}{k}) (\frac{1}{M + k}) = \sum_{k = 0}^{N - M} {(- 1)}^{k} (\binom{N - M}{k}) (\frac{\underline{lcm} ((1 \dots N))}{M + k})$
41	37 40	eqtrd	$⊢ φ \to \underline{lcm} ((1 \dots N)) F = \sum_{k = 0}^{N - M} {(- 1)}^{k} (\binom{N - M}{k}) (\frac{\underline{lcm} ((1 \dots N))}{M + k})$
42	17	adantl	$⊢ (φ \land k \in (0 \dots N - M)) \to {(- 1)}^{k} \in ℤ$
43	20	nnzd	$⊢ k \in (0 \dots N - M) \to (\binom{N - M}{k}) \in ℤ$
44	43	adantl	$⊢ (φ \land k \in (0 \dots N - M)) \to (\binom{N - M}{k}) \in ℤ$
45	42 44	zmulcld	$⊢ (φ \land k \in (0 \dots N - M)) \to {(- 1)}^{k} (\binom{N - M}{k}) \in ℤ$
46	2	adantr	$⊢ (φ \land k \in (0 \dots N - M)) \to N \in ℕ$
47	3	adantr	$⊢ (φ \land k \in (0 \dots N - M)) \to M \in ℕ$
48	4	adantr	$⊢ (φ \land k \in (0 \dots N - M)) \to M \leq N$
49		simpr	$⊢ (φ \land k \in (0 \dots N - M)) \to k \in (0 \dots N - M)$
50	46 47 48 49	lcmineqlem4	$⊢ (φ \land k \in (0 \dots N - M)) \to \frac{\underline{lcm} ((1 \dots N))}{M + k} \in ℤ$
51	45 50	zmulcld	$⊢ (φ \land k \in (0 \dots N - M)) \to {(- 1)}^{k} (\binom{N - M}{k}) (\frac{\underline{lcm} ((1 \dots N))}{M + k}) \in ℤ$
52	7 51	fsumzcl	$⊢ φ \to \sum_{k = 0}^{N - M} {(- 1)}^{k} (\binom{N - M}{k}) (\frac{\underline{lcm} ((1 \dots N))}{M + k}) \in ℤ$
53	41 52	eqeltrd	$⊢ φ \to \underline{lcm} ((1 \dots N)) F \in ℤ$

Metamath Proof Explorer

Theorem lcmineqlem6

Proof