Metamath Proof Explorer


Theorem lighneallem4a

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

Ref Expression
Assertion lighneallem4a ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ ‘ 3 ) ∧ 𝑆 = ( ( ( 𝐴𝑀 ) + 1 ) / ( 𝐴 + 1 ) ) ) → 2 ≤ 𝑆 )

Proof

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