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