![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > div23d | Structured version Visualization version GIF version |
Description: A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
div1d.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
divcld.2 | ⊢ (𝜑 → 𝐵 ∈ ℂ) |
divmuld.3 | ⊢ (𝜑 → 𝐶 ∈ ℂ) |
divassd.4 | ⊢ (𝜑 → 𝐶 ≠ 0) |
Ref | Expression |
---|---|
div23d | ⊢ (𝜑 → ((𝐴 · 𝐵) / 𝐶) = ((𝐴 / 𝐶) · 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | div1d.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | divcld.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℂ) | |
3 | divmuld.3 | . 2 ⊢ (𝜑 → 𝐶 ∈ ℂ) | |
4 | divassd.4 | . 2 ⊢ (𝜑 → 𝐶 ≠ 0) | |
5 | div23 11154 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 · 𝐵) / 𝐶) = ((𝐴 / 𝐶) · 𝐵)) | |
6 | 1, 2, 3, 4, 5 | syl112anc 1365 | 1 ⊢ (𝜑 → ((𝐴 · 𝐵) / 𝐶) = ((𝐴 / 𝐶) · 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1520 ∈ wcel 2079 ≠ wne 2982 (class class class)co 7007 ℂcc 10370 0cc0 10372 · cmul 10377 / cdiv 11134 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-13 2342 ax-ext 2767 ax-sep 5088 ax-nul 5095 ax-pow 5150 ax-pr 5214 ax-un 7310 ax-resscn 10429 ax-1cn 10430 ax-icn 10431 ax-addcl 10432 ax-addrcl 10433 ax-mulcl 10434 ax-mulrcl 10435 ax-mulcom 10436 ax-addass 10437 ax-mulass 10438 ax-distr 10439 ax-i2m1 10440 ax-1ne0 10441 ax-1rid 10442 ax-rnegex 10443 ax-rrecex 10444 ax-cnre 10445 ax-pre-lttri 10446 ax-pre-lttrn 10447 ax-pre-ltadd 10448 ax-pre-mulgt0 10449 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1079 df-3an 1080 df-tru 1523 df-ex 1760 df-nf 1764 df-sb 2041 df-mo 2574 df-eu 2610 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-ne 2983 df-nel 3089 df-ral 3108 df-rex 3109 df-reu 3110 df-rmo 3111 df-rab 3112 df-v 3434 df-sbc 3702 df-csb 3807 df-dif 3857 df-un 3859 df-in 3861 df-ss 3869 df-nul 4207 df-if 4376 df-pw 4449 df-sn 4467 df-pr 4469 df-op 4473 df-uni 4740 df-br 4957 df-opab 5019 df-mpt 5036 df-id 5340 df-po 5354 df-so 5355 df-xp 5441 df-rel 5442 df-cnv 5443 df-co 5444 df-dm 5445 df-rn 5446 df-res 5447 df-ima 5448 df-iota 6181 df-fun 6219 df-fn 6220 df-f 6221 df-f1 6222 df-fo 6223 df-f1o 6224 df-fv 6225 df-riota 6968 df-ov 7010 df-oprab 7011 df-mpo 7012 df-er 8130 df-en 8348 df-dom 8349 df-sdom 8350 df-pnf 10512 df-mnf 10513 df-xr 10514 df-ltxr 10515 df-le 10516 df-sub 10708 df-neg 10709 df-div 11135 |
This theorem is referenced by: bcpasc 13519 abslem2 14521 geolim 15047 bpolydiflem 15229 efaddlem 15267 eftlub 15283 bitsinv1lem 15611 pjthlem1 23711 itg2monolem3 24024 dvmulbr 24207 dvrecg 24241 dvmptdiv 24242 dvtaylp 24629 itgulm 24667 tanregt0 24792 logtayl2 24914 cxpeq 25007 heron 25085 dcubic2 25091 cubic2 25095 dquartlem1 25098 dquartlem2 25099 dquart 25100 quart1lem 25102 quart1 25103 dvatan 25182 atantayl 25184 jensenlem2 25235 lgamgulmlem2 25277 lgamgulmlem3 25278 ftalem2 25321 bclbnd 25526 bposlem9 25538 lgseisenlem4 25624 lgsquadlem1 25626 lgsquadlem2 25627 dchrvmasumlem1 25741 mulog2sumlem2 25781 2vmadivsumlem 25786 selberg3lem1 25803 selberg4lem1 25806 selberg4 25807 selberg3r 25815 pntrlog2bndlem4 25826 pntrlog2bndlem5 25827 pntibndlem2 25837 pntlemo 25853 brbtwn2 26362 colinearalg 26367 axsegconlem10 26383 axpaschlem 26397 axcontlem8 26428 pjhthlem1 28847 sinccvglem 32468 knoppndvlem14 33417 bj-bary1lem 34074 dvtan 34419 binomcxplemnotnn0 40178 dvnprodlem2 41727 itgsinexp 41735 stirlinglem3 41857 stirlinglem4 41858 dirkertrigeqlem3 41881 fourierdlem95 41982 eenglngeehlnmlem1 44159 eenglngeehlnmlem2 44160 |
Copyright terms: Public domain | W3C validator |