Metamath Proof Explorer

Theorem halfpm6th

Description: One half plus or minus one sixth. (Contributed by Paul Chapman, 17-Jan-2008)

Ref Expression
Assertion halfpm6th 
|- ( ( ( 1 / 2 ) - ( 1 / 6 ) ) = ( 1 / 3 ) /\ ( ( 1 / 2 ) + ( 1 / 6 ) ) = ( 2 / 3 ) )

Proof

Step Hyp Ref Expression
1 3cn 
 |-  3 e. CC
2 ax-1cn 
 |-  1 e. CC
3 2cn 
 |-  2 e. CC
4 3ne0 
 |-  3 =/= 0
5 2ne0 
 |-  2 =/= 0
6 1 1 2 3 4 5 divmuldivi 
 |-  ( ( 3 / 3 ) x. ( 1 / 2 ) ) = ( ( 3 x. 1 ) / ( 3 x. 2 ) )
7 1 4 dividi 
 |-  ( 3 / 3 ) = 1
8 7 oveq1i 
 |-  ( ( 3 / 3 ) x. ( 1 / 2 ) ) = ( 1 x. ( 1 / 2 ) )
9 halfcn 
 |-  ( 1 / 2 ) e. CC
10 9 mulid2i 
 |-  ( 1 x. ( 1 / 2 ) ) = ( 1 / 2 )
11 8 10 eqtri 
 |-  ( ( 3 / 3 ) x. ( 1 / 2 ) ) = ( 1 / 2 )
12 1 mulid1i 
 |-  ( 3 x. 1 ) = 3
13 3t2e6 
 |-  ( 3 x. 2 ) = 6
14 12 13 oveq12i 
 |-  ( ( 3 x. 1 ) / ( 3 x. 2 ) ) = ( 3 / 6 )
15 6 11 14 3eqtr3i 
 |-  ( 1 / 2 ) = ( 3 / 6 )
16 15 oveq1i 
 |-  ( ( 1 / 2 ) - ( 1 / 6 ) ) = ( ( 3 / 6 ) - ( 1 / 6 ) )
17 6cn 
 |-  6 e. CC
18 6re 
 |-  6 e. RR
19 6pos 
 |-  0 < 6
20 18 19 gt0ne0ii 
 |-  6 =/= 0
21 17 20 pm3.2i 
 |-  ( 6 e. CC /\ 6 =/= 0 )
22 divsubdir 
 |-  ( ( 3 e. CC /\ 1 e. CC /\ ( 6 e. CC /\ 6 =/= 0 ) ) -> ( ( 3 - 1 ) / 6 ) = ( ( 3 / 6 ) - ( 1 / 6 ) ) )
23 1 2 21 22 mp3an 
 |-  ( ( 3 - 1 ) / 6 ) = ( ( 3 / 6 ) - ( 1 / 6 ) )
24 3m1e2 
 |-  ( 3 - 1 ) = 2
25 24 oveq1i 
 |-  ( ( 3 - 1 ) / 6 ) = ( 2 / 6 )
26 3 mulid2i 
 |-  ( 1 x. 2 ) = 2
27 26 13 oveq12i 
 |-  ( ( 1 x. 2 ) / ( 3 x. 2 ) ) = ( 2 / 6 )
28 3 5 dividi 
 |-  ( 2 / 2 ) = 1
29 28 oveq2i 
 |-  ( ( 1 / 3 ) x. ( 2 / 2 ) ) = ( ( 1 / 3 ) x. 1 )
30 2 1 3 3 4 5 divmuldivi 
 |-  ( ( 1 / 3 ) x. ( 2 / 2 ) ) = ( ( 1 x. 2 ) / ( 3 x. 2 ) )
31 1 4 reccli 
 |-  ( 1 / 3 ) e. CC
32 31 mulid1i 
 |-  ( ( 1 / 3 ) x. 1 ) = ( 1 / 3 )
33 29 30 32 3eqtr3i 
 |-  ( ( 1 x. 2 ) / ( 3 x. 2 ) ) = ( 1 / 3 )
34 25 27 33 3eqtr2i 
 |-  ( ( 3 - 1 ) / 6 ) = ( 1 / 3 )
35 16 23 34 3eqtr2i 
 |-  ( ( 1 / 2 ) - ( 1 / 6 ) ) = ( 1 / 3 )
36 1 2 17 20 divdiri 
 |-  ( ( 3 + 1 ) / 6 ) = ( ( 3 / 6 ) + ( 1 / 6 ) )
37 df-4 
 |-  4 = ( 3 + 1 )
38 37 oveq1i 
 |-  ( 4 / 6 ) = ( ( 3 + 1 ) / 6 )
39 15 oveq1i 
 |-  ( ( 1 / 2 ) + ( 1 / 6 ) ) = ( ( 3 / 6 ) + ( 1 / 6 ) )
40 36 38 39 3eqtr4ri 
 |-  ( ( 1 / 2 ) + ( 1 / 6 ) ) = ( 4 / 6 )
41 2t2e4 
 |-  ( 2 x. 2 ) = 4
42 41 13 oveq12i 
 |-  ( ( 2 x. 2 ) / ( 3 x. 2 ) ) = ( 4 / 6 )
43 28 oveq2i 
 |-  ( ( 2 / 3 ) x. ( 2 / 2 ) ) = ( ( 2 / 3 ) x. 1 )
44 3 1 3 3 4 5 divmuldivi 
 |-  ( ( 2 / 3 ) x. ( 2 / 2 ) ) = ( ( 2 x. 2 ) / ( 3 x. 2 ) )
45 3 1 4 divcli 
 |-  ( 2 / 3 ) e. CC
46 45 mulid1i 
 |-  ( ( 2 / 3 ) x. 1 ) = ( 2 / 3 )
47 43 44 46 3eqtr3i 
 |-  ( ( 2 x. 2 ) / ( 3 x. 2 ) ) = ( 2 / 3 )
48 40 42 47 3eqtr2i 
 |-  ( ( 1 / 2 ) + ( 1 / 6 ) ) = ( 2 / 3 )
49 35 48 pm3.2i 
 |-  ( ( ( 1 / 2 ) - ( 1 / 6 ) ) = ( 1 / 3 ) /\ ( ( 1 / 2 ) + ( 1 / 6 ) ) = ( 2 / 3 ) )