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 ... 𝑁 ) ) · 𝐹 ) ∈ ℕ ) |