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\cdot 10+5+1\cdot 10+4=3\cdot 10+9$$

Proof

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