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 e. CC
problem4.2 
|- B e. CC
problem4.3 
|- ( A + B ) = 3
problem4.4 
|- ( ( 3 x. A ) + ( 2 x. B ) ) = 7
Assertion problem4 
|- ( A = 1 /\ B = 2 )

Proof

Step Hyp Ref Expression
1 problem4.1 
 |-  A e. CC
2 problem4.2 
 |-  B e. CC
3 problem4.3 
 |-  ( A + B ) = 3
4 problem4.4 
 |-  ( ( 3 x. A ) + ( 2 x. B ) ) = 7
5 7re 
 |-  7 e. RR
6 5 recni 
 |-  7 e. CC
7 6re 
 |-  6 e. RR
8 7 recni 
 |-  6 e. CC
9 ax-1cn 
 |-  1 e. CC
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 e. CC
15 2cn 
 |-  2 e. CC
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 ) x. A ) = ( 1 x. A )
20 1 mulid2i 
 |-  ( 1 x. A ) = A
21 19 20 eqtri 
 |-  ( ( 3 - 2 ) x. A ) = A
22 21 eqcomi 
 |-  A = ( ( 3 - 2 ) x. A )
23 14 15 1 subdiri 
 |-  ( ( 3 - 2 ) x. A ) = ( ( 3 x. A ) - ( 2 x. A ) )
24 22 23 eqtri 
 |-  A = ( ( 3 x. A ) - ( 2 x. A ) )
25 24 oveq1i 
 |-  ( A + 6 ) = ( ( ( 3 x. A ) - ( 2 x. A ) ) + 6 )
26 14 1 mulcli 
 |-  ( 3 x. A ) e. CC
27 15 1 mulcli 
 |-  ( 2 x. A ) e. CC
28 subadd23 
 |-  ( ( ( 3 x. A ) e. CC /\ ( 2 x. A ) e. CC /\ 6 e. CC ) -> ( ( ( 3 x. A ) - ( 2 x. A ) ) + 6 ) = ( ( 3 x. A ) + ( 6 - ( 2 x. A ) ) ) )
29 26 27 8 28 mp3an 
 |-  ( ( ( 3 x. A ) - ( 2 x. A ) ) + 6 ) = ( ( 3 x. A ) + ( 6 - ( 2 x. A ) ) )
30 3t2e6 
 |-  ( 3 x. 2 ) = 6
31 1 15 mulcomi 
 |-  ( A x. 2 ) = ( 2 x. A )
32 30 31 oveq12i 
 |-  ( ( 3 x. 2 ) - ( A x. 2 ) ) = ( 6 - ( 2 x. A ) )
33 32 eqcomi 
 |-  ( 6 - ( 2 x. A ) ) = ( ( 3 x. 2 ) - ( A x. 2 ) )
34 14 1 15 subdiri 
 |-  ( ( 3 - A ) x. 2 ) = ( ( 3 x. 2 ) - ( A x. 2 ) )
35 34 eqcomi 
 |-  ( ( 3 x. 2 ) - ( A x. 2 ) ) = ( ( 3 - A ) x. 2 )
36 14 1 subcli 
 |-  ( 3 - A ) e. CC
37 15 36 mulcomi 
 |-  ( 2 x. ( 3 - A ) ) = ( ( 3 - A ) x. 2 )
38 37 eqcomi 
 |-  ( ( 3 - A ) x. 2 ) = ( 2 x. ( 3 - A ) )
39 14 1 2 3 subaddrii 
 |-  ( 3 - A ) = B
40 39 eqcomi 
 |-  B = ( 3 - A )
41 40 oveq2i 
 |-  ( 2 x. B ) = ( 2 x. ( 3 - A ) )
42 41 eqcomi 
 |-  ( 2 x. ( 3 - A ) ) = ( 2 x. B )
43 38 42 eqtri 
 |-  ( ( 3 - A ) x. 2 ) = ( 2 x. B )
44 35 43 eqtri 
 |-  ( ( 3 x. 2 ) - ( A x. 2 ) ) = ( 2 x. B )
45 33 44 eqtri 
 |-  ( 6 - ( 2 x. A ) ) = ( 2 x. B )
46 45 eqcomi 
 |-  ( 2 x. B ) = ( 6 - ( 2 x. A ) )
47 46 oveq2i 
 |-  ( ( 3 x. A ) + ( 2 x. B ) ) = ( ( 3 x. A ) + ( 6 - ( 2 x. A ) ) )
48 47 eqcomi 
 |-  ( ( 3 x. A ) + ( 6 - ( 2 x. A ) ) ) = ( ( 3 x. A ) + ( 2 x. B ) )
49 29 48 eqtri 
 |-  ( ( ( 3 x. A ) - ( 2 x. A ) ) + 6 ) = ( ( 3 x. A ) + ( 2 x. B ) )
50 25 49 eqtri 
 |-  ( A + 6 ) = ( ( 3 x. A ) + ( 2 x. 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 )