Metamath Proof Explorer

Theorem lcmineqlem16

Description: Technical divisibility lemma. (Contributed by metakunt, 12-May-2024)

Ref Expression
Hypotheses lcmineqlem16.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
lcmineqlem16.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
lcmineqlem16.3 ⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
Assertion lcmineqlem16 ( 𝜑 → ( 𝑀 · ( 𝑁 C 𝑀 ) ) ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 lcmineqlem16.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 lcmineqlem16.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 lcmineqlem16.3 ⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
4 fz1ssnn ⊢ ( 1 ... 𝑁 ) ⊆ ℕ
5 fzfi ⊢ ( 1 ... 𝑁 ) ∈ Fin
6 lcmfnncl ⊢ ( ( ( 1 ... 𝑁 ) ⊆ ℕ ∧ ( 1 ... 𝑁 ) ∈ Fin ) → ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℕ )
7 4 5 6 mp2an ⊢ ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℕ
8 7 a1i ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℕ )
9 8 nncnd ⊢ ( 𝜑 → ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℂ )
10 1 nncnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
11 1 nnnn0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
12 2 11 3 bccl2d ⊢ ( 𝜑 → ( 𝑁 C 𝑀 ) ∈ ℕ )
13 12 nncnd ⊢ ( 𝜑 → ( 𝑁 C 𝑀 ) ∈ ℂ )
14 10 13 mulcld ⊢ ( 𝜑 → ( 𝑀 · ( 𝑁 C 𝑀 ) ) ∈ ℂ )
15 1 nnne0d ⊢ ( 𝜑 → 𝑀 ≠ 0 )
16 12 nnne0d ⊢ ( 𝜑 → ( 𝑁 C 𝑀 ) ≠ 0 )
17 10 13 15 16 mulne0d ⊢ ( 𝜑 → ( 𝑀 · ( 𝑁 C 𝑀 ) ) ≠ 0 )
18 9 14 17 divrecd ⊢ ( 𝜑 → ( ( lcm ‘ ( 1 ... 𝑁 ) ) / ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) = ( ( lcm ‘ ( 1 ... 𝑁 ) ) · ( 1 / ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) ) )
19 eqid ⊢ ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥
20 19 1 2 3 lcmineqlem13 ⊢ ( 𝜑 → ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 = ( 1 / ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) )
21 20 oveq2d ⊢ ( 𝜑 → ( ( lcm ‘ ( 1 ... 𝑁 ) ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) = ( ( lcm ‘ ( 1 ... 𝑁 ) ) · ( 1 / ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) ) )
22 19 2 1 3 lcmineqlem15 ⊢ ( 𝜑 → ( ( lcm ‘ ( 1 ... 𝑁 ) ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) ∈ ℕ )
23 21 22 eqeltrrd ⊢ ( 𝜑 → ( ( lcm ‘ ( 1 ... 𝑁 ) ) · ( 1 / ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) ) ∈ ℕ )
24 18 23 eqeltrd ⊢ ( 𝜑 → ( ( lcm ‘ ( 1 ... 𝑁 ) ) / ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) ∈ ℕ )
25 1 12 nnmulcld ⊢ ( 𝜑 → ( 𝑀 · ( 𝑁 C 𝑀 ) ) ∈ ℕ )
26 25 8 nndivdvdsd ⊢ ( 𝜑 → ( ( 𝑀 · ( 𝑁 C 𝑀 ) ) ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) ↔ ( ( lcm ‘ ( 1 ... 𝑁 ) ) / ( 𝑀 · ( 𝑁 C 𝑀 ) ) ) ∈ ℕ ) )
27 24 26 mpbird ⊢ ( 𝜑 → ( 𝑀 · ( 𝑁 C 𝑀 ) ) ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) )