Metamath Proof Explorer

Theorem halfpm6th

Description: One half plus or minus one sixth. (Contributed by Paul Chapman, 17-Jan-2008) (Proof shortened by SN, 22-Oct-2025)

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 3ne0 
 |-  3 =/= 0
3 1 2 reccli 
 |-  ( 1 / 3 ) e. CC
4 6cn 
 |-  6 e. CC
5 6re 
 |-  6 e. RR
6 6pos 
 |-  0 < 6
7 5 6 gt0ne0ii 
 |-  6 =/= 0
8 4 7 reccli 
 |-  ( 1 / 6 ) e. CC
9 halfcn 
 |-  ( 1 / 2 ) e. CC
10 3 9 pncan3i 
 |-  ( ( 1 / 3 ) + ( ( 1 / 2 ) - ( 1 / 3 ) ) ) = ( 1 / 2 )
11 halfthird 
 |-  ( ( 1 / 2 ) - ( 1 / 3 ) ) = ( 1 / 6 )
12 11 oveq2i 
 |-  ( ( 1 / 3 ) + ( ( 1 / 2 ) - ( 1 / 3 ) ) ) = ( ( 1 / 3 ) + ( 1 / 6 ) )
13 10 12 eqtr3i 
 |-  ( 1 / 2 ) = ( ( 1 / 3 ) + ( 1 / 6 ) )
14 3 8 13 mvrraddi 
 |-  ( ( 1 / 2 ) - ( 1 / 6 ) ) = ( 1 / 3 )
15 11 oveq2i 
 |-  ( ( 1 / 2 ) + ( ( 1 / 2 ) - ( 1 / 3 ) ) ) = ( ( 1 / 2 ) + ( 1 / 6 ) )
16 9 9 3 addsubassi 
 |-  ( ( ( 1 / 2 ) + ( 1 / 2 ) ) - ( 1 / 3 ) ) = ( ( 1 / 2 ) + ( ( 1 / 2 ) - ( 1 / 3 ) ) )
17 2cn 
 |-  2 e. CC
18 17 1 2 divcli 
 |-  ( 2 / 3 ) e. CC
19 ax-1cn 
 |-  1 e. CC
20 2halves 
 |-  ( 1 e. CC -> ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1 )
21 19 20 ax-mp 
 |-  ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1
22 2p1e3 
 |-  ( 2 + 1 ) = 3
23 22 oveq1i 
 |-  ( ( 2 + 1 ) / 3 ) = ( 3 / 3 )
24 1 2 dividi 
 |-  ( 3 / 3 ) = 1
25 23 24 eqtri 
 |-  ( ( 2 + 1 ) / 3 ) = 1
26 17 19 1 2 divdiri 
 |-  ( ( 2 + 1 ) / 3 ) = ( ( 2 / 3 ) + ( 1 / 3 ) )
27 21 25 26 3eqtr2i 
 |-  ( ( 1 / 2 ) + ( 1 / 2 ) ) = ( ( 2 / 3 ) + ( 1 / 3 ) )
28 18 3 27 mvrraddi 
 |-  ( ( ( 1 / 2 ) + ( 1 / 2 ) ) - ( 1 / 3 ) ) = ( 2 / 3 )
29 16 28 eqtr3i 
 |-  ( ( 1 / 2 ) + ( ( 1 / 2 ) - ( 1 / 3 ) ) ) = ( 2 / 3 )
30 15 29 eqtr3i 
 |-  ( ( 1 / 2 ) + ( 1 / 6 ) ) = ( 2 / 3 )
31 14 30 pm3.2i 
 |-  ( ( ( 1 / 2 ) - ( 1 / 6 ) ) = ( 1 / 3 ) /\ ( ( 1 / 2 ) + ( 1 / 6 ) ) = ( 2 / 3 ) )