Theorem 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 = S. ( 0 [,] 1 ) ( ( x ^ ( M - 1 ) ) x. ( ( 1 - x ) ^ ( N - M ) ) ) _d x
	lcmineqlem15.2	|- ( ph -> N e. NN )
	lcmineqlem15.3	|- ( ph -> M e. NN )
	lcmineqlem15.4	|- ( ph -> M <_ N )
Assertion	lcmineqlem15	|- ( ph -> ( ( _lcm ` ( 1 ... N ) ) x. F ) e. NN )

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem15.1	|- F = S. ( 0 [,] 1 ) ( ( x ^ ( M - 1 ) ) x. ( ( 1 - x ) ^ ( N - M ) ) ) _d x
2		lcmineqlem15.2	|- ( ph -> N e. NN )
3		lcmineqlem15.3	|- ( ph -> M e. NN )
4		lcmineqlem15.4	|- ( ph -> M <_ N )
5	1 2 3 4	lcmineqlem6	|- ( ph -> ( ( _lcm ` ( 1 ... N ) ) x. F ) e. ZZ )
6		fz1ssnn	|- ( 1 ... N ) C_ NN
7		fzfi	|- ( 1 ... N ) e. Fin
8		lcmfnncl	|- ( ( ( 1 ... N ) C_ NN /\ ( 1 ... N ) e. Fin ) -> ( _lcm ` ( 1 ... N ) ) e. NN )
9	6 7 8	mp2an	|- ( _lcm ` ( 1 ... N ) ) e. NN
10	9	a1i	|- ( ph -> ( _lcm ` ( 1 ... N ) ) e. NN )
11	10	nnred	|- ( ph -> ( _lcm ` ( 1 ... N ) ) e. RR )
12	1 3 2 4	lcmineqlem13	|- ( ph -> F = ( 1 / ( M x. ( N _C M ) ) ) )
13		1red	|- ( ph -> 1 e. RR )
14	3	nnnn0d	|- ( ph -> M e. NN0 )
15	2 14 4	bccl2d	|- ( ph -> ( N _C M ) e. NN )
16	3 15	nnmulcld	|- ( ph -> ( M x. ( N _C M ) ) e. NN )
17	16	nnred	|- ( ph -> ( M x. ( N _C M ) ) e. RR )
18	16	nnne0d	|- ( ph -> ( M x. ( N _C M ) ) =/= 0 )
19	13 17 18	redivcld	|- ( ph -> ( 1 / ( M x. ( N _C M ) ) ) e. RR )
20	12 19	eqeltrd	|- ( ph -> F e. RR )
21	10	nngt0d	|- ( ph -> 0 < ( _lcm ` ( 1 ... N ) ) )
22		nnrecgt0	|- ( ( M x. ( N _C M ) ) e. NN -> 0 < ( 1 / ( M x. ( N _C M ) ) ) )
23	16 22	syl	|- ( ph -> 0 < ( 1 / ( M x. ( N _C M ) ) ) )
24	23 12	breqtrrd	|- ( ph -> 0 < F )
25	11 20 21 24	mulgt0d	|- ( ph -> 0 < ( ( _lcm ` ( 1 ... N ) ) x. F ) )
26		elnnz	|- ( ( ( _lcm ` ( 1 ... N ) ) x. F ) e. NN <-> ( ( ( _lcm ` ( 1 ... N ) ) x. F ) e. ZZ /\ 0 < ( ( _lcm ` ( 1 ... N ) ) x. F ) ) )
27	5 25 26	sylanbrc	|- ( ph -> ( ( _lcm ` ( 1 ... N ) ) x. F ) e. NN )