knoppndvlem21

	Ref	Expression
Hypotheses	knoppndvlem21.t	$⊢ T = (x \in ℝ ⟼ \|⌊x + (\frac{1}{2})⌋ - x\|)$
	knoppndvlem21.f	$⊢ F = (y \in ℝ ⟼ (n \in ℕ_{0} ⟼ C^{n} T ({2 \cdot N}^{n} y)))$
	knoppndvlem21.w	$⊢ W = (w \in ℝ ⟼ \sum_{i \in ℕ_{0}} F (w) (i))$
	knoppndvlem21.g	$⊢ G = 1 - (\frac{1}{2 \cdot N \|C\| - 1})$
	knoppndvlem21.c	$⊢ φ \to C \in (- 1, 1)$
	knoppndvlem21.d	$⊢ φ \to D \in ℝ^{+}$
	knoppndvlem21.e	$⊢ φ \to E \in ℝ^{+}$
	knoppndvlem21.h	$⊢ φ \to H \in ℝ$
	knoppndvlem21.j	$⊢ φ \to J \in ℕ_{0}$
	knoppndvlem21.n	$⊢ φ \to N \in ℕ$
	knoppndvlem21.1	$⊢ φ \to 1 < N \|C\|$
	knoppndvlem21.2	$⊢ φ \to \frac{{2 \cdot N}^{- J}}{2} < D$
	knoppndvlem21.3	$⊢ φ \to E \leq {2 \cdot N \|C\|}^{J} G$
