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 ∈ ℂ
2		2cn	⊢ 2 ∈ ℂ
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