Theorem 4p4e8ALT 43088

Description: A shorter proof of 4p4e8 12414 if 6p2e8 12418 was moved up. The most clean way to do this would be to start with 7p2e9 12420, then go 6p2e8 12418, 6p3e9 12419, etc., which is still inelegant. The idea here is that using 4 = 2 + 2 and 2cn 12335 is shorter than using 4 = 3 + 1, 3cn 12341, and ax-1cn 11177. This also works with 5p4e9 12417. (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 12345	. . 3 ⊢ 4 ∈ ℂ
2		2cn 12335	. . 3 ⊢ 2 ∈ ℂ
3	1, 2, 2	addassi 11238	. 2 ⊢ ((4 + 2) + 2) = (4 + (2 + 2))
4		4p2e6 12412	. . . 4 ⊢ (4 + 2) = 6
5	4	oveq1i 7429	. . 3 ⊢ ((4 + 2) + 2) = (6 + 2)
6		6p2e8 12418	. . 3 ⊢ (6 + 2) = 8
7	5, 6	eqtri 2788	. 2 ⊢ ((4 + 2) + 2) = 8
8		2p2e4 12394	. . 3 ⊢ (2 + 2) = 4
9	8	oveq2i 7430	. 2 ⊢ (4 + (2 + 2)) = (4 + 4)
10	3, 7, 9	3eqtr3ri 2797	1 ⊢ (4 + 4) = 8

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7419   + caddc 11122  2c2 12314  4c4 12316  6c6 12318  8c8 12320

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 2148  ax-9 2156  ax-ext 2737  ax-1cn 11177  ax-addcl 11179  ax-addass 11184

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-2 12322  df-3 12323  df-4 12324  df-5 12325  df-6 12326  df-7 12327  df-8 12328

This theorem is used by: (None)