Theorem lcmineqlem19

Description: Dividing implies inequality for lcm inequality lemma. (Contributed by metakunt, 12-May-2024)

	Ref	Expression
Hypothesis	lcmineqlem19.1	$$⊢\phi \to N\in \mathbb{N}$$
Assertion	lcmineqlem19	$$⊢\phi \to N\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{N}\right)\parallel \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem19.1	$$⊢\phi \to N\in \mathbb{N}$$
2		2nn	$$⊢2\in \mathbb{N}$$
3	2	a1i	$$⊢\phi \to 2\in \mathbb{N}$$
4	3 1	nnmulcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in \mathbb{N}$$
5	4	peano2nnd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\in \mathbb{N}$$
6	1	nnnn0d	$$⊢\phi \to N\in {\mathbb{N}}_0$$
7	1	nnred	$$⊢\phi \to N\in ℝ$$
8		2re	$$⊢2\in ℝ$$
9	8	a1i	$$⊢\phi \to 2\in ℝ$$
10	6	nn0ge0d	$$⊢\phi \to 0\le N$$
11	3	nnge1d	$$⊢\phi \to 1\le 2$$
12	7 9 10 11	lemulge12d	$$⊢\phi \to N\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
13	4 6 12	bccl2d	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{N}\right)\in \mathbb{N}$$
14		fz1ssnn	$$⊢\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\subseteq \mathbb{N}$$
15		fzfi	$$⊢\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\in \mathrm{Fin}$$
16		lcmfnncl	$$⊢\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\subseteq \mathbb{N}\wedge \left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\in \mathrm{Fin}\right)\to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)\in \mathbb{N}$$
17	14 15 16	mp2an	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)\in \mathbb{N}$$
18	17	a1i	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)\in \mathbb{N}$$
19		fz1ssnn	$$⊢\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\subseteq \mathbb{N}$$
20		fzfi	$$⊢\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\in \mathrm{Fin}$$
21		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}$$
22	19 20 21	mp2an	$$⊢\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\in \mathbb{N}$$
23	22	a1i	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\in \mathbb{N}$$
24	1 4 12	lcmineqlem16	$$⊢\phi \to N\left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{N}\right)\parallel \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)$$
25	1	lcmineqlem18	$$⊢\phi \to \left(N+1\right)\left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{N+1}\right)=\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{N}\right)$$
26	1	peano2nnd	$$⊢\phi \to N+1\in \mathbb{N}$$
27	9 7	remulcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ$$
28		1red	$$⊢\phi \to 1\in ℝ$$
29	7 27 28 12	leadd1dd	$$⊢\phi \to N+1\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1$$
30	26 5 29	lcmineqlem16	$$⊢\phi \to \left(N+1\right)\left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1}{N+1}\right)\parallel \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)$$
31	25 30	eqbrtrrd	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{N}\right)\parallel \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)$$
32	18	nnzd	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)\in \mathbb{Z}$$
33	5	nnzd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\in \mathbb{Z}$$
34	32 33	jca	$$⊢\phi \to \left(\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)\in \mathbb{Z}\wedge 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\in \mathbb{Z}\right)$$
35		dvdslcm	$$⊢\left(\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)\in \mathbb{Z}\wedge 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\in \mathbb{Z}\right)\to \left(\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)\parallel \left(\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)\mathrm{lcm}\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\wedge \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\parallel \left(\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)\mathrm{lcm}\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\right)$$
36	34 35	syl	$$⊢\phi \to \left(\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)\parallel \left(\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)\mathrm{lcm}\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\wedge \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\parallel \left(\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)\mathrm{lcm}\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)\right)$$
37	36	simpld	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)\parallel \left(\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)\mathrm{lcm}\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)$$
38	5	lcmfunnnd	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1-1\right)\right)\mathrm{lcm}\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)$$
39	27	recnd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ$$
40		1cnd	$$⊢\phi \to 1\in ℂ$$
41	39 40	pncand	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1-1=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
42	41	oveq2d	$$⊢\phi \to \left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1-1\right)=\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
43	42	fveq2d	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1-1\right)\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)$$
44	43	oveq1d	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1-1\right)\right)\mathrm{lcm}\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)\mathrm{lcm}\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)$$
45	38 44	eqtrd	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)=\underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)\mathrm{lcm}\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)$$
46	37 45	breqtrrd	$$⊢\phi \to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\right)\parallel \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)$$
47	1	nnzd	$$⊢\phi \to N\in \mathbb{Z}$$
48		2z	$$⊢2\in \mathbb{Z}$$
49		1z	$$⊢1\in \mathbb{Z}$$
50		gcdaddm	$$⊢\left(2\in \mathbb{Z}\wedge N\in \mathbb{Z}\wedge 1\in \mathbb{Z}\right)\to N\gcd 1=N\gcd \left(1+2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
51	48 49 50	mp3an13	$$⊢N\in \mathbb{Z}\to N\gcd 1=N\gcd \left(1+2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
52	47 51	syl	$$⊢\phi \to N\gcd 1=N\gcd \left(1+2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
53	40 39	addcomd	$$⊢\phi \to 1+2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1$$
54	53	oveq2d	$$⊢\phi \to N\gcd \left(1+2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)=N\gcd \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)$$
55	52 54	eqtrd	$$⊢\phi \to N\gcd 1=N\gcd \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)$$
56		gcd1	$$⊢N\in \mathbb{Z}\to N\gcd 1=1$$
57	47 56	syl	$$⊢\phi \to N\gcd 1=1$$
58	55 57	eqtr3d	$$⊢\phi \to N\gcd \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)=1$$
59	1 5 13 18 23 24 31 46 58	lcmineqlem14	$$⊢\phi \to N\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\left(\genfrac{}{}{0ex}{}{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{N}\right)\parallel \underset{\_}{\mathrm{lcm}}\left(\left(1\dots 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+1\right)\right)$$