Theorem 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	⊢ 𝐹 = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥
	lcmineqlem1.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	lcmineqlem1.3	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	lcmineqlem1.4	⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
Assertion	lcmineqlem1	⊢ ( 𝜑 → 𝐹 = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( 𝑥 ↑ 𝑘 ) ) ) d 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem1.1	⊢ 𝐹 = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥
2		lcmineqlem1.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3		lcmineqlem1.3	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
4		lcmineqlem1.4	⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
5		elunitcn	⊢ ( 𝑥 ∈ ( 0 [,] 1 ) → 𝑥 ∈ ℂ )
6		ax-1cn	⊢ 1 ∈ ℂ
7		negsub	⊢ ( ( 1 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 1 + - 𝑥 ) = ( 1 − 𝑥 ) )
8	6 7	mpan	⊢ ( 𝑥 ∈ ℂ → ( 1 + - 𝑥 ) = ( 1 − 𝑥 ) )
9	8	oveq1d	⊢ ( 𝑥 ∈ ℂ → ( ( 1 + - 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) = ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) )
10	9	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 1 + - 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) = ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) )
11		negcl	⊢ ( 𝑥 ∈ ℂ → - 𝑥 ∈ ℂ )
12		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
13	3	nnnn0d	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
14	2	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
15		nn0sub	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝑁 − 𝑀 ) ∈ ℕ0 ) )
16	13 14 15	syl2anc	⊢ ( 𝜑 → ( 𝑀 ≤ 𝑁 ↔ ( 𝑁 − 𝑀 ) ∈ ℕ0 ) )
17	4 16	mpbid	⊢ ( 𝜑 → ( 𝑁 − 𝑀 ) ∈ ℕ0 )
18		binom	⊢ ( ( 1 ∈ ℂ ∧ - 𝑥 ∈ ℂ ∧ ( 𝑁 − 𝑀 ) ∈ ℕ0 ) → ( ( 1 + - 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( 𝑁 − 𝑀 ) C 𝑘 ) · ( ( 1 ↑ ( ( 𝑁 − 𝑀 ) − 𝑘 ) ) · ( - 𝑥 ↑ 𝑘 ) ) ) )
19	18	3com23	⊢ ( ( 1 ∈ ℂ ∧ ( 𝑁 − 𝑀 ) ∈ ℕ0 ∧ - 𝑥 ∈ ℂ ) → ( ( 1 + - 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( 𝑁 − 𝑀 ) C 𝑘 ) · ( ( 1 ↑ ( ( 𝑁 − 𝑀 ) − 𝑘 ) ) · ( - 𝑥 ↑ 𝑘 ) ) ) )
20	19	3expia	⊢ ( ( 1 ∈ ℂ ∧ ( 𝑁 − 𝑀 ) ∈ ℕ0 ) → ( - 𝑥 ∈ ℂ → ( ( 1 + - 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( 𝑁 − 𝑀 ) C 𝑘 ) · ( ( 1 ↑ ( ( 𝑁 − 𝑀 ) − 𝑘 ) ) · ( - 𝑥 ↑ 𝑘 ) ) ) ) )
21	12 17 20	syl2anc	⊢ ( 𝜑 → ( - 𝑥 ∈ ℂ → ( ( 1 + - 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( 𝑁 − 𝑀 ) C 𝑘 ) · ( ( 1 ↑ ( ( 𝑁 − 𝑀 ) − 𝑘 ) ) · ( - 𝑥 ↑ 𝑘 ) ) ) ) )
22	11 21	syl5	⊢ ( 𝜑 → ( 𝑥 ∈ ℂ → ( ( 1 + - 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( 𝑁 − 𝑀 ) C 𝑘 ) · ( ( 1 ↑ ( ( 𝑁 − 𝑀 ) − 𝑘 ) ) · ( - 𝑥 ↑ 𝑘 ) ) ) ) )
23	22	imp	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 1 + - 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( 𝑁 − 𝑀 ) C 𝑘 ) · ( ( 1 ↑ ( ( 𝑁 − 𝑀 ) − 𝑘 ) ) · ( - 𝑥 ↑ 𝑘 ) ) ) )
24	10 23	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( 𝑁 − 𝑀 ) C 𝑘 ) · ( ( 1 ↑ ( ( 𝑁 − 𝑀 ) − 𝑘 ) ) · ( - 𝑥 ↑ 𝑘 ) ) ) )
25		elfzelz	⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → 𝑘 ∈ ℤ )
26	2	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
27	3	nnzd	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
28		zsubcl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 − 𝑀 ) ∈ ℤ )
29	26 27 28	syl2anc	⊢ ( 𝜑 → ( 𝑁 − 𝑀 ) ∈ ℤ )
30		zsubcl	⊢ ( ( ( 𝑁 − 𝑀 ) ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑁 − 𝑀 ) − 𝑘 ) ∈ ℤ )
31	29 30	sylan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ( 𝑁 − 𝑀 ) − 𝑘 ) ∈ ℤ )
32	25 31	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 𝑁 − 𝑀 ) − 𝑘 ) ∈ ℤ )
33		1exp	⊢ ( ( ( 𝑁 − 𝑀 ) − 𝑘 ) ∈ ℤ → ( 1 ↑ ( ( 𝑁 − 𝑀 ) − 𝑘 ) ) = 1 )
34	32 33	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( 1 ↑ ( ( 𝑁 − 𝑀 ) − 𝑘 ) ) = 1 )
35	34	3adant2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( 1 ↑ ( ( 𝑁 − 𝑀 ) − 𝑘 ) ) = 1 )
36	35	oveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 1 ↑ ( ( 𝑁 − 𝑀 ) − 𝑘 ) ) · ( - 𝑥 ↑ 𝑘 ) ) = ( 1 · ( - 𝑥 ↑ 𝑘 ) ) )
37	11	3ad2ant2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → - 𝑥 ∈ ℂ )
38		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → 𝑘 ∈ ℕ0 )
39	38	3ad2ant3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → 𝑘 ∈ ℕ0 )
40		expcl	⊢ ( ( - 𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( - 𝑥 ↑ 𝑘 ) ∈ ℂ )
41	37 39 40	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( - 𝑥 ↑ 𝑘 ) ∈ ℂ )
42	41	mullidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( 1 · ( - 𝑥 ↑ 𝑘 ) ) = ( - 𝑥 ↑ 𝑘 ) )
43	36 42	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 1 ↑ ( ( 𝑁 − 𝑀 ) − 𝑘 ) ) · ( - 𝑥 ↑ 𝑘 ) ) = ( - 𝑥 ↑ 𝑘 ) )
44		mulm1	⊢ ( 𝑥 ∈ ℂ → ( - 1 · 𝑥 ) = - 𝑥 )
45	44	oveq1d	⊢ ( 𝑥 ∈ ℂ → ( ( - 1 · 𝑥 ) ↑ 𝑘 ) = ( - 𝑥 ↑ 𝑘 ) )
46	45	3ad2ant2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( - 1 · 𝑥 ) ↑ 𝑘 ) = ( - 𝑥 ↑ 𝑘 ) )
47	43 46	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 1 ↑ ( ( 𝑁 − 𝑀 ) − 𝑘 ) ) · ( - 𝑥 ↑ 𝑘 ) ) = ( ( - 1 · 𝑥 ) ↑ 𝑘 ) )
48		neg1cn	⊢ - 1 ∈ ℂ
49		mulexp	⊢ ( ( - 1 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( - 1 · 𝑥 ) ↑ 𝑘 ) = ( ( - 1 ↑ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) )
50	48 49	mp3an1	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( - 1 · 𝑥 ) ↑ 𝑘 ) = ( ( - 1 ↑ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) )
51	38 50	sylan2	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( - 1 · 𝑥 ) ↑ 𝑘 ) = ( ( - 1 ↑ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) )
52	51	3adant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( - 1 · 𝑥 ) ↑ 𝑘 ) = ( ( - 1 ↑ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) )
53	47 52	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 1 ↑ ( ( 𝑁 − 𝑀 ) − 𝑘 ) ) · ( - 𝑥 ↑ 𝑘 ) ) = ( ( - 1 ↑ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) )
54	53	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( ( 𝑁 − 𝑀 ) C 𝑘 ) · ( ( 1 ↑ ( ( 𝑁 − 𝑀 ) − 𝑘 ) ) · ( - 𝑥 ↑ 𝑘 ) ) ) = ( ( ( 𝑁 − 𝑀 ) C 𝑘 ) · ( ( - 1 ↑ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) )
55		bccl	⊢ ( ( ( 𝑁 − 𝑀 ) ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( ( 𝑁 − 𝑀 ) C 𝑘 ) ∈ ℕ0 )
56	17 25 55	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 𝑁 − 𝑀 ) C 𝑘 ) ∈ ℕ0 )
57	56	3adant2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 𝑁 − 𝑀 ) C 𝑘 ) ∈ ℕ0 )
58	57	nn0cnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 𝑁 − 𝑀 ) C 𝑘 ) ∈ ℂ )
59		expcl	⊢ ( ( - 1 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( - 1 ↑ 𝑘 ) ∈ ℂ )
60	48 39 59	sylancr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( - 1 ↑ 𝑘 ) ∈ ℂ )
61		expcl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑥 ↑ 𝑘 ) ∈ ℂ )
62	38 61	sylan2	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( 𝑥 ↑ 𝑘 ) ∈ ℂ )
63	62	3adant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( 𝑥 ↑ 𝑘 ) ∈ ℂ )
64	58 60 63	mulassd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( ( ( 𝑁 − 𝑀 ) C 𝑘 ) · ( - 1 ↑ 𝑘 ) ) · ( 𝑥 ↑ 𝑘 ) ) = ( ( ( 𝑁 − 𝑀 ) C 𝑘 ) · ( ( - 1 ↑ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) )
65	54 64	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( ( 𝑁 − 𝑀 ) C 𝑘 ) · ( ( 1 ↑ ( ( 𝑁 − 𝑀 ) − 𝑘 ) ) · ( - 𝑥 ↑ 𝑘 ) ) ) = ( ( ( ( 𝑁 − 𝑀 ) C 𝑘 ) · ( - 1 ↑ 𝑘 ) ) · ( 𝑥 ↑ 𝑘 ) ) )
66	58 60	mulcomd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( ( 𝑁 − 𝑀 ) C 𝑘 ) · ( - 1 ↑ 𝑘 ) ) = ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) )
67	66	oveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( ( ( 𝑁 − 𝑀 ) C 𝑘 ) · ( - 1 ↑ 𝑘 ) ) · ( 𝑥 ↑ 𝑘 ) ) = ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( 𝑥 ↑ 𝑘 ) ) )
68	65 67	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( ( 𝑁 − 𝑀 ) C 𝑘 ) · ( ( 1 ↑ ( ( 𝑁 − 𝑀 ) − 𝑘 ) ) · ( - 𝑥 ↑ 𝑘 ) ) ) = ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( 𝑥 ↑ 𝑘 ) ) )
69	68	3expa	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( ( 𝑁 − 𝑀 ) C 𝑘 ) · ( ( 1 ↑ ( ( 𝑁 − 𝑀 ) − 𝑘 ) ) · ( - 𝑥 ↑ 𝑘 ) ) ) = ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( 𝑥 ↑ 𝑘 ) ) )
70	69	sumeq2dv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( 𝑁 − 𝑀 ) C 𝑘 ) · ( ( 1 ↑ ( ( 𝑁 − 𝑀 ) − 𝑘 ) ) · ( - 𝑥 ↑ 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( 𝑥 ↑ 𝑘 ) ) )
71	24 70	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( 𝑥 ↑ 𝑘 ) ) )
72	5 71	sylan2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( 𝑥 ↑ 𝑘 ) ) )
73	72	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) = ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( 𝑥 ↑ 𝑘 ) ) ) )
74	73	itgeq2dv	⊢ ( 𝜑 → ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( 𝑥 ↑ 𝑘 ) ) ) d 𝑥 )
75	1 74	eqtrid	⊢ ( 𝜑 → 𝐹 = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( 𝑥 ↑ 𝑘 ) ) ) d 𝑥 )