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

Theorem stoweidlem1 37973
 Description: Lemma for stoweid 38037. This lemma is used by Lemma 1 in [BrosowskiDeutsh] p. 90; the key step uses Bernoulli's inequality bernneq 12436. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem1.1
stoweidlem1.2
stoweidlem1.3
stoweidlem1.5
stoweidlem1.6
stoweidlem1.7
stoweidlem1.8
Assertion
Ref Expression
stoweidlem1

Proof of Theorem stoweidlem1
StepHypRef Expression
1 1re 9660 . . . . 5
21a1i 11 . . . 4
3 stoweidlem1.5 . . . . . 6
43rpred 11364 . . . . 5
5 stoweidlem1.1 . . . . . 6
65nnnn0d 10949 . . . . 5
74, 6reexpcld 12471 . . . 4
82, 7resubcld 10068 . . 3
9 stoweidlem1.2 . . . . 5
109nnnn0d 10949 . . . 4
1110, 6nn0expcld 12476 . . 3
128, 11reexpcld 12471 . 2
13 2nn0 10910 . . . . . . . 8
1413a1i 11 . . . . . . 7
1514, 6nn0mulcld 10954 . . . . . 6
164, 15reexpcld 12471 . . . . 5
172, 16resubcld 10068 . . . 4
1817, 11reexpcld 12471 . . 3
199nnred 10646 . . . . 5
2019, 4remulcld 9689 . . . 4
2120, 6reexpcld 12471 . . 3
229nncnd 10647 . . . . 5
233rpcnd 11366 . . . . 5
249nnne0d 10676 . . . . 5
253rpne0d 11369 . . . . 5
2622, 23, 24, 25mulne0d 10286 . . . 4
2722, 23mulcld 9681 . . . . 5
28 expne0 12341 . . . . 5
2927, 5, 28syl2anc 673 . . . 4
3026, 29mpbird 240 . . 3
3118, 21, 30redivcld 10457 . 2
32 stoweidlem1.3 . . . . . 6
3332rpred 11364 . . . . 5
3419, 33remulcld 9689 . . . 4
3534, 6reexpcld 12471 . . 3
3632rpcnd 11366 . . . . 5
3732rpne0d 11369 . . . . 5
3822, 36, 24, 37mulne0d 10286 . . . 4
3922, 36mulcld 9681 . . . . 5
40 expne0 12341 . . . . 5
4139, 5, 40syl2anc 673 . . . 4
4238, 41mpbird 240 . . 3
432, 35, 42redivcld 10457 . 2
4419, 6reexpcld 12471 . . . . . . . 8
4544, 7remulcld 9689 . . . . . . 7
462, 45readdcld 9688 . . . . . 6
4712, 46remulcld 9689 . . . . 5
4847, 21, 30redivcld 10457 . . . 4
492, 7readdcld 9688 . . . . . . 7
5049, 11reexpcld 12471 . . . . . 6
5112, 50remulcld 9689 . . . . 5
5251, 21, 30redivcld 10457 . . . 4
5346, 21, 30redivcld 10457 . . . . . 6
54 stoweidlem1.6 . . . . . . . . 9
55 stoweidlem1.7 . . . . . . . . 9
56 exple1 12370 . . . . . . . . 9
574, 54, 55, 6, 56syl31anc 1295 . . . . . . . 8
582, 7subge0d 10224 . . . . . . . 8
5957, 58mpbird 240 . . . . . . 7
608, 11, 59expge0d 12472 . . . . . 6
6127, 6expcld 12454 . . . . . . . . 9
6261, 30dividd 10403 . . . . . . . 8
6361addid2d 9852 . . . . . . . . . 10
64 0red 9662 . . . . . . . . . . 11
65 0le1 10158 . . . . . . . . . . . 12
6665a1i 11 . . . . . . . . . . 11
6764, 2, 21, 66leadd1dd 10248 . . . . . . . . . 10
6863, 67eqbrtrrd 4418 . . . . . . . . 9
692, 21readdcld 9688 . . . . . . . . . 10
705nnzd 11062 . . . . . . . . . . 11
719nngt0d 10675 . . . . . . . . . . . 12
723rpgt0d 11367 . . . . . . . . . . . 12
7319, 4, 71, 72mulgt0d 9807 . . . . . . . . . . 11
74 expgt0 12343 . . . . . . . . . . 11
7520, 70, 73, 74syl3anc 1292 . . . . . . . . . 10
76 lediv1 10492 . . . . . . . . . 10
7721, 69, 21, 75, 76syl112anc 1296 . . . . . . . . 9
7868, 77mpbid 215 . . . . . . . 8
7962, 78eqbrtrrd 4418 . . . . . . 7
8022, 23, 6mulexpd 12469 . . . . . . . . 9
8180oveq2d 6324 . . . . . . . 8
8281oveq1d 6323 . . . . . . 7
8379, 82breqtrd 4420 . . . . . 6
8412, 53, 60, 83lemulge11d 10566 . . . . 5
85 1cnd 9677 . . . . . . . 8
8623, 6expcld 12454 . . . . . . . 8
8785, 86subcld 10005 . . . . . . 7
8887, 11expcld 12454 . . . . . 6
8922, 6expcld 12454 . . . . . . . 8
9089, 86mulcld 9681 . . . . . . 7
9185, 90addcld 9680 . . . . . 6
9288, 91, 61, 30divassd 10440 . . . . 5
9384, 92breqtrrd 4422 . . . 4
9489, 86mulcomd 9682 . . . . . . . 8
9594oveq2d 6324 . . . . . . 7
962renegcld 10067 . . . . . . . . 9
97 le0neg2 10144 . . . . . . . . . . . 12
981, 97ax-mp 5 . . . . . . . . . . 11
9965, 98mpbi 213 . . . . . . . . . 10
10099a1i 11 . . . . . . . . 9
1014, 6, 54expge0d 12472 . . . . . . . . 9
10296, 64, 7, 100, 101letrd 9809 . . . . . . . 8
103 bernneq 12436 . . . . . . . 8
1047, 11, 102, 103syl3anc 1292 . . . . . . 7
10595, 104eqbrtrd 4416 . . . . . 6
10646, 50, 12, 60, 105lemul2ad 10569 . . . . 5
107 lediv1 10492 . . . . . 6
10847, 51, 21, 75, 107syl112anc 1296 . . . . 5
109106, 108mpbid 215 . . . 4
11012, 48, 52, 93, 109letrd 9809 . . 3
11185, 86addcld 9680 . . . . . . 7
11287, 111mulcomd 9682 . . . . . 6
113112oveq1d 6323 . . . . 5
11487, 111, 11mulexpd 12469 . . . . 5
115 subsq 12420 . . . . . . . 8
11685, 86, 115syl2anc 673 . . . . . . 7
117 sq1 12407 . . . . . . . . 9
118117a1i 11 . . . . . . . 8
11923, 14, 6expmuld 12457 . . . . . . . . 9
1205nncnd 10647 . . . . . . . . . . 11
121 2cnd 10704 . . . . . . . . . . 11
122120, 121mulcomd 9682 . . . . . . . . . 10
123122oveq2d 6324 . . . . . . . . 9
124119, 123eqtr3d 2507 . . . . . . . 8
125118, 124oveq12d 6326 . . . . . . 7
126116, 125eqtr3d 2507 . . . . . 6
127126oveq1d 6323 . . . . 5
128113, 114, 1273eqtr3d 2513 . . . 4
129128oveq1d 6323 . . 3
130110, 129breqtrd 4420 . 2
13118, 2jca 541 . . . 4
132 exple1 12370 . . . . . . 7
1334, 54, 55, 15, 132syl31anc 1295 . . . . . 6
1342, 16subge0d 10224 . . . . . 6
135133, 134mpbird 240 . . . . 5
13617, 11, 135expge0d 12472 . . . 4
137 1m1e0 10700 . . . . . . 7
1384, 15, 54expge0d 12472 . . . . . . 7
139137, 138syl5eqbr 4429 . . . . . 6
1402, 2, 16, 139subled 10237 . . . . 5
141 exple1 12370 . . . . 5
14217, 135, 140, 11, 141syl31anc 1295 . . . 4
143131, 136, 142jca32 544 . . 3
14435, 21jca 541 . . 3
14532rpgt0d 11367 . . . . . 6
14619, 33, 71, 145mulgt0d 9807 . . . . 5
147 expgt0 12343 . . . . 5
14834, 70, 146, 147syl3anc 1292 . . . 4
14964, 19, 71ltled 9800 . . . . . 6
15064, 33, 145ltled 9800 . . . . . 6
15119, 33, 149, 150mulge0d 10211 . . . . 5
152 stoweidlem1.8 . . . . . 6
15333, 4, 19, 149, 152lemul2ad 10569 . . . . 5
154 leexp1a 12369 . . . . 5
15534, 20, 6, 151, 153, 154syl32anc 1300 . . . 4
156148, 155jca 541 . . 3
157 lediv12a 10521 . . 3
158143, 144, 156, 157syl12anc 1290 . 2
15912, 31, 43, 130, 158letrd 9809 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 189   wa 376   wceq 1452   wcel 1904   wne 2641   class class class wbr 4395  (class class class)co 6308  cc 9555  cr 9556  cc0 9557  c1 9558   caddc 9560   cmul 9562   clt 9693   cle 9694   cmin 9880  cneg 9881   cdiv 10291  cn 10631  c2 10681  cn0 10893  cz 10961  crp 11325  cexp 12310 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-er 7381  df-en 7588  df-dom 7589  df-sdom 7590  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-div 10292  df-nn 10632  df-2 10690  df-n0 10894  df-z 10962  df-uz 11183  df-rp 11326  df-seq 12252  df-exp 12311 This theorem is referenced by:  stoweidlem25  37997
 Copyright terms: Public domain W3C validator