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

Theorem stoweidlem51 29520
Description: There exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91. Here is used to represent in the paper, because here is used for the subalgebra of functions. is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem51.1
stoweidlem51.2
stoweidlem51.3
stoweidlem51.4
stoweidlem51.5
stoweidlem51.6
stoweidlem51.7
stoweidlem51.8
stoweidlem51.9
stoweidlem51.10
stoweidlem51.11
stoweidlem51.12
stoweidlem51.13
stoweidlem51.14
stoweidlem51.15
stoweidlem51.16
stoweidlem51.17
stoweidlem51.18
stoweidlem51.19
stoweidlem51.20
stoweidlem51.21
stoweidlem51.22
stoweidlem51.23
Assertion
Ref Expression
stoweidlem51
Distinct variable groups:   , , , ,   , ,M, ,   , ,   , , , ,   , , , ,   , ,   , ,   ,M   , ,   ,   ,   ,   ,   , ,   , ,   ,   ,   ,   ,   ,

Proof of Theorem stoweidlem51
StepHypRef Expression
1 stoweidlem51.5 . . . 4
2 ssrab2 3414 . . . 4
31, 2eqsstri 3363 . . 3
4 stoweidlem51.6 . . . 4
5 stoweidlem51.7 . . . 4
6 1z 10621 . . . . . . 7
76a1i 11 . . . . . 6
8 stoweidlem51.10 . . . . . . 7
98nnzd 10691 . . . . . 6
107, 9, 93jca 1153 . . . . 5
118nnge1d 10310 . . . . . 6
128nnred 10283 . . . . . . 7
1312leidd 9852 . . . . . 6
1411, 13jca 522 . . . . 5
15 elfz2 11388 . . . . 5
1610, 14, 15sylanbrc 649 . . . 4
17 stoweidlem51.12 . . . 4
18 stoweidlem51.2 . . . . 5
19 eqid 2422 . . . . 5
20 stoweidlem51.20 . . . . 5
21 stoweidlem51.19 . . . . 5
2218, 1, 19, 20, 21stoweidlem16 29485 . . . 4
23 stoweidlem51.21 . . . 4
244, 5, 16, 17, 22, 23fmulcl 29435 . . 3
253, 24sseldi 3331 . 2
261eleq2i 2486 . . . . . . 7
27 nfcv 2558 . . . . . . . . . . 11
28 nfrab1 2880 . . . . . . . . . . . . . 14
291, 28nfcxfr 2555 . . . . . . . . . . . . 13
30 nfcv 2558 . . . . . . . . . . . . 13
3129, 29, 30nfmpt2 6125 . . . . . . . . . . . 12
324, 31nfcxfr 2555 . . . . . . . . . . 11
33 nfcv 2558 . . . . . . . . . . 11
3427, 32, 33nfseq 11757 . . . . . . . . . 10
35 nfcv 2558 . . . . . . . . . 10
3634, 35nffv 5668 . . . . . . . . 9
375, 36nfcxfr 2555 . . . . . . . 8
38 nfcv 2558 . . . . . . . 8
39 nfcv 2558 . . . . . . . . 9
40 nfcv 2558 . . . . . . . . . . 11
41 nfcv 2558 . . . . . . . . . . 11
42 nfcv 2558 . . . . . . . . . . . 12
4337, 42nffv 5668 . . . . . . . . . . 11
4440, 41, 43nfbr 4311 . . . . . . . . . 10
4543, 41, 27nfbr 4311 . . . . . . . . . 10
4644, 45nfan 1851 . . . . . . . . 9
4739, 46nfral 2748 . . . . . . . 8
48 nfcv 2558 . . . . . . . . . . . . 13
49 nfra1 2745 . . . . . . . . . . . . . . . . 17
50 nfcv 2558 . . . . . . . . . . . . . . . . 17
5149, 50nfrab 2881 . . . . . . . . . . . . . . . 16
521, 51nfcxfr 2555 . . . . . . . . . . . . . . 15
53 nfmpt1 4356 . . . . . . . . . . . . . . 15
5452, 52, 53nfmpt2 6125 . . . . . . . . . . . . . 14
554, 54nfcxfr 2555 . . . . . . . . . . . . 13
56 nfcv 2558 . . . . . . . . . . . . 13
5748, 55, 56nfseq 11757 . . . . . . . . . . . 12
58 nfcv 2558 . . . . . . . . . . . 12
5957, 58nffv 5668 . . . . . . . . . . 11
605, 59nfcxfr 2555 . . . . . . . . . 10
6160nfeq2 2569 . . . . . . . . 9
62 fveq1 5660 . . . . . . . . . . 11
6362breq2d 4279 . . . . . . . . . 10
6462breq1d 4277 . . . . . . . . . 10
6563, 64anbi12d 695 . . . . . . . . 9
6661, 65ralbid 2712 . . . . . . . 8
6737, 38, 47, 66elrabf 3093 . . . . . . 7
6826, 67bitri 243 . . . . . 6
6924, 68sylib 190 . . . . 5
7069simprd 453 . . . 4
71 stoweidlem51.1 . . . . 5
72 stoweidlem51.8 . . . . 5
73 stoweidlem51.9 . . . . 5
74 stoweidlem51.11 . . . . 5
75 stoweidlem51.14 . . . . 5
76 stoweidlem51.15 . . . . 5
77 nfv 1664 . . . . . . 7
7818, 77nfan 1851 . . . . . 6
7917fnvinran 29409 . . . . . . . . . . . 12
80 fveq1 5660 . . . . . . . . . . . . . . . . 17
8180breq2d 4279 . . . . . . . . . . . . . . . 16
8280breq1d 4277 . . . . . . . . . . . . . . . 16
8381, 82anbi12d 695 . . . . . . . . . . . . . . 15
8483ralbidv 2714 . . . . . . . . . . . . . 14
8584, 1elrab2 3097 . . . . . . . . . . . . 13
8685simplbi 450 . . . . . . . . . . . 12
8779, 86syl 16 . . . . . . . . . . 11
88 eleq1 2482 . . . . . . . . . . . . . . 15
8988anbi2d 688 . . . . . . . . . . . . . 14
90 feq1 5512 . . . . . . . . . . . . . 14
9189, 90imbi12d 314 . . . . . . . . . . . . 13
9220a1i 11 . . . . . . . . . . . . 13
9391, 92vtoclga 3014 . . . . . . . . . . . 12
9493anabsi7 800 . . . . . . . . . . 11
9587, 94syldan 460 . . . . . . . . . 10
9695adantr 455 . . . . . . . . 9
9774fnvinran 29409 . . . . . . . . . . 11
98 simpl 447 . . . . . . . . . . . 12
9998, 97jca 522 . . . . . . . . . . 11
100 stoweidlem51.3 . . . . . . . . . . . . . 14
101 stoweidlem51.4 . . . . . . . . . . . . . . 15
102101nfel2 2570 . . . . . . . . . . . . . 14
103100, 102nfan 1851 . . . . . . . . . . . . 13
104 nfv 1664 . . . . . . . . . . . . 13
105103, 104nfim 1843 . . . . . . . . . . . 12
106 eleq1 2482 . . . . . . . . . . . . . 14
107106anbi2d 688 . . . . . . . . . . . . 13
108 sseq1 3354 . . . . . . . . . . . . 13
109107, 108imbi12d 314 . . . . . . . . . . . 12
110 stoweidlem51.13 . . . . . . . . . . . 12
111105, 109, 110vtoclg1f 3007 . . . . . . . . . . 11
11297, 99, 111sylc 59 . . . . . . . . . 10
113112sselda 3333 . . . . . . . . 9
11496, 113ffvelrnd 5814 . . . . . . . 8
115 stoweidlem51.22 . . . . . . . . . . 11
116115rpred 10972 . . . . . . . . . 10
117116ad2antrr 710 . . . . . . . . 9
11812ad2antrr 710 . . . . . . . . 9
1198nnne0d 10312 . . . . . . . . . 10
120119ad2antrr 710 . . . . . . . . 9
121117, 118, 120redivcld 10105 . . . . . . . 8
122 stoweidlem51.17 . . . . . . . . 9
123122r19.21bi 2793 . . . . . . . 8
124 1re 9331 . . . . . . . . . . . . 13
125124a1i 11 . . . . . . . . . . . 12
126 0lt1 9808 . . . . . . . . . . . . 13
127126a1i 11 . . . . . . . . . . . 12
1288nngt0d 10311 . . . . . . . . . . . 12
129115rpregt0d 10978 . . . . . . . . . . . 12
130 lediv2 10168 . . . . . . . . . . . 12
131125, 127, 12, 128, 129, 130syl221anc 1214 . . . . . . . . . . 11
13211, 131mpbid 204 . . . . . . . . . 10
133115rpcnd 10974 . . . . . . . . . . 11
134133div1d 10045 . . . . . . . . . 10
135132, 134breqtrd 4291 . . . . . . . . 9
136135ad2antrr 710 . . . . . . . 8
137114, 121, 117, 123, 136ltletrd 9477 . . . . . . 7
138137ex 427 . . . . . 6
13978, 138ralrimi 2776 . . . . 5
14071, 18, 1, 4, 5, 72, 73, 8, 74, 17, 75, 76, 139, 23, 20, 21, 115stoweidlem48 29517 . . . 4
141 stoweidlem51.18 . . . . 5
142 stoweidlem51.23 . . . . 5
1433sseli 3329 . . . . . 6
144143, 20sylan2 464 . . . . 5
145 stoweidlem51.16 . . . . 5
14671, 18, 52, 4, 5, 72, 73, 8, 17, 141, 115, 142, 144, 22, 23, 145stoweidlem42 29511 . . . 4
14770, 140, 1463jca 1153 . . 3
14825, 147jca 522 . 2
149 eleq1 2482 . . . 4
15060nfeq2 2569 . . . . . 6
151 fveq1 5660 . . . . . . . 8
152151breq2d 4279 . . . . . . 7
153151breq1d 4277 . . . . . . 7
154152, 153anbi12d 695 . . . . . 6
155150, 154ralbid 2712 . . . . 5
156151breq1d 4277 . . . . . 6
157150, 156ralbid 2712 . . . . 5
158151breq2d 4279 . . . . . 6
159150, 158ralbid 2712 . . . . 5
160155, 157, 1593anbi123d 1274 . . . 4
161149, 160anbi12d 695 . . 3
162161spcegv 3036 . 2
16325, 148, 162sylc 59 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 178  /\wa 362  /\w3a 950  E.wex 1581  F/wnf 1584  =wceq 1687  e.wcel 1749  F/_wnfc 2545  =/=wne 2585  A.wral 2694  {crab 2698   cvv 2951  C_wss 3305  U.cuni 4066   class class class wbr 4267  e.cmpt 4325  rancrn 4812  -->wf 5386  `cfv 5390  (class class class)co 6061  e.cmpt2 6063   cr 9227  0cc0 9228  1c1 9229   cmul 9233   clt 9364   cle 9365   cmin 9541   cdiv 9939   cn 10268  3c3 10318   cz 10591   crp 10936   cfz 11381  seqcseq 11747
This theorem is referenced by:  stoweidlem54  29523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-8 1751  ax-9 1753  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403  ax-rep 4378  ax-sep 4388  ax-nul 4396  ax-pow 4442  ax-pr 4503  ax-un 6342  ax-cnex 9284  ax-resscn 9285  ax-1cn 9286  ax-icn 9287  ax-addcl 9288  ax-addrcl 9289  ax-mulcl 9290  ax-mulrcl 9291  ax-mulcom 9292  ax-addass 9293  ax-mulass 9294  ax-distr 9295  ax-i2m1 9296  ax-1ne0 9297  ax-1rid 9298  ax-rnegex 9299  ax-rrecex 9300  ax-cnre 9301  ax-pre-lttri 9302  ax-pre-lttrn 9303  ax-pre-ltadd 9304  ax-pre-mulgt0 9305
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3or 951  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-eu 2248  df-mo 2249  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-ne 2587  df-nel 2588  df-ral 2699  df-rex 2700  df-reu 2701  df-rmo 2702  df-rab 2703  df-v 2953  df-sbc 3165  df-csb 3266  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-pss 3321  df-nul 3615  df-if 3769  df-pw 3839  df-sn 3859  df-pr 3860  df-tp 3861  df-op 3862  df-uni 4067  df-iun 4148  df-br 4268  df-opab 4326  df-mpt 4327  df-tr 4361  df-eprel 4603  df-id 4607  df-po 4612  df-so 4613  df-fr 4650  df-we 4652  df-ord 4693  df-on 4694  df-lim 4695  df-suc 4696  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5353  df-fun 5392  df-fn 5393  df-f 5394  df-f1 5395  df-fo 5396  df-f1o 5397  df-fv 5398  df-riota 6020  df-ov 6064  df-oprab 6065  df-mpt2 6066  df-om 6447  df-1st 6546  df-2nd 6547  df-recs 6791  df-rdg 6825  df-er 7062  df-en 7270  df-dom 7271  df-sdom 7272  df-pnf 9366  df-mnf 9367  df-xr 9368  df-ltxr 9369  df-le 9370  df-sub 9543  df-neg 9544  df-div 9940  df-nn 10269  df-2 10326  df-3 10327  df-n0 10526  df-z 10592  df-uz 10807  df-rp 10937  df-fz 11382  df-fzo 11490  df-seq 11748  df-exp 11807
  Copyright terms: Public domain W3C validator