stoweidlem45

Description: This lemma proves that, given an appropriate K (in another theorem we prove such a K exists), 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 . We use y to represent the final q_n in the paper (the one with n large enough), N to represent n in the paper, K to represent k , D to represent δ, E to represent ε, and P to represent p . (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem45.1	$⊢ \underline{Ⅎ} t P$
	stoweidlem45.2	$⊢ Ⅎ t φ$
	stoweidlem45.3	$⊢ V = \{t \in T \| P (t) < \frac{D}{2}\}$
	stoweidlem45.4	$⊢ Q = (t \in T ⟼ {(1 - {P (t)}^{N})}^{K^{N}})$
	stoweidlem45.5	$⊢ φ \to N \in ℕ$
	stoweidlem45.6	$⊢ φ \to K \in ℕ$
	stoweidlem45.7	$⊢ φ \to D \in ℝ^{+}$
	stoweidlem45.8	$⊢ φ \to D < 1$
	stoweidlem45.9	$⊢ φ \to P \in A$
	stoweidlem45.10	$⊢ φ \to P : T ⟶ ℝ$
	stoweidlem45.11	$⊢ φ \to \forall t \in T (0 \leq P (t) \land P (t) \leq 1)$
	stoweidlem45.12	$⊢ φ \to \forall t \in (T ∖ U) D \leq P (t)$
	stoweidlem45.13	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
	stoweidlem45.14	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
	stoweidlem45.15	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
	stoweidlem45.16	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
	stoweidlem45.17	$⊢ φ \to E \in ℝ^{+}$
	stoweidlem45.18	$⊢ φ \to 1 - E < 1 - {(\frac{K D}{2})}^{N}$
	stoweidlem45.19	$⊢ φ \to \frac{1}{{K D}^{N}} < E$
Assertion	stoweidlem45	$⊢ φ \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		stoweidlem45.1	$⊢ \underline{Ⅎ} t P$
2		stoweidlem45.2	$⊢ Ⅎ t φ$
3		stoweidlem45.3	$⊢ V = \{t \in T \| P (t) < \frac{D}{2}\}$
4		stoweidlem45.4	$⊢ Q = (t \in T ⟼ {(1 - {P (t)}^{N})}^{K^{N}})$
5		stoweidlem45.5	$⊢ φ \to N \in ℕ$
6		stoweidlem45.6	$⊢ φ \to K \in ℕ$
7		stoweidlem45.7	$⊢ φ \to D \in ℝ^{+}$
8		stoweidlem45.8	$⊢ φ \to D < 1$
9		stoweidlem45.9	$⊢ φ \to P \in A$
10		stoweidlem45.10	$⊢ φ \to P : T ⟶ ℝ$
11		stoweidlem45.11	$⊢ φ \to \forall t \in T (0 \leq P (t) \land P (t) \leq 1)$
12		stoweidlem45.12	$⊢ φ \to \forall t \in (T ∖ U) D \leq P (t)$
13		stoweidlem45.13	$⊢ (φ \land f \in A) \to f : T ⟶ ℝ$
14		stoweidlem45.14	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
15		stoweidlem45.15	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
16		stoweidlem45.16	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
17		stoweidlem45.17	$⊢ φ \to E \in ℝ^{+}$
18		stoweidlem45.18	$⊢ φ \to 1 - E < 1 - {(\frac{K D}{2})}^{N}$
19		stoweidlem45.19	$⊢ φ \to \frac{1}{{K D}^{N}} < E$
20		eqid	$⊢ (t \in T ⟼ 1 - {P (t)}^{N}) = (t \in T ⟼ 1 - {P (t)}^{N})$
21		eqid	$⊢ (t \in T ⟼ 1) = (t \in T ⟼ 1)$
22		eqid	$⊢ (t \in T ⟼ {P (t)}^{N}) = (t \in T ⟼ {P (t)}^{N})$
23	5	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
24	6 23	nnexpcld	$⊢ φ \to K^{N} \in ℕ$
25	1 2 4 20 21 22 9 10 13 14 15 16 5 24	stoweidlem40	$⊢ φ \to Q \in A$
26		1red	$⊢ (φ \land t \in T) \to 1 \in ℝ$
27	10	ffvelcdmda	$⊢ (φ \land t \in T) \to P (t) \in ℝ$
28	23	adantr	$⊢ (φ \land t \in T) \to N \in ℕ_{0}$
29	27 28	reexpcld	$⊢ (φ \land t \in T) \to {P (t)}^{N} \in ℝ$
30	26 29	resubcld	$⊢ (φ \land t \in T) \to 1 - {P (t)}^{N} \in ℝ$
31	6	nnnn0d	$⊢ φ \to K \in ℕ_{0}$
32	31 23	nn0expcld	$⊢ φ \to K^{N} \in ℕ_{0}$
33	32	adantr	$⊢ (φ \land t \in T) \to K^{N} \in ℕ_{0}$
34		1m1e0	$⊢ 1 - 1 = 0$
35	11	r19.21bi	$⊢ (φ \land t \in T) \to (0 \leq P (t) \land P (t) \leq 1)$
36	35	simpld	$⊢ (φ \land t \in T) \to 0 \leq P (t)$
37	35	simprd	$⊢ (φ \land t \in T) \to P (t) \leq 1$
38		exple1	$⊢ ((P (t) \in ℝ \land 0 \leq P (t) \land P (t) \leq 1) \land N \in ℕ_{0}) \to {P (t)}^{N} \leq 1$
39	27 36 37 28 38	syl31anc	$⊢ (φ \land t \in T) \to {P (t)}^{N} \leq 1$
40	29 26 26 39	lesub2dd	$⊢ (φ \land t \in T) \to 1 - 1 \leq 1 - {P (t)}^{N}$
41	34 40	eqbrtrrid	$⊢ (φ \land t \in T) \to 0 \leq 1 - {P (t)}^{N}$
42	30 33 41	expge0d	$⊢ (φ \land t \in T) \to 0 \leq {(1 - {P (t)}^{N})}^{K^{N}}$
43	4 10 23 31	stoweidlem12	$⊢ (φ \land t \in T) \to Q (t) = {(1 - {P (t)}^{N})}^{K^{N}}$
44	42 43	breqtrrd	$⊢ (φ \land t \in T) \to 0 \leq Q (t)$
45		0red	$⊢ (φ \land t \in T) \to 0 \in ℝ$
46	27 28 36	expge0d	$⊢ (φ \land t \in T) \to 0 \leq {P (t)}^{N}$
47	45 29 26 46	lesub2dd	$⊢ (φ \land t \in T) \to 1 - {P (t)}^{N} \leq 1 - 0$
48		1m0e1	$⊢ 1 - 0 = 1$
49	47 48	breqtrdi	$⊢ (φ \land t \in T) \to 1 - {P (t)}^{N} \leq 1$
50		exple1	$⊢ ((1 - {P (t)}^{N} \in ℝ \land 0 \leq 1 - {P (t)}^{N} \land 1 - {P (t)}^{N} \leq 1) \land K^{N} \in ℕ_{0}) \to {(1 - {P (t)}^{N})}^{K^{N}} \leq 1$
51	30 41 49 33 50	syl31anc	$⊢ (φ \land t \in T) \to {(1 - {P (t)}^{N})}^{K^{N}} \leq 1$
52	43 51	eqbrtrd	$⊢ (φ \land t \in T) \to Q (t) \leq 1$
53	44 52	jca	$⊢ (φ \land t \in T) \to (0 \leq Q (t) \land Q (t) \leq 1)$
54	53	ex	$⊢ φ \to (t \in T \to (0 \leq Q (t) \land Q (t) \leq 1))$
55	2 54	ralrimi	$⊢ φ \to \forall t \in T (0 \leq Q (t) \land Q (t) \leq 1)$
56	3 4 10 23 31 7 17 18 11	stoweidlem24	$⊢ (φ \land t \in V) \to 1 - E < Q (t)$
57	56	ex	$⊢ φ \to (t \in V \to 1 - E < Q (t))$
58	2 57	ralrimi	$⊢ φ \to \forall t \in V 1 - E < Q (t)$
59	4 5 6 7 10 11 12 17 19	stoweidlem25	$⊢ (φ \land t \in (T ∖ U)) \to Q (t) < E$
60	59	ex	$⊢ φ \to (t \in (T ∖ U) \to Q (t) < E)$
61	2 60	ralrimi	$⊢ φ \to \forall t \in (T ∖ U) Q (t) < E$
62		nfmpt1	$⊢ \underline{Ⅎ} t (t \in T ⟼ {(1 - {P (t)}^{N})}^{K^{N}})$
63	4 62	nfcxfr	$⊢ \underline{Ⅎ} t Q$
64	63	nfeq2	$⊢ Ⅎ t y = Q$
65		fveq1	$⊢ y = Q \to y (t) = Q (t)$
66	65	breq2d	$⊢ y = Q \to (0 \leq y (t) \leftrightarrow 0 \leq Q (t))$
67	65	breq1d	$⊢ y = Q \to (y (t) \leq 1 \leftrightarrow Q (t) \leq 1)$
68	66 67	anbi12d	$⊢ y = Q \to ((0 \leq y (t) \land y (t) \leq 1) \leftrightarrow (0 \leq Q (t) \land Q (t) \leq 1))$
69	64 68	ralbid	$⊢ y = Q \to (\forall t \in T (0 \leq y (t) \land y (t) \leq 1) \leftrightarrow \forall t \in T (0 \leq Q (t) \land Q (t) \leq 1))$
70	65	breq2d	$⊢ y = Q \to (1 - E < y (t) \leftrightarrow 1 - E < Q (t))$
71	64 70	ralbid	$⊢ y = Q \to (\forall t \in V 1 - E < y (t) \leftrightarrow \forall t \in V 1 - E < Q (t))$
72	65	breq1d	$⊢ y = Q \to (y (t) < E \leftrightarrow Q (t) < E)$
73	64 72	ralbid	$⊢ y = Q \to (\forall t \in (T ∖ U) y (t) < E \leftrightarrow \forall t \in (T ∖ U) Q (t) < E)$
74	69 71 73	3anbi123d	$⊢ y = Q \to ((\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) \leftrightarrow (\forall t \in T (0 \leq Q (t) \land Q (t) \leq 1) \land \forall t \in V 1 - E < Q (t) \land \forall t \in (T ∖ U) Q (t) < E))$
75	74	rspcev	$⊢ (Q \in A \land (\forall t \in T (0 \leq Q (t) \land Q (t) \leq 1) \land \forall t \in V 1 - E < Q (t) \land \forall t \in (T ∖ U) Q (t) < 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)$
76	25 55 58 61 75	syl13anc	$⊢ φ \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 stoweidlem45

Proof