![]() |
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 7782 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 11263 | . . 3 ⊢ 2 = (1 + 1) | |
2 | 1 | oveq2i 6816 | . 2 ⊢ (2 + 2) = (2 + (1 + 1)) |
3 | df-4 11265 | . . 3 ⊢ 4 = (3 + 1) | |
4 | df-3 11264 | . . . 4 ⊢ 3 = (2 + 1) | |
5 | 4 | oveq1i 6815 | . . 3 ⊢ (3 + 1) = ((2 + 1) + 1) |
6 | 2cn 11275 | . . . 4 ⊢ 2 ∈ ℂ | |
7 | ax-1cn 10178 | . . . 4 ⊢ 1 ∈ ℂ | |
8 | 6, 7, 7 | addassi 10232 | . . 3 ⊢ ((2 + 1) + 1) = (2 + (1 + 1)) |
9 | 3, 5, 8 | 3eqtri 2778 | . 2 ⊢ 4 = (2 + (1 + 1)) |
10 | 2, 9 | eqtr4i 2777 | 1 ⊢ (2 + 2) = 4 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1624 (class class class)co 6805 1c1 10121 + caddc 10123 2c2 11254 3c3 11255 4c4 11256 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 ax-resscn 10177 ax-1cn 10178 ax-icn 10179 ax-addcl 10180 ax-addrcl 10181 ax-mulcl 10182 ax-mulrcl 10183 ax-addass 10185 ax-i2m1 10188 ax-1ne0 10189 ax-rrecex 10192 ax-cnre 10193 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1627 df-ex 1846 df-nf 1851 df-sb 2039 df-clab 2739 df-cleq 2745 df-clel 2748 df-nfc 2883 df-ne 2925 df-ral 3047 df-rex 3048 df-rab 3051 df-v 3334 df-dif 3710 df-un 3712 df-in 3714 df-ss 3721 df-nul 4051 df-if 4223 df-sn 4314 df-pr 4316 df-op 4320 df-uni 4581 df-br 4797 df-iota 6004 df-fv 6049 df-ov 6808 df-2 11263 df-3 11264 df-4 11265 |
This theorem is referenced by: 2t2e4 11361 i4 13153 4bc2eq6 13302 bpoly4 14981 fsumcube 14982 ef01bndlem 15105 6gcd4e2 15449 pythagtriplem1 15715 prmlem2 16021 43prm 16023 1259lem4 16035 2503lem1 16038 2503lem2 16039 2503lem3 16040 4001lem1 16042 4001lem4 16045 cphipval2 23232 quart1lem 24773 log2ub 24867 hgt750lem2 31031 wallispi2lem1 40783 stirlinglem8 40793 sqwvfourb 40941 fmtnorec4 41963 m11nprm 42020 3exp4mod41 42035 gbowgt5 42152 gbpart7 42157 sbgoldbaltlem1 42169 sbgoldbalt 42171 sgoldbeven3prm 42173 mogoldbb 42175 nnsum3primes4 42178 2t6m3t4e0 42628 2p2ne5 43049 |
Copyright terms: Public domain | W3C validator |