Metamath Proof Explorer

Theorem lcmineqlem16

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

Ref Expression
Hypotheses lcmineqlem16.1 ⊢φ→M∈ℕ
lcmineqlem16.2 ⊢φ→N∈ℕ
lcmineqlem16.3 ⊢φ→M≤N
Assertion lcmineqlem16 ⊢φ→M⁢(NM)∥lcm_⁡1…N

Proof

Step Hyp Ref Expression
1 lcmineqlem16.1 ⊢φ→M∈ℕ
2 lcmineqlem16.2 ⊢φ→N∈ℕ
3 lcmineqlem16.3 ⊢φ→M≤N
4 fz1ssnn ⊢1…N⊆ℕ
5 fzfi ⊢1…N∈Fin
6 lcmfnncl ⊢1…N⊆ℕ∧1…N∈Fin→lcm_⁡1…N∈ℕ
7 4 5 6 mp2an ⊢lcm_⁡1…N∈ℕ
8 7 a1i ⊢φ→lcm_⁡1…N∈ℕ
9 8 nncnd ⊢φ→lcm_⁡1…N∈ℂ
10 1 nncnd ⊢φ→M∈ℂ
11 1 nnnn0d ⊢φ→M∈ℕ0
12 2 11 3 bccl2d ⊢φ→(NM)∈ℕ
13 12 nncnd ⊢φ→(NM)∈ℂ
14 10 13 mulcld ⊢φ→M⁢(NM)∈ℂ
15 1 nnne0d ⊢φ→M≠0
16 12 nnne0d ⊢φ→(NM)≠0
17 10 13 15 16 mulne0d ⊢φ→M⁢(NM)≠0
18 9 14 17 divrecd ⊢φ→lcm_⁡1…NM⁢(NM)=lcm_⁡1…N⁢1M⁢(NM)
19 eqid ⊢∫01xM−1⁢1−xN−Mdx=∫01xM−1⁢1−xN−Mdx
20 19 1 2 3 lcmineqlem13 ⊢φ→∫01xM−1⁢1−xN−Mdx=1M⁢(NM)
21 20 oveq2d ⊢φ→lcm_⁡1…N⁢∫01xM−1⁢1−xN−Mdx=lcm_⁡1…N⁢1M⁢(NM)
22 19 2 1 3 lcmineqlem15 ⊢φ→lcm_⁡1…N⁢∫01xM−1⁢1−xN−Mdx∈ℕ
23 21 22 eqeltrrd ⊢φ→lcm_⁡1…N⁢1M⁢(NM)∈ℕ
24 18 23 eqeltrd ⊢φ→lcm_⁡1…NM⁢(NM)∈ℕ
25 1 12 nnmulcld ⊢φ→M⁢(NM)∈ℕ
26 25 8 nndivdvdsd ⊢φ→M⁢(NM)∥lcm_⁡1…N↔lcm_⁡1…NM⁢(NM)∈ℕ
27 24 26 mpbird ⊢φ→M⁢(NM)∥lcm_⁡1…N