![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > divrec2d | Unicode version |
Description: Relationship between division and reciprocal. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
div1d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
divcld.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
divcld.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
divrec2d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | div1d.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | divcld.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | divcld.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | divrec2 9651 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 1, 2, 3, 4 | syl3anc 1184 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem is referenced by: expaddzlem 11378 rediv 11891 imdiv 11898 geo2sum 12605 efaddlem 12650 sinhval 12710 sca2rab 19361 itg2mulclem 19591 itg2mulc 19592 dvmptdivc 19804 dvexp3 19815 dvlip 19830 dvradcnv 20290 tanregt0 20394 logtayl 20504 cxpeq 20594 chordthmlem2 20627 chordthmlem4 20629 dquartlem1 20644 asinlem3 20664 asinsin 20685 efiatan2 20710 atantayl2 20731 amgmlem 20781 basellem8 20823 chebbnd1lem3 21118 dchrmusum2 21141 dchrvmasumlem3 21146 dchrisum0lem1 21163 selberg2lem 21197 logdivbnd 21203 pntrsumo1 21212 pntrlog2bndlem5 21228 pntibndlem2 21238 pntlemr 21249 pntlemo 21254 nmblolbii 22253 blocnilem 22258 nmbdoplbi 23480 nmcoplbi 23484 nmbdfnlbi 23505 nmcfnlbi 23508 clim2div 25170 dvreasin 26179 areacirclem2 26181 areacirclem5 26185 wallispi2lem1 27687 stirlinglem4 27693 stirlinglem5 27694 stirlinglem15 27704 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 |
This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-op 3783 df-uni 3976 df-br 4173 df-opab 4227 df-mpt 4228 df-id 4458 df-po 4463 df-so 4464 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-riota 6508 df-er 6864 df-en 7069 df-dom 7070 df-sdom 7071 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 |
Copyright terms: Public domain | W3C validator |