stoweidlem24

Description: This lemma proves that for n sufficiently large, q_n( t ) > ( 1 - epsilon ), for all t in V : see Lemma 1 BrosowskiDeutsh p. 90, (at the bottom of page 90). Q is used to represent q_n in the paper, N to represent n in the paper, K to represent k , D to represent δ, and E to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem24.1	$⊢ V = \{t \in T \| P (t) < \frac{D}{2}\}$
	stoweidlem24.2	$⊢ Q = (t \in T ⟼ {(1 - {P (t)}^{N})}^{K^{N}})$
	stoweidlem24.3	$⊢ φ \to P : T ⟶ ℝ$
	stoweidlem24.4	$⊢ φ \to N \in ℕ_{0}$
	stoweidlem24.5	$⊢ φ \to K \in ℕ_{0}$
	stoweidlem24.6	$⊢ φ \to D \in ℝ^{+}$
	stoweidlem24.8	$⊢ φ \to E \in ℝ^{+}$
	stoweidlem24.9	$⊢ φ \to 1 - E < 1 - {(\frac{K D}{2})}^{N}$
	stoweidlem24.10	$⊢ φ \to \forall t \in T (0 \leq P (t) \land P (t) \leq 1)$
Assertion	stoweidlem24	$⊢ (φ \land t \in V) \to 1 - E < Q (t)$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem24.1	$⊢ V = \{t \in T \| P (t) < \frac{D}{2}\}$
2		stoweidlem24.2	$⊢ Q = (t \in T ⟼ {(1 - {P (t)}^{N})}^{K^{N}})$
3		stoweidlem24.3	$⊢ φ \to P : T ⟶ ℝ$
4		stoweidlem24.4	$⊢ φ \to N \in ℕ_{0}$
5		stoweidlem24.5	$⊢ φ \to K \in ℕ_{0}$
6		stoweidlem24.6	$⊢ φ \to D \in ℝ^{+}$
7		stoweidlem24.8	$⊢ φ \to E \in ℝ^{+}$
8		stoweidlem24.9	$⊢ φ \to 1 - E < 1 - {(\frac{K D}{2})}^{N}$
9		stoweidlem24.10	$⊢ φ \to \forall t \in T (0 \leq P (t) \land P (t) \leq 1)$
10		1red	$⊢ (φ \land t \in V) \to 1 \in ℝ$
11	7	rpred	$⊢ φ \to E \in ℝ$
12	11	adantr	$⊢ (φ \land t \in V) \to E \in ℝ$
13	10 12	resubcld	$⊢ (φ \land t \in V) \to 1 - E \in ℝ$
14	5	nn0red	$⊢ φ \to K \in ℝ$
15	14	adantr	$⊢ (φ \land t \in V) \to K \in ℝ$
16	3	adantr	$⊢ (φ \land t \in V) \to P : T ⟶ ℝ$
17	1	rabeq2i	$⊢ t \in V \leftrightarrow (t \in T \land P (t) < \frac{D}{2})$
18	17	simplbi	$⊢ t \in V \to t \in T$
19	18	adantl	$⊢ (φ \land t \in V) \to t \in T$
20	16 19	ffvelrnd	$⊢ (φ \land t \in V) \to P (t) \in ℝ$
21	15 20	remulcld	$⊢ (φ \land t \in V) \to K P (t) \in ℝ$
22	4	adantr	$⊢ (φ \land t \in V) \to N \in ℕ_{0}$
23	21 22	reexpcld	$⊢ (φ \land t \in V) \to {K P (t)}^{N} \in ℝ$
24	10 23	resubcld	$⊢ (φ \land t \in V) \to 1 - {K P (t)}^{N} \in ℝ$
25	20 22	reexpcld	$⊢ (φ \land t \in V) \to {P (t)}^{N} \in ℝ$
26	10 25	resubcld	$⊢ (φ \land t \in V) \to 1 - {P (t)}^{N} \in ℝ$
27	5 4	jca	$⊢ φ \to (K \in ℕ_{0} \land N \in ℕ_{0})$
28	27	adantr	$⊢ (φ \land t \in V) \to (K \in ℕ_{0} \land N \in ℕ_{0})$
29		nn0expcl	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0}) \to K^{N} \in ℕ_{0}$
30	28 29	syl	$⊢ (φ \land t \in V) \to K^{N} \in ℕ_{0}$
31	26 30	reexpcld	$⊢ (φ \land t \in V) \to {(1 - {P (t)}^{N})}^{K^{N}} \in ℝ$
32		1red	$⊢ φ \to 1 \in ℝ$
33	6	rpred	$⊢ φ \to D \in ℝ$
34	14 33	remulcld	$⊢ φ \to K D \in ℝ$
35	34	rehalfcld	$⊢ φ \to \frac{K D}{2} \in ℝ$
36	35 4	reexpcld	$⊢ φ \to {(\frac{K D}{2})}^{N} \in ℝ$
37	32 36	resubcld	$⊢ φ \to 1 - {(\frac{K D}{2})}^{N} \in ℝ$
38	37	adantr	$⊢ (φ \land t \in V) \to 1 - {(\frac{K D}{2})}^{N} \in ℝ$
39	8	adantr	$⊢ (φ \land t \in V) \to 1 - E < 1 - {(\frac{K D}{2})}^{N}$
40	36	adantr	$⊢ (φ \land t \in V) \to {(\frac{K D}{2})}^{N} \in ℝ$
41	35	adantr	$⊢ (φ \land t \in V) \to \frac{K D}{2} \in ℝ$
42	5	nn0ge0d	$⊢ φ \to 0 \leq K$
43	14 42	jca	$⊢ φ \to (K \in ℝ \land 0 \leq K)$
44	43	adantr	$⊢ (φ \land t \in V) \to (K \in ℝ \land 0 \leq K)$
45	9	r19.21bi	$⊢ (φ \land t \in T) \to (0 \leq P (t) \land P (t) \leq 1)$
46	45	simpld	$⊢ (φ \land t \in T) \to 0 \leq P (t)$
47	18 46	sylan2	$⊢ (φ \land t \in V) \to 0 \leq P (t)$
48		mulge0	$⊢ ((K \in ℝ \land 0 \leq K) \land (P (t) \in ℝ \land 0 \leq P (t))) \to 0 \leq K P (t)$
49	44 20 47 48	syl12anc	$⊢ (φ \land t \in V) \to 0 \leq K P (t)$
50	33	rehalfcld	$⊢ φ \to \frac{D}{2} \in ℝ$
51	50	adantr	$⊢ (φ \land t \in V) \to \frac{D}{2} \in ℝ$
52	17	simprbi	$⊢ t \in V \to P (t) < \frac{D}{2}$
53	52	adantl	$⊢ (φ \land t \in V) \to P (t) < \frac{D}{2}$
54	20 51 53	ltled	$⊢ (φ \land t \in V) \to P (t) \leq \frac{D}{2}$
55		lemul2a	$⊢ ((P (t) \in ℝ \land \frac{D}{2} \in ℝ \land (K \in ℝ \land 0 \leq K)) \land P (t) \leq \frac{D}{2}) \to K P (t) \leq K (\frac{D}{2})$
56	20 51 44 54 55	syl31anc	$⊢ (φ \land t \in V) \to K P (t) \leq K (\frac{D}{2})$
57	5	nn0cnd	$⊢ φ \to K \in ℂ$
58	57	adantr	$⊢ (φ \land t \in V) \to K \in ℂ$
59	6	rpcnd	$⊢ φ \to D \in ℂ$
60	59	adantr	$⊢ (φ \land t \in V) \to D \in ℂ$
61		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
62	61	a1i	$⊢ (φ \land t \in V) \to (2 \in ℂ \land 2 \neq 0)$
63		divass	$⊢ (K \in ℂ \land D \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to \frac{K D}{2} = K (\frac{D}{2})$
64	58 60 62 63	syl3anc	$⊢ (φ \land t \in V) \to \frac{K D}{2} = K (\frac{D}{2})$
65	56 64	breqtrrd	$⊢ (φ \land t \in V) \to K P (t) \leq \frac{K D}{2}$
66		leexp1a	$⊢ ((K P (t) \in ℝ \land \frac{K D}{2} \in ℝ \land N \in ℕ_{0}) \land (0 \leq K P (t) \land K P (t) \leq \frac{K D}{2})) \to {K P (t)}^{N} \leq {(\frac{K D}{2})}^{N}$
67	21 41 22 49 65 66	syl32anc	$⊢ (φ \land t \in V) \to {K P (t)}^{N} \leq {(\frac{K D}{2})}^{N}$
68	23 40 10 67	lesub2dd	$⊢ (φ \land t \in V) \to 1 - {(\frac{K D}{2})}^{N} \leq 1 - {K P (t)}^{N}$
69	13 38 24 39 68	ltletrd	$⊢ (φ \land t \in V) \to 1 - E < 1 - {K P (t)}^{N}$
70	20	recnd	$⊢ (φ \land t \in V) \to P (t) \in ℂ$
71	58 70 22	mulexpd	$⊢ (φ \land t \in V) \to {K P (t)}^{N} = K^{N} {P (t)}^{N}$
72	71	eqcomd	$⊢ (φ \land t \in V) \to K^{N} {P (t)}^{N} = {K P (t)}^{N}$
73	72	oveq2d	$⊢ (φ \land t \in V) \to 1 - K^{N} {P (t)}^{N} = 1 - {K P (t)}^{N}$
74	18 45	sylan2	$⊢ (φ \land t \in V) \to (0 \leq P (t) \land P (t) \leq 1)$
75	74	simprd	$⊢ (φ \land t \in V) \to P (t) \leq 1$
76		exple1	$⊢ ((P (t) \in ℝ \land 0 \leq P (t) \land P (t) \leq 1) \land N \in ℕ_{0}) \to {P (t)}^{N} \leq 1$
77	20 47 75 22 76	syl31anc	$⊢ (φ \land t \in V) \to {P (t)}^{N} \leq 1$
78		stoweidlem10	$⊢ ({P (t)}^{N} \in ℝ \land K^{N} \in ℕ_{0} \land {P (t)}^{N} \leq 1) \to 1 - K^{N} {P (t)}^{N} \leq {(1 - {P (t)}^{N})}^{K^{N}}$
79	25 30 77 78	syl3anc	$⊢ (φ \land t \in V) \to 1 - K^{N} {P (t)}^{N} \leq {(1 - {P (t)}^{N})}^{K^{N}}$
80	73 79	eqbrtrrd	$⊢ (φ \land t \in V) \to 1 - {K P (t)}^{N} \leq {(1 - {P (t)}^{N})}^{K^{N}}$
81	13 24 31 69 80	ltletrd	$⊢ (φ \land t \in V) \to 1 - E < {(1 - {P (t)}^{N})}^{K^{N}}$
82	2 3 4 5	stoweidlem12	$⊢ (φ \land t \in T) \to Q (t) = {(1 - {P (t)}^{N})}^{K^{N}}$
83	18 82	sylan2	$⊢ (φ \land t \in V) \to Q (t) = {(1 - {P (t)}^{N})}^{K^{N}}$
84	81 83	breqtrrd	$⊢ (φ \land t \in V) \to 1 - E < Q (t)$

Metamath Proof Explorer

Theorem stoweidlem24

Proof