| Step |
Hyp |
Ref |
Expression |
| 1 |
|
2rp |
⊢ 2 ∈ ℝ+ |
| 2 |
|
rpdivcl |
⊢ ( ( 2 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( 2 / 𝐵 ) ∈ ℝ+ ) |
| 3 |
1 2
|
mpan |
⊢ ( 𝐵 ∈ ℝ+ → ( 2 / 𝐵 ) ∈ ℝ+ ) |
| 4 |
3
|
rpred |
⊢ ( 𝐵 ∈ ℝ+ → ( 2 / 𝐵 ) ∈ ℝ ) |
| 5 |
|
2re |
⊢ 2 ∈ ℝ |
| 6 |
|
1lt2 |
⊢ 1 < 2 |
| 7 |
|
expnbnd |
⊢ ( ( ( 2 / 𝐵 ) ∈ ℝ ∧ 2 ∈ ℝ ∧ 1 < 2 ) → ∃ 𝑎 ∈ ℕ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) |
| 8 |
5 6 7
|
mp3an23 |
⊢ ( ( 2 / 𝐵 ) ∈ ℝ → ∃ 𝑎 ∈ ℕ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) |
| 9 |
4 8
|
syl |
⊢ ( 𝐵 ∈ ℝ+ → ∃ 𝑎 ∈ ℕ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) |
| 10 |
9
|
adantl |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) → ∃ 𝑎 ∈ ℕ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) |
| 11 |
|
simprl |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → 𝑎 ∈ ℕ ) |
| 12 |
|
simpll |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → 𝐴 ∈ ℕ ) |
| 13 |
|
nnaddm1cl |
⊢ ( ( 𝑎 ∈ ℕ ∧ 𝐴 ∈ ℕ ) → ( ( 𝑎 + 𝐴 ) − 1 ) ∈ ℕ ) |
| 14 |
11 12 13
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ( 𝑎 + 𝐴 ) − 1 ) ∈ ℕ ) |
| 15 |
|
simplr |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → 𝐵 ∈ ℝ+ ) |
| 16 |
|
rerpdivcl |
⊢ ( ( 2 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 2 / 𝐵 ) ∈ ℝ ) |
| 17 |
5 15 16
|
sylancr |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 2 / 𝐵 ) ∈ ℝ ) |
| 18 |
11
|
nnnn0d |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → 𝑎 ∈ ℕ0 ) |
| 19 |
|
reexpcl |
⊢ ( ( 2 ∈ ℝ ∧ 𝑎 ∈ ℕ0 ) → ( 2 ↑ 𝑎 ) ∈ ℝ ) |
| 20 |
5 18 19
|
sylancr |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 2 ↑ 𝑎 ) ∈ ℝ ) |
| 21 |
11 12
|
nnaddcld |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 𝑎 + 𝐴 ) ∈ ℕ ) |
| 22 |
|
nnm1nn0 |
⊢ ( ( 𝑎 + 𝐴 ) ∈ ℕ → ( ( 𝑎 + 𝐴 ) − 1 ) ∈ ℕ0 ) |
| 23 |
21 22
|
syl |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ( 𝑎 + 𝐴 ) − 1 ) ∈ ℕ0 ) |
| 24 |
|
peano2nn0 |
⊢ ( ( ( 𝑎 + 𝐴 ) − 1 ) ∈ ℕ0 → ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ∈ ℕ0 ) |
| 25 |
23 24
|
syl |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ∈ ℕ0 ) |
| 26 |
25
|
faccld |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ∈ ℕ ) |
| 27 |
26
|
nnzd |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ∈ ℤ ) |
| 28 |
23
|
faccld |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ∈ ℕ ) |
| 29 |
28
|
nnzd |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ∈ ℤ ) |
| 30 |
12
|
nnzd |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → 𝐴 ∈ ℤ ) |
| 31 |
29 30
|
zmulcld |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝐴 ) ∈ ℤ ) |
| 32 |
27 31
|
zsubcld |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) − ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝐴 ) ) ∈ ℤ ) |
| 33 |
|
rpexpcl |
⊢ ( ( 2 ∈ ℝ+ ∧ ( ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) − ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝐴 ) ) ∈ ℤ ) → ( 2 ↑ ( ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) − ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝐴 ) ) ) ∈ ℝ+ ) |
| 34 |
1 32 33
|
sylancr |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 2 ↑ ( ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) − ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝐴 ) ) ) ∈ ℝ+ ) |
| 35 |
34
|
rpred |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 2 ↑ ( ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) − ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝐴 ) ) ) ∈ ℝ ) |
| 36 |
|
simprr |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) |
| 37 |
17 20 36
|
ltled |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 2 / 𝐵 ) ≤ ( 2 ↑ 𝑎 ) ) |
| 38 |
5
|
a1i |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → 2 ∈ ℝ ) |
| 39 |
|
1le2 |
⊢ 1 ≤ 2 |
| 40 |
39
|
a1i |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → 1 ≤ 2 ) |
| 41 |
11
|
nnred |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → 𝑎 ∈ ℝ ) |
| 42 |
28
|
nnred |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ∈ ℝ ) |
| 43 |
18
|
nn0ge0d |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → 0 ≤ 𝑎 ) |
| 44 |
28
|
nnge1d |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → 1 ≤ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) |
| 45 |
41 42 43 44
|
lemulge12d |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → 𝑎 ≤ ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝑎 ) ) |
| 46 |
|
facp1 |
⊢ ( ( ( 𝑎 + 𝐴 ) − 1 ) ∈ ℕ0 → ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) = ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) |
| 47 |
23 46
|
syl |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) = ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) |
| 48 |
47
|
oveq1d |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) − ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝐴 ) ) = ( ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) − ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝐴 ) ) ) |
| 49 |
28
|
nncnd |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ∈ ℂ ) |
| 50 |
25
|
nn0cnd |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ∈ ℂ ) |
| 51 |
12
|
nncnd |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → 𝐴 ∈ ℂ ) |
| 52 |
49 50 51
|
subdid |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · ( ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) − 𝐴 ) ) = ( ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) − ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝐴 ) ) ) |
| 53 |
11
|
nncnd |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → 𝑎 ∈ ℂ ) |
| 54 |
21
|
nncnd |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 𝑎 + 𝐴 ) ∈ ℂ ) |
| 55 |
|
1cnd |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → 1 ∈ ℂ ) |
| 56 |
54 55
|
npcand |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) = ( 𝑎 + 𝐴 ) ) |
| 57 |
53 51 56
|
mvrraddd |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) − 𝐴 ) = 𝑎 ) |
| 58 |
57
|
oveq2d |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · ( ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) − 𝐴 ) ) = ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝑎 ) ) |
| 59 |
48 52 58
|
3eqtr2d |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) − ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝐴 ) ) = ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝑎 ) ) |
| 60 |
45 59
|
breqtrrd |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → 𝑎 ≤ ( ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) − ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝐴 ) ) ) |
| 61 |
11
|
nnzd |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → 𝑎 ∈ ℤ ) |
| 62 |
|
eluz |
⊢ ( ( 𝑎 ∈ ℤ ∧ ( ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) − ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝐴 ) ) ∈ ℤ ) → ( ( ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) − ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝐴 ) ) ∈ ( ℤ≥ ‘ 𝑎 ) ↔ 𝑎 ≤ ( ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) − ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝐴 ) ) ) ) |
| 63 |
61 32 62
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ( ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) − ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝐴 ) ) ∈ ( ℤ≥ ‘ 𝑎 ) ↔ 𝑎 ≤ ( ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) − ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝐴 ) ) ) ) |
| 64 |
60 63
|
mpbird |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) − ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝐴 ) ) ∈ ( ℤ≥ ‘ 𝑎 ) ) |
| 65 |
38 40 64
|
leexp2ad |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 2 ↑ 𝑎 ) ≤ ( 2 ↑ ( ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) − ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝐴 ) ) ) ) |
| 66 |
17 20 35 37 65
|
letrd |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 2 / 𝐵 ) ≤ ( 2 ↑ ( ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) − ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝐴 ) ) ) ) |
| 67 |
|
rpcnne0 |
⊢ ( 2 ∈ ℝ+ → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) |
| 68 |
1 67
|
mp1i |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) |
| 69 |
|
expsub |
⊢ ( ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ∈ ℤ ∧ ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝐴 ) ∈ ℤ ) ) → ( 2 ↑ ( ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) − ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝐴 ) ) ) = ( ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) / ( 2 ↑ ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝐴 ) ) ) ) |
| 70 |
68 27 31 69
|
syl12anc |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 2 ↑ ( ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) − ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝐴 ) ) ) = ( ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) / ( 2 ↑ ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝐴 ) ) ) ) |
| 71 |
|
2cn |
⊢ 2 ∈ ℂ |
| 72 |
71
|
a1i |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → 2 ∈ ℂ ) |
| 73 |
12
|
nnnn0d |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → 𝐴 ∈ ℕ0 ) |
| 74 |
28
|
nnnn0d |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ∈ ℕ0 ) |
| 75 |
72 73 74
|
expmuld |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 2 ↑ ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝐴 ) ) = ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) |
| 76 |
75
|
oveq2d |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) / ( 2 ↑ ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝐴 ) ) ) = ( ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) / ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) ) |
| 77 |
|
rpexpcl |
⊢ ( ( 2 ∈ ℝ+ ∧ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ∈ ℤ ) → ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) ∈ ℝ+ ) |
| 78 |
1 27 77
|
sylancr |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) ∈ ℝ+ ) |
| 79 |
78
|
rpcnd |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) ∈ ℂ ) |
| 80 |
|
rpexpcl |
⊢ ( ( 2 ∈ ℝ+ ∧ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ∈ ℤ ) → ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ∈ ℝ+ ) |
| 81 |
1 29 80
|
sylancr |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ∈ ℝ+ ) |
| 82 |
81 30
|
rpexpcld |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ∈ ℝ+ ) |
| 83 |
82
|
rpcnd |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ∈ ℂ ) |
| 84 |
82
|
rpne0d |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ≠ 0 ) |
| 85 |
79 83 84
|
divrecd |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) / ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) = ( ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) · ( 1 / ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) ) ) |
| 86 |
70 76 85
|
3eqtrrd |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) · ( 1 / ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) ) = ( 2 ↑ ( ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) − ( ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) · 𝐴 ) ) ) ) |
| 87 |
66 86
|
breqtrrd |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 2 / 𝐵 ) ≤ ( ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) · ( 1 / ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) ) ) |
| 88 |
82
|
rpreccld |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 1 / ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) ∈ ℝ+ ) |
| 89 |
78 88
|
rpmulcld |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) · ( 1 / ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) ) ∈ ℝ+ ) |
| 90 |
89
|
rpred |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) · ( 1 / ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) ) ∈ ℝ ) |
| 91 |
38 90 15
|
ledivmuld |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ( 2 / 𝐵 ) ≤ ( ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) · ( 1 / ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) ) ↔ 2 ≤ ( 𝐵 · ( ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) · ( 1 / ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) ) ) ) ) |
| 92 |
87 91
|
mpbid |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → 2 ≤ ( 𝐵 · ( ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) · ( 1 / ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) ) ) ) |
| 93 |
15
|
rpcnd |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → 𝐵 ∈ ℂ ) |
| 94 |
88
|
rpcnd |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 1 / ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) ∈ ℂ ) |
| 95 |
93 79 94
|
mul12d |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 𝐵 · ( ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) · ( 1 / ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) ) ) = ( ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) · ( 𝐵 · ( 1 / ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) ) ) ) |
| 96 |
92 95
|
breqtrd |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → 2 ≤ ( ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) · ( 𝐵 · ( 1 / ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) ) ) ) |
| 97 |
15 88
|
rpmulcld |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 𝐵 · ( 1 / ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) ) ∈ ℝ+ ) |
| 98 |
97
|
rpred |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 𝐵 · ( 1 / ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) ) ∈ ℝ ) |
| 99 |
38 98 78
|
ledivmuld |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ( 2 / ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) ) ≤ ( 𝐵 · ( 1 / ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) ) ↔ 2 ≤ ( ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) · ( 𝐵 · ( 1 / ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) ) ) ) ) |
| 100 |
96 99
|
mpbird |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 2 / ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) ) ≤ ( 𝐵 · ( 1 / ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) ) ) |
| 101 |
26
|
nnnn0d |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ∈ ℕ0 ) |
| 102 |
|
expneg |
⊢ ( ( 2 ∈ ℂ ∧ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ∈ ℕ0 ) → ( 2 ↑ - ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) = ( 1 / ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) ) ) |
| 103 |
71 101 102
|
sylancr |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 2 ↑ - ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) = ( 1 / ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) ) ) |
| 104 |
103
|
oveq2d |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 2 · ( 2 ↑ - ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) ) = ( 2 · ( 1 / ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) ) ) ) |
| 105 |
78
|
rpne0d |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) ≠ 0 ) |
| 106 |
72 79 105
|
divrecd |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 2 / ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) ) = ( 2 · ( 1 / ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) ) ) ) |
| 107 |
104 106
|
eqtr4d |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 2 · ( 2 ↑ - ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) ) = ( 2 / ( 2 ↑ ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) ) ) |
| 108 |
93 83 84
|
divrecd |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 𝐵 / ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) = ( 𝐵 · ( 1 / ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) ) ) |
| 109 |
100 107 108
|
3brtr4d |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ( 2 · ( 2 ↑ - ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) ) ≤ ( 𝐵 / ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) ) |
| 110 |
|
fvoveq1 |
⊢ ( 𝑥 = ( ( 𝑎 + 𝐴 ) − 1 ) → ( ! ‘ ( 𝑥 + 1 ) ) = ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) |
| 111 |
110
|
negeqd |
⊢ ( 𝑥 = ( ( 𝑎 + 𝐴 ) − 1 ) → - ( ! ‘ ( 𝑥 + 1 ) ) = - ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) |
| 112 |
111
|
oveq2d |
⊢ ( 𝑥 = ( ( 𝑎 + 𝐴 ) − 1 ) → ( 2 ↑ - ( ! ‘ ( 𝑥 + 1 ) ) ) = ( 2 ↑ - ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) ) |
| 113 |
112
|
oveq2d |
⊢ ( 𝑥 = ( ( 𝑎 + 𝐴 ) − 1 ) → ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑥 + 1 ) ) ) ) = ( 2 · ( 2 ↑ - ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) ) ) |
| 114 |
|
fveq2 |
⊢ ( 𝑥 = ( ( 𝑎 + 𝐴 ) − 1 ) → ( ! ‘ 𝑥 ) = ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) |
| 115 |
114
|
oveq2d |
⊢ ( 𝑥 = ( ( 𝑎 + 𝐴 ) − 1 ) → ( 2 ↑ ( ! ‘ 𝑥 ) ) = ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ) |
| 116 |
115
|
oveq1d |
⊢ ( 𝑥 = ( ( 𝑎 + 𝐴 ) − 1 ) → ( ( 2 ↑ ( ! ‘ 𝑥 ) ) ↑ 𝐴 ) = ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) |
| 117 |
116
|
oveq2d |
⊢ ( 𝑥 = ( ( 𝑎 + 𝐴 ) − 1 ) → ( 𝐵 / ( ( 2 ↑ ( ! ‘ 𝑥 ) ) ↑ 𝐴 ) ) = ( 𝐵 / ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) ) |
| 118 |
113 117
|
breq12d |
⊢ ( 𝑥 = ( ( 𝑎 + 𝐴 ) − 1 ) → ( ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑥 + 1 ) ) ) ) ≤ ( 𝐵 / ( ( 2 ↑ ( ! ‘ 𝑥 ) ) ↑ 𝐴 ) ) ↔ ( 2 · ( 2 ↑ - ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) ) ≤ ( 𝐵 / ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) ) ) |
| 119 |
118
|
rspcev |
⊢ ( ( ( ( 𝑎 + 𝐴 ) − 1 ) ∈ ℕ ∧ ( 2 · ( 2 ↑ - ( ! ‘ ( ( ( 𝑎 + 𝐴 ) − 1 ) + 1 ) ) ) ) ≤ ( 𝐵 / ( ( 2 ↑ ( ! ‘ ( ( 𝑎 + 𝐴 ) − 1 ) ) ) ↑ 𝐴 ) ) ) → ∃ 𝑥 ∈ ℕ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑥 + 1 ) ) ) ) ≤ ( 𝐵 / ( ( 2 ↑ ( ! ‘ 𝑥 ) ) ↑ 𝐴 ) ) ) |
| 120 |
14 109 119
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℕ ∧ ( 2 / 𝐵 ) < ( 2 ↑ 𝑎 ) ) ) → ∃ 𝑥 ∈ ℕ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑥 + 1 ) ) ) ) ≤ ( 𝐵 / ( ( 2 ↑ ( ! ‘ 𝑥 ) ) ↑ 𝐴 ) ) ) |
| 121 |
10 120
|
rexlimddv |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+ ) → ∃ 𝑥 ∈ ℕ ( 2 · ( 2 ↑ - ( ! ‘ ( 𝑥 + 1 ) ) ) ) ≤ ( 𝐵 / ( ( 2 ↑ ( ! ‘ 𝑥 ) ) ↑ 𝐴 ) ) ) |