Metamath Proof Explorer


Theorem expmulnbnd

Description: Exponentiation with a base 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 eqtr3id ( 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𝑘 ∈ ( ℤ𝑗 ) ( 𝐴 · 𝑘 ) < ( 𝐵𝑘 ) )