Theorem 4p4e8ALT 43309

Description: A shorter proof of 4p4e8 12497 if 6p2e8 12501 was moved up. The most clean way to do this would be to start with 7p2e9 12503, then go 6p2e8 12501, 6p3e9 12502, etc., which is still inelegant. The idea here is that using 4 = 2 + 2 and 2cn 12418 is shorter than using 4 = 3 + 1, 3cn 12424, and ax-1cn 11258. This also works with 5p4e9 12500. (Contributed by SN, 24-Aug-2026.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
4p4e8ALT	⊢ (4 + 4) = 8

Proof of Theorem 4p4e8ALT

Step	Hyp	Ref	Expression
1		4cn 12428	. . 3 ⊢ 4 ∈ ℂ
2		2cn 12418	. . 3 ⊢ 2 ∈ ℂ
3	1, 2, 2	addassi 11319	. 2 ⊢ ((4 + 2) + 2) = (4 + (2 + 2))
4		4p2e6 12495	. . . 4 ⊢ (4 + 2) = 6
5	4	oveq1i 7430	. . 3 ⊢ ((4 + 2) + 2) = (6 + 2)
6		6p2e8 12501	. . 3 ⊢ (6 + 2) = 8
7	5, 6	eqtri 2784	. 2 ⊢ ((4 + 2) + 2) = 8
8		2p2e4 12477	. . 3 ⊢ (2 + 2) = 4
9	8	oveq2i 7431	. 2 ⊢ (4 + (2 + 2)) = (4 + 4)
10	3, 7, 9	3eqtr3ri 2793	1 ⊢ (4 + 4) = 8

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7420   + caddc 11203  2c2 12397  4c4 12399  6c6 12401  8c8 12403

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-1cn 11258  ax-addcl 11260  ax-addass 11265

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6494  df-fv 6546  df-ov 7423  df-2 12405  df-3 12406  df-4 12407  df-5 12408  df-6 12409  df-7 12410  df-8 12411

This theorem is used by: (None)