Metamath Proof Explorer


Theorem halfthird

Description: Half minus a third. (Contributed by Scott Fenton, 8-Jul-2015)

Ref Expression
Assertion halfthird ( ( 1 / 2 ) − ( 1 / 3 ) ) = ( 1 / 6 )

Proof

Step Hyp Ref Expression
1 2cn 2 ∈ ℂ
2 3cn 3 ∈ ℂ
3 2ne0 2 ≠ 0
4 3ne0 3 ≠ 0
5 1 2 3 4 subreci ( ( 1 / 2 ) − ( 1 / 3 ) ) = ( ( 3 − 2 ) / ( 2 · 3 ) )
6 ax-1cn 1 ∈ ℂ
7 2p1e3 ( 2 + 1 ) = 3
8 2 1 6 7 subaddrii ( 3 − 2 ) = 1
9 3t2e6 ( 3 · 2 ) = 6
10 2 1 9 mulcomli ( 2 · 3 ) = 6
11 8 10 oveq12i ( ( 3 − 2 ) / ( 2 · 3 ) ) = ( 1 / 6 )
12 5 11 eqtri ( ( 1 / 2 ) − ( 1 / 3 ) ) = ( 1 / 6 )