Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 2t2e4 | Structured version Visualization version GIF version |
Description: 2 times 2 equals 4. (Contributed by NM, 1-Aug-1999.) |
Ref | Expression |
---|---|
2t2e4 | ⊢ (2 · 2) = 4 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2cn 11902 | . . 3 ⊢ 2 ∈ ℂ | |
2 | 1 | 2timesi 11965 | . 2 ⊢ (2 · 2) = (2 + 2) |
3 | 2p2e4 11962 | . 2 ⊢ (2 + 2) = 4 | |
4 | 2, 3 | eqtri 2765 | 1 ⊢ (2 · 2) = 4 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1543 (class class class)co 7210 + caddc 10729 · cmul 10731 2c2 11882 4c4 11884 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 ax-resscn 10783 ax-1cn 10784 ax-icn 10785 ax-addcl 10786 ax-mulcl 10788 ax-mulcom 10790 ax-addass 10791 ax-mulass 10792 ax-distr 10793 ax-1rid 10796 ax-cnre 10799 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3063 df-rex 3064 df-rab 3067 df-v 3407 df-dif 3866 df-un 3868 df-in 3870 df-ss 3880 df-nul 4235 df-if 4437 df-sn 4539 df-pr 4541 df-op 4545 df-uni 4817 df-br 5051 df-iota 6335 df-fv 6385 df-ov 7213 df-2 11890 df-3 11891 df-4 11892 |
This theorem is referenced by: 4d2e2 11997 halfpm6th 12048 div4p1lem1div2 12082 3halfnz 12253 decbin0 12430 fldiv4lem1div2uz2 13408 sq2 13763 sq4e2t8 13765 discr 13804 sqoddm1div8 13807 faclbnd2 13854 4bc2eq6 13892 amgm2 14930 bpoly3 15617 sin4lt0 15753 z4even 15930 flodddiv4 15971 flodddiv4t2lthalf 15974 4nprm 16249 2exp4 16635 2exp16 16641 5prm 16659 631prm 16677 1259lem1 16681 1259lem4 16684 2503lem1 16687 2503lem2 16688 2503lem3 16689 4001lem1 16691 4001lem2 16692 4001lem3 16693 4001prm 16695 pcoass 23918 minveclem2 24320 uniioombllem5 24481 uniioombl 24483 dveflem 24873 pilem2 25341 sinhalfpilem 25350 sincosq1lem 25384 tangtx 25392 sincos4thpi 25400 heron 25718 quad2 25719 dquartlem1 25731 dquart 25733 quart1 25736 atan1 25808 log2ublem3 25828 log2ub 25829 chtub 26090 bclbnd 26158 bpos1 26161 bposlem2 26163 bposlem6 26167 bposlem9 26170 gausslemma2dlem3 26246 m1lgs 26266 2lgslem1a2 26268 2lgslem3a 26274 2lgslem3b 26275 2lgslem3c 26276 2lgslem3d 26277 pntibndlem2 26469 pntlemg 26476 pntlemr 26480 ex-fl 28527 minvecolem2 28953 polid2i 29235 quad3 33338 420lcm8e840 39751 3exp7 39793 3lexlogpow5ineq1 39794 3lexlogpow2ineq2 39799 3lexlogpow5ineq5 39800 aks4d1p1p2 39809 aks4d1p1 39815 2ap1caineq 39821 flt4lem 40183 3cubeslem3l 40209 3cubeslem3r 40210 wallispi2lem1 43285 wallispi2lem2 43286 stirlinglem3 43290 stirlinglem10 43297 fmtnorec4 44672 2exp340mod341 44856 8exp8mod9 44859 ackval2012 45708 |
Copyright terms: Public domain | W3C validator |