Metamath Proof Explorer

Theorem lighneallem4a

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

Ref Expression
Assertion lighneallem4a 
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 3 ) /\ S = ( ( ( A ^ M ) + 1 ) / ( A + 1 ) ) ) -> 2 <_ S )

Proof

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