![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2times | Structured version Visualization version GIF version |
Description: Two times a number. (Contributed by NM, 10-Oct-2004.) (Revised by Mario Carneiro, 27-May-2016.) (Proof shortened by AV, 26-Feb-2020.) |
Ref | Expression |
---|---|
2times | ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-2 11496 | . . 3 ⊢ 2 = (1 + 1) | |
2 | 1 | oveq1i 6980 | . 2 ⊢ (2 · 𝐴) = ((1 + 1) · 𝐴) |
3 | 1p1times 10603 | . 2 ⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴)) | |
4 | 2, 3 | syl5eq 2820 | 1 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1507 ∈ wcel 2048 (class class class)co 6970 ℂcc 10325 1c1 10328 + caddc 10330 · cmul 10332 2c2 11488 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-ext 2745 ax-resscn 10384 ax-1cn 10385 ax-icn 10386 ax-addcl 10387 ax-mulcl 10389 ax-mulcom 10391 ax-mulass 10393 ax-distr 10394 ax-1rid 10397 ax-cnre 10400 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-clab 2754 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ral 3087 df-rex 3088 df-rab 3091 df-v 3411 df-dif 3828 df-un 3830 df-in 3832 df-ss 3839 df-nul 4174 df-if 4345 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4707 df-br 4924 df-iota 6146 df-fv 6190 df-ov 6973 df-2 11496 |
This theorem is referenced by: times2 11577 2timesi 11578 2txmxeqx 11580 2halves 11668 halfaddsub 11673 avglt2 11679 2timesd 11683 expubnd 13349 absmax 14540 sinmul 15375 sin2t 15380 cos2t 15381 sadadd2lem2 15649 pythagtriplem4 16002 pythagtriplem14 16011 pythagtriplem16 16013 2sqreultlem 25715 2sqreunnltlem 25718 cncph 28363 pellexlem2 38768 acongrep 38918 sub2times 40915 2timesgt 40929 |
Copyright terms: Public domain | W3C validator |