Metamath Proof Explorer


Theorem lcmineqlem15

Description: F times the least common multiple of 1 to n is a natural number. (Contributed by metakunt, 10-May-2024)

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

Proof

Step Hyp Ref Expression
1 lcmineqlem15.1 𝐹 = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁𝑀 ) ) ) d 𝑥
2 lcmineqlem15.2 ( 𝜑𝑁 ∈ ℕ )
3 lcmineqlem15.3 ( 𝜑𝑀 ∈ ℕ )
4 lcmineqlem15.4 ( 𝜑𝑀𝑁 )
5 1 2 3 4 lcmineqlem6 ( 𝜑 → ( ( lcm ‘ ( 1 ... 𝑁 ) ) · 𝐹 ) ∈ ℤ )
6 fz1ssnn ( 1 ... 𝑁 ) ⊆ ℕ
7 fzfi ( 1 ... 𝑁 ) ∈ Fin
8 lcmfnncl ( ( ( 1 ... 𝑁 ) ⊆ ℕ ∧ ( 1 ... 𝑁 ) ∈ Fin ) → ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℕ )
9 6 7 8 mp2an ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℕ
10 9 a1i ( 𝜑 → ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℕ )
11 10 nnred ( 𝜑 → ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℝ )
12 1 3 2 4 lcmineqlem13 ( 𝜑𝐹 = ( 1 / ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) )
13 1red ( 𝜑 → 1 ∈ ℝ )
14 3 nnnn0d ( 𝜑𝑀 ∈ ℕ0 )
15 2 14 4 bccl2d ( 𝜑 → ( 𝑁 C 𝑀 ) ∈ ℕ )
16 3 15 nnmulcld ( 𝜑 → ( 𝑀 · ( 𝑁 C 𝑀 ) ) ∈ ℕ )
17 16 nnred ( 𝜑 → ( 𝑀 · ( 𝑁 C 𝑀 ) ) ∈ ℝ )
18 16 nnne0d ( 𝜑 → ( 𝑀 · ( 𝑁 C 𝑀 ) ) ≠ 0 )
19 13 17 18 redivcld ( 𝜑 → ( 1 / ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) ∈ ℝ )
20 12 19 eqeltrd ( 𝜑𝐹 ∈ ℝ )
21 10 nngt0d ( 𝜑 → 0 < ( lcm ‘ ( 1 ... 𝑁 ) ) )
22 nnrecgt0 ( ( 𝑀 · ( 𝑁 C 𝑀 ) ) ∈ ℕ → 0 < ( 1 / ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) )
23 16 22 syl ( 𝜑 → 0 < ( 1 / ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) )
24 23 12 breqtrrd ( 𝜑 → 0 < 𝐹 )
25 11 20 21 24 mulgt0d ( 𝜑 → 0 < ( ( lcm ‘ ( 1 ... 𝑁 ) ) · 𝐹 ) )
26 elnnz ( ( ( lcm ‘ ( 1 ... 𝑁 ) ) · 𝐹 ) ∈ ℕ ↔ ( ( ( lcm ‘ ( 1 ... 𝑁 ) ) · 𝐹 ) ∈ ℤ ∧ 0 < ( ( lcm ‘ ( 1 ... 𝑁 ) ) · 𝐹 ) ) )
27 5 25 26 sylanbrc ( 𝜑 → ( ( lcm ‘ ( 1 ... 𝑁 ) ) · 𝐹 ) ∈ ℕ )