![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > divdiv1 | Structured version Visualization version GIF version |
Description: Division into a fraction. (Contributed by NM, 31-Dec-2007.) |
Ref | Expression |
---|---|
divdiv1 | ⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐵) / 𝐶) = (𝐴 / (𝐵 · 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1cn 10282 | . . . . 5 ⊢ 1 ∈ ℂ | |
2 | ax-1ne0 10293 | . . . . 5 ⊢ 1 ≠ 0 | |
3 | 1, 2 | pm3.2i 463 | . . . 4 ⊢ (1 ∈ ℂ ∧ 1 ≠ 0) |
4 | divdivdiv 11018 | . . . 4 ⊢ (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (1 ∈ ℂ ∧ 1 ≠ 0))) → ((𝐴 / 𝐵) / (𝐶 / 1)) = ((𝐴 · 1) / (𝐵 · 𝐶))) | |
5 | 3, 4 | mpanr2 696 | . . 3 ⊢ (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐵) / (𝐶 / 1)) = ((𝐴 · 1) / (𝐵 · 𝐶))) |
6 | 5 | 3impa 1137 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐵) / (𝐶 / 1)) = ((𝐴 · 1) / (𝐵 · 𝐶))) |
7 | div1 11008 | . . . . 5 ⊢ (𝐶 ∈ ℂ → (𝐶 / 1) = 𝐶) | |
8 | 7 | oveq2d 6894 | . . . 4 ⊢ (𝐶 ∈ ℂ → ((𝐴 / 𝐵) / (𝐶 / 1)) = ((𝐴 / 𝐵) / 𝐶)) |
9 | 8 | ad2antrl 720 | . . 3 ⊢ (((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐵) / (𝐶 / 1)) = ((𝐴 / 𝐵) / 𝐶)) |
10 | 9 | 3adant1 1161 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐵) / (𝐶 / 1)) = ((𝐴 / 𝐵) / 𝐶)) |
11 | mulid1 10326 | . . . 4 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴) | |
12 | 11 | oveq1d 6893 | . . 3 ⊢ (𝐴 ∈ ℂ → ((𝐴 · 1) / (𝐵 · 𝐶)) = (𝐴 / (𝐵 · 𝐶))) |
13 | 12 | 3ad2ant1 1164 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 · 1) / (𝐵 · 𝐶)) = (𝐴 / (𝐵 · 𝐶))) |
14 | 6, 10, 13 | 3eqtr3d 2841 | 1 ⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐵) / 𝐶) = (𝐴 / (𝐵 · 𝐶))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 ∧ w3a 1108 = wceq 1653 ∈ wcel 2157 ≠ wne 2971 (class class class)co 6878 ℂcc 10222 0cc0 10224 1c1 10225 · cmul 10229 / cdiv 10976 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 ax-sep 4975 ax-nul 4983 ax-pow 5035 ax-pr 5097 ax-un 7183 ax-resscn 10281 ax-1cn 10282 ax-icn 10283 ax-addcl 10284 ax-addrcl 10285 ax-mulcl 10286 ax-mulrcl 10287 ax-mulcom 10288 ax-addass 10289 ax-mulass 10290 ax-distr 10291 ax-i2m1 10292 ax-1ne0 10293 ax-1rid 10294 ax-rnegex 10295 ax-rrecex 10296 ax-cnre 10297 ax-pre-lttri 10298 ax-pre-lttrn 10299 ax-pre-ltadd 10300 ax-pre-mulgt0 10301 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3or 1109 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ne 2972 df-nel 3075 df-ral 3094 df-rex 3095 df-reu 3096 df-rmo 3097 df-rab 3098 df-v 3387 df-sbc 3634 df-csb 3729 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-nul 4116 df-if 4278 df-pw 4351 df-sn 4369 df-pr 4371 df-op 4375 df-uni 4629 df-br 4844 df-opab 4906 df-mpt 4923 df-id 5220 df-po 5233 df-so 5234 df-xp 5318 df-rel 5319 df-cnv 5320 df-co 5321 df-dm 5322 df-rn 5323 df-res 5324 df-ima 5325 df-iota 6064 df-fun 6103 df-fn 6104 df-f 6105 df-f1 6106 df-fo 6107 df-f1o 6108 df-fv 6109 df-riota 6839 df-ov 6881 df-oprab 6882 df-mpt2 6883 df-er 7982 df-en 8196 df-dom 8197 df-sdom 8198 df-pnf 10365 df-mnf 10366 df-xr 10367 df-ltxr 10368 df-le 10369 df-sub 10558 df-neg 10559 df-div 10977 |
This theorem is referenced by: recdiv2 11030 divdiv1d 11124 fldiv4lem1div2uz2 12892 fldiv2 12915 sin01bnd 15251 flodddiv4t2lthalf 15475 pythagtriplem12 15864 pythagtriplem14 15866 pythagtriplem16 15868 coseq1 24616 efeq1 24617 ang180lem1 24891 atan1 25007 fsumdvdscom 25263 bposlem8 25368 gausslemma2dlem3 25445 2lgslem1a2 25467 rplogsumlem2 25526 dchrvmasum2lem 25537 dchrisum0lem2 25559 dchrisum0lem3 25560 mulogsum 25573 mulog2sumlem2 25576 pntlemr 25643 pntlemf 25646 hgt750lem 31249 quad3 32079 wallispilem4 41028 dirkertrigeqlem3 41060 dirkercncflem1 41063 fourierswlem 41190 dignn0flhalflem2 43209 dignn0ehalf 43210 |
Copyright terms: Public domain | W3C validator |