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 11767 | . 2 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (2 · 𝐴) = (𝐴 + 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 ∈ wcel 2110 (class class class)co 7150 ℂcc 10529 + caddc 10534 · cmul 10536 2c2 11686 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-resscn 10588 ax-1cn 10589 ax-icn 10590 ax-addcl 10591 ax-mulcl 10593 ax-mulcom 10595 ax-mulass 10597 ax-distr 10598 ax-1rid 10601 ax-cnre 10604 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3496 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4467 df-sn 4561 df-pr 4563 df-op 4567 df-uni 4832 df-br 5059 df-iota 6308 df-fv 6357 df-ov 7153 df-2 11694 |
This theorem is referenced by: 2t2e4 11795 nn0le2xi 11945 binom2i 13568 rddif 14694 abs3lemi 14764 iseraltlem2 15033 prmreclem6 16251 mod2xi 16399 numexp2x 16409 prmlem2 16447 iihalf2 23531 pcoass 23622 ovolunlem1a 24091 tangtx 25085 sinq34lt0t 25089 eff1o 25127 ang180lem2 25382 dvatan 25507 basellem2 25653 basellem5 25656 chtub 25782 bposlem9 25862 ex-dvds 28229 norm3lem 28920 normpari 28925 polid2i 28928 ballotth 31790 heiborlem6 35088 sqsumi 39160 dirkertrigeqlem1 42377 fourierdlem94 42479 fourierdlem102 42487 fourierdlem111 42496 fourierdlem112 42497 fourierdlem113 42498 fourierdlem114 42499 sqwvfoura 42507 sqwvfourb 42508 fouriersw 42510 fmtnorec3 43704 2t6m3t4e0 44390 zlmodzxzequa 44545 |
Copyright terms: Public domain | W3C validator |