Metamath Proof Explorer


Theorem 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=tT1PtNKN
stoweidlem25.2 φN
stoweidlem25.3 φK
stoweidlem25.4 φD+
stoweidlem25.6 φP:T
stoweidlem25.7 φtT0PtPt1
stoweidlem25.8 φtTUDPt
stoweidlem25.9 φE+
stoweidlem25.11 φ1KDN<E
Assertion stoweidlem25 φtTUQt<E

Proof

Step Hyp Ref Expression
1 stoweidlem25.1 Q=tT1PtNKN
2 stoweidlem25.2 φN
3 stoweidlem25.3 φK
4 stoweidlem25.4 φD+
5 stoweidlem25.6 φP:T
6 stoweidlem25.7 φtT0PtPt1
7 stoweidlem25.8 φtTUDPt
8 stoweidlem25.9 φE+
9 stoweidlem25.11 φ1KDN<E
10 eldifi tTUtT
11 2 nnnn0d φN0
12 3 nnnn0d φK0
13 1 5 11 12 stoweidlem12 φtTQt=1PtNKN
14 1red φtT1
15 5 ffvelrnda φtTPt
16 11 adantr φtTN0
17 15 16 reexpcld φtTPtN
18 14 17 resubcld φtT1PtN
19 3 11 nnexpcld φKN
20 19 nnnn0d φKN0
21 20 adantr φtTKN0
22 18 21 reexpcld φtT1PtNKN
23 13 22 eqeltrd φtTQt
24 10 23 sylan2 φtTUQt
25 3 nnred φK
26 4 rpred φD
27 25 26 remulcld φKD
28 27 11 reexpcld φKDN
29 3 nncnd φK
30 3 nnne0d φK0
31 4 rpcnne0d φDD0
32 mulne0 KK0DD0KD0
33 29 30 31 32 syl21anc φKD0
34 4 rpcnd φD
35 29 34 mulcld φKD
36 expne0 KDNKDN0KD0
37 35 2 36 syl2anc φKDN0KD0
38 33 37 mpbird φKDN0
39 28 38 rereccld φ1KDN
40 39 adantr φtTU1KDN
41 8 rpred φE
42 41 adantr φtTUE
43 10 13 sylan2 φtTUQt=1PtNKN
44 2 adantr φtTUN
45 3 adantr φtTUK
46 4 adantr φtTUD+
47 5 adantr φtTUP:T
48 10 adantl φtTUtT
49 47 48 ffvelrnd φtTUPt
50 0red φtTU0
51 26 adantr φtTUD
52 4 rpgt0d φ0<D
53 52 adantr φtTU0<D
54 7 r19.21bi φtTUDPt
55 50 51 49 53 54 ltletrd φtTU0<Pt
56 49 55 elrpd φtTUPt+
57 6 adantr φtTUtT0PtPt1
58 rsp tT0PtPt1tT0PtPt1
59 57 48 58 sylc φtTU0PtPt1
60 59 simpld φtTU0Pt
61 59 simprd φtTUPt1
62 44 45 46 56 60 61 54 stoweidlem1 φtTU1PtNKN1KDN
63 43 62 eqbrtrd φtTUQt1KDN
64 9 adantr φtTU1KDN<E
65 24 40 42 63 64 lelttrd φtTUQt<E