knoppndvlem18

	Ref	Expression
Hypotheses	knoppndvlem18.c	$⊢ φ \to C \in (- 1, 1)$
	knoppndvlem18.n	$⊢ φ \to N \in ℕ$
	knoppndvlem18.d	$⊢ φ \to D \in ℝ^{+}$
	knoppndvlem18.e	$⊢ φ \to E \in ℝ^{+}$
	knoppndvlem18.g	$⊢ φ \to G \in ℝ^{+}$
	knoppndvlem18.1	$⊢ φ \to 1 < N \|C\|$
Assertion	knoppndvlem18	$⊢ φ \to \exists j \in ℕ_{0} (\frac{{2 \cdot N}^{- j}}{2} < D \land E \leq {2 \cdot N \|C\|}^{j} G)$

Proof

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

Metamath Proof Explorer

Theorem knoppndvlem18

Proof