Mathbox for Alan Sare < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isosctrlem1ALT Structured version   Unicode version

Theorem isosctrlem1ALT 37305
 Description: Lemma for isosctr 23749. This proof was automatically derived by completeusersproof from its Virtual Deduction proof counterpart http://us.metamath.org/other/completeusersproof/isosctrlem1altvd.html. As it is verified by the Metamath program, isosctrlem1ALT 37305 verifies http://us.metamath.org/other/completeusersproof/isosctrlem1altvd.html. (Contributed by Alan Sare, 22-Apr-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
isosctrlem1ALT

Proof of Theorem isosctrlem1ALT
StepHypRef Expression
1 ax-1cn 9605 . . . . . . . 8
21a1i 11 . . . . . . 7
3 id 22 . . . . . . 7
42, 3subcld 9994 . . . . . 6
54adantr 466 . . . . 5
6 subeq0 9908 . . . . . . . . . . 11
76biimpd 210 . . . . . . . . . 10
87idiALT 36803 . . . . . . . . 9
91, 3, 8sylancr 667 . . . . . . . 8
109con3d 138 . . . . . . 7
11 df-ne 2616 . . . . . . . 8
1211biimpri 209 . . . . . . 7
1310, 12syl6 34 . . . . . 6
1413imp 430 . . . . 5
155, 14logcld 23519 . . . 4
1615imcld 13259 . . 3
17163adant2 1024 . 2
18 pire 23412 . . . . 5
19 2re 10687 . . . . 5
20 2ne0 10710 . . . . 5
2118, 19, 20redivcli 10382 . . . 4
2221a1i 11 . . 3
2318a1i 11 . . 3
24 neghalfpirx 23420 . . . 4
2521rexri 9701 . . . 4
263recld 13258 . . . . . . . . . 10
2726recnd 9677 . . . . . . . . 9
2827subidd 9982 . . . . . . . 8
2928adantr 466 . . . . . . 7
30 1re 9650 . . . . . . . . . 10
3130a1i 11 . . . . . . . . 9
321, 31ax-mp 5 . . . . . . . 8
333releabsd 13513 . . . . . . . . . 10
3433adantr 466 . . . . . . . . 9
35 id 22 . . . . . . . . . 10
3635adantl 467 . . . . . . . . 9
3734, 36breqtrd 4448 . . . . . . . 8
38 lesub1 10116 . . . . . . . . . 10
39383impcombi 37178 . . . . . . . . 9
4039idiALT 36803 . . . . . . . 8
4132, 26, 37, 40eel0121 37063 . . . . . . 7
4229, 41eqbrtrrd 4446 . . . . . 6
4332a1i 11 . . . . . . . . . . 11
4443rered 13288 . . . . . . . . . 10
4544trud 1446 . . . . . . . . 9
46 oveq1 6313 . . . . . . . . . 10
4746eqcomd 2430 . . . . . . . . 9
4845, 47ax-mp 5 . . . . . . . 8
49 resub 13191 . . . . . . . . . . 11
5049eqcomd 2430 . . . . . . . . . 10
5150idiALT 36803 . . . . . . . . 9
521, 3, 51sylancr 667 . . . . . . . 8
5348, 52syl5eq 2475 . . . . . . 7
5453adantr 466 . . . . . 6
5542, 54breqtrd 4448 . . . . 5
56 argrege0 23559 . . . . . . 7
57563coml 1212 . . . . . 6
58573com13 1210 . . . . 5
594, 55, 14, 58eel12131 37071 . . . 4
60 iccleub 11698 . . . 4
6124, 25, 59, 60eel001 37066 . . 3
62 pipos 23414 . . . . . 6
6318, 62elrpii 11313 . . . . 5
64 rphalflt 11337 . . . . 5
6563, 64ax-mp 5 . . . 4
6665a1i 11 . . 3
6717, 22, 23, 61, 66lelttrd 9801 . 2
6817, 67ltned 9779 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wa 370   w3a 982   wceq 1437   wtru 1438   wcel 1872   wne 2614   class class class wbr 4423  cfv 5601  (class class class)co 6306  cc 9545  cr 9546  cc0 9547  c1 9548  cxr 9682   clt 9683   cle 9684   cmin 9868  cneg 9869   cdiv 10277  c2 10667  crp 11310  cicc 11646  cre 13161  cim 13162  cabs 13298  cpi 14119  clog 23503 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 2057  ax-ext 2401  ax-rep 4536  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6598  ax-inf2 8156  ax-cnex 9603  ax-resscn 9604  ax-1cn 9605  ax-icn 9606  ax-addcl 9607  ax-addrcl 9608  ax-mulcl 9609  ax-mulrcl 9610  ax-mulcom 9611  ax-addass 9612  ax-mulass 9613  ax-distr 9614  ax-i2m1 9615  ax-1ne0 9616  ax-1rid 9617  ax-rnegex 9618  ax-rrecex 9619  ax-cnre 9620  ax-pre-lttri 9621  ax-pre-lttrn 9622  ax-pre-ltadd 9623  ax-pre-mulgt0 9624  ax-pre-sup 9625  ax-addf 9626  ax-mulf 9627 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rmo 2779  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-int 4256  df-iun 4301  df-iin 4302  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-se 4813  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6268  df-ov 6309  df-oprab 6310  df-mpt2 6311  df-of 6546  df-om 6708  df-1st 6808  df-2nd 6809  df-supp 6927  df-wrecs 7040  df-recs 7102  df-rdg 7140  df-1o 7194  df-2o 7195  df-oadd 7198  df-er 7375  df-map 7486  df-pm 7487  df-ixp 7535  df-en 7582  df-dom 7583  df-sdom 7584  df-fin 7585  df-fsupp 7894  df-fi 7935  df-sup 7966  df-inf 7967  df-oi 8035  df-card 8382  df-cda 8606  df-pnf 9685  df-mnf 9686  df-xr 9687  df-ltxr 9688  df-le 9689  df-sub 9870  df-neg 9871  df-div 10278  df-nn 10618  df-2 10676  df-3 10677  df-4 10678  df-5 10679  df-6 10680  df-7 10681  df-8 10682  df-9 10683  df-10 10684  df-n0 10878  df-z 10946  df-dec 11060  df-uz 11168  df-q 11273  df-rp 11311  df-xneg 11417  df-xadd 11418  df-xmul 11419  df-ioo 11647  df-ioc 11648  df-ico 11649  df-icc 11650  df-fz 11793  df-fzo 11924  df-fl 12035  df-mod 12104  df-seq 12221  df-exp 12280  df-fac 12467  df-bc 12495  df-hash 12523  df-shft 13131  df-cj 13163  df-re 13164  df-im 13165  df-sqrt 13299  df-abs 13300  df-limsup 13526  df-clim 13552  df-rlim 13553  df-sum 13753  df-ef 14121  df-sin 14123  df-cos 14124  df-pi 14126  df-struct 15123  df-ndx 15124  df-slot 15125  df-base 15126  df-sets 15127  df-ress 15128  df-plusg 15203  df-mulr 15204  df-starv 15205  df-sca 15206  df-vsca 15207  df-ip 15208  df-tset 15209  df-ple 15210  df-ds 15212  df-unif 15213  df-hom 15214  df-cco 15215  df-rest 15321  df-topn 15322  df-0g 15340  df-gsum 15341  df-topgen 15342  df-pt 15343  df-prds 15346  df-xrs 15400  df-qtop 15406  df-imas 15407  df-xps 15410  df-mre 15492  df-mrc 15493  df-acs 15495  df-mgm 16488  df-sgrp 16527  df-mnd 16537  df-submnd 16583  df-mulg 16676  df-cntz 16971  df-cmn 17432  df-psmet 18962  df-xmet 18963  df-met 18964  df-bl 18965  df-mopn 18966  df-fbas 18967  df-fg 18968  df-cnfld 18971  df-top 19920  df-bases 19921  df-topon 19922  df-topsp 19923  df-cld 20033  df-ntr 20034  df-cls 20035  df-nei 20113  df-lp 20151  df-perf 20152  df-cn 20242  df-cnp 20243  df-haus 20330  df-tx 20576  df-hmeo 20769  df-fil 20860  df-fm 20952  df-flim 20953  df-flf 20954  df-xms 21334  df-ms 21335  df-tms 21336  df-cncf 21909  df-limc 22820  df-dv 22821  df-log 23505 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator