Metamath Proof Explorer

Theorem jm2.17a

Description: First half of lemma 2.17 of JonesMatijasevic p. 696. (Contributed by Stefan O'Rear, 14-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑎 = 0 → ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑎 ) = ( ( ( 2 · 𝐴 ) − 1 ) ↑ 0 ) )
2 oveq1 ⊢ ( 𝑎 = 0 → ( 𝑎 + 1 ) = ( 0 + 1 ) )
3 2 oveq2d ⊢ ( 𝑎 = 0 → ( 𝐴 Yrm ( 𝑎 + 1 ) ) = ( 𝐴 Yrm ( 0 + 1 ) ) )
4 1 3 breq12d ⊢ ( 𝑎 = 0 → ( ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑎 ) ≤ ( 𝐴 Yrm ( 𝑎 + 1 ) ) ↔ ( ( ( 2 · 𝐴 ) − 1 ) ↑ 0 ) ≤ ( 𝐴 Yrm ( 0 + 1 ) ) ) )
5 4 imbi2d ⊢ ( 𝑎 = 0 → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑎 ) ≤ ( 𝐴 Yrm ( 𝑎 + 1 ) ) ) ↔ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 2 · 𝐴 ) − 1 ) ↑ 0 ) ≤ ( 𝐴 Yrm ( 0 + 1 ) ) ) ) )
6 oveq2 ⊢ ( 𝑎 = 𝑏 → ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑎 ) = ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑏 ) )
7 oveq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑎 + 1 ) = ( 𝑏 + 1 ) )
8 7 oveq2d ⊢ ( 𝑎 = 𝑏 → ( 𝐴 Yrm ( 𝑎 + 1 ) ) = ( 𝐴 Yrm ( 𝑏 + 1 ) ) )
9 6 8 breq12d ⊢ ( 𝑎 = 𝑏 → ( ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑎 ) ≤ ( 𝐴 Yrm ( 𝑎 + 1 ) ) ↔ ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑏 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) )
10 9 imbi2d ⊢ ( 𝑎 = 𝑏 → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑎 ) ≤ ( 𝐴 Yrm ( 𝑎 + 1 ) ) ) ↔ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑏 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ) )
11 oveq2 ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑎 ) = ( ( ( 2 · 𝐴 ) − 1 ) ↑ ( 𝑏 + 1 ) ) )
12 oveq1 ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝑎 + 1 ) = ( ( 𝑏 + 1 ) + 1 ) )
13 12 oveq2d ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝐴 Yrm ( 𝑎 + 1 ) ) = ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) )
14 11 13 breq12d ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑎 ) ≤ ( 𝐴 Yrm ( 𝑎 + 1 ) ) ↔ ( ( ( 2 · 𝐴 ) − 1 ) ↑ ( 𝑏 + 1 ) ) ≤ ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) ) )
15 14 imbi2d ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑎 ) ≤ ( 𝐴 Yrm ( 𝑎 + 1 ) ) ) ↔ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 2 · 𝐴 ) − 1 ) ↑ ( 𝑏 + 1 ) ) ≤ ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) ) ) )
16 oveq2 ⊢ ( 𝑎 = 𝑁 → ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑎 ) = ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑁 ) )
17 oveq1 ⊢ ( 𝑎 = 𝑁 → ( 𝑎 + 1 ) = ( 𝑁 + 1 ) )
18 17 oveq2d ⊢ ( 𝑎 = 𝑁 → ( 𝐴 Yrm ( 𝑎 + 1 ) ) = ( 𝐴 Yrm ( 𝑁 + 1 ) ) )
19 16 18 breq12d ⊢ ( 𝑎 = 𝑁 → ( ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑎 ) ≤ ( 𝐴 Yrm ( 𝑎 + 1 ) ) ↔ ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑁 ) ≤ ( 𝐴 Yrm ( 𝑁 + 1 ) ) ) )
20 19 imbi2d ⊢ ( 𝑎 = 𝑁 → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑎 ) ≤ ( 𝐴 Yrm ( 𝑎 + 1 ) ) ) ↔ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑁 ) ≤ ( 𝐴 Yrm ( 𝑁 + 1 ) ) ) ) )
21 1le1 ⊢ 1 ≤ 1
22 21 a1i ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 1 ≤ 1 )
23 2cn ⊢ 2 ∈ ℂ
24 eluzelcn ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℂ )
25 mulcl ⊢ ( ( 2 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 2 · 𝐴 ) ∈ ℂ )
26 23 24 25 sylancr ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · 𝐴 ) ∈ ℂ )
27 ax-1cn ⊢ 1 ∈ ℂ
28 subcl ⊢ ( ( ( 2 · 𝐴 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 2 · 𝐴 ) − 1 ) ∈ ℂ )
29 26 27 28 sylancl ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 · 𝐴 ) − 1 ) ∈ ℂ )
30 29 exp0d ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 2 · 𝐴 ) − 1 ) ↑ 0 ) = 1 )
31 0p1e1 ⊢ ( 0 + 1 ) = 1
32 31 oveq2i ⊢ ( 𝐴 Yrm ( 0 + 1 ) ) = ( 𝐴 Yrm 1 )
33 rmy1 ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm 1 ) = 1 )
34 32 33 syl5eq ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm ( 0 + 1 ) ) = 1 )
35 22 30 34 3brtr4d ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 2 · 𝐴 ) − 1 ) ↑ 0 ) ≤ ( 𝐴 Yrm ( 0 + 1 ) ) )
36 2re ⊢ 2 ∈ ℝ
37 eluzelre ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℝ )
38 37 adantl ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐴 ∈ ℝ )
39 remulcl ⊢ ( ( 2 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 2 · 𝐴 ) ∈ ℝ )
40 36 38 39 sylancr ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( 2 · 𝐴 ) ∈ ℝ )
41 1re ⊢ 1 ∈ ℝ
42 resubcl ⊢ ( ( ( 2 · 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 2 · 𝐴 ) − 1 ) ∈ ℝ )
43 40 41 42 sylancl ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 2 · 𝐴 ) − 1 ) ∈ ℝ )
44 peano2nn0 ⊢ ( 𝑏 ∈ ℕ0 → ( 𝑏 + 1 ) ∈ ℕ0 )
45 44 adantr ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑏 + 1 ) ∈ ℕ0 )
46 43 45 reexpcld ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ( 2 · 𝐴 ) − 1 ) ↑ ( 𝑏 + 1 ) ) ∈ ℝ )
47 46 3adant3 ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑏 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) → ( ( ( 2 · 𝐴 ) − 1 ) ↑ ( 𝑏 + 1 ) ) ∈ ℝ )
48 simpr ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
49 nn0z ⊢ ( 𝑏 ∈ ℕ0 → 𝑏 ∈ ℤ )
50 49 adantr ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑏 ∈ ℤ )
51 50 peano2zd ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑏 + 1 ) ∈ ℤ )
52 frmy ⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
53 52 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑏 + 1 ) ∈ ℤ ) → ( 𝐴 Yrm ( 𝑏 + 1 ) ) ∈ ℤ )
54 53 zred ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑏 + 1 ) ∈ ℤ ) → ( 𝐴 Yrm ( 𝑏 + 1 ) ) ∈ ℝ )
55 48 51 54 syl2anc ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 Yrm ( 𝑏 + 1 ) ) ∈ ℝ )
56 55 43 remulcld ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) · ( ( 2 · 𝐴 ) − 1 ) ) ∈ ℝ )
57 56 3adant3 ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑏 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) → ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) · ( ( 2 · 𝐴 ) − 1 ) ) ∈ ℝ )
58 51 peano2zd ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑏 + 1 ) + 1 ) ∈ ℤ )
59 52 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( 𝑏 + 1 ) + 1 ) ∈ ℤ ) → ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) ∈ ℤ )
60 59 zred ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( 𝑏 + 1 ) + 1 ) ∈ ℤ ) → ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) ∈ ℝ )
61 48 58 60 syl2anc ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) ∈ ℝ )
62 61 3adant3 ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑏 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) → ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) ∈ ℝ )
63 29 3ad2ant2 ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑏 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) → ( ( 2 · 𝐴 ) − 1 ) ∈ ℂ )
64 simp1 ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑏 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) → 𝑏 ∈ ℕ0 )
65 63 64 expp1d ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑏 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) → ( ( ( 2 · 𝐴 ) − 1 ) ↑ ( 𝑏 + 1 ) ) = ( ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑏 ) · ( ( 2 · 𝐴 ) − 1 ) ) )
66 simpl ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑏 ∈ ℕ0 )
67 43 66 reexpcld ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑏 ) ∈ ℝ )
68 2nn ⊢ 2 ∈ ℕ
69 eluz2nn ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℕ )
70 69 adantl ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐴 ∈ ℕ )
71 nnmulcl ⊢ ( ( 2 ∈ ℕ ∧ 𝐴 ∈ ℕ ) → ( 2 · 𝐴 ) ∈ ℕ )
72 68 70 71 sylancr ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( 2 · 𝐴 ) ∈ ℕ )
73 nnm1nn0 ⊢ ( ( 2 · 𝐴 ) ∈ ℕ → ( ( 2 · 𝐴 ) − 1 ) ∈ ℕ0 )
74 nn0ge0 ⊢ ( ( ( 2 · 𝐴 ) − 1 ) ∈ ℕ0 → 0 ≤ ( ( 2 · 𝐴 ) − 1 ) )
75 72 73 74 3syl ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → 0 ≤ ( ( 2 · 𝐴 ) − 1 ) )
76 43 75 jca ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ( 2 · 𝐴 ) − 1 ) ∈ ℝ ∧ 0 ≤ ( ( 2 · 𝐴 ) − 1 ) ) )
77 67 55 76 3jca ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑏 ) ∈ ℝ ∧ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ∈ ℝ ∧ ( ( ( 2 · 𝐴 ) − 1 ) ∈ ℝ ∧ 0 ≤ ( ( 2 · 𝐴 ) − 1 ) ) ) )
78 lemul1a ⊢ ( ( ( ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑏 ) ∈ ℝ ∧ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ∈ ℝ ∧ ( ( ( 2 · 𝐴 ) − 1 ) ∈ ℝ ∧ 0 ≤ ( ( 2 · 𝐴 ) − 1 ) ) ) ∧ ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑏 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) → ( ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑏 ) · ( ( 2 · 𝐴 ) − 1 ) ) ≤ ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) · ( ( 2 · 𝐴 ) − 1 ) ) )
79 77 78 stoic3 ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑏 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) → ( ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑏 ) · ( ( 2 · 𝐴 ) − 1 ) ) ≤ ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) · ( ( 2 · 𝐴 ) − 1 ) ) )
80 65 79 eqbrtrd ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑏 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) → ( ( ( 2 · 𝐴 ) − 1 ) ↑ ( 𝑏 + 1 ) ) ≤ ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) · ( ( 2 · 𝐴 ) − 1 ) ) )
81 nn0cn ⊢ ( 𝑏 ∈ ℕ0 → 𝑏 ∈ ℂ )
82 81 adantr ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑏 ∈ ℂ )
83 pncan ⊢ ( ( 𝑏 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑏 + 1 ) − 1 ) = 𝑏 )
84 82 27 83 sylancl ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑏 + 1 ) − 1 ) = 𝑏 )
85 84 oveq2d ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 Yrm ( ( 𝑏 + 1 ) − 1 ) ) = ( 𝐴 Yrm 𝑏 ) )
86 52 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ) → ( 𝐴 Yrm 𝑏 ) ∈ ℤ )
87 86 zred ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ) → ( 𝐴 Yrm 𝑏 ) ∈ ℝ )
88 48 50 87 syl2anc ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 Yrm 𝑏 ) ∈ ℝ )
89 85 88 eqeltrd ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 Yrm ( ( 𝑏 + 1 ) − 1 ) ) ∈ ℝ )
90 remulcl ⊢ ( ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) · 1 ) ∈ ℝ )
91 55 41 90 sylancl ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) · 1 ) ∈ ℝ )
92 40 55 remulcld ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) ∈ ℝ )
93 nn0re ⊢ ( 𝑏 ∈ ℕ0 → 𝑏 ∈ ℝ )
94 93 adantr ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑏 ∈ ℝ )
95 94 lep1d ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑏 ≤ ( 𝑏 + 1 ) )
96 lermy ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ∧ ( 𝑏 + 1 ) ∈ ℤ ) → ( 𝑏 ≤ ( 𝑏 + 1 ) ↔ ( 𝐴 Yrm 𝑏 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) )
97 48 50 51 96 syl3anc ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑏 ≤ ( 𝑏 + 1 ) ↔ ( 𝐴 Yrm 𝑏 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) )
98 95 97 mpbid ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 Yrm 𝑏 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) )
99 55 recnd ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 Yrm ( 𝑏 + 1 ) ) ∈ ℂ )
100 99 mulid1d ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) · 1 ) = ( 𝐴 Yrm ( 𝑏 + 1 ) ) )
101 98 85 100 3brtr4d ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 Yrm ( ( 𝑏 + 1 ) − 1 ) ) ≤ ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) · 1 ) )
102 89 91 92 101 lesub2dd ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) − ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) · 1 ) ) ≤ ( ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) − ( 𝐴 Yrm ( ( 𝑏 + 1 ) − 1 ) ) ) )
103 40 recnd ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( 2 · 𝐴 ) ∈ ℂ )
104 27 a1i ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → 1 ∈ ℂ )
105 99 103 104 subdid ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) · ( ( 2 · 𝐴 ) − 1 ) ) = ( ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) · ( 2 · 𝐴 ) ) − ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) · 1 ) ) )
106 99 103 mulcomd ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) · ( 2 · 𝐴 ) ) = ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) )
107 106 oveq1d ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) · ( 2 · 𝐴 ) ) − ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) · 1 ) ) = ( ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) − ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) · 1 ) ) )
108 105 107 eqtrd ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) · ( ( 2 · 𝐴 ) − 1 ) ) = ( ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) − ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) · 1 ) ) )
109 rmyluc2 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑏 + 1 ) ∈ ℤ ) → ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) = ( ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) − ( 𝐴 Yrm ( ( 𝑏 + 1 ) − 1 ) ) ) )
110 48 51 109 syl2anc ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) = ( ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) − ( 𝐴 Yrm ( ( 𝑏 + 1 ) − 1 ) ) ) )
111 102 108 110 3brtr4d ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) · ( ( 2 · 𝐴 ) − 1 ) ) ≤ ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) )
112 111 3adant3 ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑏 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) → ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) · ( ( 2 · 𝐴 ) − 1 ) ) ≤ ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) )
113 47 57 62 80 112 letrd ⊢ ( ( 𝑏 ∈ ℕ0 ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑏 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) → ( ( ( 2 · 𝐴 ) − 1 ) ↑ ( 𝑏 + 1 ) ) ≤ ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) )
114 113 3exp ⊢ ( 𝑏 ∈ ℕ0 → ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑏 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) → ( ( ( 2 · 𝐴 ) − 1 ) ↑ ( 𝑏 + 1 ) ) ≤ ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) ) ) )
115 114 a2d ⊢ ( 𝑏 ∈ ℕ0 → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑏 ) ≤ ( 𝐴 Yrm ( 𝑏 + 1 ) ) ) → ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 2 · 𝐴 ) − 1 ) ↑ ( 𝑏 + 1 ) ) ≤ ( 𝐴 Yrm ( ( 𝑏 + 1 ) + 1 ) ) ) ) )
116 5 10 15 20 35 115 nn0ind ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑁 ) ≤ ( 𝐴 Yrm ( 𝑁 + 1 ) ) ) )
117 116 impcom ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 2 · 𝐴 ) − 1 ) ↑ 𝑁 ) ≤ ( 𝐴 Yrm ( 𝑁 + 1 ) ) )