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 eluz3nn ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 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 ≤ 𝑆 )