Theorem problem2

Description: Practice problem 2. Clues: oveq12i adddiri add4i mulcli recni 2re 3eqtri 10re 5re 1re 4re eqcomi 5p4e9 oveq1i df-3 . (Contributed by Filip Cernatescu, 16-Mar-2019) (Revised by AV, 9-Sep-2021) (Proof modification is discouraged.)

	Ref	Expression
Assertion	problem2	⊢ ( ( ( 2 · ; 1 0 ) + 5 ) + ( ( 1 · ; 1 0 ) + 4 ) ) = ( ( 3 · ; 1 0 ) + 9 )

Proof

Step	Hyp	Ref	Expression
1		2re	⊢ 2 ∈ ℝ
2	1	recni	⊢ 2 ∈ ℂ
3		10re	⊢ ; 1 0 ∈ ℝ
4	3	recni	⊢ ; 1 0 ∈ ℂ
5	2 4	mulcli	⊢ ( 2 · ; 1 0 ) ∈ ℂ
6		5re	⊢ 5 ∈ ℝ
7	6	recni	⊢ 5 ∈ ℂ
8		1re	⊢ 1 ∈ ℝ
9	8	recni	⊢ 1 ∈ ℂ
10	9 4	mulcli	⊢ ( 1 · ; 1 0 ) ∈ ℂ
11		4re	⊢ 4 ∈ ℝ
12	11	recni	⊢ 4 ∈ ℂ
13	5 7 10 12	add4i	⊢ ( ( ( 2 · ; 1 0 ) + 5 ) + ( ( 1 · ; 1 0 ) + 4 ) ) = ( ( ( 2 · ; 1 0 ) + ( 1 · ; 1 0 ) ) + ( 5 + 4 ) )
14	2 9 4	adddiri	⊢ ( ( 2 + 1 ) · ; 1 0 ) = ( ( 2 · ; 1 0 ) + ( 1 · ; 1 0 ) )
15	14	eqcomi	⊢ ( ( 2 · ; 1 0 ) + ( 1 · ; 1 0 ) ) = ( ( 2 + 1 ) · ; 1 0 )
16		5p4e9	⊢ ( 5 + 4 ) = 9
17	15 16	oveq12i	⊢ ( ( ( 2 · ; 1 0 ) + ( 1 · ; 1 0 ) ) + ( 5 + 4 ) ) = ( ( ( 2 + 1 ) · ; 1 0 ) + 9 )
18		df-3	⊢ 3 = ( 2 + 1 )
19	18	eqcomi	⊢ ( 2 + 1 ) = 3
20	19	oveq1i	⊢ ( ( 2 + 1 ) · ; 1 0 ) = ( 3 · ; 1 0 )
21	20	oveq1i	⊢ ( ( ( 2 + 1 ) · ; 1 0 ) + 9 ) = ( ( 3 · ; 1 0 ) + 9 )
22	13 17 21	3eqtri	⊢ ( ( ( 2 · ; 1 0 ) + 5 ) + ( ( 1 · ; 1 0 ) + 4 ) ) = ( ( 3 · ; 1 0 ) + 9 )