lcmineqlem3

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, 30-Apr-2024)

	Ref	Expression
Hypotheses	lcmineqlem3.1	$⊢ F = \int_{[0, 1]} x^{M - 1} {(1 - x)}^{N - M} d x$
	lcmineqlem3.2	$⊢ φ \to N \in ℕ$
	lcmineqlem3.3	$⊢ φ \to M \in ℕ$
	lcmineqlem3.4	$⊢ φ \to M \leq N$
Assertion	lcmineqlem3	$⊢ φ \to F = \sum_{k = 0}^{N - M} {(- 1)}^{k} (\binom{N - M}{k}) (\frac{1}{M + k})$

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem3.1	$⊢ F = \int_{[0, 1]} x^{M - 1} {(1 - x)}^{N - M} d x$
2		lcmineqlem3.2	$⊢ φ \to N \in ℕ$
3		lcmineqlem3.3	$⊢ φ \to M \in ℕ$
4		lcmineqlem3.4	$⊢ φ \to M \leq N$
5	1 2 3 4	lcmineqlem2	$⊢ φ \to F = \sum_{k = 0}^{N - M} {(- 1)}^{k} (\binom{N - M}{k}) \int_{[0, 1]} x^{M - 1} x^{k} d x$
6		elunitcn	$⊢ x \in [0, 1] \to x \in ℂ$
7	6	3ad2ant3	$⊢ (φ \land k \in (0 \dots N - M) \land x \in [0, 1]) \to x \in ℂ$
8		elfznn0	$⊢ k \in (0 \dots N - M) \to k \in ℕ_{0}$
9	8	3ad2ant2	$⊢ (φ \land k \in (0 \dots N - M) \land x \in [0, 1]) \to k \in ℕ_{0}$
10		nnm1nn0	$⊢ M \in ℕ \to M - 1 \in ℕ_{0}$
11	3 10	syl	$⊢ φ \to M - 1 \in ℕ_{0}$
12	11	3ad2ant1	$⊢ (φ \land k \in (0 \dots N - M) \land x \in [0, 1]) \to M - 1 \in ℕ_{0}$
13	7 9 12	expaddd	$⊢ (φ \land k \in (0 \dots N - M) \land x \in [0, 1]) \to x^{M - 1 + k} = x^{M - 1} x^{k}$
14	13	3expa	$⊢ ((φ \land k \in (0 \dots N - M)) \land x \in [0, 1]) \to x^{M - 1 + k} = x^{M - 1} x^{k}$
15	14	itgeq2dv	$⊢ (φ \land k \in (0 \dots N - M)) \to \int_{[0, 1]} x^{M - 1 + k} d x = \int_{[0, 1]} x^{M - 1} x^{k} d x$
16	15	oveq2d	$⊢ (φ \land k \in (0 \dots N - M)) \to {(- 1)}^{k} (\binom{N - M}{k}) \int_{[0, 1]} x^{M - 1 + k} d x = {(- 1)}^{k} (\binom{N - M}{k}) \int_{[0, 1]} x^{M - 1} x^{k} d x$
17	16	sumeq2dv	$⊢ φ \to \sum_{k = 0}^{N - M} {(- 1)}^{k} (\binom{N - M}{k}) \int_{[0, 1]} x^{M - 1 + k} d x = \sum_{k = 0}^{N - M} {(- 1)}^{k} (\binom{N - M}{k}) \int_{[0, 1]} x^{M - 1} x^{k} d x$
18		0red	$⊢ (φ \land k \in (0 \dots N - M)) \to 0 \in ℝ$
19		1red	$⊢ (φ \land k \in (0 \dots N - M)) \to 1 \in ℝ$
20		0le1	$⊢ 0 \leq 1$
21	20	a1i	$⊢ (φ \land k \in (0 \dots N - M)) \to 0 \leq 1$
22	11	adantr	$⊢ (φ \land k \in (0 \dots N - M)) \to M - 1 \in ℕ_{0}$
23	8	adantl	$⊢ (φ \land k \in (0 \dots N - M)) \to k \in ℕ_{0}$
24	22 23	nn0addcld	$⊢ (φ \land k \in (0 \dots N - M)) \to M - 1 + k \in ℕ_{0}$
25	18 19 21 24	itgpowd	$⊢ (φ \land k \in (0 \dots N - M)) \to \int_{[0, 1]} x^{M - 1 + k} d x = \frac{1^{(M - 1) + k + 1} - 0^{(M - 1) + k + 1}}{(M - 1) + k + 1}$
26	3	nncnd	$⊢ φ \to M \in ℂ$
27	26	adantr	$⊢ (φ \land k \in (0 \dots N - M)) \to M \in ℂ$
28		1cnd	$⊢ (φ \land k \in (0 \dots N - M)) \to 1 \in ℂ$
29		nn0cn	$⊢ k \in ℕ_{0} \to k \in ℂ$
30	8 29	syl	$⊢ k \in (0 \dots N - M) \to k \in ℂ$
31	30	adantl	$⊢ (φ \land k \in (0 \dots N - M)) \to k \in ℂ$
32	27 28 31	nppcand	$⊢ (φ \land k \in (0 \dots N - M)) \to (M - 1) + k + 1 = M + k$
33	32	oveq2d	$⊢ (φ \land k \in (0 \dots N - M)) \to 1^{(M - 1) + k + 1} = 1^{M + k}$
34	32	oveq2d	$⊢ (φ \land k \in (0 \dots N - M)) \to 0^{(M - 1) + k + 1} = 0^{M + k}$
35	33 34	oveq12d	$⊢ (φ \land k \in (0 \dots N - M)) \to 1^{(M - 1) + k + 1} - 0^{(M - 1) + k + 1} = 1^{M + k} - 0^{M + k}$
36	3	adantr	$⊢ (φ \land k \in (0 \dots N - M)) \to M \in ℕ$
37		nnnn0addcl	$⊢ (M \in ℕ \land k \in ℕ_{0}) \to M + k \in ℕ$
38	36 23 37	syl2anc	$⊢ (φ \land k \in (0 \dots N - M)) \to M + k \in ℕ$
39	38	nnzd	$⊢ (φ \land k \in (0 \dots N - M)) \to M + k \in ℤ$
40		1exp	$⊢ M + k \in ℤ \to 1^{M + k} = 1$
41	39 40	syl	$⊢ (φ \land k \in (0 \dots N - M)) \to 1^{M + k} = 1$
42		0exp	$⊢ M + k \in ℕ \to 0^{M + k} = 0$
43	38 42	syl	$⊢ (φ \land k \in (0 \dots N - M)) \to 0^{M + k} = 0$
44	41 43	oveq12d	$⊢ (φ \land k \in (0 \dots N - M)) \to 1^{M + k} - 0^{M + k} = 1 - 0$
45	35 44	eqtrd	$⊢ (φ \land k \in (0 \dots N - M)) \to 1^{(M - 1) + k + 1} - 0^{(M - 1) + k + 1} = 1 - 0$
46		1m0e1	$⊢ 1 - 0 = 1$
47	45 46	eqtrdi	$⊢ (φ \land k \in (0 \dots N - M)) \to 1^{(M - 1) + k + 1} - 0^{(M - 1) + k + 1} = 1$
48	47 32	oveq12d	$⊢ (φ \land k \in (0 \dots N - M)) \to \frac{1^{(M - 1) + k + 1} - 0^{(M - 1) + k + 1}}{(M - 1) + k + 1} = \frac{1}{M + k}$
49	25 48	eqtrd	$⊢ (φ \land k \in (0 \dots N - M)) \to \int_{[0, 1]} x^{M - 1 + k} d x = \frac{1}{M + k}$
50	49	oveq2d	$⊢ (φ \land k \in (0 \dots N - M)) \to {(- 1)}^{k} (\binom{N - M}{k}) \int_{[0, 1]} x^{M - 1 + k} d x = {(- 1)}^{k} (\binom{N - M}{k}) (\frac{1}{M + k})$
51	50	sumeq2dv	$⊢ φ \to \sum_{k = 0}^{N - M} {(- 1)}^{k} (\binom{N - M}{k}) \int_{[0, 1]} x^{M - 1 + k} d x = \sum_{k = 0}^{N - M} {(- 1)}^{k} (\binom{N - M}{k}) (\frac{1}{M + k})$
52	5 17 51	3eqtr2d	$⊢ φ \to F = \sum_{k = 0}^{N - M} {(- 1)}^{k} (\binom{N - M}{k}) (\frac{1}{M + k})$

Metamath Proof Explorer

Theorem lcmineqlem3

Proof