Metamath Proof Explorer

Theorem jm2.17c

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

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

Proof

Step Hyp Ref Expression
1 2re ⊢ 2 ∈ ℝ
2 eluzelre ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℝ )
3 2 adantr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 𝐴 ∈ ℝ )
4 remulcl ⊢ ( ( 2 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 2 · 𝐴 ) ∈ ℝ )
5 1 3 4 sylancr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 2 · 𝐴 ) ∈ ℝ )
6 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
7 6 adantl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℤ )
8 7 peano2zd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 + 1 ) ∈ ℤ )
9 frmy ⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
10 9 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 + 1 ) ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 + 1 ) ) ∈ ℤ )
11 10 zred ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 + 1 ) ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 + 1 ) ) ∈ ℝ )
12 8 11 syldan ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm ( 𝑁 + 1 ) ) ∈ ℝ )
13 5 12 remulcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑁 + 1 ) ) ) ∈ ℝ )
14 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
15 14 adantl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℂ )
16 ax-1cn ⊢ 1 ∈ ℂ
17 pncan ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
18 15 16 17 sylancl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
19 18 oveq2d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm ( ( 𝑁 + 1 ) − 1 ) ) = ( 𝐴 Yrm 𝑁 ) )
20 9 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
21 20 zred ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℝ )
22 6 21 sylan2 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℝ )
23 19 22 eqeltrd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm ( ( 𝑁 + 1 ) − 1 ) ) ∈ ℝ )
24 13 23 resubcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑁 + 1 ) ) ) − ( 𝐴 Yrm ( ( 𝑁 + 1 ) − 1 ) ) ) ∈ ℝ )
25 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
26 25 adantl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ0 )
27 5 26 reexpcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 2 · 𝐴 ) ↑ 𝑁 ) ∈ ℝ )
28 5 27 remulcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 2 · 𝐴 ) · ( ( 2 · 𝐴 ) ↑ 𝑁 ) ) ∈ ℝ )
29 rmy0 ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm 0 ) = 0 )
30 29 adantr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm 0 ) = 0 )
31 nngt0 ⊢ ( 𝑁 ∈ ℕ → 0 < 𝑁 )
32 31 adantl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 0 < 𝑁 )
33 simpl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
34 0zd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 0 ∈ ℤ )
35 ltrmy ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 < 𝑁 ↔ ( 𝐴 Yrm 0 ) < ( 𝐴 Yrm 𝑁 ) ) )
36 33 34 7 35 syl3anc ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 0 < 𝑁 ↔ ( 𝐴 Yrm 0 ) < ( 𝐴 Yrm 𝑁 ) ) )
37 32 36 mpbid ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm 0 ) < ( 𝐴 Yrm 𝑁 ) )
38 30 37 eqbrtrrd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 0 < ( 𝐴 Yrm 𝑁 ) )
39 38 19 breqtrrd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 0 < ( 𝐴 Yrm ( ( 𝑁 + 1 ) − 1 ) ) )
40 23 13 ltsubposd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 0 < ( 𝐴 Yrm ( ( 𝑁 + 1 ) − 1 ) ) ↔ ( ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑁 + 1 ) ) ) − ( 𝐴 Yrm ( ( 𝑁 + 1 ) − 1 ) ) ) < ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑁 + 1 ) ) ) ) )
41 39 40 mpbid ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑁 + 1 ) ) ) − ( 𝐴 Yrm ( ( 𝑁 + 1 ) − 1 ) ) ) < ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑁 + 1 ) ) ) )
42 jm2.17b ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 Yrm ( 𝑁 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑁 ) )
43 25 42 sylan2 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm ( 𝑁 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑁 ) )
44 2nn ⊢ 2 ∈ ℕ
45 eluz2nn ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℕ )
46 nnmulcl ⊢ ( ( 2 ∈ ℕ ∧ 𝐴 ∈ ℕ ) → ( 2 · 𝐴 ) ∈ ℕ )
47 44 45 46 sylancr ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · 𝐴 ) ∈ ℕ )
48 47 nngt0d ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 0 < ( 2 · 𝐴 ) )
49 48 adantr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 0 < ( 2 · 𝐴 ) )
50 lemul2 ⊢ ( ( ( 𝐴 Yrm ( 𝑁 + 1 ) ) ∈ ℝ ∧ ( ( 2 · 𝐴 ) ↑ 𝑁 ) ∈ ℝ ∧ ( ( 2 · 𝐴 ) ∈ ℝ ∧ 0 < ( 2 · 𝐴 ) ) ) → ( ( 𝐴 Yrm ( 𝑁 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑁 ) ↔ ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑁 + 1 ) ) ) ≤ ( ( 2 · 𝐴 ) · ( ( 2 · 𝐴 ) ↑ 𝑁 ) ) ) )
51 12 27 5 49 50 syl112anc ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 Yrm ( 𝑁 + 1 ) ) ≤ ( ( 2 · 𝐴 ) ↑ 𝑁 ) ↔ ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑁 + 1 ) ) ) ≤ ( ( 2 · 𝐴 ) · ( ( 2 · 𝐴 ) ↑ 𝑁 ) ) ) )
52 43 51 mpbid ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑁 + 1 ) ) ) ≤ ( ( 2 · 𝐴 ) · ( ( 2 · 𝐴 ) ↑ 𝑁 ) ) )
53 24 13 28 41 52 ltletrd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑁 + 1 ) ) ) − ( 𝐴 Yrm ( ( 𝑁 + 1 ) − 1 ) ) ) < ( ( 2 · 𝐴 ) · ( ( 2 · 𝐴 ) ↑ 𝑁 ) ) )
54 rmyluc2 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 + 1 ) ∈ ℤ ) → ( 𝐴 Yrm ( ( 𝑁 + 1 ) + 1 ) ) = ( ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑁 + 1 ) ) ) − ( 𝐴 Yrm ( ( 𝑁 + 1 ) − 1 ) ) ) )
55 8 54 syldan ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm ( ( 𝑁 + 1 ) + 1 ) ) = ( ( ( 2 · 𝐴 ) · ( 𝐴 Yrm ( 𝑁 + 1 ) ) ) − ( 𝐴 Yrm ( ( 𝑁 + 1 ) − 1 ) ) ) )
56 5 recnd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 2 · 𝐴 ) ∈ ℂ )
57 56 26 expp1d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 2 · 𝐴 ) ↑ ( 𝑁 + 1 ) ) = ( ( ( 2 · 𝐴 ) ↑ 𝑁 ) · ( 2 · 𝐴 ) ) )
58 27 recnd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 2 · 𝐴 ) ↑ 𝑁 ) ∈ ℂ )
59 58 56 mulcomd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( ( 2 · 𝐴 ) ↑ 𝑁 ) · ( 2 · 𝐴 ) ) = ( ( 2 · 𝐴 ) · ( ( 2 · 𝐴 ) ↑ 𝑁 ) ) )
60 57 59 eqtrd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( 2 · 𝐴 ) ↑ ( 𝑁 + 1 ) ) = ( ( 2 · 𝐴 ) · ( ( 2 · 𝐴 ) ↑ 𝑁 ) ) )
61 53 55 60 3brtr4d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐴 Yrm ( ( 𝑁 + 1 ) + 1 ) ) < ( ( 2 · 𝐴 ) ↑ ( 𝑁 + 1 ) ) )