![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3m1e2 | Structured version Visualization version GIF version |
Description: 3 - 1 = 2. (Contributed by FL, 17-Oct-2010.) (Revised by NM, 10-Dec-2017.) (Proof shortened by AV, 6-Sep-2021.) |
Ref | Expression |
---|---|
3m1e2 | ⊢ (3 − 1) = 2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2cn 11560 | . 2 ⊢ 2 ∈ ℂ | |
2 | ax-1cn 10441 | . 2 ⊢ 1 ∈ ℂ | |
3 | df-3 11549 | . 2 ⊢ 3 = (2 + 1) | |
4 | 1, 2, 3 | mvrraddi 10751 | 1 ⊢ (3 − 1) = 2 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1522 (class class class)co 7016 1c1 10384 − cmin 10717 2c2 11540 3c3 11541 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5094 ax-nul 5101 ax-pow 5157 ax-pr 5221 ax-un 7319 ax-resscn 10440 ax-1cn 10441 ax-icn 10442 ax-addcl 10443 ax-addrcl 10444 ax-mulcl 10445 ax-mulrcl 10446 ax-mulcom 10447 ax-addass 10448 ax-mulass 10449 ax-distr 10450 ax-i2m1 10451 ax-1ne0 10452 ax-1rid 10453 ax-rnegex 10454 ax-rrecex 10455 ax-cnre 10456 ax-pre-lttri 10457 ax-pre-lttrn 10458 ax-pre-ltadd 10459 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-nel 3091 df-ral 3110 df-rex 3111 df-reu 3112 df-rab 3114 df-v 3439 df-sbc 3707 df-csb 3812 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-pw 4455 df-sn 4473 df-pr 4475 df-op 4479 df-uni 4746 df-br 4963 df-opab 5025 df-mpt 5042 df-id 5348 df-po 5362 df-so 5363 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-rn 5454 df-res 5455 df-ima 5456 df-iota 6189 df-fun 6227 df-fn 6228 df-f 6229 df-f1 6230 df-fo 6231 df-f1o 6232 df-fv 6233 df-riota 6977 df-ov 7019 df-oprab 7020 df-mpo 7021 df-er 8139 df-en 8358 df-dom 8359 df-sdom 8360 df-pnf 10523 df-mnf 10524 df-ltxr 10526 df-sub 10719 df-2 11548 df-3 11549 |
This theorem is referenced by: halfpm6th 11706 ige3m2fz 12781 fzo13pr 12971 fzo0to3tp 12973 fldiv4p1lem1div2 13055 lsws3 14103 bpoly3 15245 rpnnen2lem3 15402 rpnnen2lem11 15410 n2dvds3OLD 15555 3prm 15867 prmo3 16206 1cubrlem 25100 1cubr 25101 quart1 25115 log2cnv 25204 log2ublem3 25208 2lgslem3b 25655 2lgslem3d 25657 axlowdimlem16 26426 2pthd 27406 wlk2v2e 27623 ex-bc 27923 cyc3fv1 30416 cyc3fv2 30417 cyc3fv3 30418 fib4 31279 circlemethhgt 31531 cusgracyclt3v 32011 itg2addnclem3 34476 lhe4.4ex1a 40199 wallispilem4 41895 fmtnoge3 43174 fmtnoprmfac2lem1 43210 nnsum3primesle9 43441 |
Copyright terms: Public domain | W3C validator |