Metamath Proof Explorer

Theorem jm2.24nn

Description: X(n) is strictly greater than Y(n) + Y(n-1). Lemma 2.24 of JonesMatijasevic p. 697 restricted to NN . (Contributed by Stefan O'Rear, 3-Oct-2014)

Ref Expression
Assertion jm2.24nn ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) < ( 𝐴 Xrm 𝑁 ) )

Proof

Step Hyp Ref Expression
1 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
2 1z ⊢ 1 ∈ ℤ
3 zsubcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 𝑁 − 1 ) ∈ ℤ )
4 1 2 3 sylancl ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℤ )
5 frmy ⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
6 5 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 − 1 ) ) ∈ ℤ )
7 4 6 sylan2 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm ( 𝑁 − 1 ) ) ∈ ℤ )
8 7 zred ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm ( 𝑁 − 1 ) ) ∈ ℝ )
9 5 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
10 1 9 sylan2 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
11 10 zred ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℝ )
12 8 11 readdcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) ∈ ℝ )
13 2re ⊢ 2 ∈ ℝ
14 remulcl ⊢ ( ( 2 ∈ ℝ ∧ ( 𝐴 Yrm 𝑁 ) ∈ ℝ ) → ( 2 · ( 𝐴 Yrm 𝑁 ) ) ∈ ℝ )
15 13 11 14 sylancr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 2 · ( 𝐴 Yrm 𝑁 ) ) ∈ ℝ )
16 15 8 resubcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 2 · ( 𝐴 Yrm 𝑁 ) ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) ∈ ℝ )
17 frmx ⊢ Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0
18 17 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 )
19 1 18 sylan2 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 )
20 19 nn0red ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℝ )
21 11 8 resubcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Yrm 𝑁 ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) ∈ ℝ )
22 remulcl ⊢ ( ( 2 ∈ ℝ ∧ ( 𝐴 Yrm ( 𝑁 − 1 ) ) ∈ ℝ ) → ( 2 · ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) ∈ ℝ )
23 13 8 22 sylancr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 2 · ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) ∈ ℝ )
24 eluzelre ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℝ )
25 24 adantr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 𝐴 ∈ ℝ )
26 25 8 remulcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 · ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) ∈ ℝ )
27 8 25 remulcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) · 𝐴 ) ∈ ℝ )
28 17 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( 𝐴 Xrm ( 𝑁 − 1 ) ) ∈ ℕ0 )
29 4 28 sylan2 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Xrm ( 𝑁 − 1 ) ) ∈ ℕ0 )
30 29 nn0red ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Xrm ( 𝑁 − 1 ) ) ∈ ℝ )
31 27 30 readdcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) · 𝐴 ) + ( 𝐴 Xrm ( 𝑁 − 1 ) ) ) ∈ ℝ )
32 13 a1i ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 2 ∈ ℝ )
33 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
34 rmxypos ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 − 1 ) ∈ ℕ0 ) → ( 0 < ( 𝐴 Xrm ( 𝑁 − 1 ) ) ∧ 0 ≤ ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) )
35 34 simprd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 − 1 ) ∈ ℕ0 ) → 0 ≤ ( 𝐴 Yrm ( 𝑁 − 1 ) ) )
36 33 35 sylan2 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 0 ≤ ( 𝐴 Yrm ( 𝑁 − 1 ) ) )
37 eluzle ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ 𝐴 )
38 37 adantr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 2 ≤ 𝐴 )
39 32 25 8 36 38 lemul1ad ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 2 · ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) ≤ ( 𝐴 · ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) )
40 25 recnd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 𝐴 ∈ ℂ )
41 8 recnd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm ( 𝑁 − 1 ) ) ∈ ℂ )
42 40 41 mulcomd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 · ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) = ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) · 𝐴 ) )
43 34 simpld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 − 1 ) ∈ ℕ0 ) → 0 < ( 𝐴 Xrm ( 𝑁 − 1 ) ) )
44 33 43 sylan2 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 0 < ( 𝐴 Xrm ( 𝑁 − 1 ) ) )
45 30 27 ltaddposd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 0 < ( 𝐴 Xrm ( 𝑁 − 1 ) ) ↔ ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) · 𝐴 ) < ( ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) · 𝐴 ) + ( 𝐴 Xrm ( 𝑁 − 1 ) ) ) ) )
46 44 45 mpbid ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) · 𝐴 ) < ( ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) · 𝐴 ) + ( 𝐴 Xrm ( 𝑁 − 1 ) ) ) )
47 42 46 eqbrtrd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 · ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) < ( ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) · 𝐴 ) + ( 𝐴 Xrm ( 𝑁 − 1 ) ) ) )
48 23 26 31 39 47 lelttrd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 2 · ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) < ( ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) · 𝐴 ) + ( 𝐴 Xrm ( 𝑁 − 1 ) ) ) )
49 41 2timesd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 2 · ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) = ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) )
50 rmyp1 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( 𝐴 Yrm ( ( 𝑁 − 1 ) + 1 ) ) = ( ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) · 𝐴 ) + ( 𝐴 Xrm ( 𝑁 − 1 ) ) ) )
51 4 50 sylan2 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm ( ( 𝑁 − 1 ) + 1 ) ) = ( ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) · 𝐴 ) + ( 𝐴 Xrm ( 𝑁 − 1 ) ) ) )
52 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
53 52 adantl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℝ )
54 53 recnd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℂ )
55 ax-1cn ⊢ 1 ∈ ℂ
56 npcan ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
57 54 55 56 sylancl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
58 57 oveq2d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm ( ( 𝑁 − 1 ) + 1 ) ) = ( 𝐴 Yrm 𝑁 ) )
59 51 58 eqtr3d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) · 𝐴 ) + ( 𝐴 Xrm ( 𝑁 − 1 ) ) ) = ( 𝐴 Yrm 𝑁 ) )
60 48 49 59 3brtr3d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) < ( 𝐴 Yrm 𝑁 ) )
61 8 8 11 ltaddsubd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) < ( 𝐴 Yrm 𝑁 ) ↔ ( 𝐴 Yrm ( 𝑁 − 1 ) ) < ( ( 𝐴 Yrm 𝑁 ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) ) )
62 60 61 mpbid ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm ( 𝑁 − 1 ) ) < ( ( 𝐴 Yrm 𝑁 ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) )
63 8 21 11 62 ltadd1dd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) < ( ( ( 𝐴 Yrm 𝑁 ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) + ( 𝐴 Yrm 𝑁 ) ) )
64 11 recnd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℂ )
65 64 2timesd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 2 · ( 𝐴 Yrm 𝑁 ) ) = ( ( 𝐴 Yrm 𝑁 ) + ( 𝐴 Yrm 𝑁 ) ) )
66 65 oveq1d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 2 · ( 𝐴 Yrm 𝑁 ) ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) = ( ( ( 𝐴 Yrm 𝑁 ) + ( 𝐴 Yrm 𝑁 ) ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) )
67 64 64 41 addsubd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 Yrm 𝑁 ) + ( 𝐴 Yrm 𝑁 ) ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) = ( ( ( 𝐴 Yrm 𝑁 ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) + ( 𝐴 Yrm 𝑁 ) ) )
68 66 67 eqtrd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 2 · ( 𝐴 Yrm 𝑁 ) ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) = ( ( ( 𝐴 Yrm 𝑁 ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) + ( 𝐴 Yrm 𝑁 ) ) )
69 63 68 breqtrrd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) < ( ( 2 · ( 𝐴 Yrm 𝑁 ) ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) )
70 25 11 remulcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 · ( 𝐴 Yrm 𝑁 ) ) ∈ ℝ )
71 rmy0 ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm 0 ) = 0 )
72 71 adantr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm 0 ) = 0 )
73 nngt0 ⊢ ( 𝑁 ∈ ℕ → 0 < 𝑁 )
74 73 adantl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 0 < 𝑁 )
75 simpl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
76 0zd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 0 ∈ ℤ )
77 1 adantl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℤ )
78 ltrmy ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 < 𝑁 ↔ ( 𝐴 Yrm 0 ) < ( 𝐴 Yrm 𝑁 ) ) )
79 75 76 77 78 syl3anc ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 0 < 𝑁 ↔ ( 𝐴 Yrm 0 ) < ( 𝐴 Yrm 𝑁 ) ) )
80 74 79 mpbid ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm 0 ) < ( 𝐴 Yrm 𝑁 ) )
81 72 80 eqbrtrrd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 0 < ( 𝐴 Yrm 𝑁 ) )
82 lemul1 ⊢ ( ( 2 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ( ( 𝐴 Yrm 𝑁 ) ∈ ℝ ∧ 0 < ( 𝐴 Yrm 𝑁 ) ) ) → ( 2 ≤ 𝐴 ↔ ( 2 · ( 𝐴 Yrm 𝑁 ) ) ≤ ( 𝐴 · ( 𝐴 Yrm 𝑁 ) ) ) )
83 32 25 11 81 82 syl112anc ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 2 ≤ 𝐴 ↔ ( 2 · ( 𝐴 Yrm 𝑁 ) ) ≤ ( 𝐴 · ( 𝐴 Yrm 𝑁 ) ) ) )
84 38 83 mpbid ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 2 · ( 𝐴 Yrm 𝑁 ) ) ≤ ( 𝐴 · ( 𝐴 Yrm 𝑁 ) ) )
85 15 70 8 84 lesub1dd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 2 · ( 𝐴 Yrm 𝑁 ) ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) ≤ ( ( 𝐴 · ( 𝐴 Yrm 𝑁 ) ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) )
86 rmym1 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 − 1 ) ) = ( ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) − ( 𝐴 Xrm 𝑁 ) ) )
87 1 86 sylan2 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm ( 𝑁 − 1 ) ) = ( ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) − ( 𝐴 Xrm 𝑁 ) ) )
88 64 40 mulcomd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) = ( 𝐴 · ( 𝐴 Yrm 𝑁 ) ) )
89 88 oveq1d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) − ( 𝐴 Xrm 𝑁 ) ) = ( ( 𝐴 · ( 𝐴 Yrm 𝑁 ) ) − ( 𝐴 Xrm 𝑁 ) ) )
90 87 89 eqtr2d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 · ( 𝐴 Yrm 𝑁 ) ) − ( 𝐴 Xrm 𝑁 ) ) = ( 𝐴 Yrm ( 𝑁 − 1 ) ) )
91 70 recnd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 · ( 𝐴 Yrm 𝑁 ) ) ∈ ℂ )
92 20 recnd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℂ )
93 subsub23 ⊢ ( ( ( 𝐴 · ( 𝐴 Yrm 𝑁 ) ) ∈ ℂ ∧ ( 𝐴 Xrm 𝑁 ) ∈ ℂ ∧ ( 𝐴 Yrm ( 𝑁 − 1 ) ) ∈ ℂ ) → ( ( ( 𝐴 · ( 𝐴 Yrm 𝑁 ) ) − ( 𝐴 Xrm 𝑁 ) ) = ( 𝐴 Yrm ( 𝑁 − 1 ) ) ↔ ( ( 𝐴 · ( 𝐴 Yrm 𝑁 ) ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) = ( 𝐴 Xrm 𝑁 ) ) )
94 91 92 41 93 syl3anc ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 · ( 𝐴 Yrm 𝑁 ) ) − ( 𝐴 Xrm 𝑁 ) ) = ( 𝐴 Yrm ( 𝑁 − 1 ) ) ↔ ( ( 𝐴 · ( 𝐴 Yrm 𝑁 ) ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) = ( 𝐴 Xrm 𝑁 ) ) )
95 90 94 mpbid ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 · ( 𝐴 Yrm 𝑁 ) ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) = ( 𝐴 Xrm 𝑁 ) )
96 85 95 breqtrd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 2 · ( 𝐴 Yrm 𝑁 ) ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) ≤ ( 𝐴 Xrm 𝑁 ) )
97 12 16 20 69 96 ltletrd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Yrm ( 𝑁 − 1 ) ) + ( 𝐴 Yrm 𝑁 ) ) < ( 𝐴 Xrm 𝑁 ) )