Description: Half minus a third. (Contributed by Scott Fenton, 8-Jul-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | halfthird | ⊢ ( ( 1 / 2 ) − ( 1 / 3 ) ) = ( 1 / 6 ) |
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 ) |