|   | 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 12403 | . 2 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴)) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ (2 · 𝐴) = (𝐴 + 𝐴) | 
| Colors of variables: wff setvar class | 
| Syntax hints: = wceq 1539 ∈ wcel 2107 (class class class)co 7432 ℂcc 11154 + caddc 11159 · cmul 11161 2c2 12322 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 ax-resscn 11213 ax-1cn 11214 ax-icn 11215 ax-addcl 11216 ax-mulcl 11218 ax-mulcom 11220 ax-mulass 11222 ax-distr 11223 ax-1rid 11226 ax-cnre 11229 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-rex 3070 df-rab 3436 df-v 3481 df-dif 3953 df-un 3955 df-ss 3967 df-nul 4333 df-if 4525 df-sn 4626 df-pr 4628 df-op 4632 df-uni 4907 df-br 5143 df-iota 6513 df-fv 6568 df-ov 7435 df-2 12330 | 
| This theorem is referenced by: 2t2e4 12431 binom2i 14252 rddif 15380 abs3lemi 15450 iseraltlem2 15720 prmreclem6 16960 mod2xi 17108 numexp2x 17117 prmlem2 17158 iihalf2 24962 pcoass 25058 ovolunlem1a 25532 tangtx 26548 sinq34lt0t 26552 eff1o 26592 ang180lem2 26854 dvatan 26979 basellem2 27126 basellem5 27129 chtub 27257 bposlem9 27337 ex-dvds 30476 norm3lem 31169 normpari 31174 polid2i 31177 ballotth 34541 heiborlem6 37824 sqsumi 42321 dirkertrigeqlem1 46118 fourierdlem94 46220 fourierdlem102 46228 fourierdlem111 46237 fourierdlem112 46238 fourierdlem113 46239 fourierdlem114 46240 sqwvfoura 46248 sqwvfourb 46249 fouriersw 46251 fmtnorec3 47540 2t6m3t4e0 48269 zlmodzxzequa 48418 | 
| Copyright terms: Public domain | W3C validator |