Theorem lcmineqlem21

Description: The lcm inequality lemma without base cases 7 and 8. (Contributed by metakunt, 12-May-2024)

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

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem21.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		lcmineqlem21.2	⊢ ( 𝜑 → 4 ≤ 𝑁 )
3		2nn0	⊢ 2 ∈ ℕ0
4	3	a1i	⊢ ( 𝜑 → 2 ∈ ℕ0 )
5	4	nn0red	⊢ ( 𝜑 → 2 ∈ ℝ )
6	1	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
7	4 6	nn0mulcld	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℕ0 )
8	7 4	nn0addcld	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) + 2 ) ∈ ℕ0 )
9	5 8	reexpcld	⊢ ( 𝜑 → ( 2 ↑ ( ( 2 · 𝑁 ) + 2 ) ) ∈ ℝ )
10	1	nnred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
11		2rp	⊢ 2 ∈ ℝ+
12	11	a1i	⊢ ( 𝜑 → 2 ∈ ℝ+ )
13		2z	⊢ 2 ∈ ℤ
14	13	a1i	⊢ ( 𝜑 → 2 ∈ ℤ )
15	1	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
16	14 15	zmulcld	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℤ )
17	12 16	rpexpcld	⊢ ( 𝜑 → ( 2 ↑ ( 2 · 𝑁 ) ) ∈ ℝ+ )
18	17	rpred	⊢ ( 𝜑 → ( 2 ↑ ( 2 · 𝑁 ) ) ∈ ℝ )
19	10 18	remulcld	⊢ ( 𝜑 → ( 𝑁 · ( 2 ↑ ( 2 · 𝑁 ) ) ) ∈ ℝ )
20		fz1ssnn	⊢ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ⊆ ℕ
21		fzfi	⊢ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ∈ Fin
22		lcmfnncl	⊢ ( ( ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ⊆ ℕ ∧ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ∈ Fin ) → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℕ )
23	20 21 22	mp2an	⊢ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℕ
24	23	a1i	⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℕ )
25	24	nnred	⊢ ( 𝜑 → ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) ∈ ℝ )
26		4re	⊢ 4 ∈ ℝ
27	26	a1i	⊢ ( 𝜑 → 4 ∈ ℝ )
28	27 10 17	lemul1d	⊢ ( 𝜑 → ( 4 ≤ 𝑁 ↔ ( 4 · ( 2 ↑ ( 2 · 𝑁 ) ) ) ≤ ( 𝑁 · ( 2 ↑ ( 2 · 𝑁 ) ) ) ) )
29	2 28	mpbid	⊢ ( 𝜑 → ( 4 · ( 2 ↑ ( 2 · 𝑁 ) ) ) ≤ ( 𝑁 · ( 2 ↑ ( 2 · 𝑁 ) ) ) )
30		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
31	30 4 7	expaddd	⊢ ( 𝜑 → ( 2 ↑ ( ( 2 · 𝑁 ) + 2 ) ) = ( ( 2 ↑ ( 2 · 𝑁 ) ) · ( 2 ↑ 2 ) ) )
32		sq2	⊢ ( 2 ↑ 2 ) = 4
33	32	oveq2i	⊢ ( ( 2 ↑ ( 2 · 𝑁 ) ) · ( 2 ↑ 2 ) ) = ( ( 2 ↑ ( 2 · 𝑁 ) ) · 4 )
34	31 33	eqtrdi	⊢ ( 𝜑 → ( 2 ↑ ( ( 2 · 𝑁 ) + 2 ) ) = ( ( 2 ↑ ( 2 · 𝑁 ) ) · 4 ) )
35	17	rpcnd	⊢ ( 𝜑 → ( 2 ↑ ( 2 · 𝑁 ) ) ∈ ℂ )
36	27	recnd	⊢ ( 𝜑 → 4 ∈ ℂ )
37	35 36	mulcomd	⊢ ( 𝜑 → ( ( 2 ↑ ( 2 · 𝑁 ) ) · 4 ) = ( 4 · ( 2 ↑ ( 2 · 𝑁 ) ) ) )
38	34 37	eqtrd	⊢ ( 𝜑 → ( 2 ↑ ( ( 2 · 𝑁 ) + 2 ) ) = ( 4 · ( 2 ↑ ( 2 · 𝑁 ) ) ) )
39	38	breq1d	⊢ ( 𝜑 → ( ( 2 ↑ ( ( 2 · 𝑁 ) + 2 ) ) ≤ ( 𝑁 · ( 2 ↑ ( 2 · 𝑁 ) ) ) ↔ ( 4 · ( 2 ↑ ( 2 · 𝑁 ) ) ) ≤ ( 𝑁 · ( 2 ↑ ( 2 · 𝑁 ) ) ) ) )
40	29 39	mpbird	⊢ ( 𝜑 → ( 2 ↑ ( ( 2 · 𝑁 ) + 2 ) ) ≤ ( 𝑁 · ( 2 ↑ ( 2 · 𝑁 ) ) ) )
41	1	lcmineqlem20	⊢ ( 𝜑 → ( 𝑁 · ( 2 ↑ ( 2 · 𝑁 ) ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) )
42	9 19 25 40 41	letrd	⊢ ( 𝜑 → ( 2 ↑ ( ( 2 · 𝑁 ) + 2 ) ) ≤ ( lcm ‘ ( 1 ... ( ( 2 · 𝑁 ) + 1 ) ) ) )