Metamath Proof Explorer

Theorem expmulnbnd

Description: Exponentiation with a mantissa greater than 1 is not bounded by any linear function. (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Assertion expmulnbnd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ∃ 𝑗 ∈ ℕ0 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐴 · 𝑘 ) < ( 𝐵 ↑ 𝑘 ) )

Proof

Step Hyp Ref Expression
1 2re ⊢ 2 ∈ ℝ
2 simp1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → 𝐴 ∈ ℝ )
3 remulcl ⊢ ( ( 2 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 2 · 𝐴 ) ∈ ℝ )
4 1 2 3 sylancr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( 2 · 𝐴 ) ∈ ℝ )
5 simp3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → 1 < 𝐵 )
6 1re ⊢ 1 ∈ ℝ
7 simp2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → 𝐵 ∈ ℝ )
8 difrp ⊢ ( ( 1 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 1 < 𝐵 ↔ ( 𝐵 − 1 ) ∈ ℝ+ ) )
9 6 7 8 sylancr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( 1 < 𝐵 ↔ ( 𝐵 − 1 ) ∈ ℝ+ ) )
10 5 9 mpbid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( 𝐵 − 1 ) ∈ ℝ+ )
11 4 10 rerpdivcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) ∈ ℝ )
12 expnbnd ⊢ ( ( ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ∃ 𝑛 ∈ ℕ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) )
13 11 7 5 12 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ∃ 𝑛 ∈ ℕ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) )
14 2nn0 ⊢ 2 ∈ ℕ0
15 nnnn0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
16 15 ad2antrl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) → 𝑛 ∈ ℕ0 )
17 nn0mulcl ⊢ ( ( 2 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 2 · 𝑛 ) ∈ ℕ0 )
18 14 16 17 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) → ( 2 · 𝑛 ) ∈ ℕ0 )
19 2 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 𝐴 ∈ ℝ )
20 2nn ⊢ 2 ∈ ℕ
21 simprl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) → 𝑛 ∈ ℕ )
22 nnmulcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → ( 2 · 𝑛 ) ∈ ℕ )
23 20 21 22 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) → ( 2 · 𝑛 ) ∈ ℕ )
24 eluznn ⊢ ( ( ( 2 · 𝑛 ) ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 𝑘 ∈ ℕ )
25 23 24 sylan ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 𝑘 ∈ ℕ )
26 25 nnred ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 𝑘 ∈ ℝ )
27 19 26 remulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 𝐴 · 𝑘 ) ∈ ℝ )
28 0re ⊢ 0 ∈ ℝ
29 ifcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ∈ ℝ )
30 19 28 29 sylancl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ∈ ℝ )
31 remulcl ⊢ ( ( 2 ∈ ℝ ∧ if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ∈ ℝ ) → ( 2 · if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) ∈ ℝ )
32 1 30 31 sylancr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 2 · if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) ∈ ℝ )
33 simplrl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 𝑛 ∈ ℕ )
34 33 nnred ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 𝑛 ∈ ℝ )
35 26 34 resubcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 𝑘 − 𝑛 ) ∈ ℝ )
36 32 35 remulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( ( 2 · if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) · ( 𝑘 − 𝑛 ) ) ∈ ℝ )
37 7 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 𝐵 ∈ ℝ )
38 25 nnnn0d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 𝑘 ∈ ℕ0 )
39 reexpcl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐵 ↑ 𝑘 ) ∈ ℝ )
40 37 38 39 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 𝐵 ↑ 𝑘 ) ∈ ℝ )
41 remulcl ⊢ ( ( 2 ∈ ℝ ∧ ( 𝑘 − 𝑛 ) ∈ ℝ ) → ( 2 · ( 𝑘 − 𝑛 ) ) ∈ ℝ )
42 1 35 41 sylancr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 2 · ( 𝑘 − 𝑛 ) ) ∈ ℝ )
43 38 nn0ge0d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 0 ≤ 𝑘 )
44 max1 ⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → 0 ≤ if ( 0 ≤ 𝐴 , 𝐴 , 0 ) )
45 28 19 44 sylancr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 0 ≤ if ( 0 ≤ 𝐴 , 𝐴 , 0 ) )
46 remulcl ⊢ ( ( 2 ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ( 2 · 𝑛 ) ∈ ℝ )
47 1 34 46 sylancr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 2 · 𝑛 ) ∈ ℝ )
48 eluzle ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) → ( 2 · 𝑛 ) ≤ 𝑘 )
49 48 adantl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 2 · 𝑛 ) ≤ 𝑘 )
50 47 26 26 49 leadd2dd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 𝑘 + ( 2 · 𝑛 ) ) ≤ ( 𝑘 + 𝑘 ) )
51 26 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 𝑘 ∈ ℂ )
52 51 2timesd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 2 · 𝑘 ) = ( 𝑘 + 𝑘 ) )
53 50 52 breqtrrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 𝑘 + ( 2 · 𝑛 ) ) ≤ ( 2 · 𝑘 ) )
54 remulcl ⊢ ( ( 2 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 2 · 𝑘 ) ∈ ℝ )
55 1 26 54 sylancr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 2 · 𝑘 ) ∈ ℝ )
56 leaddsub ⊢ ( ( 𝑘 ∈ ℝ ∧ ( 2 · 𝑛 ) ∈ ℝ ∧ ( 2 · 𝑘 ) ∈ ℝ ) → ( ( 𝑘 + ( 2 · 𝑛 ) ) ≤ ( 2 · 𝑘 ) ↔ 𝑘 ≤ ( ( 2 · 𝑘 ) − ( 2 · 𝑛 ) ) ) )
57 26 47 55 56 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( ( 𝑘 + ( 2 · 𝑛 ) ) ≤ ( 2 · 𝑘 ) ↔ 𝑘 ≤ ( ( 2 · 𝑘 ) − ( 2 · 𝑛 ) ) ) )
58 53 57 mpbid ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 𝑘 ≤ ( ( 2 · 𝑘 ) − ( 2 · 𝑛 ) ) )
59 2cnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 2 ∈ ℂ )
60 34 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 𝑛 ∈ ℂ )
61 59 51 60 subdid ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 2 · ( 𝑘 − 𝑛 ) ) = ( ( 2 · 𝑘 ) − ( 2 · 𝑛 ) ) )
62 58 61 breqtrrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 𝑘 ≤ ( 2 · ( 𝑘 − 𝑛 ) ) )
63 max2 ⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → 𝐴 ≤ if ( 0 ≤ 𝐴 , 𝐴 , 0 ) )
64 28 19 63 sylancr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 𝐴 ≤ if ( 0 ≤ 𝐴 , 𝐴 , 0 ) )
65 26 42 19 30 43 45 62 64 lemul12bd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 𝑘 · 𝐴 ) ≤ ( ( 2 · ( 𝑘 − 𝑛 ) ) · if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) )
66 19 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 𝐴 ∈ ℂ )
67 66 51 mulcomd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 𝐴 · 𝑘 ) = ( 𝑘 · 𝐴 ) )
68 30 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ∈ ℂ )
69 35 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 𝑘 − 𝑛 ) ∈ ℂ )
70 59 68 69 mul32d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( ( 2 · if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) · ( 𝑘 − 𝑛 ) ) = ( ( 2 · ( 𝑘 − 𝑛 ) ) · if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) )
71 65 67 70 3brtr4d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 𝐴 · 𝑘 ) ≤ ( ( 2 · if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) · ( 𝑘 − 𝑛 ) ) )
72 10 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 𝐵 − 1 ) ∈ ℝ+ )
73 72 rpred ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 𝐵 − 1 ) ∈ ℝ )
74 73 35 remulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( ( 𝐵 − 1 ) · ( 𝑘 − 𝑛 ) ) ∈ ℝ )
75 33 nnnn0d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 𝑛 ∈ ℕ0 )
76 reexpcl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑛 ∈ ℕ0 ) → ( 𝐵 ↑ 𝑛 ) ∈ ℝ )
77 37 75 76 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 𝐵 ↑ 𝑛 ) ∈ ℝ )
78 74 77 remulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( ( ( 𝐵 − 1 ) · ( 𝑘 − 𝑛 ) ) · ( 𝐵 ↑ 𝑛 ) ) ∈ ℝ )
79 simplrr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) )
80 1 19 3 sylancr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 2 · 𝐴 ) ∈ ℝ )
81 80 77 72 ltdivmuld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ↔ ( 2 · 𝐴 ) < ( ( 𝐵 − 1 ) · ( 𝐵 ↑ 𝑛 ) ) ) )
82 79 81 mpbid ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 2 · 𝐴 ) < ( ( 𝐵 − 1 ) · ( 𝐵 ↑ 𝑛 ) ) )
83 5 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 1 < 𝐵 )
84 posdif ⊢ ( ( 1 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 1 < 𝐵 ↔ 0 < ( 𝐵 − 1 ) ) )
85 6 37 84 sylancr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 1 < 𝐵 ↔ 0 < ( 𝐵 − 1 ) ) )
86 83 85 mpbid ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 0 < ( 𝐵 − 1 ) )
87 33 nnzd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 𝑛 ∈ ℤ )
88 28 a1i ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 0 ∈ ℝ )
89 6 a1i ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 1 ∈ ℝ )
90 0lt1 ⊢ 0 < 1
91 90 a1i ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 0 < 1 )
92 88 89 37 91 83 lttrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 0 < 𝐵 )
93 expgt0 ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑛 ∈ ℤ ∧ 0 < 𝐵 ) → 0 < ( 𝐵 ↑ 𝑛 ) )
94 37 87 92 93 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 0 < ( 𝐵 ↑ 𝑛 ) )
95 73 77 86 94 mulgt0d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 0 < ( ( 𝐵 − 1 ) · ( 𝐵 ↑ 𝑛 ) ) )
96 oveq2 ⊢ ( 𝐴 = if ( 0 ≤ 𝐴 , 𝐴 , 0 ) → ( 2 · 𝐴 ) = ( 2 · if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) )
97 96 breq1d ⊢ ( 𝐴 = if ( 0 ≤ 𝐴 , 𝐴 , 0 ) → ( ( 2 · 𝐴 ) < ( ( 𝐵 − 1 ) · ( 𝐵 ↑ 𝑛 ) ) ↔ ( 2 · if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) < ( ( 𝐵 − 1 ) · ( 𝐵 ↑ 𝑛 ) ) ) )
98 2t0e0 ⊢ ( 2 · 0 ) = 0
99 oveq2 ⊢ ( 0 = if ( 0 ≤ 𝐴 , 𝐴 , 0 ) → ( 2 · 0 ) = ( 2 · if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) )
100 98 99 syl5eqr ⊢ ( 0 = if ( 0 ≤ 𝐴 , 𝐴 , 0 ) → 0 = ( 2 · if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) )
101 100 breq1d ⊢ ( 0 = if ( 0 ≤ 𝐴 , 𝐴 , 0 ) → ( 0 < ( ( 𝐵 − 1 ) · ( 𝐵 ↑ 𝑛 ) ) ↔ ( 2 · if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) < ( ( 𝐵 − 1 ) · ( 𝐵 ↑ 𝑛 ) ) ) )
102 97 101 ifboth ⊢ ( ( ( 2 · 𝐴 ) < ( ( 𝐵 − 1 ) · ( 𝐵 ↑ 𝑛 ) ) ∧ 0 < ( ( 𝐵 − 1 ) · ( 𝐵 ↑ 𝑛 ) ) ) → ( 2 · if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) < ( ( 𝐵 − 1 ) · ( 𝐵 ↑ 𝑛 ) ) )
103 82 95 102 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 2 · if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) < ( ( 𝐵 − 1 ) · ( 𝐵 ↑ 𝑛 ) ) )
104 73 77 remulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( ( 𝐵 − 1 ) · ( 𝐵 ↑ 𝑛 ) ) ∈ ℝ )
105 simpr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) )
106 60 2timesd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 2 · 𝑛 ) = ( 𝑛 + 𝑛 ) )
107 106 fveq2d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( ℤ≥ ‘ ( 2 · 𝑛 ) ) = ( ℤ≥ ‘ ( 𝑛 + 𝑛 ) ) )
108 105 107 eleqtrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 𝑛 ) ) )
109 eluzsub ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 𝑛 ) ) ) → ( 𝑘 − 𝑛 ) ∈ ( ℤ≥ ‘ 𝑛 ) )
110 87 87 108 109 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 𝑘 − 𝑛 ) ∈ ( ℤ≥ ‘ 𝑛 ) )
111 eluznn ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑘 − 𝑛 ) ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 𝑘 − 𝑛 ) ∈ ℕ )
112 33 110 111 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 𝑘 − 𝑛 ) ∈ ℕ )
113 112 nngt0d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 0 < ( 𝑘 − 𝑛 ) )
114 ltmul1 ⊢ ( ( ( 2 · if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) ∈ ℝ ∧ ( ( 𝐵 − 1 ) · ( 𝐵 ↑ 𝑛 ) ) ∈ ℝ ∧ ( ( 𝑘 − 𝑛 ) ∈ ℝ ∧ 0 < ( 𝑘 − 𝑛 ) ) ) → ( ( 2 · if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) < ( ( 𝐵 − 1 ) · ( 𝐵 ↑ 𝑛 ) ) ↔ ( ( 2 · if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) · ( 𝑘 − 𝑛 ) ) < ( ( ( 𝐵 − 1 ) · ( 𝐵 ↑ 𝑛 ) ) · ( 𝑘 − 𝑛 ) ) ) )
115 32 104 35 113 114 syl112anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( ( 2 · if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) < ( ( 𝐵 − 1 ) · ( 𝐵 ↑ 𝑛 ) ) ↔ ( ( 2 · if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) · ( 𝑘 − 𝑛 ) ) < ( ( ( 𝐵 − 1 ) · ( 𝐵 ↑ 𝑛 ) ) · ( 𝑘 − 𝑛 ) ) ) )
116 103 115 mpbid ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( ( 2 · if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) · ( 𝑘 − 𝑛 ) ) < ( ( ( 𝐵 − 1 ) · ( 𝐵 ↑ 𝑛 ) ) · ( 𝑘 − 𝑛 ) ) )
117 73 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 𝐵 − 1 ) ∈ ℂ )
118 77 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 𝐵 ↑ 𝑛 ) ∈ ℂ )
119 117 118 69 mul32d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( ( ( 𝐵 − 1 ) · ( 𝐵 ↑ 𝑛 ) ) · ( 𝑘 − 𝑛 ) ) = ( ( ( 𝐵 − 1 ) · ( 𝑘 − 𝑛 ) ) · ( 𝐵 ↑ 𝑛 ) ) )
120 116 119 breqtrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( ( 2 · if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) · ( 𝑘 − 𝑛 ) ) < ( ( ( 𝐵 − 1 ) · ( 𝑘 − 𝑛 ) ) · ( 𝐵 ↑ 𝑛 ) ) )
121 peano2re ⊢ ( ( ( 𝐵 − 1 ) · ( 𝑘 − 𝑛 ) ) ∈ ℝ → ( ( ( 𝐵 − 1 ) · ( 𝑘 − 𝑛 ) ) + 1 ) ∈ ℝ )
122 74 121 syl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( ( ( 𝐵 − 1 ) · ( 𝑘 − 𝑛 ) ) + 1 ) ∈ ℝ )
123 112 nnnn0d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 𝑘 − 𝑛 ) ∈ ℕ0 )
124 reexpcl ⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝑘 − 𝑛 ) ∈ ℕ0 ) → ( 𝐵 ↑ ( 𝑘 − 𝑛 ) ) ∈ ℝ )
125 37 123 124 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 𝐵 ↑ ( 𝑘 − 𝑛 ) ) ∈ ℝ )
126 74 ltp1d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( ( 𝐵 − 1 ) · ( 𝑘 − 𝑛 ) ) < ( ( ( 𝐵 − 1 ) · ( 𝑘 − 𝑛 ) ) + 1 ) )
127 88 37 92 ltled ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 0 ≤ 𝐵 )
128 bernneq2 ⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝑘 − 𝑛 ) ∈ ℕ0 ∧ 0 ≤ 𝐵 ) → ( ( ( 𝐵 − 1 ) · ( 𝑘 − 𝑛 ) ) + 1 ) ≤ ( 𝐵 ↑ ( 𝑘 − 𝑛 ) ) )
129 37 123 127 128 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( ( ( 𝐵 − 1 ) · ( 𝑘 − 𝑛 ) ) + 1 ) ≤ ( 𝐵 ↑ ( 𝑘 − 𝑛 ) ) )
130 74 122 125 126 129 ltletrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( ( 𝐵 − 1 ) · ( 𝑘 − 𝑛 ) ) < ( 𝐵 ↑ ( 𝑘 − 𝑛 ) ) )
131 37 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 𝐵 ∈ ℂ )
132 92 gt0ne0d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 𝐵 ≠ 0 )
133 eluzelz ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) → 𝑘 ∈ ℤ )
134 133 adantl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → 𝑘 ∈ ℤ )
135 expsub ⊢ ( ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ) → ( 𝐵 ↑ ( 𝑘 − 𝑛 ) ) = ( ( 𝐵 ↑ 𝑘 ) / ( 𝐵 ↑ 𝑛 ) ) )
136 131 132 134 87 135 syl22anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 𝐵 ↑ ( 𝑘 − 𝑛 ) ) = ( ( 𝐵 ↑ 𝑘 ) / ( 𝐵 ↑ 𝑛 ) ) )
137 130 136 breqtrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( ( 𝐵 − 1 ) · ( 𝑘 − 𝑛 ) ) < ( ( 𝐵 ↑ 𝑘 ) / ( 𝐵 ↑ 𝑛 ) ) )
138 ltmuldiv ⊢ ( ( ( ( 𝐵 − 1 ) · ( 𝑘 − 𝑛 ) ) ∈ ℝ ∧ ( 𝐵 ↑ 𝑘 ) ∈ ℝ ∧ ( ( 𝐵 ↑ 𝑛 ) ∈ ℝ ∧ 0 < ( 𝐵 ↑ 𝑛 ) ) ) → ( ( ( ( 𝐵 − 1 ) · ( 𝑘 − 𝑛 ) ) · ( 𝐵 ↑ 𝑛 ) ) < ( 𝐵 ↑ 𝑘 ) ↔ ( ( 𝐵 − 1 ) · ( 𝑘 − 𝑛 ) ) < ( ( 𝐵 ↑ 𝑘 ) / ( 𝐵 ↑ 𝑛 ) ) ) )
139 74 40 77 94 138 syl112anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( ( ( ( 𝐵 − 1 ) · ( 𝑘 − 𝑛 ) ) · ( 𝐵 ↑ 𝑛 ) ) < ( 𝐵 ↑ 𝑘 ) ↔ ( ( 𝐵 − 1 ) · ( 𝑘 − 𝑛 ) ) < ( ( 𝐵 ↑ 𝑘 ) / ( 𝐵 ↑ 𝑛 ) ) ) )
140 137 139 mpbird ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( ( ( 𝐵 − 1 ) · ( 𝑘 − 𝑛 ) ) · ( 𝐵 ↑ 𝑛 ) ) < ( 𝐵 ↑ 𝑘 ) )
141 36 78 40 120 140 lttrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( ( 2 · if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) · ( 𝑘 − 𝑛 ) ) < ( 𝐵 ↑ 𝑘 ) )
142 27 36 40 71 141 lelttrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ) → ( 𝐴 · 𝑘 ) < ( 𝐵 ↑ 𝑘 ) )
143 142 ralrimiva ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ( 𝐴 · 𝑘 ) < ( 𝐵 ↑ 𝑘 ) )
144 fveq2 ⊢ ( 𝑗 = ( 2 · 𝑛 ) → ( ℤ≥ ‘ 𝑗 ) = ( ℤ≥ ‘ ( 2 · 𝑛 ) ) )
145 144 raleqdv ⊢ ( 𝑗 = ( 2 · 𝑛 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐴 · 𝑘 ) < ( 𝐵 ↑ 𝑘 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ( 𝐴 · 𝑘 ) < ( 𝐵 ↑ 𝑘 ) ) )
146 145 rspcev ⊢ ( ( ( 2 · 𝑛 ) ∈ ℕ0 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ ( 2 · 𝑛 ) ) ( 𝐴 · 𝑘 ) < ( 𝐵 ↑ 𝑘 ) ) → ∃ 𝑗 ∈ ℕ0 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐴 · 𝑘 ) < ( 𝐵 ↑ 𝑘 ) )
147 18 143 146 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( 𝑛 ∈ ℕ ∧ ( ( 2 · 𝐴 ) / ( 𝐵 − 1 ) ) < ( 𝐵 ↑ 𝑛 ) ) ) → ∃ 𝑗 ∈ ℕ0 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐴 · 𝑘 ) < ( 𝐵 ↑ 𝑘 ) )
148 13 147 rexlimddv ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ∃ 𝑗 ∈ ℕ0 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐴 · 𝑘 ) < ( 𝐵 ↑ 𝑘 ) )