negsubt - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem negsubt 5354

Description: Relationship between subtraction and negative. Theorem I.3 of [Apostol] p. 18.

**Assertion**
Ref	Expression
negsubt	⊢ ((A ∈ ℂ ⋀ B ∈ ℂ) → (A + -B) = (A − B))

**Proof of Theorem negsubt**
Step	Hyp	Ref	Expression
1		opreq1 3953	. . 3 ⊢ (A = if(A ∈ ℂ, A, 0) → (A + -B) = ( if(A ∈ ℂ, A, 0) + -B))
2		opreq1 3953	. . 3 ⊢ (A = if(A ∈ ℂ, A, 0) → (A − B) = ( if(A ∈ ℂ, A, 0) − B))
3	1, 2	eqeq12d 1481	. 2 ⊢ (A = if(A ∈ ℂ, A, 0) → ((A + -B) = (A − B) ↔ ( if(A ∈ ℂ, A, 0) + -B) = ( if(A ∈ ℂ, A, 0) − B)))
4		negeq 5331	. . . 4 ⊢ (B = if(B ∈ ℂ, B, 0) → -B = - if(B ∈ ℂ, B, 0))
5	4	opreq2d 3961	. . 3 ⊢ (B = if(B ∈ ℂ, B, 0) → ( if(A ∈ ℂ, A, 0) + -B) = ( if(A ∈ ℂ, A, 0) + - if(B ∈ ℂ, B, 0)))
6		opreq2 3954	. . 3 ⊢ (B = if(B ∈ ℂ, B, 0) → ( if(A ∈ ℂ, A, 0) − B) = ( if(A ∈ ℂ, A, 0) − if(B ∈ ℂ, B, 0)))
7	5, 6	eqeq12d 1481	. 2 ⊢ (B = if(B ∈ ℂ, B, 0) → (( if(A ∈ ℂ, A, 0) + -B) = ( if(A ∈ ℂ, A, 0) − B) ↔ ( if(A ∈ ℂ, A, 0) + - if(B ∈ ℂ, B, 0)) = ( if(A ∈ ℂ, A, 0) − if(B ∈ ℂ, B, 0))))
8		0cn 5300	. . . 4 ⊢ 0 ∈ ℂ
9	8	elimel 2384	. . 3 ⊢ if(A ∈ ℂ, A, 0) ∈ ℂ
10	8	elimel 2384	. . 3 ⊢ if(B ∈ ℂ, B, 0) ∈ ℂ
11	9, 10	negsub 5353	. 2 ⊢ ( if(A ∈ ℂ, A, 0) + - if(B ∈ ℂ, B, 0)) = ( if(A ∈ ℂ, A, 0) − if(B ∈ ℂ, B, 0))
12	3, 7, 11	dedth2h 2377	1 ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ) → (A + -B) = (A − B))

Colors of variables: wff set class

Syntax hints: → wi 3 ⋀ wa 223 = wceq 953 ∈ wcel 955 ifcif 2351 (class class class)co 3948 ℂcc 5204 0cc0 5206 + caddc 5209 − cmin 5264 -cneg 5265

This theorem is referenced by: addsubasst 5355 subnegt 5366 subcan2t 5374 subcant 5384 resubclt 5410 negdi2t 5428 negsubdit 5429 negsubdi2t 5430 submul2t 5432 subsub2t 5433 subsub4t 5436 nnncan1t 5439 addsub4t 5445 mulsubt 5449 pnncant 5452 lesub1t 5633 lesub2t 5634 ltsub1t 5635 ltsub2t 5636 subge0t 5647 divsubdirt 5731 zaddclt 6112 zsubclt 6115 zltp1let 6128 ceim1lt 6192 qsubclt 6210 icoshftf1oi 6342 fzsubelt 6433 seqzval2t 6485 resubt 6741 imsubt 6744 cjsubt 6751 recjt 6753 cjreimt 6763 cj11t 6765 absdifltt 6821 absdiflet 6822 fsumshftm 6970 climge0 7049 climsub 7066 clim2serzt 7070 clim2serz 7081 geolimilem 7170 efsubt 7313 efi4pt 7377 efmivalt 7390 sinsubt 7397 cossubt 7398 sincossqt 7403 demoivre 7426 vcsubdir 8112 cnnvm 8251 ipval2 8291 cnph 8409 ipasslem2 8422 ipsubdir 8439 shftefif1olem 8661 shftefif1olemOLD 8662 hvsubdistr2t 8838 his2subt 8879 lnfnsub 9890 mslb1 10473

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 959 ax-gen 960 ax-8 961 ax-9 962 ax-10 963 ax-11 964 ax-12 965 ax-13 966 ax-14 967 ax-17 968 ax-4 970 ax-5o 972 ax-6o 975 ax-9o 1119 ax-10o 1136 ax-16 1206 ax-11o 1213 ax-ext 1452 ax-rep 2683 ax-sep 2693 ax-nul 2700 ax-pow 2732 ax-pr 2769 ax-un 2857 ax-inf2 4597

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 774 df-3an 775 df-ex 978 df-sb 1168 df-eu 1375 df-mo 1376 df-clab 1457 df-cleq 1462 df-clel 1465 df-ne 1579 df-ral 1641 df-rex 1642 df-reu 1643 df-rab 1644 df-v 1803 df-sbc 1932 df-csb 1992 df-dif 2039 df-un 2040 df-in 2041 df-ss 2043 df-pss 2045 df-nul 2271 df-if 2352 df-pw 2392 df-sn 2402 df-pr 2403 df-tp 2405 df-op 2406 df-uni 2494 df-int 2524 df-iun 2558 df-br 2610 df-opab 2657 df-tr 2671 df-eprel 2821 df-id 2824 df-po 2831 df-so 2841 df-fr 2907 df-we 2924 df-ord 2941 df-on 2942 df-lim 2943 df-suc 2944 df-om 3122 df-xp 3174 df-rel 3175 df-cnv 3176 df-co 3177 df-dm 3178 df-rn 3179 df-res 3180 df-ima 3181 df-fun 3182 df-fn 3183 df-f 3184 df-fv 3188 df-rdg 3917 df-opr 3950 df-oprab 3951 df-1st 4063 df-2nd 4064 df-1o 4117 df-oadd 4119 df-omul 4120 df-er 4245 df-ec 4247 df-qs 4250 df-ni 4972 df-pli 4973 df-mi 4974 df-lti 4975 df-plpq 5007 df-mpq 5008 df-enq 5009 df-nq 5010 df-plq 5011 df-mq 5012 df-rq 5013 df-ltq 5014 df-1q 5015 df-np 5058 df-1p 5059 df-plp 5060 df-mp 5061 df-ltp 5062 df-plpr 5136 df-mpr 5137 df-enr 5138 df-nr 5139 df-plr 5140 df-mr 5141 df-0r 5143 df-1r 5144 df-m1r 5145 df-c 5212 df-0 5213 df-1 5214 df-i 5215 df-r 5216 df-plus 5217 df-mul 5218 df-sub 5328 df-neg 5330