Metamath Proof Explorer

Theorem jm2.17b

Description: Weak form of the second half of lemma 2.17 of JonesMatijasevic p. 696, allowing induction to start lower. (Contributed by Stefan O'Rear, 15-Oct-2014)

Ref Expression
Assertion jm2.17b ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 Yrm ( 𝑁 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑎 = 0 → ( 𝑎 + 1 ) = ( 0 + 1 ) )
2 1 oveq2d ⊢ ( 𝑎 = 0 → ( 𝐴 Yrm ( 𝑎 + 1 ) ) = ( 𝐴 Yrm ( 0 + 1 ) ) )
3 oveq2 ⊢ ( 𝑎 = 0 → ( ( 2 · 𝐴 ) ↑ 𝑎 ) = ( ( 2 · 𝐴 ) ↑ 0 ) )
4 2 3 breq12d ⊢ ( 𝑎 = 0 → ( ( 𝐴 Yrm ( 𝑎 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑎 ) ↔ ( 𝐴 Yrm ( 0 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 0 ) ) )
5 4 imbi2d ⊢ ( 𝑎 = 0 → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm ( 𝑎 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑎 ) ) ↔ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm ( 0 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 0 ) ) ) )
6 oveq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑎 + 1 ) = ( 𝑏 + 1 ) )
7 6 oveq2d ⊢ ( 𝑎 = 𝑏 → ( 𝐴 Yrm ( 𝑎 + 1 ) ) = ( 𝐴 Yrm ( 𝑏 + 1 ) ) )
8 oveq2 ⊢ ( 𝑎 = 𝑏 → ( ( 2 · 𝐴 ) ↑ 𝑎 ) = ( ( 2 · 𝐴 ) ↑ 𝑏 ) )
9 7 8 breq12d ⊢ ( 𝑎 = 𝑏 → ( ( 𝐴 Yrm ( 𝑎 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑎 ) ↔ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑏 ) ) )
10 9 imbi2d ⊢ ( 𝑎 = 𝑏 → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm ( 𝑎 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑎 ) ) ↔ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm ( 𝑏 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑏 ) ) ) )
11 oveq1 ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝑎 + 1 ) = ( ( 𝑏 + 1 ) + 1 ) )
12 11 oveq2d ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝐴 Yrm ( 𝑎 + 1 ) ) = ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) )
13 oveq2 ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( 2 · 𝐴 ) ↑ 𝑎 ) = ( ( 2 · 𝐴 ) ↑ ( 𝑏 + 1 ) ) )
14 12 13 breq12d ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( 𝐴 Yrm ( 𝑎 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑎 ) ↔ ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ ( 𝑏 + 1 ) ) ) )
15 14 imbi2d ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm ( 𝑎 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑎 ) ) ↔ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ ( 𝑏 + 1 ) ) ) ) )
16 oveq1 ⊢ ( 𝑎 = 𝑁 → ( 𝑎 + 1 ) = ( 𝑁 + 1 ) )
17 16 oveq2d ⊢ ( 𝑎 = 𝑁 → ( 𝐴 Yrm ( 𝑎 + 1 ) ) = ( 𝐴 Yrm ( 𝑁 + 1 ) ) )
18 oveq2 ⊢ ( 𝑎 = 𝑁 → ( ( 2 · 𝐴 ) ↑ 𝑎 ) = ( ( 2 · 𝐴 ) ↑ 𝑁 ) )
19 17 18 breq12d ⊢ ( 𝑎 = 𝑁 → ( ( 𝐴 Yrm ( 𝑎 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑎 ) ↔ ( 𝐴 Yrm ( 𝑁 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑁 ) ) )
20 19 imbi2d ⊢ ( 𝑎 = 𝑁 → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm ( 𝑎 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑎 ) ) ↔ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm ( 𝑁 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑁 ) ) ) )
21 1le1 ⊢ 1 ≤ 1
22 0p1e1 ⊢ ( 0 + 1 ) = 1
23 22 oveq2i ⊢ ( 𝐴 Yrm ( 0 + 1 ) ) = ( 𝐴 Yrm 1 )
24 rmy1 ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm 1 ) = 1 )
25 23 24 syl5eq ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm ( 0 + 1 ) ) = 1 )
26 2re ⊢ 2 ∈ ℝ
27 eluzelre ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℝ )
28 remulcl ⊢ ( ( 2 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 2 · 𝐴 ) ∈ ℝ )
29 26 27 28 sylancr ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · 𝐴 ) ∈ ℝ )
30 29 recnd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · 𝐴 ) ∈ ℂ )
31 30 exp0d ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 · 𝐴 ) ↑ 0 ) = 1 )
32 25 31 breq12d ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 Yrm ( 0 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 0 ) ↔ 1 ≤ 1 ) )
33 21 32 mpbiri ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm ( 0 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 0 ) )
34 simpr ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
35 nn0z ⊢ ( 𝑏 ∈ ℕ0 → 𝑏 ∈ ℤ )
36 35 adantr ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑏 ∈ ℤ )
37 36 peano2zd ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑏 + 1 ) ∈ ℤ )
38 rmyluc2 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑏 + 1 ) ∈ ℤ ) → ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) = ( ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) − ( 𝐴 Yrm ( ( 𝑏 + 1 ) − 1 ) ) ) )
39 34 37 38 syl2anc ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) = ( ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) − ( 𝐴 Yrm ( ( 𝑏 + 1 ) − 1 ) ) ) )
40 rmxypos ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → ( 0 < ( 𝐴 Xrm 𝑏 ) ∧ 0 ≤ ( 𝐴 Yrm 𝑏 ) ) )
41 40 simprd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℕ0 ) → 0 ≤ ( 𝐴 Yrm 𝑏 ) )
42 41 ancoms ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → 0 ≤ ( 𝐴 Yrm 𝑏 ) )
43 nn0re ⊢ ( 𝑏 ∈ ℕ0 → 𝑏 ∈ ℝ )
44 43 adantr ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑏 ∈ ℝ )
45 44 recnd ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑏 ∈ ℂ )
46 ax-1cn ⊢ 1 ∈ ℂ
47 pncan ⊢ ( ( 𝑏 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑏 + 1 ) − 1 ) = 𝑏 )
48 45 46 47 sylancl ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑏 + 1 ) − 1 ) = 𝑏 )
49 48 oveq2d ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 Yrm ( ( 𝑏 + 1 ) − 1 ) ) = ( 𝐴 Yrm 𝑏 ) )
50 42 49 breqtrrd ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → 0 ≤ ( 𝐴 Yrm ( ( 𝑏 + 1 ) − 1 ) ) )
51 27 adantl ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐴 ∈ ℝ )
52 26 51 28 sylancr ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( 2 · 𝐴 ) ∈ ℝ )
53 frmy ⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
54 53 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑏 + 1 ) ∈ ℤ ) → ( 𝐴 Yrm ( 𝑏 + 1 ) ) ∈ ℤ )
55 54 zred ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑏 + 1 ) ∈ ℤ ) → ( 𝐴 Yrm ( 𝑏 + 1 ) ) ∈ ℝ )
56 34 37 55 syl2anc ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 Yrm ( 𝑏 + 1 ) ) ∈ ℝ )
57 52 56 remulcld ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ∈ ℝ )
58 53 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ) → ( 𝐴 Yrm 𝑏 ) ∈ ℤ )
59 58 zred ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ) → ( 𝐴 Yrm 𝑏 ) ∈ ℝ )
60 34 36 59 syl2anc ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 Yrm 𝑏 ) ∈ ℝ )
61 49 60 eqeltrd ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 Yrm ( ( 𝑏 + 1 ) − 1 ) ) ∈ ℝ )
62 57 61 subge02d ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( 0 ≤ ( 𝐴 Yrm ( ( 𝑏 + 1 ) − 1 ) ) ↔ ( ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) − ( 𝐴 Yrm ( ( 𝑏 + 1 ) − 1 ) ) ) ≤ ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ) )
63 50 62 mpbid ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) − ( 𝐴 Yrm ( ( 𝑏 + 1 ) − 1 ) ) ) ≤ ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) )
64 39 63 eqbrtrd ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) ≤ ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) )
65 64 3adant3 ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑏 ) ) → ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) ≤ ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) )
66 simpl ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑏 ∈ ℕ0 )
67 52 66 reexpcld ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 2 · 𝐴 ) ↑ 𝑏 ) ∈ ℝ )
68 2nn ⊢ 2 ∈ ℕ
69 eluz2nn ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℕ )
70 nnmulcl ⊢ ( ( 2 ∈ ℕ ∧ 𝐴 ∈ ℕ ) → ( 2 · 𝐴 ) ∈ ℕ )
71 68 69 70 sylancr ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · 𝐴 ) ∈ ℕ )
72 71 nngt0d ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 0 < ( 2 · 𝐴 ) )
73 72 adantl ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → 0 < ( 2 · 𝐴 ) )
74 lemul2 ⊢ ( ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) ∈ ℝ ∧ ( ( 2 · 𝐴 ) ↑ 𝑏 ) ∈ ℝ ∧ ( ( 2 · 𝐴 ) ∈ ℝ ∧ 0 < ( 2 · 𝐴 ) ) ) → ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑏 ) ↔ ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ≤ ( ( 2 · 𝐴 ) · ( ( 2 · 𝐴 ) ↑ 𝑏 ) ) ) )
75 56 67 52 73 74 syl112anc ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑏 ) ↔ ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ≤ ( ( 2 · 𝐴 ) · ( ( 2 · 𝐴 ) ↑ 𝑏 ) ) ) )
76 75 biimp3a ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑏 ) ) → ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ≤ ( ( 2 · 𝐴 ) · ( ( 2 · 𝐴 ) ↑ 𝑏 ) ) )
77 52 recnd ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( 2 · 𝐴 ) ∈ ℂ )
78 77 66 expp1d ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 2 · 𝐴 ) ↑ ( 𝑏 + 1 ) ) = ( ( ( 2 · 𝐴 ) ↑ 𝑏 ) · ( 2 · 𝐴 ) ) )
79 67 recnd ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 2 · 𝐴 ) ↑ 𝑏 ) ∈ ℂ )
80 79 77 mulcomd ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ( 2 · 𝐴 ) ↑ 𝑏 ) · ( 2 · 𝐴 ) ) = ( ( 2 · 𝐴 ) · ( ( 2 · 𝐴 ) ↑ 𝑏 ) ) )
81 78 80 eqtrd ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 2 · 𝐴 ) ↑ ( 𝑏 + 1 ) ) = ( ( 2 · 𝐴 ) · ( ( 2 · 𝐴 ) ↑ 𝑏 ) ) )
82 81 3adant3 ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑏 ) ) → ( ( 2 · 𝐴 ) ↑ ( 𝑏 + 1 ) ) = ( ( 2 · 𝐴 ) · ( ( 2 · 𝐴 ) ↑ 𝑏 ) ) )
83 76 82 breqtrrd ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑏 ) ) → ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ≤ ( ( 2 · 𝐴 ) ↑ ( 𝑏 + 1 ) ) )
84 37 peano2zd ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑏 + 1 ) + 1 ) ∈ ℤ )
85 53 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( 𝑏 + 1 ) + 1 ) ∈ ℤ ) → ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) ∈ ℤ )
86 85 zred ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( 𝑏 + 1 ) + 1 ) ∈ ℤ ) → ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) ∈ ℝ )
87 34 84 86 syl2anc ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) ∈ ℝ )
88 peano2nn0 ⊢ ( 𝑏 ∈ ℕ0 → ( 𝑏 + 1 ) ∈ ℕ0 )
89 88 adantr ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑏 + 1 ) ∈ ℕ0 )
90 52 89 reexpcld ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 2 · 𝐴 ) ↑ ( 𝑏 + 1 ) ) ∈ ℝ )
91 letr ⊢ ( ( ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) ∈ ℝ ∧ ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ∈ ℝ ∧ ( ( 2 · 𝐴 ) ↑ ( 𝑏 + 1 ) ) ∈ ℝ ) → ( ( ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) ≤ ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ∧ ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ≤ ( ( 2 · 𝐴 ) ↑ ( 𝑏 + 1 ) ) ) → ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ ( 𝑏 + 1 ) ) ) )
92 87 57 90 91 syl3anc ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) ≤ ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ∧ ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ≤ ( ( 2 · 𝐴 ) ↑ ( 𝑏 + 1 ) ) ) → ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ ( 𝑏 + 1 ) ) ) )
93 92 3adant3 ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑏 ) ) → ( ( ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) ≤ ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ∧ ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ≤ ( ( 2 · 𝐴 ) ↑ ( 𝑏 + 1 ) ) ) → ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ ( 𝑏 + 1 ) ) ) )
94 65 83 93 mp2and ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑏 ) ) → ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ ( 𝑏 + 1 ) ) )
95 94 3exp ⊢ ( 𝑏 ∈ ℕ0 → ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑏 ) → ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ ( 𝑏 + 1 ) ) ) ) )
96 95 a2d ⊢ ( 𝑏 ∈ ℕ0 → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm ( 𝑏 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑏 ) ) → ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ ( 𝑏 + 1 ) ) ) ) )
97 5 10 15 20 33 96 nn0ind ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm ( 𝑁 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑁 ) ) )
98 97 impcom ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 Yrm ( 𝑁 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑁 ) )