Step | Hyp | Ref
| Expression |
1 | | aaliou3lem8 23904 |
. . . . . 6
⊢ ((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
→ ∃𝑒 ∈
ℕ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎))) |
2 | | aaliou3lem.c |
. . . . . . . . 9
⊢ 𝐹 = (𝑎 ∈ ℕ ↦
(2↑-(!‘𝑎))) |
3 | | aaliou3lem.d |
. . . . . . . . 9
⊢ 𝐿 = Σ𝑏 ∈ ℕ (𝐹‘𝑏) |
4 | | aaliou3lem.e |
. . . . . . . . 9
⊢ 𝐻 = (𝑐 ∈ ℕ ↦ Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏)) |
5 | 2, 3, 4 | aaliou3lem6 23907 |
. . . . . . . 8
⊢ (𝑒 ∈ ℕ → ((𝐻‘𝑒) · (2↑(!‘𝑒))) ∈
ℤ) |
6 | 5 | ad2antrl 760 |
. . . . . . 7
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → ((𝐻‘𝑒) · (2↑(!‘𝑒))) ∈
ℤ) |
7 | | 2nn 11062 |
. . . . . . . 8
⊢ 2 ∈
ℕ |
8 | | nnnn0 11176 |
. . . . . . . . . 10
⊢ (𝑒 ∈ ℕ → 𝑒 ∈
ℕ0) |
9 | 8 | ad2antrl 760 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → 𝑒 ∈ ℕ0) |
10 | | faccl 12932 |
. . . . . . . . 9
⊢ (𝑒 ∈ ℕ0
→ (!‘𝑒) ∈
ℕ) |
11 | | nnnn0 11176 |
. . . . . . . . 9
⊢
((!‘𝑒) ∈
ℕ → (!‘𝑒)
∈ ℕ0) |
12 | 9, 10, 11 | 3syl 18 |
. . . . . . . 8
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (!‘𝑒) ∈
ℕ0) |
13 | | nnexpcl 12735 |
. . . . . . . 8
⊢ ((2
∈ ℕ ∧ (!‘𝑒) ∈ ℕ0) →
(2↑(!‘𝑒)) ∈
ℕ) |
14 | 7, 12, 13 | sylancr 694 |
. . . . . . 7
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (2↑(!‘𝑒)) ∈
ℕ) |
15 | 2, 3, 4 | aaliou3lem5 23906 |
. . . . . . . . . . . . 13
⊢ (𝑒 ∈ ℕ → (𝐻‘𝑒) ∈ ℝ) |
16 | 15 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (𝐻‘𝑒) ∈ ℝ) |
17 | 16 | recnd 9947 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (𝐻‘𝑒) ∈ ℂ) |
18 | 14 | nncnd 10913 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (2↑(!‘𝑒)) ∈
ℂ) |
19 | 14 | nnne0d 10942 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (2↑(!‘𝑒)) ≠ 0) |
20 | 17, 18, 19 | divcan4d 10686 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))) = (𝐻‘𝑒)) |
21 | 2, 3, 4 | aaliou3lem7 23908 |
. . . . . . . . . . . 12
⊢ (𝑒 ∈ ℕ → ((𝐻‘𝑒) ≠ 𝐿 ∧ (abs‘(𝐿 − (𝐻‘𝑒))) ≤ (2 · (2↑-(!‘(𝑒 + 1)))))) |
22 | 21 | simpld 474 |
. . . . . . . . . . 11
⊢ (𝑒 ∈ ℕ → (𝐻‘𝑒) ≠ 𝐿) |
23 | 22 | ad2antrl 760 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (𝐻‘𝑒) ≠ 𝐿) |
24 | 20, 23 | eqnetrd 2849 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))) ≠ 𝐿) |
25 | 24 | necomd 2837 |
. . . . . . . 8
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → 𝐿 ≠ (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))) |
26 | 25 | neneqd 2787 |
. . . . . . 7
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → ¬ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))) |
27 | 2, 3, 4 | aaliou3lem4 23905 |
. . . . . . . . . . . 12
⊢ 𝐿 ∈ ℝ |
28 | 14 | nnred 10912 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (2↑(!‘𝑒)) ∈
ℝ) |
29 | 16, 28 | remulcld 9949 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → ((𝐻‘𝑒) · (2↑(!‘𝑒))) ∈
ℝ) |
30 | 29, 14 | nndivred 10946 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))) ∈
ℝ) |
31 | | resubcl 10224 |
. . . . . . . . . . . 12
⊢ ((𝐿 ∈ ℝ ∧ (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))) ∈ ℝ) →
(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))) ∈
ℝ) |
32 | 27, 30, 31 | sylancr 694 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))) ∈
ℝ) |
33 | 32 | recnd 9947 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))) ∈
ℂ) |
34 | 33 | abscld 14023 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))) ∈
ℝ) |
35 | | 2rp 11713 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ+ |
36 | | peano2nn0 11210 |
. . . . . . . . . . . . . 14
⊢ (𝑒 ∈ ℕ0
→ (𝑒 + 1) ∈
ℕ0) |
37 | | faccl 12932 |
. . . . . . . . . . . . . 14
⊢ ((𝑒 + 1) ∈ ℕ0
→ (!‘(𝑒 + 1))
∈ ℕ) |
38 | 9, 36, 37 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (!‘(𝑒 + 1)) ∈ ℕ) |
39 | | nnz 11276 |
. . . . . . . . . . . . 13
⊢
((!‘(𝑒 + 1))
∈ ℕ → (!‘(𝑒 + 1)) ∈ ℤ) |
40 | | znegcl 11289 |
. . . . . . . . . . . . 13
⊢
((!‘(𝑒 + 1))
∈ ℤ → -(!‘(𝑒 + 1)) ∈ ℤ) |
41 | 38, 39, 40 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → -(!‘(𝑒 + 1)) ∈ ℤ) |
42 | | rpexpcl 12741 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℝ+ ∧ -(!‘(𝑒 + 1)) ∈ ℤ) →
(2↑-(!‘(𝑒 + 1)))
∈ ℝ+) |
43 | 35, 41, 42 | sylancr 694 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (2↑-(!‘(𝑒 + 1))) ∈
ℝ+) |
44 | | rpmulcl 11731 |
. . . . . . . . . . 11
⊢ ((2
∈ ℝ+ ∧ (2↑-(!‘(𝑒 + 1))) ∈ ℝ+) → (2
· (2↑-(!‘(𝑒 + 1)))) ∈
ℝ+) |
45 | 35, 43, 44 | sylancr 694 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (2 ·
(2↑-(!‘(𝑒 +
1)))) ∈ ℝ+) |
46 | 45 | rpred 11748 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (2 ·
(2↑-(!‘(𝑒 +
1)))) ∈ ℝ) |
47 | | simplr 788 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → 𝑏 ∈ ℝ+) |
48 | | nnnn0 11176 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ ℕ → 𝑎 ∈
ℕ0) |
49 | 48 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → 𝑎 ∈ ℕ0) |
50 | 14, 49 | nnexpcld 12892 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → ((2↑(!‘𝑒))↑𝑎) ∈ ℕ) |
51 | 50 | nnrpd 11746 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → ((2↑(!‘𝑒))↑𝑎) ∈
ℝ+) |
52 | 47, 51 | rpdivcld 11765 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (𝑏 / ((2↑(!‘𝑒))↑𝑎)) ∈
ℝ+) |
53 | 52 | rpred 11748 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (𝑏 / ((2↑(!‘𝑒))↑𝑎)) ∈ ℝ) |
54 | 20 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))) = (𝐿 − (𝐻‘𝑒))) |
55 | 54 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))) = (abs‘(𝐿 − (𝐻‘𝑒)))) |
56 | 21 | simprd 478 |
. . . . . . . . . . 11
⊢ (𝑒 ∈ ℕ →
(abs‘(𝐿 −
(𝐻‘𝑒))) ≤ (2 · (2↑-(!‘(𝑒 + 1))))) |
57 | 56 | ad2antrl 760 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (abs‘(𝐿 − (𝐻‘𝑒))) ≤ (2 · (2↑-(!‘(𝑒 + 1))))) |
58 | 55, 57 | eqbrtrd 4605 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))) ≤ (2 ·
(2↑-(!‘(𝑒 +
1))))) |
59 | | simprr 792 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (2 ·
(2↑-(!‘(𝑒 +
1)))) ≤ (𝑏 /
((2↑(!‘𝑒))↑𝑎))) |
60 | 34, 46, 53, 58, 59 | letrd 10073 |
. . . . . . . 8
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎))) |
61 | 34, 53 | lenltd 10062 |
. . . . . . . 8
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → ((abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)) ↔ ¬ (𝑏 / ((2↑(!‘𝑒))↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))))) |
62 | 60, 61 | mpbid 221 |
. . . . . . 7
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → ¬ (𝑏 / ((2↑(!‘𝑒))↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))))) |
63 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑓 = ((𝐻‘𝑒) · (2↑(!‘𝑒))) → (𝑓 / 𝑑) = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑)) |
64 | 63 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑓 = ((𝐻‘𝑒) · (2↑(!‘𝑒))) → (𝐿 = (𝑓 / 𝑑) ↔ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑))) |
65 | 64 | notbid 307 |
. . . . . . . . 9
⊢ (𝑓 = ((𝐻‘𝑒) · (2↑(!‘𝑒))) → (¬ 𝐿 = (𝑓 / 𝑑) ↔ ¬ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑))) |
66 | 63 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑓 = ((𝐻‘𝑒) · (2↑(!‘𝑒))) → (𝐿 − (𝑓 / 𝑑)) = (𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑))) |
67 | 66 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑓 = ((𝐻‘𝑒) · (2↑(!‘𝑒))) → (abs‘(𝐿 − (𝑓 / 𝑑))) = (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑)))) |
68 | 67 | breq2d 4595 |
. . . . . . . . . 10
⊢ (𝑓 = ((𝐻‘𝑒) · (2↑(!‘𝑒))) → ((𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))) ↔ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑))))) |
69 | 68 | notbid 307 |
. . . . . . . . 9
⊢ (𝑓 = ((𝐻‘𝑒) · (2↑(!‘𝑒))) → (¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))) ↔ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑))))) |
70 | 65, 69 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑓 = ((𝐻‘𝑒) · (2↑(!‘𝑒))) → ((¬ 𝐿 = (𝑓 / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))) ↔ (¬ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑)))))) |
71 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑑 = (2↑(!‘𝑒)) → (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑) = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))) |
72 | 71 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑑 = (2↑(!‘𝑒)) → (𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑) ↔ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))) |
73 | 72 | notbid 307 |
. . . . . . . . 9
⊢ (𝑑 = (2↑(!‘𝑒)) → (¬ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑) ↔ ¬ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))) |
74 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑑 = (2↑(!‘𝑒)) → (𝑑↑𝑎) = ((2↑(!‘𝑒))↑𝑎)) |
75 | 74 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑑 = (2↑(!‘𝑒)) → (𝑏 / (𝑑↑𝑎)) = (𝑏 / ((2↑(!‘𝑒))↑𝑎))) |
76 | 71 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑑 = (2↑(!‘𝑒)) → (𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑)) = (𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))) |
77 | 76 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑑 = (2↑(!‘𝑒)) → (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑))) = (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))))) |
78 | 75, 77 | breq12d 4596 |
. . . . . . . . . 10
⊢ (𝑑 = (2↑(!‘𝑒)) → ((𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑))) ↔ (𝑏 / ((2↑(!‘𝑒))↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))))) |
79 | 78 | notbid 307 |
. . . . . . . . 9
⊢ (𝑑 = (2↑(!‘𝑒)) → (¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑))) ↔ ¬ (𝑏 / ((2↑(!‘𝑒))↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))))) |
80 | 73, 79 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑑 = (2↑(!‘𝑒)) → ((¬ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑)))) ↔ (¬ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))) ∧ ¬ (𝑏 / ((2↑(!‘𝑒))↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))))))) |
81 | 70, 80 | rspc2ev 3295 |
. . . . . . 7
⊢ ((((𝐻‘𝑒) · (2↑(!‘𝑒))) ∈ ℤ ∧
(2↑(!‘𝑒)) ∈
ℕ ∧ (¬ 𝐿 =
(((𝐻‘𝑒) ·
(2↑(!‘𝑒))) /
(2↑(!‘𝑒))) ∧
¬ (𝑏 /
((2↑(!‘𝑒))↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))))) → ∃𝑓 ∈ ℤ ∃𝑑 ∈ ℕ (¬ 𝐿 = (𝑓 / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))))) |
82 | 6, 14, 26, 62, 81 | syl112anc 1322 |
. . . . . 6
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → ∃𝑓 ∈ ℤ ∃𝑑 ∈ ℕ (¬ 𝐿 = (𝑓 / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))))) |
83 | 1, 82 | rexlimddv 3017 |
. . . . 5
⊢ ((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
→ ∃𝑓 ∈
ℤ ∃𝑑 ∈
ℕ (¬ 𝐿 = (𝑓 / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))))) |
84 | | pm4.56 515 |
. . . . . . . . 9
⊢ ((¬
𝐿 = (𝑓 / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))) ↔ ¬ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))))) |
85 | 84 | rexbii 3023 |
. . . . . . . 8
⊢
(∃𝑑 ∈
ℕ (¬ 𝐿 = (𝑓 / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))) ↔ ∃𝑑 ∈ ℕ ¬ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))))) |
86 | | rexnal 2978 |
. . . . . . . 8
⊢
(∃𝑑 ∈
ℕ ¬ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))) ↔ ¬ ∀𝑑 ∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))))) |
87 | 85, 86 | bitri 263 |
. . . . . . 7
⊢
(∃𝑑 ∈
ℕ (¬ 𝐿 = (𝑓 / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))) ↔ ¬ ∀𝑑 ∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))))) |
88 | 87 | rexbii 3023 |
. . . . . 6
⊢
(∃𝑓 ∈
ℤ ∃𝑑 ∈
ℕ (¬ 𝐿 = (𝑓 / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))) ↔ ∃𝑓 ∈ ℤ ¬ ∀𝑑 ∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))))) |
89 | | rexnal 2978 |
. . . . . 6
⊢
(∃𝑓 ∈
ℤ ¬ ∀𝑑
∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))) ↔ ¬ ∀𝑓 ∈ ℤ ∀𝑑 ∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))))) |
90 | 88, 89 | bitri 263 |
. . . . 5
⊢
(∃𝑓 ∈
ℤ ∃𝑑 ∈
ℕ (¬ 𝐿 = (𝑓 / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))) ↔ ¬ ∀𝑓 ∈ ℤ ∀𝑑 ∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))))) |
91 | 83, 90 | sylib 207 |
. . . 4
⊢ ((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
→ ¬ ∀𝑓
∈ ℤ ∀𝑑
∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))))) |
92 | 91 | nrexdv 2984 |
. . 3
⊢ (𝑎 ∈ ℕ → ¬
∃𝑏 ∈
ℝ+ ∀𝑓 ∈ ℤ ∀𝑑 ∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))))) |
93 | 92 | nrex 2983 |
. 2
⊢ ¬
∃𝑎 ∈ ℕ
∃𝑏 ∈
ℝ+ ∀𝑓 ∈ ℤ ∀𝑑 ∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))) |
94 | | aaliou2b 23900 |
. 2
⊢ (𝐿 ∈ 𝔸 →
∃𝑎 ∈ ℕ
∃𝑏 ∈
ℝ+ ∀𝑓 ∈ ℤ ∀𝑑 ∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))))) |
95 | 93, 94 | mto 187 |
1
⊢ ¬
𝐿 ∈
𝔸 |