![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > negsubd | GIF version |
Description: Relationship between subtraction and negative. Theorem I.3 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
negidd.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
pncand.2 | ⊢ (𝜑 → 𝐵 ∈ ℂ) |
Ref | Expression |
---|---|
negsubd | ⊢ (𝜑 → (𝐴 + -𝐵) = (𝐴 − 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | negidd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | pncand.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℂ) | |
3 | negsub 7412 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵)) | |
4 | 1, 2, 3 | syl2anc 403 | 1 ⊢ (𝜑 → (𝐴 + -𝐵) = (𝐴 − 𝐵)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1285 ∈ wcel 1434 (class class class)co 5537 ℂcc 7030 + caddc 7035 − cmin 7335 -cneg 7336 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2064 ax-sep 3898 ax-pow 3950 ax-pr 3966 ax-setind 4282 ax-resscn 7119 ax-1cn 7120 ax-icn 7122 ax-addcl 7123 ax-addrcl 7124 ax-mulcl 7125 ax-addcom 7127 ax-addass 7129 ax-distr 7131 ax-i2m1 7132 ax-0id 7135 ax-rnegex 7136 ax-cnre 7138 |
This theorem depends on definitions: df-bi 115 df-3an 922 df-tru 1288 df-fal 1291 df-nf 1391 df-sb 1687 df-eu 1945 df-mo 1946 df-clab 2069 df-cleq 2075 df-clel 2078 df-nfc 2209 df-ne 2247 df-ral 2354 df-rex 2355 df-reu 2356 df-rab 2358 df-v 2604 df-sbc 2817 df-dif 2976 df-un 2978 df-in 2980 df-ss 2987 df-pw 3386 df-sn 3406 df-pr 3407 df-op 3409 df-uni 3604 df-br 3788 df-opab 3842 df-id 4050 df-xp 4371 df-rel 4372 df-cnv 4373 df-co 4374 df-dm 4375 df-iota 4891 df-fun 4928 df-fv 4934 df-riota 5493 df-ov 5540 df-oprab 5541 df-mpt2 5542 df-sub 7337 df-neg 7338 |
This theorem is referenced by: mulsub 7561 subap0d 7796 divsubdirap 7852 divsubdivap 7872 zaddcllemneg 8460 icoshftf1o 9078 fzosubel 9269 ceiqm1l 9382 modqcyc2 9431 qnegmod 9440 modqsub12d 9452 modsumfzodifsn 9467 expaddzaplem 9605 binom2sub 9673 cjreb 9880 recj 9881 remullem 9885 imcj 9889 resqrexlemover 10023 resqrexlemcalc1 10027 resqrexlemcalc3 10029 subcn2 10277 moddvds 10338 dvdsadd2b 10376 |
Copyright terms: Public domain | W3C validator |