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