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

Theorem stoweidlem25 27876
 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 simpl 443 . . . . 5
2 eldifi 3311 . . . . . 6
32adantl 452 . . . . 5
41, 3jca 518 . . . 4
5 1re 8853 . . . . . . . . . 10
65a1i 10 . . . . . . . . 9
7 stoweidlem25.6 . . . . . . . . . . . . . . 15
87adantr 451 . . . . . . . . . . . . . 14
9 simpr 447 . . . . . . . . . . . . . 14
108, 9jca 518 . . . . . . . . . . . . 13
1110idi 2 . . . . . . . . . . . 12
12 ffvelrn 5679 . . . . . . . . . . . 12
1311, 12syl 15 . . . . . . . . . . 11
14 stoweidlem25.2 . . . . . . . . . . . . 13
15 nnnn0 9988 . . . . . . . . . . . . 13
1614, 15syl 15 . . . . . . . . . . . 12
1716adantr 451 . . . . . . . . . . 11
1813, 17jca 518 . . . . . . . . . 10
19 reexpcl 11136 . . . . . . . . . 10
2018, 19syl 15 . . . . . . . . 9
216, 20jca 518 . . . . . . . 8
22 resubcl 9127 . . . . . . . 8
2321, 22syl 15 . . . . . . 7
24 stoweidlem25.3 . . . . . . . . . . 11
2524, 16jca 518 . . . . . . . . . 10
26 nnexpcl 11132 . . . . . . . . . 10
2725, 26syl 15 . . . . . . . . 9
28 nnnn0 9988 . . . . . . . . 9
2927, 28syl 15 . . . . . . . 8
3029adantr 451 . . . . . . 7
3123, 30jca 518 . . . . . 6
32 reexpcl 11136 . . . . . 6
3331, 32syl 15 . . . . 5
34 stoweidlem25.1 . . . . . . 7
35 nnnn0 9988 . . . . . . . 8
3624, 35syl 15 . . . . . . 7
3734, 7, 16, 36stoweidlem12 27863 . . . . . 6
3837eleq1d 2362 . . . . 5
3933, 38mpbird 223 . . . 4
404, 39syl 15 . . 3
415a1i 10 . . . . . 6
42 nnre 9769 . . . . . . . . . . 11
4324, 42syl 15 . . . . . . . . . 10
44 stoweidlem25.4 . . . . . . . . . . 11
45 rpre 10376 . . . . . . . . . . 11
4644, 45syl 15 . . . . . . . . . 10
4743, 46jca 518 . . . . . . . . 9
48 remulcl 8838 . . . . . . . . 9
4947, 48syl 15 . . . . . . . 8
5049, 16jca 518 . . . . . . 7
51 reexpcl 11136 . . . . . . 7
5250, 51syl 15 . . . . . 6
53 nncn 9770 . . . . . . . . . . 11
5424, 53syl 15 . . . . . . . . . 10
55 nnne0 9794 . . . . . . . . . . 11
5624, 55syl 15 . . . . . . . . . 10
5754, 56jca 518 . . . . . . . . 9
58 rpcn 10378 . . . . . . . . . . 11
5944, 58syl 15 . . . . . . . . . 10
60 rpne0 10385 . . . . . . . . . . 11
6144, 60syl 15 . . . . . . . . . 10
6259, 61jca 518 . . . . . . . . 9
6357, 62jca 518 . . . . . . . 8
64 mulne0 9426 . . . . . . . 8
6563, 64syl 15 . . . . . . 7
6654, 59jca 518 . . . . . . . . . 10
67 mulcl 8837 . . . . . . . . . 10
6866, 67syl 15 . . . . . . . . 9
6968, 14jca 518 . . . . . . . 8
70 expne0 11149 . . . . . . . 8
7169, 70syl 15 . . . . . . 7
7265, 71mpbird 223 . . . . . 6
7341, 52, 723jca 1132 . . . . 5
74 redivcl 9495 . . . . 5
7573, 74syl 15 . . . 4
77 stoweidlem25.9 . . . . 5
78 rpre 10376 . . . . 5
7977, 78syl 15 . . . 4
8140, 76, 803jca 1132 . 2
824, 37syl 15 . . . 4
8314adantr 451 . . . . 5
8424adantr 451 . . . . 5
8544adantr 451 . . . . 5
867adantr 451 . . . . . . . . 9
8786, 3jca 518 . . . . . . . 8
8887, 12syl 15 . . . . . . 7
89 0re 8854 . . . . . . . . . 10
9089a1i 10 . . . . . . . . 9
9146adantr 451 . . . . . . . . 9
9290, 91, 883jca 1132 . . . . . . . 8
93 rpgt0 10381 . . . . . . . . . . 11
9444, 93syl 15 . . . . . . . . . 10
9594adantr 451 . . . . . . . . 9
96 stoweidlem25.8 . . . . . . . . . . 11
97 rsp 2616 . . . . . . . . . . 11
9896, 97syl 15 . . . . . . . . . 10
9998imp 418 . . . . . . . . 9
10095, 99jca 518 . . . . . . . 8
101 ltletr 8929 . . . . . . . 8
10292, 100, 101sylc 56 . . . . . . 7
10388, 102jca 518 . . . . . 6
104 elrp 10372 . . . . . 6
105103, 104sylibr 203 . . . . 5
106 stoweidlem25.7 . . . . . . . 8
107106adantr 451 . . . . . . 7
108 rsp 2616 . . . . . . 7
109107, 3, 108sylc 56 . . . . . 6
110109simpld 445 . . . . 5
111109simprd 449 . . . . 5
11283, 84, 85, 105, 110, 111, 99stoweidlem1 27852 . . . 4
11382, 112eqbrtrd 4059 . . 3
114 stoweidlem25.11 . . . 4