Users' Mathboxes Mathbox for Asger C. Ipsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  knoppndvlem18 Structured version   Visualization version   GIF version

Theorem knoppndvlem18 32891
Description: Lemma for knoppndv 32896. (Contributed by Asger C. Ipsen, 14-Aug-2021.)
Hypotheses
Ref Expression
knoppndvlem18.c (𝜑𝐶 ∈ (-1(,)1))
knoppndvlem18.n (𝜑𝑁 ∈ ℕ)
knoppndvlem18.d (𝜑𝐷 ∈ ℝ+)
knoppndvlem18.e (𝜑𝐸 ∈ ℝ+)
knoppndvlem18.g (𝜑𝐺 ∈ ℝ+)
knoppndvlem18.1 (𝜑 → 1 < (𝑁 · (abs‘𝐶)))
Assertion
Ref Expression
knoppndvlem18 (𝜑 → ∃𝑗 ∈ ℕ0 ((((2 · 𝑁)↑-𝑗) / 2) < 𝐷𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺)))
Distinct variable groups:   𝐶,𝑗   𝐷,𝑗   𝑗,𝐸   𝑗,𝐺   𝑗,𝑁   𝜑,𝑗

Proof of Theorem knoppndvlem18
StepHypRef Expression
1 2re 11346 . . . . . . . . . . . 12 2 ∈ ℝ
21a1i 11 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℝ)
3 knoppndvlem18.n . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℕ)
43nnred 11291 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℝ)
52, 4remulcld 10324 . . . . . . . . . 10 (𝜑 → (2 · 𝑁) ∈ ℝ)
65adantr 472 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (2 · 𝑁) ∈ ℝ)
76recnd 10322 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (2 · 𝑁) ∈ ℂ)
8 2pos 11382 . . . . . . . . . . . 12 0 < 2
98a1i 11 . . . . . . . . . . 11 (𝜑 → 0 < 2)
103nngt0d 11321 . . . . . . . . . . 11 (𝜑 → 0 < 𝑁)
112, 4, 9, 10mulgt0d 10446 . . . . . . . . . 10 (𝜑 → 0 < (2 · 𝑁))
1211gt0ne0d 10846 . . . . . . . . 9 (𝜑 → (2 · 𝑁) ≠ 0)
1312adantr 472 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (2 · 𝑁) ≠ 0)
14 nnz 11646 . . . . . . . . 9 (𝑗 ∈ ℕ → 𝑗 ∈ ℤ)
1514adantl 473 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℤ)
167, 13, 15expnegd 13222 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → ((2 · 𝑁)↑-𝑗) = (1 / ((2 · 𝑁)↑𝑗)))
1716adantrr 708 . . . . . 6 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → ((2 · 𝑁)↑-𝑗) = (1 / ((2 · 𝑁)↑𝑗)))
18 2rp 12033 . . . . . . . . . . 11 2 ∈ ℝ+
1918a1i 11 . . . . . . . . . 10 (𝜑 → 2 ∈ ℝ+)
20 knoppndvlem18.d . . . . . . . . . 10 (𝜑𝐷 ∈ ℝ+)
2119, 20jca 507 . . . . . . . . 9 (𝜑 → (2 ∈ ℝ+𝐷 ∈ ℝ+))
22 rpmulcl 12053 . . . . . . . . 9 ((2 ∈ ℝ+𝐷 ∈ ℝ+) → (2 · 𝐷) ∈ ℝ+)
2321, 22syl 17 . . . . . . . 8 (𝜑 → (2 · 𝐷) ∈ ℝ+)
2423adantr 472 . . . . . . 7 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (2 · 𝐷) ∈ ℝ+)
255, 11elrpd 12067 . . . . . . . . . 10 (𝜑 → (2 · 𝑁) ∈ ℝ+)
2625adantr 472 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (2 · 𝑁) ∈ ℝ+)
2726, 15rpexpcld 13239 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → ((2 · 𝑁)↑𝑗) ∈ ℝ+)
2827adantrr 708 . . . . . . 7 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → ((2 · 𝑁)↑𝑗) ∈ ℝ+)
2924rprecred 12081 . . . . . . . 8 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (1 / (2 · 𝐷)) ∈ ℝ)
30 knoppndvlem18.c . . . . . . . . . . . . . . . 16 (𝜑𝐶 ∈ (-1(,)1))
3130knoppndvlem3 32876 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶 ∈ ℝ ∧ (abs‘𝐶) < 1))
3231simpld 488 . . . . . . . . . . . . . 14 (𝜑𝐶 ∈ ℝ)
3332recnd 10322 . . . . . . . . . . . . 13 (𝜑𝐶 ∈ ℂ)
3433abscld 14462 . . . . . . . . . . . 12 (𝜑 → (abs‘𝐶) ∈ ℝ)
355, 34remulcld 10324 . . . . . . . . . . 11 (𝜑 → ((2 · 𝑁) · (abs‘𝐶)) ∈ ℝ)
3635adantr 472 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → ((2 · 𝑁) · (abs‘𝐶)) ∈ ℝ)
37 nnnn0 11546 . . . . . . . . . . 11 (𝑗 ∈ ℕ → 𝑗 ∈ ℕ0)
3837adantl 473 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℕ0)
3936, 38reexpcld 13232 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (((2 · 𝑁) · (abs‘𝐶))↑𝑗) ∈ ℝ)
4039adantrr 708 . . . . . . . 8 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (((2 · 𝑁) · (abs‘𝐶))↑𝑗) ∈ ℝ)
4128rpred 12070 . . . . . . . 8 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → ((2 · 𝑁)↑𝑗) ∈ ℝ)
42 knoppndvlem18.e . . . . . . . . . . . . 13 (𝜑𝐸 ∈ ℝ+)
4342rpred 12070 . . . . . . . . . . . 12 (𝜑𝐸 ∈ ℝ)
44 knoppndvlem18.g . . . . . . . . . . . . 13 (𝜑𝐺 ∈ ℝ+)
4544rpred 12070 . . . . . . . . . . . 12 (𝜑𝐺 ∈ ℝ)
4644rpne0d 12075 . . . . . . . . . . . 12 (𝜑𝐺 ≠ 0)
4743, 45, 46redivcld 11107 . . . . . . . . . . 11 (𝜑 → (𝐸 / 𝐺) ∈ ℝ)
4823rprecred 12081 . . . . . . . . . . 11 (𝜑 → (1 / (2 · 𝐷)) ∈ ℝ)
4947, 48ifcld 4288 . . . . . . . . . 10 (𝜑 → if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) ∈ ℝ)
5049adantr 472 . . . . . . . . 9 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) ∈ ℝ)
5148, 47jca 507 . . . . . . . . . . 11 (𝜑 → ((1 / (2 · 𝐷)) ∈ ℝ ∧ (𝐸 / 𝐺) ∈ ℝ))
52 max1 12218 . . . . . . . . . . 11 (((1 / (2 · 𝐷)) ∈ ℝ ∧ (𝐸 / 𝐺) ∈ ℝ) → (1 / (2 · 𝐷)) ≤ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))))
5351, 52syl 17 . . . . . . . . . 10 (𝜑 → (1 / (2 · 𝐷)) ≤ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))))
5453adantr 472 . . . . . . . . 9 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (1 / (2 · 𝐷)) ≤ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))))
55 simprr 789 . . . . . . . . 9 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))
5629, 50, 40, 54, 55lelttrd 10449 . . . . . . . 8 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (1 / (2 · 𝐷)) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))
5734recnd 10322 . . . . . . . . . . . 12 (𝜑 → (abs‘𝐶) ∈ ℂ)
5857adantr 472 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (abs‘𝐶) ∈ ℂ)
597, 58, 38mulexpd 13230 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (((2 · 𝑁) · (abs‘𝐶))↑𝑗) = (((2 · 𝑁)↑𝑗) · ((abs‘𝐶)↑𝑗)))
6034adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (abs‘𝐶) ∈ ℝ)
6160, 38reexpcld 13232 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → ((abs‘𝐶)↑𝑗) ∈ ℝ)
62 1red 10294 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 1 ∈ ℝ)
6327rpred 12070 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → ((2 · 𝑁)↑𝑗) ∈ ℝ)
6427rpge0d 12074 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 0 ≤ ((2 · 𝑁)↑𝑗))
6533absge0d 14470 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ (abs‘𝐶))
66 1red 10294 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ∈ ℝ)
6731simprd 489 . . . . . . . . . . . . . . . . 17 (𝜑 → (abs‘𝐶) < 1)
6834, 66, 67ltled 10439 . . . . . . . . . . . . . . . 16 (𝜑 → (abs‘𝐶) ≤ 1)
6934, 65, 683jca 1158 . . . . . . . . . . . . . . 15 (𝜑 → ((abs‘𝐶) ∈ ℝ ∧ 0 ≤ (abs‘𝐶) ∧ (abs‘𝐶) ≤ 1))
7069adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ((abs‘𝐶) ∈ ℝ ∧ 0 ≤ (abs‘𝐶) ∧ (abs‘𝐶) ≤ 1))
7170, 38jca 507 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (((abs‘𝐶) ∈ ℝ ∧ 0 ≤ (abs‘𝐶) ∧ (abs‘𝐶) ≤ 1) ∧ 𝑗 ∈ ℕ0))
72 exple1 13127 . . . . . . . . . . . . 13 ((((abs‘𝐶) ∈ ℝ ∧ 0 ≤ (abs‘𝐶) ∧ (abs‘𝐶) ≤ 1) ∧ 𝑗 ∈ ℕ0) → ((abs‘𝐶)↑𝑗) ≤ 1)
7371, 72syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → ((abs‘𝐶)↑𝑗) ≤ 1)
7461, 62, 63, 64, 73lemul2ad 11218 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (((2 · 𝑁)↑𝑗) · ((abs‘𝐶)↑𝑗)) ≤ (((2 · 𝑁)↑𝑗) · 1))
7563recnd 10322 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → ((2 · 𝑁)↑𝑗) ∈ ℂ)
7675mulid1d 10311 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (((2 · 𝑁)↑𝑗) · 1) = ((2 · 𝑁)↑𝑗))
7774, 76breqtrd 4835 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (((2 · 𝑁)↑𝑗) · ((abs‘𝐶)↑𝑗)) ≤ ((2 · 𝑁)↑𝑗))
7859, 77eqbrtrd 4831 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (((2 · 𝑁) · (abs‘𝐶))↑𝑗) ≤ ((2 · 𝑁)↑𝑗))
7978adantrr 708 . . . . . . . 8 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (((2 · 𝑁) · (abs‘𝐶))↑𝑗) ≤ ((2 · 𝑁)↑𝑗))
8029, 40, 41, 56, 79ltletrd 10451 . . . . . . 7 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (1 / (2 · 𝐷)) < ((2 · 𝑁)↑𝑗))
8124, 28, 80ltrec1d 12090 . . . . . 6 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (1 / ((2 · 𝑁)↑𝑗)) < (2 · 𝐷))
8217, 81eqbrtrd 4831 . . . . 5 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → ((2 · 𝑁)↑-𝑗) < (2 · 𝐷))
83 nnnegz 11627 . . . . . . . . 9 (𝑗 ∈ ℕ → -𝑗 ∈ ℤ)
8483adantl 473 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → -𝑗 ∈ ℤ)
856, 13, 84reexpclzd 13241 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → ((2 · 𝑁)↑-𝑗) ∈ ℝ)
8620rpred 12070 . . . . . . . 8 (𝜑𝐷 ∈ ℝ)
8786adantr 472 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → 𝐷 ∈ ℝ)
8818a1i 11 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → 2 ∈ ℝ+)
8985, 87, 88ltdivmuld 12121 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((((2 · 𝑁)↑-𝑗) / 2) < 𝐷 ↔ ((2 · 𝑁)↑-𝑗) < (2 · 𝐷)))
9089adantrr 708 . . . . 5 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → ((((2 · 𝑁)↑-𝑗) / 2) < 𝐷 ↔ ((2 · 𝑁)↑-𝑗) < (2 · 𝐷)))
9182, 90mpbird 248 . . . 4 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (((2 · 𝑁)↑-𝑗) / 2) < 𝐷)
9247adantr 472 . . . . . 6 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (𝐸 / 𝐺) ∈ ℝ)
93 max2 12220 . . . . . . . 8 (((1 / (2 · 𝐷)) ∈ ℝ ∧ (𝐸 / 𝐺) ∈ ℝ) → (𝐸 / 𝐺) ≤ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))))
9451, 93syl 17 . . . . . . 7 (𝜑 → (𝐸 / 𝐺) ≤ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))))
9594adantr 472 . . . . . 6 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (𝐸 / 𝐺) ≤ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))))
9650, 40, 55ltled 10439 . . . . . 6 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) ≤ (((2 · 𝑁) · (abs‘𝐶))↑𝑗))
9792, 50, 40, 95, 96letrd 10448 . . . . 5 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (𝐸 / 𝐺) ≤ (((2 · 𝑁) · (abs‘𝐶))↑𝑗))
9843adantr 472 . . . . . 6 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → 𝐸 ∈ ℝ)
9944adantr 472 . . . . . 6 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → 𝐺 ∈ ℝ+)
10098, 40, 99ledivmul2d 12124 . . . . 5 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → ((𝐸 / 𝐺) ≤ (((2 · 𝑁) · (abs‘𝐶))↑𝑗) ↔ 𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺)))
10197, 100mpbid 223 . . . 4 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → 𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺))
10291, 101jca 507 . . 3 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → ((((2 · 𝑁)↑-𝑗) / 2) < 𝐷𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺)))
103 1t1e1 11440 . . . . . . . . 9 (1 · 1) = 1
104103eqcomi 2774 . . . . . . . 8 1 = (1 · 1)
105104a1i 11 . . . . . . 7 (𝜑 → 1 = (1 · 1))
1064, 34remulcld 10324 . . . . . . . 8 (𝜑 → (𝑁 · (abs‘𝐶)) ∈ ℝ)
107 0le1 10805 . . . . . . . . 9 0 ≤ 1
108107a1i 11 . . . . . . . 8 (𝜑 → 0 ≤ 1)
109 1lt2 11449 . . . . . . . . 9 1 < 2
110109a1i 11 . . . . . . . 8 (𝜑 → 1 < 2)
111 knoppndvlem18.1 . . . . . . . 8 (𝜑 → 1 < (𝑁 · (abs‘𝐶)))
11266, 2, 66, 106, 108, 110, 108, 111ltmul12ad 11219 . . . . . . 7 (𝜑 → (1 · 1) < (2 · (𝑁 · (abs‘𝐶))))
113105, 112eqbrtrd 4831 . . . . . 6 (𝜑 → 1 < (2 · (𝑁 · (abs‘𝐶))))
1142recnd 10322 . . . . . . . 8 (𝜑 → 2 ∈ ℂ)
1154recnd 10322 . . . . . . . 8 (𝜑𝑁 ∈ ℂ)
116114, 115, 57mulassd 10317 . . . . . . 7 (𝜑 → ((2 · 𝑁) · (abs‘𝐶)) = (2 · (𝑁 · (abs‘𝐶))))
117116eqcomd 2771 . . . . . 6 (𝜑 → (2 · (𝑁 · (abs‘𝐶))) = ((2 · 𝑁) · (abs‘𝐶)))
118113, 117breqtrd 4835 . . . . 5 (𝜑 → 1 < ((2 · 𝑁) · (abs‘𝐶)))
11949, 35, 1183jca 1158 . . . 4 (𝜑 → (if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) ∈ ℝ ∧ ((2 · 𝑁) · (abs‘𝐶)) ∈ ℝ ∧ 1 < ((2 · 𝑁) · (abs‘𝐶))))
120 expnbnd 13200 . . . 4 ((if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) ∈ ℝ ∧ ((2 · 𝑁) · (abs‘𝐶)) ∈ ℝ ∧ 1 < ((2 · 𝑁) · (abs‘𝐶))) → ∃𝑗 ∈ ℕ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))
121119, 120syl 17 . . 3 (𝜑 → ∃𝑗 ∈ ℕ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))
122102, 121reximddv 3164 . 2 (𝜑 → ∃𝑗 ∈ ℕ ((((2 · 𝑁)↑-𝑗) / 2) < 𝐷𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺)))
123 nnssnn0 11541 . . 3 ℕ ⊆ ℕ0
124 ssrexv 3827 . . 3 (ℕ ⊆ ℕ0 → (∃𝑗 ∈ ℕ ((((2 · 𝑁)↑-𝑗) / 2) < 𝐷𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺)) → ∃𝑗 ∈ ℕ0 ((((2 · 𝑁)↑-𝑗) / 2) < 𝐷𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺))))
125123, 124ax-mp 5 . 2 (∃𝑗 ∈ ℕ ((((2 · 𝑁)↑-𝑗) / 2) < 𝐷𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺)) → ∃𝑗 ∈ ℕ0 ((((2 · 𝑁)↑-𝑗) / 2) < 𝐷𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺)))
126122, 125syl 17 1 (𝜑 → ∃𝑗 ∈ ℕ0 ((((2 · 𝑁)↑-𝑗) / 2) < 𝐷𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wrex 3056  wss 3732  ifcif 4243   class class class wbr 4809  cfv 6068  (class class class)co 6842  cc 10187  cr 10188  0cc0 10189  1c1 10190   · cmul 10194   < clt 10328  cle 10329  -cneg 10521   / cdiv 10938  cn 11274  2c2 11327  0cn0 11538  cz 11624  +crp 12028  (,)cioo 12377  cexp 13067  abscabs 14261
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-er 7947  df-en 8161  df-dom 8162  df-sdom 8163  df-sup 8555  df-inf 8556  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-n0 11539  df-z 11625  df-uz 11887  df-rp 12029  df-ioo 12381  df-fl 12801  df-seq 13009  df-exp 13068  df-cj 14126  df-re 14127  df-im 14128  df-sqrt 14262  df-abs 14263
This theorem is referenced by:  knoppndvlem22  32895
  Copyright terms: Public domain W3C validator