![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2timesi | Structured version Visualization version GIF version |
Description: Two times a number. (Contributed by NM, 1-Aug-1999.) |
Ref | Expression |
---|---|
2timesi.1 | ⊢ 𝐴 ∈ ℂ |
Ref | Expression |
---|---|
2timesi | ⊢ (2 · 𝐴) = (𝐴 + 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2timesi.1 | . 2 ⊢ 𝐴 ∈ ℂ | |
2 | 2times 11494 | . 2 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (2 · 𝐴) = (𝐴 + 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1658 ∈ wcel 2166 (class class class)co 6905 ℂcc 10250 + caddc 10255 · cmul 10257 2c2 11406 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2803 ax-resscn 10309 ax-1cn 10310 ax-icn 10311 ax-addcl 10312 ax-mulcl 10314 ax-mulcom 10316 ax-mulass 10318 ax-distr 10319 ax-1rid 10322 ax-cnre 10325 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ral 3122 df-rex 3123 df-rab 3126 df-v 3416 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4145 df-if 4307 df-sn 4398 df-pr 4400 df-op 4404 df-uni 4659 df-br 4874 df-iota 6086 df-fv 6131 df-ov 6908 df-2 11414 |
This theorem is referenced by: 2t2e4 11522 nn0le2xi 11674 binom2i 13268 rddif 14457 abs3lemi 14526 iseraltlem2 14790 prmreclem6 15996 mod2xi 16144 numexp2x 16154 prmlem2 16192 iihalf2 23102 pcoass 23193 ovolunlem1a 23662 tangtx 24657 sinq34lt0t 24661 eff1o 24695 ang180lem2 24950 dvatan 25075 basellem2 25221 basellem5 25224 chtub 25350 bposlem9 25430 ex-dvds 27871 norm3lem 28561 normpari 28566 polid2i 28569 ballotth 31145 heiborlem6 34157 sqsumi 38056 dirkertrigeqlem1 41109 fourierdlem94 41211 fourierdlem102 41219 fourierdlem111 41228 fourierdlem112 41229 fourierdlem113 41230 fourierdlem114 41231 sqwvfoura 41239 sqwvfourb 41240 fouriersw 41242 fmtnorec3 42290 2t6m3t4e0 42973 zlmodzxzequa 43132 |
Copyright terms: Public domain | W3C validator |