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	3 13 14	3syl	$⊢ φ \to (x \in ℂ ⟼ x^{M - 1}) : ℂ \underset{cn}{⟶} ℂ$
16		rescncf	$⊢ [0, 1] \subseteq ℂ \to ((x \in ℂ ⟼ x^{M - 1}) : ℂ \underset{cn}{⟶} ℂ \to ({(x \in ℂ ⟼ x^{M - 1}) ↾}_{[0, 1]}) : [0, 1] \underset{cn}{⟶} ℂ)$
17	10 16	ax-mp	$⊢ (x \in ℂ ⟼ x^{M - 1}) : ℂ \underset{cn}{⟶} ℂ \to ({(x \in ℂ ⟼ x^{M - 1}) ↾}_{[0, 1]}) : [0, 1] \underset{cn}{⟶} ℂ$
18	15 17	syl	$⊢ φ \to ({(x \in ℂ ⟼ x^{M - 1}) ↾}_{[0, 1]}) : [0, 1] \underset{cn}{⟶} ℂ$
19	12 18	eqeltrrid	$⊢ φ \to (x \in [0, 1] ⟼ x^{M - 1}) : [0, 1] \underset{cn}{⟶} ℂ$
20		elfznn0	$⊢ k \in (0 \dots N - M) \to k \in ℕ_{0}$
21		neg1cn	$⊢ - 1 \in ℂ$
22		expcl	$⊢ (- 1 \in ℂ \land k \in ℕ_{0}) \to {(- 1)}^{k} \in ℂ$
23	21 22	mpan	$⊢ k \in ℕ_{0} \to {(- 1)}^{k} \in ℂ$
24	20 23	syl	$⊢ k \in (0 \dots N - M) \to {(- 1)}^{k} \in ℂ$
25	24	adantl	$⊢ (φ \land k \in (0 \dots N - M)) \to {(- 1)}^{k} \in ℂ$
26	3	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
27	2	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
28		nn0sub	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (M \leq N \leftrightarrow N - M \in ℕ_{0})$
29	26 27 28	syl2anc	$⊢ φ \to (M \leq N \leftrightarrow N - M \in ℕ_{0})$
30	4 29	mpbid	$⊢ φ \to N - M \in ℕ_{0}$
31		nn0z	$⊢ k \in ℕ_{0} \to k \in ℤ$
32	20 31	syl	$⊢ k \in (0 \dots N - M) \to k \in ℤ$
33		bccl	$⊢ (N - M \in ℕ_{0} \land k \in ℤ) \to (\binom{N - M}{k}) \in ℕ_{0}$
34	32 33	sylan2	$⊢ (N - M \in ℕ_{0} \land k \in (0 \dots N - M)) \to (\binom{N - M}{k}) \in ℕ_{0}$
35	30 34	sylan	$⊢ (φ \land k \in (0 \dots N - M)) \to (\binom{N - M}{k}) \in ℕ_{0}$
36	35	nn0cnd	$⊢ (φ \land k \in (0 \dots N - M)) \to (\binom{N - M}{k}) \in ℂ$
37	25 36	mulcld	$⊢ (φ \land k \in (0 \dots N - M)) \to {(- 1)}^{k} (\binom{N - M}{k}) \in ℂ$
38		resmpt	$⊢ [0, 1] \subseteq ℂ \to {(x \in ℂ ⟼ x^{k}) ↾}_{[0, 1]} = (x \in [0, 1] ⟼ x^{k})$
39	10 38	ax-mp	$⊢ {(x \in ℂ ⟼ x^{k}) ↾}_{[0, 1]} = (x \in [0, 1] ⟼ x^{k})$
40		expcncf	$⊢ k \in ℕ_{0} \to (x \in ℂ ⟼ x^{k}) : ℂ \underset{cn}{⟶} ℂ$
41	20 40	syl	$⊢ k \in (0 \dots N - M) \to (x \in ℂ ⟼ x^{k}) : ℂ \underset{cn}{⟶} ℂ$
42		rescncf	$⊢ [0, 1] \subseteq ℂ \to ((x \in ℂ ⟼ x^{k}) : ℂ \underset{cn}{⟶} ℂ \to ({(x \in ℂ ⟼ x^{k}) ↾}_{[0, 1]}) : [0, 1] \underset{cn}{⟶} ℂ)$
43	10 42	ax-mp	$⊢ (x \in ℂ ⟼ x^{k}) : ℂ \underset{cn}{⟶} ℂ \to ({(x \in ℂ ⟼ x^{k}) ↾}_{[0, 1]}) : [0, 1] \underset{cn}{⟶} ℂ$
44	41 43	syl	$⊢ k \in (0 \dots N - M) \to ({(x \in ℂ ⟼ x^{k}) ↾}_{[0, 1]}) : [0, 1] \underset{cn}{⟶} ℂ$
45	39 44	eqeltrrid	$⊢ k \in (0 \dots N - M) \to (x \in [0, 1] ⟼ x^{k}) : [0, 1] \underset{cn}{⟶} ℂ$
46	45	adantl	$⊢ (φ \land k \in (0 \dots N - M)) \to (x \in [0, 1] ⟼ x^{k}) : [0, 1] \underset{cn}{⟶} ℂ$
47	6 7 8 9 19 37 46	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$
48	5 47	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