Proof of Theorem halfpm6th
Step | Hyp | Ref
| Expression |
1 | | 3cn 8914 |
. . . . . 6
⊢ 3 ∈
ℂ |
2 | | ax-1cn 7828 |
. . . . . 6
⊢ 1 ∈
ℂ |
3 | | 2cn 8910 |
. . . . . 6
⊢ 2 ∈
ℂ |
4 | | 3re 8913 |
. . . . . . 7
⊢ 3 ∈
ℝ |
5 | | 3pos 8933 |
. . . . . . 7
⊢ 0 <
3 |
6 | 4, 5 | gt0ap0ii 8508 |
. . . . . 6
⊢ 3 #
0 |
7 | | 2ap0 8932 |
. . . . . 6
⊢ 2 #
0 |
8 | 1, 1, 2, 3, 6, 7 | divmuldivapi 8650 |
. . . . 5
⊢ ((3 / 3)
· (1 / 2)) = ((3 · 1) / (3 · 2)) |
9 | 1, 6 | dividapi 8623 |
. . . . . . 7
⊢ (3 / 3) =
1 |
10 | 9 | oveq1i 5837 |
. . . . . 6
⊢ ((3 / 3)
· (1 / 2)) = (1 · (1 / 2)) |
11 | | halfcn 9053 |
. . . . . . 7
⊢ (1 / 2)
∈ ℂ |
12 | 11 | mulid2i 7884 |
. . . . . 6
⊢ (1
· (1 / 2)) = (1 / 2) |
13 | 10, 12 | eqtri 2178 |
. . . . 5
⊢ ((3 / 3)
· (1 / 2)) = (1 / 2) |
14 | 1 | mulid1i 7883 |
. . . . . 6
⊢ (3
· 1) = 3 |
15 | | 3t2e6 8995 |
. . . . . 6
⊢ (3
· 2) = 6 |
16 | 14, 15 | oveq12i 5839 |
. . . . 5
⊢ ((3
· 1) / (3 · 2)) = (3 / 6) |
17 | 8, 13, 16 | 3eqtr3i 2186 |
. . . 4
⊢ (1 / 2) =
(3 / 6) |
18 | 17 | oveq1i 5837 |
. . 3
⊢ ((1 / 2)
− (1 / 6)) = ((3 / 6) − (1 / 6)) |
19 | | 6cn 8921 |
. . . . 5
⊢ 6 ∈
ℂ |
20 | | 6re 8920 |
. . . . . 6
⊢ 6 ∈
ℝ |
21 | | 6pos 8940 |
. . . . . 6
⊢ 0 <
6 |
22 | 20, 21 | gt0ap0ii 8508 |
. . . . 5
⊢ 6 #
0 |
23 | 19, 22 | pm3.2i 270 |
. . . 4
⊢ (6 ∈
ℂ ∧ 6 # 0) |
24 | | divsubdirap 8586 |
. . . 4
⊢ ((3
∈ ℂ ∧ 1 ∈ ℂ ∧ (6 ∈ ℂ ∧ 6 # 0))
→ ((3 − 1) / 6) = ((3 / 6) − (1 / 6))) |
25 | 1, 2, 23, 24 | mp3an 1319 |
. . 3
⊢ ((3
− 1) / 6) = ((3 / 6) − (1 / 6)) |
26 | | 3m1e2 8959 |
. . . . 5
⊢ (3
− 1) = 2 |
27 | 26 | oveq1i 5837 |
. . . 4
⊢ ((3
− 1) / 6) = (2 / 6) |
28 | 3 | mulid2i 7884 |
. . . . 5
⊢ (1
· 2) = 2 |
29 | 28, 15 | oveq12i 5839 |
. . . 4
⊢ ((1
· 2) / (3 · 2)) = (2 / 6) |
30 | 3, 7 | dividapi 8623 |
. . . . . 6
⊢ (2 / 2) =
1 |
31 | 30 | oveq2i 5838 |
. . . . 5
⊢ ((1 / 3)
· (2 / 2)) = ((1 / 3) · 1) |
32 | 2, 1, 3, 3, 6, 7 | divmuldivapi 8650 |
. . . . 5
⊢ ((1 / 3)
· (2 / 2)) = ((1 · 2) / (3 · 2)) |
33 | 1, 6 | recclapi 8620 |
. . . . . 6
⊢ (1 / 3)
∈ ℂ |
34 | 33 | mulid1i 7883 |
. . . . 5
⊢ ((1 / 3)
· 1) = (1 / 3) |
35 | 31, 32, 34 | 3eqtr3i 2186 |
. . . 4
⊢ ((1
· 2) / (3 · 2)) = (1 / 3) |
36 | 27, 29, 35 | 3eqtr2i 2184 |
. . 3
⊢ ((3
− 1) / 6) = (1 / 3) |
37 | 18, 25, 36 | 3eqtr2i 2184 |
. 2
⊢ ((1 / 2)
− (1 / 6)) = (1 / 3) |
38 | 1, 2, 19, 22 | divdirapi 8647 |
. . . 4
⊢ ((3 + 1)
/ 6) = ((3 / 6) + (1 / 6)) |
39 | | df-4 8900 |
. . . . 5
⊢ 4 = (3 +
1) |
40 | 39 | oveq1i 5837 |
. . . 4
⊢ (4 / 6) =
((3 + 1) / 6) |
41 | 17 | oveq1i 5837 |
. . . 4
⊢ ((1 / 2)
+ (1 / 6)) = ((3 / 6) + (1 / 6)) |
42 | 38, 40, 41 | 3eqtr4ri 2189 |
. . 3
⊢ ((1 / 2)
+ (1 / 6)) = (4 / 6) |
43 | | 2t2e4 8993 |
. . . 4
⊢ (2
· 2) = 4 |
44 | 43, 15 | oveq12i 5839 |
. . 3
⊢ ((2
· 2) / (3 · 2)) = (4 / 6) |
45 | 30 | oveq2i 5838 |
. . . 4
⊢ ((2 / 3)
· (2 / 2)) = ((2 / 3) · 1) |
46 | 3, 1, 3, 3, 6, 7 | divmuldivapi 8650 |
. . . 4
⊢ ((2 / 3)
· (2 / 2)) = ((2 · 2) / (3 · 2)) |
47 | 3, 1, 6 | divclapi 8632 |
. . . . 5
⊢ (2 / 3)
∈ ℂ |
48 | 47 | mulid1i 7883 |
. . . 4
⊢ ((2 / 3)
· 1) = (2 / 3) |
49 | 45, 46, 48 | 3eqtr3i 2186 |
. . 3
⊢ ((2
· 2) / (3 · 2)) = (2 / 3) |
50 | 42, 44, 49 | 3eqtr2i 2184 |
. 2
⊢ ((1 / 2)
+ (1 / 6)) = (2 / 3) |
51 | 37, 50 | pm3.2i 270 |
1
⊢ (((1 / 2)
− (1 / 6)) = (1 / 3) ∧ ((1 / 2) + (1 / 6)) = (2 /
3)) |