Metamath Proof Explorer

Theorem knoppndvlem18

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 14-Aug-2021)

Ref Expression
Hypotheses knoppndvlem18.c ⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
knoppndvlem18.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
knoppndvlem18.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
knoppndvlem18.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
knoppndvlem18.g ⊢ ( 𝜑 → 𝐺 ∈ ℝ+ )
knoppndvlem18.1 ⊢ ( 𝜑 → 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) )
Assertion knoppndvlem18 ( 𝜑 → ∃ 𝑗 ∈ ℕ0 ( ( ( ( 2 · 𝑁 ) ↑ - 𝑗 ) / 2 ) < 𝐷 ∧ 𝐸 ≤ ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) · 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 knoppndvlem18.c ⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
2 knoppndvlem18.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 knoppndvlem18.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
4 knoppndvlem18.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
5 knoppndvlem18.g ⊢ ( 𝜑 → 𝐺 ∈ ℝ+ )
6 knoppndvlem18.1 ⊢ ( 𝜑 → 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) )
7 2re ⊢ 2 ∈ ℝ
8 7 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
9 2 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
10 8 9 remulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
11 10 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 · 𝑁 ) ∈ ℝ )
12 11 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 · 𝑁 ) ∈ ℂ )
13 2pos ⊢ 0 < 2
14 13 a1i ⊢ ( 𝜑 → 0 < 2 )
15 2 nngt0d ⊢ ( 𝜑 → 0 < 𝑁 )
16 8 9 14 15 mulgt0d ⊢ ( 𝜑 → 0 < ( 2 · 𝑁 ) )
17 16 gt0ne0d ⊢ ( 𝜑 → ( 2 · 𝑁 ) ≠ 0 )
18 17 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 · 𝑁 ) ≠ 0 )
19 nnz ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℤ )
20 19 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℤ )
21 12 18 20 expnegd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 2 · 𝑁 ) ↑ - 𝑗 ) = ( 1 / ( ( 2 · 𝑁 ) ↑ 𝑗 ) ) )
22 21 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ) ) → ( ( 2 · 𝑁 ) ↑ - 𝑗 ) = ( 1 / ( ( 2 · 𝑁 ) ↑ 𝑗 ) ) )
23 2rp ⊢ 2 ∈ ℝ+
24 23 a1i ⊢ ( 𝜑 → 2 ∈ ℝ+ )
25 24 3 jca ⊢ ( 𝜑 → ( 2 ∈ ℝ+ ∧ 𝐷 ∈ ℝ+ ) )
26 rpmulcl ⊢ ( ( 2 ∈ ℝ+ ∧ 𝐷 ∈ ℝ+ ) → ( 2 · 𝐷 ) ∈ ℝ+ )
27 25 26 syl ⊢ ( 𝜑 → ( 2 · 𝐷 ) ∈ ℝ+ )
28 27 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ) ) → ( 2 · 𝐷 ) ∈ ℝ+ )
29 10 16 elrpd ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ+ )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 2 · 𝑁 ) ∈ ℝ+ )
31 30 20 rpexpcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 2 · 𝑁 ) ↑ 𝑗 ) ∈ ℝ+ )
32 31 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ) ) → ( ( 2 · 𝑁 ) ↑ 𝑗 ) ∈ ℝ+ )
33 28 rprecred ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ) ) → ( 1 / ( 2 · 𝐷 ) ) ∈ ℝ )
34 1 knoppndvlem3 ⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ ( abs ‘ 𝐶 ) < 1 ) )
35 34 simpld ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
36 35 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
37 36 abscld ⊢ ( 𝜑 → ( abs ‘ 𝐶 ) ∈ ℝ )
38 10 37 remulcld ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ∈ ℝ )
39 38 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ∈ ℝ )
40 nnnn0 ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℕ0 )
41 40 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ0 )
42 39 41 reexpcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ∈ ℝ )
43 42 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ) ) → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ∈ ℝ )
44 32 rpred ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ) ) → ( ( 2 · 𝑁 ) ↑ 𝑗 ) ∈ ℝ )
45 4 rpred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
46 5 rpred ⊢ ( 𝜑 → 𝐺 ∈ ℝ )
47 5 rpne0d ⊢ ( 𝜑 → 𝐺 ≠ 0 )
48 45 46 47 redivcld ⊢ ( 𝜑 → ( 𝐸 / 𝐺 ) ∈ ℝ )
49 27 rprecred ⊢ ( 𝜑 → ( 1 / ( 2 · 𝐷 ) ) ∈ ℝ )
50 48 49 ifcld ⊢ ( 𝜑 → if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) ∈ ℝ )
51 50 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ) ) → if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) ∈ ℝ )
52 49 48 jca ⊢ ( 𝜑 → ( ( 1 / ( 2 · 𝐷 ) ) ∈ ℝ ∧ ( 𝐸 / 𝐺 ) ∈ ℝ ) )
53 max1 ⊢ ( ( ( 1 / ( 2 · 𝐷 ) ) ∈ ℝ ∧ ( 𝐸 / 𝐺 ) ∈ ℝ ) → ( 1 / ( 2 · 𝐷 ) ) ≤ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) )
54 52 53 syl ⊢ ( 𝜑 → ( 1 / ( 2 · 𝐷 ) ) ≤ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) )
55 54 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ) ) → ( 1 / ( 2 · 𝐷 ) ) ≤ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) )
56 simprr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ) ) → if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) )
57 33 51 43 55 56 lelttrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ) ) → ( 1 / ( 2 · 𝐷 ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) )
58 37 recnd ⊢ ( 𝜑 → ( abs ‘ 𝐶 ) ∈ ℂ )
59 58 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( abs ‘ 𝐶 ) ∈ ℂ )
60 12 59 41 mulexpd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) = ( ( ( 2 · 𝑁 ) ↑ 𝑗 ) · ( ( abs ‘ 𝐶 ) ↑ 𝑗 ) ) )
61 37 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( abs ‘ 𝐶 ) ∈ ℝ )
62 61 41 reexpcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( abs ‘ 𝐶 ) ↑ 𝑗 ) ∈ ℝ )
63 1red ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 1 ∈ ℝ )
64 31 rpred ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 2 · 𝑁 ) ↑ 𝑗 ) ∈ ℝ )
65 31 rpge0d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 0 ≤ ( ( 2 · 𝑁 ) ↑ 𝑗 ) )
66 36 absge0d ⊢ ( 𝜑 → 0 ≤ ( abs ‘ 𝐶 ) )
67 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
68 34 simprd ⊢ ( 𝜑 → ( abs ‘ 𝐶 ) < 1 )
69 37 67 68 ltled ⊢ ( 𝜑 → ( abs ‘ 𝐶 ) ≤ 1 )
70 37 66 69 3jca ⊢ ( 𝜑 → ( ( abs ‘ 𝐶 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐶 ) ∧ ( abs ‘ 𝐶 ) ≤ 1 ) )
71 70 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( abs ‘ 𝐶 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐶 ) ∧ ( abs ‘ 𝐶 ) ≤ 1 ) )
72 71 41 jca ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( ( abs ‘ 𝐶 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐶 ) ∧ ( abs ‘ 𝐶 ) ≤ 1 ) ∧ 𝑗 ∈ ℕ0 ) )
73 exple1 ⊢ ( ( ( ( abs ‘ 𝐶 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐶 ) ∧ ( abs ‘ 𝐶 ) ≤ 1 ) ∧ 𝑗 ∈ ℕ0 ) → ( ( abs ‘ 𝐶 ) ↑ 𝑗 ) ≤ 1 )
74 72 73 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( abs ‘ 𝐶 ) ↑ 𝑗 ) ≤ 1 )
75 62 63 64 65 74 lemul2ad ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( ( 2 · 𝑁 ) ↑ 𝑗 ) · ( ( abs ‘ 𝐶 ) ↑ 𝑗 ) ) ≤ ( ( ( 2 · 𝑁 ) ↑ 𝑗 ) · 1 ) )
76 64 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 2 · 𝑁 ) ↑ 𝑗 ) ∈ ℂ )
77 76 mulridd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( ( 2 · 𝑁 ) ↑ 𝑗 ) · 1 ) = ( ( 2 · 𝑁 ) ↑ 𝑗 ) )
78 75 77 breqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( ( 2 · 𝑁 ) ↑ 𝑗 ) · ( ( abs ‘ 𝐶 ) ↑ 𝑗 ) ) ≤ ( ( 2 · 𝑁 ) ↑ 𝑗 ) )
79 60 78 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ≤ ( ( 2 · 𝑁 ) ↑ 𝑗 ) )
80 79 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ) ) → ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ≤ ( ( 2 · 𝑁 ) ↑ 𝑗 ) )
81 33 43 44 57 80 ltletrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ) ) → ( 1 / ( 2 · 𝐷 ) ) < ( ( 2 · 𝑁 ) ↑ 𝑗 ) )
82 28 32 81 ltrec1d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ) ) → ( 1 / ( ( 2 · 𝑁 ) ↑ 𝑗 ) ) < ( 2 · 𝐷 ) )
83 22 82 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ) ) → ( ( 2 · 𝑁 ) ↑ - 𝑗 ) < ( 2 · 𝐷 ) )
84 nnnegz ⊢ ( 𝑗 ∈ ℕ → - 𝑗 ∈ ℤ )
85 84 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → - 𝑗 ∈ ℤ )
86 11 18 85 reexpclzd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 2 · 𝑁 ) ↑ - 𝑗 ) ∈ ℝ )
87 3 rpred ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
88 87 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝐷 ∈ ℝ )
89 23 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 2 ∈ ℝ+ )
90 86 88 89 ltdivmuld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( ( ( 2 · 𝑁 ) ↑ - 𝑗 ) / 2 ) < 𝐷 ↔ ( ( 2 · 𝑁 ) ↑ - 𝑗 ) < ( 2 · 𝐷 ) ) )
91 90 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ) ) → ( ( ( ( 2 · 𝑁 ) ↑ - 𝑗 ) / 2 ) < 𝐷 ↔ ( ( 2 · 𝑁 ) ↑ - 𝑗 ) < ( 2 · 𝐷 ) ) )
92 83 91 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ) ) → ( ( ( 2 · 𝑁 ) ↑ - 𝑗 ) / 2 ) < 𝐷 )
93 48 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ) ) → ( 𝐸 / 𝐺 ) ∈ ℝ )
94 max2 ⊢ ( ( ( 1 / ( 2 · 𝐷 ) ) ∈ ℝ ∧ ( 𝐸 / 𝐺 ) ∈ ℝ ) → ( 𝐸 / 𝐺 ) ≤ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) )
95 52 94 syl ⊢ ( 𝜑 → ( 𝐸 / 𝐺 ) ≤ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) )
96 95 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ) ) → ( 𝐸 / 𝐺 ) ≤ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) )
97 51 43 56 ltled ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ) ) → if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) ≤ ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) )
98 93 51 43 96 97 letrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ) ) → ( 𝐸 / 𝐺 ) ≤ ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) )
99 45 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ) ) → 𝐸 ∈ ℝ )
100 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ) ) → 𝐺 ∈ ℝ+ )
101 99 43 100 ledivmul2d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ) ) → ( ( 𝐸 / 𝐺 ) ≤ ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ↔ 𝐸 ≤ ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) · 𝐺 ) ) )
102 98 101 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ) ) → 𝐸 ≤ ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) · 𝐺 ) )
103 92 102 jca ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ ∧ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) ) ) → ( ( ( ( 2 · 𝑁 ) ↑ - 𝑗 ) / 2 ) < 𝐷 ∧ 𝐸 ≤ ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) · 𝐺 ) ) )
104 1t1e1 ⊢ ( 1 · 1 ) = 1
105 104 eqcomi ⊢ 1 = ( 1 · 1 )
106 105 a1i ⊢ ( 𝜑 → 1 = ( 1 · 1 ) )
107 9 37 remulcld ⊢ ( 𝜑 → ( 𝑁 · ( abs ‘ 𝐶 ) ) ∈ ℝ )
108 0le1 ⊢ 0 ≤ 1
109 108 a1i ⊢ ( 𝜑 → 0 ≤ 1 )
110 1lt2 ⊢ 1 < 2
111 110 a1i ⊢ ( 𝜑 → 1 < 2 )
112 67 8 67 107 109 111 109 6 ltmul12ad ⊢ ( 𝜑 → ( 1 · 1 ) < ( 2 · ( 𝑁 · ( abs ‘ 𝐶 ) ) ) )
113 106 112 eqbrtrd ⊢ ( 𝜑 → 1 < ( 2 · ( 𝑁 · ( abs ‘ 𝐶 ) ) ) )
114 8 recnd ⊢ ( 𝜑 → 2 ∈ ℂ )
115 9 recnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
116 114 115 58 mulassd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) = ( 2 · ( 𝑁 · ( abs ‘ 𝐶 ) ) ) )
117 116 eqcomd ⊢ ( 𝜑 → ( 2 · ( 𝑁 · ( abs ‘ 𝐶 ) ) ) = ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) )
118 113 117 breqtrd ⊢ ( 𝜑 → 1 < ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) )
119 50 38 118 3jca ⊢ ( 𝜑 → ( if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) ∈ ℝ ∧ ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ∈ ℝ ∧ 1 < ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ) )
120 expnbnd ⊢ ( ( if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) ∈ ℝ ∧ ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ∈ ℝ ∧ 1 < ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ) → ∃ 𝑗 ∈ ℕ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) )
121 119 120 syl ⊢ ( 𝜑 → ∃ 𝑗 ∈ ℕ if ( ( 1 / ( 2 · 𝐷 ) ) ≤ ( 𝐸 / 𝐺 ) , ( 𝐸 / 𝐺 ) , ( 1 / ( 2 · 𝐷 ) ) ) < ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) )
122 103 121 reximddv ⊢ ( 𝜑 → ∃ 𝑗 ∈ ℕ ( ( ( ( 2 · 𝑁 ) ↑ - 𝑗 ) / 2 ) < 𝐷 ∧ 𝐸 ≤ ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) · 𝐺 ) ) )
123 nnssnn0 ⊢ ℕ ⊆ ℕ0
124 ssrexv ⊢ ( ℕ ⊆ ℕ0 → ( ∃ 𝑗 ∈ ℕ ( ( ( ( 2 · 𝑁 ) ↑ - 𝑗 ) / 2 ) < 𝐷 ∧ 𝐸 ≤ ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) · 𝐺 ) ) → ∃ 𝑗 ∈ ℕ0 ( ( ( ( 2 · 𝑁 ) ↑ - 𝑗 ) / 2 ) < 𝐷 ∧ 𝐸 ≤ ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) · 𝐺 ) ) ) )
125 123 124 ax-mp ⊢ ( ∃ 𝑗 ∈ ℕ ( ( ( ( 2 · 𝑁 ) ↑ - 𝑗 ) / 2 ) < 𝐷 ∧ 𝐸 ≤ ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) · 𝐺 ) ) → ∃ 𝑗 ∈ ℕ0 ( ( ( ( 2 · 𝑁 ) ↑ - 𝑗 ) / 2 ) < 𝐷 ∧ 𝐸 ≤ ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) · 𝐺 ) ) )
126 122 125 syl ⊢ ( 𝜑 → ∃ 𝑗 ∈ ℕ0 ( ( ( ( 2 · 𝑁 ) ↑ - 𝑗 ) / 2 ) < 𝐷 ∧ 𝐸 ≤ ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) · 𝐺 ) ) )