Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  abelthlem2 Structured version   Unicode version

Theorem abelthlem2 23379
 Description: Lemma for abelth 23388. The peculiar region , known as a Stolz angle , is a teardrop-shaped subset of the closed unit ball containing . Indeed, except for itself, the rest of the Stolz angle is enclosed in the open unit ball. (Contributed by Mario Carneiro, 31-Mar-2015.)
Hypotheses
Ref Expression
abelth.1
abelth.2
abelth.3
abelth.4
abelth.5
Assertion
Ref Expression
abelthlem2
Distinct variable groups:   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem abelthlem2
StepHypRef Expression
1 abelth.3 . 2
2 abelth.4 . 2
3 1cnd 9661 . . . 4
4 0le0 10701 . . . . 5
5 simpl 459 . . . . . . 7
65recnd 9671 . . . . . 6
76mul01d 9834 . . . . 5
84, 7syl5breqr 4458 . . . 4
9 oveq2 6311 . . . . . . . 8
10 1m1e0 10680 . . . . . . . 8
119, 10syl6eq 2480 . . . . . . 7
1211abs00bd 13348 . . . . . 6
13 fveq2 5879 . . . . . . . . . 10
14 abs1 13354 . . . . . . . . . 10
1513, 14syl6eq 2480 . . . . . . . . 9
1615oveq2d 6319 . . . . . . . 8
1716, 10syl6eq 2480 . . . . . . 7
1817oveq2d 6319 . . . . . 6
1912, 18breq12d 4434 . . . . 5
20 abelth.5 . . . . 5
2119, 20elrab2 3232 . . . 4
223, 8, 21sylanbrc 669 . . 3
23 elsn 4011 . . . . . . . . . 10
2423necon3bbii 2686 . . . . . . . . 9
25 simprll 771 . . . . . . . . . . . . . . 15
26 0cn 9637 . . . . . . . . . . . . . . 15
27 eqid 2423 . . . . . . . . . . . . . . . 16
2827cnmetdval 21783 . . . . . . . . . . . . . . 15
2925, 26, 28sylancl 667 . . . . . . . . . . . . . 14
3025subid1d 9977 . . . . . . . . . . . . . . 15
3130fveq2d 5883 . . . . . . . . . . . . . 14
3229, 31eqtrd 2464 . . . . . . . . . . . . 13
33 simprlr 772 . . . . . . . . . . . . . . . 16
34 ax-1cn 9599 . . . . . . . . . . . . . . . . . . 19
35 subcl 9876 . . . . . . . . . . . . . . . . . . 19
3634, 25, 35sylancr 668 . . . . . . . . . . . . . . . . . 18
3736abscld 13491 . . . . . . . . . . . . . . . . 17
38 simpll 759 . . . . . . . . . . . . . . . . . 18
39 1re 9644 . . . . . . . . . . . . . . . . . . 19
4025abscld 13491 . . . . . . . . . . . . . . . . . . 19
41 resubcl 9940 . . . . . . . . . . . . . . . . . . 19
4239, 40, 41sylancr 668 . . . . . . . . . . . . . . . . . 18
4338, 42remulcld 9673 . . . . . . . . . . . . . . . . 17
4437, 43lenltd 9783 . . . . . . . . . . . . . . . 16
4533, 44mpbid 214 . . . . . . . . . . . . . . 15
467adantr 467 . . . . . . . . . . . . . . . . . 18
47 simprr 765 . . . . . . . . . . . . . . . . . . . . 21
4847necomd 2696 . . . . . . . . . . . . . . . . . . . 20
49 subeq0 9902 . . . . . . . . . . . . . . . . . . . . . 22
5049necon3bid 2683 . . . . . . . . . . . . . . . . . . . . 21
5134, 25, 50sylancr 668 . . . . . . . . . . . . . . . . . . . 20
5248, 51mpbird 236 . . . . . . . . . . . . . . . . . . 19
53 absgt0 13381 . . . . . . . . . . . . . . . . . . . 20
5436, 53syl 17 . . . . . . . . . . . . . . . . . . 19
5552, 54mpbid 214 . . . . . . . . . . . . . . . . . 18
5646, 55eqbrtrd 4442 . . . . . . . . . . . . . . . . 17
57 oveq2 6311 . . . . . . . . . . . . . . . . . . . 20
5810, 57syl5eqr 2478 . . . . . . . . . . . . . . . . . . 19
5958oveq2d 6319 . . . . . . . . . . . . . . . . . 18
6059breq1d 4431 . . . . . . . . . . . . . . . . 17
6156, 60syl5ibcom 224 . . . . . . . . . . . . . . . 16
6261necon3bd 2637 . . . . . . . . . . . . . . 15
6345, 62mpd 15 . . . . . . . . . . . . . 14
64 1red 9660 . . . . . . . . . . . . . . 15
65 resubcl 9940 . . . . . . . . . . . . . . . . . . . . . 22
6640, 39, 65sylancl 667 . . . . . . . . . . . . . . . . . . . . 21
6714oveq2i 6314 . . . . . . . . . . . . . . . . . . . . . . 23
68 abs2dif 13389 . . . . . . . . . . . . . . . . . . . . . . . 24
6925, 34, 68sylancl 667 . . . . . . . . . . . . . . . . . . . . . . 23
7067, 69syl5eqbrr 4456 . . . . . . . . . . . . . . . . . . . . . 22
71 abssub 13383 . . . . . . . . . . . . . . . . . . . . . . 23
7225, 34, 71sylancl 667 . . . . . . . . . . . . . . . . . . . . . 22
7370, 72breqtrd 4446 . . . . . . . . . . . . . . . . . . . . 21
7466, 37, 43, 73, 33letrd 9794 . . . . . . . . . . . . . . . . . . . 20
7540, 64, 43lesubaddd 10212 . . . . . . . . . . . . . . . . . . . 20
7674, 75mpbid 214 . . . . . . . . . . . . . . . . . . 19
776adantr 467 . . . . . . . . . . . . . . . . . . . . 21
78 1cnd 9661 . . . . . . . . . . . . . . . . . . . . 21
7938, 40remulcld 9673 . . . . . . . . . . . . . . . . . . . . . 22
8079recnd 9671 . . . . . . . . . . . . . . . . . . . . 21
8177, 78, 80addsubd 10009 . . . . . . . . . . . . . . . . . . . 20
8240recnd 9671 . . . . . . . . . . . . . . . . . . . . . . 23
8377, 78, 82subdid 10076 . . . . . . . . . . . . . . . . . . . . . 22
8477mulid1d 9662 . . . . . . . . . . . . . . . . . . . . . . 23
8584oveq1d 6318 . . . . . . . . . . . . . . . . . . . . . 22
8683, 85eqtrd 2464 . . . . . . . . . . . . . . . . . . . . 21
8786oveq1d 6318 . . . . . . . . . . . . . . . . . . . 20
8881, 87eqtr4d 2467 . . . . . . . . . . . . . . . . . . 19
8976, 88breqtrrd 4448 . . . . . . . . . . . . . . . . . 18
90 peano2re 9808 . . . . . . . . . . . . . . . . . . . 20
9138, 90syl 17 . . . . . . . . . . . . . . . . . . 19
9279, 40, 91leaddsub2d 10217 . . . . . . . . . . . . . . . . . 18
9389, 92mpbird 236 . . . . . . . . . . . . . . . . 17
9477, 78, 82adddird 9670 . . . . . . . . . . . . . . . . . 18
9582mulid2d 9663 . . . . . . . . . . . . . . . . . . 19
9695oveq2d 6319 . . . . . . . . . . . . . . . . . 18
9794, 96eqtrd 2464 . . . . . . . . . . . . . . . . 17
9891recnd 9671 . . . . . . . . . . . . . . . . . 18
9998mulid1d 9662 . . . . . . . . . . . . . . . . 17
10093, 97, 993brtr4d 4452 . . . . . . . . . . . . . . . 16
101 0red 9646 . . . . . . . . . . . . . . . . . 18
102 simplr 761 . . . . . . . . . . . . . . . . . 18
10338ltp1d 10539 . . . . . . . . . . . . . . . . . 18
104101, 38, 91, 102, 103lelttrd 9795 . . . . . . . . . . . . . . . . 17
105 lemul2 10460 . . . . . . . . . . . . . . . . 17
10640, 64, 91, 104, 105syl112anc 1269 . . . . . . . . . . . . . . . 16
107100, 106mpbird 236 . . . . . . . . . . . . . . 15
10840, 64, 107leltned 9790 . . . . . . . . . . . . . 14
10963, 108mpbird 236 . . . . . . . . . . . . 13
11032, 109eqbrtrd 4442 . . . . . . . . . . . 12
111 cnxmet 21785 . . . . . . . . . . . . . 14
112 1rp 11308 . . . . . . . . . . . . . . 15
113 rpxr 11311 . . . . . . . . . . . . . . 15
114112, 113ax-mp 5 . . . . . . . . . . . . . 14
115 elbl3 21399 . . . . . . . . . . . . . 14
116111, 114, 115mpanl12 687 . . . . . . . . . . . . 13
11726, 25, 116sylancr 668 . . . . . . . . . . . 12
118110, 117mpbird 236 . . . . . . . . . . 11
119118expr 619 . . . . . . . . . 10
1201193impb 1202 . . . . . . . . 9
12124, 120syl5bi 221 . . . . . . . 8
122121orrd 380 . . . . . . 7
123 elun 3607 . . . . . . 7
124122, 123sylibr 216 . . . . . 6
125124rabssdv 3542 . . . . 5
12620, 125syl5eqss 3509 . . . 4
127 ssundif 3880 . . . 4
128126, 127sylib 200 . . 3
12922, 128jca 535 . 2
1301, 2, 129syl2anc 666 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 188   wo 370   wa 371   w3a 983   wceq 1438   wcel 1869   wne 2619  crab 2780   cdif 3434   cun 3435   wss 3437  csn 3997   class class class wbr 4421   cdm 4851   ccom 4855  wf 5595  cfv 5599  (class class class)co 6303  cc 9539  cr 9540  cc0 9541  c1 9542   caddc 9544   cmul 9546  cxr 9676   clt 9677   cle 9678   cmin 9862  cn0 10871  crp 11304   cseq 12214  cabs 13291   cli 13541  cxmt 18948  cbl 18950 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595  ax-cnex 9597  ax-resscn 9598  ax-1cn 9599  ax-icn 9600  ax-addcl 9601  ax-addrcl 9602  ax-mulcl 9603  ax-mulrcl 9604  ax-mulcom 9605  ax-addass 9606  ax-mulass 9607  ax-distr 9608  ax-i2m1 9609  ax-1ne0 9610  ax-1rid 9611  ax-rnegex 9612  ax-rrecex 9613  ax-cnre 9614  ax-pre-lttri 9615  ax-pre-lttrn 9616  ax-pre-ltadd 9617  ax-pre-mulgt0 9618  ax-pre-sup 9619 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-reu 2783  df-rmo 2784  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-tp 4002  df-op 4004  df-uni 4218  df-iun 4299  df-br 4422  df-opab 4481  df-mpt 4482  df-tr 4517  df-eprel 4762  df-id 4766  df-po 4772  df-so 4773  df-fr 4810  df-we 4812  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-pred 5397  df-ord 5443  df-on 5444  df-lim 5445  df-suc 5446  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-f1 5604  df-fo 5605  df-f1o 5606  df-fv 5607  df-riota 6265  df-ov 6306  df-oprab 6307  df-mpt2 6308  df-om 6705  df-1st 6805  df-2nd 6806  df-wrecs 7034  df-recs 7096  df-rdg 7134  df-er 7369  df-map 7480  df-en 7576  df-dom 7577  df-sdom 7578  df-sup 7960  df-pnf 9679  df-mnf 9680  df-xr 9681  df-ltxr 9682  df-le 9683  df-sub 9864  df-neg 9865  df-div 10272  df-nn 10612  df-2 10670  df-3 10671  df-n0 10872  df-z 10940  df-uz 11162  df-rp 11305  df-xadd 11412  df-seq 12215  df-exp 12274  df-cj 13156  df-re 13157  df-im 13158  df-sqrt 13292  df-abs 13293  df-psmet 18955  df-xmet 18956  df-met 18957  df-bl 18958 This theorem is referenced by:  abelthlem3  23380  abelthlem6  23383  abelthlem7  23385  abelthlem8  23386  abelthlem9  23387  abelth  23388
 Copyright terms: Public domain W3C validator