| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > divmuld | Structured version Visualization version GIF version | ||
| Description: Relationship between division and multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
| Ref | Expression |
|---|---|
| div1d.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
| divcld.2 | ⊢ (𝜑 → 𝐵 ∈ ℂ) |
| divmuld.3 | ⊢ (𝜑 → 𝐶 ∈ ℂ) |
| divmuld.4 | ⊢ (𝜑 → 𝐵 ≠ 0) |
| Ref | Expression |
|---|---|
| divmuld | ⊢ (𝜑 → ((𝐴 / 𝐵) = 𝐶 ↔ (𝐵 · 𝐶) = 𝐴)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | div1d.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
| 2 | divmuld.3 | . 2 ⊢ (𝜑 → 𝐶 ∈ ℂ) | |
| 3 | divcld.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℂ) | |
| 4 | divmuld.4 | . 2 ⊢ (𝜑 → 𝐵 ≠ 0) | |
| 5 | divmul 11863 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → ((𝐴 / 𝐵) = 𝐶 ↔ (𝐵 · 𝐶) = 𝐴)) | |
| 6 | 1, 2, 3, 4, 5 | syl112anc 1397 | 1 ⊢ (𝜑 → ((𝐴 / 𝐵) = 𝐶 ↔ (𝐵 · 𝐶) = 𝐴)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 209 = wceq 1563 ∈ wcel 2145 ≠ wne 2960 (class class class)co 7400 ℂcc 11086 0cc0 11088 · cmul 11093 / cdiv 11859 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-sep 5250 ax-nul 5260 ax-pow 5326 ax-pr 5394 ax-un 7722 ax-resscn 11145 ax-1cn 11146 ax-icn 11147 ax-addcl 11148 ax-addrcl 11149 ax-mulcl 11150 ax-mulrcl 11151 ax-mulcom 11152 ax-addass 11153 ax-mulass 11154 ax-distr 11155 ax-i2m1 11156 ax-1ne0 11157 ax-1rid 11158 ax-rnegex 11159 ax-rrecex 11160 ax-cnre 11161 ax-pre-lttri 11162 ax-pre-lttrn 11163 ax-pre-ltadd 11164 ax-pre-mulgt0 11165 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-br 5105 df-opab 5167 df-mpt 5186 df-id 5546 df-po 5559 df-so 5560 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-er 8682 df-en 8932 df-dom 8933 df-sdom 8934 df-pnf 11233 df-mnf 11234 df-xr 11235 df-ltxr 11236 df-le 11237 df-sub 11431 df-neg 11432 df-div 11860 |
| This theorem is referenced by: nndiv 12270 recval 15362 clim2div 15931 sinadd 16208 tanaddlem 16210 pc2dvds 16927 odmulgeq 19615 zringunit 21573 prmirredlem 21579 nrginvrcnlem 24805 i1fmulclem 25818 itg1mulc 25820 mvth 26108 efopn 26777 cxpeq 26876 ang180lem3 26930 quad2 26958 asinneg 27005 dvdsflf1o 27305 muinv 27311 brbtwn2 29160 colinearalg 29165 axeuclidlem 29217 axcontlem8 29226 qdiff 37826 lcmineqlem10 42662 3lexlogpow5ineq5 42684 aks6d1c2 42754 unitscyglem4 42822 qirropth 43492 binomcxplemfrat 44920 binomcxplemnotnn0 44925 fourierswlem 46803 eenglngeehlnmlem1 49369 eenglngeehlnmlem2 49370 line2x 49386 |
| Copyright terms: Public domain | W3C validator |