This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ ℂ
2 3ne0 ⊢ 3 ≠ 0
3 1 2 reccli ⊢ ( 1 / 3 ) ∈ ℂ
4 6cn ⊢ 6 ∈ ℂ
5 6re ⊢ 6 ∈ ℝ
6 6pos ⊢ 0 < 6
7 5 6 gt0ne0ii ⊢ 6 ≠ 0
8 4 7 reccli ⊢ ( 1 / 6 ) ∈ ℂ
9 halfcn ⊢ ( 1 / 2 ) ∈ ℂ
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 ∈ ℂ
18 17 1 2 divcli ⊢ ( 2 / 3 ) ∈ ℂ
19 ax-1cn ⊢ 1 ∈ ℂ
20 2halves ⊢ ( 1 ∈ ℂ → ( ( 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 ) )