Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 2p2e4 | Structured version Visualization version GIF version |
Description: Two plus two equals four. For more information, see "2+2=4 Trivia" on the Metamath Proof Explorer Home Page: mmset.html#trivia. This proof is simple, but it depends on many other proof steps because 2 and 4 are complex numbers and thus it depends on our construction of complex numbers. The proof o2p2e4 8157 is similar but proves 2 + 2 = 4 using ordinal natural numbers (finite integers starting at 0), so that proof depends on fewer intermediate steps. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
2p2e4 | ⊢ (2 + 2) = 4 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-2 11689 | . . 3 ⊢ 2 = (1 + 1) | |
2 | 1 | oveq2i 7156 | . 2 ⊢ (2 + 2) = (2 + (1 + 1)) |
3 | df-4 11691 | . . 3 ⊢ 4 = (3 + 1) | |
4 | df-3 11690 | . . . 4 ⊢ 3 = (2 + 1) | |
5 | 4 | oveq1i 7155 | . . 3 ⊢ (3 + 1) = ((2 + 1) + 1) |
6 | 2cn 11701 | . . . 4 ⊢ 2 ∈ ℂ | |
7 | ax-1cn 10584 | . . . 4 ⊢ 1 ∈ ℂ | |
8 | 6, 7, 7 | addassi 10640 | . . 3 ⊢ ((2 + 1) + 1) = (2 + (1 + 1)) |
9 | 3, 5, 8 | 3eqtri 2848 | . 2 ⊢ 4 = (2 + (1 + 1)) |
10 | 2, 9 | eqtr4i 2847 | 1 ⊢ (2 + 2) = 4 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 (class class class)co 7145 1c1 10527 + caddc 10529 2c2 11681 3c3 11682 4c4 11683 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 ax-1cn 10584 ax-addcl 10586 ax-addass 10591 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rex 3144 df-rab 3147 df-v 3497 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-uni 4833 df-br 5059 df-iota 6308 df-fv 6357 df-ov 7148 df-2 11689 df-3 11690 df-4 11691 |
This theorem is referenced by: 2t2e4 11790 i4 13557 4bc2eq6 13679 bpoly4 15403 fsumcube 15404 ef01bndlem 15527 6gcd4e2 15876 pythagtriplem1 16143 prmlem2 16443 43prm 16445 1259lem4 16457 2503lem1 16460 2503lem2 16461 2503lem3 16462 4001lem1 16464 4001lem4 16467 cphipval2 23773 quart1lem 25360 log2ub 25455 hgt750lem2 31823 3cubeslem3l 39163 3cubeslem3r 39164 wallispi2lem1 42237 stirlinglem8 42247 sqwvfourb 42395 fmtnorec4 43558 m11nprm 43613 3exp4mod41 43628 gbowgt5 43774 gbpart7 43779 sbgoldbaltlem1 43791 sbgoldbalt 43793 sgoldbeven3prm 43795 mogoldbb 43797 nnsum3primes4 43800 2t6m3t4e0 44294 2p2ne5 44797 |
Copyright terms: Public domain | W3C validator |