stoweidlem42

Description: This lemma is used to prove that x built as in Lemma 2 of BrosowskiDeutsh p. 91, is such that x > 1 - ε on B. Here X is used to represent x in the paper, and E is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem42.1	$⊢ Ⅎ i φ$
	stoweidlem42.2	$⊢ Ⅎ t φ$
	stoweidlem42.3	$⊢ \underline{Ⅎ} t Y$
	stoweidlem42.4	$⊢ P = (f \in Y, g \in Y ⟼ (t \in T ⟼ f (t) g (t)))$
	stoweidlem42.5	$⊢ X = seq 1 (P, U) (M)$
	stoweidlem42.6	$⊢ F = (t \in T ⟼ (i \in (1 \dots M) ⟼ U (i) (t)))$
	stoweidlem42.7	$⊢ Z = (t \in T ⟼ seq 1 (\times F (t)) (M))$
	stoweidlem42.8	$⊢ φ \to M \in ℕ$
	stoweidlem42.9	$⊢ φ \to U : (1 \dots M) ⟶ Y$
	stoweidlem42.10	$⊢ (φ \land i \in (1 \dots M)) \to \forall t \in B 1 - (\frac{E}{M}) < U (i) (t)$
	stoweidlem42.11	$⊢ φ \to E \in ℝ^{+}$
	stoweidlem42.12	$⊢ φ \to E < \frac{1}{3}$
	stoweidlem42.13	$⊢ (φ \land f \in Y) \to f : T ⟶ ℝ$
	stoweidlem42.14	$⊢ (φ \land f \in Y \land g \in Y) \to (t \in T ⟼ f (t) g (t)) \in Y$
	stoweidlem42.15	$⊢ φ \to T \in V$
	stoweidlem42.16	$⊢ φ \to B \subseteq T$
