Theorem lcmineqlem21

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

	Ref	Expression
Hypotheses	lcmineqlem21.1	$$⊢\phi \to N\in \mathbb{N}$$
	lcmineqlem21.2	$$⊢\phi \to 4\le N$$
Assertion	lcmineqlem21	$$⊢\phi \to 2^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2}\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem21.1	$$⊢\phi \to N\in \mathbb{N}$$
2		lcmineqlem21.2	$$⊢\phi \to 4\le N$$
3		2nn0	$$⊢2\in {\mathbb{N}}_0$$
4	3	a1i	$$⊢\phi \to 2\in {\mathbb{N}}_0$$
5	4	nn0red	$$⊢\phi \to 2\in ℝ$$
6	1	nnnn0d	$$⊢\phi \to N\in {\mathbb{N}}_0$$
7	4 6	nn0mulcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in {\mathbb{N}}_0$$
8	7 4	nn0addcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\in {\mathbb{N}}_0$$
9	5 8	reexpcld	$$⊢\phi \to 2^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2}\in ℝ$$
10	1	nnred	$$⊢\phi \to N\in ℝ$$
11		2rp	$$⊢2\in {ℝ}^{+}$$
12	11	a1i	$$⊢\phi \to 2\in {ℝ}^{+}$$
13		2z	$$⊢2\in \mathbb{Z}$$
14	13	a1i	$$⊢\phi \to 2\in \mathbb{Z}$$
15	1	nnzd	$$⊢\phi \to N\in \mathbb{Z}$$
16	14 15	zmulcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in \mathbb{Z}$$
17	12 16	rpexpcld	$$⊢\phi \to 2^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\in {ℝ}^{+}$$
18	17	rpred	$$⊢\phi \to 2^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\in ℝ$$
19	10 18	remulcld	$$⊢\phi \to N{2}^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\in ℝ$$
20		fz1ssnn	$$⊢\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\subseteq \mathbb{N}$$
21		fzfi	$$⊢\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\in \mathrm{Fin}$$
22		lcmfnncl	$$⊢\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\subseteq \mathbb{N}\wedge \left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\in \mathrm{Fin}\right)\to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\in \mathbb{N}$$
23	20 21 22	mp2an	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\in \mathbb{N}$$
24	23	a1i	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\in \mathbb{N}$$
25	24	nnred	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\in ℝ$$
26		4re	$$⊢4\in ℝ$$
27	26	a1i	$$⊢\phi \to 4\in ℝ$$
28	27 10 17	lemul1d	$$⊢\phi \to \left(4\le N\leftrightarrow 42^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\le N{2}^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\right)$$
29	2 28	mpbid	$$⊢\phi \to 42^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\le N{2}^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}$$
30		2cnd	$$⊢\phi \to 2\in ℂ$$
31	30 4 7	expaddd	$$⊢\phi \to 2^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2}=2^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{2}^2$$
32		sq2	$$⊢2^2=4$$
33	32	oveq2i	$$⊢2^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{2}^2=2^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\cdot 4$$
34	31 33	eqtrdi	$$⊢\phi \to 2^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2}=2^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\cdot 4$$
35	17	rpcnd	$$⊢\phi \to 2^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\in ℂ$$
36	27	recnd	$$⊢\phi \to 4\in ℂ$$
37	35 36	mulcomd	$$⊢\phi \to 2^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\cdot 4=42^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}$$
38	34 37	eqtrd	$$⊢\phi \to 2^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2}=42^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}$$
39	38	breq1d	$$⊢\phi \to \left(2^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2}\le N{2}^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\leftrightarrow 42^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\le N{2}^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\right)$$
40	29 39	mpbird	$$⊢\phi \to 2^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2}\le N{2}^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}$$
41	1	lcmineqlem20	$$⊢\phi \to N{2}^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)$$
42	9 19 25 40 41	letrd	$$⊢\phi \to 2^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2}\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)$$