Metamath Proof Explorer


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
problem4.2 B
problem4.3 A + B = 3
problem4.4 3 A + 2 B = 7
Assertion problem4 A = 1 B = 2

Proof

Step Hyp Ref Expression
1 problem4.1 A
2 problem4.2 B
3 problem4.3 A + B = 3
4 problem4.4 3 A + 2 B = 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 A = 1 A
20 1 mulid2i 1 A = A
21 19 20 eqtri 3 2 A = A
22 21 eqcomi A = 3 2 A
23 14 15 1 subdiri 3 2 A = 3 A 2 A
24 22 23 eqtri A = 3 A 2 A
25 24 oveq1i A + 6 = 3 A - 2 A + 6
26 14 1 mulcli 3 A
27 15 1 mulcli 2 A
28 subadd23 3 A 2 A 6 3 A - 2 A + 6 = 3 A + 6 - 2 A
29 26 27 8 28 mp3an 3 A - 2 A + 6 = 3 A + 6 - 2 A
30 3t2e6 3 2 = 6
31 1 15 mulcomi A 2 = 2 A
32 30 31 oveq12i 3 2 A 2 = 6 2 A
33 32 eqcomi 6 2 A = 3 2 A 2
34 14 1 15 subdiri 3 A 2 = 3 2 A 2
35 34 eqcomi 3 2 A 2 = 3 A 2
36 14 1 subcli 3 A
37 15 36 mulcomi 2 3 A = 3 A 2
38 37 eqcomi 3 A 2 = 2 3 A
39 14 1 2 3 subaddrii 3 A = B
40 39 eqcomi B = 3 A
41 40 oveq2i 2 B = 2 3 A
42 41 eqcomi 2 3 A = 2 B
43 38 42 eqtri 3 A 2 = 2 B
44 35 43 eqtri 3 2 A 2 = 2 B
45 33 44 eqtri 6 2 A = 2 B
46 45 eqcomi 2 B = 6 2 A
47 46 oveq2i 3 A + 2 B = 3 A + 6 - 2 A
48 47 eqcomi 3 A + 6 - 2 A = 3 A + 2 B
49 29 48 eqtri 3 A - 2 A + 6 = 3 A + 2 B
50 25 49 eqtri A + 6 = 3 A + 2 B
51 50 4 eqtri A + 6 = 7
52 6 8 1 subadd2i 7 6 = A A + 6 = 7
53 52 biimpri A + 6 = 7 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 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 A = 2
62 40 61 eqtri B = 2
63 56 62 pm3.2i A = 1 B = 2