Proof of Theorem halfpm6th
| Step | Hyp | Ref
| Expression |
| 1 | | 3cn 12347 |
. . . . . 6
⊢ 3 ∈
ℂ |
| 2 | | ax-1cn 11213 |
. . . . . 6
⊢ 1 ∈
ℂ |
| 3 | | 2cn 12341 |
. . . . . 6
⊢ 2 ∈
ℂ |
| 4 | | 3ne0 12372 |
. . . . . 6
⊢ 3 ≠
0 |
| 5 | | 2ne0 12370 |
. . . . . 6
⊢ 2 ≠
0 |
| 6 | 1, 1, 2, 3, 4, 5 | divmuldivi 12027 |
. . . . 5
⊢ ((3 / 3)
· (1 / 2)) = ((3 · 1) / (3 · 2)) |
| 7 | 1, 4 | dividi 12000 |
. . . . . . 7
⊢ (3 / 3) =
1 |
| 8 | 7 | oveq1i 7441 |
. . . . . 6
⊢ ((3 / 3)
· (1 / 2)) = (1 · (1 / 2)) |
| 9 | | halfcn 12481 |
. . . . . . 7
⊢ (1 / 2)
∈ ℂ |
| 10 | 9 | mullidi 11266 |
. . . . . 6
⊢ (1
· (1 / 2)) = (1 / 2) |
| 11 | 8, 10 | eqtri 2765 |
. . . . 5
⊢ ((3 / 3)
· (1 / 2)) = (1 / 2) |
| 12 | 1 | mulridi 11265 |
. . . . . 6
⊢ (3
· 1) = 3 |
| 13 | | 3t2e6 12432 |
. . . . . 6
⊢ (3
· 2) = 6 |
| 14 | 12, 13 | oveq12i 7443 |
. . . . 5
⊢ ((3
· 1) / (3 · 2)) = (3 / 6) |
| 15 | 6, 11, 14 | 3eqtr3i 2773 |
. . . 4
⊢ (1 / 2) =
(3 / 6) |
| 16 | 15 | oveq1i 7441 |
. . 3
⊢ ((1 / 2)
− (1 / 6)) = ((3 / 6) − (1 / 6)) |
| 17 | | 6cn 12357 |
. . . . 5
⊢ 6 ∈
ℂ |
| 18 | | 6re 12356 |
. . . . . 6
⊢ 6 ∈
ℝ |
| 19 | | 6pos 12376 |
. . . . . 6
⊢ 0 <
6 |
| 20 | 18, 19 | gt0ne0ii 11799 |
. . . . 5
⊢ 6 ≠
0 |
| 21 | 17, 20 | pm3.2i 470 |
. . . 4
⊢ (6 ∈
ℂ ∧ 6 ≠ 0) |
| 22 | | divsubdir 11961 |
. . . 4
⊢ ((3
∈ ℂ ∧ 1 ∈ ℂ ∧ (6 ∈ ℂ ∧ 6 ≠ 0))
→ ((3 − 1) / 6) = ((3 / 6) − (1 / 6))) |
| 23 | 1, 2, 21, 22 | mp3an 1463 |
. . 3
⊢ ((3
− 1) / 6) = ((3 / 6) − (1 / 6)) |
| 24 | | 3m1e2 12394 |
. . . . 5
⊢ (3
− 1) = 2 |
| 25 | 24 | oveq1i 7441 |
. . . 4
⊢ ((3
− 1) / 6) = (2 / 6) |
| 26 | 3 | mullidi 11266 |
. . . . 5
⊢ (1
· 2) = 2 |
| 27 | 26, 13 | oveq12i 7443 |
. . . 4
⊢ ((1
· 2) / (3 · 2)) = (2 / 6) |
| 28 | 3, 5 | dividi 12000 |
. . . . . 6
⊢ (2 / 2) =
1 |
| 29 | 28 | oveq2i 7442 |
. . . . 5
⊢ ((1 / 3)
· (2 / 2)) = ((1 / 3) · 1) |
| 30 | 2, 1, 3, 3, 4, 5 | divmuldivi 12027 |
. . . . 5
⊢ ((1 / 3)
· (2 / 2)) = ((1 · 2) / (3 · 2)) |
| 31 | 1, 4 | reccli 11997 |
. . . . . 6
⊢ (1 / 3)
∈ ℂ |
| 32 | 31 | mulridi 11265 |
. . . . 5
⊢ ((1 / 3)
· 1) = (1 / 3) |
| 33 | 29, 30, 32 | 3eqtr3i 2773 |
. . . 4
⊢ ((1
· 2) / (3 · 2)) = (1 / 3) |
| 34 | 25, 27, 33 | 3eqtr2i 2771 |
. . 3
⊢ ((3
− 1) / 6) = (1 / 3) |
| 35 | 16, 23, 34 | 3eqtr2i 2771 |
. 2
⊢ ((1 / 2)
− (1 / 6)) = (1 / 3) |
| 36 | 1, 2, 17, 20 | divdiri 12024 |
. . . 4
⊢ ((3 + 1)
/ 6) = ((3 / 6) + (1 / 6)) |
| 37 | | df-4 12331 |
. . . . 5
⊢ 4 = (3 +
1) |
| 38 | 37 | oveq1i 7441 |
. . . 4
⊢ (4 / 6) =
((3 + 1) / 6) |
| 39 | 15 | oveq1i 7441 |
. . . 4
⊢ ((1 / 2)
+ (1 / 6)) = ((3 / 6) + (1 / 6)) |
| 40 | 36, 38, 39 | 3eqtr4ri 2776 |
. . 3
⊢ ((1 / 2)
+ (1 / 6)) = (4 / 6) |
| 41 | | 2t2e4 12430 |
. . . 4
⊢ (2
· 2) = 4 |
| 42 | 41, 13 | oveq12i 7443 |
. . 3
⊢ ((2
· 2) / (3 · 2)) = (4 / 6) |
| 43 | 28 | oveq2i 7442 |
. . . 4
⊢ ((2 / 3)
· (2 / 2)) = ((2 / 3) · 1) |
| 44 | 3, 1, 3, 3, 4, 5 | divmuldivi 12027 |
. . . 4
⊢ ((2 / 3)
· (2 / 2)) = ((2 · 2) / (3 · 2)) |
| 45 | 3, 1, 4 | divcli 12009 |
. . . . 5
⊢ (2 / 3)
∈ ℂ |
| 46 | 45 | mulridi 11265 |
. . . 4
⊢ ((2 / 3)
· 1) = (2 / 3) |
| 47 | 43, 44, 46 | 3eqtr3i 2773 |
. . 3
⊢ ((2
· 2) / (3 · 2)) = (2 / 3) |
| 48 | 40, 42, 47 | 3eqtr2i 2771 |
. 2
⊢ ((1 / 2)
+ (1 / 6)) = (2 / 3) |
| 49 | 35, 48 | pm3.2i 470 |
1
⊢ (((1 / 2)
− (1 / 6)) = (1 / 3) ∧ ((1 / 2) + (1 / 6)) = (2 /
3)) |