Step | Hyp | Ref
| Expression |
1 | | ppncan 8198 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ด โ โ) โ ((๐ด + ๐ต) + (๐ด โ ๐ต)) = (๐ด + ๐ด)) |
2 | 1 | 3anidm13 1296 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) + (๐ด โ ๐ต)) = (๐ด + ๐ด)) |
3 | | 2times 9046 |
. . . . . 6
โข (๐ด โ โ โ (2
ยท ๐ด) = (๐ด + ๐ด)) |
4 | 3 | adantr 276 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (2
ยท ๐ด) = (๐ด + ๐ด)) |
5 | 2, 4 | eqtr4d 2213 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) + (๐ด โ ๐ต)) = (2 ยท ๐ด)) |
6 | 5 | oveq1d 5889 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + ๐ต) + (๐ด โ ๐ต)) / 2) = ((2 ยท ๐ด) / 2)) |
7 | | addcl 7935 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + ๐ต) โ โ) |
8 | | subcl 8155 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โ ๐ต) โ โ) |
9 | | 2cn 8989 |
. . . . . 6
โข 2 โ
โ |
10 | | 2ap0 9011 |
. . . . . 6
โข 2 #
0 |
11 | 9, 10 | pm3.2i 272 |
. . . . 5
โข (2 โ
โ โง 2 # 0) |
12 | | divdirap 8653 |
. . . . 5
โข (((๐ด + ๐ต) โ โ โง (๐ด โ ๐ต) โ โ โง (2 โ โ
โง 2 # 0)) โ (((๐ด +
๐ต) + (๐ด โ ๐ต)) / 2) = (((๐ด + ๐ต) / 2) + ((๐ด โ ๐ต) / 2))) |
13 | 11, 12 | mp3an3 1326 |
. . . 4
โข (((๐ด + ๐ต) โ โ โง (๐ด โ ๐ต) โ โ) โ (((๐ด + ๐ต) + (๐ด โ ๐ต)) / 2) = (((๐ด + ๐ต) / 2) + ((๐ด โ ๐ต) / 2))) |
14 | 7, 8, 13 | syl2anc 411 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + ๐ต) + (๐ด โ ๐ต)) / 2) = (((๐ด + ๐ต) / 2) + ((๐ด โ ๐ต) / 2))) |
15 | | divcanap3 8654 |
. . . . 5
โข ((๐ด โ โ โง 2 โ
โ โง 2 # 0) โ ((2 ยท ๐ด) / 2) = ๐ด) |
16 | 9, 10, 15 | mp3an23 1329 |
. . . 4
โข (๐ด โ โ โ ((2
ยท ๐ด) / 2) = ๐ด) |
17 | 16 | adantr 276 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ ((2
ยท ๐ด) / 2) = ๐ด) |
18 | 6, 14, 17 | 3eqtr3d 2218 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + ๐ต) / 2) + ((๐ด โ ๐ต) / 2)) = ๐ด) |
19 | | pnncan 8197 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) โ (๐ด โ ๐ต)) = (๐ต + ๐ต)) |
20 | 19 | 3anidm23 1297 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) โ (๐ด โ ๐ต)) = (๐ต + ๐ต)) |
21 | | 2times 9046 |
. . . . . 6
โข (๐ต โ โ โ (2
ยท ๐ต) = (๐ต + ๐ต)) |
22 | 21 | adantl 277 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (2
ยท ๐ต) = (๐ต + ๐ต)) |
23 | 20, 22 | eqtr4d 2213 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) โ (๐ด โ ๐ต)) = (2 ยท ๐ต)) |
24 | 23 | oveq1d 5889 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + ๐ต) โ (๐ด โ ๐ต)) / 2) = ((2 ยท ๐ต) / 2)) |
25 | | divsubdirap 8664 |
. . . . 5
โข (((๐ด + ๐ต) โ โ โง (๐ด โ ๐ต) โ โ โง (2 โ โ
โง 2 # 0)) โ (((๐ด +
๐ต) โ (๐ด โ ๐ต)) / 2) = (((๐ด + ๐ต) / 2) โ ((๐ด โ ๐ต) / 2))) |
26 | 11, 25 | mp3an3 1326 |
. . . 4
โข (((๐ด + ๐ต) โ โ โง (๐ด โ ๐ต) โ โ) โ (((๐ด + ๐ต) โ (๐ด โ ๐ต)) / 2) = (((๐ด + ๐ต) / 2) โ ((๐ด โ ๐ต) / 2))) |
27 | 7, 8, 26 | syl2anc 411 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + ๐ต) โ (๐ด โ ๐ต)) / 2) = (((๐ด + ๐ต) / 2) โ ((๐ด โ ๐ต) / 2))) |
28 | | divcanap3 8654 |
. . . . 5
โข ((๐ต โ โ โง 2 โ
โ โง 2 # 0) โ ((2 ยท ๐ต) / 2) = ๐ต) |
29 | 9, 10, 28 | mp3an23 1329 |
. . . 4
โข (๐ต โ โ โ ((2
ยท ๐ต) / 2) = ๐ต) |
30 | 29 | adantl 277 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ ((2
ยท ๐ต) / 2) = ๐ต) |
31 | 24, 27, 30 | 3eqtr3d 2218 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + ๐ต) / 2) โ ((๐ด โ ๐ต) / 2)) = ๐ต) |
32 | 18, 31 | jca 306 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((๐ด + ๐ต) / 2) + ((๐ด โ ๐ต) / 2)) = ๐ด โง (((๐ด + ๐ต) / 2) โ ((๐ด โ ๐ต) / 2)) = ๐ต)) |