Theorem lcmineqlem23

Description: Penultimate step to the lcm inequality lemma. (Contributed by metakunt, 12-May-2024)

	Ref	Expression
Hypotheses	lcmineqlem23.1	$$⊢\phi \to N\in \mathbb{N}$$
	lcmineqlem23.2	$$⊢\phi \to 9\le N$$
Assertion	lcmineqlem23	$$⊢\phi \to 2^N\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem23.1	$$⊢\phi \to N\in \mathbb{N}$$
2		lcmineqlem23.2	$$⊢\phi \to 9\le N$$
3		2nn	$$⊢2\in \mathbb{N}$$
4	3	a1i	$$⊢\phi \to 2\in \mathbb{N}$$
5	1 4	jca	$$⊢\phi \to \left(N\in \mathbb{N}\wedge 2\in \mathbb{N}\right)$$
6		nndivdvds	$$⊢\left(N\in \mathbb{N}\wedge 2\in \mathbb{N}\right)\to \left(2\parallel N\leftrightarrow \frac{N}{2}\in \mathbb{N}\right)$$
7	5 6	syl	$$⊢\phi \to \left(2\parallel N\leftrightarrow \frac{N}{2}\in \mathbb{N}\right)$$
8	7	biimpa	$$⊢\left(\phi \wedge 2\parallel N\right)\to \frac{N}{2}\in \mathbb{N}$$
9	8	nnzd	$$⊢\left(\phi \wedge 2\parallel N\right)\to \frac{N}{2}\in \mathbb{Z}$$
10		1zzd	$$⊢\left(\phi \wedge 2\parallel N\right)\to 1\in \mathbb{Z}$$
11	9 10	zsubcld	$$⊢\left(\phi \wedge 2\parallel N\right)\to \left(\frac{N}{2}\right)-1\in \mathbb{Z}$$
12		0red	$$⊢\left(\phi \wedge 2\parallel N\right)\to 0\in ℝ$$
13		4re	$$⊢4\in ℝ$$
14	13	a1i	$$⊢\left(\phi \wedge 2\parallel N\right)\to 4\in ℝ$$
15	8	nnred	$$⊢\left(\phi \wedge 2\parallel N\right)\to \frac{N}{2}\in ℝ$$
16		1red	$$⊢\left(\phi \wedge 2\parallel N\right)\to 1\in ℝ$$
17	15 16	resubcld	$$⊢\left(\phi \wedge 2\parallel N\right)\to \left(\frac{N}{2}\right)-1\in ℝ$$
18		4pos	$$⊢0<4$$
19	18	a1i	$$⊢\left(\phi \wedge 2\parallel N\right)\to 0<4$$
20		5m1e4	$$⊢5-1=4$$
21		5re	$$⊢5\in ℝ$$
22	21	a1i	$$⊢\left(\phi \wedge 2\parallel N\right)\to 5\in ℝ$$
23	3	nncni	$$⊢2\in ℂ$$
24		5cn	$$⊢5\in ℂ$$
25	23 24	mulcomi	$$⊢2\cdot 5=5\cdot 2$$
26		5t2e10	$$⊢5\cdot 2=10$$
27	25 26	eqtri	$$⊢2\cdot 5=10$$
28		10re	$$⊢10\in ℝ$$
29	28	recni	$$⊢10\in ℂ$$
30	3	nnne0i	$$⊢2\ne 0$$
31	29 23 24 30	divmuli	$$⊢\frac{10}{2}=5\leftrightarrow 2\cdot 5=10$$
32	27 31	mpbir	$$⊢\frac{10}{2}=5$$
33	28	a1i	$$⊢\left(\phi \wedge 2\parallel N\right)\to 10\in ℝ$$
34	1	nnred	$$⊢\phi \to N\in ℝ$$
35	34	adantr	$$⊢\left(\phi \wedge 2\parallel N\right)\to N\in ℝ$$
36		2rp	$$⊢2\in {ℝ}^{+}$$
37	36	a1i	$$⊢\left(\phi \wedge 2\parallel N\right)\to 2\in {ℝ}^{+}$$
38		9p1e10	$$⊢9+1=10$$
39		9re	$$⊢9\in ℝ$$
40	39	a1i	$$⊢\phi \to 9\in ℝ$$
41	40 34	leloed	$$⊢\phi \to \left(9\le N\leftrightarrow \left(9<N\vee 9=N\right)\right)$$
42	2 41	mpbid	$$⊢\phi \to \left(9<N\vee 9=N\right)$$
43	42	adantr	$$⊢\left(\phi \wedge 2\parallel N\right)\to \left(9<N\vee 9=N\right)$$
44		4cn	$$⊢4\in ℂ$$
45	23 44	mulcomi	$$⊢2\cdot 4=4\cdot 2$$
46		4t2e8	$$⊢4\cdot 2=8$$
47	45 46	eqtri	$$⊢2\cdot 4=8$$
48		8re	$$⊢8\in ℝ$$
49	48	recni	$$⊢8\in ℂ$$
50	49 23 44 30	divmuli	$$⊢\frac{8}{2}=4\leftrightarrow 2\cdot 4=8$$
51	47 50	mpbir	$$⊢\frac{8}{2}=4$$
52		4nn	$$⊢4\in \mathbb{N}$$
53	51 52	eqeltri	$$⊢\frac{8}{2}\in \mathbb{N}$$
54		8nn	$$⊢8\in \mathbb{N}$$
55		nndivdvds	$$⊢\left(8\in \mathbb{N}\wedge 2\in \mathbb{N}\right)\to \left(2\parallel 8\leftrightarrow \frac{8}{2}\in \mathbb{N}\right)$$
56	54 3 55	mp2an	$$⊢2\parallel 8\leftrightarrow \frac{8}{2}\in \mathbb{N}$$
57	53 56	mpbir	$$⊢2\parallel 8$$
58		9m1e8	$$⊢9-1=8$$
59	57 58	breqtrri	$$⊢2\parallel \left(9-1\right)$$
60		9nn	$$⊢9\in \mathbb{N}$$
61	60	nnzi	$$⊢9\in \mathbb{Z}$$
62		oddm1even	$$⊢9\in \mathbb{Z}\to \left(\neg 2\parallel 9\leftrightarrow 2\parallel \left(9-1\right)\right)$$
63	61 62	ax-mp	$$⊢\neg 2\parallel 9\leftrightarrow 2\parallel \left(9-1\right)$$
64	59 63	mpbir	$$⊢\neg 2\parallel 9$$
65		breq2	$$⊢9=N\to \left(2\parallel 9\leftrightarrow 2\parallel N\right)$$
66	64 65	mtbii	$$⊢9=N\to \neg 2\parallel N$$
67	66	con2i	$$⊢2\parallel N\to \neg 9=N$$
68	67	adantl	$$⊢\left(\phi \wedge 2\parallel N\right)\to \neg 9=N$$
69	43 68	olcnd	$$⊢\left(\phi \wedge 2\parallel N\right)\to 9<N$$
70	1	nnzd	$$⊢\phi \to N\in \mathbb{Z}$$
71		zltp1le	$$⊢\left(9\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(9<N\leftrightarrow 9+1\le N\right)$$
72	61 71	mpan	$$⊢N\in \mathbb{Z}\to \left(9<N\leftrightarrow 9+1\le N\right)$$
73	70 72	syl	$$⊢\phi \to \left(9<N\leftrightarrow 9+1\le N\right)$$
74	73	adantr	$$⊢\left(\phi \wedge 2\parallel N\right)\to \left(9<N\leftrightarrow 9+1\le N\right)$$
75	69 74	mpbid	$$⊢\left(\phi \wedge 2\parallel N\right)\to 9+1\le N$$
76	38 75	eqbrtrrid	$$⊢\left(\phi \wedge 2\parallel N\right)\to 10\le N$$
77	33 35 37 76	lediv1dd	$$⊢\left(\phi \wedge 2\parallel N\right)\to \frac{10}{2}\le \frac{N}{2}$$
78	32 77	eqbrtrrid	$$⊢\left(\phi \wedge 2\parallel N\right)\to 5\le \frac{N}{2}$$
79	22 15 16 78	lesub1dd	$$⊢\left(\phi \wedge 2\parallel N\right)\to 5-1\le \left(\frac{N}{2}\right)-1$$
80	20 79	eqbrtrrid	$$⊢\left(\phi \wedge 2\parallel N\right)\to 4\le \left(\frac{N}{2}\right)-1$$
81	12 14 17 19 80	ltletrd	$$⊢\left(\phi \wedge 2\parallel N\right)\to 0<\left(\frac{N}{2}\right)-1$$
82	11 81	jca	$$⊢\left(\phi \wedge 2\parallel N\right)\to \left(\left(\frac{N}{2}\right)-1\in \mathbb{Z}\wedge 0<\left(\frac{N}{2}\right)-1\right)$$
83		elnnz	$$⊢\left(\frac{N}{2}\right)-1\in \mathbb{N}\leftrightarrow \left(\left(\frac{N}{2}\right)-1\in \mathbb{Z}\wedge 0<\left(\frac{N}{2}\right)-1\right)$$
84	82 83	sylibr	$$⊢\left(\phi \wedge 2\parallel N\right)\to \left(\frac{N}{2}\right)-1\in \mathbb{N}$$
85	84 80	lcmineqlem22	$$⊢\left(\phi \wedge 2\parallel N\right)\to \left(2^{2\left(\left(\frac{N}{2}\right)-1\right)+1}\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\left(\left(\frac{N}{2}\right)-1\right)+1\right)\right)\wedge 2^{2\left(\left(\frac{N}{2}\right)-1\right)+2}\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\left(\left(\frac{N}{2}\right)-1\right)+2\right)\right)\right)$$
86	85	simprd	$$⊢\left(\phi \wedge 2\parallel N\right)\to 2^{2\left(\left(\frac{N}{2}\right)-1\right)+2}\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\left(\left(\frac{N}{2}\right)-1\right)+2\right)\right)$$
87	4	nncnd	$$⊢\phi \to 2\in ℂ$$
88	1	nncnd	$$⊢\phi \to N\in ℂ$$
89	88	halfcld	$$⊢\phi \to \frac{N}{2}\in ℂ$$
90	87 89	muls1d	$$⊢\phi \to 2\left(\left(\frac{N}{2}\right)-1\right)=2\left(\frac{N}{2}\right)-2$$
91	90	oveq1d	$$⊢\phi \to 2\left(\left(\frac{N}{2}\right)-1\right)+2=2\left(\frac{N}{2}\right)-2+2$$
92	87 89	mulcld	$$⊢\phi \to 2\left(\frac{N}{2}\right)\in ℂ$$
93	92 87	npcand	$$⊢\phi \to 2\left(\frac{N}{2}\right)-2+2=2\left(\frac{N}{2}\right)$$
94	91 93	eqtrd	$$⊢\phi \to 2\left(\left(\frac{N}{2}\right)-1\right)+2=2\left(\frac{N}{2}\right)$$
95	4	nnne0d	$$⊢\phi \to 2\ne 0$$
96	88 87 95	divcan2d	$$⊢\phi \to 2\left(\frac{N}{2}\right)=N$$
97	94 96	eqtrd	$$⊢\phi \to 2\left(\left(\frac{N}{2}\right)-1\right)+2=N$$
98	97	oveq2d	$$⊢\phi \to 2^{2\left(\left(\frac{N}{2}\right)-1\right)+2}=2^N$$
99	97	oveq2d	$$⊢\phi \to \left(1\dots 2\left(\left(\frac{N}{2}\right)-1\right)+2\right)=\left(1\dots N\right)$$
100	99	fveq2d	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\left(\left(\frac{N}{2}\right)-1\right)+2\right)\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)$$
101	98 100	breq12d	$$⊢\phi \to \left(2^{2\left(\left(\frac{N}{2}\right)-1\right)+2}\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\left(\left(\frac{N}{2}\right)-1\right)+2\right)\right)\leftrightarrow 2^N\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)\right)$$
102	101	adantr	$$⊢\left(\phi \wedge 2\parallel N\right)\to \left(2^{2\left(\left(\frac{N}{2}\right)-1\right)+2}\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\left(\left(\frac{N}{2}\right)-1\right)+2\right)\right)\leftrightarrow 2^N\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)\right)$$
103	86 102	mpbid	$$⊢\left(\phi \wedge 2\parallel N\right)\to 2^N\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)$$
104		oddm1even	$$⊢N\in \mathbb{Z}\to \left(\neg 2\parallel N\leftrightarrow 2\parallel \left(N-1\right)\right)$$
105	70 104	syl	$$⊢\phi \to \left(\neg 2\parallel N\leftrightarrow 2\parallel \left(N-1\right)\right)$$
106	105	biimpa	$$⊢\left(\phi \wedge \neg 2\parallel N\right)\to 2\parallel \left(N-1\right)$$
107	3	a1i	$$⊢\left(\phi \wedge \neg 2\parallel N\right)\to 2\in \mathbb{N}$$
108		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
109	70 108	zsubcld	$$⊢\phi \to N-1\in \mathbb{Z}$$
110		0red	$$⊢\phi \to 0\in ℝ$$
111	48	a1i	$$⊢\phi \to 8\in ℝ$$
112		1red	$$⊢\phi \to 1\in ℝ$$
113	34 112	resubcld	$$⊢\phi \to N-1\in ℝ$$
114		8pos	$$⊢0<8$$
115	114	a1i	$$⊢\phi \to 0<8$$
116	40 34 112 2	lesub1dd	$$⊢\phi \to 9-1\le N-1$$
117	58 116	eqbrtrrid	$$⊢\phi \to 8\le N-1$$
118	110 111 113 115 117	ltletrd	$$⊢\phi \to 0<N-1$$
119	109 118	jca	$$⊢\phi \to \left(N-1\in \mathbb{Z}\wedge 0<N-1\right)$$
120		elnnz	$$⊢N-1\in \mathbb{N}\leftrightarrow \left(N-1\in \mathbb{Z}\wedge 0<N-1\right)$$
121	119 120	sylibr	$$⊢\phi \to N-1\in \mathbb{N}$$
122	121	adantr	$$⊢\left(\phi \wedge \neg 2\parallel N\right)\to N-1\in \mathbb{N}$$
123	107 122	nndivdvdsd	$$⊢\left(\phi \wedge \neg 2\parallel N\right)\to \left(2\parallel \left(N-1\right)\leftrightarrow \frac{N-1}{2}\in \mathbb{N}\right)$$
124	106 123	mpbid	$$⊢\left(\phi \wedge \neg 2\parallel N\right)\to \frac{N-1}{2}\in \mathbb{N}$$
125	44 23	mulcomi	$$⊢4\cdot 2=2\cdot 4$$
126	125 46	eqtr3i	$$⊢2\cdot 4=8$$
127	126 50	mpbir	$$⊢\frac{8}{2}=4$$
128	4	nnrpd	$$⊢\phi \to 2\in {ℝ}^{+}$$
129	111 113 128 117	lediv1dd	$$⊢\phi \to \frac{8}{2}\le \frac{N-1}{2}$$
130	127 129	eqbrtrrid	$$⊢\phi \to 4\le \frac{N-1}{2}$$
131	130	adantr	$$⊢\left(\phi \wedge \neg 2\parallel N\right)\to 4\le \frac{N-1}{2}$$
132	124 131	lcmineqlem22	$$⊢\left(\phi \wedge \neg 2\parallel N\right)\to \left(2^{2\left(\frac{N-1}{2}\right)+1}\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\left(\frac{N-1}{2}\right)+1\right)\right)\wedge 2^{2\left(\frac{N-1}{2}\right)+2}\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\left(\frac{N-1}{2}\right)+2\right)\right)\right)$$
133	132	simpld	$$⊢\left(\phi \wedge \neg 2\parallel N\right)\to 2^{2\left(\frac{N-1}{2}\right)+1}\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\left(\frac{N-1}{2}\right)+1\right)\right)$$
134		1cnd	$$⊢\phi \to 1\in ℂ$$
135	88 134	subcld	$$⊢\phi \to N-1\in ℂ$$
136	135 87 95	divcan2d	$$⊢\phi \to 2\left(\frac{N-1}{2}\right)=N-1$$
137	136	oveq1d	$$⊢\phi \to 2\left(\frac{N-1}{2}\right)+1=N-1+1$$
138	88 134	npcand	$$⊢\phi \to N-1+1=N$$
139	137 138	eqtrd	$$⊢\phi \to 2\left(\frac{N-1}{2}\right)+1=N$$
140	139	oveq2d	$$⊢\phi \to 2^{2\left(\frac{N-1}{2}\right)+1}=2^N$$
141	139	oveq2d	$$⊢\phi \to \left(1\dots 2\left(\frac{N-1}{2}\right)+1\right)=\left(1\dots N\right)$$
142	141	fveq2d	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\left(\frac{N-1}{2}\right)+1\right)\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)$$
143	140 142	breq12d	$$⊢\phi \to \left(2^{2\left(\frac{N-1}{2}\right)+1}\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\left(\frac{N-1}{2}\right)+1\right)\right)\leftrightarrow 2^N\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)\right)$$
144	143	adantr	$$⊢\left(\phi \wedge \neg 2\parallel N\right)\to \left(2^{2\left(\frac{N-1}{2}\right)+1}\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\left(\frac{N-1}{2}\right)+1\right)\right)\leftrightarrow 2^N\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)\right)$$
145	133 144	mpbid	$$⊢\left(\phi \wedge \neg 2\parallel N\right)\to 2^N\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)$$
146	103 145	pm2.61dan	$$⊢\phi \to 2^N\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)$$