Metamath Proof Explorer

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 mulid2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ 𝑘 ∈ ( 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 syl5eq ⊢ ( 𝜑 → 𝐹 = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( 𝑥 ↑ 𝑘 ) ) ) d 𝑥 )