stoweidlem49

Description: There exists a function q_n as in the proof of Lemma 1 in BrosowskiDeutsh p. 91 (at the top of page 91): 0 <= q_n <= 1 , q_n < ε on T \ U , and q_n > 1 - ε on V . Here y is used to represent the final q_n in the paper (the one with n large enough), N represents n in the paper, K represents k , D represents δ, E represents ε, and P represents p . (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem49.1	$⊢ \underline{Ⅎ} t P$
	stoweidlem49.2	$⊢ Ⅎ t φ$
	stoweidlem49.3	$⊢ V = \{t \in T \| P (t) < \frac{D}{2}\}$
	stoweidlem49.4	$⊢ φ \to D \in ℝ^{+}$
	stoweidlem49.5	$⊢ φ \to D < 1$
	stoweidlem49.6	$⊢ φ \to P \in A$
	stoweidlem49.7	$⊢ φ \to P : T ⟶ ℝ$
	stoweidlem49.8	$⊢ φ \to \forall t \in T (0 \leq P (t) \land P (t) \leq 1)$
	stoweidlem49.9	$⊢ φ \to \forall t \in (T ∖ U) D \leq P (t)$
	stoweidlem49.10	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
	stoweidlem49.11	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
	stoweidlem49.12	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
	stoweidlem49.13	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
	stoweidlem49.14	$⊢ φ \to E \in ℝ^{+}$
Assertion	stoweidlem49	$⊢ φ \to \exists y \in A (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - E < y (t) \land \forall t \in (T ∖ U) y (t) < E)$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem49.1	$⊢ \underline{Ⅎ} t P$
2		stoweidlem49.2	$⊢ Ⅎ t φ$
3		stoweidlem49.3	$⊢ V = \{t \in T \| P (t) < \frac{D}{2}\}$
4		stoweidlem49.4	$⊢ φ \to D \in ℝ^{+}$
5		stoweidlem49.5	$⊢ φ \to D < 1$
6		stoweidlem49.6	$⊢ φ \to P \in A$
7		stoweidlem49.7	$⊢ φ \to P : T ⟶ ℝ$
8		stoweidlem49.8	$⊢ φ \to \forall t \in T (0 \leq P (t) \land P (t) \leq 1)$
9		stoweidlem49.9	$⊢ φ \to \forall t \in (T ∖ U) D \leq P (t)$
10		stoweidlem49.10	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
11		stoweidlem49.11	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
12		stoweidlem49.12	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
13		stoweidlem49.13	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
14		stoweidlem49.14	$⊢ φ \to E \in ℝ^{+}$
15		breq2	$⊢ j = i \to (\frac{1}{D} < j \leftrightarrow \frac{1}{D} < i)$
16	15	cbvrabv	$⊢ \{j \in ℕ \| \frac{1}{D} < j\} = \{i \in ℕ \| \frac{1}{D} < i\}$
17	16 4 5	stoweidlem14	$⊢ φ \to \exists k \in ℕ (1 < k D \land \frac{k D}{2} < 1)$
18		eqid	$⊢ (i \in ℕ_{0} ⟼ {(\frac{1}{k D})}^{i}) = (i \in ℕ_{0} ⟼ {(\frac{1}{k D})}^{i})$
19		eqid	$⊢ (i \in ℕ_{0} ⟼ {(\frac{k D}{2})}^{i}) = (i \in ℕ_{0} ⟼ {(\frac{k D}{2})}^{i})$
20		nnre	$⊢ k \in ℕ \to k \in ℝ$
21	20	adantl	$⊢ (φ \land k \in ℕ) \to k \in ℝ$
22	4	rpred	$⊢ φ \to D \in ℝ$
23	22	adantr	$⊢ (φ \land k \in ℕ) \to D \in ℝ$
24	21 23	remulcld	$⊢ (φ \land k \in ℕ) \to k D \in ℝ$
25	24	adantr	$⊢ ((φ \land k \in ℕ) \land (1 < k D \land \frac{k D}{2} < 1)) \to k D \in ℝ$
26		simprl	$⊢ ((φ \land k \in ℕ) \land (1 < k D \land \frac{k D}{2} < 1)) \to 1 < k D$
27	24	rehalfcld	$⊢ (φ \land k \in ℕ) \to \frac{k D}{2} \in ℝ$
28		nngt0	$⊢ k \in ℕ \to 0 < k$
29	28	adantl	$⊢ (φ \land k \in ℕ) \to 0 < k$
30	4	rpgt0d	$⊢ φ \to 0 < D$
31	30	adantr	$⊢ (φ \land k \in ℕ) \to 0 < D$
32	21 23 29 31	mulgt0d	$⊢ (φ \land k \in ℕ) \to 0 < k D$
33		2re	$⊢ 2 \in ℝ$
34		2pos	$⊢ 0 < 2$
35	33 34	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
36	35	a1i	$⊢ (φ \land k \in ℕ) \to (2 \in ℝ \land 0 < 2)$
37		divgt0	$⊢ ((k D \in ℝ \land 0 < k D) \land (2 \in ℝ \land 0 < 2)) \to 0 < \frac{k D}{2}$
38	24 32 36 37	syl21anc	$⊢ (φ \land k \in ℕ) \to 0 < \frac{k D}{2}$
39	27 38	elrpd	$⊢ (φ \land k \in ℕ) \to \frac{k D}{2} \in ℝ^{+}$
40	39	adantr	$⊢ ((φ \land k \in ℕ) \land (1 < k D \land \frac{k D}{2} < 1)) \to \frac{k D}{2} \in ℝ^{+}$
41		simprr	$⊢ ((φ \land k \in ℕ) \land (1 < k D \land \frac{k D}{2} < 1)) \to \frac{k D}{2} < 1$
42	14	ad2antrr	$⊢ ((φ \land k \in ℕ) \land (1 < k D \land \frac{k D}{2} < 1)) \to E \in ℝ^{+}$
43	18 19 25 26 40 41 42	stoweidlem7	$⊢ ((φ \land k \in ℕ) \land (1 < k D \land \frac{k D}{2} < 1)) \to \exists n \in ℕ (1 - E < 1 - {(\frac{k D}{2})}^{n} \land \frac{1}{{k D}^{n}} < E)$
44	43	ex	$⊢ (φ \land k \in ℕ) \to ((1 < k D \land \frac{k D}{2} < 1) \to \exists n \in ℕ (1 - E < 1 - {(\frac{k D}{2})}^{n} \land \frac{1}{{k D}^{n}} < E))$
45	44	reximdva	$⊢ φ \to (\exists k \in ℕ (1 < k D \land \frac{k D}{2} < 1) \to \exists k \in ℕ \exists n \in ℕ (1 - E < 1 - {(\frac{k D}{2})}^{n} \land \frac{1}{{k D}^{n}} < E))$
46	17 45	mpd	$⊢ φ \to \exists k \in ℕ \exists n \in ℕ (1 - E < 1 - {(\frac{k D}{2})}^{n} \land \frac{1}{{k D}^{n}} < E)$
47		nfv	$⊢ Ⅎ t (k \in ℕ \land n \in ℕ)$
48	2 47	nfan	$⊢ Ⅎ t (φ \land (k \in ℕ \land n \in ℕ))$
49		nfv	$⊢ Ⅎ t (1 - E < 1 - {(\frac{k D}{2})}^{n} \land \frac{1}{{k D}^{n}} < E)$
50	48 49	nfan	$⊢ Ⅎ t ((φ \land (k \in ℕ \land n \in ℕ)) \land (1 - E < 1 - {(\frac{k D}{2})}^{n} \land \frac{1}{{k D}^{n}} < E))$
51		eqid	$⊢ (t \in T ⟼ {(1 - {P (t)}^{n})}^{k^{n}}) = (t \in T ⟼ {(1 - {P (t)}^{n})}^{k^{n}})$
52		simplrr	$⊢ ((φ \land (k \in ℕ \land n \in ℕ)) \land (1 - E < 1 - {(\frac{k D}{2})}^{n} \land \frac{1}{{k D}^{n}} < E)) \to n \in ℕ$
53		simplrl	$⊢ ((φ \land (k \in ℕ \land n \in ℕ)) \land (1 - E < 1 - {(\frac{k D}{2})}^{n} \land \frac{1}{{k D}^{n}} < E)) \to k \in ℕ$
54	4	ad2antrr	$⊢ ((φ \land (k \in ℕ \land n \in ℕ)) \land (1 - E < 1 - {(\frac{k D}{2})}^{n} \land \frac{1}{{k D}^{n}} < E)) \to D \in ℝ^{+}$
55	5	ad2antrr	$⊢ ((φ \land (k \in ℕ \land n \in ℕ)) \land (1 - E < 1 - {(\frac{k D}{2})}^{n} \land \frac{1}{{k D}^{n}} < E)) \to D < 1$
56	6	ad2antrr	$⊢ ((φ \land (k \in ℕ \land n \in ℕ)) \land (1 - E < 1 - {(\frac{k D}{2})}^{n} \land \frac{1}{{k D}^{n}} < E)) \to P \in A$
57	7	ad2antrr	$⊢ ((φ \land (k \in ℕ \land n \in ℕ)) \land (1 - E < 1 - {(\frac{k D}{2})}^{n} \land \frac{1}{{k D}^{n}} < E)) \to P : T ⟶ ℝ$
58	8	ad2antrr	$⊢ ((φ \land (k \in ℕ \land n \in ℕ)) \land (1 - E < 1 - {(\frac{k D}{2})}^{n} \land \frac{1}{{k D}^{n}} < E)) \to \forall t \in T (0 \leq P (t) \land P (t) \leq 1)$
59	9	ad2antrr	$⊢ ((φ \land (k \in ℕ \land n \in ℕ)) \land (1 - E < 1 - {(\frac{k D}{2})}^{n} \land \frac{1}{{k D}^{n}} < E)) \to \forall t \in (T ∖ U) D \leq P (t)$
60	10	ad4ant14	$⊢ (((φ \land (k \in ℕ \land n \in ℕ)) \land (1 - E < 1 - {(\frac{k D}{2})}^{n} \land \frac{1}{{k D}^{n}} < E)) \land f \in A) \to f : T ⟶ ℝ$
61		simp1ll	$⊢ (((φ \land (k \in ℕ \land n \in ℕ)) \land (1 - E < 1 - {(\frac{k D}{2})}^{n} \land \frac{1}{{k D}^{n}} < E)) \land f \in A \land g \in A) \to φ$
62	61 11	syld3an1	$⊢ (((φ \land (k \in ℕ \land n \in ℕ)) \land (1 - E < 1 - {(\frac{k D}{2})}^{n} \land \frac{1}{{k D}^{n}} < E)) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
63	61 12	syld3an1	$⊢ (((φ \land (k \in ℕ \land n \in ℕ)) \land (1 - E < 1 - {(\frac{k D}{2})}^{n} \land \frac{1}{{k D}^{n}} < E)) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
64	13	ad4ant14	$⊢ (((φ \land (k \in ℕ \land n \in ℕ)) \land (1 - E < 1 - {(\frac{k D}{2})}^{n} \land \frac{1}{{k D}^{n}} < E)) \land x \in ℝ) \to (t \in T ⟼ x) \in A$
65	14	ad2antrr	$⊢ ((φ \land (k \in ℕ \land n \in ℕ)) \land (1 - E < 1 - {(\frac{k D}{2})}^{n} \land \frac{1}{{k D}^{n}} < E)) \to E \in ℝ^{+}$
66		simprl	$⊢ ((φ \land (k \in ℕ \land n \in ℕ)) \land (1 - E < 1 - {(\frac{k D}{2})}^{n} \land \frac{1}{{k D}^{n}} < E)) \to 1 - E < 1 - {(\frac{k D}{2})}^{n}$
67		simprr	$⊢ ((φ \land (k \in ℕ \land n \in ℕ)) \land (1 - E < 1 - {(\frac{k D}{2})}^{n} \land \frac{1}{{k D}^{n}} < E)) \to \frac{1}{{k D}^{n}} < E$
68	1 50 3 51 52 53 54 55 56 57 58 59 60 62 63 64 65 66 67	stoweidlem45	$⊢ ((φ \land (k \in ℕ \land n \in ℕ)) \land (1 - E < 1 - {(\frac{k D}{2})}^{n} \land \frac{1}{{k D}^{n}} < E)) \to \exists y \in A (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - E < y (t) \land \forall t \in (T ∖ U) y (t) < E)$
69	68	ex	$⊢ (φ \land (k \in ℕ \land n \in ℕ)) \to ((1 - E < 1 - {(\frac{k D}{2})}^{n} \land \frac{1}{{k D}^{n}} < E) \to \exists y \in A (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - E < y (t) \land \forall t \in (T ∖ U) y (t) < E))$
70	69	rexlimdvva	$⊢ φ \to (\exists k \in ℕ \exists n \in ℕ (1 - E < 1 - {(\frac{k D}{2})}^{n} \land \frac{1}{{k D}^{n}} < E) \to \exists y \in A (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - E < y (t) \land \forall t \in (T ∖ U) y (t) < E))$
71	46 70	mpd	$⊢ φ \to \exists y \in A (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \land \forall t \in V 1 - E < y (t) \land \forall t \in (T ∖ U) y (t) < E)$

Metamath Proof Explorer

Theorem stoweidlem49

Proof