stoweidlem25

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

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

Proof

Step	Hyp	Ref	Expression
1		stoweidlem25.1	$⊢ Q = (t \in T ⟼ {(1 - {P (t)}^{N})}^{K^{N}})$
2		stoweidlem25.2	$⊢ φ \to N \in ℕ$
3		stoweidlem25.3	$⊢ φ \to K \in ℕ$
4		stoweidlem25.4	$⊢ φ \to D \in ℝ^{+}$
5		stoweidlem25.6	$⊢ φ \to P : T ⟶ ℝ$
6		stoweidlem25.7	$⊢ φ \to \forall t \in T (0 \leq P (t) \land P (t) \leq 1)$
7		stoweidlem25.8	$⊢ φ \to \forall t \in (T ∖ U) D \leq P (t)$
8		stoweidlem25.9	$⊢ φ \to E \in ℝ^{+}$
9		stoweidlem25.11	$⊢ φ \to \frac{1}{{K D}^{N}} < E$
10		eldifi	$⊢ t \in (T ∖ U) \to t \in T$
11	2	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
12	3	nnnn0d	$⊢ φ \to K \in ℕ_{0}$
13	1 5 11 12	stoweidlem12	$⊢ (φ \land t \in T) \to Q (t) = {(1 - {P (t)}^{N})}^{K^{N}}$
14		1red	$⊢ (φ \land t \in T) \to 1 \in ℝ$
15	5	ffvelrnda	$⊢ (φ \land t \in T) \to P (t) \in ℝ$
16	11	adantr	$⊢ (φ \land t \in T) \to N \in ℕ_{0}$
17	15 16	reexpcld	$⊢ (φ \land t \in T) \to {P (t)}^{N} \in ℝ$
18	14 17	resubcld	$⊢ (φ \land t \in T) \to 1 - {P (t)}^{N} \in ℝ$
19	3 11	nnexpcld	$⊢ φ \to K^{N} \in ℕ$
20	19	nnnn0d	$⊢ φ \to K^{N} \in ℕ_{0}$
21	20	adantr	$⊢ (φ \land t \in T) \to K^{N} \in ℕ_{0}$
22	18 21	reexpcld	$⊢ (φ \land t \in T) \to {(1 - {P (t)}^{N})}^{K^{N}} \in ℝ$
23	13 22	eqeltrd	$⊢ (φ \land t \in T) \to Q (t) \in ℝ$
24	10 23	sylan2	$⊢ (φ \land t \in (T ∖ U)) \to Q (t) \in ℝ$
25	3	nnred	$⊢ φ \to K \in ℝ$
26	4	rpred	$⊢ φ \to D \in ℝ$
27	25 26	remulcld	$⊢ φ \to K D \in ℝ$
28	27 11	reexpcld	$⊢ φ \to {K D}^{N} \in ℝ$
29	3	nncnd	$⊢ φ \to K \in ℂ$
30	3	nnne0d	$⊢ φ \to K \neq 0$
31	4	rpcnne0d	$⊢ φ \to (D \in ℂ \land D \neq 0)$
32		mulne0	$⊢ ((K \in ℂ \land K \neq 0) \land (D \in ℂ \land D \neq 0)) \to K D \neq 0$
33	29 30 31 32	syl21anc	$⊢ φ \to K D \neq 0$
34	4	rpcnd	$⊢ φ \to D \in ℂ$
35	29 34	mulcld	$⊢ φ \to K D \in ℂ$
36		expne0	$⊢ (K D \in ℂ \land N \in ℕ) \to ({K D}^{N} \neq 0 \leftrightarrow K D \neq 0)$
37	35 2 36	syl2anc	$⊢ φ \to ({K D}^{N} \neq 0 \leftrightarrow K D \neq 0)$
38	33 37	mpbird	$⊢ φ \to {K D}^{N} \neq 0$
39	28 38	rereccld	$⊢ φ \to \frac{1}{{K D}^{N}} \in ℝ$
40	39	adantr	$⊢ (φ \land t \in (T ∖ U)) \to \frac{1}{{K D}^{N}} \in ℝ$
41	8	rpred	$⊢ φ \to E \in ℝ$
42	41	adantr	$⊢ (φ \land t \in (T ∖ U)) \to E \in ℝ$
43	10 13	sylan2	$⊢ (φ \land t \in (T ∖ U)) \to Q (t) = {(1 - {P (t)}^{N})}^{K^{N}}$
44	2	adantr	$⊢ (φ \land t \in (T ∖ U)) \to N \in ℕ$
45	3	adantr	$⊢ (φ \land t \in (T ∖ U)) \to K \in ℕ$
46	4	adantr	$⊢ (φ \land t \in (T ∖ U)) \to D \in ℝ^{+}$
47	5	adantr	$⊢ (φ \land t \in (T ∖ U)) \to P : T ⟶ ℝ$
48	10	adantl	$⊢ (φ \land t \in (T ∖ U)) \to t \in T$
49	47 48	ffvelrnd	$⊢ (φ \land t \in (T ∖ U)) \to P (t) \in ℝ$
50		0red	$⊢ (φ \land t \in (T ∖ U)) \to 0 \in ℝ$
51	26	adantr	$⊢ (φ \land t \in (T ∖ U)) \to D \in ℝ$
52	4	rpgt0d	$⊢ φ \to 0 < D$
53	52	adantr	$⊢ (φ \land t \in (T ∖ U)) \to 0 < D$
54	7	r19.21bi	$⊢ (φ \land t \in (T ∖ U)) \to D \leq P (t)$
55	50 51 49 53 54	ltletrd	$⊢ (φ \land t \in (T ∖ U)) \to 0 < P (t)$
56	49 55	elrpd	$⊢ (φ \land t \in (T ∖ U)) \to P (t) \in ℝ^{+}$
57	6	adantr	$⊢ (φ \land t \in (T ∖ U)) \to \forall t \in T (0 \leq P (t) \land P (t) \leq 1)$
58		rsp	$⊢ \forall t \in T (0 \leq P (t) \land P (t) \leq 1) \to (t \in T \to (0 \leq P (t) \land P (t) \leq 1))$
59	57 48 58	sylc	$⊢ (φ \land t \in (T ∖ U)) \to (0 \leq P (t) \land P (t) \leq 1)$
60	59	simpld	$⊢ (φ \land t \in (T ∖ U)) \to 0 \leq P (t)$
61	59	simprd	$⊢ (φ \land t \in (T ∖ U)) \to P (t) \leq 1$
62	44 45 46 56 60 61 54	stoweidlem1	$⊢ (φ \land t \in (T ∖ U)) \to {(1 - {P (t)}^{N})}^{K^{N}} \leq \frac{1}{{K D}^{N}}$
63	43 62	eqbrtrd	$⊢ (φ \land t \in (T ∖ U)) \to Q (t) \leq \frac{1}{{K D}^{N}}$
64	9	adantr	$⊢ (φ \land t \in (T ∖ U)) \to \frac{1}{{K D}^{N}} < E$
65	24 40 42 63 64	lelttrd	$⊢ (φ \land t \in (T ∖ U)) \to Q (t) < E$

Metamath Proof Explorer

Theorem stoweidlem25

Proof