divdir - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > divdir		Structured version Visualization version GIF version

Theorem divdir 11834

Description: Distribution of division over addition. (Contributed by NM, 31-Jul-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)

**Assertion**
Ref	Expression
divdir	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶)))

**Proof of Theorem divdir**
Step	Hyp	Ref	Expression
1		simp1 1137	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → 𝐴 ∈ ℂ)
2		simp2 1138	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → 𝐵 ∈ ℂ)
3		reccl 11816	. . . 4 ⊢ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) → (1 / 𝐶) ∈ ℂ)
4	3	3ad2ant3 1136	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → (1 / 𝐶) ∈ ℂ)
5	1, 2, 4	adddird 11170	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 + 𝐵) · (1 / 𝐶)) = ((𝐴 · (1 / 𝐶)) + (𝐵 · (1 / 𝐶))))
6	1, 2	addcld 11164	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → (𝐴 + 𝐵) ∈ ℂ)
7		simp3l 1203	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → 𝐶 ∈ ℂ)
8		simp3r 1204	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → 𝐶 ≠ 0)
9		divrec 11825	. . 3 ⊢ (((𝐴 + 𝐵) ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 + 𝐵) · (1 / 𝐶)))
10	6, 7, 8, 9	syl3anc 1374	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 + 𝐵) · (1 / 𝐶)))
11		divrec 11825	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) → (𝐴 / 𝐶) = (𝐴 · (1 / 𝐶)))
12	1, 7, 8, 11	syl3anc 1374	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → (𝐴 / 𝐶) = (𝐴 · (1 / 𝐶)))
13		divrec 11825	. . . 4 ⊢ ((𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) → (𝐵 / 𝐶) = (𝐵 · (1 / 𝐶)))
14	2, 7, 8, 13	syl3anc 1374	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → (𝐵 / 𝐶) = (𝐵 · (1 / 𝐶)))
15	12, 14	oveq12d 7385	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐶) + (𝐵 / 𝐶)) = ((𝐴 · (1 / 𝐶)) + (𝐵 · (1 / 𝐶))))
16	5, 10, 15	3eqtr4d 2781	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2932 (class class class)co 7367 ℂcc 11036 0cc0 11038 1c1 11039 + caddc 11041 · cmul 11043 / cdiv 11807

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-rmo 3342 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4851 df-br 5086 df-opab 5148 df-mpt 5167 df-id 5526 df-po 5539 df-so 5540 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-er 8643 df-en 8894 df-dom 8895 df-sdom 8896 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-div 11808

This theorem is referenced by: muldivdir 11847 divsubdir 11848 divadddiv 11870 divdirzi 11907 divdird 11969 2halves 12395 halfaddsub 12410 zdivadd 12600 nneo 12613 rpnnen1lem5 12931 2tnp1ge0ge0 13788 fldiv 13819 modcyc 13865 mulsubdivbinom2 14224 crim 15077 efival 16119 flodddiv4 16384 divgcdcoprm0 16634 pythagtriplem17 16802 ptolemy 26460 relogbmul 26741 harmonicbnd4 26974 ppiub 27167 logfacrlim 27187 bposlem9 27255 2lgslem3a 27359 2lgslem3b 27360 2lgslem3c 27361 2lgslem3d 27362 chpchtlim 27442 mudivsum 27493 selberglem2 27509 pntrsumo1 27528 pntibndlem2 27554 pntibndlem3 27555 pntlemb 27560 dpfrac1 32951 heiborlem6 38137 zofldiv2ALTV 48138 zofldiv2 49007 sinhpcosh 50215 onetansqsecsq 50236

W3C validator