This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2p2e4

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 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
Assertion 2p2e4 
|- ( 2 + 2 ) = 4

Proof

Step Hyp Ref Expression
1 df-2 
 |-  2 = ( 1 + 1 )
2 1 oveq2i 
 |-  ( 2 + 2 ) = ( 2 + ( 1 + 1 ) )
3 df-4 
 |-  4 = ( 3 + 1 )
4 df-3 
 |-  3 = ( 2 + 1 )
5 4 oveq1i 
 |-  ( 3 + 1 ) = ( ( 2 + 1 ) + 1 )
6 2cn 
 |-  2 e. CC
7 ax-1cn 
 |-  1 e. CC
8 6 7 7 addassi 
 |-  ( ( 2 + 1 ) + 1 ) = ( 2 + ( 1 + 1 ) )
9 3 5 8 3eqtri 
 |-  4 = ( 2 + ( 1 + 1 ) )
10 2 9 eqtr4i 
 |-  ( 2 + 2 ) = 4