Theorem lcmineqlem22

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

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

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem22.1	$$⊢\phi \to N\in \mathbb{N}$$
2		lcmineqlem22.2	$$⊢\phi \to 4\le N$$
3		2re	$$⊢2\in ℝ$$
4	3	a1i	$$⊢\phi \to 2\in ℝ$$
5		2nn0	$$⊢2\in {\mathbb{N}}_0$$
6	5	a1i	$$⊢\phi \to 2\in {\mathbb{N}}_0$$
7	1	nnnn0d	$$⊢\phi \to N\in {\mathbb{N}}_0$$
8	6 7	nn0mulcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in {\mathbb{N}}_0$$
9		1nn0	$$⊢1\in {\mathbb{N}}_0$$
10	9	a1i	$$⊢\phi \to 1\in {\mathbb{N}}_0$$
11	8 10	nn0addcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\in {\mathbb{N}}_0$$
12	4 11	reexpcld	$$⊢\phi \to 2^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\in ℝ$$
13	8 6	nn0addcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\in {\mathbb{N}}_0$$
14	4 13	reexpcld	$$⊢\phi \to 2^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2}\in ℝ$$
15		fz1ssnn	$$⊢\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\subseteq \mathbb{N}$$
16		fzfi	$$⊢\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\in \mathrm{Fin}$$
17		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}$$
18	15 16 17	mp2an	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\in \mathbb{N}$$
19	18	a1i	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\in \mathbb{N}$$
20	19	nnred	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\in ℝ$$
21		1red	$$⊢\phi \to 1\in ℝ$$
22	1	nnred	$$⊢\phi \to N\in ℝ$$
23	4 22	remulcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ$$
24		1lt2	$$⊢1<2$$
25	24	a1i	$$⊢\phi \to 1<2$$
26	21 4 25	ltled	$$⊢\phi \to 1\le 2$$
27	21 4 23 26	leadd2dd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2$$
28		2z	$$⊢2\in \mathbb{Z}$$
29	28	a1i	$$⊢\phi \to 2\in \mathbb{Z}$$
30	1	nnzd	$$⊢\phi \to N\in \mathbb{Z}$$
31	29 30	zmulcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in \mathbb{Z}$$
32	31	peano2zd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\in \mathbb{Z}$$
33	31 29	zaddcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\in \mathbb{Z}$$
34	4 32 33 25	leexp2d	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\leftrightarrow 2^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\le 2^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2}\right)$$
35	27 34	mpbid	$$⊢\phi \to 2^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\le 2^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2}$$
36	1 2	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)$$
37	12 14 20 35 36	letrd	$$⊢\phi \to 2^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)$$
38		fz1ssnn	$$⊢\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\subseteq \mathbb{N}$$
39		fzfi	$$⊢\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\in \mathrm{Fin}$$
40		lcmfnncl	$$⊢\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\subseteq \mathbb{N}\wedge \left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\in \mathrm{Fin}\right)\to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\right)\in \mathbb{N}$$
41	38 39 40	mp2an	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\right)\in \mathbb{N}$$
42	41	a1i	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\right)\in \mathbb{N}$$
43	42	nnred	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\right)\in ℝ$$
44	19	nnzd	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\in \mathbb{Z}$$
45	44 33	jca	$$⊢\phi \to \left(\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\in \mathbb{Z}\wedge 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\in \mathbb{Z}\right)$$
46		dvdslcm	$$⊢\left(\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\in \mathbb{Z}\wedge 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\in \mathbb{Z}\right)\to \left(\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\parallel \left(\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\mathrm{lcm}\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\right)\wedge \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\parallel \left(\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\mathrm{lcm}\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\right)\right)$$
47	45 46	syl	$$⊢\phi \to \left(\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\parallel \left(\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\mathrm{lcm}\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\right)\wedge \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\parallel \left(\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\mathrm{lcm}\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\right)\right)$$
48	47	simpld	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\parallel \left(\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\mathrm{lcm}\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\right)$$
49		2nn	$$⊢2\in \mathbb{N}$$
50	49	a1i	$$⊢\phi \to 2\in \mathbb{N}$$
51	50 1	nnmulcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in \mathbb{N}$$
52	51 50	nnaddcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\in \mathbb{N}$$
53	52	lcmfunnnd	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2-1\right)\right)\mathrm{lcm}\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)$$
54	23	recnd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ$$
55	4	recnd	$$⊢\phi \to 2\in ℂ$$
56		1cnd	$$⊢\phi \to 1\in ℂ$$
57	54 55 56	addsubassd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2-1=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2-1$$
58		2m1e1	$$⊢2-1=1$$
59	58	oveq2i	$$⊢2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2-1=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1$$
60	57 59	eqtrdi	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2-1=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1$$
61	60	oveq2d	$$⊢\phi \to \left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2-1\right)=\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)$$
62	61	fveq2d	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2-1\right)\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)$$
63	62	oveq1d	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2-1\right)\right)\mathrm{lcm}\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\mathrm{lcm}\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)$$
64	53 63	eqtrd	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\mathrm{lcm}\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)$$
65	48 64	breqtrrd	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\parallel \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\right)$$
66	44 42	jca	$$⊢\phi \to \left(\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\in \mathbb{Z}\wedge \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\right)\in \mathbb{N}\right)$$
67		dvdsle	$$⊢\left(\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\in \mathbb{Z}\wedge \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\right)\in \mathbb{N}\right)\to \left(\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\parallel \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\right)\to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\right)\right)$$
68	66 67	syl	$$⊢\phi \to \left(\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\parallel \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\right)\to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\right)\right)$$
69	65 68	mpd	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+2\right)\right)$$
70	14 20 43 36 69	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>}+2\right)\right)$$
71	37 70	jca	$$⊢\phi \to \left(2^{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\wedge 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>}+2\right)\right)\right)$$