Proof of Theorem knoppndvlem18
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2re 12341 | . . . . . . . . . . . 12
⊢ 2 ∈
ℝ | 
| 2 | 1 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℝ) | 
| 3 |  | knoppndvlem18.n | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 4 | 3 | nnred 12282 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 5 | 2, 4 | remulcld 11292 | . . . . . . . . . 10
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ) | 
| 6 | 5 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2 · 𝑁) ∈
ℝ) | 
| 7 | 6 | recnd 11290 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2 · 𝑁) ∈
ℂ) | 
| 8 |  | 2pos 12370 | . . . . . . . . . . . 12
⊢ 0 <
2 | 
| 9 | 8 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → 0 < 2) | 
| 10 | 3 | nngt0d 12316 | . . . . . . . . . . 11
⊢ (𝜑 → 0 < 𝑁) | 
| 11 | 2, 4, 9, 10 | mulgt0d 11417 | . . . . . . . . . 10
⊢ (𝜑 → 0 < (2 · 𝑁)) | 
| 12 | 11 | gt0ne0d 11828 | . . . . . . . . 9
⊢ (𝜑 → (2 · 𝑁) ≠ 0) | 
| 13 | 12 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2 · 𝑁) ≠ 0) | 
| 14 |  | nnz 12636 | . . . . . . . . 9
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℤ) | 
| 15 | 14 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℤ) | 
| 16 | 7, 13, 15 | expnegd 14194 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2 · 𝑁)↑-𝑗) = (1 / ((2 · 𝑁)↑𝑗))) | 
| 17 | 16 | adantrr 717 | . . . . . 6
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 ·
𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → ((2 · 𝑁)↑-𝑗) = (1 / ((2 · 𝑁)↑𝑗))) | 
| 18 |  | 2rp 13040 | . . . . . . . . . . 11
⊢ 2 ∈
ℝ+ | 
| 19 | 18 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → 2 ∈
ℝ+) | 
| 20 |  | knoppndvlem18.d | . . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈
ℝ+) | 
| 21 | 19, 20 | jca 511 | . . . . . . . . 9
⊢ (𝜑 → (2 ∈
ℝ+ ∧ 𝐷
∈ ℝ+)) | 
| 22 |  | rpmulcl 13059 | . . . . . . . . 9
⊢ ((2
∈ ℝ+ ∧ 𝐷 ∈ ℝ+) → (2
· 𝐷) ∈
ℝ+) | 
| 23 | 21, 22 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (2 · 𝐷) ∈
ℝ+) | 
| 24 | 23 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 ·
𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (2 · 𝐷) ∈
ℝ+) | 
| 25 | 5, 11 | elrpd 13075 | . . . . . . . . . 10
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ+) | 
| 26 | 25 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2 · 𝑁) ∈
ℝ+) | 
| 27 | 26, 15 | rpexpcld 14287 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2 · 𝑁)↑𝑗) ∈
ℝ+) | 
| 28 | 27 | adantrr 717 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 ·
𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → ((2 · 𝑁)↑𝑗) ∈
ℝ+) | 
| 29 | 24 | rprecred 13089 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 ·
𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (1 / (2 · 𝐷)) ∈ ℝ) | 
| 30 |  | knoppndvlem18.c | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) | 
| 31 | 30 | knoppndvlem3 36516 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐶 ∈ ℝ ∧ (abs‘𝐶) < 1)) | 
| 32 | 31 | simpld 494 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ∈ ℝ) | 
| 33 | 32 | recnd 11290 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 34 | 33 | abscld 15476 | . . . . . . . . . . . 12
⊢ (𝜑 → (abs‘𝐶) ∈
ℝ) | 
| 35 | 5, 34 | remulcld 11292 | . . . . . . . . . . 11
⊢ (𝜑 → ((2 · 𝑁) · (abs‘𝐶)) ∈
ℝ) | 
| 36 | 35 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2 · 𝑁) · (abs‘𝐶)) ∈
ℝ) | 
| 37 |  | nnnn0 12535 | . . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ0) | 
| 38 | 37 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ0) | 
| 39 | 36, 38 | reexpcld 14204 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((2 · 𝑁) · (abs‘𝐶))↑𝑗) ∈ ℝ) | 
| 40 | 39 | adantrr 717 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 ·
𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (((2 · 𝑁) · (abs‘𝐶))↑𝑗) ∈ ℝ) | 
| 41 | 28 | rpred 13078 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 ·
𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → ((2 · 𝑁)↑𝑗) ∈ ℝ) | 
| 42 |  | knoppndvlem18.e | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐸 ∈
ℝ+) | 
| 43 | 42 | rpred 13078 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 ∈ ℝ) | 
| 44 |  | knoppndvlem18.g | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 ∈
ℝ+) | 
| 45 | 44 | rpred 13078 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 ∈ ℝ) | 
| 46 | 44 | rpne0d 13083 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 ≠ 0) | 
| 47 | 43, 45, 46 | redivcld 12096 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐸 / 𝐺) ∈ ℝ) | 
| 48 | 23 | rprecred 13089 | . . . . . . . . . . 11
⊢ (𝜑 → (1 / (2 · 𝐷)) ∈
ℝ) | 
| 49 | 47, 48 | ifcld 4571 | . . . . . . . . . 10
⊢ (𝜑 → if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) ∈ ℝ) | 
| 50 | 49 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 ·
𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) ∈ ℝ) | 
| 51 | 48, 47 | jca 511 | . . . . . . . . . . 11
⊢ (𝜑 → ((1 / (2 · 𝐷)) ∈ ℝ ∧ (𝐸 / 𝐺) ∈ ℝ)) | 
| 52 |  | max1 13228 | . . . . . . . . . . 11
⊢ (((1 / (2
· 𝐷)) ∈ ℝ
∧ (𝐸 / 𝐺) ∈ ℝ) → (1 / (2
· 𝐷)) ≤ if((1 /
(2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷)))) | 
| 53 | 51, 52 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (1 / (2 · 𝐷)) ≤ if((1 / (2 ·
𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷)))) | 
| 54 | 53 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 ·
𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (1 / (2 · 𝐷)) ≤ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷)))) | 
| 55 |  | simprr 772 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 ·
𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗)) | 
| 56 | 29, 50, 40, 54, 55 | lelttrd 11420 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 ·
𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (1 / (2 · 𝐷)) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗)) | 
| 57 | 34 | recnd 11290 | . . . . . . . . . . . 12
⊢ (𝜑 → (abs‘𝐶) ∈
ℂ) | 
| 58 | 57 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (abs‘𝐶) ∈
ℂ) | 
| 59 | 7, 58, 38 | mulexpd 14202 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((2 · 𝑁) · (abs‘𝐶))↑𝑗) = (((2 · 𝑁)↑𝑗) · ((abs‘𝐶)↑𝑗))) | 
| 60 | 34 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (abs‘𝐶) ∈
ℝ) | 
| 61 | 60, 38 | reexpcld 14204 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((abs‘𝐶)↑𝑗) ∈ ℝ) | 
| 62 |  | 1red 11263 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 1 ∈
ℝ) | 
| 63 | 27 | rpred 13078 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2 · 𝑁)↑𝑗) ∈ ℝ) | 
| 64 | 27 | rpge0d 13082 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 0 ≤ ((2 ·
𝑁)↑𝑗)) | 
| 65 | 33 | absge0d 15484 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 ≤ (abs‘𝐶)) | 
| 66 |  | 1red 11263 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ∈
ℝ) | 
| 67 | 31 | simprd 495 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (abs‘𝐶) < 1) | 
| 68 | 34, 66, 67 | ltled 11410 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (abs‘𝐶) ≤ 1) | 
| 69 | 34, 65, 68 | 3jca 1128 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((abs‘𝐶) ∈ ℝ ∧ 0 ≤
(abs‘𝐶) ∧
(abs‘𝐶) ≤
1)) | 
| 70 | 69 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((abs‘𝐶) ∈ ℝ ∧ 0 ≤
(abs‘𝐶) ∧
(abs‘𝐶) ≤
1)) | 
| 71 | 70, 38 | jca 511 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((abs‘𝐶) ∈ ℝ ∧ 0 ≤
(abs‘𝐶) ∧
(abs‘𝐶) ≤ 1) ∧
𝑗 ∈
ℕ0)) | 
| 72 |  | exple1 14217 | . . . . . . . . . . . . 13
⊢
((((abs‘𝐶)
∈ ℝ ∧ 0 ≤ (abs‘𝐶) ∧ (abs‘𝐶) ≤ 1) ∧ 𝑗 ∈ ℕ0) →
((abs‘𝐶)↑𝑗) ≤ 1) | 
| 73 | 71, 72 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((abs‘𝐶)↑𝑗) ≤ 1) | 
| 74 | 61, 62, 63, 64, 73 | lemul2ad 12209 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((2 · 𝑁)↑𝑗) · ((abs‘𝐶)↑𝑗)) ≤ (((2 · 𝑁)↑𝑗) · 1)) | 
| 75 | 63 | recnd 11290 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2 · 𝑁)↑𝑗) ∈ ℂ) | 
| 76 | 75 | mulridd 11279 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((2 · 𝑁)↑𝑗) · 1) = ((2 · 𝑁)↑𝑗)) | 
| 77 | 74, 76 | breqtrd 5168 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((2 · 𝑁)↑𝑗) · ((abs‘𝐶)↑𝑗)) ≤ ((2 · 𝑁)↑𝑗)) | 
| 78 | 59, 77 | eqbrtrd 5164 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((2 · 𝑁) · (abs‘𝐶))↑𝑗) ≤ ((2 · 𝑁)↑𝑗)) | 
| 79 | 78 | adantrr 717 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 ·
𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (((2 · 𝑁) · (abs‘𝐶))↑𝑗) ≤ ((2 · 𝑁)↑𝑗)) | 
| 80 | 29, 40, 41, 56, 79 | ltletrd 11422 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 ·
𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (1 / (2 · 𝐷)) < ((2 · 𝑁)↑𝑗)) | 
| 81 | 24, 28, 80 | ltrec1d 13098 | . . . . . 6
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 ·
𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (1 / ((2 · 𝑁)↑𝑗)) < (2 · 𝐷)) | 
| 82 | 17, 81 | eqbrtrd 5164 | . . . . 5
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 ·
𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → ((2 · 𝑁)↑-𝑗) < (2 · 𝐷)) | 
| 83 |  | nnnegz 12618 | . . . . . . . . 9
⊢ (𝑗 ∈ ℕ → -𝑗 ∈
ℤ) | 
| 84 | 83 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → -𝑗 ∈ ℤ) | 
| 85 | 6, 13, 84 | reexpclzd 14289 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2 · 𝑁)↑-𝑗) ∈ ℝ) | 
| 86 | 20 | rpred 13078 | . . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ ℝ) | 
| 87 | 86 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐷 ∈ ℝ) | 
| 88 | 18 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 2 ∈
ℝ+) | 
| 89 | 85, 87, 88 | ltdivmuld 13129 | . . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((((2 · 𝑁)↑-𝑗) / 2) < 𝐷 ↔ ((2 · 𝑁)↑-𝑗) < (2 · 𝐷))) | 
| 90 | 89 | adantrr 717 | . . . . 5
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 ·
𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → ((((2 · 𝑁)↑-𝑗) / 2) < 𝐷 ↔ ((2 · 𝑁)↑-𝑗) < (2 · 𝐷))) | 
| 91 | 82, 90 | mpbird 257 | . . . 4
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 ·
𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (((2 · 𝑁)↑-𝑗) / 2) < 𝐷) | 
| 92 | 47 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 ·
𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (𝐸 / 𝐺) ∈ ℝ) | 
| 93 |  | max2 13230 | . . . . . . . 8
⊢ (((1 / (2
· 𝐷)) ∈ ℝ
∧ (𝐸 / 𝐺) ∈ ℝ) → (𝐸 / 𝐺) ≤ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷)))) | 
| 94 | 51, 93 | syl 17 | . . . . . . 7
⊢ (𝜑 → (𝐸 / 𝐺) ≤ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷)))) | 
| 95 | 94 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 ·
𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (𝐸 / 𝐺) ≤ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷)))) | 
| 96 | 50, 40, 55 | ltled 11410 | . . . . . 6
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 ·
𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) ≤ (((2 · 𝑁) · (abs‘𝐶))↑𝑗)) | 
| 97 | 92, 50, 40, 95, 96 | letrd 11419 | . . . . 5
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 ·
𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (𝐸 / 𝐺) ≤ (((2 · 𝑁) · (abs‘𝐶))↑𝑗)) | 
| 98 | 43 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 ·
𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → 𝐸 ∈ ℝ) | 
| 99 | 44 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 ·
𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → 𝐺 ∈
ℝ+) | 
| 100 | 98, 40, 99 | ledivmul2d 13132 | . . . . 5
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 ·
𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → ((𝐸 / 𝐺) ≤ (((2 · 𝑁) · (abs‘𝐶))↑𝑗) ↔ 𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺))) | 
| 101 | 97, 100 | mpbid 232 | . . . 4
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 ·
𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → 𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺)) | 
| 102 | 91, 101 | jca 511 | . . 3
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 ·
𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → ((((2 · 𝑁)↑-𝑗) / 2) < 𝐷 ∧ 𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺))) | 
| 103 |  | 1t1e1 12429 | . . . . . . . . 9
⊢ (1
· 1) = 1 | 
| 104 | 103 | eqcomi 2745 | . . . . . . . 8
⊢ 1 = (1
· 1) | 
| 105 | 104 | a1i 11 | . . . . . . 7
⊢ (𝜑 → 1 = (1 ·
1)) | 
| 106 | 4, 34 | remulcld 11292 | . . . . . . . 8
⊢ (𝜑 → (𝑁 · (abs‘𝐶)) ∈ ℝ) | 
| 107 |  | 0le1 11787 | . . . . . . . . 9
⊢ 0 ≤
1 | 
| 108 | 107 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → 0 ≤ 1) | 
| 109 |  | 1lt2 12438 | . . . . . . . . 9
⊢ 1 <
2 | 
| 110 | 109 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → 1 < 2) | 
| 111 |  | knoppndvlem18.1 | . . . . . . . 8
⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶))) | 
| 112 | 66, 2, 66, 106, 108, 110, 108, 111 | ltmul12ad 12210 | . . . . . . 7
⊢ (𝜑 → (1 · 1) < (2
· (𝑁 ·
(abs‘𝐶)))) | 
| 113 | 105, 112 | eqbrtrd 5164 | . . . . . 6
⊢ (𝜑 → 1 < (2 · (𝑁 · (abs‘𝐶)))) | 
| 114 | 2 | recnd 11290 | . . . . . . . 8
⊢ (𝜑 → 2 ∈
ℂ) | 
| 115 | 4 | recnd 11290 | . . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℂ) | 
| 116 | 114, 115,
57 | mulassd 11285 | . . . . . . 7
⊢ (𝜑 → ((2 · 𝑁) · (abs‘𝐶)) = (2 · (𝑁 · (abs‘𝐶)))) | 
| 117 | 116 | eqcomd 2742 | . . . . . 6
⊢ (𝜑 → (2 · (𝑁 · (abs‘𝐶))) = ((2 · 𝑁) · (abs‘𝐶))) | 
| 118 | 113, 117 | breqtrd 5168 | . . . . 5
⊢ (𝜑 → 1 < ((2 · 𝑁) · (abs‘𝐶))) | 
| 119 | 49, 35, 118 | 3jca 1128 | . . . 4
⊢ (𝜑 → (if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) ∈ ℝ ∧ ((2 · 𝑁) · (abs‘𝐶)) ∈ ℝ ∧ 1 <
((2 · 𝑁) ·
(abs‘𝐶)))) | 
| 120 |  | expnbnd 14272 | . . . 4
⊢ ((if((1 /
(2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) ∈ ℝ ∧ ((2 · 𝑁) · (abs‘𝐶)) ∈ ℝ ∧ 1 <
((2 · 𝑁) ·
(abs‘𝐶))) →
∃𝑗 ∈ ℕ
if((1 / (2 · 𝐷))
≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗)) | 
| 121 | 119, 120 | syl 17 | . . 3
⊢ (𝜑 → ∃𝑗 ∈ ℕ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗)) | 
| 122 | 102, 121 | reximddv 3170 | . 2
⊢ (𝜑 → ∃𝑗 ∈ ℕ ((((2 · 𝑁)↑-𝑗) / 2) < 𝐷 ∧ 𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺))) | 
| 123 |  | nnssnn0 12531 | . . 3
⊢ ℕ
⊆ ℕ0 | 
| 124 |  | ssrexv 4052 | . . 3
⊢ (ℕ
⊆ ℕ0 → (∃𝑗 ∈ ℕ ((((2 · 𝑁)↑-𝑗) / 2) < 𝐷 ∧ 𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺)) → ∃𝑗 ∈ ℕ0 ((((2 ·
𝑁)↑-𝑗) / 2) < 𝐷 ∧ 𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺)))) | 
| 125 | 123, 124 | ax-mp 5 | . 2
⊢
(∃𝑗 ∈
ℕ ((((2 · 𝑁)↑-𝑗) / 2) < 𝐷 ∧ 𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺)) → ∃𝑗 ∈ ℕ0 ((((2 ·
𝑁)↑-𝑗) / 2) < 𝐷 ∧ 𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺))) | 
| 126 | 122, 125 | syl 17 | 1
⊢ (𝜑 → ∃𝑗 ∈ ℕ0 ((((2 ·
𝑁)↑-𝑗) / 2) < 𝐷 ∧ 𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺))) |