| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | aaliou3lem8 26388 | . . . . . 6
⊢ ((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
→ ∃𝑒 ∈
ℕ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎))) | 
| 2 |  | aaliou3lem.c | . . . . . . . . 9
⊢ 𝐹 = (𝑎 ∈ ℕ ↦
(2↑-(!‘𝑎))) | 
| 3 |  | aaliou3lem.d | . . . . . . . . 9
⊢ 𝐿 = Σ𝑏 ∈ ℕ (𝐹‘𝑏) | 
| 4 |  | aaliou3lem.e | . . . . . . . . 9
⊢ 𝐻 = (𝑐 ∈ ℕ ↦ Σ𝑏 ∈ (1...𝑐)(𝐹‘𝑏)) | 
| 5 | 2, 3, 4 | aaliou3lem6 26391 | . . . . . . . 8
⊢ (𝑒 ∈ ℕ → ((𝐻‘𝑒) · (2↑(!‘𝑒))) ∈
ℤ) | 
| 6 | 5 | ad2antrl 728 | . . . . . . 7
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → ((𝐻‘𝑒) · (2↑(!‘𝑒))) ∈
ℤ) | 
| 7 |  | 2nn 12340 | . . . . . . . 8
⊢ 2 ∈
ℕ | 
| 8 |  | nnnn0 12535 | . . . . . . . . . 10
⊢ (𝑒 ∈ ℕ → 𝑒 ∈
ℕ0) | 
| 9 | 8 | ad2antrl 728 | . . . . . . . . 9
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → 𝑒 ∈ ℕ0) | 
| 10 |  | faccl 14323 | . . . . . . . . 9
⊢ (𝑒 ∈ ℕ0
→ (!‘𝑒) ∈
ℕ) | 
| 11 |  | nnnn0 12535 | . . . . . . . . 9
⊢
((!‘𝑒) ∈
ℕ → (!‘𝑒)
∈ ℕ0) | 
| 12 | 9, 10, 11 | 3syl 18 | . . . . . . . 8
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (!‘𝑒) ∈
ℕ0) | 
| 13 |  | nnexpcl 14116 | . . . . . . . 8
⊢ ((2
∈ ℕ ∧ (!‘𝑒) ∈ ℕ0) →
(2↑(!‘𝑒)) ∈
ℕ) | 
| 14 | 7, 12, 13 | sylancr 587 | . . . . . . 7
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (2↑(!‘𝑒)) ∈
ℕ) | 
| 15 | 2, 3, 4 | aaliou3lem5 26390 | . . . . . . . . . . . . 13
⊢ (𝑒 ∈ ℕ → (𝐻‘𝑒) ∈ ℝ) | 
| 16 | 15 | ad2antrl 728 | . . . . . . . . . . . 12
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (𝐻‘𝑒) ∈ ℝ) | 
| 17 | 16 | recnd 11290 | . . . . . . . . . . 11
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (𝐻‘𝑒) ∈ ℂ) | 
| 18 | 14 | nncnd 12283 | . . . . . . . . . . 11
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (2↑(!‘𝑒)) ∈
ℂ) | 
| 19 | 14 | nnne0d 12317 | . . . . . . . . . . 11
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (2↑(!‘𝑒)) ≠ 0) | 
| 20 | 17, 18, 19 | divcan4d 12050 | . . . . . . . . . 10
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))) = (𝐻‘𝑒)) | 
| 21 | 2, 3, 4 | aaliou3lem7 26392 | . . . . . . . . . . . 12
⊢ (𝑒 ∈ ℕ → ((𝐻‘𝑒) ≠ 𝐿 ∧ (abs‘(𝐿 − (𝐻‘𝑒))) ≤ (2 · (2↑-(!‘(𝑒 + 1)))))) | 
| 22 | 21 | simpld 494 | . . . . . . . . . . 11
⊢ (𝑒 ∈ ℕ → (𝐻‘𝑒) ≠ 𝐿) | 
| 23 | 22 | ad2antrl 728 | . . . . . . . . . 10
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (𝐻‘𝑒) ≠ 𝐿) | 
| 24 | 20, 23 | eqnetrd 3007 | . . . . . . . . 9
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))) ≠ 𝐿) | 
| 25 | 24 | necomd 2995 | . . . . . . . 8
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → 𝐿 ≠ (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))) | 
| 26 | 25 | neneqd 2944 | . . . . . . 7
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → ¬ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))) | 
| 27 | 2, 3, 4 | aaliou3lem4 26389 | . . . . . . . . . . 11
⊢ 𝐿 ∈ ℝ | 
| 28 | 14 | nnred 12282 | . . . . . . . . . . . . 13
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (2↑(!‘𝑒)) ∈
ℝ) | 
| 29 | 16, 28 | remulcld 11292 | . . . . . . . . . . . 12
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → ((𝐻‘𝑒) · (2↑(!‘𝑒))) ∈
ℝ) | 
| 30 | 29, 14 | nndivred 12321 | . . . . . . . . . . 11
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))) ∈
ℝ) | 
| 31 |  | resubcl 11574 | . . . . . . . . . . 11
⊢ ((𝐿 ∈ ℝ ∧ (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))) ∈ ℝ) →
(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))) ∈
ℝ) | 
| 32 | 27, 30, 31 | sylancr 587 | . . . . . . . . . 10
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))) ∈
ℝ) | 
| 33 | 32 | recnd 11290 | . . . . . . . . 9
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))) ∈
ℂ) | 
| 34 | 33 | abscld 15476 | . . . . . . . 8
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))) ∈
ℝ) | 
| 35 |  | simplr 768 | . . . . . . . . . 10
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → 𝑏 ∈ ℝ+) | 
| 36 |  | nnnn0 12535 | . . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℕ → 𝑎 ∈
ℕ0) | 
| 37 | 36 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → 𝑎 ∈ ℕ0) | 
| 38 | 14, 37 | nnexpcld 14285 | . . . . . . . . . . 11
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → ((2↑(!‘𝑒))↑𝑎) ∈ ℕ) | 
| 39 | 38 | nnrpd 13076 | . . . . . . . . . 10
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → ((2↑(!‘𝑒))↑𝑎) ∈
ℝ+) | 
| 40 | 35, 39 | rpdivcld 13095 | . . . . . . . . 9
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (𝑏 / ((2↑(!‘𝑒))↑𝑎)) ∈
ℝ+) | 
| 41 | 40 | rpred 13078 | . . . . . . . 8
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (𝑏 / ((2↑(!‘𝑒))↑𝑎)) ∈ ℝ) | 
| 42 |  | 2rp 13040 | . . . . . . . . . . 11
⊢ 2 ∈
ℝ+ | 
| 43 |  | peano2nn0 12568 | . . . . . . . . . . . . . 14
⊢ (𝑒 ∈ ℕ0
→ (𝑒 + 1) ∈
ℕ0) | 
| 44 |  | faccl 14323 | . . . . . . . . . . . . . 14
⊢ ((𝑒 + 1) ∈ ℕ0
→ (!‘(𝑒 + 1))
∈ ℕ) | 
| 45 | 9, 43, 44 | 3syl 18 | . . . . . . . . . . . . 13
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (!‘(𝑒 + 1)) ∈ ℕ) | 
| 46 |  | nnz 12636 | . . . . . . . . . . . . 13
⊢
((!‘(𝑒 + 1))
∈ ℕ → (!‘(𝑒 + 1)) ∈ ℤ) | 
| 47 |  | znegcl 12654 | . . . . . . . . . . . . 13
⊢
((!‘(𝑒 + 1))
∈ ℤ → -(!‘(𝑒 + 1)) ∈ ℤ) | 
| 48 | 45, 46, 47 | 3syl 18 | . . . . . . . . . . . 12
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → -(!‘(𝑒 + 1)) ∈ ℤ) | 
| 49 |  | rpexpcl 14122 | . . . . . . . . . . . 12
⊢ ((2
∈ ℝ+ ∧ -(!‘(𝑒 + 1)) ∈ ℤ) →
(2↑-(!‘(𝑒 + 1)))
∈ ℝ+) | 
| 50 | 42, 48, 49 | sylancr 587 | . . . . . . . . . . 11
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (2↑-(!‘(𝑒 + 1))) ∈
ℝ+) | 
| 51 |  | rpmulcl 13059 | . . . . . . . . . . 11
⊢ ((2
∈ ℝ+ ∧ (2↑-(!‘(𝑒 + 1))) ∈ ℝ+) → (2
· (2↑-(!‘(𝑒 + 1)))) ∈
ℝ+) | 
| 52 | 42, 50, 51 | sylancr 587 | . . . . . . . . . 10
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (2 ·
(2↑-(!‘(𝑒 +
1)))) ∈ ℝ+) | 
| 53 | 52 | rpred 13078 | . . . . . . . . 9
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (2 ·
(2↑-(!‘(𝑒 +
1)))) ∈ ℝ) | 
| 54 | 20 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))) = (𝐿 − (𝐻‘𝑒))) | 
| 55 | 54 | fveq2d 6909 | . . . . . . . . . 10
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))) = (abs‘(𝐿 − (𝐻‘𝑒)))) | 
| 56 | 21 | simprd 495 | . . . . . . . . . . 11
⊢ (𝑒 ∈ ℕ →
(abs‘(𝐿 −
(𝐻‘𝑒))) ≤ (2 · (2↑-(!‘(𝑒 + 1))))) | 
| 57 | 56 | ad2antrl 728 | . . . . . . . . . 10
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (abs‘(𝐿 − (𝐻‘𝑒))) ≤ (2 · (2↑-(!‘(𝑒 + 1))))) | 
| 58 | 55, 57 | eqbrtrd 5164 | . . . . . . . . 9
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))) ≤ (2 ·
(2↑-(!‘(𝑒 +
1))))) | 
| 59 |  | simprr 772 | . . . . . . . . 9
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (2 ·
(2↑-(!‘(𝑒 +
1)))) ≤ (𝑏 /
((2↑(!‘𝑒))↑𝑎))) | 
| 60 | 34, 53, 41, 58, 59 | letrd 11419 | . . . . . . . 8
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎))) | 
| 61 | 34, 41, 60 | lensymd 11413 | . . . . . . 7
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → ¬ (𝑏 / ((2↑(!‘𝑒))↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))))) | 
| 62 |  | oveq1 7439 | . . . . . . . . . . 11
⊢ (𝑓 = ((𝐻‘𝑒) · (2↑(!‘𝑒))) → (𝑓 / 𝑑) = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑)) | 
| 63 | 62 | eqeq2d 2747 | . . . . . . . . . 10
⊢ (𝑓 = ((𝐻‘𝑒) · (2↑(!‘𝑒))) → (𝐿 = (𝑓 / 𝑑) ↔ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑))) | 
| 64 | 63 | notbid 318 | . . . . . . . . 9
⊢ (𝑓 = ((𝐻‘𝑒) · (2↑(!‘𝑒))) → (¬ 𝐿 = (𝑓 / 𝑑) ↔ ¬ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑))) | 
| 65 | 62 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝑓 = ((𝐻‘𝑒) · (2↑(!‘𝑒))) → (𝐿 − (𝑓 / 𝑑)) = (𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑))) | 
| 66 | 65 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (𝑓 = ((𝐻‘𝑒) · (2↑(!‘𝑒))) → (abs‘(𝐿 − (𝑓 / 𝑑))) = (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑)))) | 
| 67 | 66 | breq2d 5154 | . . . . . . . . . 10
⊢ (𝑓 = ((𝐻‘𝑒) · (2↑(!‘𝑒))) → ((𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))) ↔ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑))))) | 
| 68 | 67 | notbid 318 | . . . . . . . . 9
⊢ (𝑓 = ((𝐻‘𝑒) · (2↑(!‘𝑒))) → (¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))) ↔ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑))))) | 
| 69 | 64, 68 | anbi12d 632 | . . . . . . . 8
⊢ (𝑓 = ((𝐻‘𝑒) · (2↑(!‘𝑒))) → ((¬ 𝐿 = (𝑓 / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))) ↔ (¬ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑)))))) | 
| 70 |  | oveq2 7440 | . . . . . . . . . . 11
⊢ (𝑑 = (2↑(!‘𝑒)) → (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑) = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))) | 
| 71 | 70 | eqeq2d 2747 | . . . . . . . . . 10
⊢ (𝑑 = (2↑(!‘𝑒)) → (𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑) ↔ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))) | 
| 72 | 71 | notbid 318 | . . . . . . . . 9
⊢ (𝑑 = (2↑(!‘𝑒)) → (¬ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑) ↔ ¬ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))) | 
| 73 |  | oveq1 7439 | . . . . . . . . . . . 12
⊢ (𝑑 = (2↑(!‘𝑒)) → (𝑑↑𝑎) = ((2↑(!‘𝑒))↑𝑎)) | 
| 74 | 73 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (𝑑 = (2↑(!‘𝑒)) → (𝑏 / (𝑑↑𝑎)) = (𝑏 / ((2↑(!‘𝑒))↑𝑎))) | 
| 75 | 70 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝑑 = (2↑(!‘𝑒)) → (𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑)) = (𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))) | 
| 76 | 75 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (𝑑 = (2↑(!‘𝑒)) → (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑))) = (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))))) | 
| 77 | 74, 76 | breq12d 5155 | . . . . . . . . . 10
⊢ (𝑑 = (2↑(!‘𝑒)) → ((𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑))) ↔ (𝑏 / ((2↑(!‘𝑒))↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))))) | 
| 78 | 77 | notbid 318 | . . . . . . . . 9
⊢ (𝑑 = (2↑(!‘𝑒)) → (¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑))) ↔ ¬ (𝑏 / ((2↑(!‘𝑒))↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))))) | 
| 79 | 72, 78 | anbi12d 632 | . . . . . . . 8
⊢ (𝑑 = (2↑(!‘𝑒)) → ((¬ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / 𝑑)))) ↔ (¬ 𝐿 = (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))) ∧ ¬ (𝑏 / ((2↑(!‘𝑒))↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒)))))))) | 
| 80 | 69, 79 | rspc2ev 3634 | . . . . . . 7
⊢ ((((𝐻‘𝑒) · (2↑(!‘𝑒))) ∈ ℤ ∧
(2↑(!‘𝑒)) ∈
ℕ ∧ (¬ 𝐿 =
(((𝐻‘𝑒) ·
(2↑(!‘𝑒))) /
(2↑(!‘𝑒))) ∧
¬ (𝑏 /
((2↑(!‘𝑒))↑𝑎)) < (abs‘(𝐿 − (((𝐻‘𝑒) · (2↑(!‘𝑒))) / (2↑(!‘𝑒))))))) → ∃𝑓 ∈ ℤ ∃𝑑 ∈ ℕ (¬ 𝐿 = (𝑓 / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))))) | 
| 81 | 6, 14, 26, 61, 80 | syl112anc 1375 | . . . . . 6
⊢ (((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
∧ (𝑒 ∈ ℕ
∧ (2 · (2↑-(!‘(𝑒 + 1)))) ≤ (𝑏 / ((2↑(!‘𝑒))↑𝑎)))) → ∃𝑓 ∈ ℤ ∃𝑑 ∈ ℕ (¬ 𝐿 = (𝑓 / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))))) | 
| 82 | 1, 81 | rexlimddv 3160 | . . . . 5
⊢ ((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
→ ∃𝑓 ∈
ℤ ∃𝑑 ∈
ℕ (¬ 𝐿 = (𝑓 / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))))) | 
| 83 |  | pm4.56 990 | . . . . . . . . 9
⊢ ((¬
𝐿 = (𝑓 / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))) ↔ ¬ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))))) | 
| 84 | 83 | rexbii 3093 | . . . . . . . 8
⊢
(∃𝑑 ∈
ℕ (¬ 𝐿 = (𝑓 / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))) ↔ ∃𝑑 ∈ ℕ ¬ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))))) | 
| 85 |  | rexnal 3099 | . . . . . . . 8
⊢
(∃𝑑 ∈
ℕ ¬ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))) ↔ ¬ ∀𝑑 ∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))))) | 
| 86 | 84, 85 | bitri 275 | . . . . . . 7
⊢
(∃𝑑 ∈
ℕ (¬ 𝐿 = (𝑓 / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))) ↔ ¬ ∀𝑑 ∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))))) | 
| 87 | 86 | rexbii 3093 | . . . . . 6
⊢
(∃𝑓 ∈
ℤ ∃𝑑 ∈
ℕ (¬ 𝐿 = (𝑓 / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))) ↔ ∃𝑓 ∈ ℤ ¬ ∀𝑑 ∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))))) | 
| 88 |  | rexnal 3099 | . . . . . 6
⊢
(∃𝑓 ∈
ℤ ¬ ∀𝑑
∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))) ↔ ¬ ∀𝑓 ∈ ℤ ∀𝑑 ∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))))) | 
| 89 | 87, 88 | bitri 275 | . . . . 5
⊢
(∃𝑓 ∈
ℤ ∃𝑑 ∈
ℕ (¬ 𝐿 = (𝑓 / 𝑑) ∧ ¬ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))) ↔ ¬ ∀𝑓 ∈ ℤ ∀𝑑 ∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))))) | 
| 90 | 82, 89 | sylib 218 | . . . 4
⊢ ((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℝ+)
→ ¬ ∀𝑓
∈ ℤ ∀𝑑
∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))))) | 
| 91 | 90 | nrexdv 3148 | . . 3
⊢ (𝑎 ∈ ℕ → ¬
∃𝑏 ∈
ℝ+ ∀𝑓 ∈ ℤ ∀𝑑 ∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))))) | 
| 92 | 91 | nrex 3073 | . 2
⊢  ¬
∃𝑎 ∈ ℕ
∃𝑏 ∈
ℝ+ ∀𝑓 ∈ ℤ ∀𝑑 ∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑)))) | 
| 93 |  | aaliou2b 26384 | . 2
⊢ (𝐿 ∈ 𝔸 →
∃𝑎 ∈ ℕ
∃𝑏 ∈
ℝ+ ∀𝑓 ∈ ℤ ∀𝑑 ∈ ℕ (𝐿 = (𝑓 / 𝑑) ∨ (𝑏 / (𝑑↑𝑎)) < (abs‘(𝐿 − (𝑓 / 𝑑))))) | 
| 94 | 92, 93 | mto 197 | 1
⊢  ¬
𝐿 ∈
𝔸 |