Metamath Proof Explorer

Theorem jm3.1lem2

Description: Lemma for jm3.1 . (Contributed by Stefan O'Rear, 16-Oct-2014)

Ref Expression
Hypotheses jm3.1.a ⊢ ( 𝜑 → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
jm3.1.b ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 2 ) )
jm3.1.c ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
jm3.1.d ⊢ ( 𝜑 → ( 𝐾 Yrm ( 𝑁 + 1 ) ) ≤ 𝐴 )
Assertion jm3.1lem2 ( 𝜑 → ( 𝐾 ↑ 𝑁 ) < ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) )

Proof

Step Hyp Ref Expression
1 jm3.1.a ⊢ ( 𝜑 → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
2 jm3.1.b ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 2 ) )
3 jm3.1.c ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 jm3.1.d ⊢ ( 𝜑 → ( 𝐾 Yrm ( 𝑁 + 1 ) ) ≤ 𝐴 )
5 eluzelre ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) → 𝐾 ∈ ℝ )
6 2 5 syl ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
7 3 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
8 6 7 reexpcld ⊢ ( 𝜑 → ( 𝐾 ↑ 𝑁 ) ∈ ℝ )
9 eluzelre ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℝ )
10 1 9 syl ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
11 2re ⊢ 2 ∈ ℝ
12 remulcl ⊢ ( ( 2 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 2 · 𝐴 ) ∈ ℝ )
13 11 10 12 sylancr ⊢ ( 𝜑 → ( 2 · 𝐴 ) ∈ ℝ )
14 13 6 remulcld ⊢ ( 𝜑 → ( ( 2 · 𝐴 ) · 𝐾 ) ∈ ℝ )
15 6 resqcld ⊢ ( 𝜑 → ( 𝐾 ↑ 2 ) ∈ ℝ )
16 14 15 resubcld ⊢ ( 𝜑 → ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) ∈ ℝ )
17 1re ⊢ 1 ∈ ℝ
18 resubcl ⊢ ( ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) ∈ ℝ )
19 16 17 18 sylancl ⊢ ( 𝜑 → ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) ∈ ℝ )
20 1 2 3 4 jm3.1lem1 ⊢ ( 𝜑 → ( 𝐾 ↑ 𝑁 ) < 𝐴 )
21 10 6 remulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐾 ) ∈ ℝ )
22 resubcl ⊢ ( ( 𝐾 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝐾 − 1 ) ∈ ℝ )
23 6 17 22 sylancl ⊢ ( 𝜑 → ( 𝐾 − 1 ) ∈ ℝ )
24 21 23 readdcld ⊢ ( 𝜑 → ( ( 𝐴 · 𝐾 ) + ( 𝐾 − 1 ) ) ∈ ℝ )
25 eluz2b1 ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝐾 ∈ ℤ ∧ 1 < 𝐾 ) )
26 25 simprbi ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝐾 )
27 2 26 syl ⊢ ( 𝜑 → 1 < 𝐾 )
28 eluz2nn ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℕ )
29 1 28 syl ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
30 29 nngt0d ⊢ ( 𝜑 → 0 < 𝐴 )
31 ltmulgt11 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 0 < 𝐴 ) → ( 1 < 𝐾 ↔ 𝐴 < ( 𝐴 · 𝐾 ) ) )
32 10 6 30 31 syl3anc ⊢ ( 𝜑 → ( 1 < 𝐾 ↔ 𝐴 < ( 𝐴 · 𝐾 ) ) )
33 27 32 mpbid ⊢ ( 𝜑 → 𝐴 < ( 𝐴 · 𝐾 ) )
34 uz2m1nn ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐾 − 1 ) ∈ ℕ )
35 2 34 syl ⊢ ( 𝜑 → ( 𝐾 − 1 ) ∈ ℕ )
36 35 nnrpd ⊢ ( 𝜑 → ( 𝐾 − 1 ) ∈ ℝ+ )
37 21 36 ltaddrpd ⊢ ( 𝜑 → ( 𝐴 · 𝐾 ) < ( ( 𝐴 · 𝐾 ) + ( 𝐾 − 1 ) ) )
38 10 21 24 33 37 lttrd ⊢ ( 𝜑 → 𝐴 < ( ( 𝐴 · 𝐾 ) + ( 𝐾 − 1 ) ) )
39 peano2re ⊢ ( 𝐾 ∈ ℝ → ( 𝐾 + 1 ) ∈ ℝ )
40 6 39 syl ⊢ ( 𝜑 → ( 𝐾 + 1 ) ∈ ℝ )
41 40 6 remulcld ⊢ ( 𝜑 → ( ( 𝐾 + 1 ) · 𝐾 ) ∈ ℝ )
42 resubcl ⊢ ( ( ( 𝐴 · 𝐾 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 𝐴 · 𝐾 ) − 1 ) ∈ ℝ )
43 21 17 42 sylancl ⊢ ( 𝜑 → ( ( 𝐴 · 𝐾 ) − 1 ) ∈ ℝ )
44 43 15 resubcld ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐾 ) − 1 ) − ( 𝐾 ↑ 2 ) ) ∈ ℝ )
45 6 recnd ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
46 45 exp1d ⊢ ( 𝜑 → ( 𝐾 ↑ 1 ) = 𝐾 )
47 eluz2nn ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) → 𝐾 ∈ ℕ )
48 2 47 syl ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
49 48 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝐾 )
50 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
51 3 50 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
52 6 49 51 leexp2ad ⊢ ( 𝜑 → ( 𝐾 ↑ 1 ) ≤ ( 𝐾 ↑ 𝑁 ) )
53 46 52 eqbrtrrd ⊢ ( 𝜑 → 𝐾 ≤ ( 𝐾 ↑ 𝑁 ) )
54 6 8 10 53 20 lelttrd ⊢ ( 𝜑 → 𝐾 < 𝐴 )
55 eluzelz ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) → 𝐾 ∈ ℤ )
56 2 55 syl ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
57 eluzelz ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℤ )
58 1 57 syl ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
59 zltp1le ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 𝐾 < 𝐴 ↔ ( 𝐾 + 1 ) ≤ 𝐴 ) )
60 56 58 59 syl2anc ⊢ ( 𝜑 → ( 𝐾 < 𝐴 ↔ ( 𝐾 + 1 ) ≤ 𝐴 ) )
61 54 60 mpbid ⊢ ( 𝜑 → ( 𝐾 + 1 ) ≤ 𝐴 )
62 48 nngt0d ⊢ ( 𝜑 → 0 < 𝐾 )
63 lemul1 ⊢ ( ( ( 𝐾 + 1 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ( 𝐾 ∈ ℝ ∧ 0 < 𝐾 ) ) → ( ( 𝐾 + 1 ) ≤ 𝐴 ↔ ( ( 𝐾 + 1 ) · 𝐾 ) ≤ ( 𝐴 · 𝐾 ) ) )
64 40 10 6 62 63 syl112anc ⊢ ( 𝜑 → ( ( 𝐾 + 1 ) ≤ 𝐴 ↔ ( ( 𝐾 + 1 ) · 𝐾 ) ≤ ( 𝐴 · 𝐾 ) ) )
65 61 64 mpbid ⊢ ( 𝜑 → ( ( 𝐾 + 1 ) · 𝐾 ) ≤ ( 𝐴 · 𝐾 ) )
66 41 21 44 65 leadd1dd ⊢ ( 𝜑 → ( ( ( 𝐾 + 1 ) · 𝐾 ) + ( ( ( 𝐴 · 𝐾 ) − 1 ) − ( 𝐾 ↑ 2 ) ) ) ≤ ( ( 𝐴 · 𝐾 ) + ( ( ( 𝐴 · 𝐾 ) − 1 ) − ( 𝐾 ↑ 2 ) ) ) )
67 21 recnd ⊢ ( 𝜑 → ( 𝐴 · 𝐾 ) ∈ ℂ )
68 41 15 resubcld ⊢ ( 𝜑 → ( ( ( 𝐾 + 1 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) ∈ ℝ )
69 68 recnd ⊢ ( 𝜑 → ( ( ( 𝐾 + 1 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) ∈ ℂ )
70 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
71 67 69 70 addsub12d ⊢ ( 𝜑 → ( ( 𝐴 · 𝐾 ) + ( ( ( ( 𝐾 + 1 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) ) = ( ( ( ( 𝐾 + 1 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) + ( ( 𝐴 · 𝐾 ) − 1 ) ) )
72 45 70 45 adddird ⊢ ( 𝜑 → ( ( 𝐾 + 1 ) · 𝐾 ) = ( ( 𝐾 · 𝐾 ) + ( 1 · 𝐾 ) ) )
73 45 sqvald ⊢ ( 𝜑 → ( 𝐾 ↑ 2 ) = ( 𝐾 · 𝐾 ) )
74 72 73 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐾 + 1 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) = ( ( ( 𝐾 · 𝐾 ) + ( 1 · 𝐾 ) ) − ( 𝐾 · 𝐾 ) ) )
75 45 45 mulcld ⊢ ( 𝜑 → ( 𝐾 · 𝐾 ) ∈ ℂ )
76 ax-1cn ⊢ 1 ∈ ℂ
77 mulcl ⊢ ( ( 1 ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( 1 · 𝐾 ) ∈ ℂ )
78 76 45 77 sylancr ⊢ ( 𝜑 → ( 1 · 𝐾 ) ∈ ℂ )
79 75 78 pncan2d ⊢ ( 𝜑 → ( ( ( 𝐾 · 𝐾 ) + ( 1 · 𝐾 ) ) − ( 𝐾 · 𝐾 ) ) = ( 1 · 𝐾 ) )
80 45 mulid2d ⊢ ( 𝜑 → ( 1 · 𝐾 ) = 𝐾 )
81 74 79 80 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝐾 + 1 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) = 𝐾 )
82 81 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝐾 + 1 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) = ( 𝐾 − 1 ) )
83 82 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 · 𝐾 ) + ( ( ( ( 𝐾 + 1 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) ) = ( ( 𝐴 · 𝐾 ) + ( 𝐾 − 1 ) ) )
84 41 recnd ⊢ ( 𝜑 → ( ( 𝐾 + 1 ) · 𝐾 ) ∈ ℂ )
85 15 recnd ⊢ ( 𝜑 → ( 𝐾 ↑ 2 ) ∈ ℂ )
86 43 recnd ⊢ ( 𝜑 → ( ( 𝐴 · 𝐾 ) − 1 ) ∈ ℂ )
87 84 85 86 subadd23d ⊢ ( 𝜑 → ( ( ( ( 𝐾 + 1 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) + ( ( 𝐴 · 𝐾 ) − 1 ) ) = ( ( ( 𝐾 + 1 ) · 𝐾 ) + ( ( ( 𝐴 · 𝐾 ) − 1 ) − ( 𝐾 ↑ 2 ) ) ) )
88 71 83 87 3eqtr3d ⊢ ( 𝜑 → ( ( 𝐴 · 𝐾 ) + ( 𝐾 − 1 ) ) = ( ( ( 𝐾 + 1 ) · 𝐾 ) + ( ( ( 𝐴 · 𝐾 ) − 1 ) − ( 𝐾 ↑ 2 ) ) ) )
89 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
90 10 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
91 89 90 45 mulassd ⊢ ( 𝜑 → ( ( 2 · 𝐴 ) · 𝐾 ) = ( 2 · ( 𝐴 · 𝐾 ) ) )
92 67 2timesd ⊢ ( 𝜑 → ( 2 · ( 𝐴 · 𝐾 ) ) = ( ( 𝐴 · 𝐾 ) + ( 𝐴 · 𝐾 ) ) )
93 91 92 eqtrd ⊢ ( 𝜑 → ( ( 2 · 𝐴 ) · 𝐾 ) = ( ( 𝐴 · 𝐾 ) + ( 𝐴 · 𝐾 ) ) )
94 93 oveq1d ⊢ ( 𝜑 → ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) = ( ( ( 𝐴 · 𝐾 ) + ( 𝐴 · 𝐾 ) ) − ( 𝐾 ↑ 2 ) ) )
95 94 oveq1d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) = ( ( ( ( 𝐴 · 𝐾 ) + ( 𝐴 · 𝐾 ) ) − ( 𝐾 ↑ 2 ) ) − 1 ) )
96 21 21 readdcld ⊢ ( 𝜑 → ( ( 𝐴 · 𝐾 ) + ( 𝐴 · 𝐾 ) ) ∈ ℝ )
97 96 recnd ⊢ ( 𝜑 → ( ( 𝐴 · 𝐾 ) + ( 𝐴 · 𝐾 ) ) ∈ ℂ )
98 97 85 70 sub32d ⊢ ( 𝜑 → ( ( ( ( 𝐴 · 𝐾 ) + ( 𝐴 · 𝐾 ) ) − ( 𝐾 ↑ 2 ) ) − 1 ) = ( ( ( ( 𝐴 · 𝐾 ) + ( 𝐴 · 𝐾 ) ) − 1 ) − ( 𝐾 ↑ 2 ) ) )
99 67 67 70 addsubassd ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐾 ) + ( 𝐴 · 𝐾 ) ) − 1 ) = ( ( 𝐴 · 𝐾 ) + ( ( 𝐴 · 𝐾 ) − 1 ) ) )
100 99 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝐴 · 𝐾 ) + ( 𝐴 · 𝐾 ) ) − 1 ) − ( 𝐾 ↑ 2 ) ) = ( ( ( 𝐴 · 𝐾 ) + ( ( 𝐴 · 𝐾 ) − 1 ) ) − ( 𝐾 ↑ 2 ) ) )
101 67 86 85 addsubassd ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐾 ) + ( ( 𝐴 · 𝐾 ) − 1 ) ) − ( 𝐾 ↑ 2 ) ) = ( ( 𝐴 · 𝐾 ) + ( ( ( 𝐴 · 𝐾 ) − 1 ) − ( 𝐾 ↑ 2 ) ) ) )
102 100 101 eqtrd ⊢ ( 𝜑 → ( ( ( ( 𝐴 · 𝐾 ) + ( 𝐴 · 𝐾 ) ) − 1 ) − ( 𝐾 ↑ 2 ) ) = ( ( 𝐴 · 𝐾 ) + ( ( ( 𝐴 · 𝐾 ) − 1 ) − ( 𝐾 ↑ 2 ) ) ) )
103 95 98 102 3eqtrd ⊢ ( 𝜑 → ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) = ( ( 𝐴 · 𝐾 ) + ( ( ( 𝐴 · 𝐾 ) − 1 ) − ( 𝐾 ↑ 2 ) ) ) )
104 66 88 103 3brtr4d ⊢ ( 𝜑 → ( ( 𝐴 · 𝐾 ) + ( 𝐾 − 1 ) ) ≤ ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) )
105 10 24 19 38 104 ltletrd ⊢ ( 𝜑 → 𝐴 < ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) )
106 8 10 19 20 105 lttrd ⊢ ( 𝜑 → ( 𝐾 ↑ 𝑁 ) < ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) )