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 ⊢ F = ∫ 0 1 x M − 1 ⁢ 1 − x N − M dx
lcmineqlem3.2 ⊢ φ → N ∈ ℕ
lcmineqlem3.3 ⊢ φ → M ∈ ℕ
lcmineqlem3.4 ⊢ φ → M ≤ N
Assertion lcmineqlem3 ⊢ φ → F = ∑ k = 0 N − M − 1 k ⁢ ( N − M k) ⁢ 1 M + k

Proof

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