Step | Hyp | Ref
| Expression |
1 | | ppncan 11377 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ด โ โ) โ ((๐ด + ๐ต) + (๐ด โ ๐ต)) = (๐ด + ๐ด)) |
2 | 1 | 3anidm13 1421 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) + (๐ด โ ๐ต)) = (๐ด + ๐ด)) |
3 | | 2times 12223 |
. . . . . 6
โข (๐ด โ โ โ (2
ยท ๐ด) = (๐ด + ๐ด)) |
4 | 3 | adantr 482 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (2
ยท ๐ด) = (๐ด + ๐ด)) |
5 | 2, 4 | eqtr4d 2781 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) + (๐ด โ ๐ต)) = (2 ยท ๐ด)) |
6 | 5 | oveq1d 7365 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + ๐ต) + (๐ด โ ๐ต)) / 2) = ((2 ยท ๐ด) / 2)) |
7 | | addcl 11067 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + ๐ต) โ โ) |
8 | | subcl 11334 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โ ๐ต) โ โ) |
9 | | 2cnne0 12297 |
. . . . 5
โข (2 โ
โ โง 2 โ 0) |
10 | | divdir 11772 |
. . . . 5
โข (((๐ด + ๐ต) โ โ โง (๐ด โ ๐ต) โ โ โง (2 โ โ
โง 2 โ 0)) โ (((๐ด + ๐ต) + (๐ด โ ๐ต)) / 2) = (((๐ด + ๐ต) / 2) + ((๐ด โ ๐ต) / 2))) |
11 | 9, 10 | mp3an3 1451 |
. . . 4
โข (((๐ด + ๐ต) โ โ โง (๐ด โ ๐ต) โ โ) โ (((๐ด + ๐ต) + (๐ด โ ๐ต)) / 2) = (((๐ด + ๐ต) / 2) + ((๐ด โ ๐ต) / 2))) |
12 | 7, 8, 11 | syl2anc 585 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + ๐ต) + (๐ด โ ๐ต)) / 2) = (((๐ด + ๐ต) / 2) + ((๐ด โ ๐ต) / 2))) |
13 | | 2cn 12162 |
. . . . 5
โข 2 โ
โ |
14 | | 2ne0 12191 |
. . . . 5
โข 2 โ
0 |
15 | | divcan3 11773 |
. . . . 5
โข ((๐ด โ โ โง 2 โ
โ โง 2 โ 0) โ ((2 ยท ๐ด) / 2) = ๐ด) |
16 | 13, 14, 15 | mp3an23 1454 |
. . . 4
โข (๐ด โ โ โ ((2
ยท ๐ด) / 2) = ๐ด) |
17 | 16 | adantr 482 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ ((2
ยท ๐ด) / 2) = ๐ด) |
18 | 6, 12, 17 | 3eqtr3d 2786 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + ๐ต) / 2) + ((๐ด โ ๐ต) / 2)) = ๐ด) |
19 | | pnncan 11376 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) โ (๐ด โ ๐ต)) = (๐ต + ๐ต)) |
20 | 19 | 3anidm23 1422 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) โ (๐ด โ ๐ต)) = (๐ต + ๐ต)) |
21 | | 2times 12223 |
. . . . . 6
โข (๐ต โ โ โ (2
ยท ๐ต) = (๐ต + ๐ต)) |
22 | 21 | adantl 483 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (2
ยท ๐ต) = (๐ต + ๐ต)) |
23 | 20, 22 | eqtr4d 2781 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด + ๐ต) โ (๐ด โ ๐ต)) = (2 ยท ๐ต)) |
24 | 23 | oveq1d 7365 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + ๐ต) โ (๐ด โ ๐ต)) / 2) = ((2 ยท ๐ต) / 2)) |
25 | | divsubdir 11783 |
. . . . 5
โข (((๐ด + ๐ต) โ โ โง (๐ด โ ๐ต) โ โ โง (2 โ โ
โง 2 โ 0)) โ (((๐ด + ๐ต) โ (๐ด โ ๐ต)) / 2) = (((๐ด + ๐ต) / 2) โ ((๐ด โ ๐ต) / 2))) |
26 | 9, 25 | mp3an3 1451 |
. . . 4
โข (((๐ด + ๐ต) โ โ โง (๐ด โ ๐ต) โ โ) โ (((๐ด + ๐ต) โ (๐ด โ ๐ต)) / 2) = (((๐ด + ๐ต) / 2) โ ((๐ด โ ๐ต) / 2))) |
27 | 7, 8, 26 | syl2anc 585 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + ๐ต) โ (๐ด โ ๐ต)) / 2) = (((๐ด + ๐ต) / 2) โ ((๐ด โ ๐ต) / 2))) |
28 | | divcan3 11773 |
. . . . 5
โข ((๐ต โ โ โง 2 โ
โ โง 2 โ 0) โ ((2 ยท ๐ต) / 2) = ๐ต) |
29 | 13, 14, 28 | mp3an23 1454 |
. . . 4
โข (๐ต โ โ โ ((2
ยท ๐ต) / 2) = ๐ต) |
30 | 29 | adantl 483 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ ((2
ยท ๐ต) / 2) = ๐ต) |
31 | 24, 27, 30 | 3eqtr3d 2786 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด + ๐ต) / 2) โ ((๐ด โ ๐ต) / 2)) = ๐ต) |
32 | 18, 31 | jca 513 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((๐ด + ๐ต) / 2) + ((๐ด โ ๐ต) / 2)) = ๐ด โง (((๐ด + ๐ต) / 2) โ ((๐ด โ ๐ต) / 2)) = ๐ต)) |