Theorem lcmineqlem

Description: The least common multiple inequality lemma, a central result for future use. Theorem 3.1 from https://www3.nd.edu/%7eandyp/notes/AKS.pdf (Contributed by metakunt, 16-May-2024)

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

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem.1	$$⊢\phi \to N\in \mathbb{N}$$
2		lcmineqlem.2	$$⊢\phi \to 7\le N$$
3		7re	$$⊢7\in ℝ$$
4	3	a1i	$$⊢\phi \to 7\in ℝ$$
5	1	nnred	$$⊢\phi \to N\in ℝ$$
6	4 5	leloed	$$⊢\phi \to \left(7\le N\leftrightarrow \left(7<N\vee 7=N\right)\right)$$
7	1	nnzd	$$⊢\phi \to N\in \mathbb{Z}$$
8		7nn	$$⊢7\in \mathbb{N}$$
9	8	nnzi	$$⊢7\in \mathbb{Z}$$
10		zltp1le	$$⊢\left(7\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(7<N\leftrightarrow 7+1\le N\right)$$
11	9 10	mpan	$$⊢N\in \mathbb{Z}\to \left(7<N\leftrightarrow 7+1\le N\right)$$
12	7 11	syl	$$⊢\phi \to \left(7<N\leftrightarrow 7+1\le N\right)$$
13		7p1e8	$$⊢7+1=8$$
14	13	breq1i	$$⊢7+1\le N\leftrightarrow 8\le N$$
15	12 14	syl6bb	$$⊢\phi \to \left(7<N\leftrightarrow 8\le N\right)$$
16		8re	$$⊢8\in ℝ$$
17	16	a1i	$$⊢\phi \to 8\in ℝ$$
18	17 5	leloed	$$⊢\phi \to \left(8\le N\leftrightarrow \left(8<N\vee 8=N\right)\right)$$
19	1	adantr	$$⊢\left(\phi \wedge 8<N\right)\to N\in \mathbb{N}$$
20		8p1e9	$$⊢8+1=9$$
21		8nn	$$⊢8\in \mathbb{N}$$
22	21	nnzi	$$⊢8\in \mathbb{Z}$$
23		zltp1le	$$⊢\left(8\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(8<N\leftrightarrow 8+1\le N\right)$$
24	22 23	mpan	$$⊢N\in \mathbb{Z}\to \left(8<N\leftrightarrow 8+1\le N\right)$$
25	7 24	syl	$$⊢\phi \to \left(8<N\leftrightarrow 8+1\le N\right)$$
26	25	biimpd	$$⊢\phi \to \left(8<N\to 8+1\le N\right)$$
27	26	imp	$$⊢\left(\phi \wedge 8<N\right)\to 8+1\le N$$
28	20 27	eqbrtrrid	$$⊢\left(\phi \wedge 8<N\right)\to 9\le N$$
29	19 28	lcmineqlem23	$$⊢\left(\phi \wedge 8<N\right)\to 2^N\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)$$
30	29	ex	$$⊢\phi \to \left(8<N\to 2^N\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)\right)$$
31		2nn0	$$⊢2\in {\mathbb{N}}_0$$
32		8nn0	$$⊢8\in {\mathbb{N}}_0$$
33		5nn0	$$⊢5\in {\mathbb{N}}_0$$
34		4nn0	$$⊢4\in {\mathbb{N}}_0$$
35		6nn0	$$⊢6\in {\mathbb{N}}_0$$
36		0nn0	$$⊢0\in {\mathbb{N}}_0$$
37		2lt8	$$⊢2<8$$
38		5lt10	$$⊢5<10$$
39		6lt10	$$⊢6<10$$
40	31 32 33 34 35 36 37 38 39	3decltc	$$⊢256<840$$
41		5nn	$$⊢5\in \mathbb{N}$$
42	31 41	decnncl	$$⊢25\in \mathbb{N}$$
43	42	nnnn0i	$$⊢25\in {\mathbb{N}}_0$$
44		6nn	$$⊢6\in \mathbb{N}$$
45	43 44	decnncl	$$⊢256\in \mathbb{N}$$
46	45	nnrei	$$⊢256\in ℝ$$
47		4nn	$$⊢4\in \mathbb{N}$$
48	32 47	decnncl	$$⊢84\in \mathbb{N}$$
49	48	decnncl2	$$⊢840\in \mathbb{N}$$
50	49	nnrei	$$⊢840\in ℝ$$
51	46 50	ltlei	$$⊢256<840\to 256\le 840$$
52	40 51	ax-mp	$$⊢256\le 840$$
53		2exp8	$$⊢2^8=256$$
54		oveq2	$$⊢8=N\to 2^8=2^N$$
55	53 54	syl5eqr	$$⊢8=N\to 256=2^N$$
56		lcm8un	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 8\right)\right)=840$$
57		oveq2	$$⊢8=N\to \left(1\dots 8\right)=\left(1\dots N\right)$$
58	57	fveq2d	$$⊢8=N\to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 8\right)\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)$$
59	56 58	syl5eqr	$$⊢8=N\to 840=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)$$
60	55 59	breq12d	$$⊢8=N\to \left(256\le 840\leftrightarrow 2^N\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)\right)$$
61	52 60	mpbii	$$⊢8=N\to 2^N\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)$$
62	61	adantl	$$⊢\left(\phi \wedge 8=N\right)\to 2^N\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)$$
63	62	ex	$$⊢\phi \to \left(8=N\to 2^N\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)\right)$$
64	30 63	jaod	$$⊢\phi \to \left(\left(8<N\vee 8=N\right)\to 2^N\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)\right)$$
65	18 64	sylbid	$$⊢\phi \to \left(8\le N\to 2^N\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)\right)$$
66	15 65	sylbid	$$⊢\phi \to \left(7<N\to 2^N\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)\right)$$
67		1nn0	$$⊢1\in {\mathbb{N}}_0$$
68		1lt4	$$⊢1<4$$
69		2lt10	$$⊢2<10$$
70		8lt10	$$⊢8<10$$
71	67 34 31 31 32 36 68 69 70	3decltc	$$⊢128<420$$
72		2nn	$$⊢2\in \mathbb{N}$$
73	67 72	decnncl	$$⊢12\in \mathbb{N}$$
74	73	nnnn0i	$$⊢12\in {\mathbb{N}}_0$$
75	74 21	decnncl	$$⊢128\in \mathbb{N}$$
76	75	nnrei	$$⊢128\in ℝ$$
77	34 72	decnncl	$$⊢42\in \mathbb{N}$$
78	77	decnncl2	$$⊢420\in \mathbb{N}$$
79	78	nnrei	$$⊢420\in ℝ$$
80	76 79	ltlei	$$⊢128<420\to 128\le 420$$
81	71 80	ax-mp	$$⊢128\le 420$$
82		2exp7	$$⊢2^7=128$$
83		oveq2	$$⊢7=N\to 2^7=2^N$$
84	82 83	syl5eqr	$$⊢7=N\to 128=2^N$$
85		lcm7un	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 7\right)\right)=420$$
86		oveq2	$$⊢7=N\to \left(1\dots 7\right)=\left(1\dots N\right)$$
87	86	fveq2d	$$⊢7=N\to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 7\right)\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)$$
88	85 87	syl5eqr	$$⊢7=N\to 420=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)$$
89	84 88	breq12d	$$⊢7=N\to \left(128\le 420\leftrightarrow 2^N\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)\right)$$
90	81 89	mpbii	$$⊢7=N\to 2^N\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)$$
91	90	a1i	$$⊢\phi \to \left(7=N\to 2^N\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)\right)$$
92	66 91	jaod	$$⊢\phi \to \left(\left(7<N\vee 7=N\right)\to 2^N\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)\right)$$
93	6 92	sylbid	$$⊢\phi \to \left(7\le N\to 2^N\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)\right)$$
94	2 93	mpd	$$⊢\phi \to 2^N\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)$$