Proof of Theorem halfpm6th
Step | Hyp | Ref
| Expression |
1 | | 3cn 8953 |
. . . . . 6
⊢ 3 ∈
ℂ |
2 | | ax-1cn 7867 |
. . . . . 6
⊢ 1 ∈
ℂ |
3 | | 2cn 8949 |
. . . . . 6
⊢ 2 ∈
ℂ |
4 | | 3re 8952 |
. . . . . . 7
⊢ 3 ∈
ℝ |
5 | | 3pos 8972 |
. . . . . . 7
⊢ 0 <
3 |
6 | 4, 5 | gt0ap0ii 8547 |
. . . . . 6
⊢ 3 #
0 |
7 | | 2ap0 8971 |
. . . . . 6
⊢ 2 #
0 |
8 | 1, 1, 2, 3, 6, 7 | divmuldivapi 8689 |
. . . . 5
⊢ ((3 / 3)
· (1 / 2)) = ((3 · 1) / (3 · 2)) |
9 | 1, 6 | dividapi 8662 |
. . . . . . 7
⊢ (3 / 3) =
1 |
10 | 9 | oveq1i 5863 |
. . . . . 6
⊢ ((3 / 3)
· (1 / 2)) = (1 · (1 / 2)) |
11 | | halfcn 9092 |
. . . . . . 7
⊢ (1 / 2)
∈ ℂ |
12 | 11 | mulid2i 7923 |
. . . . . 6
⊢ (1
· (1 / 2)) = (1 / 2) |
13 | 10, 12 | eqtri 2191 |
. . . . 5
⊢ ((3 / 3)
· (1 / 2)) = (1 / 2) |
14 | 1 | mulid1i 7922 |
. . . . . 6
⊢ (3
· 1) = 3 |
15 | | 3t2e6 9034 |
. . . . . 6
⊢ (3
· 2) = 6 |
16 | 14, 15 | oveq12i 5865 |
. . . . 5
⊢ ((3
· 1) / (3 · 2)) = (3 / 6) |
17 | 8, 13, 16 | 3eqtr3i 2199 |
. . . 4
⊢ (1 / 2) =
(3 / 6) |
18 | 17 | oveq1i 5863 |
. . 3
⊢ ((1 / 2)
− (1 / 6)) = ((3 / 6) − (1 / 6)) |
19 | | 6cn 8960 |
. . . . 5
⊢ 6 ∈
ℂ |
20 | | 6re 8959 |
. . . . . 6
⊢ 6 ∈
ℝ |
21 | | 6pos 8979 |
. . . . . 6
⊢ 0 <
6 |
22 | 20, 21 | gt0ap0ii 8547 |
. . . . 5
⊢ 6 #
0 |
23 | 19, 22 | pm3.2i 270 |
. . . 4
⊢ (6 ∈
ℂ ∧ 6 # 0) |
24 | | divsubdirap 8625 |
. . . 4
⊢ ((3
∈ ℂ ∧ 1 ∈ ℂ ∧ (6 ∈ ℂ ∧ 6 # 0))
→ ((3 − 1) / 6) = ((3 / 6) − (1 / 6))) |
25 | 1, 2, 23, 24 | mp3an 1332 |
. . 3
⊢ ((3
− 1) / 6) = ((3 / 6) − (1 / 6)) |
26 | | 3m1e2 8998 |
. . . . 5
⊢ (3
− 1) = 2 |
27 | 26 | oveq1i 5863 |
. . . 4
⊢ ((3
− 1) / 6) = (2 / 6) |
28 | 3 | mulid2i 7923 |
. . . . 5
⊢ (1
· 2) = 2 |
29 | 28, 15 | oveq12i 5865 |
. . . 4
⊢ ((1
· 2) / (3 · 2)) = (2 / 6) |
30 | 3, 7 | dividapi 8662 |
. . . . . 6
⊢ (2 / 2) =
1 |
31 | 30 | oveq2i 5864 |
. . . . 5
⊢ ((1 / 3)
· (2 / 2)) = ((1 / 3) · 1) |
32 | 2, 1, 3, 3, 6, 7 | divmuldivapi 8689 |
. . . . 5
⊢ ((1 / 3)
· (2 / 2)) = ((1 · 2) / (3 · 2)) |
33 | 1, 6 | recclapi 8659 |
. . . . . 6
⊢ (1 / 3)
∈ ℂ |
34 | 33 | mulid1i 7922 |
. . . . 5
⊢ ((1 / 3)
· 1) = (1 / 3) |
35 | 31, 32, 34 | 3eqtr3i 2199 |
. . . 4
⊢ ((1
· 2) / (3 · 2)) = (1 / 3) |
36 | 27, 29, 35 | 3eqtr2i 2197 |
. . 3
⊢ ((3
− 1) / 6) = (1 / 3) |
37 | 18, 25, 36 | 3eqtr2i 2197 |
. 2
⊢ ((1 / 2)
− (1 / 6)) = (1 / 3) |
38 | 1, 2, 19, 22 | divdirapi 8686 |
. . . 4
⊢ ((3 + 1)
/ 6) = ((3 / 6) + (1 / 6)) |
39 | | df-4 8939 |
. . . . 5
⊢ 4 = (3 +
1) |
40 | 39 | oveq1i 5863 |
. . . 4
⊢ (4 / 6) =
((3 + 1) / 6) |
41 | 17 | oveq1i 5863 |
. . . 4
⊢ ((1 / 2)
+ (1 / 6)) = ((3 / 6) + (1 / 6)) |
42 | 38, 40, 41 | 3eqtr4ri 2202 |
. . 3
⊢ ((1 / 2)
+ (1 / 6)) = (4 / 6) |
43 | | 2t2e4 9032 |
. . . 4
⊢ (2
· 2) = 4 |
44 | 43, 15 | oveq12i 5865 |
. . 3
⊢ ((2
· 2) / (3 · 2)) = (4 / 6) |
45 | 30 | oveq2i 5864 |
. . . 4
⊢ ((2 / 3)
· (2 / 2)) = ((2 / 3) · 1) |
46 | 3, 1, 3, 3, 6, 7 | divmuldivapi 8689 |
. . . 4
⊢ ((2 / 3)
· (2 / 2)) = ((2 · 2) / (3 · 2)) |
47 | 3, 1, 6 | divclapi 8671 |
. . . . 5
⊢ (2 / 3)
∈ ℂ |
48 | 47 | mulid1i 7922 |
. . . 4
⊢ ((2 / 3)
· 1) = (2 / 3) |
49 | 45, 46, 48 | 3eqtr3i 2199 |
. . 3
⊢ ((2
· 2) / (3 · 2)) = (2 / 3) |
50 | 42, 44, 49 | 3eqtr2i 2197 |
. 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)) |