# Metamath Proof Explorer

## Theorem knoppndvlem18

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

Ref Expression
Hypotheses knoppndvlem18.c ${⊢}{\phi }\to {C}\in \left(-1,1\right)$
knoppndvlem18.n ${⊢}{\phi }\to {N}\in ℕ$
knoppndvlem18.d ${⊢}{\phi }\to {D}\in {ℝ}^{+}$
knoppndvlem18.e ${⊢}{\phi }\to {E}\in {ℝ}^{+}$
knoppndvlem18.g ${⊢}{\phi }\to {G}\in {ℝ}^{+}$
knoppndvlem18.1 ${⊢}{\phi }\to 1<{N}\left|{C}\right|$
Assertion knoppndvlem18 ${⊢}{\phi }\to \exists {j}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\frac{{2\cdot {N}}^{-{j}}}{2}<{D}\wedge {E}\le {2\cdot {N}\left|{C}\right|}^{{j}}{G}\right)$

### Proof

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