Theorem lcmineqlem2

Description: Part of lcm inequality lemma, this part eventually shows that F times the least common multiple of 1 to n is an integer. (Contributed by metakunt, 29-Apr-2024)

	Ref	Expression
Hypotheses	lcmineqlem2.1	⊢ 𝐹 = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥
	lcmineqlem2.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	lcmineqlem2.3	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	lcmineqlem2.4	⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
Assertion	lcmineqlem2	⊢ ( 𝜑 → 𝐹 = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( 𝑥 ↑ 𝑘 ) ) d 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem2.1	⊢ 𝐹 = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥
2		lcmineqlem2.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3		lcmineqlem2.3	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
4		lcmineqlem2.4	⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
5	1 2 3 4	lcmineqlem1	⊢ ( 𝜑 → 𝐹 = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( 𝑥 ↑ 𝑘 ) ) ) d 𝑥 )
6		eqid	⊢ ( 0 [,] 1 ) = ( 0 [,] 1 )
7		fzfid	⊢ ( 𝜑 → ( 0 ... ( 𝑁 − 𝑀 ) ) ∈ Fin )
8		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
9		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
10		unitsscn	⊢ ( 0 [,] 1 ) ⊆ ℂ
11		resmpt	⊢ ( ( 0 [,] 1 ) ⊆ ℂ → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ↾ ( 0 [,] 1 ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) )
12	10 11	ax-mp	⊢ ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ↾ ( 0 [,] 1 ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ↑ ( 𝑀 − 1 ) ) )
13		nnm1nn0	⊢ ( 𝑀 ∈ ℕ → ( 𝑀 − 1 ) ∈ ℕ0 )
14		expcncf	⊢ ( ( 𝑀 − 1 ) ∈ ℕ0 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
15	3 13 14	3syl	⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
16		rescncf	⊢ ( ( 0 [,] 1 ) ⊆ ℂ → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ∈ ( ℂ –cn→ ℂ ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ↾ ( 0 [,] 1 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) ) )
17	10 16	ax-mp	⊢ ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ∈ ( ℂ –cn→ ℂ ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ↾ ( 0 [,] 1 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
18	15 17	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ↾ ( 0 [,] 1 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
19	12 18	eqeltrrid	⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
20		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → 𝑘 ∈ ℕ0 )
21		neg1cn	⊢ - 1 ∈ ℂ
22		expcl	⊢ ( ( - 1 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( - 1 ↑ 𝑘 ) ∈ ℂ )
23	21 22	mpan	⊢ ( 𝑘 ∈ ℕ0 → ( - 1 ↑ 𝑘 ) ∈ ℂ )
24	20 23	syl	⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → ( - 1 ↑ 𝑘 ) ∈ ℂ )
25	24	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( - 1 ↑ 𝑘 ) ∈ ℂ )
26	3	nnnn0d	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
27	2	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
28		nn0sub	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝑁 − 𝑀 ) ∈ ℕ0 ) )
29	26 27 28	syl2anc	⊢ ( 𝜑 → ( 𝑀 ≤ 𝑁 ↔ ( 𝑁 − 𝑀 ) ∈ ℕ0 ) )
30	4 29	mpbid	⊢ ( 𝜑 → ( 𝑁 − 𝑀 ) ∈ ℕ0 )
31		nn0z	⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℤ )
32	20 31	syl	⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → 𝑘 ∈ ℤ )
33		bccl	⊢ ( ( ( 𝑁 − 𝑀 ) ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( ( 𝑁 − 𝑀 ) C 𝑘 ) ∈ ℕ0 )
34	32 33	sylan2	⊢ ( ( ( 𝑁 − 𝑀 ) ∈ ℕ0 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 𝑁 − 𝑀 ) C 𝑘 ) ∈ ℕ0 )
35	30 34	sylan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 𝑁 − 𝑀 ) C 𝑘 ) ∈ ℕ0 )
36	35	nn0cnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 𝑁 − 𝑀 ) C 𝑘 ) ∈ ℂ )
37	25 36	mulcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) ∈ ℂ )
38		resmpt	⊢ ( ( 0 [,] 1 ) ⊆ ℂ → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ↾ ( 0 [,] 1 ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ↑ 𝑘 ) ) )
39	10 38	ax-mp	⊢ ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ↾ ( 0 [,] 1 ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ↑ 𝑘 ) )
40		expcncf	⊢ ( 𝑘 ∈ ℕ0 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( ℂ –cn→ ℂ ) )
41	20 40	syl	⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( ℂ –cn→ ℂ ) )
42		rescncf	⊢ ( ( 0 [,] 1 ) ⊆ ℂ → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( ℂ –cn→ ℂ ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ↾ ( 0 [,] 1 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) ) )
43	10 42	ax-mp	⊢ ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( ℂ –cn→ ℂ ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ↾ ( 0 [,] 1 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
44	41 43	syl	⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ↾ ( 0 [,] 1 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
45	39 44	eqeltrrid	⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
46	45	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
47	6 7 8 9 19 37 46	3factsumint	⊢ ( 𝜑 → ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ( 𝑥 ↑ 𝑘 ) ) ) d 𝑥 = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( 𝑥 ↑ 𝑘 ) ) d 𝑥 ) )
48	5 47	eqtrd	⊢ ( 𝜑 → 𝐹 = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 𝑀 ) C 𝑘 ) ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( 𝑥 ↑ 𝑘 ) ) d 𝑥 ) )