![]() |
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 12186 | . . 3 ⊢ 2 ∈ ℂ | |
2 | 1 | 2timesi 12249 | . 2 ⊢ (2 · 2) = (2 + 2) |
3 | 2p2e4 12246 | . 2 ⊢ (2 + 2) = 4 | |
4 | 2, 3 | eqtri 2765 | 1 ⊢ (2 · 2) = 4 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 (class class class)co 7351 + caddc 11012 · cmul 11014 2c2 12166 4c4 12168 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2708 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-mulcl 11071 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-1rid 11079 ax-cnre 11082 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2715 df-cleq 2729 df-clel 2815 df-rex 3072 df-rab 3406 df-v 3445 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-br 5104 df-iota 6445 df-fv 6501 df-ov 7354 df-2 12174 df-3 12175 df-4 12176 |
This theorem is referenced by: 4d2e2 12281 halfpm6th 12332 div4p1lem1div2 12366 3halfnz 12540 decbin0 12716 fldiv4lem1div2uz2 13695 sq2 14055 sq4e2t8 14057 discr 14097 sqoddm1div8 14100 faclbnd2 14145 4bc2eq6 14183 amgm2 15214 bpoly3 15901 sin4lt0 16037 z4even 16214 flodddiv4 16255 flodddiv4t2lthalf 16258 4nprm 16531 2exp4 16917 2exp16 16923 5prm 16941 631prm 16959 1259lem1 16963 1259lem4 16966 2503lem1 16969 2503lem2 16970 2503lem3 16971 4001lem1 16973 4001lem2 16974 4001lem3 16975 4001prm 16977 pcoass 24339 minveclem2 24742 uniioombllem5 24903 uniioombl 24905 dveflem 25295 pilem2 25763 sinhalfpilem 25772 sincosq1lem 25806 tangtx 25814 sincos4thpi 25822 heron 26140 quad2 26141 dquartlem1 26153 dquart 26155 quart1 26158 atan1 26230 log2ublem3 26250 log2ub 26251 chtub 26512 bclbnd 26580 bpos1 26583 bposlem2 26585 bposlem6 26589 bposlem9 26592 gausslemma2dlem3 26668 m1lgs 26688 2lgslem1a2 26690 2lgslem3a 26696 2lgslem3b 26697 2lgslem3c 26698 2lgslem3d 26699 pntibndlem2 26891 pntlemg 26898 pntlemr 26902 ex-fl 29220 minvecolem2 29646 polid2i 29928 quad3 34070 420lcm8e840 40406 3exp7 40448 3lexlogpow5ineq1 40449 3lexlogpow2ineq2 40454 3lexlogpow5ineq5 40455 aks4d1p1p2 40465 aks4d1p1 40471 2ap1caineq 40491 flt4lem 40892 3cubeslem3l 40918 3cubeslem3r 40919 wallispi2lem1 44213 wallispi2lem2 44214 stirlinglem3 44218 stirlinglem10 44225 fmtnorec4 45642 2exp340mod341 45826 8exp8mod9 45829 ackval2012 46678 |
Copyright terms: Public domain | W3C validator |