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 \mathbb{N}$$
	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 {\mathbb{N}}_0\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}}{2}<D\wedge E\le {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\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 \mathbb{N}$$
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 \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ$$
11	10	adantr	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ$$
12	11	recnd	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\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 \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
17	16	gt0ne0d	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\ne 0$$
18	17	adantr	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\ne 0$$
19		nnz	$$⊢j\in \mathbb{N}\to j\in \mathbb{Z}$$
20	19	adantl	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to j\in \mathbb{Z}$$
21	12 18 20	expnegd	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}=\frac{1}{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^j}$$
22	21	adantrr	$$⊢\left(\phi \wedge \left(j\in \mathbb{N}\wedge if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\right)\right)\to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}=\frac{1}{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^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 2D\in {ℝ}^{+}$$
27	25 26	syl	$$⊢\phi \to 2D\in {ℝ}^{+}$$
28	27	adantr	$$⊢\left(\phi \wedge \left(j\in \mathbb{N}\wedge if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\right)\right)\to 2D\in {ℝ}^{+}$$
29	10 16	elrpd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in {ℝ}^{+}$$
30	29	adantr	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in {ℝ}^{+}$$
31	30 20	rpexpcld	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^j\in {ℝ}^{+}$$
32	31	adantrr	$$⊢\left(\phi \wedge \left(j\in \mathbb{N}\wedge if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\right)\right)\to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^j\in {ℝ}^{+}$$
33	28	rprecred	$$⊢\left(\phi \wedge \left(j\in \mathbb{N}\wedge if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\right)\right)\to \frac{1}{2D}\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 \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|\in ℝ$$
39	38	adantr	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|\in ℝ$$
40		nnnn0	$$⊢j\in \mathbb{N}\to j\in {\mathbb{N}}_0$$
41	40	adantl	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to j\in {\mathbb{N}}_0$$
42	39 41	reexpcld	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\in ℝ$$
43	42	adantrr	$$⊢\left(\phi \wedge \left(j\in \mathbb{N}\wedge if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\right)\right)\to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\in ℝ$$
44	32	rpred	$$⊢\left(\phi \wedge \left(j\in \mathbb{N}\wedge if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\right)\right)\to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^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}{2D}\in ℝ$$
50	48 49	ifcld	$$⊢\phi \to if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)\in ℝ$$
51	50	adantr	$$⊢\left(\phi \wedge \left(j\in \mathbb{N}\wedge if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\right)\right)\to if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)\in ℝ$$
52	49 48	jca	$$⊢\phi \to \left(\frac{1}{2D}\in ℝ\wedge \frac{E}{G}\in ℝ\right)$$
53		max1	$$⊢\left(\frac{1}{2D}\in ℝ\wedge \frac{E}{G}\in ℝ\right)\to \frac{1}{2D}\le if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)$$
54	52 53	syl	$$⊢\phi \to \frac{1}{2D}\le if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)$$
55	54	adantr	$$⊢\left(\phi \wedge \left(j\in \mathbb{N}\wedge if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\right)\right)\to \frac{1}{2D}\le if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)$$
56		simprr	$$⊢\left(\phi \wedge \left(j\in \mathbb{N}\wedge if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\right)\right)\to if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j$$
57	33 51 43 55 56	lelttrd	$$⊢\left(\phi \wedge \left(j\in \mathbb{N}\wedge if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\right)\right)\to \frac{1}{2D}<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j$$
58	37	recnd	$$⊢\phi \to \left|C\right|\in ℂ$$
59	58	adantr	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to \left|C\right|\in ℂ$$
60	12 59 41	mulexpd	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^j{\left|C\right|}^j$$
61	37	adantr	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to \left|C\right|\in ℝ$$
62	61 41	reexpcld	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to {\left|C\right|}^j\in ℝ$$
63		1red	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to 1\in ℝ$$
64	31	rpred	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^j\in ℝ$$
65	31	rpge0d	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to 0\le {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^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 \mathbb{N}\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 \mathbb{N}\right)\to \left(\left(\left|C\right|\in ℝ\wedge 0\le \left|C\right|\wedge \left|C\right|\le 1\right)\wedge j\in {\mathbb{N}}_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 {\mathbb{N}}_0\right)\to {\left|C\right|}^j\le 1$$
74	72 73	syl	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to {\left|C\right|}^j\le 1$$
75	62 63 64 65 74	lemul2ad	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^j{\left|C\right|}^j\le {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^j\cdot 1$$
76	64	recnd	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^j\in ℂ$$
77	76	mulridd	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^j\cdot 1={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^j$$
78	75 77	breqtrd	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^j{\left|C\right|}^j\le {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^j$$
79	60 78	eqbrtrd	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\le {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^j$$
80	79	adantrr	$$⊢\left(\phi \wedge \left(j\in \mathbb{N}\wedge if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\right)\right)\to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\le {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^j$$
81	33 43 44 57 80	ltletrd	$$⊢\left(\phi \wedge \left(j\in \mathbb{N}\wedge if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\right)\right)\to \frac{1}{2D}<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^j$$
82	28 32 81	ltrec1d	$$⊢\left(\phi \wedge \left(j\in \mathbb{N}\wedge if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\right)\right)\to \frac{1}{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^j}<2D$$
83	22 82	eqbrtrd	$$⊢\left(\phi \wedge \left(j\in \mathbb{N}\wedge if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\right)\right)\to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}<2D$$
84		nnnegz	$$⊢j\in \mathbb{N}\to -j\in \mathbb{Z}$$
85	84	adantl	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to -j\in \mathbb{Z}$$
86	11 18 85	reexpclzd	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}\in ℝ$$
87	3	rpred	$$⊢\phi \to D\in ℝ$$
88	87	adantr	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to D\in ℝ$$
89	23	a1i	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to 2\in {ℝ}^{+}$$
90	86 88 89	ltdivmuld	$$⊢\left(\phi \wedge j\in \mathbb{N}\right)\to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}}{2}<D\leftrightarrow {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}<2D\right)$$
91	90	adantrr	$$⊢\left(\phi \wedge \left(j\in \mathbb{N}\wedge if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\right)\right)\to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}}{2}<D\leftrightarrow {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}<2D\right)$$
92	83 91	mpbird	$$⊢\left(\phi \wedge \left(j\in \mathbb{N}\wedge if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\right)\right)\to \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}}{2}<D$$
93	48	adantr	$$⊢\left(\phi \wedge \left(j\in \mathbb{N}\wedge if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\right)\right)\to \frac{E}{G}\in ℝ$$
94		max2	$$⊢\left(\frac{1}{2D}\in ℝ\wedge \frac{E}{G}\in ℝ\right)\to \frac{E}{G}\le if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)$$
95	52 94	syl	$$⊢\phi \to \frac{E}{G}\le if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)$$
96	95	adantr	$$⊢\left(\phi \wedge \left(j\in \mathbb{N}\wedge if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\right)\right)\to \frac{E}{G}\le if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)$$
97	51 43 56	ltled	$$⊢\left(\phi \wedge \left(j\in \mathbb{N}\wedge if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\right)\right)\to if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)\le {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j$$
98	93 51 43 96 97	letrd	$$⊢\left(\phi \wedge \left(j\in \mathbb{N}\wedge if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\right)\right)\to \frac{E}{G}\le {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j$$
99	45	adantr	$$⊢\left(\phi \wedge \left(j\in \mathbb{N}\wedge if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\right)\right)\to E\in ℝ$$
100	5	adantr	$$⊢\left(\phi \wedge \left(j\in \mathbb{N}\wedge if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\right)\right)\to G\in {ℝ}^{+}$$
101	99 43 100	ledivmul2d	$$⊢\left(\phi \wedge \left(j\in \mathbb{N}\wedge if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\right)\right)\to \left(\frac{E}{G}\le {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\leftrightarrow E\le {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^{j}G\right)$$
102	98 101	mpbid	$$⊢\left(\phi \wedge \left(j\in \mathbb{N}\wedge if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\right)\right)\to E\le {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^{j}G$$
103	92 102	jca	$$⊢\left(\phi \wedge \left(j\in \mathbb{N}\wedge if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j\right)\right)\to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}}{2}<D\wedge E\le {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\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<2N\left|C\right|$$
113	106 112	eqbrtrd	$$⊢\phi \to 1<2N\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 \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|=2N\left|C\right|$$
117	116	eqcomd	$$⊢\phi \to 2N\left|C\right|=2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|$$
118	113 117	breqtrd	$$⊢\phi \to 1<2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|$$
119	50 38 118	3jca	$$⊢\phi \to \left(if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)\in ℝ\wedge 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|\in ℝ\wedge 1<2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|\right)$$
120		expnbnd	$$⊢\left(if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)\in ℝ\wedge 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|\in ℝ\wedge 1<2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|\right)\to \exists j\in \mathbb{N}if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j$$
121	119 120	syl	$$⊢\phi \to \exists j\in \mathbb{N}if\left(\frac{1}{2D}\le \frac{E}{G},\frac{E}{G},\frac{1}{2D}\right)<{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^j$$
122	103 121	reximddv	$$⊢\phi \to \exists j\in \mathbb{N}\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}}{2}<D\wedge E\le {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^{j}G\right)$$
123		nnssnn0	$$⊢\mathbb{N}\subseteq {\mathbb{N}}_0$$
124		ssrexv	$$⊢\mathbb{N}\subseteq {\mathbb{N}}_0\to \left(\exists j\in \mathbb{N}\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}}{2}<D\wedge E\le {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^{j}G\right)\to \exists j\in {\mathbb{N}}_0\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}}{2}<D\wedge E\le {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^{j}G\right)\right)$$
125	123 124	ax-mp	$$⊢\exists j\in \mathbb{N}\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}}{2}<D\wedge E\le {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^{j}G\right)\to \exists j\in {\mathbb{N}}_0\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}}{2}<D\wedge E\le {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^{j}G\right)$$
126	122 125	syl	$$⊢\phi \to \exists j\in {\mathbb{N}}_0\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-j}}{2}<D\wedge E\le {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\left|C\right|}^{j}G\right)$$