Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mul01 | Structured version Visualization version GIF version |
Description: Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by NM, 15-May-1999.) (Revised by Scott Fenton, 3-Jan-2013.) |
Ref | Expression |
---|---|
mul01 | ⊢ (𝐴 ∈ ℂ → (𝐴 · 0) = 0) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0cn 10712 | . . 3 ⊢ 0 ∈ ℂ | |
2 | mulcom 10702 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → (𝐴 · 0) = (0 · 𝐴)) | |
3 | 1, 2 | mpan2 691 | . 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 0) = (0 · 𝐴)) |
4 | mul02 10897 | . 2 ⊢ (𝐴 ∈ ℂ → (0 · 𝐴) = 0) | |
5 | 3, 4 | eqtrd 2773 | 1 ⊢ (𝐴 ∈ ℂ → (𝐴 · 0) = 0) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2113 (class class class)co 7171 ℂcc 10614 0cc0 10616 · cmul 10621 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-sep 5168 ax-nul 5175 ax-pow 5233 ax-pr 5297 ax-un 7480 ax-resscn 10673 ax-1cn 10674 ax-icn 10675 ax-addcl 10676 ax-addrcl 10677 ax-mulcl 10678 ax-mulrcl 10679 ax-mulcom 10680 ax-addass 10681 ax-mulass 10682 ax-distr 10683 ax-i2m1 10684 ax-1ne0 10685 ax-1rid 10686 ax-rnegex 10687 ax-rrecex 10688 ax-cnre 10689 ax-pre-lttri 10690 ax-pre-lttrn 10691 ax-pre-ltadd 10692 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-nel 3039 df-ral 3058 df-rex 3059 df-rab 3062 df-v 3400 df-sbc 3683 df-csb 3792 df-dif 3847 df-un 3849 df-in 3851 df-ss 3861 df-nul 4213 df-if 4416 df-pw 4491 df-sn 4518 df-pr 4520 df-op 4524 df-uni 4798 df-br 5032 df-opab 5094 df-mpt 5112 df-id 5430 df-po 5443 df-so 5444 df-xp 5532 df-rel 5533 df-cnv 5534 df-co 5535 df-dm 5536 df-rn 5537 df-res 5538 df-ima 5539 df-iota 6298 df-fun 6342 df-fn 6343 df-f 6344 df-f1 6345 df-fo 6346 df-f1o 6347 df-fv 6348 df-ov 7174 df-er 8321 df-en 8557 df-dom 8558 df-sdom 8559 df-pnf 10756 df-mnf 10757 df-ltxr 10759 |
This theorem is referenced by: addid1 10899 cnegex 10900 mul01i 10909 mul01d 10918 bernneq 13683 bcval5 13771 geo2lim 15324 efexp 15547 gcdmultiplezOLD 15998 plymul0or 25029 fta1lem 25055 1cxp 25415 cxpmul2 25432 efrlim 25707 lgsne0 26071 vcz 28510 blocnilem 28739 hvmul0 28959 ocsh 29218 0lnfn 29920 nlelshi 29995 0even 45015 2zrngamgm 45023 |
Copyright terms: Public domain | W3C validator |