![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > addid1i | Structured version Visualization version GIF version |
Description: 0 is an additive identity. (Contributed by NM, 23-Nov-1994.) (Revised by Scott Fenton, 3-Jan-2013.) |
Ref | Expression |
---|---|
mul.1 | ⊢ 𝐴 ∈ ℂ |
Ref | Expression |
---|---|
addid1i | ⊢ (𝐴 + 0) = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mul.1 | . 2 ⊢ 𝐴 ∈ ℂ | |
2 | addid1 11332 | . 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 + 0) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 ∈ wcel 2106 (class class class)co 7354 ℂcc 11046 0cc0 11048 + caddc 11051 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5255 ax-nul 5262 ax-pow 5319 ax-pr 5383 ax-un 7669 ax-resscn 11105 ax-1cn 11106 ax-icn 11107 ax-addcl 11108 ax-addrcl 11109 ax-mulcl 11110 ax-mulrcl 11111 ax-mulcom 11112 ax-addass 11113 ax-mulass 11114 ax-distr 11115 ax-i2m1 11116 ax-1ne0 11117 ax-1rid 11118 ax-rnegex 11119 ax-rrecex 11120 ax-cnre 11121 ax-pre-lttri 11122 ax-pre-lttrn 11123 ax-pre-ltadd 11124 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3064 df-rex 3073 df-rab 3407 df-v 3446 df-sbc 3739 df-csb 3855 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-nul 4282 df-if 4486 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4865 df-br 5105 df-opab 5167 df-mpt 5188 df-id 5530 df-po 5544 df-so 5545 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-iota 6446 df-fun 6496 df-fn 6497 df-f 6498 df-f1 6499 df-fo 6500 df-f1o 6501 df-fv 6502 df-ov 7357 df-er 8645 df-en 8881 df-dom 8882 df-sdom 8883 df-pnf 11188 df-mnf 11189 df-ltxr 11191 |
This theorem is referenced by: 1p0e1 12274 9p1e10 12617 num0u 12626 numnncl2 12638 decrmanc 12672 decaddi 12675 decaddci 12676 decmul1 12679 decmulnc 12682 fsumrelem 15689 bpoly4 15939 demoivreALT 16080 decexp2 16944 decsplit0 16950 37prm 16990 43prm 16991 139prm 16993 163prm 16994 317prm 16995 631prm 16996 1259lem2 17001 1259lem3 17002 1259lem4 17003 1259lem5 17004 2503lem1 17006 2503lem2 17007 2503lem3 17008 4001lem1 17010 4001lem2 17011 4001lem3 17012 4001lem4 17013 sinhalfpilem 25816 efipi 25826 asin1 26240 log2ublem3 26294 log2ub 26295 emcllem6 26346 lgam1 26409 ip2i 29668 pythi 29690 normlem6 29955 normpythi 29982 normpari 29994 pjneli 30563 dp20u 31629 1mhdrd 31667 ballotth 33028 hgt750lemd 33152 hgt750lem2 33156 420gcd8e4 40452 60lcm7e420 40456 420lcm8e840 40457 3lexlogpow5ineq1 40500 3lexlogpow5ineq5 40506 dirkertrigeqlem3 44311 fourierdlem103 44420 fourierdlem104 44421 fouriersw 44442 257prm 45723 fmtno4nprmfac193 45736 fmtno5faclem3 45743 fmtno5fac 45744 139prmALT 45758 127prm 45761 m11nprm 45763 |
Copyright terms: Public domain | W3C validator |