![]() |
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 12352 | . 2 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (2 · 𝐴) = (𝐴 + 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 ∈ wcel 2098 (class class class)co 7405 ℂcc 11110 + caddc 11115 · cmul 11117 2c2 12271 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2697 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-mulcl 11174 ax-mulcom 11176 ax-mulass 11178 ax-distr 11179 ax-1rid 11182 ax-cnre 11185 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2704 df-cleq 2718 df-clel 2804 df-rex 3065 df-rab 3427 df-v 3470 df-dif 3946 df-un 3948 df-in 3950 df-ss 3960 df-nul 4318 df-if 4524 df-sn 4624 df-pr 4626 df-op 4630 df-uni 4903 df-br 5142 df-iota 6489 df-fv 6545 df-ov 7408 df-2 12279 |
This theorem is referenced by: 2t2e4 12380 nn0le2xi 12530 binom2i 14181 rddif 15293 abs3lemi 15363 iseraltlem2 15635 prmreclem6 16863 mod2xi 17011 numexp2x 17021 prmlem2 17062 iihalf2 24810 pcoass 24906 ovolunlem1a 25380 tangtx 26395 sinq34lt0t 26399 eff1o 26438 ang180lem2 26697 dvatan 26822 basellem2 26969 basellem5 26972 chtub 27100 bposlem9 27180 ex-dvds 30218 norm3lem 30911 normpari 30916 polid2i 30919 ballotth 34066 heiborlem6 37197 sqsumi 41756 dirkertrigeqlem1 45391 fourierdlem94 45493 fourierdlem102 45501 fourierdlem111 45510 fourierdlem112 45511 fourierdlem113 45512 fourierdlem114 45513 sqwvfoura 45521 sqwvfourb 45522 fouriersw 45524 fmtnorec3 46793 2t6m3t4e0 47305 zlmodzxzequa 47457 |
Copyright terms: Public domain | W3C validator |