![]() |
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 8149 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 11688 | . . 3 ⊢ 2 = (1 + 1) | |
2 | 1 | oveq2i 7146 | . 2 ⊢ (2 + 2) = (2 + (1 + 1)) |
3 | df-4 11690 | . . 3 ⊢ 4 = (3 + 1) | |
4 | df-3 11689 | . . . 4 ⊢ 3 = (2 + 1) | |
5 | 4 | oveq1i 7145 | . . 3 ⊢ (3 + 1) = ((2 + 1) + 1) |
6 | 2cn 11700 | . . . 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 2825 | . 2 ⊢ 4 = (2 + (1 + 1)) |
10 | 2, 9 | eqtr4i 2824 | 1 ⊢ (2 + 2) = 4 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1538 (class class class)co 7135 1c1 10527 + caddc 10529 2c2 11680 3c3 11681 4c4 11682 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 ax-1cn 10584 ax-addcl 10586 ax-addass 10591 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-v 3443 df-un 3886 df-in 3888 df-ss 3898 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-iota 6283 df-fv 6332 df-ov 7138 df-2 11688 df-3 11689 df-4 11690 |
This theorem is referenced by: 2t2e4 11789 i4 13563 4bc2eq6 13685 bpoly4 15405 fsumcube 15406 ef01bndlem 15529 6gcd4e2 15876 pythagtriplem1 16143 prmlem2 16445 43prm 16447 1259lem4 16459 2503lem1 16462 2503lem2 16463 2503lem3 16464 4001lem1 16466 4001lem4 16469 cphipval2 23845 quart1lem 25441 log2ub 25535 hgt750lem2 32033 3cubeslem3l 39627 3cubeslem3r 39628 wallispi2lem1 42713 stirlinglem8 42723 sqwvfourb 42871 fmtnorec4 44066 m11nprm 44119 3exp4mod41 44134 gbowgt5 44280 gbpart7 44285 sbgoldbaltlem1 44297 sbgoldbalt 44299 sgoldbeven3prm 44301 mogoldbb 44303 nnsum3primes4 44306 2t6m3t4e0 44750 ackval1012 45104 2p2ne5 45326 |
Copyright terms: Public domain | W3C validator |