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	⊢ 𝐴 ∈ ℂ
	problem4.2	⊢ 𝐵 ∈ ℂ
	problem4.3	⊢ ( 𝐴 + 𝐵 ) = 3
	problem4.4	⊢ ( ( 3 · 𝐴 ) + ( 2 · 𝐵 ) ) = 7
Assertion	problem4	⊢ ( 𝐴 = 1 ∧ 𝐵 = 2 )

Proof

Step	Hyp	Ref	Expression
1		problem4.1	⊢ 𝐴 ∈ ℂ
2		problem4.2	⊢ 𝐵 ∈ ℂ
3		problem4.3	⊢ ( 𝐴 + 𝐵 ) = 3
4		problem4.4	⊢ ( ( 3 · 𝐴 ) + ( 2 · 𝐵 ) ) = 7
5		7re	⊢ 7 ∈ ℝ
6	5	recni	⊢ 7 ∈ ℂ
7		6re	⊢ 6 ∈ ℝ
8	7	recni	⊢ 6 ∈ ℂ
9		ax-1cn	⊢ 1 ∈ ℂ
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 ∈ ℂ
15		2cn	⊢ 2 ∈ ℂ
16		df-3	⊢ 3 = ( 2 + 1 )
17	16	eqcomi	⊢ ( 2 + 1 ) = 3
18	14 15 9 17	subaddrii	⊢ ( 3 − 2 ) = 1
19	18	oveq1i	⊢ ( ( 3 − 2 ) · 𝐴 ) = ( 1 · 𝐴 )
20	1	mulid2i	⊢ ( 1 · 𝐴 ) = 𝐴
21	19 20	eqtri	⊢ ( ( 3 − 2 ) · 𝐴 ) = 𝐴
22	21	eqcomi	⊢ 𝐴 = ( ( 3 − 2 ) · 𝐴 )
23	14 15 1	subdiri	⊢ ( ( 3 − 2 ) · 𝐴 ) = ( ( 3 · 𝐴 ) − ( 2 · 𝐴 ) )
24	22 23	eqtri	⊢ 𝐴 = ( ( 3 · 𝐴 ) − ( 2 · 𝐴 ) )
25	24	oveq1i	⊢ ( 𝐴 + 6 ) = ( ( ( 3 · 𝐴 ) − ( 2 · 𝐴 ) ) + 6 )
26	14 1	mulcli	⊢ ( 3 · 𝐴 ) ∈ ℂ
27	15 1	mulcli	⊢ ( 2 · 𝐴 ) ∈ ℂ
28		subadd23	⊢ ( ( ( 3 · 𝐴 ) ∈ ℂ ∧ ( 2 · 𝐴 ) ∈ ℂ ∧ 6 ∈ ℂ ) → ( ( ( 3 · 𝐴 ) − ( 2 · 𝐴 ) ) + 6 ) = ( ( 3 · 𝐴 ) + ( 6 − ( 2 · 𝐴 ) ) ) )
29	26 27 8 28	mp3an	⊢ ( ( ( 3 · 𝐴 ) − ( 2 · 𝐴 ) ) + 6 ) = ( ( 3 · 𝐴 ) + ( 6 − ( 2 · 𝐴 ) ) )
30		3t2e6	⊢ ( 3 · 2 ) = 6
31	1 15	mulcomi	⊢ ( 𝐴 · 2 ) = ( 2 · 𝐴 )
32	30 31	oveq12i	⊢ ( ( 3 · 2 ) − ( 𝐴 · 2 ) ) = ( 6 − ( 2 · 𝐴 ) )
33	32	eqcomi	⊢ ( 6 − ( 2 · 𝐴 ) ) = ( ( 3 · 2 ) − ( 𝐴 · 2 ) )
34	14 1 15	subdiri	⊢ ( ( 3 − 𝐴 ) · 2 ) = ( ( 3 · 2 ) − ( 𝐴 · 2 ) )
35	34	eqcomi	⊢ ( ( 3 · 2 ) − ( 𝐴 · 2 ) ) = ( ( 3 − 𝐴 ) · 2 )
36	14 1	subcli	⊢ ( 3 − 𝐴 ) ∈ ℂ
37	15 36	mulcomi	⊢ ( 2 · ( 3 − 𝐴 ) ) = ( ( 3 − 𝐴 ) · 2 )
38	37	eqcomi	⊢ ( ( 3 − 𝐴 ) · 2 ) = ( 2 · ( 3 − 𝐴 ) )
39	14 1 2 3	subaddrii	⊢ ( 3 − 𝐴 ) = 𝐵
40	39	eqcomi	⊢ 𝐵 = ( 3 − 𝐴 )
41	40	oveq2i	⊢ ( 2 · 𝐵 ) = ( 2 · ( 3 − 𝐴 ) )
42	41	eqcomi	⊢ ( 2 · ( 3 − 𝐴 ) ) = ( 2 · 𝐵 )
43	38 42	eqtri	⊢ ( ( 3 − 𝐴 ) · 2 ) = ( 2 · 𝐵 )
44	35 43	eqtri	⊢ ( ( 3 · 2 ) − ( 𝐴 · 2 ) ) = ( 2 · 𝐵 )
45	33 44	eqtri	⊢ ( 6 − ( 2 · 𝐴 ) ) = ( 2 · 𝐵 )
46	45	eqcomi	⊢ ( 2 · 𝐵 ) = ( 6 − ( 2 · 𝐴 ) )
47	46	oveq2i	⊢ ( ( 3 · 𝐴 ) + ( 2 · 𝐵 ) ) = ( ( 3 · 𝐴 ) + ( 6 − ( 2 · 𝐴 ) ) )
48	47	eqcomi	⊢ ( ( 3 · 𝐴 ) + ( 6 − ( 2 · 𝐴 ) ) ) = ( ( 3 · 𝐴 ) + ( 2 · 𝐵 ) )
49	29 48	eqtri	⊢ ( ( ( 3 · 𝐴 ) − ( 2 · 𝐴 ) ) + 6 ) = ( ( 3 · 𝐴 ) + ( 2 · 𝐵 ) )
50	25 49	eqtri	⊢ ( 𝐴 + 6 ) = ( ( 3 · 𝐴 ) + ( 2 · 𝐵 ) )
51	50 4	eqtri	⊢ ( 𝐴 + 6 ) = 7
52	6 8 1	subadd2i	⊢ ( ( 7 − 6 ) = 𝐴 ↔ ( 𝐴 + 6 ) = 7 )
53	52	biimpri	⊢ ( ( 𝐴 + 6 ) = 7 → ( 7 − 6 ) = 𝐴 )
54	51 53	ax-mp	⊢ ( 7 − 6 ) = 𝐴
55	13 54	eqtri	⊢ 1 = 𝐴
56	55	eqcomi	⊢ 𝐴 = 1
57	56	oveq2i	⊢ ( 3 − 𝐴 ) = ( 3 − 1 )
58	14 9 15	subadd2i	⊢ ( ( 3 − 1 ) = 2 ↔ ( 2 + 1 ) = 3 )
59	58	biimpri	⊢ ( ( 2 + 1 ) = 3 → ( 3 − 1 ) = 2 )
60	17 59	ax-mp	⊢ ( 3 − 1 ) = 2
61	57 60	eqtri	⊢ ( 3 − 𝐴 ) = 2
62	40 61	eqtri	⊢ 𝐵 = 2
63	56 62	pm3.2i	⊢ ( 𝐴 = 1 ∧ 𝐵 = 2 )