Theorem 4p4e8ALT

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

	Ref	Expression
Assertion	4p4e8ALT	$$⊢4+4=8$$

Proof

Step	Hyp	Ref	Expression
1		4cn	$$⊢4\in ℂ$$
2		2cn	$$⊢2\in ℂ$$
3	1 2 2	addassi	$$⊢4+2+2=4+2+2$$
4		4p2e6	$$⊢4+2=6$$
5	4	oveq1i	$$⊢4+2+2=6+2$$
6		6p2e8	$$⊢6+2=8$$
7	5 6	eqtri	$$⊢4+2+2=8$$
8		2p2e4	$$⊢2+2=4$$
9	8	oveq2i	$$⊢4+2+2=4+4$$
10	3 7 9	3eqtr3ri	$$⊢4+4=8$$