lcmineqlem2

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

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

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem2.1	$⊢ F = \int_{[0, 1]} x^{M - 1} {(1 - x)}^{N - M} d x$
2		lcmineqlem2.2	$⊢ φ \to N \in ℕ$
3		lcmineqlem2.3	$⊢ φ \to M \in ℕ$
4		lcmineqlem2.4	$⊢ φ \to M \leq N$
5	1 2 3 4	lcmineqlem1	$⊢ φ \to F = \int_{[0, 1]} x^{M - 1} \sum_{k = 0}^{N - M} {(- 1)}^{k} (\binom{N - M}{k}) x^{k} d x$
6		eqid	$⊢ [0, 1] = [0, 1]$
7		fzfid	$⊢ φ \to (0 \dots N - M) \in Fin$
8		0red	$⊢ φ \to 0 \in ℝ$
9		1red	$⊢ φ \to 1 \in ℝ$
10		unitsscn	$⊢ [0, 1] \subseteq ℂ$
11		resmpt	$⊢ [0, 1] \subseteq ℂ \to {(x \in ℂ ⟼ x^{M - 1}) ↾}_{[0, 1]} = (x \in [0, 1] ⟼ x^{M - 1})$
12	10 11	ax-mp	$⊢ {(x \in ℂ ⟼ x^{M - 1}) ↾}_{[0, 1]} = (x \in [0, 1] ⟼ x^{M - 1})$
13		nnm1nn0	$⊢ M \in ℕ \to M - 1 \in ℕ_{0}$
14		expcncf	$⊢ M - 1 \in ℕ_{0} \to (x \in ℂ ⟼ x^{M - 1}) : ℂ \underset{cn}{⟶} ℂ$
15		rescncf	$⊢ [0, 1] \subseteq ℂ \to ((x \in ℂ ⟼ x^{M - 1}) : ℂ \underset{cn}{⟶} ℂ \to ({(x \in ℂ ⟼ x^{M - 1}) ↾}_{[0, 1]}) : [0, 1] \underset{cn}{⟶} ℂ)$
16	10 15	ax-mp	$⊢ (x \in ℂ ⟼ x^{M - 1}) : ℂ \underset{cn}{⟶} ℂ \to ({(x \in ℂ ⟼ x^{M - 1}) ↾}_{[0, 1]}) : [0, 1] \underset{cn}{⟶} ℂ$
17	3 13 14 16	4syl	$⊢ φ \to ({(x \in ℂ ⟼ x^{M - 1}) ↾}_{[0, 1]}) : [0, 1] \underset{cn}{⟶} ℂ$
18	12 17	eqeltrrid	$⊢ φ \to (x \in [0, 1] ⟼ x^{M - 1}) : [0, 1] \underset{cn}{⟶} ℂ$
19		elfznn0	$⊢ k \in (0 \dots N - M) \to k \in ℕ_{0}$
20		neg1cn	$⊢ - 1 \in ℂ$
21		expcl	$⊢ (- 1 \in ℂ \land k \in ℕ_{0}) \to {(- 1)}^{k} \in ℂ$
22	20 21	mpan	$⊢ k \in ℕ_{0} \to {(- 1)}^{k} \in ℂ$
23	19 22	syl	$⊢ k \in (0 \dots N - M) \to {(- 1)}^{k} \in ℂ$
24	23	adantl	$⊢ (φ \land k \in (0 \dots N - M)) \to {(- 1)}^{k} \in ℂ$
25	3	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
26	2	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
27		nn0sub	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (M \leq N \leftrightarrow N - M \in ℕ_{0})$
28	25 26 27	syl2anc	$⊢ φ \to (M \leq N \leftrightarrow N - M \in ℕ_{0})$
29	4 28	mpbid	$⊢ φ \to N - M \in ℕ_{0}$
30		nn0z	$⊢ k \in ℕ_{0} \to k \in ℤ$
31	19 30	syl	$⊢ k \in (0 \dots N - M) \to k \in ℤ$
32		bccl	$⊢ (N - M \in ℕ_{0} \land k \in ℤ) \to (\binom{N - M}{k}) \in ℕ_{0}$
33	31 32	sylan2	$⊢ (N - M \in ℕ_{0} \land k \in (0 \dots N - M)) \to (\binom{N - M}{k}) \in ℕ_{0}$
34	29 33	sylan	$⊢ (φ \land k \in (0 \dots N - M)) \to (\binom{N - M}{k}) \in ℕ_{0}$
35	34	nn0cnd	$⊢ (φ \land k \in (0 \dots N - M)) \to (\binom{N - M}{k}) \in ℂ$
36	24 35	mulcld	$⊢ (φ \land k \in (0 \dots N - M)) \to {(- 1)}^{k} (\binom{N - M}{k}) \in ℂ$
37		resmpt	$⊢ [0, 1] \subseteq ℂ \to {(x \in ℂ ⟼ x^{k}) ↾}_{[0, 1]} = (x \in [0, 1] ⟼ x^{k})$
38	10 37	ax-mp	$⊢ {(x \in ℂ ⟼ x^{k}) ↾}_{[0, 1]} = (x \in [0, 1] ⟼ x^{k})$
39		expcncf	$⊢ k \in ℕ_{0} \to (x \in ℂ ⟼ x^{k}) : ℂ \underset{cn}{⟶} ℂ$
40	19 39	syl	$⊢ k \in (0 \dots N - M) \to (x \in ℂ ⟼ x^{k}) : ℂ \underset{cn}{⟶} ℂ$
41		rescncf	$⊢ [0, 1] \subseteq ℂ \to ((x \in ℂ ⟼ x^{k}) : ℂ \underset{cn}{⟶} ℂ \to ({(x \in ℂ ⟼ x^{k}) ↾}_{[0, 1]}) : [0, 1] \underset{cn}{⟶} ℂ)$
42	10 41	ax-mp	$⊢ (x \in ℂ ⟼ x^{k}) : ℂ \underset{cn}{⟶} ℂ \to ({(x \in ℂ ⟼ x^{k}) ↾}_{[0, 1]}) : [0, 1] \underset{cn}{⟶} ℂ$
43	40 42	syl	$⊢ k \in (0 \dots N - M) \to ({(x \in ℂ ⟼ x^{k}) ↾}_{[0, 1]}) : [0, 1] \underset{cn}{⟶} ℂ$
44	38 43	eqeltrrid	$⊢ k \in (0 \dots N - M) \to (x \in [0, 1] ⟼ x^{k}) : [0, 1] \underset{cn}{⟶} ℂ$
45	44	adantl	$⊢ (φ \land k \in (0 \dots N - M)) \to (x \in [0, 1] ⟼ x^{k}) : [0, 1] \underset{cn}{⟶} ℂ$
46	6 7 8 9 18 36 45	3factsumint	$⊢ φ \to \int_{[0, 1]} x^{M - 1} \sum_{k = 0}^{N - M} {(- 1)}^{k} (\binom{N - M}{k}) x^{k} d x = \sum_{k = 0}^{N - M} {(- 1)}^{k} (\binom{N - M}{k}) \int_{[0, 1]} x^{M - 1} x^{k} d x$
47	5 46	eqtrd	$⊢ φ \to F = \sum_{k = 0}^{N - M} {(- 1)}^{k} (\binom{N - M}{k}) \int_{[0, 1]} x^{M - 1} x^{k} d x$

Metamath Proof Explorer

Theorem lcmineqlem2

Proof