lcmineqlem1

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	lcmineqlem1.1	$⊢ F = \int_{[0, 1]} x^{M - 1} {(1 - x)}^{N - M} d x$
	lcmineqlem1.2	$⊢ φ \to N \in ℕ$
	lcmineqlem1.3	$⊢ φ \to M \in ℕ$
	lcmineqlem1.4	$⊢ φ \to M \leq N$
Assertion	lcmineqlem1	$⊢ φ \to F = \int_{[0, 1]} x^{M - 1} \sum_{k = 0}^{N - M} {(- 1)}^{k} (\binom{N - M}{k}) x^{k} d x$

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem1.1	$⊢ F = \int_{[0, 1]} x^{M - 1} {(1 - x)}^{N - M} d x$
2		lcmineqlem1.2	$⊢ φ \to N \in ℕ$
3		lcmineqlem1.3	$⊢ φ \to M \in ℕ$
4		lcmineqlem1.4	$⊢ φ \to M \leq N$
5		elunitcn	$⊢ x \in [0, 1] \to x \in ℂ$
6		ax-1cn	$⊢ 1 \in ℂ$
7		negsub	$⊢ (1 \in ℂ \land x \in ℂ) \to 1 + (- x) = 1 - x$
8	6 7	mpan	$⊢ x \in ℂ \to 1 + (- x) = 1 - x$
9	8	oveq1d	$⊢ x \in ℂ \to {(1 + (- x))}^{N - M} = {(1 - x)}^{N - M}$
10	9	adantl	$⊢ (φ \land x \in ℂ) \to {(1 + (- x))}^{N - M} = {(1 - x)}^{N - M}$
11		negcl	$⊢ x \in ℂ \to - x \in ℂ$
12		1cnd	$⊢ φ \to 1 \in ℂ$
13	3	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
14	2	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
15		nn0sub	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (M \leq N \leftrightarrow N - M \in ℕ_{0})$
16	13 14 15	syl2anc	$⊢ φ \to (M \leq N \leftrightarrow N - M \in ℕ_{0})$
17	4 16	mpbid	$⊢ φ \to N - M \in ℕ_{0}$
18		binom	$⊢ (1 \in ℂ \land - x \in ℂ \land N - M \in ℕ_{0}) \to {(1 + (- x))}^{N - M} = \sum_{k = 0}^{N - M} (\binom{N - M}{k}) 1^{N - M - k} {(- x)}^{k}$
19	18	3com23	$⊢ (1 \in ℂ \land N - M \in ℕ_{0} \land - x \in ℂ) \to {(1 + (- x))}^{N - M} = \sum_{k = 0}^{N - M} (\binom{N - M}{k}) 1^{N - M - k} {(- x)}^{k}$
20	19	3expia	$⊢ (1 \in ℂ \land N - M \in ℕ_{0}) \to (- x \in ℂ \to {(1 + (- x))}^{N - M} = \sum_{k = 0}^{N - M} (\binom{N - M}{k}) 1^{N - M - k} {(- x)}^{k})$
21	12 17 20	syl2anc	$⊢ φ \to (- x \in ℂ \to {(1 + (- x))}^{N - M} = \sum_{k = 0}^{N - M} (\binom{N - M}{k}) 1^{N - M - k} {(- x)}^{k})$
22	11 21	syl5	$⊢ φ \to (x \in ℂ \to {(1 + (- x))}^{N - M} = \sum_{k = 0}^{N - M} (\binom{N - M}{k}) 1^{N - M - k} {(- x)}^{k})$
23	22	imp	$⊢ (φ \land x \in ℂ) \to {(1 + (- x))}^{N - M} = \sum_{k = 0}^{N - M} (\binom{N - M}{k}) 1^{N - M - k} {(- x)}^{k}$
24	10 23	eqtr3d	$⊢ (φ \land x \in ℂ) \to {(1 - x)}^{N - M} = \sum_{k = 0}^{N - M} (\binom{N - M}{k}) 1^{N - M - k} {(- x)}^{k}$
25		elfzelz	$⊢ k \in (0 \dots N - M) \to k \in ℤ$
26	2	nnzd	$⊢ φ \to N \in ℤ$
27	3	nnzd	$⊢ φ \to M \in ℤ$
28		zsubcl	$⊢ (N \in ℤ \land M \in ℤ) \to N - M \in ℤ$
29	26 27 28	syl2anc	$⊢ φ \to N - M \in ℤ$
30		zsubcl	$⊢ (N - M \in ℤ \land k \in ℤ) \to N - M - k \in ℤ$
31	29 30	sylan	$⊢ (φ \land k \in ℤ) \to N - M - k \in ℤ$
32	25 31	sylan2	$⊢ (φ \land k \in (0 \dots N - M)) \to N - M - k \in ℤ$
33		1exp	$⊢ N - M - k \in ℤ \to 1^{N - M - k} = 1$
34	32 33	syl	$⊢ (φ \land k \in (0 \dots N - M)) \to 1^{N - M - k} = 1$
35	34	3adant2	$⊢ (φ \land x \in ℂ \land k \in (0 \dots N - M)) \to 1^{N - M - k} = 1$
36	35	oveq1d	$⊢ (φ \land x \in ℂ \land k \in (0 \dots N - M)) \to 1^{N - M - k} {(- x)}^{k} = 1 {(- x)}^{k}$
37	11	3ad2ant2	$⊢ (φ \land x \in ℂ \land k \in (0 \dots N - M)) \to - x \in ℂ$
38		elfznn0	$⊢ k \in (0 \dots N - M) \to k \in ℕ_{0}$
39	38	3ad2ant3	$⊢ (φ \land x \in ℂ \land k \in (0 \dots N - M)) \to k \in ℕ_{0}$
40		expcl	$⊢ (- x \in ℂ \land k \in ℕ_{0}) \to {(- x)}^{k} \in ℂ$
41	37 39 40	syl2anc	$⊢ (φ \land x \in ℂ \land k \in (0 \dots N - M)) \to {(- x)}^{k} \in ℂ$
42	41	mulid2d	$⊢ (φ \land x \in ℂ \land k \in (0 \dots N - M)) \to 1 {(- x)}^{k} = {(- x)}^{k}$
43	36 42	eqtrd	$⊢ (φ \land x \in ℂ \land k \in (0 \dots N - M)) \to 1^{N - M - k} {(- x)}^{k} = {(- x)}^{k}$
44		mulm1	$⊢ x \in ℂ \to -1 x = - x$
45	44	oveq1d	$⊢ x \in ℂ \to {-1 x}^{k} = {(- x)}^{k}$
46	45	3ad2ant2	$⊢ (φ \land x \in ℂ \land k \in (0 \dots N - M)) \to {-1 x}^{k} = {(- x)}^{k}$
47	43 46	eqtr4d	$⊢ (φ \land x \in ℂ \land k \in (0 \dots N - M)) \to 1^{N - M - k} {(- x)}^{k} = {-1 x}^{k}$
48		neg1cn	$⊢ - 1 \in ℂ$
49		mulexp	$⊢ (- 1 \in ℂ \land x \in ℂ \land k \in ℕ_{0}) \to {-1 x}^{k} = {(- 1)}^{k} x^{k}$
50	48 49	mp3an1	$⊢ (x \in ℂ \land k \in ℕ_{0}) \to {-1 x}^{k} = {(- 1)}^{k} x^{k}$
51	38 50	sylan2	$⊢ (x \in ℂ \land k \in (0 \dots N - M)) \to {-1 x}^{k} = {(- 1)}^{k} x^{k}$
52	51	3adant1	$⊢ (φ \land x \in ℂ \land k \in (0 \dots N - M)) \to {-1 x}^{k} = {(- 1)}^{k} x^{k}$
53	47 52	eqtrd	$⊢ (φ \land x \in ℂ \land k \in (0 \dots N - M)) \to 1^{N - M - k} {(- x)}^{k} = {(- 1)}^{k} x^{k}$
54	53	oveq2d	$⊢ (φ \land x \in ℂ \land k \in (0 \dots N - M)) \to (\binom{N - M}{k}) 1^{N - M - k} {(- x)}^{k} = (\binom{N - M}{k}) {(- 1)}^{k} x^{k}$
55		bccl	$⊢ (N - M \in ℕ_{0} \land k \in ℤ) \to (\binom{N - M}{k}) \in ℕ_{0}$
56	17 25 55	syl2an	$⊢ (φ \land k \in (0 \dots N - M)) \to (\binom{N - M}{k}) \in ℕ_{0}$
57	56	3adant2	$⊢ (φ \land x \in ℂ \land k \in (0 \dots N - M)) \to (\binom{N - M}{k}) \in ℕ_{0}$
58	57	nn0cnd	$⊢ (φ \land x \in ℂ \land k \in (0 \dots N - M)) \to (\binom{N - M}{k}) \in ℂ$
59		expcl	$⊢ (- 1 \in ℂ \land k \in ℕ_{0}) \to {(- 1)}^{k} \in ℂ$
60	48 39 59	sylancr	$⊢ (φ \land x \in ℂ \land k \in (0 \dots N - M)) \to {(- 1)}^{k} \in ℂ$
61		expcl	$⊢ (x \in ℂ \land k \in ℕ_{0}) \to x^{k} \in ℂ$
62	38 61	sylan2	$⊢ (x \in ℂ \land k \in (0 \dots N - M)) \to x^{k} \in ℂ$
63	62	3adant1	$⊢ (φ \land x \in ℂ \land k \in (0 \dots N - M)) \to x^{k} \in ℂ$
64	58 60 63	mulassd	$⊢ (φ \land x \in ℂ \land k \in (0 \dots N - M)) \to (\binom{N - M}{k}) {(- 1)}^{k} x^{k} = (\binom{N - M}{k}) {(- 1)}^{k} x^{k}$
65	54 64	eqtr4d	$⊢ (φ \land x \in ℂ \land k \in (0 \dots N - M)) \to (\binom{N - M}{k}) 1^{N - M - k} {(- x)}^{k} = (\binom{N - M}{k}) {(- 1)}^{k} x^{k}$
66	58 60	mulcomd	$⊢ (φ \land x \in ℂ \land k \in (0 \dots N - M)) \to (\binom{N - M}{k}) {(- 1)}^{k} = {(- 1)}^{k} (\binom{N - M}{k})$
67	66	oveq1d	$⊢ (φ \land x \in ℂ \land k \in (0 \dots N - M)) \to (\binom{N - M}{k}) {(- 1)}^{k} x^{k} = {(- 1)}^{k} (\binom{N - M}{k}) x^{k}$
68	65 67	eqtrd	$⊢ (φ \land x \in ℂ \land k \in (0 \dots N - M)) \to (\binom{N - M}{k}) 1^{N - M - k} {(- x)}^{k} = {(- 1)}^{k} (\binom{N - M}{k}) x^{k}$
69	68	3expa	$⊢ ((φ \land x \in ℂ) \land k \in (0 \dots N - M)) \to (\binom{N - M}{k}) 1^{N - M - k} {(- x)}^{k} = {(- 1)}^{k} (\binom{N - M}{k}) x^{k}$
70	69	sumeq2dv	$⊢ (φ \land x \in ℂ) \to \sum_{k = 0}^{N - M} (\binom{N - M}{k}) 1^{N - M - k} {(- x)}^{k} = \sum_{k = 0}^{N - M} {(- 1)}^{k} (\binom{N - M}{k}) x^{k}$
71	24 70	eqtrd	$⊢ (φ \land x \in ℂ) \to {(1 - x)}^{N - M} = \sum_{k = 0}^{N - M} {(- 1)}^{k} (\binom{N - M}{k}) x^{k}$
72	5 71	sylan2	$⊢ (φ \land x \in [0, 1]) \to {(1 - x)}^{N - M} = \sum_{k = 0}^{N - M} {(- 1)}^{k} (\binom{N - M}{k}) x^{k}$
73	72	oveq2d	$⊢ (φ \land x \in [0, 1]) \to x^{M - 1} {(1 - x)}^{N - M} = x^{M - 1} \sum_{k = 0}^{N - M} {(- 1)}^{k} (\binom{N - M}{k}) x^{k}$
74	73	itgeq2dv	$⊢ φ \to \int_{[0, 1]} x^{M - 1} {(1 - x)}^{N - M} d x = \int_{[0, 1]} x^{M - 1} \sum_{k = 0}^{N - M} {(- 1)}^{k} (\binom{N - M}{k}) x^{k} d x$
75	1 74	syl5eq	$⊢ φ \to F = \int_{[0, 1]} x^{M - 1} \sum_{k = 0}^{N - M} {(- 1)}^{k} (\binom{N - M}{k}) x^{k} d x$

Metamath Proof Explorer

Theorem lcmineqlem1

Proof