Theorem stoweidlem25 27774

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.)

Hypotheses

Ref	Expression
stoweidlem25.1	|- Q = ( t e. T |-> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )
stoweidlem25.2	|- ( ph -> N e. NN )
stoweidlem25.3	|- ( ph -> K e. NN )
stoweidlem25.4	|- ( ph -> D e. RR+ )
stoweidlem25.6	|- ( ph -> P : T --> RR )
stoweidlem25.7	|- ( ph -> A. t e. T ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )
stoweidlem25.8	|- ( ph -> A. t e. ( T \ U ) D <_ ( P ` t ) )
stoweidlem25.9	|- ( ph -> E e. RR+ )
stoweidlem25.11	|- ( ph -> ( 1 / ( ( K x. D ) ^ N ) ) < E )

Assertion

Ref	Expression
stoweidlem25	|- ( ( ph /\ t e. ( T \ U ) ) -> ( Q ` t ) < E )

Distinct variable group:   t, T

Allowed substitution hints:   ph( t)   D( t)   P( t)   Q( t)   U( t)   E( t)   K( t)   N( t)

Proof of Theorem stoweidlem25

Step	Hyp	Ref	Expression
1		simpl 443	. . . . 5 |- ( ( ph /\ t e. ( T \ U ) ) -> ph )
2		eldifi 3298	. . . . . 6 |- ( t e. ( T \ U ) -> t e. T )
3	2	adantl 452	. . . . 5 |- ( ( ph /\ t e. ( T \ U ) ) -> t e. T )
4	1, 3	jca 518	. . . 4 |- ( ( ph /\ t e. ( T \ U ) ) -> ( ph /\ t e. T ) )
5		1re 8837	. . . . . . . . . 10 |- 1 e. RR
6	5	a1i 10	. . . . . . . . 9 |- ( ( ph /\ t e. T ) -> 1 e. RR )
7		stoweidlem25.6	. . . . . . . . . . . . . . 15 |- ( ph -> P : T --> RR )
8	7	adantr 451	. . . . . . . . . . . . . 14 |- ( ( ph /\ t e. T ) -> P : T --> RR )
9		simpr 447	. . . . . . . . . . . . . 14 |- ( ( ph /\ t e. T ) -> t e. T )
10	8, 9	jca 518	. . . . . . . . . . . . 13 |- ( ( ph /\ t e. T ) -> ( P : T --> RR /\ t e. T ) )
11	10	idi 2	. . . . . . . . . . . 12 |- ( ( ph /\ t e. T ) -> ( P : T --> RR /\ t e. T ) )
12		ffvelrn 5663	. . . . . . . . . . . 12 |- ( ( P : T --> RR /\ t e. T ) -> ( P ` t ) e. RR )
13	11, 12	syl 15	. . . . . . . . . . 11 |- ( ( ph /\ t e. T ) -> ( P ` t ) e. RR )
14		stoweidlem25.2	. . . . . . . . . . . . 13 |- ( ph -> N e. NN )
15		nnnn0 9972	. . . . . . . . . . . . 13 |- ( N e. NN -> N e. NN0 )
16	14, 15	syl 15	. . . . . . . . . . . 12 |- ( ph -> N e. NN0 )
17	16	adantr 451	. . . . . . . . . . 11 |- ( ( ph /\ t e. T ) -> N e. NN0 )
18	13, 17	jca 518	. . . . . . . . . 10 |- ( ( ph /\ t e. T ) -> ( ( P ` t ) e. RR /\ N e. NN0 ) )
19		reexpcl 11120	. . . . . . . . . 10 |- ( ( ( P ` t ) e. RR /\ N e. NN0 ) -> ( ( P ` t ) ^ N ) e. RR )
20	18, 19	syl 15	. . . . . . . . 9 |- ( ( ph /\ t e. T ) -> ( ( P ` t ) ^ N ) e. RR )
21	6, 20	jca 518	. . . . . . . 8 |- ( ( ph /\ t e. T ) -> ( 1 e. RR /\ ( ( P ` t ) ^ N ) e. RR ) )
22		resubcl 9111	. . . . . . . 8 |- ( ( 1 e. RR /\ ( ( P ` t ) ^ N ) e. RR ) -> ( 1 - ( ( P ` t ) ^ N ) ) e. RR )
23	21, 22	syl 15	. . . . . . 7 |- ( ( ph /\ t e. T ) -> ( 1 - ( ( P ` t ) ^ N ) ) e. RR )
24		stoweidlem25.3	. . . . . . . . . . 11 |- ( ph -> K e. NN )
25	24, 16	jca 518	. . . . . . . . . 10 |- ( ph -> ( K e. NN /\ N e. NN0 ) )
26		nnexpcl 11116	. . . . . . . . . 10 |- ( ( K e. NN /\ N e. NN0 ) -> ( K ^ N ) e. NN )
27	25, 26	syl 15	. . . . . . . . 9 |- ( ph -> ( K ^ N ) e. NN )
28		nnnn0 9972	. . . . . . . . 9 |- ( ( K ^ N ) e. NN -> ( K ^ N ) e. NN0 )
29	27, 28	syl 15	. . . . . . . 8 |- ( ph -> ( K ^ N ) e. NN0 )
30	29	adantr 451	. . . . . . 7 |- ( ( ph /\ t e. T ) -> ( K ^ N ) e. NN0 )
31	23, 30	jca 518	. . . . . 6 |- ( ( ph /\ t e. T ) -> ( ( 1 - ( ( P ` t ) ^ N ) ) e. RR /\ ( K ^ N ) e. NN0 ) )
32		reexpcl 11120	. . . . . 6 |- ( ( ( 1 - ( ( P ` t ) ^ N ) ) e. RR /\ ( K ^ N ) e. NN0 ) -> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) e. RR )
33	31, 32	syl 15	. . . . 5 |- ( ( ph /\ t e. T ) -> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) e. RR )
34		stoweidlem25.1	. . . . . . 7 |- Q = ( t e. T |-> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )
35		nnnn0 9972	. . . . . . . 8 |- ( K e. NN -> K e. NN0 )
36	24, 35	syl 15	. . . . . . 7 |- ( ph -> K e. NN0 )
37	34, 7, 16, 36	stoweidlem12 27761	. . . . . 6 |- ( ( ph /\ t e. T ) -> ( Q ` t ) = ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )
38	37	eleq1d 2349	. . . . 5 |- ( ( ph /\ t e. T ) -> ( ( Q ` t ) e. RR <-> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) e. RR ) )
39	33, 38	mpbird 223	. . . 4 |- ( ( ph /\ t e. T ) -> ( Q ` t ) e. RR )
40	4, 39	syl 15	. . 3 |- ( ( ph /\ t e. ( T \ U ) ) -> ( Q ` t ) e. RR )
41	5	a1i 10	. . . . . 6 |- ( ph -> 1 e. RR )
42		nnre 9753	. . . . . . . . . . 11 |- ( K e. NN -> K e. RR )
43	24, 42	syl 15	. . . . . . . . . 10 |- ( ph -> K e. RR )
44		stoweidlem25.4	. . . . . . . . . . 11 |- ( ph -> D e. RR+ )
45		rpre 10360	. . . . . . . . . . 11 |- ( D e. RR+ -> D e. RR )
46	44, 45	syl 15	. . . . . . . . . 10 |- ( ph -> D e. RR )
47	43, 46	jca 518	. . . . . . . . 9 |- ( ph -> ( K e. RR /\ D e. RR ) )
48		remulcl 8822	. . . . . . . . 9 |- ( ( K e. RR /\ D e. RR ) -> ( K x. D ) e. RR )
49	47, 48	syl 15	. . . . . . . 8 |- ( ph -> ( K x. D ) e. RR )
50	49, 16	jca 518	. . . . . . 7 |- ( ph -> ( ( K x. D ) e. RR /\ N e. NN0 ) )
51		reexpcl 11120	. . . . . . 7 |- ( ( ( K x. D ) e. RR /\ N e. NN0 ) -> ( ( K x. D ) ^ N ) e. RR )
52	50, 51	syl 15	. . . . . 6 |- ( ph -> ( ( K x. D ) ^ N ) e. RR )
53		nncn 9754	. . . . . . . . . . 11 |- ( K e. NN -> K e. CC )
54	24, 53	syl 15	. . . . . . . . . 10 |- ( ph -> K e. CC )
55		nnne0 9778	. . . . . . . . . . 11 |- ( K e. NN -> K =/= 0 )
56	24, 55	syl 15	. . . . . . . . . 10 |- ( ph -> K =/= 0 )
57	54, 56	jca 518	. . . . . . . . 9 |- ( ph -> ( K e. CC /\ K =/= 0 ) )
58		rpcn 10362	. . . . . . . . . . 11 |- ( D e. RR+ -> D e. CC )
59	44, 58	syl 15	. . . . . . . . . 10 |- ( ph -> D e. CC )
60		rpne0 10369	. . . . . . . . . . 11 |- ( D e. RR+ -> D =/= 0 )
61	44, 60	syl 15	. . . . . . . . . 10 |- ( ph -> D =/= 0 )
62	59, 61	jca 518	. . . . . . . . 9 |- ( ph -> ( D e. CC /\ D =/= 0 ) )
63	57, 62	jca 518	. . . . . . . 8 |- ( ph -> ( ( K e. CC /\ K =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) )
64		mulne0 9410	. . . . . . . 8 |- ( ( ( K e. CC /\ K =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( K x. D ) =/= 0 )
65	63, 64	syl 15	. . . . . . 7 |- ( ph -> ( K x. D ) =/= 0 )
66	54, 59	jca 518	. . . . . . . . . 10 |- ( ph -> ( K e. CC /\ D e. CC ) )
67		mulcl 8821	. . . . . . . . . 10 |- ( ( K e. CC /\ D e. CC ) -> ( K x. D ) e. CC )
68	66, 67	syl 15	. . . . . . . . 9 |- ( ph -> ( K x. D ) e. CC )
69	68, 14	jca 518	. . . . . . . 8 |- ( ph -> ( ( K x. D ) e. CC /\ N e. NN ) )
70		expne0 11133	. . . . . . . 8 |- ( ( ( K x. D ) e. CC /\ N e. NN ) -> ( ( ( K x. D ) ^ N ) =/= 0 <-> ( K x. D ) =/= 0 ) )
71	69, 70	syl 15	. . . . . . 7 |- ( ph -> ( ( ( K x. D ) ^ N ) =/= 0 <-> ( K x. D ) =/= 0 ) )
72	65, 71	mpbird 223	. . . . . 6 |- ( ph -> ( ( K x. D ) ^ N ) =/= 0 )
73	41, 52, 72	3jca 1132	. . . . 5 |- ( ph -> ( 1 e. RR /\ ( ( K x. D ) ^ N ) e. RR /\ ( ( K x. D ) ^ N ) =/= 0 ) )
74		redivcl 9479	. . . . 5 |- ( ( 1 e. RR /\ ( ( K x. D ) ^ N ) e. RR /\ ( ( K x. D ) ^ N ) =/= 0 ) -> ( 1 / ( ( K x. D ) ^ N ) ) e. RR )
75	73, 74	syl 15	. . . 4 |- ( ph -> ( 1 / ( ( K x. D ) ^ N ) ) e. RR )
76	75	adantr 451	. . 3 |- ( ( ph /\ t e. ( T \ U ) ) -> ( 1 / ( ( K x. D ) ^ N ) ) e. RR )
77		stoweidlem25.9	. . . . 5 |- ( ph -> E e. RR+ )
78		rpre 10360	. . . . 5 |- ( E e. RR+ -> E e. RR )
79	77, 78	syl 15	. . . 4 |- ( ph -> E e. RR )
80	79	adantr 451	. . 3 |- ( ( ph /\ t e. ( T \ U ) ) -> E e. RR )
81	40, 76, 80	3jca 1132	. 2 |- ( ( ph /\ t e. ( T \ U ) ) -> ( ( Q ` t ) e. RR /\ ( 1 / ( ( K x. D ) ^ N ) ) e. RR /\ E e. RR ) )
82	4, 37	syl 15	. . . 4 |- ( ( ph /\ t e. ( T \ U ) ) -> ( Q ` t ) = ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )
83	14	adantr 451	. . . . 5 |- ( ( ph /\ t e. ( T \ U ) ) -> N e. NN )
84	24	adantr 451	. . . . 5 |- ( ( ph /\ t e. ( T \ U ) ) -> K e. NN )
85	44	adantr 451	. . . . 5 |- ( ( ph /\ t e. ( T \ U ) ) -> D e. RR+ )
86	7	adantr 451	. . . . . . . . 9 |- ( ( ph /\ t e. ( T \ U ) ) -> P : T --> RR )
87	86, 3	jca 518	. . . . . . . 8 |- ( ( ph /\ t e. ( T \ U ) ) -> ( P : T --> RR /\ t e. T ) )
88	87, 12	syl 15	. . . . . . 7 |- ( ( ph /\ t e. ( T \ U ) ) -> ( P ` t ) e. RR )
89		0re 8838	. . . . . . . . . 10 |- 0 e. RR
90	89	a1i 10	. . . . . . . . 9 |- ( ( ph /\ t e. ( T \ U ) ) -> 0 e. RR )
91	46	adantr 451	. . . . . . . . 9 |- ( ( ph /\ t e. ( T \ U ) ) -> D e. RR )
92	90, 91, 88	3jca 1132	. . . . . . . 8 |- ( ( ph /\ t e. ( T \ U ) ) -> ( 0 e. RR /\ D e. RR /\ ( P ` t ) e. RR ) )
93		rpgt0 10365	. . . . . . . . . . 11 |- ( D e. RR+ -> 0 < D )
94	44, 93	syl 15	. . . . . . . . . 10 |- ( ph -> 0 < D )
95	94	adantr 451	. . . . . . . . 9 |- ( ( ph /\ t e. ( T \ U ) ) -> 0 < D )
96		stoweidlem25.8	. . . . . . . . . . 11 |- ( ph -> A. t e. ( T \ U ) D <_ ( P ` t ) )
97		rsp 2603	. . . . . . . . . . 11 |- ( A. t e. ( T \ U ) D <_ ( P ` t ) -> ( t e. ( T \ U ) -> D <_ ( P ` t ) ) )
98	96, 97	syl 15	. . . . . . . . . 10 |- ( ph -> ( t e. ( T \ U ) -> D <_ ( P ` t ) ) )
99	98	imp 418	. . . . . . . . 9 |- ( ( ph /\ t e. ( T \ U ) ) -> D <_ ( P ` t ) )
100	95, 99	jca 518	. . . . . . . 8 |- ( ( ph /\ t e. ( T \ U ) ) -> ( 0 < D /\ D <_ ( P ` t ) ) )
101		ltletr 8913	. . . . . . . 8 |- ( ( 0 e. RR /\ D e. RR /\ ( P ` t ) e. RR ) -> ( ( 0 < D /\ D <_ ( P ` t ) ) -> 0 < ( P ` t ) ) )
102	92, 100, 101	sylc 56	. . . . . . 7 |- ( ( ph /\ t e. ( T \ U ) ) -> 0 < ( P ` t ) )
103	88, 102	jca 518	. . . . . 6 |- ( ( ph /\ t e. ( T \ U ) ) -> ( ( P ` t ) e. RR /\ 0 < ( P ` t ) ) )
104		elrp 10356	. . . . . 6 |- ( ( P ` t ) e. RR+ <-> ( ( P ` t ) e. RR /\ 0 < ( P ` t ) ) )
105	103, 104	sylibr 203	. . . . 5 |- ( ( ph /\ t e. ( T \ U ) ) -> ( P ` t ) e. RR+ )
106		stoweidlem25.7	. . . . . . . 8 |- ( ph -> A. t e. T ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )
107	106	adantr 451	. . . . . . 7 |- ( ( ph /\ t e. ( T \ U ) ) -> A. t e. T ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )
108		rsp 2603	. . . . . . 7 |- ( A. t e. T ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) -> ( t e. T -> ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) ) )
109	107, 3, 108	sylc 56	. . . . . 6 |- ( ( ph /\ t e. ( T \ U ) ) -> ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )
110	109	simpld 445	. . . . 5 |- ( ( ph /\ t e. ( T \ U ) ) -> 0 <_ ( P ` t ) )
111	109	simprd 449	. . . . 5 |- ( ( ph /\ t e. ( T \ U ) ) -> ( P ` t ) <_ 1 )
112	83, 84, 85, 105, 110, 111, 99	stoweidlem1 27750	. . . 4 |- ( ( ph /\ t e. ( T \ U ) ) -> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) <_ ( 1 / ( ( K x. D ) ^ N ) ) )
113	82, 112	eqbrtrd 4043	. . 3 |- ( ( ph /\ t e. ( T \ U ) ) -> ( Q ` t ) <_ ( 1 / ( ( K x. D ) ^ N ) ) )
114		stoweidlem25.11	. . . 4 |- ( ph -> ( 1 / ( ( K x. D ) ^ N ) ) < E )
115	114	adantr 451	. . 3 |- ( ( ph /\ t e. ( T \ U ) ) -> ( 1 / ( ( K x. D ) ^ N ) ) < E )
116	113, 115	jca 518	. 2 |- ( ( ph /\ t e. ( T \ U ) ) -> ( ( Q ` t ) <_ ( 1 / ( ( K x. D ) ^ N ) ) /\ ( 1 / ( ( K x. D ) ^ N ) ) < E ) )
117		lelttr 8912	. 2 |- ( ( ( Q ` t ) e. RR /\ ( 1 / ( ( K x. D ) ^ N ) ) e. RR /\ E e. RR ) -> ( ( ( Q ` t ) <_ ( 1 / ( ( K x. D ) ^ N ) ) /\ ( 1 / ( ( K x. D ) ^ N ) ) < E ) -> ( Q ` t ) < E ) )
118	81, 116, 117	sylc 56	1 |- ( ( ph /\ t e. ( T \ U ) ) -> ( Q ` t ) < E )

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358   /\ w3a 934   = wceq 1623   e. wcel 1684   =/= wne 2446   A.wral 2543   \ cdif 3149   class class class wbr 4023   e. cmpt 4077   -->wf 5251   ` cfv 5255  (class class class)co 5858   CCcc 8735   RRcr 8736   0cc0 8737   1c1 8738   x. cmul 8742   < clt 8867   <_ cle 8868   - cmin 9037   / cdiv 9423   NNcn 9746   NN0cn0 9965   RR+crp 10354   ^cexp 11104

This theorem is referenced by:  stoweidlem45  27794

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-cnex 8793  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-mulcom 8801  ax-addass 8802  ax-mulass 8803  ax-distr 8804  ax-i2m1 8805  ax-1ne0 8806  ax-1rid 8807  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810  ax-pre-lttri 8811  ax-pre-lttrn 8812  ax-pre-ltadd 8813  ax-pre-mulgt0 8814

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-2nd 6123  df-riota 6304  df-recs 6388  df-rdg 6423  df-er 6660  df-en 6864  df-dom 6865  df-sdom 6866  df-pnf 8869  df-mnf 8870  df-xr 8871  df-ltxr 8872  df-le 8873  df-sub 9039  df-neg 9040  df-div 9424  df-nn 9747  df-2 9804  df-n0 9966  df-z 10025  df-uz 10231  df-rp 10355  df-seq 11047  df-exp 11105