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 36004
Description: Lemma for knoppndv 36009. (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 12316 . . . . . . . . . . . 12 2 ∈ ℝ
21a1i 11 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℝ)
3 knoppndvlem18.n . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℕ)
43nnred 12257 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℝ)
52, 4remulcld 11274 . . . . . . . . . 10 (𝜑 → (2 · 𝑁) ∈ ℝ)
65adantr 480 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (2 · 𝑁) ∈ ℝ)
76recnd 11272 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (2 · 𝑁) ∈ ℂ)
8 2pos 12345 . . . . . . . . . . . 12 0 < 2
98a1i 11 . . . . . . . . . . 11 (𝜑 → 0 < 2)
103nngt0d 12291 . . . . . . . . . . 11 (𝜑 → 0 < 𝑁)
112, 4, 9, 10mulgt0d 11399 . . . . . . . . . 10 (𝜑 → 0 < (2 · 𝑁))
1211gt0ne0d 11808 . . . . . . . . 9 (𝜑 → (2 · 𝑁) ≠ 0)
1312adantr 480 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → (2 · 𝑁) ≠ 0)
14 nnz 12609 . . . . . . . . 9 (𝑗 ∈ ℕ → 𝑗 ∈ ℤ)
1514adantl 481 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℤ)
167, 13, 15expnegd 14149 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → ((2 · 𝑁)↑-𝑗) = (1 / ((2 · 𝑁)↑𝑗)))
1716adantrr 716 . . . . . 6 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → ((2 · 𝑁)↑-𝑗) = (1 / ((2 · 𝑁)↑𝑗)))
18 2rp 13011 . . . . . . . . . . 11 2 ∈ ℝ+
1918a1i 11 . . . . . . . . . 10 (𝜑 → 2 ∈ ℝ+)
20 knoppndvlem18.d . . . . . . . . . 10 (𝜑𝐷 ∈ ℝ+)
2119, 20jca 511 . . . . . . . . 9 (𝜑 → (2 ∈ ℝ+𝐷 ∈ ℝ+))
22 rpmulcl 13029 . . . . . . . . 9 ((2 ∈ ℝ+𝐷 ∈ ℝ+) → (2 · 𝐷) ∈ ℝ+)
2321, 22syl 17 . . . . . . . 8 (𝜑 → (2 · 𝐷) ∈ ℝ+)
2423adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (2 · 𝐷) ∈ ℝ+)
255, 11elrpd 13045 . . . . . . . . . 10 (𝜑 → (2 · 𝑁) ∈ ℝ+)
2625adantr 480 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (2 · 𝑁) ∈ ℝ+)
2726, 15rpexpcld 14241 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → ((2 · 𝑁)↑𝑗) ∈ ℝ+)
2827adantrr 716 . . . . . . 7 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → ((2 · 𝑁)↑𝑗) ∈ ℝ+)
2924rprecred 13059 . . . . . . . 8 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (1 / (2 · 𝐷)) ∈ ℝ)
30 knoppndvlem18.c . . . . . . . . . . . . . . . 16 (𝜑𝐶 ∈ (-1(,)1))
3130knoppndvlem3 35989 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶 ∈ ℝ ∧ (abs‘𝐶) < 1))
3231simpld 494 . . . . . . . . . . . . . 14 (𝜑𝐶 ∈ ℝ)
3332recnd 11272 . . . . . . . . . . . . 13 (𝜑𝐶 ∈ ℂ)
3433abscld 15415 . . . . . . . . . . . 12 (𝜑 → (abs‘𝐶) ∈ ℝ)
355, 34remulcld 11274 . . . . . . . . . . 11 (𝜑 → ((2 · 𝑁) · (abs‘𝐶)) ∈ ℝ)
3635adantr 480 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → ((2 · 𝑁) · (abs‘𝐶)) ∈ ℝ)
37 nnnn0 12509 . . . . . . . . . . 11 (𝑗 ∈ ℕ → 𝑗 ∈ ℕ0)
3837adantl 481 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → 𝑗 ∈ ℕ0)
3936, 38reexpcld 14159 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (((2 · 𝑁) · (abs‘𝐶))↑𝑗) ∈ ℝ)
4039adantrr 716 . . . . . . . 8 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (((2 · 𝑁) · (abs‘𝐶))↑𝑗) ∈ ℝ)
4128rpred 13048 . . . . . . . 8 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → ((2 · 𝑁)↑𝑗) ∈ ℝ)
42 knoppndvlem18.e . . . . . . . . . . . . 13 (𝜑𝐸 ∈ ℝ+)
4342rpred 13048 . . . . . . . . . . . 12 (𝜑𝐸 ∈ ℝ)
44 knoppndvlem18.g . . . . . . . . . . . . 13 (𝜑𝐺 ∈ ℝ+)
4544rpred 13048 . . . . . . . . . . . 12 (𝜑𝐺 ∈ ℝ)
4644rpne0d 13053 . . . . . . . . . . . 12 (𝜑𝐺 ≠ 0)
4743, 45, 46redivcld 12072 . . . . . . . . . . 11 (𝜑 → (𝐸 / 𝐺) ∈ ℝ)
4823rprecred 13059 . . . . . . . . . . 11 (𝜑 → (1 / (2 · 𝐷)) ∈ ℝ)
4947, 48ifcld 4575 . . . . . . . . . 10 (𝜑 → if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) ∈ ℝ)
5049adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) ∈ ℝ)
5148, 47jca 511 . . . . . . . . . . 11 (𝜑 → ((1 / (2 · 𝐷)) ∈ ℝ ∧ (𝐸 / 𝐺) ∈ ℝ))
52 max1 13196 . . . . . . . . . . 11 (((1 / (2 · 𝐷)) ∈ ℝ ∧ (𝐸 / 𝐺) ∈ ℝ) → (1 / (2 · 𝐷)) ≤ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))))
5351, 52syl 17 . . . . . . . . . 10 (𝜑 → (1 / (2 · 𝐷)) ≤ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))))
5453adantr 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‘𝐶))↑𝑗))
5629, 50, 40, 54, 55lelttrd 11402 . . . . . . . 8 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (1 / (2 · 𝐷)) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))
5734recnd 11272 . . . . . . . . . . . 12 (𝜑 → (abs‘𝐶) ∈ ℂ)
5857adantr 480 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (abs‘𝐶) ∈ ℂ)
597, 58, 38mulexpd 14157 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (((2 · 𝑁) · (abs‘𝐶))↑𝑗) = (((2 · 𝑁)↑𝑗) · ((abs‘𝐶)↑𝑗)))
6034adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (abs‘𝐶) ∈ ℝ)
6160, 38reexpcld 14159 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → ((abs‘𝐶)↑𝑗) ∈ ℝ)
62 1red 11245 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 1 ∈ ℝ)
6327rpred 13048 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → ((2 · 𝑁)↑𝑗) ∈ ℝ)
6427rpge0d 13052 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → 0 ≤ ((2 · 𝑁)↑𝑗))
6533absge0d 15423 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ (abs‘𝐶))
66 1red 11245 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ∈ ℝ)
6731simprd 495 . . . . . . . . . . . . . . . . 17 (𝜑 → (abs‘𝐶) < 1)
6834, 66, 67ltled 11392 . . . . . . . . . . . . . . . 16 (𝜑 → (abs‘𝐶) ≤ 1)
6934, 65, 683jca 1126 . . . . . . . . . . . . . . 15 (𝜑 → ((abs‘𝐶) ∈ ℝ ∧ 0 ≤ (abs‘𝐶) ∧ (abs‘𝐶) ≤ 1))
7069adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ) → ((abs‘𝐶) ∈ ℝ ∧ 0 ≤ (abs‘𝐶) ∧ (abs‘𝐶) ≤ 1))
7170, 38jca 511 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ ℕ) → (((abs‘𝐶) ∈ ℝ ∧ 0 ≤ (abs‘𝐶) ∧ (abs‘𝐶) ≤ 1) ∧ 𝑗 ∈ ℕ0))
72 exple1 14172 . . . . . . . . . . . . 13 ((((abs‘𝐶) ∈ ℝ ∧ 0 ≤ (abs‘𝐶) ∧ (abs‘𝐶) ≤ 1) ∧ 𝑗 ∈ ℕ0) → ((abs‘𝐶)↑𝑗) ≤ 1)
7371, 72syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → ((abs‘𝐶)↑𝑗) ≤ 1)
7461, 62, 63, 64, 73lemul2ad 12184 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (((2 · 𝑁)↑𝑗) · ((abs‘𝐶)↑𝑗)) ≤ (((2 · 𝑁)↑𝑗) · 1))
7563recnd 11272 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ ℕ) → ((2 · 𝑁)↑𝑗) ∈ ℂ)
7675mulridd 11261 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → (((2 · 𝑁)↑𝑗) · 1) = ((2 · 𝑁)↑𝑗))
7774, 76breqtrd 5174 . . . . . . . . . 10 ((𝜑𝑗 ∈ ℕ) → (((2 · 𝑁)↑𝑗) · ((abs‘𝐶)↑𝑗)) ≤ ((2 · 𝑁)↑𝑗))
7859, 77eqbrtrd 5170 . . . . . . . . 9 ((𝜑𝑗 ∈ ℕ) → (((2 · 𝑁) · (abs‘𝐶))↑𝑗) ≤ ((2 · 𝑁)↑𝑗))
7978adantrr 716 . . . . . . . 8 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (((2 · 𝑁) · (abs‘𝐶))↑𝑗) ≤ ((2 · 𝑁)↑𝑗))
8029, 40, 41, 56, 79ltletrd 11404 . . . . . . 7 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (1 / (2 · 𝐷)) < ((2 · 𝑁)↑𝑗))
8124, 28, 80ltrec1d 13068 . . . . . 6 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (1 / ((2 · 𝑁)↑𝑗)) < (2 · 𝐷))
8217, 81eqbrtrd 5170 . . . . 5 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → ((2 · 𝑁)↑-𝑗) < (2 · 𝐷))
83 nnnegz 12591 . . . . . . . . 9 (𝑗 ∈ ℕ → -𝑗 ∈ ℤ)
8483adantl 481 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ) → -𝑗 ∈ ℤ)
856, 13, 84reexpclzd 14243 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → ((2 · 𝑁)↑-𝑗) ∈ ℝ)
8620rpred 13048 . . . . . . . 8 (𝜑𝐷 ∈ ℝ)
8786adantr 480 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → 𝐷 ∈ ℝ)
8818a1i 11 . . . . . . 7 ((𝜑𝑗 ∈ ℕ) → 2 ∈ ℝ+)
8985, 87, 88ltdivmuld 13099 . . . . . 6 ((𝜑𝑗 ∈ ℕ) → ((((2 · 𝑁)↑-𝑗) / 2) < 𝐷 ↔ ((2 · 𝑁)↑-𝑗) < (2 · 𝐷)))
9089adantrr 716 . . . . 5 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → ((((2 · 𝑁)↑-𝑗) / 2) < 𝐷 ↔ ((2 · 𝑁)↑-𝑗) < (2 · 𝐷)))
9182, 90mpbird 257 . . . 4 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (((2 · 𝑁)↑-𝑗) / 2) < 𝐷)
9247adantr 480 . . . . . 6 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (𝐸 / 𝐺) ∈ ℝ)
93 max2 13198 . . . . . . . 8 (((1 / (2 · 𝐷)) ∈ ℝ ∧ (𝐸 / 𝐺) ∈ ℝ) → (𝐸 / 𝐺) ≤ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))))
9451, 93syl 17 . . . . . . 7 (𝜑 → (𝐸 / 𝐺) ≤ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))))
9594adantr 480 . . . . . 6 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (𝐸 / 𝐺) ≤ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))))
9650, 40, 55ltled 11392 . . . . . 6 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) ≤ (((2 · 𝑁) · (abs‘𝐶))↑𝑗))
9792, 50, 40, 95, 96letrd 11401 . . . . 5 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → (𝐸 / 𝐺) ≤ (((2 · 𝑁) · (abs‘𝐶))↑𝑗))
9843adantr 480 . . . . . 6 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → 𝐸 ∈ ℝ)
9944adantr 480 . . . . . 6 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → 𝐺 ∈ ℝ+)
10098, 40, 99ledivmul2d 13102 . . . . 5 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → ((𝐸 / 𝐺) ≤ (((2 · 𝑁) · (abs‘𝐶))↑𝑗) ↔ 𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺)))
10197, 100mpbid 231 . . . 4 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → 𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺))
10291, 101jca 511 . . 3 ((𝜑 ∧ (𝑗 ∈ ℕ ∧ if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) < (((2 · 𝑁) · (abs‘𝐶))↑𝑗))) → ((((2 · 𝑁)↑-𝑗) / 2) < 𝐷𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺)))
103 1t1e1 12404 . . . . . . . . 9 (1 · 1) = 1
104103eqcomi 2737 . . . . . . . 8 1 = (1 · 1)
105104a1i 11 . . . . . . 7 (𝜑 → 1 = (1 · 1))
1064, 34remulcld 11274 . . . . . . . 8 (𝜑 → (𝑁 · (abs‘𝐶)) ∈ ℝ)
107 0le1 11767 . . . . . . . . 9 0 ≤ 1
108107a1i 11 . . . . . . . 8 (𝜑 → 0 ≤ 1)
109 1lt2 12413 . . . . . . . . 9 1 < 2
110109a1i 11 . . . . . . . 8 (𝜑 → 1 < 2)
111 knoppndvlem18.1 . . . . . . . 8 (𝜑 → 1 < (𝑁 · (abs‘𝐶)))
11266, 2, 66, 106, 108, 110, 108, 111ltmul12ad 12185 . . . . . . 7 (𝜑 → (1 · 1) < (2 · (𝑁 · (abs‘𝐶))))
113105, 112eqbrtrd 5170 . . . . . 6 (𝜑 → 1 < (2 · (𝑁 · (abs‘𝐶))))
1142recnd 11272 . . . . . . . 8 (𝜑 → 2 ∈ ℂ)
1154recnd 11272 . . . . . . . 8 (𝜑𝑁 ∈ ℂ)
116114, 115, 57mulassd 11267 . . . . . . 7 (𝜑 → ((2 · 𝑁) · (abs‘𝐶)) = (2 · (𝑁 · (abs‘𝐶))))
117116eqcomd 2734 . . . . . 6 (𝜑 → (2 · (𝑁 · (abs‘𝐶))) = ((2 · 𝑁) · (abs‘𝐶)))
118113, 117breqtrd 5174 . . . . 5 (𝜑 → 1 < ((2 · 𝑁) · (abs‘𝐶)))
11949, 35, 1183jca 1126 . . . 4 (𝜑 → (if((1 / (2 · 𝐷)) ≤ (𝐸 / 𝐺), (𝐸 / 𝐺), (1 / (2 · 𝐷))) ∈ ℝ ∧ ((2 · 𝑁) · (abs‘𝐶)) ∈ ℝ ∧ 1 < ((2 · 𝑁) · (abs‘𝐶))))
120 expnbnd 14226 . . . 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 3168 . 2 (𝜑 → ∃𝑗 ∈ ℕ ((((2 · 𝑁)↑-𝑗) / 2) < 𝐷𝐸 ≤ ((((2 · 𝑁) · (abs‘𝐶))↑𝑗) · 𝐺)))
123 nnssnn0 12505 . . 3 ℕ ⊆ ℕ0
124 ssrexv 4049 . . 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 205  wa 395  w3a 1085   = wceq 1534  wcel 2099  wne 2937  wrex 3067  wss 3947  ifcif 4529   class class class wbr 5148  cfv 6548  (class class class)co 7420  cc 11136  cr 11137  0cc0 11138  1c1 11139   · cmul 11143   < clt 11278  cle 11279  -cneg 11475   / cdiv 11901  cn 12242  2c2 12297  0cn0 12502  cz 12588  +crp 13006  (,)cioo 13356  cexp 14058  abscabs 15213
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740  ax-cnex 11194  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214  ax-pre-mulgt0 11215  ax-pre-sup 11216
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3373  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6305  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-riota 7376  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7871  df-1st 7993  df-2nd 7994  df-frecs 8286  df-wrecs 8317  df-recs 8391  df-rdg 8430  df-er 8724  df-en 8964  df-dom 8965  df-sdom 8966  df-sup 9465  df-inf 9466  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284  df-sub 11476  df-neg 11477  df-div 11902  df-nn 12243  df-2 12305  df-3 12306  df-n0 12503  df-z 12589  df-uz 12853  df-rp 13007  df-ioo 13360  df-fl 13789  df-seq 13999  df-exp 14059  df-cj 15078  df-re 15079  df-im 15080  df-sqrt 15214  df-abs 15215
This theorem is referenced by:  knoppndvlem22  36008
  Copyright terms: Public domain W3C validator