Metamath Proof Explorer

Theorem 2t6m3t4e0

Description: 2 times 6 minus 3 times 4 equals 0. (Contributed by AV, 24-May-2019)

Ref Expression
Assertion 2t6m3t4e0 
|- ( ( 2 x. 6 ) - ( 3 x. 4 ) ) = 0

Proof

Step Hyp Ref Expression
1 6cn 
 |-  6 e. CC
2 1 2timesi 
 |-  ( 2 x. 6 ) = ( 6 + 6 )
3 2p2e4 
 |-  ( 2 + 2 ) = 4
4 3 eqcomi 
 |-  4 = ( 2 + 2 )
5 4 oveq2i 
 |-  ( 3 x. 4 ) = ( 3 x. ( 2 + 2 ) )
6 3cn 
 |-  3 e. CC
7 2cn 
 |-  2 e. CC
8 6 7 7 adddii 
 |-  ( 3 x. ( 2 + 2 ) ) = ( ( 3 x. 2 ) + ( 3 x. 2 ) )
9 3t2e6 
 |-  ( 3 x. 2 ) = 6
10 9 9 oveq12i 
 |-  ( ( 3 x. 2 ) + ( 3 x. 2 ) ) = ( 6 + 6 )
11 5 8 10 3eqtri 
 |-  ( 3 x. 4 ) = ( 6 + 6 )
12 2 11 oveq12i 
 |-  ( ( 2 x. 6 ) - ( 3 x. 4 ) ) = ( ( 6 + 6 ) - ( 6 + 6 ) )
13 1 1 addcli 
 |-  ( 6 + 6 ) e. CC
14 13 subidi 
 |-  ( ( 6 + 6 ) - ( 6 + 6 ) ) = 0
15 12 14 eqtri 
 |-  ( ( 2 x. 6 ) - ( 3 x. 4 ) ) = 0