Theorem 2p2e4 11328

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.)

Assertion

Ref	Expression
2p2e4	⊢ (2 + 2) = 4

Proof of Theorem 2p2e4

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

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