Theorem 4p4e8ALT 43125

Description: A shorter proof of 4p4e8 12419 if 6p2e8 12423 was moved up. The most clean way to do this would be to start with 7p2e9 12425, then go 6p2e8 12423, 6p3e9 12424, etc., which is still inelegant. The idea here is that using 4 = 2 + 2 and 2cn 12340 is shorter than using 4 = 3 + 1, 3cn 12346, and ax-1cn 11182. This also works with 5p4e9 12422. (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 12350	. . 3 ⊢ 4 ∈ ℂ
2		2cn 12340	. . 3 ⊢ 2 ∈ ℂ
3	1, 2, 2	addassi 11243	. 2 ⊢ ((4 + 2) + 2) = (4 + (2 + 2))
4		4p2e6 12417	. . . 4 ⊢ (4 + 2) = 6
5	4	oveq1i 7423	. . 3 ⊢ ((4 + 2) + 2) = (6 + 2)
6		6p2e8 12423	. . 3 ⊢ (6 + 2) = 8
7	5, 6	eqtri 2783	. 2 ⊢ ((4 + 2) + 2) = 8
8		2p2e4 12399	. . 3 ⊢ (2 + 2) = 4
9	8	oveq2i 7424	. 2 ⊢ (4 + (2 + 2)) = (4 + 4)
10	3, 7, 9	3eqtr3ri 2792	1 ⊢ (4 + 4) = 8

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7413   + caddc 11127  2c2 12319  4c4 12321  6c6 12323  8c8 12325

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 2732  ax-1cn 11182  ax-addcl 11184  ax-addass 11189

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  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 6489  df-fv 6541  df-ov 7416  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333

This theorem is used by: (None)