Assertion	knoppndvlem21	$⊢ φ \to \exists a \in ℝ \exists b \in ℝ ((a \leq H \land H \leq b) \land (b - a < D \land a \neq b) \land E \leq \frac{\|W (b) - W (a)\|}{b - a})$

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem21.t	$⊢ T = (x \in ℝ ⟼ \|⌊x + (\frac{1}{2})⌋ - x\|)$
2		knoppndvlem21.f	$⊢ F = (y \in ℝ ⟼ (n \in ℕ_{0} ⟼ C^{n} T ({2 \cdot N}^{n} y)))$
3		knoppndvlem21.w	$⊢ W = (w \in ℝ ⟼ \sum_{i \in ℕ_{0}} F (w) (i))$
4		knoppndvlem21.g	$⊢ G = 1 - (\frac{1}{2 \cdot N \|C\| - 1})$
5		knoppndvlem21.c	$⊢ φ \to C \in (- 1, 1)$
6		knoppndvlem21.d	$⊢ φ \to D \in ℝ^{+}$
7		knoppndvlem21.e	$⊢ φ \to E \in ℝ^{+}$
8		knoppndvlem21.h	$⊢ φ \to H \in ℝ$
9		knoppndvlem21.j	$⊢ φ \to J \in ℕ_{0}$
10		knoppndvlem21.n	$⊢ φ \to N \in ℕ$
11		knoppndvlem21.1	$⊢ φ \to 1 < N \|C\|$
12		knoppndvlem21.2	$⊢ φ \to \frac{{2 \cdot N}^{- J}}{2} < D$
13		knoppndvlem21.3	$⊢ φ \to E \leq {2 \cdot N \|C\|}^{J} G$
14		eqid	$⊢ (\frac{{2 \cdot N}^{- J}}{2}) m = (\frac{{2 \cdot N}^{- J}}{2}) m$
15		eqid	$⊢ (\frac{{2 \cdot N}^{- J}}{2}) (m + 1) = (\frac{{2 \cdot N}^{- J}}{2}) (m + 1)$
16	14 15 9 8 10	knoppndvlem19	$⊢ φ \to \exists m \in ℤ ((\frac{{2 \cdot N}^{- J}}{2}) m \leq H \land H \leq (\frac{{2 \cdot N}^{- J}}{2}) (m + 1))$
17		2re	$⊢ 2 \in ℝ$
18	17	a1i	$⊢ φ \to 2 \in ℝ$
19	10	nnred	$⊢ φ \to N \in ℝ$
20	18 19	remulcld	$⊢ φ \to 2 \cdot N \in ℝ$
21		2pos	$⊢ 0 < 2$
22	21	a1i	$⊢ φ \to 0 < 2$
23	10	nngt0d	$⊢ φ \to 0 < N$
24	18 19 22 23	mulgt0d	$⊢ φ \to 0 < 2 \cdot N$
25	24	gt0ne0d	$⊢ φ \to 2 \cdot N \neq 0$
26	9	nn0zd	$⊢ φ \to J \in ℤ$
27	26	znegcld	$⊢ φ \to - J \in ℤ$
28	20 25 27	reexpclzd	$⊢ φ \to {2 \cdot N}^{- J} \in ℝ$
29	28	rehalfcld	$⊢ φ \to \frac{{2 \cdot N}^{- J}}{2} \in ℝ$
30	29	adantr	$⊢ (φ \land m \in ℤ) \to \frac{{2 \cdot N}^{- J}}{2} \in ℝ$
31		simpr	$⊢ (φ \land m \in ℤ) \to m \in ℤ$
32	31	zred	$⊢ (φ \land m \in ℤ) \to m \in ℝ$
33	30 32	remulcld	$⊢ (φ \land m \in ℤ) \to (\frac{{2 \cdot N}^{- J}}{2}) m \in ℝ$
34	33	adantrr	$⊢ (φ \land (m \in ℤ \land ((\frac{{2 \cdot N}^{- J}}{2}) m \leq H \land H \leq (\frac{{2 \cdot N}^{- J}}{2}) (m + 1)))) \to (\frac{{2 \cdot N}^{- J}}{2}) m \in ℝ$
35		peano2re	$⊢ m \in ℝ \to m + 1 \in ℝ$
36	32 35	syl	$⊢ (φ \land m \in ℤ) \to m + 1 \in ℝ$
37	30 36	jca	$⊢ (φ \land m \in ℤ) \to (\frac{{2 \cdot N}^{- J}}{2} \in ℝ \land m + 1 \in ℝ)$
38		remulcl	$⊢ (\frac{{2 \cdot N}^{- J}}{2} \in ℝ \land m + 1 \in ℝ) \to (\frac{{2 \cdot N}^{- J}}{2}) (m + 1) \in ℝ$
39	37 38	syl	$⊢ (φ \land m \in ℤ) \to (\frac{{2 \cdot N}^{- J}}{2}) (m + 1) \in ℝ$
40	39	adantrr	$⊢ (φ \land (m \in ℤ \land ((\frac{{2 \cdot N}^{- J}}{2}) m \leq H \land H \leq (\frac{{2 \cdot N}^{- J}}{2}) (m + 1)))) \to (\frac{{2 \cdot N}^{- J}}{2}) (m + 1) \in ℝ$
41		simprr	$⊢ (φ \land (m \in ℤ \land ((\frac{{2 \cdot N}^{- J}}{2}) m \leq H \land H \leq (\frac{{2 \cdot N}^{- J}}{2}) (m + 1)))) \to ((\frac{{2 \cdot N}^{- J}}{2}) m \leq H \land H \leq (\frac{{2 \cdot N}^{- J}}{2}) (m + 1))$
42	9	adantr	$⊢ (φ \land m \in ℤ) \to J \in ℕ_{0}$
43	10	adantr	$⊢ (φ \land m \in ℤ) \to N \in ℕ$
44	14 15 42 31 43	knoppndvlem16	$⊢ (φ \land m \in ℤ) \to (\frac{{2 \cdot N}^{- J}}{2}) (m + 1) - (\frac{{2 \cdot N}^{- J}}{2}) m = \frac{{2 \cdot N}^{- J}}{2}$
45	12	adantr	$⊢ (φ \land m \in ℤ) \to \frac{{2 \cdot N}^{- J}}{2} < D$
46	44 45	eqbrtrd	$⊢ (φ \land m \in ℤ) \to (\frac{{2 \cdot N}^{- J}}{2}) (m + 1) - (\frac{{2 \cdot N}^{- J}}{2}) m < D$
47	20 27 24	3jca	$⊢ φ \to (2 \cdot N \in ℝ \land - J \in ℤ \land 0 < 2 \cdot N)$
48		expgt0	$⊢ (2 \cdot N \in ℝ \land - J \in ℤ \land 0 < 2 \cdot N) \to 0 < {2 \cdot N}^{- J}$
49	47 48	syl	$⊢ φ \to 0 < {2 \cdot N}^{- J}$
50	28 18 49 22	divgt0d	$⊢ φ \to 0 < \frac{{2 \cdot N}^{- J}}{2}$
51	50	adantr	$⊢ (φ \land m \in ℤ) \to 0 < \frac{{2 \cdot N}^{- J}}{2}$
52	44	eqcomd	$⊢ (φ \land m \in ℤ) \to \frac{{2 \cdot N}^{- J}}{2} = (\frac{{2 \cdot N}^{- J}}{2}) (m + 1) - (\frac{{2 \cdot N}^{- J}}{2}) m$
53	51 52	breqtrd	$⊢ (φ \land m \in ℤ) \to 0 < (\frac{{2 \cdot N}^{- J}}{2}) (m + 1) - (\frac{{2 \cdot N}^{- J}}{2}) m$
54	33 39	posdifd	$⊢ (φ \land m \in ℤ) \to ((\frac{{2 \cdot N}^{- J}}{2}) m < (\frac{{2 \cdot N}^{- J}}{2}) (m + 1) \leftrightarrow 0 < (\frac{{2 \cdot N}^{- J}}{2}) (m + 1) - (\frac{{2 \cdot N}^{- J}}{2}) m)$
55	53 54	mpbird	$⊢ (φ \land m \in ℤ) \to (\frac{{2 \cdot N}^{- J}}{2}) m < (\frac{{2 \cdot N}^{- J}}{2}) (m + 1)$
56	33 55	ltned	$⊢ (φ \land m \in ℤ) \to (\frac{{2 \cdot N}^{- J}}{2}) m \neq (\frac{{2 \cdot N}^{- J}}{2}) (m + 1)$
57	46 56	jca	$⊢ (φ \land m \in ℤ) \to ((\frac{{2 \cdot N}^{- J}}{2}) (m + 1) - (\frac{{2 \cdot N}^{- J}}{2}) m < D \land (\frac{{2 \cdot N}^{- J}}{2}) m \neq (\frac{{2 \cdot N}^{- J}}{2}) (m + 1))$
58	57	adantrr	$⊢ (φ \land (m \in ℤ \land ((\frac{{2 \cdot N}^{- J}}{2}) m \leq H \land H \leq (\frac{{2 \cdot N}^{- J}}{2}) (m + 1)))) \to ((\frac{{2 \cdot N}^{- J}}{2}) (m + 1) - (\frac{{2 \cdot N}^{- J}}{2}) m < D \land (\frac{{2 \cdot N}^{- J}}{2}) m \neq (\frac{{2 \cdot N}^{- J}}{2}) (m + 1))$
59	7	rpred	$⊢ φ \to E \in ℝ$
60	59	adantr	$⊢ (φ \land m \in ℤ) \to E \in ℝ$
61	5	knoppndvlem3	$⊢ φ \to (C \in ℝ \land \|C\| < 1)$
62	61	simpld	$⊢ φ \to C \in ℝ$
63	62	recnd	$⊢ φ \to C \in ℂ$
64	63	abscld	$⊢ φ \to \|C\| \in ℝ$
65	20 64	remulcld	$⊢ φ \to 2 \cdot N \|C\| \in ℝ$
66	65 9	reexpcld	$⊢ φ \to {2 \cdot N \|C\|}^{J} \in ℝ$
67	4	a1i	$⊢ φ \to G = 1 - (\frac{1}{2 \cdot N \|C\| - 1})$
68	5 10 11	knoppndvlem20	$⊢ φ \to 1 - (\frac{1}{2 \cdot N \|C\| - 1}) \in ℝ^{+}$
69	68	rpred	$⊢ φ \to 1 - (\frac{1}{2 \cdot N \|C\| - 1}) \in ℝ$
70	67 69	eqeltrd	$⊢ φ \to G \in ℝ$
71	66 70	remulcld	$⊢ φ \to {2 \cdot N \|C\|}^{J} G \in ℝ$
72	71	adantr	$⊢ (φ \land m \in ℤ) \to {2 \cdot N \|C\|}^{J} G \in ℝ$
73	62	adantr	$⊢ (φ \land m \in ℤ) \to C \in ℝ$
74	61	simprd	$⊢ φ \to \|C\| < 1$
75	74	adantr	$⊢ (φ \land m \in ℤ) \to \|C\| < 1$
76	1 2 3 39 43 73 75	knoppcld	$⊢ (φ \land m \in ℤ) \to W ((\frac{{2 \cdot N}^{- J}}{2}) (m + 1)) \in ℂ$
77	1 2 3 33 43 73 75	knoppcld	$⊢ (φ \land m \in ℤ) \to W ((\frac{{2 \cdot N}^{- J}}{2}) m) \in ℂ$
78	76 77	subcld	$⊢ (φ \land m \in ℤ) \to W ((\frac{{2 \cdot N}^{- J}}{2}) (m + 1)) - W ((\frac{{2 \cdot N}^{- J}}{2}) m) \in ℂ$
79	78	abscld	$⊢ (φ \land m \in ℤ) \to \|W ((\frac{{2 \cdot N}^{- J}}{2}) (m + 1)) - W ((\frac{{2 \cdot N}^{- J}}{2}) m)\| \in ℝ$
80	44 30	eqeltrd	$⊢ (φ \land m \in ℤ) \to (\frac{{2 \cdot N}^{- J}}{2}) (m + 1) - (\frac{{2 \cdot N}^{- J}}{2}) m \in ℝ$
81	53	gt0ne0d	$⊢ (φ \land m \in ℤ) \to (\frac{{2 \cdot N}^{- J}}{2}) (m + 1) - (\frac{{2 \cdot N}^{- J}}{2}) m \neq 0$
82	79 80 81	redivcld	$⊢ (φ \land m \in ℤ) \to \frac{\|W ((\frac{{2 \cdot N}^{- J}}{2}) (m + 1)) - W ((\frac{{2 \cdot N}^{- J}}{2}) m)\|}{(\frac{{2 \cdot N}^{- J}}{2}) (m + 1) - (\frac{{2 \cdot N}^{- J}}{2}) m} \in ℝ$
83	13	adantr	$⊢ (φ \land m \in ℤ) \to E \leq {2 \cdot N \|C\|}^{J} G$
84	4	oveq2i	$⊢ {2 \cdot N \|C\|}^{J} G = {2 \cdot N \|C\|}^{J} (1 - (\frac{1}{2 \cdot N \|C\| - 1}))$
85	84	a1i	$⊢ (φ \land m \in ℤ) \to {2 \cdot N \|C\|}^{J} G = {2 \cdot N \|C\|}^{J} (1 - (\frac{1}{2 \cdot N \|C\| - 1}))$
86	5	adantr	$⊢ (φ \land m \in ℤ) \to C \in (- 1, 1)$
87	11	adantr	$⊢ (φ \land m \in ℤ) \to 1 < N \|C\|$
88	1 2 3 14 15 86 42 31 43 87	knoppndvlem17	$⊢ (φ \land m \in ℤ) \to {2 \cdot N \|C\|}^{J} (1 - (\frac{1}{2 \cdot N \|C\| - 1})) \leq \frac{\|W ((\frac{{2 \cdot N}^{- J}}{2}) (m + 1)) - W ((\frac{{2 \cdot N}^{- J}}{2}) m)\|}{(\frac{{2 \cdot N}^{- J}}{2}) (m + 1) - (\frac{{2 \cdot N}^{- J}}{2}) m}$
89	85 88	eqbrtrd	$⊢ (φ \land m \in ℤ) \to {2 \cdot N \|C\|}^{J} G \leq \frac{\|W ((\frac{{2 \cdot N}^{- J}}{2}) (m + 1)) - W ((\frac{{2 \cdot N}^{- J}}{2}) m)\|}{(\frac{{2 \cdot N}^{- J}}{2}) (m + 1) - (\frac{{2 \cdot N}^{- J}}{2}) m}$
90	60 72 82 83 89	letrd	$⊢ (φ \land m \in ℤ) \to E \leq \frac{\|W ((\frac{{2 \cdot N}^{- J}}{2}) (m + 1)) - W ((\frac{{2 \cdot N}^{- J}}{2}) m)\|}{(\frac{{2 \cdot N}^{- J}}{2}) (m + 1) - (\frac{{2 \cdot N}^{- J}}{2}) m}$
91	90	adantrr	$⊢ (φ \land (m \in ℤ \land ((\frac{{2 \cdot N}^{- J}}{2}) m \leq H \land H \leq (\frac{{2 \cdot N}^{- J}}{2}) (m + 1)))) \to E \leq \frac{\|W ((\frac{{2 \cdot N}^{- J}}{2}) (m + 1)) - W ((\frac{{2 \cdot N}^{- J}}{2}) m)\|}{(\frac{{2 \cdot N}^{- J}}{2}) (m + 1) - (\frac{{2 \cdot N}^{- J}}{2}) m}$
92	41 58 91	3jca	$⊢ (φ \land (m \in ℤ \land ((\frac{{2 \cdot N}^{- J}}{2}) m \leq H \land H \leq (\frac{{2 \cdot N}^{- J}}{2}) (m + 1)))) \to (((\frac{{2 \cdot N}^{- J}}{2}) m \leq H \land H \leq (\frac{{2 \cdot N}^{- J}}{2}) (m + 1)) \land ((\frac{{2 \cdot N}^{- J}}{2}) (m + 1) - (\frac{{2 \cdot N}^{- J}}{2}) m < D \land (\frac{{2 \cdot N}^{- J}}{2}) m \neq (\frac{{2 \cdot N}^{- J}}{2}) (m + 1)) \land E \leq \frac{\|W ((\frac{{2 \cdot N}^{- J}}{2}) (m + 1)) - W ((\frac{{2 \cdot N}^{- J}}{2}) m)\|}{(\frac{{2 \cdot N}^{- J}}{2}) (m + 1) - (\frac{{2 \cdot N}^{- J}}{2}) m})$
93	34 40 92	3jca	$⊢ (φ \land (m \in ℤ \land ((\frac{{2 \cdot N}^{- J}}{2}) m \leq H \land H \leq (\frac{{2 \cdot N}^{- J}}{2}) (m + 1)))) \to ((\frac{{2 \cdot N}^{- J}}{2}) m \in ℝ \land (\frac{{2 \cdot N}^{- J}}{2}) (m + 1) \in ℝ \land (((\frac{{2 \cdot N}^{- J}}{2}) m \leq H \land H \leq (\frac{{2 \cdot N}^{- J}}{2}) (m + 1)) \land ((\frac{{2 \cdot N}^{- J}}{2}) (m + 1) - (\frac{{2 \cdot N}^{- J}}{2}) m < D \land (\frac{{2 \cdot N}^{- J}}{2}) m \neq (\frac{{2 \cdot N}^{- J}}{2}) (m + 1)) \land E \leq \frac{\|W ((\frac{{2 \cdot N}^{- J}}{2}) (m + 1)) - W ((\frac{{2 \cdot N}^{- J}}{2}) m)\|}{(\frac{{2 \cdot N}^{- J}}{2}) (m + 1) - (\frac{{2 \cdot N}^{- J}}{2}) m}))$
94		breq1	$⊢ a = (\frac{{2 \cdot N}^{- J}}{2}) m \to (a \leq H \leftrightarrow (\frac{{2 \cdot N}^{- J}}{2}) m \leq H)$
95	94	anbi1d	$⊢ a = (\frac{{2 \cdot N}^{- J}}{2}) m \to ((a \leq H \land H \leq b) \leftrightarrow ((\frac{{2 \cdot N}^{- J}}{2}) m \leq H \land H \leq b))$
96		oveq2	$⊢ a = (\frac{{2 \cdot N}^{- J}}{2}) m \to b - a = b - (\frac{{2 \cdot N}^{- J}}{2}) m$
97	96	breq1d	$⊢ a = (\frac{{2 \cdot N}^{- J}}{2}) m \to (b - a < D \leftrightarrow b - (\frac{{2 \cdot N}^{- J}}{2}) m < D)$
98		neeq1	$⊢ a = (\frac{{2 \cdot N}^{- J}}{2}) m \to (a \neq b \leftrightarrow (\frac{{2 \cdot N}^{- J}}{2}) m \neq b)$
99	97 98	anbi12d	$⊢ a = (\frac{{2 \cdot N}^{- J}}{2}) m \to ((b - a < D \land a \neq b) \leftrightarrow (b - (\frac{{2 \cdot N}^{- J}}{2}) m < D \land (\frac{{2 \cdot N}^{- J}}{2}) m \neq b))$
100		fveq2	$⊢ a = (\frac{{2 \cdot N}^{- J}}{2}) m \to W (a) = W ((\frac{{2 \cdot N}^{- J}}{2}) m)$
101	100	oveq2d	$⊢ a = (\frac{{2 \cdot N}^{- J}}{2}) m \to W (b) - W (a) = W (b) - W ((\frac{{2 \cdot N}^{- J}}{2}) m)$
102	101	fveq2d	$⊢ a = (\frac{{2 \cdot N}^{- J}}{2}) m \to \|W (b) - W (a)\| = \|W (b) - W ((\frac{{2 \cdot N}^{- J}}{2}) m)\|$
103	102 96	oveq12d	$⊢ a = (\frac{{2 \cdot N}^{- J}}{2}) m \to \frac{\|W (b) - W (a)\|}{b - a} = \frac{\|W (b) - W ((\frac{{2 \cdot N}^{- J}}{2}) m)\|}{b - (\frac{{2 \cdot N}^{- J}}{2}) m}$
104	103	breq2d	$⊢ a = (\frac{{2 \cdot N}^{- J}}{2}) m \to (E \leq \frac{\|W (b) - W (a)\|}{b - a} \leftrightarrow E \leq \frac{\|W (b) - W ((\frac{{2 \cdot N}^{- J}}{2}) m)\|}{b - (\frac{{2 \cdot N}^{- J}}{2}) m})$
105	95 99 104	3anbi123d	$⊢ a = (\frac{{2 \cdot N}^{- J}}{2}) m \to (((a \leq H \land H \leq b) \land (b - a < D \land a \neq b) \land E \leq \frac{\|W (b) - W (a)\|}{b - a}) \leftrightarrow (((\frac{{2 \cdot N}^{- J}}{2}) m \leq H \land H \leq b) \land (b - (\frac{{2 \cdot N}^{- J}}{2}) m < D \land (\frac{{2 \cdot N}^{- J}}{2}) m \neq b) \land E \leq \frac{\|W (b) - W ((\frac{{2 \cdot N}^{- J}}{2}) m)\|}{b - (\frac{{2 \cdot N}^{- J}}{2}) m}))$
106		breq2	$⊢ b = (\frac{{2 \cdot N}^{- J}}{2}) (m + 1) \to (H \leq b \leftrightarrow H \leq (\frac{{2 \cdot N}^{- J}}{2}) (m + 1))$
107	106	anbi2d	$⊢ b = (\frac{{2 \cdot N}^{- J}}{2}) (m + 1) \to (((\frac{{2 \cdot N}^{- J}}{2}) m \leq H \land H \leq b) \leftrightarrow ((\frac{{2 \cdot N}^{- J}}{2}) m \leq H \land H \leq (\frac{{2 \cdot N}^{- J}}{2}) (m + 1)))$
108		oveq1	$⊢ b = (\frac{{2 \cdot N}^{- J}}{2}) (m + 1) \to b - (\frac{{2 \cdot N}^{- J}}{2}) m = (\frac{{2 \cdot N}^{- J}}{2}) (m + 1) - (\frac{{2 \cdot N}^{- J}}{2}) m$
109	108	breq1d	$⊢ b = (\frac{{2 \cdot N}^{- J}}{2}) (m + 1) \to (b - (\frac{{2 \cdot N}^{- J}}{2}) m < D \leftrightarrow (\frac{{2 \cdot N}^{- J}}{2}) (m + 1) - (\frac{{2 \cdot N}^{- J}}{2}) m < D)$
110		neeq2	$⊢ b = (\frac{{2 \cdot N}^{- J}}{2}) (m + 1) \to ((\frac{{2 \cdot N}^{- J}}{2}) m \neq b \leftrightarrow (\frac{{2 \cdot N}^{- J}}{2}) m \neq (\frac{{2 \cdot N}^{- J}}{2}) (m + 1))$
111	109 110	anbi12d	$⊢ b = (\frac{{2 \cdot N}^{- J}}{2}) (m + 1) \to ((b - (\frac{{2 \cdot N}^{- J}}{2}) m < D \land (\frac{{2 \cdot N}^{- J}}{2}) m \neq b) \leftrightarrow ((\frac{{2 \cdot N}^{- J}}{2}) (m + 1) - (\frac{{2 \cdot N}^{- J}}{2}) m < D \land (\frac{{2 \cdot N}^{- J}}{2}) m \neq (\frac{{2 \cdot N}^{- J}}{2}) (m + 1)))$
112		fveq2	$⊢ b = (\frac{{2 \cdot N}^{- J}}{2}) (m + 1) \to W (b) = W ((\frac{{2 \cdot N}^{- J}}{2}) (m + 1))$
113	112	fvoveq1d	$⊢ b = (\frac{{2 \cdot N}^{- J}}{2}) (m + 1) \to \|W (b) - W ((\frac{{2 \cdot N}^{- J}}{2}) m)\| = \|W ((\frac{{2 \cdot N}^{- J}}{2}) (m + 1)) - W ((\frac{{2 \cdot N}^{- J}}{2}) m)\|$
114	113 108	oveq12d	$⊢ b = (\frac{{2 \cdot N}^{- J}}{2}) (m + 1) \to \frac{\|W (b) - W ((\frac{{2 \cdot N}^{- J}}{2}) m)\|}{b - (\frac{{2 \cdot N}^{- J}}{2}) m} = \frac{\|W ((\frac{{2 \cdot N}^{- J}}{2}) (m + 1)) - W ((\frac{{2 \cdot N}^{- J}}{2}) m)\|}{(\frac{{2 \cdot N}^{- J}}{2}) (m + 1) - (\frac{{2 \cdot N}^{- J}}{2}) m}$
115	114	breq2d	$⊢ b = (\frac{{2 \cdot N}^{- J}}{2}) (m + 1) \to (E \leq \frac{\|W (b) - W ((\frac{{2 \cdot N}^{- J}}{2}) m)\|}{b - (\frac{{2 \cdot N}^{- J}}{2}) m} \leftrightarrow E \leq \frac{\|W ((\frac{{2 \cdot N}^{- J}}{2}) (m + 1)) - W ((\frac{{2 \cdot N}^{- J}}{2}) m)\|}{(\frac{{2 \cdot N}^{- J}}{2}) (m + 1) - (\frac{{2 \cdot N}^{- J}}{2}) m})$
116	107 111 115	3anbi123d	$⊢ b = (\frac{{2 \cdot N}^{- J}}{2}) (m + 1) \to ((((\frac{{2 \cdot N}^{- J}}{2}) m \leq H \land H \leq b) \land (b - (\frac{{2 \cdot N}^{- J}}{2}) m < D \land (\frac{{2 \cdot N}^{- J}}{2}) m \neq b) \land E \leq \frac{\|W (b) - W ((\frac{{2 \cdot N}^{- J}}{2}) m)\|}{b - (\frac{{2 \cdot N}^{- J}}{2}) m}) \leftrightarrow (((\frac{{2 \cdot N}^{- J}}{2}) m \leq H \land H \leq (\frac{{2 \cdot N}^{- J}}{2}) (m + 1)) \land ((\frac{{2 \cdot N}^{- J}}{2}) (m + 1) - (\frac{{2 \cdot N}^{- J}}{2}) m < D \land (\frac{{2 \cdot N}^{- J}}{2}) m \neq (\frac{{2 \cdot N}^{- J}}{2}) (m + 1)) \land E \leq \frac{\|W ((\frac{{2 \cdot N}^{- J}}{2}) (m + 1)) - W ((\frac{{2 \cdot N}^{- J}}{2}) m)\|}{(\frac{{2 \cdot N}^{- J}}{2}) (m + 1) - (\frac{{2 \cdot N}^{- J}}{2}) m}))$
117	105 116	rspc2ev	$⊢ ((\frac{{2 \cdot N}^{- J}}{2}) m \in ℝ \land (\frac{{2 \cdot N}^{- J}}{2}) (m + 1) \in ℝ \land (((\frac{{2 \cdot N}^{- J}}{2}) m \leq H \land H \leq (\frac{{2 \cdot N}^{- J}}{2}) (m + 1)) \land ((\frac{{2 \cdot N}^{- J}}{2}) (m + 1) - (\frac{{2 \cdot N}^{- J}}{2}) m < D \land (\frac{{2 \cdot N}^{- J}}{2}) m \neq (\frac{{2 \cdot N}^{- J}}{2}) (m + 1)) \land E \leq \frac{\|W ((\frac{{2 \cdot N}^{- J}}{2}) (m + 1)) - W ((\frac{{2 \cdot N}^{- J}}{2}) m)\|}{(\frac{{2 \cdot N}^{- J}}{2}) (m + 1) - (\frac{{2 \cdot N}^{- J}}{2}) m})) \to \exists a \in ℝ \exists b \in ℝ ((a \leq H \land H \leq b) \land (b - a < D \land a \neq b) \land E \leq \frac{\|W (b) - W (a)\|}{b - a})$
118	93 117	syl	$⊢ (φ \land (m \in ℤ \land ((\frac{{2 \cdot N}^{- J}}{2}) m \leq H \land H \leq (\frac{{2 \cdot N}^{- J}}{2}) (m + 1)))) \to \exists a \in ℝ \exists b \in ℝ ((a \leq H \land H \leq b) \land (b - a < D \land a \neq b) \land E \leq \frac{\|W (b) - W (a)\|}{b - a})$
119	16 118	rexlimddv	$⊢ φ \to \exists a \in ℝ \exists b \in ℝ ((a \leq H \land H \leq b) \land (b - a < D \land a \neq b) \land E \leq \frac{\|W (b) - W (a)\|}{b - a})$

Metamath Proof Explorer

Theorem knoppndvlem21

Proof