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

Theorem stoweidlem28 37771
 Description: There exists a δ as in Lemma 1 [BrosowskiDeutsh] p. 90: 0 < delta < 1 and p >= delta on . Here is used to represent δ in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem28.1
stoweidlem28.2
stoweidlem28.3
stoweidlem28.4
stoweidlem28.5
stoweidlem28.6
stoweidlem28.7
stoweidlem28.8
Assertion
Ref Expression
stoweidlem28
Distinct variable groups:   ,,   ,,   ,   ,
Allowed substitution hints:   (,)   ()   ()   (,)

Proof of Theorem stoweidlem28
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 halfre 10774 . . . . 5
2 halfgt0 10776 . . . . 5
31, 2elrpii 11251 . . . 4
43a1i 11 . . 3
5 halflt1 10777 . . . 4
65a1i 11 . . 3
7 nfcv 2564 . . . . . . 7
8 stoweidlem28.1 . . . . . . 7
97, 8nfdif 3524 . . . . . 6
109nfeq1 2577 . . . . 5
1110rzalf 37254 . . . 4
13 ovex 6272 . . . 4
14 eleq1 2489 . . . . 5
15 breq1 4364 . . . . 5
16 breq1 4364 . . . . . 6
1716ralbidv 2799 . . . . 5
1814, 15, 173anbi123d 1335 . . . 4
1913, 18spcev 3111 . . 3
204, 6, 12, 19syl3anc 1264 . 2
21 simplll 766 . . . 4
22 simplr 760 . . . 4
23 simpr 462 . . . 4
24 stoweidlem28.3 . . . . . . . . . . 11
25 stoweidlem28.4 . . . . . . . . . . 11
26 eqid 2423 . . . . . . . . . . 11
27 stoweidlem28.6 . . . . . . . . . . 11
2824, 25, 26, 27fcnre 37262 . . . . . . . . . 10
2928adantr 466 . . . . . . . . 9
30 eldifi 3525 . . . . . . . . . 10
3130adantl 467 . . . . . . . . 9
3229, 31ffvelrnd 5977 . . . . . . . 8
33 stoweidlem28.7 . . . . . . . . 9
34 nfcv 2564 . . . . . . . . . . . 12
35 nfv 1755 . . . . . . . . . . . 12
36 nfv 1755 . . . . . . . . . . . 12
37 fveq2 5820 . . . . . . . . . . . . 13
3837breq2d 4373 . . . . . . . . . . . 12
399, 34, 35, 36, 38cbvralf 2985 . . . . . . . . . . 11
4039biimpi 197 . . . . . . . . . 10
4140r19.21bi 2729 . . . . . . . . 9
4233, 41sylan 473 . . . . . . . 8
4332, 42elrpd 11284 . . . . . . 7
44433adant3 1025 . . . . . 6
45 stoweidlem28.2 . . . . . . . 8
469nfcri 2558 . . . . . . . 8
47 nfra1 2741 . . . . . . . 8
4845, 46, 47nf3an 1990 . . . . . . 7
49 rspa 2727 . . . . . . . . . 10
50493ad2antl3 1169 . . . . . . . . 9
51 simpl2 1009 . . . . . . . . . 10
52 fvres 5834 . . . . . . . . . 10
5351, 52syl 17 . . . . . . . . 9
54 fvres 5834 . . . . . . . . . 10
5554adantl 467 . . . . . . . . 9
5650, 53, 553brtr3d 4391 . . . . . . . 8
5756ex 435 . . . . . . 7
5848, 57ralrimi 2760 . . . . . 6
59 eleq1 2489 . . . . . . . . 9
60 breq1 4364 . . . . . . . . . 10
6160ralbidv 2799 . . . . . . . . 9
6259, 61anbi12d 715 . . . . . . . 8
6362spcegv 3105 . . . . . . 7
6444, 63syl 17 . . . . . 6
6544, 58, 64mp2and 683 . . . . 5
66 simpl1 1008 . . . . . 6
67 simprl 762 . . . . . 6
68 simprr 764 . . . . . 6
69 nfv 1755 . . . . . . . 8
70 nfra1 2741 . . . . . . . 8
7145, 69, 70nf3an 1990 . . . . . . 7
72 eqid 2423 . . . . . . 7
73283ad2ant1 1026 . . . . . . 7
74 difssd 3531 . . . . . . 7
75 simp2 1006 . . . . . . 7
76 simp3 1007 . . . . . . 7
7771, 72, 73, 74, 75, 76stoweidlem5 37748 . . . . . 6
7866, 67, 68, 77syl3anc 1264 . . . . 5
7965, 78exlimddv 1774 . . . 4
8021, 22, 23, 79syl3anc 1264 . . 3
81 eqid 2423 . . . . . 6 t t
82 stoweidlem28.5 . . . . . . . 8
83 stoweidlem28.8 . . . . . . . . 9
84 cmptop 20347 . . . . . . . . . . 11
8582, 84syl 17 . . . . . . . . . 10
86 elssuni 4186 . . . . . . . . . . . 12
8783, 86syl 17 . . . . . . . . . . 11
8887, 25syl6sseqr 3449 . . . . . . . . . 10
8925isopn2 19984 . . . . . . . . . 10
9085, 88, 89syl2anc 665 . . . . . . . . 9
9183, 90mpbid 213 . . . . . . . 8
92 cmpcld 20354 . . . . . . . 8 t
9382, 91, 92syl2anc 665 . . . . . . 7 t
9493adantr 466 . . . . . 6 t
9527adantr 466 . . . . . . 7
96 difssd 3531 . . . . . . 7
9725cnrest 20238 . . . . . . 7 t
9895, 96, 97syl2anc 665 . . . . . 6 t
99 df-ne 2596 . . . . . . . 8
100 difssd 3531 . . . . . . . . . 10
10125restuni 20115 . . . . . . . . . 10 t
10285, 100, 101syl2anc 665 . . . . . . . . 9 t
103102neeq1d 2655 . . . . . . . 8 t
10499, 103syl5rbbr 263 . . . . . . 7 t
105104biimpar 487 . . . . . 6 t
10681, 24, 94, 98, 105evth2 21925 . . . . 5 t t
107 nfcv 2564 . . . . . . 7 t
108 nfcv 2564 . . . . . . . . 9
109 nfcv 2564 . . . . . . . . 9 t
110108, 109, 9nfov 6270 . . . . . . . 8 t
111110nfuni 4163 . . . . . . 7 t
112 nfcv 2564 . . . . . . . . . 10
113112, 9nfres 5064 . . . . . . . . 9
114 nfcv 2564 . . . . . . . . 9
115113, 114nffv 5827 . . . . . . . 8
116 nfcv 2564 . . . . . . . 8
117 nfcv 2564 . . . . . . . . 9
118113, 117nffv 5827 . . . . . . . 8
119115, 116, 118nfbr 4406 . . . . . . 7
120 nfv 1755 . . . . . . 7
121 fveq2 5820 . . . . . . . 8
122121breq2d 4373 . . . . . . 7
123107, 111, 119, 120, 122cbvralf 2985 . . . . . 6 t t
124123rexbii 2861 . . . . 5 t t t t
125106, 124sylib 199 . . . 4 t t
1269, 111raleqf 2955 . . . . . . 7 t t
127126rexeqbi1dv 2968 . . . . . 6 t t t
128102, 127syl 17 . . . . 5 t t
129128adantr 466 . . . 4 t t
130125, 129mpbird 235 . . 3
13180, 130r19.29a 2904 . 2
13220, 131pm2.61dan 798 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wa 370   w3a 982   wceq 1437  wex 1657  wnf 1661   wcel 1872  wnfc 2551   wne 2594  wral 2709  wrex 2710   cdif 3371   wss 3374  c0 3699  cif 3849  cuni 4157   class class class wbr 4361   crn 4792   cres 4793  wf 5535  cfv 5539  (class class class)co 6244  cr 9484  cc0 9485  c1 9486   clt 9621   cle 9622   cdiv 10215  c2 10605  crp 11248  cioo 11581   ↾t crest 15257  ctg 15274  ctop 19854  ccld 19968   ccn 20177  ccmp 20338 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-rep 4474  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-inf2 8094  ax-cnex 9541  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-mulcom 9549  ax-addass 9550  ax-mulass 9551  ax-distr 9552  ax-i2m1 9553  ax-1ne0 9554  ax-1rid 9555  ax-rnegex 9556  ax-rrecex 9557  ax-cnre 9558  ax-pre-lttri 9559  ax-pre-lttrn 9560  ax-pre-ltadd 9561  ax-pre-mulgt0 9562  ax-pre-sup 9563  ax-mulf 9565 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-pss 3390  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4158  df-int 4194  df-iun 4239  df-iin 4240  df-br 4362  df-opab 4421  df-mpt 4422  df-tr 4457  df-eprel 4702  df-id 4706  df-po 4712  df-so 4713  df-fr 4750  df-se 4751  df-we 4752  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-pred 5337  df-ord 5383  df-on 5384  df-lim 5385  df-suc 5386  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-isom 5548  df-riota 6206  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-of 6484  df-om 6646  df-1st 6746  df-2nd 6747  df-supp 6865  df-wrecs 6978  df-recs 7040  df-rdg 7078  df-1o 7132  df-2o 7133  df-oadd 7136  df-er 7313  df-map 7424  df-ixp 7473  df-en 7520  df-dom 7521  df-sdom 7522  df-fin 7523  df-fsupp 7832  df-fi 7873  df-sup 7904  df-inf 7905  df-oi 7973  df-card 8320  df-cda 8544  df-pnf 9623  df-mnf 9624  df-xr 9625  df-ltxr 9626  df-le 9627  df-sub 9808  df-neg 9809  df-div 10216  df-nn 10556  df-2 10614  df-3 10615  df-4 10616  df-5 10617  df-6 10618  df-7 10619  df-8 10620  df-9 10621  df-10 10622  df-n0 10816  df-z 10884  df-dec 10998  df-uz 11106  df-q 11211  df-rp 11249  df-xneg 11355  df-xadd 11356  df-xmul 11357  df-ioo 11585  df-icc 11588  df-fz 11731  df-fzo 11862  df-seq 12159  df-exp 12218  df-hash 12461  df-cj 13101  df-re 13102  df-im 13103  df-sqrt 13237  df-abs 13238  df-struct 15061  df-ndx 15062  df-slot 15063  df-base 15064  df-sets 15065  df-ress 15066  df-plusg 15141  df-mulr 15142  df-starv 15143  df-sca 15144  df-vsca 15145  df-ip 15146  df-tset 15147  df-ple 15148  df-ds 15150  df-unif 15151  df-hom 15152  df-cco 15153  df-rest 15259  df-topn 15260  df-0g 15278  df-gsum 15279  df-topgen 15280  df-pt 15281  df-prds 15284  df-xrs 15338  df-qtop 15344  df-imas 15345  df-xps 15348  df-mre 15430  df-mrc 15431  df-acs 15433  df-mgm 16426  df-sgrp 16465  df-mnd 16475  df-submnd 16521  df-mulg 16614  df-cntz 16909  df-cmn 17370  df-psmet 18900  df-xmet 18901  df-met 18902  df-bl 18903  df-mopn 18904  df-cnfld 18909  df-top 19858  df-bases 19859  df-topon 19860  df-topsp 19861  df-cld 19971  df-cn 20180  df-cnp 20181  df-cmp 20339  df-tx 20514  df-hmeo 20707  df-xms 21272  df-ms 21273  df-tms 21274 This theorem is referenced by:  stoweidlem56  37800
 Copyright terms: Public domain W3C validator