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 ⁢ ( N M) ∥ 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 ⊢ φ → ( N M) ∈ ℕ
13 12 nncnd ⊢ φ → ( N M) ∈ ℂ
14 10 13 mulcld ⊢ φ → M ⁢ ( N M) ∈ ℂ
15 1 nnne0d ⊢ φ → M ≠ 0
16 12 nnne0d ⊢ φ → ( N M) ≠ 0
17 10 13 15 16 mulne0d ⊢ φ → M ⁢ ( N M) ≠ 0
18 9 14 17 divrecd ⊢ φ → lcm _ ⁡ 1 … N M ⁢ ( N M) = lcm _ ⁡ 1 … N ⁢ 1 M ⁢ ( N M)
19 eqid ⊢ ∫ 0 1 x M − 1 ⁢ 1 − x N − M dx = ∫ 0 1 x M − 1 ⁢ 1 − x N − M dx
20 19 1 2 3 lcmineqlem13 ⊢ φ → ∫ 0 1 x M − 1 ⁢ 1 − x N − M dx = 1 M ⁢ ( N M)
21 20 oveq2d ⊢ φ → lcm _ ⁡ 1 … N ⁢ ∫ 0 1 x M − 1 ⁢ 1 − x N − M dx = lcm _ ⁡ 1 … N ⁢ 1 M ⁢ ( N M)
22 19 2 1 3 lcmineqlem15 ⊢ φ → lcm _ ⁡ 1 … N ⁢ ∫ 0 1 x M − 1 ⁢ 1 − x N − M dx ∈ ℕ
23 21 22 eqeltrrd ⊢ φ → lcm _ ⁡ 1 … N ⁢ 1 M ⁢ ( N M) ∈ ℕ
24 18 23 eqeltrd ⊢ φ → lcm _ ⁡ 1 … N M ⁢ ( N M) ∈ ℕ
25 1 12 nnmulcld ⊢ φ → M ⁢ ( N M) ∈ ℕ
26 25 8 nndivdvdsd ⊢ φ → M ⁢ ( N M) ∥ lcm _ ⁡ 1 … N ↔ lcm _ ⁡ 1 … N M ⁢ ( N M) ∈ ℕ
27 24 26 mpbird ⊢ φ → M ⁢ ( N M) ∥ lcm _ ⁡ 1 … N