Theorem lcmineqlem20

Description: Inequality for lcm lemma. (Contributed by metakunt, 12-May-2024)

	Ref	Expression
Hypothesis	lcmineqlem20.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion	lcmineqlem20	⊢ ( 𝜑 → ( 𝑁 · ( 2 ↑ ( 2 · 𝑁 ) ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem20.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2	1	nnred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
3		2nn0	⊢ 2 ∈ ℕ0
4	3	a1i	⊢ ( 𝜑 → 2 ∈ ℕ0 )
5	1	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
6	4 5	nn0mulcld	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℕ0 )
7		2re	⊢ 2 ∈ ℝ
8		reexpcl	⊢ ( ( 2 ∈ ℝ ∧ ( 2 · 𝑁 ) ∈ ℕ0 ) → ( 2 ↑ ( 2 · 𝑁 ) ) ∈ ℝ )
9	7 8	mpan	⊢ ( ( 2 · 𝑁 ) ∈ ℕ0 → ( 2 ↑ ( 2 · 𝑁 ) ) ∈ ℝ )
10	6 9	syl	⊢ ( 𝜑 → ( 2 ↑ ( 2 · 𝑁 ) ) ∈ ℝ )
11	2 10	remulcld	⊢ ( 𝜑 → ( 𝑁 · ( 2 ↑ ( 2 · 𝑁 ) ) ) ∈ ℝ )
12	7	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
13	12 2	remulcld	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
14		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
15	13 14	readdcld	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 1 ) ∈ ℝ )
16		2nn	⊢ 2 ∈ ℕ
17	16	a1i	⊢ ( 𝜑 → 2 ∈ ℕ )
18	17 1	nnmulcld	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℕ )
19	5	nn0ge0d	⊢ ( 𝜑 → 0 ≤ 𝑁 )
20	17	nnge1d	⊢ ( 𝜑 → 1 ≤ 2 )
21	2 12 19 20	lemulge12d	⊢ ( 𝜑 → 𝑁 ≤ ( 2 · 𝑁 ) )
22	18 5 21	bccl2d	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ )
23	22	nnred	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℝ )
24	15 23	remulcld	⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) + 1 ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℝ )
25	2 24	remulcld	⊢ ( 𝜑 → ( 𝑁 · ( ( ( 2 · 𝑁 ) + 1 ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ∈ ℝ )
26		fz1ssnn	⊢ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ⊆ ℕ
27		fzfi	⊢ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ∈ Fin
28		lcmfnncl	⊢ ( ( ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ⊆ ℕ ∧ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ∈ Fin ) → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℕ )
29	26 27 28	mp2an	⊢ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℕ
30	29	a1i	⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℕ )
31	30	nnred	⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℝ )
32	5	lcmineqlem17	⊢ ( 𝜑 → ( 2 ↑ ( 2 · 𝑁 ) ) ≤ ( ( ( 2 · 𝑁 ) + 1 ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) )
33	1	nnrpd	⊢ ( 𝜑 → 𝑁 ∈ ℝ+ )
34	10 24 33	lemul2d	⊢ ( 𝜑 → ( ( 2 ↑ ( 2 · 𝑁 ) ) ≤ ( ( ( 2 · 𝑁 ) + 1 ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ↔ ( 𝑁 · ( 2 ↑ ( 2 · 𝑁 ) ) ) ≤ ( 𝑁 · ( ( ( 2 · 𝑁 ) + 1 ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ) )
35	32 34	mpbid	⊢ ( 𝜑 → ( 𝑁 · ( 2 ↑ ( 2 · 𝑁 ) ) ) ≤ ( 𝑁 · ( ( ( 2 · 𝑁 ) + 1 ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ) )
36	2	recnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
37	15	recnd	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 1 ) ∈ ℂ )
38	23	recnd	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℂ )
39	36 37 38	mulassd	⊢ ( 𝜑 → ( ( 𝑁 · ( ( 2 · 𝑁 ) + 1 ) ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) = ( 𝑁 · ( ( ( 2 · 𝑁 ) + 1 ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ) )
40	1	lcmineqlem19	⊢ ( 𝜑 → ( ( 𝑁 · ( ( 2 · 𝑁 ) + 1 ) ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ∥ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) )
41	18	peano2nnd	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 1 ) ∈ ℕ )
42	1 41	nnmulcld	⊢ ( 𝜑 → ( 𝑁 · ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℕ )
43	42 22	nnmulcld	⊢ ( 𝜑 → ( ( 𝑁 · ( ( 2 · 𝑁 ) + 1 ) ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ )
44	43	nnzd	⊢ ( 𝜑 → ( ( 𝑁 · ( ( 2 · 𝑁 ) + 1 ) ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℤ )
45		dvdsle	⊢ ( ( ( ( 𝑁 · ( ( 2 · 𝑁 ) + 1 ) ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℤ ∧ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℕ ) → ( ( ( 𝑁 · ( ( 2 · 𝑁 ) + 1 ) ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ∥ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) → ( ( 𝑁 · ( ( 2 · 𝑁 ) + 1 ) ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ) )
46	44 30 45	syl2anc	⊢ ( 𝜑 → ( ( ( 𝑁 · ( ( 2 · 𝑁 ) + 1 ) ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ∥ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) → ( ( 𝑁 · ( ( 2 · 𝑁 ) + 1 ) ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ) )
47	40 46	mpd	⊢ ( 𝜑 → ( ( 𝑁 · ( ( 2 · 𝑁 ) + 1 ) ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) )
48	39 47	eqbrtrrd	⊢ ( 𝜑 → ( 𝑁 · ( ( ( 2 · 𝑁 ) + 1 ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) )
49	11 25 31 35 48	letrd	⊢ ( 𝜑 → ( 𝑁 · ( 2 ↑ ( 2 · 𝑁 ) ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) )