subdit - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem subdit 5407

Description: Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18.

**Assertion**
Ref	Expression
subdit	⊢ ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℂ) → (A · (B − C)) = ((A · B) − (A · C)))

**Proof of Theorem subdit**
Step	Hyp	Ref	Expression
1		axdistr 5259	. . . . 5 ⊢ ((A ∈ ℂ ⋀ C ∈ ℂ ⋀ (B − C) ∈ ℂ) → (A · (C + (B − C))) = ((A · C) + (A · (B − C))))
2		3simp1 787	. . . . 5 ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℂ) → A ∈ ℂ)
3		3simp3 789	. . . . 5 ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℂ) → C ∈ ℂ)
4		subclt 5347	. . . . . 6 ⊢ ((B ∈ ℂ ⋀ C ∈ ℂ) → (B − C) ∈ ℂ)
5	4	3adant1 796	. . . . 5 ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℂ) → (B − C) ∈ ℂ)
6	1, 2, 3, 5	syl3anc 857	. . . 4 ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℂ) → (A · (C + (B − C))) = ((A · C) + (A · (B − C))))
7		pncan3t 5357	. . . . . . 7 ⊢ ((C ∈ ℂ ⋀ B ∈ ℂ) → (C + (B − C)) = B)
8	7	ancoms 436	. . . . . 6 ⊢ ((B ∈ ℂ ⋀ C ∈ ℂ) → (C + (B − C)) = B)
9	8	3adant1 796	. . . . 5 ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℂ) → (C + (B − C)) = B)
10	9	opreq2d 3967	. . . 4 ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℂ) → (A · (C + (B − C))) = (A · B))
11	6, 10	eqtr3d 1506	. . 3 ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℂ) → ((A · C) + (A · (B − C))) = (A · B))
12		subaddt 5355	. . . 4 ⊢ (((A · B) ∈ ℂ ⋀ (A · C) ∈ ℂ ⋀ (A · (B − C)) ∈ ℂ) → (((A · B) − (A · C)) = (A · (B − C)) ↔ ((A · C) + (A · (B − C))) = (A · B)))
13		axmulcl 5253	. . . . 5 ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ) → (A · B) ∈ ℂ)
14	13	3adant3 798	. . . 4 ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℂ) → (A · B) ∈ ℂ)
15		axmulcl 5253	. . . . 5 ⊢ ((A ∈ ℂ ⋀ C ∈ ℂ) → (A · C) ∈ ℂ)
16	15	3adant2 797	. . . 4 ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℂ) → (A · C) ∈ ℂ)
17		axmulcl 5253	. . . . . 6 ⊢ ((A ∈ ℂ ⋀ (B − C) ∈ ℂ) → (A · (B − C)) ∈ ℂ)
18	17, 4	sylan2 451	. . . . 5 ⊢ ((A ∈ ℂ ⋀ (B ∈ ℂ ⋀ C ∈ ℂ)) → (A · (B − C)) ∈ ℂ)
19	18	3impb 828	. . . 4 ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℂ) → (A · (B − C)) ∈ ℂ)
20	12, 14, 16, 19	syl3anc 857	. . 3 ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℂ) → (((A · B) − (A · C)) = (A · (B − C)) ↔ ((A · C) + (A · (B − C))) = (A · B)))
21	11, 20	mpbird 196	. 2 ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℂ) → ((A · B) − (A · C)) = (A · (B − C)))
22	21	eqcomd 1477	1 ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℂ) → (A · (B − C)) = ((A · B) − (A · C)))

Colors of variables: wff set class

Syntax hints: → wi 3 ↔ wb 146 ⋀ wa 223 ⋀ w3a 774 = wceq 954 ∈ wcel 956 (class class class)co 3954 ℂcc 5212 + caddc 5217 · cmul 5219 − cmin 5272

This theorem is referenced by: subdirt 5408 subdi 5409 recextlem1 5663 qbtwnre 6224 expubndt 6547 subsqt 6581 climmullem5 7068 geoser 7177 mulc1cncf 7222 cos01bndlem3 7421 ipval2 8304 minveclem27 8515 2wsms 10510

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 960 ax-gen 961 ax-8 962 ax-9 963 ax-10 964 ax-11 965 ax-12 966 ax-13 967 ax-14 968 ax-17 969 ax-4 971 ax-5o 973 ax-6o 976 ax-9o 1121 ax-10o 1138 ax-16 1208 ax-11o 1216 ax-ext 1457 ax-rep 2688 ax-sep 2698 ax-nul 2705 ax-pow 2737 ax-pr 2774 ax-un 2861 ax-inf2 4605

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 775 df-3an 776 df-ex 979 df-sb 1170 df-eu 1380 df-mo 1381 df-clab 1462 df-cleq 1467 df-clel 1470 df-ne 1584 df-ral 1646 df-rex 1647 df-reu 1648 df-rab 1649 df-v 1808 df-sbc 1938 df-csb 1998 df-dif 2045 df-un 2046 df-in 2047 df-ss 2049 df-pss 2051 df-nul 2277 df-if 2358 df-pw 2398 df-sn 2408 df-pr 2409 df-tp 2411 df-op 2412 df-uni 2499 df-int 2529 df-iun 2563 df-br 2615 df-opab 2662 df-tr 2676 df-eprel 2827 df-id 2830 df-po 2835 df-so 2845 df-fr 2912 df-we 2929 df-ord 2946 df-on 2947 df-lim 2948 df-suc 2949 df-om 3127 df-xp 3179 df-rel 3180 df-cnv 3181 df-co 3182 df-dm 3183 df-rn 3184 df-res 3185 df-ima 3186 df-fun 3187 df-fn 3188 df-f 3189 df-fv 3193 df-rdg 3923 df-opr 3956 df-oprab 3957 df-1st 4069 df-2nd 4070 df-1o 4123 df-oadd 4125 df-omul 4126 df-er 4251 df-ec 4253 df-qs 4256 df-ni 4980 df-pli 4981 df-mi 4982 df-lti 4983 df-plpq 5015 df-mpq 5016 df-enq 5017 df-nq 5018 df-plq 5019 df-mq 5020 df-rq 5021 df-ltq 5022 df-1q 5023 df-np 5066 df-1p 5067 df-plp 5068 df-mp 5069 df-ltp 5070 df-plpr 5144 df-mpr 5145 df-enr 5146 df-nr 5147 df-plr 5148 df-mr 5149 df-0r 5151 df-1r 5152 df-m1r 5153 df-c 5220 df-0 5221 df-1 5222 df-i 5223 df-r 5224 df-plus 5225 df-mul 5226 df-sub 5336