Metamath Proof Explorer

Theorem lcmineqlem6

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, 10-May-2024)

Ref Expression
Hypotheses lcmineqlem6.1 ⊢ 𝐹 = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥
lcmineqlem6.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
lcmineqlem6.3 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
lcmineqlem6.4 ⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
Assertion lcmineqlem6 ( 𝜑 → ( ( lcm ‘ ( 1 ... 𝑁 ) ) · 𝐹 ) ∈ ℤ )

Proof

Step Hyp Ref Expression
1 lcmineqlem6.1 ⊢ 𝐹 = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥
2 lcmineqlem6.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 lcmineqlem6.3 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
4 lcmineqlem6.4 ⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
5 1 2 3 4 lcmineqlem3 ⊢ ( 𝜑 → 𝐹 = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( 1 / ( 𝑀 + 𝑘 ) ) ) )
6 5 oveq2d ⊢ ( 𝜑 → ( ( lcm ‘ ( 1 ... 𝑁 ) ) · 𝐹 ) = ( ( lcm ‘ ( 1 ... 𝑁 ) ) · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( 1 / ( 𝑀 + 𝑘 ) ) ) ) )
7 fzfid ⊢ ( 𝜑 → ( 0 ... ( 𝑁 − 𝑀 ) ) ∈ Fin )
8 fz1ssnn ⊢ ( 1 ... 𝑁 ) ⊆ ℕ
9 fzfi ⊢ ( 1 ... 𝑁 ) ∈ Fin
10 8 9 pm3.2i ⊢ ( ( 1 ... 𝑁 ) ⊆ ℕ ∧ ( 1 ... 𝑁 ) ∈ Fin )
11 lcmfnncl ⊢ ( ( ( 1 ... 𝑁 ) ⊆ ℕ ∧ ( 1 ... 𝑁 ) ∈ Fin ) → ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℕ )
12 10 11 ax-mp ⊢ ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℕ
13 12 nncni ⊢ ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℂ
14 13 a1i ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℂ )
15 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → 𝑘 ∈ ℤ )
16 m1expcl ⊢ ( 𝑘 ∈ ℤ → ( - 1 ↑ 𝑘 ) ∈ ℤ )
17 15 16 syl ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → ( - 1 ↑ 𝑘 ) ∈ ℤ )
18 17 zcnd ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → ( - 1 ↑ 𝑘 ) ∈ ℂ )
19 18 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( - 1 ↑ 𝑘 ) ∈ ℂ )
20 bccl2 ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → ( ( 𝑁 − 𝑀 ) C 𝑘 ) ∈ ℕ )
21 20 nncnd ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → ( ( 𝑁 − 𝑀 ) C 𝑘 ) ∈ ℂ )
22 21 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 𝑁 − 𝑀 ) C 𝑘 ) ∈ ℂ )
23 19 22 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) ∈ ℂ )
24 3 nncnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
25 24 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → 𝑀 ∈ ℂ )
26 15 zcnd ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → 𝑘 ∈ ℂ )
27 26 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → 𝑘 ∈ ℂ )
28 25 27 addcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( 𝑀 + 𝑘 ) ∈ ℂ )
29 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → 𝑘 ∈ ℕ0 )
30 nnnn0addcl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 + 𝑘 ) ∈ ℕ )
31 29 30 sylan2 ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( 𝑀 + 𝑘 ) ∈ ℕ )
32 3 31 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( 𝑀 + 𝑘 ) ∈ ℕ )
33 32 nnne0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( 𝑀 + 𝑘 ) ≠ 0 )
34 28 33 reccld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( 1 / ( 𝑀 + 𝑘 ) ) ∈ ℂ )
35 23 34 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( 1 / ( 𝑀 + 𝑘 ) ) ) ∈ ℂ )
36 7 14 35 fsummulc2 ⊢ ( 𝜑 → ( ( lcm ‘ ( 1 ... 𝑁 ) ) · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( 1 / ( 𝑀 + 𝑘 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( lcm ‘ ( 1 ... 𝑁 ) ) · ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( 1 / ( 𝑀 + 𝑘 ) ) ) ) )
37 6 36 eqtrd ⊢ ( 𝜑 → ( ( lcm ‘ ( 1 ... 𝑁 ) ) · 𝐹 ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( lcm ‘ ( 1 ... 𝑁 ) ) · ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( 1 / ( 𝑀 + 𝑘 ) ) ) ) )
38 13 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℂ )
39 38 23 28 33 lcmineqlem5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( lcm ‘ ( 1 ... 𝑁 ) ) · ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( 1 / ( 𝑀 + 𝑘 ) ) ) ) = ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( ( lcm ‘ ( 1 ... 𝑁 ) ) / ( 𝑀 + 𝑘 ) ) ) )
40 39 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( lcm ‘ ( 1 ... 𝑁 ) ) · ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( 1 / ( 𝑀 + 𝑘 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( ( lcm ‘ ( 1 ... 𝑁 ) ) / ( 𝑀 + 𝑘 ) ) ) )
41 37 40 eqtrd ⊢ ( 𝜑 → ( ( lcm ‘ ( 1 ... 𝑁 ) ) · 𝐹 ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( ( lcm ‘ ( 1 ... 𝑁 ) ) / ( 𝑀 + 𝑘 ) ) ) )
42 17 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( - 1 ↑ 𝑘 ) ∈ ℤ )
43 20 nnzd ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → ( ( 𝑁 − 𝑀 ) C 𝑘 ) ∈ ℤ )
44 43 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 𝑁 − 𝑀 ) C 𝑘 ) ∈ ℤ )
45 42 44 zmulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) ∈ ℤ )
46 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → 𝑁 ∈ ℕ )
47 3 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → 𝑀 ∈ ℕ )
48 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → 𝑀 ≤ 𝑁 )
49 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) )
50 46 47 48 49 lcmineqlem4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( lcm ‘ ( 1 ... 𝑁 ) ) / ( 𝑀 + 𝑘 ) ) ∈ ℤ )
51 45 50 zmulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( ( lcm ‘ ( 1 ... 𝑁 ) ) / ( 𝑀 + 𝑘 ) ) ) ∈ ℤ )
52 7 51 fsumzcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( ( lcm ‘ ( 1 ... 𝑁 ) ) / ( 𝑀 + 𝑘 ) ) ) ∈ ℤ )
53 41 52 eqeltrd ⊢ ( 𝜑 → ( ( lcm ‘ ( 1 ... 𝑁 ) ) · 𝐹 ) ∈ ℤ )