Metamath Proof Explorer

Theorem lcmineqlem3

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

Ref Expression
Hypotheses lcmineqlem3.1 ⊢ 𝐹 = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥
lcmineqlem3.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
lcmineqlem3.3 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
lcmineqlem3.4 ⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
Assertion lcmineqlem3 ( 𝜑 → 𝐹 = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( 1 / ( 𝑀 + 𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 lcmineqlem3.1 ⊢ 𝐹 = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥
2 lcmineqlem3.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 lcmineqlem3.3 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
4 lcmineqlem3.4 ⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
5 1 2 3 4 lcmineqlem2 ⊢ ( 𝜑 → 𝐹 = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( 𝑥 ↑ 𝑘 ) ) d 𝑥 ) )
6 elunitcn ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) → 𝑥 ∈ ℂ )
7 6 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → 𝑥 ∈ ℂ )
8 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → 𝑘 ∈ ℕ0 )
9 8 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → 𝑘 ∈ ℕ0 )
10 nnm1nn0 ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 − 1 ) ∈ ℕ0 )
11 3 10 syl ⊢ ( 𝜑 → ( 𝑀 − 1 ) ∈ ℕ0 )
12 11 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( 𝑀 − 1 ) ∈ ℕ0 )
13 7 9 12 expaddd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( 𝑥 ↑ ( ( 𝑀 − 1 ) + 𝑘 ) ) = ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( 𝑥 ↑ 𝑘 ) ) )
14 13 3expa ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( 𝑥 ↑ ( ( 𝑀 − 1 ) + 𝑘 ) ) = ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( 𝑥 ↑ 𝑘 ) ) )
15 14 itgeq2dv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ∫ ( 0 [,] 1 ) ( 𝑥 ↑ ( ( 𝑀 − 1 ) + 𝑘 ) ) d 𝑥 = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( 𝑥 ↑ 𝑘 ) ) d 𝑥 )
16 15 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ∫ ( 0 [,] 1 ) ( 𝑥 ↑ ( ( 𝑀 − 1 ) + 𝑘 ) ) d 𝑥 ) = ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( 𝑥 ↑ 𝑘 ) ) d 𝑥 ) )
17 16 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ∫ ( 0 [,] 1 ) ( 𝑥 ↑ ( ( 𝑀 − 1 ) + 𝑘 ) ) d 𝑥 ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( 𝑥 ↑ 𝑘 ) ) d 𝑥 ) )
18 0red ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → 0 ∈ ℝ )
19 1red ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → 1 ∈ ℝ )
20 0le1 ⊢ 0 ≤ 1
21 20 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → 0 ≤ 1 )
22 11 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( 𝑀 − 1 ) ∈ ℕ0 )
23 8 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → 𝑘 ∈ ℕ0 )
24 22 23 nn0addcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 𝑀 − 1 ) + 𝑘 ) ∈ ℕ0 )
25 18 19 21 24 itgpowd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ∫ ( 0 [,] 1 ) ( 𝑥 ↑ ( ( 𝑀 − 1 ) + 𝑘 ) ) d 𝑥 = ( ( ( 1 ↑ ( ( ( 𝑀 − 1 ) + 𝑘 ) + 1 ) ) − ( 0 ↑ ( ( ( 𝑀 − 1 ) + 𝑘 ) + 1 ) ) ) / ( ( ( 𝑀 − 1 ) + 𝑘 ) + 1 ) ) )
26 3 nncnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → 𝑀 ∈ ℂ )
28 1cnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → 1 ∈ ℂ )
29 nn0cn ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ )
30 8 29 syl ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → 𝑘 ∈ ℂ )
31 30 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → 𝑘 ∈ ℂ )
32 27 28 31 nppcand ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( ( 𝑀 − 1 ) + 𝑘 ) + 1 ) = ( 𝑀 + 𝑘 ) )
33 32 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( 1 ↑ ( ( ( 𝑀 − 1 ) + 𝑘 ) + 1 ) ) = ( 1 ↑ ( 𝑀 + 𝑘 ) ) )
34 32 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( 0 ↑ ( ( ( 𝑀 − 1 ) + 𝑘 ) + 1 ) ) = ( 0 ↑ ( 𝑀 + 𝑘 ) ) )
35 33 34 oveq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 1 ↑ ( ( ( 𝑀 − 1 ) + 𝑘 ) + 1 ) ) − ( 0 ↑ ( ( ( 𝑀 − 1 ) + 𝑘 ) + 1 ) ) ) = ( ( 1 ↑ ( 𝑀 + 𝑘 ) ) − ( 0 ↑ ( 𝑀 + 𝑘 ) ) ) )
36 3 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → 𝑀 ∈ ℕ )
37 nnnn0addcl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 + 𝑘 ) ∈ ℕ )
38 36 23 37 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( 𝑀 + 𝑘 ) ∈ ℕ )
39 38 nnzd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( 𝑀 + 𝑘 ) ∈ ℤ )
40 1exp ⊢ ( ( 𝑀 + 𝑘 ) ∈ ℤ → ( 1 ↑ ( 𝑀 + 𝑘 ) ) = 1 )
41 39 40 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( 1 ↑ ( 𝑀 + 𝑘 ) ) = 1 )
42 0exp ⊢ ( ( 𝑀 + 𝑘 ) ∈ ℕ → ( 0 ↑ ( 𝑀 + 𝑘 ) ) = 0 )
43 38 42 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( 0 ↑ ( 𝑀 + 𝑘 ) ) = 0 )
44 41 43 oveq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 1 ↑ ( 𝑀 + 𝑘 ) ) − ( 0 ↑ ( 𝑀 + 𝑘 ) ) ) = ( 1 − 0 ) )
45 35 44 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 1 ↑ ( ( ( 𝑀 − 1 ) + 𝑘 ) + 1 ) ) − ( 0 ↑ ( ( ( 𝑀 − 1 ) + 𝑘 ) + 1 ) ) ) = ( 1 − 0 ) )
46 1m0e1 ⊢ ( 1 − 0 ) = 1
47 45 46 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 1 ↑ ( ( ( 𝑀 − 1 ) + 𝑘 ) + 1 ) ) − ( 0 ↑ ( ( ( 𝑀 − 1 ) + 𝑘 ) + 1 ) ) ) = 1 )
48 47 32 oveq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( ( 1 ↑ ( ( ( 𝑀 − 1 ) + 𝑘 ) + 1 ) ) − ( 0 ↑ ( ( ( 𝑀 − 1 ) + 𝑘 ) + 1 ) ) ) / ( ( ( 𝑀 − 1 ) + 𝑘 ) + 1 ) ) = ( 1 / ( 𝑀 + 𝑘 ) ) )
49 25 48 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ∫ ( 0 [,] 1 ) ( 𝑥 ↑ ( ( 𝑀 − 1 ) + 𝑘 ) ) d 𝑥 = ( 1 / ( 𝑀 + 𝑘 ) ) )
50 49 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ∫ ( 0 [,] 1 ) ( 𝑥 ↑ ( ( 𝑀 − 1 ) + 𝑘 ) ) d 𝑥 ) = ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( 1 / ( 𝑀 + 𝑘 ) ) ) )
51 50 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ∫ ( 0 [,] 1 ) ( 𝑥 ↑ ( ( 𝑀 − 1 ) + 𝑘 ) ) d 𝑥 ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( 1 / ( 𝑀 + 𝑘 ) ) ) )
52 5 17 51 3eqtr2d ⊢ ( 𝜑 → 𝐹 = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( 1 / ( 𝑀 + 𝑘 ) ) ) )