Theorem lighneallem4a

Description: Lemma 1 for lighneallem4 . (Contributed by AV, 16-Aug-2021)

	Ref	Expression
Assertion	lighneallem4a	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\wedge S=\frac{A^M+1}{A+1}\right)\to 2\le S$$

Proof

Step	Hyp	Ref	Expression
1		2re	$$⊢2\in ℝ$$
2	1	a1i	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 2\in ℝ$$
3		eluzelre	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\in ℝ$$
4		peano2re	$$⊢A\in ℝ\to A+1\in ℝ$$
5	3 4	syl	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A+1\in ℝ$$
6	2 5	remulcld	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 2\left(A+1\right)\in ℝ$$
7	6	adantr	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to 2\left(A+1\right)\in ℝ$$
8		eluzge2nn0	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\in {\mathbb{N}}_0$$
9	8	adantr	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to A\in {\mathbb{N}}_0$$
10		eluz3nn	$$⊢M\in {\mathbb{Z}}_{\ge 3}\to M\in \mathbb{N}$$
11	10	nnnn0d	$$⊢M\in {\mathbb{Z}}_{\ge 3}\to M\in {\mathbb{N}}_0$$
12	11	adantl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to M\in {\mathbb{N}}_0$$
13	9 12	nn0expcld	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to A^M\in {\mathbb{N}}_0$$
14	13	nn0red	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to A^M\in ℝ$$
15		peano2re	$$⊢A^M\in ℝ\to A^M+1\in ℝ$$
16	14 15	syl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to A^M+1\in ℝ$$
17	2 3	remulcld	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 2A\in ℝ$$
18	2 17	remulcld	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 22A\in ℝ$$
19	18	adantr	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to 22A\in ℝ$$
20		1red	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 1\in ℝ$$
21		eluz2nn	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\in \mathbb{N}$$
22	21	nnge1d	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 1\le A$$
23	20 3 3 22	leadd2dd	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A+1\le A+A$$
24		eluzelcn	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\in ℂ$$
25	24	2timesd	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 2A=A+A$$
26	23 25	breqtrrd	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A+1\le 2A$$
27	26	adantr	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to A+1\le 2A$$
28		2pos	$$⊢0<2$$
29	1 28	pm3.2i	$$⊢\left(2\in ℝ\wedge 0<2\right)$$
30	29	a1i	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \left(2\in ℝ\wedge 0<2\right)$$
31	5 17 30	3jca	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \left(A+1\in ℝ\wedge 2A\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)$$
32	31	adantr	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to \left(A+1\in ℝ\wedge 2A\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)$$
33		lemul2	$$⊢\left(A+1\in ℝ\wedge 2A\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left(A+1\le 2A\leftrightarrow 2\left(A+1\right)\le 22A\right)$$
34	32 33	syl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to \left(A+1\le 2A\leftrightarrow 2\left(A+1\right)\le 22A\right)$$
35	27 34	mpbid	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to 2\left(A+1\right)\le 22A$$
36		2cn	$$⊢2\in ℂ$$
37	36	a1i	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to 2\in ℂ$$
38	24	adantr	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to A\in ℂ$$
39	37 37 38	mulassd	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to 2\cdot 2A=22A$$
40		sq2	$$⊢2^2=4$$
41		4re	$$⊢4\in ℝ$$
42	40 41	eqeltri	$$⊢2^2\in ℝ$$
43	42	a1i	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to 2^2\in ℝ$$
44		nn0sqcl	$$⊢A\in {\mathbb{N}}_0\to A^2\in {\mathbb{N}}_0$$
45	8 44	syl	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A^2\in {\mathbb{N}}_0$$
46	45	nn0red	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A^2\in ℝ$$
47	46	adantr	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to A^2\in ℝ$$
48		nnm1nn0	$$⊢M\in \mathbb{N}\to M-1\in {\mathbb{N}}_0$$
49	10 48	syl	$$⊢M\in {\mathbb{Z}}_{\ge 3}\to M-1\in {\mathbb{N}}_0$$
50	49	adantl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to M-1\in {\mathbb{N}}_0$$
51	9 50	nn0expcld	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to A^{M-1}\in {\mathbb{N}}_0$$
52	51	nn0red	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to A^{M-1}\in ℝ$$
53		2nn0	$$⊢2\in {\mathbb{N}}_0$$
54	53	a1i	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 2\in {\mathbb{N}}_0$$
55	2 3 54	3jca	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \left(2\in ℝ\wedge A\in ℝ\wedge 2\in {\mathbb{N}}_0\right)$$
56	55	adantr	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to \left(2\in ℝ\wedge A\in ℝ\wedge 2\in {\mathbb{N}}_0\right)$$
57		0le2	$$⊢0\le 2$$
58	57	a1i	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to 0\le 2$$
59		eluzle	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 2\le A$$
60	59	adantr	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to 2\le A$$
61		leexp1a	$$⊢\left(\left(2\in ℝ\wedge A\in ℝ\wedge 2\in {\mathbb{N}}_0\right)\wedge \left(0\le 2\wedge 2\le A\right)\right)\to 2^2\le A^2$$
62	56 58 60 61	syl12anc	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to 2^2\le A^2$$
63		2p1e3	$$⊢2+1=3$$
64		eluzle	$$⊢M\in {\mathbb{Z}}_{\ge 3}\to 3\le M$$
65	63 64	eqbrtrid	$$⊢M\in {\mathbb{Z}}_{\ge 3}\to 2+1\le M$$
66		1red	$$⊢M\in {\mathbb{Z}}_{\ge 3}\to 1\in ℝ$$
67		eluzelre	$$⊢M\in {\mathbb{Z}}_{\ge 3}\to M\in ℝ$$
68		leaddsub	$$⊢\left(2\in ℝ\wedge 1\in ℝ\wedge M\in ℝ\right)\to \left(2+1\le M\leftrightarrow 2\le M-1\right)$$
69	1 66 67 68	mp3an2i	$$⊢M\in {\mathbb{Z}}_{\ge 3}\to \left(2+1\le M\leftrightarrow 2\le M-1\right)$$
70	65 69	mpbid	$$⊢M\in {\mathbb{Z}}_{\ge 3}\to 2\le M-1$$
71	70	adantl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to 2\le M-1$$
72	3	adantr	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to A\in ℝ$$
73		2z	$$⊢2\in \mathbb{Z}$$
74	73	a1i	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to 2\in \mathbb{Z}$$
75		eluzelz	$$⊢M\in {\mathbb{Z}}_{\ge 3}\to M\in \mathbb{Z}$$
76		peano2zm	$$⊢M\in \mathbb{Z}\to M-1\in \mathbb{Z}$$
77	75 76	syl	$$⊢M\in {\mathbb{Z}}_{\ge 3}\to M-1\in \mathbb{Z}$$
78	77	adantl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to M-1\in \mathbb{Z}$$
79		eluz2gt1	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 1<A$$
80	79	adantr	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to 1<A$$
81	72 74 78 80	leexp2d	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to \left(2\le M-1\leftrightarrow A^2\le A^{M-1}\right)$$
82	71 81	mpbid	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to A^2\le A^{M-1}$$
83	43 47 52 62 82	letrd	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to 2^2\le A^{M-1}$$
84	36	sqvali	$$⊢2^2=2\cdot 2$$
85	84	eqcomi	$$⊢2\cdot 2=2^2$$
86	85	a1i	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to 2\cdot 2=2^2$$
87		eluz2n0	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\ne 0$$
88	87	adantr	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to A\ne 0$$
89	75	adantl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to M\in \mathbb{Z}$$
90	38 88 89	expm1d	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to A^{M-1}=\frac{A^M}{A}$$
91	90	eqcomd	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to \frac{A^M}{A}=A^{M-1}$$
92	83 86 91	3brtr4d	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to 2\cdot 2\le \frac{A^M}{A}$$
93	1 1	remulcli	$$⊢2\cdot 2\in ℝ$$
94	21	nngt0d	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 0<A$$
95	3 94	jca	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \left(A\in ℝ\wedge 0<A\right)$$
96	95	adantr	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to \left(A\in ℝ\wedge 0<A\right)$$
97		lemuldiv	$$⊢\left(2\cdot 2\in ℝ\wedge A^M\in ℝ\wedge \left(A\in ℝ\wedge 0<A\right)\right)\to \left(2\cdot 2A\le A^M\leftrightarrow 2\cdot 2\le \frac{A^M}{A}\right)$$
98	93 14 96 97	mp3an2i	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to \left(2\cdot 2A\le A^M\leftrightarrow 2\cdot 2\le \frac{A^M}{A}\right)$$
99	92 98	mpbird	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to 2\cdot 2A\le A^M$$
100	39 99	eqbrtrrd	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to 22A\le A^M$$
101	7 19 14 35 100	letrd	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to 2\left(A+1\right)\le A^M$$
102	14	lep1d	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to A^M\le A^M+1$$
103	7 14 16 101 102	letrd	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to 2\left(A+1\right)\le A^M+1$$
104		nnnn0	$$⊢A\in \mathbb{N}\to A\in {\mathbb{N}}_0$$
105		nn0p1gt0	$$⊢A\in {\mathbb{N}}_0\to 0<A+1$$
106	21 104 105	3syl	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 0<A+1$$
107	5 106	jca	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to \left(A+1\in ℝ\wedge 0<A+1\right)$$
108	107	adantr	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to \left(A+1\in ℝ\wedge 0<A+1\right)$$
109		lemuldiv	$$⊢\left(2\in ℝ\wedge A^M+1\in ℝ\wedge \left(A+1\in ℝ\wedge 0<A+1\right)\right)\to \left(2\left(A+1\right)\le A^M+1\leftrightarrow 2\le \frac{A^M+1}{A+1}\right)$$
110	1 16 108 109	mp3an2i	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to \left(2\left(A+1\right)\le A^M+1\leftrightarrow 2\le \frac{A^M+1}{A+1}\right)$$
111	103 110	mpbid	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\right)\to 2\le \frac{A^M+1}{A+1}$$
112	111	3adant3	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\wedge S=\frac{A^M+1}{A+1}\right)\to 2\le \frac{A^M+1}{A+1}$$
113		breq2	$$⊢S=\frac{A^M+1}{A+1}\to \left(2\le S\leftrightarrow 2\le \frac{A^M+1}{A+1}\right)$$
114	113	3ad2ant3	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\wedge S=\frac{A^M+1}{A+1}\right)\to \left(2\le S\leftrightarrow 2\le \frac{A^M+1}{A+1}\right)$$
115	112 114	mpbird	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{Z}}_{\ge 3}\wedge S=\frac{A^M+1}{A+1}\right)\to 2\le S$$