Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stoweidlem25 Structured version   Visualization version   Unicode version

Theorem stoweidlem25 37879
 Description: This lemma proves that for n sufficiently large, qn( t ) < ε, for all in : see Lemma 1 [BrosowskiDeutsh] p. 91 (at the top of page 91). is used to represent qn in the paper, to represent n in the paper, to represent k, to represent δ, to represent p, and to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem25.1
stoweidlem25.2
stoweidlem25.3
stoweidlem25.4
stoweidlem25.6
stoweidlem25.7
stoweidlem25.8
stoweidlem25.9
stoweidlem25.11
Assertion
Ref Expression
stoweidlem25
Distinct variable group:   ,
Allowed substitution hints:   ()   ()   ()   ()   ()   ()   ()   ()

Proof of Theorem stoweidlem25
StepHypRef Expression
1 eldifi 3554 . . 3
2 stoweidlem25.1 . . . . 5
3 stoweidlem25.6 . . . . 5
4 stoweidlem25.2 . . . . . 6
54nnnn0d 10922 . . . . 5
6 stoweidlem25.3 . . . . . 6
76nnnn0d 10922 . . . . 5
82, 3, 5, 7stoweidlem12 37866 . . . 4
9 1red 9655 . . . . . 6
103fnvinran 37329 . . . . . . 7
115adantr 467 . . . . . . 7
1210, 11reexpcld 12430 . . . . . 6
139, 12resubcld 10044 . . . . 5
146, 5nnexpcld 12434 . . . . . . 7
1514nnnn0d 10922 . . . . . 6
1615adantr 467 . . . . 5
1713, 16reexpcld 12430 . . . 4
188, 17eqeltrd 2528 . . 3
191, 18sylan2 477 . 2
206nnred 10621 . . . . . 6
21 stoweidlem25.4 . . . . . . 7
2221rpred 11338 . . . . . 6
2320, 22remulcld 9668 . . . . 5
2423, 5reexpcld 12430 . . . 4
256nncnd 10622 . . . . . 6
266nnne0d 10651 . . . . . 6
2721rpcnne0d 11347 . . . . . 6
28 mulne0 10251 . . . . . 6
2925, 26, 27, 28syl21anc 1266 . . . . 5
3021rpcnd 11340 . . . . . . 7
3125, 30mulcld 9660 . . . . . 6
32 expne0 12300 . . . . . 6
3331, 4, 32syl2anc 666 . . . . 5
3429, 33mpbird 236 . . . 4
3524, 34rereccld 10431 . . 3
37 stoweidlem25.9 . . . 4
3837rpred 11338 . . 3
401, 8sylan2 477 . . 3
414adantr 467 . . . 4
426adantr 467 . . . 4
4321adantr 467 . . . 4
443adantr 467 . . . . . 6
451adantl 468 . . . . . 6
4644, 45ffvelrnd 6021 . . . . 5
47 0red 9641 . . . . . 6
4822adantr 467 . . . . . 6
4921rpgt0d 11341 . . . . . . 7
5049adantr 467 . . . . . 6
51 stoweidlem25.8 . . . . . . 7
5251r19.21bi 2756 . . . . . 6
5347, 48, 46, 50, 52ltletrd 9792 . . . . 5
5446, 53elrpd 11335 . . . 4
55 stoweidlem25.7 . . . . . . 7
5655adantr 467 . . . . . 6
57 rsp 2753 . . . . . 6
5856, 45, 57sylc 62 . . . . 5
5958simpld 461 . . . 4
6058simprd 465 . . . 4
6141, 42, 43, 54, 59, 60, 52stoweidlem1 37855 . . 3
6240, 61eqbrtrd 4422 . 2
63 stoweidlem25.11 . . 3