Metamath Proof Explorer

Theorem lcmineqlem2

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

Proof

Step Hyp Ref Expression
1 lcmineqlem2.1 ⊢ 𝐹 = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥
2 lcmineqlem2.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 lcmineqlem2.3 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
4 lcmineqlem2.4 ⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
5 1 2 3 4 lcmineqlem1 ⊢ ( 𝜑 → 𝐹 = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( 𝑥 ↑ 𝑘 ) ) ) d 𝑥 )
6 eqid ⊢ ( 0 [,] 1 ) = ( 0 [,] 1 )
7 fzfid ⊢ ( 𝜑 → ( 0 ... ( 𝑁 − 𝑀 ) ) ∈ Fin )
8 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
9 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
10 unitsscn ⊢ ( 0 [,] 1 ) ⊆ ℂ
11 resmpt ⊢ ( ( 0 [,] 1 ) ⊆ ℂ → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ↾ ( 0 [,] 1 ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) )
12 10 11 ax-mp ⊢ ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ↾ ( 0 [,] 1 ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ↑ ( 𝑀 − 1 ) ) )
13 nnm1nn0 ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 − 1 ) ∈ ℕ0 )
14 expcncf ⊢ ( ( 𝑀 − 1 ) ∈ ℕ0 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
15 rescncf ⊢ ( ( 0 [,] 1 ) ⊆ ℂ → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ∈ ( ℂ –cn→ ℂ ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ↾ ( 0 [,] 1 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) ) )
16 10 15 ax-mp ⊢ ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ∈ ( ℂ –cn→ ℂ ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ↾ ( 0 [,] 1 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
17 3 13 14 16 4syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ↾ ( 0 [,] 1 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
18 12 17 eqeltrrid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
19 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → 𝑘 ∈ ℕ0 )
20 neg1cn ⊢ - 1 ∈ ℂ
21 expcl ⊢ ( ( - 1 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( - 1 ↑ 𝑘 ) ∈ ℂ )
22 20 21 mpan ⊢ ( 𝑘 ∈ ℕ0 → ( - 1 ↑ 𝑘 ) ∈ ℂ )
23 19 22 syl ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → ( - 1 ↑ 𝑘 ) ∈ ℂ )
24 23 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( - 1 ↑ 𝑘 ) ∈ ℂ )
25 3 nnnn0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
26 2 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
27 nn0sub ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝑁 − 𝑀 ) ∈ ℕ0 ) )
28 25 26 27 syl2anc ⊢ ( 𝜑 → ( 𝑀 ≤ 𝑁 ↔ ( 𝑁 − 𝑀 ) ∈ ℕ0 ) )
29 4 28 mpbid ⊢ ( 𝜑 → ( 𝑁 − 𝑀 ) ∈ ℕ0 )
30 nn0z ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℤ )
31 19 30 syl ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → 𝑘 ∈ ℤ )
32 bccl ⊢ ( ( ( 𝑁 − 𝑀 ) ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( ( 𝑁 − 𝑀 ) C 𝑘 ) ∈ ℕ0 )
33 31 32 sylan2 ⊢ ( ( ( 𝑁 − 𝑀 ) ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 𝑁 − 𝑀 ) C 𝑘 ) ∈ ℕ0 )
34 29 33 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 𝑁 − 𝑀 ) C 𝑘 ) ∈ ℕ0 )
35 34 nn0cnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 𝑁 − 𝑀 ) C 𝑘 ) ∈ ℂ )
36 24 35 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) ∈ ℂ )
37 resmpt ⊢ ( ( 0 [,] 1 ) ⊆ ℂ → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ↾ ( 0 [,] 1 ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ↑ 𝑘 ) ) )
38 10 37 ax-mp ⊢ ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ↾ ( 0 [,] 1 ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ↑ 𝑘 ) )
39 expcncf ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( ℂ –cn→ ℂ ) )
40 19 39 syl ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( ℂ –cn→ ℂ ) )
41 rescncf ⊢ ( ( 0 [,] 1 ) ⊆ ℂ → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( ℂ –cn→ ℂ ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ↾ ( 0 [,] 1 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) ) )
42 10 41 ax-mp ⊢ ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( ℂ –cn→ ℂ ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ↾ ( 0 [,] 1 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
43 40 42 syl ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ↾ ( 0 [,] 1 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
44 38 43 eqeltrrid ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
45 44 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
46 6 7 8 9 18 36 45 3factsumint ⊢ ( 𝜑 → ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( 𝑥 ↑ 𝑘 ) ) ) d 𝑥 = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( 𝑥 ↑ 𝑘 ) ) d 𝑥 ) )
47 5 46 eqtrd ⊢ ( 𝜑 → 𝐹 = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( 𝑥 ↑ 𝑘 ) ) d 𝑥 ) )