Theorem 4p4e8ALT 43452

Description: A shorter proof of 4p4e8 12510 if 6p2e8 12514 was moved up. The most clean way to do this would be to start with 7p2e9 12516, then go 6p2e8 12514, 6p3e9 12515, etc., which is still inelegant. The idea here is that using 4 = 2 + 2 and 2cn 12431 is shorter than using 4 = 3 + 1, 3cn 12437, and ax-1cn 11271. This also works with 5p4e9 12513. (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 12441	. . 3 ⊢ 4 ∈ ℂ
2		2cn 12431	. . 3 ⊢ 2 ∈ ℂ
3	1, 2, 2	addassi 11332	. 2 ⊢ ((4 + 2) + 2) = (4 + (2 + 2))
4		4p2e6 12508	. . . 4 ⊢ (4 + 2) = 6
5	4	oveq1i 7440	. . 3 ⊢ ((4 + 2) + 2) = (6 + 2)
6		6p2e8 12514	. . 3 ⊢ (6 + 2) = 8
7	5, 6	eqtri 2786	. 2 ⊢ ((4 + 2) + 2) = 8
8		2p2e4 12490	. . 3 ⊢ (2 + 2) = 4
9	8	oveq2i 7441	. 2 ⊢ (4 + (2 + 2)) = (4 + 4)
10	3, 7, 9	3eqtr3ri 2795	1 ⊢ (4 + 4) = 8

This proof depends on syntax axioms:   = wceq 1569  (class class class)co 7430   + caddc 11216  2c2 12410  4c4 12412  6c6 12414  8c8 12416

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-1cn 11271  ax-addcl 11273  ax-addass 11278

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6501  df-fv 6555  df-ov 7433  df-2 12418  df-3 12419  df-4 12420  df-5 12421  df-6 12422  df-7 12423  df-8 12424

This theorem is used by: (None)