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	$⊢ F = \int_{[0, 1]} x^{M - 1} {(1 - x)}^{N - M} d x$
	lcmineqlem15.2	$⊢ φ \to N \in ℕ$
	lcmineqlem15.3	$⊢ φ \to M \in ℕ$
	lcmineqlem15.4	$⊢ φ \to M \leq N$
Assertion	lcmineqlem15	$⊢ φ \to \underline{lcm} ((1 \dots N)) F \in ℕ$

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem15.1	$⊢ F = \int_{[0, 1]} x^{M - 1} {(1 - x)}^{N - M} d x$
2		lcmineqlem15.2	$⊢ φ \to N \in ℕ$
3		lcmineqlem15.3	$⊢ φ \to M \in ℕ$
4		lcmineqlem15.4	$⊢ φ \to M \leq N$
5	1 2 3 4	lcmineqlem6	$⊢ φ \to \underline{lcm} ((1 \dots N)) F \in ℤ$
6		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
7		fzfi	$⊢ (1 \dots N) \in Fin$
8		lcmfnncl	$⊢ ((1 \dots N) \subseteq ℕ \land (1 \dots N) \in Fin) \to \underline{lcm} ((1 \dots N)) \in ℕ$
9	6 7 8	mp2an	$⊢ \underline{lcm} ((1 \dots N)) \in ℕ$
10	9	a1i	$⊢ φ \to \underline{lcm} ((1 \dots N)) \in ℕ$
11	10	nnred	$⊢ φ \to \underline{lcm} ((1 \dots N)) \in ℝ$
12	1 3 2 4	lcmineqlem13	$⊢ φ \to F = \frac{1}{M (\binom{N}{M})}$
13		1red	$⊢ φ \to 1 \in ℝ$
14	3	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
15	2 14 4	bccl2d	$⊢ φ \to (\binom{N}{M}) \in ℕ$
16	3 15	nnmulcld	$⊢ φ \to M (\binom{N}{M}) \in ℕ$
17	16	nnred	$⊢ φ \to M (\binom{N}{M}) \in ℝ$
18	16	nnne0d	$⊢ φ \to M (\binom{N}{M}) \neq 0$
19	13 17 18	redivcld	$⊢ φ \to \frac{1}{M (\binom{N}{M})} \in ℝ$
20	12 19	eqeltrd	$⊢ φ \to F \in ℝ$
21	10	nngt0d	$⊢ φ \to 0 < \underline{lcm} ((1 \dots N))$
22		nnrecgt0	$⊢ M (\binom{N}{M}) \in ℕ \to 0 < \frac{1}{M (\binom{N}{M})}$
23	16 22	syl	$⊢ φ \to 0 < \frac{1}{M (\binom{N}{M})}$
24	23 12	breqtrrd	$⊢ φ \to 0 < F$
25	11 20 21 24	mulgt0d	$⊢ φ \to 0 < \underline{lcm} ((1 \dots N)) F$
26		elnnz	$⊢ \underline{lcm} ((1 \dots N)) F \in ℕ \leftrightarrow (\underline{lcm} ((1 \dots N)) F \in ℤ \land 0 < \underline{lcm} ((1 \dots N)) F)$
27	5 25 26	sylanbrc	$⊢ φ \to \underline{lcm} ((1 \dots N)) F \in ℕ$

Metamath Proof Explorer

Theorem lcmineqlem15

Proof