Theorem problem4

Description: Practice problem 4. Clues: pm3.2i eqcomi eqtri subaddrii recni 7re 6re ax-1cn df-7 ax-mp oveq1i 3cn 2cn df-3 mulid2i subdiri mp3an mulcli subadd23 oveq2i oveq12i 3t2e6 mulcomi subcli biimpri subadd2i . (Contributed by Filip Cernatescu, 16-Mar-2019) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	problem4.1	$$⊢A\in ℂ$$
	problem4.2	$$⊢B\in ℂ$$
	problem4.3	$$⊢A+B=3$$
	problem4.4	$$⊢3A+2B=7$$
Assertion	problem4	$$⊢\left(A=1\wedge B=2\right)$$

Proof

Step	Hyp	Ref	Expression
1		problem4.1	$$⊢A\in ℂ$$
2		problem4.2	$$⊢B\in ℂ$$
3		problem4.3	$$⊢A+B=3$$
4		problem4.4	$$⊢3A+2B=7$$
5		7re	$$⊢7\in ℝ$$
6	5	recni	$$⊢7\in ℂ$$
7		6re	$$⊢6\in ℝ$$
8	7	recni	$$⊢6\in ℂ$$
9		ax-1cn	$$⊢1\in ℂ$$
10		df-7	$$⊢7=6+1$$
11	10	eqcomi	$$⊢6+1=7$$
12	6 8 9 11	subaddrii	$$⊢7-6=1$$
13	12	eqcomi	$$⊢1=7-6$$
14		3cn	$$⊢3\in ℂ$$
15		2cn	$$⊢2\in ℂ$$
16		df-3	$$⊢3=2+1$$
17	16	eqcomi	$$⊢2+1=3$$
18	14 15 9 17	subaddrii	$$⊢3-2=1$$
19	18	oveq1i	$$⊢\left(3-2\right)A=1A$$
20	1	mulid2i	$$⊢1A=A$$
21	19 20	eqtri	$$⊢\left(3-2\right)A=A$$
22	21	eqcomi	$$⊢A=\left(3-2\right)A$$
23	14 15 1	subdiri	$$⊢\left(3-2\right)A=3A-2A$$
24	22 23	eqtri	$$⊢A=3A-2A$$
25	24	oveq1i	$$⊢A+6=3A-2A+6$$
26	14 1	mulcli	$$⊢3A\in ℂ$$
27	15 1	mulcli	$$⊢2A\in ℂ$$
28		subadd23	$$⊢\left(3A\in ℂ\wedge 2A\in ℂ\wedge 6\in ℂ\right)\to 3A-2A+6=3A+6-2A$$
29	26 27 8 28	mp3an	$$⊢3A-2A+6=3A+6-2A$$
30		3t2e6	$$⊢3\cdot 2=6$$
31	1 15	mulcomi	$$⊢A\cdot 2=2A$$
32	30 31	oveq12i	$$⊢3\cdot 2-A\cdot 2=6-2A$$
33	32	eqcomi	$$⊢6-2A=3\cdot 2-A\cdot 2$$
34	14 1 15	subdiri	$$⊢\left(3-A\right)\cdot 2=3\cdot 2-A\cdot 2$$
35	34	eqcomi	$$⊢3\cdot 2-A\cdot 2=\left(3-A\right)\cdot 2$$
36	14 1	subcli	$$⊢3-A\in ℂ$$
37	15 36	mulcomi	$$⊢2\left(3-A\right)=\left(3-A\right)\cdot 2$$
38	37	eqcomi	$$⊢\left(3-A\right)\cdot 2=2\left(3-A\right)$$
39	14 1 2 3	subaddrii	$$⊢3-A=B$$
40	39	eqcomi	$$⊢B=3-A$$
41	40	oveq2i	$$⊢2B=2\left(3-A\right)$$
42	41	eqcomi	$$⊢2\left(3-A\right)=2B$$
43	38 42	eqtri	$$⊢\left(3-A\right)\cdot 2=2B$$
44	35 43	eqtri	$$⊢3\cdot 2-A\cdot 2=2B$$
45	33 44	eqtri	$$⊢6-2A=2B$$
46	45	eqcomi	$$⊢2B=6-2A$$
47	46	oveq2i	$$⊢3A+2B=3A+6-2A$$
48	47	eqcomi	$$⊢3A+6-2A=3A+2B$$
49	29 48	eqtri	$$⊢3A-2A+6=3A+2B$$
50	25 49	eqtri	$$⊢A+6=3A+2B$$
51	50 4	eqtri	$$⊢A+6=7$$
52	6 8 1	subadd2i	$$⊢7-6=A\leftrightarrow A+6=7$$
53	52	biimpri	$$⊢A+6=7\to 7-6=A$$
54	51 53	ax-mp	$$⊢7-6=A$$
55	13 54	eqtri	$$⊢1=A$$
56	55	eqcomi	$$⊢A=1$$
57	56	oveq2i	$$⊢3-A=3-1$$
58	14 9 15	subadd2i	$$⊢3-1=2\leftrightarrow 2+1=3$$
59	58	biimpri	$$⊢2+1=3\to 3-1=2$$
60	17 59	ax-mp	$$⊢3-1=2$$
61	57 60	eqtri	$$⊢3-A=2$$
62	40 61	eqtri	$$⊢B=2$$
63	56 62	pm3.2i	$$⊢\left(A=1\wedge B=2\right)$$