Metamath Proof Explorer

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 x. ; 1 0 ) + 5 ) + ( ( 1 x. ; 1 0 ) + 4 ) ) = ( ( 3 x. ; 1 0 ) + 9 )

Proof

Step Hyp Ref Expression
1 2re 
 |-  2 e. RR
2 1 recni 
 |-  2 e. CC
3 10re 
 |-  ; 1 0 e. RR
4 3 recni 
 |-  ; 1 0 e. CC
5 2 4 mulcli 
 |-  ( 2 x. ; 1 0 ) e. CC
6 5re 
 |-  5 e. RR
7 6 recni 
 |-  5 e. CC
8 1re 
 |-  1 e. RR
9 8 recni 
 |-  1 e. CC
10 9 4 mulcli 
 |-  ( 1 x. ; 1 0 ) e. CC
11 4re 
 |-  4 e. RR
12 11 recni 
 |-  4 e. CC
13 5 7 10 12 add4i 
 |-  ( ( ( 2 x. ; 1 0 ) + 5 ) + ( ( 1 x. ; 1 0 ) + 4 ) ) = ( ( ( 2 x. ; 1 0 ) + ( 1 x. ; 1 0 ) ) + ( 5 + 4 ) )
14 2 9 4 adddiri 
 |-  ( ( 2 + 1 ) x. ; 1 0 ) = ( ( 2 x. ; 1 0 ) + ( 1 x. ; 1 0 ) )
15 14 eqcomi 
 |-  ( ( 2 x. ; 1 0 ) + ( 1 x. ; 1 0 ) ) = ( ( 2 + 1 ) x. ; 1 0 )
16 5p4e9 
 |-  ( 5 + 4 ) = 9
17 15 16 oveq12i 
 |-  ( ( ( 2 x. ; 1 0 ) + ( 1 x. ; 1 0 ) ) + ( 5 + 4 ) ) = ( ( ( 2 + 1 ) x. ; 1 0 ) + 9 )
18 df-3 
 |-  3 = ( 2 + 1 )
19 18 eqcomi 
 |-  ( 2 + 1 ) = 3
20 19 oveq1i 
 |-  ( ( 2 + 1 ) x. ; 1 0 ) = ( 3 x. ; 1 0 )
21 20 oveq1i 
 |-  ( ( ( 2 + 1 ) x. ; 1 0 ) + 9 ) = ( ( 3 x. ; 1 0 ) + 9 )
22 13 17 21 3eqtri 
 |-  ( ( ( 2 x. ; 1 0 ) + 5 ) + ( ( 1 x. ; 1 0 ) + 4 ) ) = ( ( 3 x. ; 1 0 ) + 9 )