Assertion	stoweidlem42	$⊢ φ \to \forall t \in B 1 - E < X (t)$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem42.1	$⊢ Ⅎ i φ$
2		stoweidlem42.2	$⊢ Ⅎ t φ$
3		stoweidlem42.3	$⊢ \underline{Ⅎ} t Y$
4		stoweidlem42.4	$⊢ P = (f \in Y, g \in Y ⟼ (t \in T ⟼ f (t) g (t)))$
5		stoweidlem42.5	$⊢ X = seq 1 (P, U) (M)$
6		stoweidlem42.6	$⊢ F = (t \in T ⟼ (i \in (1 \dots M) ⟼ U (i) (t)))$
7		stoweidlem42.7	$⊢ Z = (t \in T ⟼ seq 1 (\times F (t)) (M))$
8		stoweidlem42.8	$⊢ φ \to M \in ℕ$
9		stoweidlem42.9	$⊢ φ \to U : (1 \dots M) ⟶ Y$
10		stoweidlem42.10	$⊢ (φ \land i \in (1 \dots M)) \to \forall t \in B 1 - (\frac{E}{M}) < U (i) (t)$
11		stoweidlem42.11	$⊢ φ \to E \in ℝ^{+}$
12		stoweidlem42.12	$⊢ φ \to E < \frac{1}{3}$
13		stoweidlem42.13	$⊢ (φ \land f \in Y) \to f : T ⟶ ℝ$
14		stoweidlem42.14	$⊢ (φ \land f \in Y \land g \in Y) \to (t \in T ⟼ f (t) g (t)) \in Y$
15		stoweidlem42.15	$⊢ φ \to T \in V$
16		stoweidlem42.16	$⊢ φ \to B \subseteq T$
17		1red	$⊢ φ \to 1 \in ℝ$
18	11	rpred	$⊢ φ \to E \in ℝ$
19	17 18	resubcld	$⊢ φ \to 1 - E \in ℝ$
20	19	adantr	$⊢ (φ \land t \in B) \to 1 - E \in ℝ$
21	18 8	nndivred	$⊢ φ \to \frac{E}{M} \in ℝ$
22	17 21	resubcld	$⊢ φ \to 1 - (\frac{E}{M}) \in ℝ$
23	22	adantr	$⊢ (φ \land t \in B) \to 1 - (\frac{E}{M}) \in ℝ$
24	8	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
25	24	adantr	$⊢ (φ \land t \in B) \to M \in ℕ_{0}$
26	23 25	reexpcld	$⊢ (φ \land t \in B) \to {(1 - (\frac{E}{M}))}^{M} \in ℝ$
27		elnnuz	$⊢ M \in ℕ \leftrightarrow M \in ℤ_{\geq 1}$
28	8 27	sylib	$⊢ φ \to M \in ℤ_{\geq 1}$
29	28	adantr	$⊢ (φ \land t \in B) \to M \in ℤ_{\geq 1}$
30		nfv	$⊢ Ⅎ i t \in B$
31	1 30	nfan	$⊢ Ⅎ i (φ \land t \in B)$
32		nfv	$⊢ Ⅎ i a \in (1 \dots M)$
33	31 32	nfan	$⊢ Ⅎ i ((φ \land t \in B) \land a \in (1 \dots M))$
34		nfcv	$⊢ \underline{Ⅎ} i T$
35		nfmpt1	$⊢ \underline{Ⅎ} i (i \in (1 \dots M) ⟼ U (i) (t))$
36	34 35	nfmpt	$⊢ \underline{Ⅎ} i (t \in T ⟼ (i \in (1 \dots M) ⟼ U (i) (t)))$
37	6 36	nfcxfr	$⊢ \underline{Ⅎ} i F$
38		nfcv	$⊢ \underline{Ⅎ} i t$
39	37 38	nffv	$⊢ \underline{Ⅎ} i F (t)$
40		nfcv	$⊢ \underline{Ⅎ} i a$
41	39 40	nffv	$⊢ \underline{Ⅎ} i F (t) (a)$
42	41	nfel1	$⊢ Ⅎ i F (t) (a) \in ℝ$
43	33 42	nfim	$⊢ Ⅎ i (((φ \land t \in B) \land a \in (1 \dots M)) \to F (t) (a) \in ℝ)$
44		eleq1	$⊢ i = a \to (i \in (1 \dots M) \leftrightarrow a \in (1 \dots M))$
45	44	anbi2d	$⊢ i = a \to (((φ \land t \in B) \land i \in (1 \dots M)) \leftrightarrow ((φ \land t \in B) \land a \in (1 \dots M)))$
46		fveq2	$⊢ i = a \to F (t) (i) = F (t) (a)$
47	46	eleq1d	$⊢ i = a \to (F (t) (i) \in ℝ \leftrightarrow F (t) (a) \in ℝ)$
48	45 47	imbi12d	$⊢ i = a \to ((((φ \land t \in B) \land i \in (1 \dots M)) \to F (t) (i) \in ℝ) \leftrightarrow (((φ \land t \in B) \land a \in (1 \dots M)) \to F (t) (a) \in ℝ))$
49	16	sselda	$⊢ (φ \land t \in B) \to t \in T$
50		ovex	$⊢ (1 \dots M) \in V$
51		mptexg	$⊢ (1 \dots M) \in V \to (i \in (1 \dots M) ⟼ U (i) (t)) \in V$
52	50 51	mp1i	$⊢ (φ \land t \in B) \to (i \in (1 \dots M) ⟼ U (i) (t)) \in V$
53	6	fvmpt2	$⊢ (t \in T \land (i \in (1 \dots M) ⟼ U (i) (t)) \in V) \to F (t) = (i \in (1 \dots M) ⟼ U (i) (t))$
54	49 52 53	syl2anc	$⊢ (φ \land t \in B) \to F (t) = (i \in (1 \dots M) ⟼ U (i) (t))$
55	9	ffvelcdmda	$⊢ (φ \land i \in (1 \dots M)) \to U (i) \in Y$
56		simpl	$⊢ (φ \land i \in (1 \dots M)) \to φ$
57	56 55	jca	$⊢ (φ \land i \in (1 \dots M)) \to (φ \land U (i) \in Y)$
58		eleq1	$⊢ f = U (i) \to (f \in Y \leftrightarrow U (i) \in Y)$
59	58	anbi2d	$⊢ f = U (i) \to ((φ \land f \in Y) \leftrightarrow (φ \land U (i) \in Y))$
60		feq1	$⊢ f = U (i) \to (f : T ⟶ ℝ \leftrightarrow U (i) : T ⟶ ℝ)$
61	59 60	imbi12d	$⊢ f = U (i) \to (((φ \land f \in Y) \to f : T ⟶ ℝ) \leftrightarrow ((φ \land U (i) \in Y) \to U (i) : T ⟶ ℝ))$
62	61 13	vtoclg	$⊢ U (i) \in Y \to ((φ \land U (i) \in Y) \to U (i) : T ⟶ ℝ)$
63	55 57 62	sylc	$⊢ (φ \land i \in (1 \dots M)) \to U (i) : T ⟶ ℝ$
64	63	adantlr	$⊢ ((φ \land t \in B) \land i \in (1 \dots M)) \to U (i) : T ⟶ ℝ$
65	49	adantr	$⊢ ((φ \land t \in B) \land i \in (1 \dots M)) \to t \in T$
66	64 65	ffvelcdmd	$⊢ ((φ \land t \in B) \land i \in (1 \dots M)) \to U (i) (t) \in ℝ$
67	54 66	fvmpt2d	$⊢ ((φ \land t \in B) \land i \in (1 \dots M)) \to F (t) (i) = U (i) (t)$
68	67 66	eqeltrd	$⊢ ((φ \land t \in B) \land i \in (1 \dots M)) \to F (t) (i) \in ℝ$
69	43 48 68	chvarfv	$⊢ ((φ \land t \in B) \land a \in (1 \dots M)) \to F (t) (a) \in ℝ$
70		remulcl	$⊢ (a \in ℝ \land j \in ℝ) \to a j \in ℝ$
71	70	adantl	$⊢ ((φ \land t \in B) \land (a \in ℝ \land j \in ℝ)) \to a j \in ℝ$
72	29 69 71	seqcl	$⊢ (φ \land t \in B) \to seq 1 (\times F (t)) (M) \in ℝ$
73	11	rpcnd	$⊢ φ \to E \in ℂ$
74	8	nncnd	$⊢ φ \to M \in ℂ$
75	8	nnne0d	$⊢ φ \to M \neq 0$
76	73 74 75	divcan1d	$⊢ φ \to (\frac{E}{M}) \cdot M = E$
77	76	eqcomd	$⊢ φ \to E = (\frac{E}{M}) \cdot M$
78	77	oveq2d	$⊢ φ \to 1 - E = 1 - (\frac{E}{M}) \cdot M$
79		1cnd	$⊢ φ \to 1 \in ℂ$
80	73 74 75	divcld	$⊢ φ \to \frac{E}{M} \in ℂ$
81	80 74	mulcld	$⊢ φ \to (\frac{E}{M}) \cdot M \in ℂ$
82	79 81	negsubd	$⊢ φ \to 1 + (- (\frac{E}{M}) \cdot M) = 1 - (\frac{E}{M}) \cdot M$
83	80 74	mulneg1d	$⊢ φ \to (- \frac{E}{M}) \cdot M = - (\frac{E}{M}) \cdot M$
84	83	eqcomd	$⊢ φ \to - (\frac{E}{M}) \cdot M = (- \frac{E}{M}) \cdot M$
85	84	oveq2d	$⊢ φ \to 1 + (- (\frac{E}{M}) \cdot M) = 1 + (- \frac{E}{M}) \cdot M$
86	78 82 85	3eqtr2d	$⊢ φ \to 1 - E = 1 + (- \frac{E}{M}) \cdot M$
87	21	renegcld	$⊢ φ \to - \frac{E}{M} \in ℝ$
88	8	nnred	$⊢ φ \to M \in ℝ$
89		3re	$⊢ 3 \in ℝ$
90	89	a1i	$⊢ φ \to 3 \in ℝ$
91		3ne0	$⊢ 3 \neq 0$
92	91	a1i	$⊢ φ \to 3 \neq 0$
93	90 92	rereccld	$⊢ φ \to \frac{1}{3} \in ℝ$
94		1lt3	$⊢ 1 < 3$
95	94	a1i	$⊢ φ \to 1 < 3$
96		0lt1	$⊢ 0 < 1$
97	96	a1i	$⊢ φ \to 0 < 1$
98		3pos	$⊢ 0 < 3$
99	98	a1i	$⊢ φ \to 0 < 3$
100		ltdiv2	$⊢ ((1 \in ℝ \land 0 < 1) \land (3 \in ℝ \land 0 < 3) \land (1 \in ℝ \land 0 < 1)) \to (1 < 3 \leftrightarrow \frac{1}{3} < \frac{1}{1})$
101	17 97 90 99 17 97 100	syl222anc	$⊢ φ \to (1 < 3 \leftrightarrow \frac{1}{3} < \frac{1}{1})$
102	95 101	mpbid	$⊢ φ \to \frac{1}{3} < \frac{1}{1}$
103		1div1e1	$⊢ \frac{1}{1} = 1$
104	102 103	breqtrdi	$⊢ φ \to \frac{1}{3} < 1$
105	18 93 17 12 104	lttrd	$⊢ φ \to E < 1$
106	8	nnge1d	$⊢ φ \to 1 \leq M$
107	18 17 88 105 106	ltletrd	$⊢ φ \to E < M$
108	18 88 107	ltled	$⊢ φ \to E \leq M$
109	11	rpregt0d	$⊢ φ \to (E \in ℝ \land 0 < E)$
110	8	nngt0d	$⊢ φ \to 0 < M$
111		lediv2	$⊢ ((E \in ℝ \land 0 < E) \land (M \in ℝ \land 0 < M) \land (E \in ℝ \land 0 < E)) \to (E \leq M \leftrightarrow \frac{E}{M} \leq \frac{E}{E})$
112	109 88 110 109 111	syl121anc	$⊢ φ \to (E \leq M \leftrightarrow \frac{E}{M} \leq \frac{E}{E})$
113	108 112	mpbid	$⊢ φ \to \frac{E}{M} \leq \frac{E}{E}$
114	11	rpcnne0d	$⊢ φ \to (E \in ℂ \land E \neq 0)$
115		divid	$⊢ (E \in ℂ \land E \neq 0) \to \frac{E}{E} = 1$
116	114 115	syl	$⊢ φ \to \frac{E}{E} = 1$
117	113 116	breqtrd	$⊢ φ \to \frac{E}{M} \leq 1$
118	21 17	lenegd	$⊢ φ \to (\frac{E}{M} \leq 1 \leftrightarrow - 1 \leq - \frac{E}{M})$
119	117 118	mpbid	$⊢ φ \to - 1 \leq - \frac{E}{M}$
120		bernneq	$⊢ (- \frac{E}{M} \in ℝ \land M \in ℕ_{0} \land - 1 \leq - \frac{E}{M}) \to 1 + (- \frac{E}{M}) \cdot M \leq {(1 + (- \frac{E}{M}))}^{M}$
121	87 24 119 120	syl3anc	$⊢ φ \to 1 + (- \frac{E}{M}) \cdot M \leq {(1 + (- \frac{E}{M}))}^{M}$
122	79 80	negsubd	$⊢ φ \to 1 + (- \frac{E}{M}) = 1 - (\frac{E}{M})$
123	122	oveq1d	$⊢ φ \to {(1 + (- \frac{E}{M}))}^{M} = {(1 - (\frac{E}{M}))}^{M}$
124	121 123	breqtrd	$⊢ φ \to 1 + (- \frac{E}{M}) \cdot M \leq {(1 - (\frac{E}{M}))}^{M}$
125	86 124	eqbrtrd	$⊢ φ \to 1 - E \leq {(1 - (\frac{E}{M}))}^{M}$
126	125	adantr	$⊢ (φ \land t \in B) \to 1 - E \leq {(1 - (\frac{E}{M}))}^{M}$
127		eqid	$⊢ seq 1 (\times F (t)) = seq 1 (\times F (t))$
128	8	adantr	$⊢ (φ \land t \in B) \to M \in ℕ$
129		eqid	$⊢ (i \in (1 \dots M) ⟼ U (i) (t)) = (i \in (1 \dots M) ⟼ U (i) (t))$
130	31 66 129	fmptdf	$⊢ (φ \land t \in B) \to (i \in (1 \dots M) ⟼ U (i) (t)) : (1 \dots M) ⟶ ℝ$
131	54	feq1d	$⊢ (φ \land t \in B) \to (F (t) : (1 \dots M) ⟶ ℝ \leftrightarrow (i \in (1 \dots M) ⟼ U (i) (t)) : (1 \dots M) ⟶ ℝ)$
132	130 131	mpbird	$⊢ (φ \land t \in B) \to F (t) : (1 \dots M) ⟶ ℝ$
133	10	r19.21bi	$⊢ ((φ \land i \in (1 \dots M)) \land t \in B) \to 1 - (\frac{E}{M}) < U (i) (t)$
134	133	an32s	$⊢ ((φ \land t \in B) \land i \in (1 \dots M)) \to 1 - (\frac{E}{M}) < U (i) (t)$
135	134 67	breqtrrd	$⊢ ((φ \land t \in B) \land i \in (1 \dots M)) \to 1 - (\frac{E}{M}) < F (t) (i)$
136	80	addlidd	$⊢ φ \to 0 + (\frac{E}{M}) = \frac{E}{M}$
137		lediv2	$⊢ ((1 \in ℝ \land 0 < 1) \land (M \in ℝ \land 0 < M) \land (E \in ℝ \land 0 < E)) \to (1 \leq M \leftrightarrow \frac{E}{M} \leq \frac{E}{1})$
138	17 97 88 110 109 137	syl221anc	$⊢ φ \to (1 \leq M \leftrightarrow \frac{E}{M} \leq \frac{E}{1})$
139	106 138	mpbid	$⊢ φ \to \frac{E}{M} \leq \frac{E}{1}$
140	73	div1d	$⊢ φ \to \frac{E}{1} = E$
141	139 140	breqtrd	$⊢ φ \to \frac{E}{M} \leq E$
142	21 18 17 141 105	lelttrd	$⊢ φ \to \frac{E}{M} < 1$
143	136 142	eqbrtrd	$⊢ φ \to 0 + (\frac{E}{M}) < 1$
144		0red	$⊢ φ \to 0 \in ℝ$
145	144 21 17	ltaddsubd	$⊢ φ \to (0 + (\frac{E}{M}) < 1 \leftrightarrow 0 < 1 - (\frac{E}{M}))$
146	143 145	mpbid	$⊢ φ \to 0 < 1 - (\frac{E}{M})$
147	22 146	elrpd	$⊢ φ \to 1 - (\frac{E}{M}) \in ℝ^{+}$
148	147	adantr	$⊢ (φ \land t \in B) \to 1 - (\frac{E}{M}) \in ℝ^{+}$
149	39 31 127 128 132 135 148	stoweidlem3	$⊢ (φ \land t \in B) \to {(1 - (\frac{E}{M}))}^{M} < seq 1 (\times F (t)) (M)$
150	20 26 72 126 149	lelttrd	$⊢ (φ \land t \in B) \to 1 - E < seq 1 (\times F (t)) (M)$
151	7	fvmpt2	$⊢ (t \in T \land seq 1 (\times F (t)) (M) \in ℝ) \to Z (t) = seq 1 (\times F (t)) (M)$
152	49 72 151	syl2anc	$⊢ (φ \land t \in B) \to Z (t) = seq 1 (\times F (t)) (M)$
153	150 152	breqtrrd	$⊢ (φ \land t \in B) \to 1 - E < Z (t)$
154		simpl	$⊢ (φ \land t \in B) \to φ$
155	1 3 4 5 6 7 15 8 9 13 14	fmuldfeq	$⊢ (φ \land t \in T) \to X (t) = Z (t)$
156	154 49 155	syl2anc	$⊢ (φ \land t \in B) \to X (t) = Z (t)$
157	153 156	breqtrrd	$⊢ (φ \land t \in B) \to 1 - E < X (t)$
158	157	ex	$⊢ φ \to (t \in B \to 1 - E < X (t))$
159	2 158	ralrimi	$⊢ φ \to \forall t \in B 1 - E < X (t)$

Metamath Proof Explorer

Theorem stoweidlem42

Proof