Step | Hyp | Ref
| Expression |
1 | | simp1 1136 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โ ๐ด โ
โ) |
2 | 1 | adantr 481 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ ๐ด โ
โ) |
3 | | simpl2 1192 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ ๐ต โ
โ) |
4 | | simpl 483 |
. . . 4
โข ((๐ถ โ โ โง ๐ถ โ 0) โ ๐ถ โ
โ) |
5 | 4 | adantl 482 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ ๐ถ โ
โ) |
6 | | mulbinom2 14182 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (((๐ถ ยท ๐ด) + ๐ต)โ2) = ((((๐ถ ยท ๐ด)โ2) + ((2 ยท ๐ถ) ยท (๐ด ยท ๐ต))) + (๐ตโ2))) |
7 | 6 | oveq1d 7420 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ
((((๐ถ ยท ๐ด) + ๐ต)โ2) โ ๐ท) = (((((๐ถ ยท ๐ด)โ2) + ((2 ยท ๐ถ) ยท (๐ด ยท ๐ต))) + (๐ตโ2)) โ ๐ท)) |
8 | 7 | oveq1d 7420 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ
(((((๐ถ ยท ๐ด) + ๐ต)โ2) โ ๐ท) / ๐ถ) = ((((((๐ถ ยท ๐ด)โ2) + ((2 ยท ๐ถ) ยท (๐ด ยท ๐ต))) + (๐ตโ2)) โ ๐ท) / ๐ถ)) |
9 | 2, 3, 5, 8 | syl3anc 1371 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (((((๐ถ ยท ๐ด) + ๐ต)โ2) โ ๐ท) / ๐ถ) = ((((((๐ถ ยท ๐ด)โ2) + ((2 ยท ๐ถ) ยท (๐ด ยท ๐ต))) + (๐ตโ2)) โ ๐ท) / ๐ถ)) |
10 | 5, 2 | mulcld 11230 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (๐ถ ยท ๐ด) โ โ) |
11 | 10 | sqcld 14105 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ ((๐ถ ยท ๐ด)โ2) โ โ) |
12 | | 2cnd 12286 |
. . . . . . . . . 10
โข (๐ถ โ โ โ 2 โ
โ) |
13 | | id 22 |
. . . . . . . . . 10
โข (๐ถ โ โ โ ๐ถ โ
โ) |
14 | 12, 13 | mulcld 11230 |
. . . . . . . . 9
โข (๐ถ โ โ โ (2
ยท ๐ถ) โ
โ) |
15 | 14 | adantr 481 |
. . . . . . . 8
โข ((๐ถ โ โ โง ๐ถ โ 0) โ (2 ยท
๐ถ) โ
โ) |
16 | 15 | adantl 482 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (2 ยท
๐ถ) โ
โ) |
17 | | mulcl 11190 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) โ โ) |
18 | 17 | 3adant3 1132 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โ (๐ด ยท ๐ต) โ โ) |
19 | 18 | adantr 481 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (๐ด ยท ๐ต) โ โ) |
20 | 16, 19 | mulcld 11230 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ ((2 ยท
๐ถ) ยท (๐ด ยท ๐ต)) โ โ) |
21 | 11, 20 | addcld 11229 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (((๐ถ ยท ๐ด)โ2) + ((2 ยท ๐ถ) ยท (๐ด ยท ๐ต))) โ โ) |
22 | | sqcl 14079 |
. . . . . . 7
โข (๐ต โ โ โ (๐ตโ2) โ
โ) |
23 | 22 | 3ad2ant2 1134 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โ (๐ตโ2) โ
โ) |
24 | 23 | adantr 481 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (๐ตโ2) โ
โ) |
25 | 21, 24 | addcld 11229 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ ((((๐ถ ยท ๐ด)โ2) + ((2 ยท ๐ถ) ยท (๐ด ยท ๐ต))) + (๐ตโ2)) โ โ) |
26 | | simpl3 1193 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ ๐ท โ
โ) |
27 | | simpr 485 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (๐ถ โ โ โง ๐ถ โ 0)) |
28 | | divsubdir 11904 |
. . . 4
โข
((((((๐ถ ยท
๐ด)โ2) + ((2 ยท
๐ถ) ยท (๐ด ยท ๐ต))) + (๐ตโ2)) โ โ โง ๐ท โ โ โง (๐ถ โ โ โง ๐ถ โ 0)) โ ((((((๐ถ ยท ๐ด)โ2) + ((2 ยท ๐ถ) ยท (๐ด ยท ๐ต))) + (๐ตโ2)) โ ๐ท) / ๐ถ) = ((((((๐ถ ยท ๐ด)โ2) + ((2 ยท ๐ถ) ยท (๐ด ยท ๐ต))) + (๐ตโ2)) / ๐ถ) โ (๐ท / ๐ถ))) |
29 | 25, 26, 27, 28 | syl3anc 1371 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ ((((((๐ถ ยท ๐ด)โ2) + ((2 ยท ๐ถ) ยท (๐ด ยท ๐ต))) + (๐ตโ2)) โ ๐ท) / ๐ถ) = ((((((๐ถ ยท ๐ด)โ2) + ((2 ยท ๐ถ) ยท (๐ด ยท ๐ต))) + (๐ตโ2)) / ๐ถ) โ (๐ท / ๐ถ))) |
30 | | divdir 11893 |
. . . . . 6
โข
(((((๐ถ ยท
๐ด)โ2) + ((2 ยท
๐ถ) ยท (๐ด ยท ๐ต))) โ โ โง (๐ตโ2) โ โ โง (๐ถ โ โ โง ๐ถ โ 0)) โ (((((๐ถ ยท ๐ด)โ2) + ((2 ยท ๐ถ) ยท (๐ด ยท ๐ต))) + (๐ตโ2)) / ๐ถ) = (((((๐ถ ยท ๐ด)โ2) + ((2 ยท ๐ถ) ยท (๐ด ยท ๐ต))) / ๐ถ) + ((๐ตโ2) / ๐ถ))) |
31 | 21, 24, 27, 30 | syl3anc 1371 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (((((๐ถ ยท ๐ด)โ2) + ((2 ยท ๐ถ) ยท (๐ด ยท ๐ต))) + (๐ตโ2)) / ๐ถ) = (((((๐ถ ยท ๐ด)โ2) + ((2 ยท ๐ถ) ยท (๐ด ยท ๐ต))) / ๐ถ) + ((๐ตโ2) / ๐ถ))) |
32 | | divdir 11893 |
. . . . . . . 8
โข ((((๐ถ ยท ๐ด)โ2) โ โ โง ((2 ยท
๐ถ) ยท (๐ด ยท ๐ต)) โ โ โง (๐ถ โ โ โง ๐ถ โ 0)) โ ((((๐ถ ยท ๐ด)โ2) + ((2 ยท ๐ถ) ยท (๐ด ยท ๐ต))) / ๐ถ) = ((((๐ถ ยท ๐ด)โ2) / ๐ถ) + (((2 ยท ๐ถ) ยท (๐ด ยท ๐ต)) / ๐ถ))) |
33 | 11, 20, 27, 32 | syl3anc 1371 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ ((((๐ถ ยท ๐ด)โ2) + ((2 ยท ๐ถ) ยท (๐ด ยท ๐ต))) / ๐ถ) = ((((๐ถ ยท ๐ด)โ2) / ๐ถ) + (((2 ยท ๐ถ) ยท (๐ด ยท ๐ต)) / ๐ถ))) |
34 | | sqmul 14080 |
. . . . . . . . . . 11
โข ((๐ถ โ โ โง ๐ด โ โ) โ ((๐ถ ยท ๐ด)โ2) = ((๐ถโ2) ยท (๐ดโ2))) |
35 | 4, 1, 34 | syl2anr 597 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ ((๐ถ ยท ๐ด)โ2) = ((๐ถโ2) ยท (๐ดโ2))) |
36 | 35 | oveq1d 7420 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (((๐ถ ยท ๐ด)โ2) / ๐ถ) = (((๐ถโ2) ยท (๐ดโ2)) / ๐ถ)) |
37 | | sqcl 14079 |
. . . . . . . . . . . 12
โข (๐ถ โ โ โ (๐ถโ2) โ
โ) |
38 | 37 | adantr 481 |
. . . . . . . . . . 11
โข ((๐ถ โ โ โง ๐ถ โ 0) โ (๐ถโ2) โ
โ) |
39 | 38 | adantl 482 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (๐ถโ2) โ
โ) |
40 | | sqcl 14079 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ (๐ดโ2) โ
โ) |
41 | 40 | 3ad2ant1 1133 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โ (๐ดโ2) โ
โ) |
42 | 41 | adantr 481 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (๐ดโ2) โ
โ) |
43 | | div23 11887 |
. . . . . . . . . 10
โข (((๐ถโ2) โ โ โง
(๐ดโ2) โ โ
โง (๐ถ โ โ
โง ๐ถ โ 0)) โ
(((๐ถโ2) ยท
(๐ดโ2)) / ๐ถ) = (((๐ถโ2) / ๐ถ) ยท (๐ดโ2))) |
44 | 39, 42, 27, 43 | syl3anc 1371 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (((๐ถโ2) ยท (๐ดโ2)) / ๐ถ) = (((๐ถโ2) / ๐ถ) ยท (๐ดโ2))) |
45 | | sqdivid 14083 |
. . . . . . . . . . 11
โข ((๐ถ โ โ โง ๐ถ โ 0) โ ((๐ถโ2) / ๐ถ) = ๐ถ) |
46 | 45 | adantl 482 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ ((๐ถโ2) / ๐ถ) = ๐ถ) |
47 | 46 | oveq1d 7420 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (((๐ถโ2) / ๐ถ) ยท (๐ดโ2)) = (๐ถ ยท (๐ดโ2))) |
48 | 36, 44, 47 | 3eqtrd 2776 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (((๐ถ ยท ๐ด)โ2) / ๐ถ) = (๐ถ ยท (๐ดโ2))) |
49 | | div23 11887 |
. . . . . . . . . 10
โข (((2
ยท ๐ถ) โ โ
โง (๐ด ยท ๐ต) โ โ โง (๐ถ โ โ โง ๐ถ โ 0)) โ (((2 ยท
๐ถ) ยท (๐ด ยท ๐ต)) / ๐ถ) = (((2 ยท ๐ถ) / ๐ถ) ยท (๐ด ยท ๐ต))) |
50 | 16, 19, 27, 49 | syl3anc 1371 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (((2 ยท
๐ถ) ยท (๐ด ยท ๐ต)) / ๐ถ) = (((2 ยท ๐ถ) / ๐ถ) ยท (๐ด ยท ๐ต))) |
51 | | 2cnd 12286 |
. . . . . . . . . . . 12
โข ((๐ถ โ โ โง ๐ถ โ 0) โ 2 โ
โ) |
52 | | simpr 485 |
. . . . . . . . . . . 12
โข ((๐ถ โ โ โง ๐ถ โ 0) โ ๐ถ โ 0) |
53 | 51, 4, 52 | divcan4d 11992 |
. . . . . . . . . . 11
โข ((๐ถ โ โ โง ๐ถ โ 0) โ ((2 ยท
๐ถ) / ๐ถ) = 2) |
54 | 53 | adantl 482 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ ((2 ยท
๐ถ) / ๐ถ) = 2) |
55 | 54 | oveq1d 7420 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (((2 ยท
๐ถ) / ๐ถ) ยท (๐ด ยท ๐ต)) = (2 ยท (๐ด ยท ๐ต))) |
56 | 50, 55 | eqtrd 2772 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (((2 ยท
๐ถ) ยท (๐ด ยท ๐ต)) / ๐ถ) = (2 ยท (๐ด ยท ๐ต))) |
57 | 48, 56 | oveq12d 7423 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ ((((๐ถ ยท ๐ด)โ2) / ๐ถ) + (((2 ยท ๐ถ) ยท (๐ด ยท ๐ต)) / ๐ถ)) = ((๐ถ ยท (๐ดโ2)) + (2 ยท (๐ด ยท ๐ต)))) |
58 | 33, 57 | eqtrd 2772 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ ((((๐ถ ยท ๐ด)โ2) + ((2 ยท ๐ถ) ยท (๐ด ยท ๐ต))) / ๐ถ) = ((๐ถ ยท (๐ดโ2)) + (2 ยท (๐ด ยท ๐ต)))) |
59 | 58 | oveq1d 7420 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (((((๐ถ ยท ๐ด)โ2) + ((2 ยท ๐ถ) ยท (๐ด ยท ๐ต))) / ๐ถ) + ((๐ตโ2) / ๐ถ)) = (((๐ถ ยท (๐ดโ2)) + (2 ยท (๐ด ยท ๐ต))) + ((๐ตโ2) / ๐ถ))) |
60 | 31, 59 | eqtrd 2772 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (((((๐ถ ยท ๐ด)โ2) + ((2 ยท ๐ถ) ยท (๐ด ยท ๐ต))) + (๐ตโ2)) / ๐ถ) = (((๐ถ ยท (๐ดโ2)) + (2 ยท (๐ด ยท ๐ต))) + ((๐ตโ2) / ๐ถ))) |
61 | 60 | oveq1d 7420 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ ((((((๐ถ ยท ๐ด)โ2) + ((2 ยท ๐ถ) ยท (๐ด ยท ๐ต))) + (๐ตโ2)) / ๐ถ) โ (๐ท / ๐ถ)) = ((((๐ถ ยท (๐ดโ2)) + (2 ยท (๐ด ยท ๐ต))) + ((๐ตโ2) / ๐ถ)) โ (๐ท / ๐ถ))) |
62 | 5, 42 | mulcld 11230 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (๐ถ ยท (๐ดโ2)) โ โ) |
63 | | 2cnd 12286 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ 2 โ
โ) |
64 | 63, 17 | mulcld 11230 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (2
ยท (๐ด ยท ๐ต)) โ
โ) |
65 | 64 | 3adant3 1132 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โ (2
ยท (๐ด ยท ๐ต)) โ
โ) |
66 | 65 | adantr 481 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (2 ยท
(๐ด ยท ๐ต)) โ
โ) |
67 | 62, 66 | addcld 11229 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ ((๐ถ ยท (๐ดโ2)) + (2 ยท (๐ด ยท ๐ต))) โ โ) |
68 | 52 | adantl 482 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ ๐ถ โ 0) |
69 | 24, 5, 68 | divcld 11986 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ ((๐ตโ2) / ๐ถ) โ โ) |
70 | 26, 5, 68 | divcld 11986 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (๐ท / ๐ถ) โ โ) |
71 | 67, 69, 70 | addsubassd 11587 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ ((((๐ถ ยท (๐ดโ2)) + (2 ยท (๐ด ยท ๐ต))) + ((๐ตโ2) / ๐ถ)) โ (๐ท / ๐ถ)) = (((๐ถ ยท (๐ดโ2)) + (2 ยท (๐ด ยท ๐ต))) + (((๐ตโ2) / ๐ถ) โ (๐ท / ๐ถ)))) |
72 | 29, 61, 71 | 3eqtrd 2776 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ ((((((๐ถ ยท ๐ด)โ2) + ((2 ยท ๐ถ) ยท (๐ด ยท ๐ต))) + (๐ตโ2)) โ ๐ท) / ๐ถ) = (((๐ถ ยท (๐ดโ2)) + (2 ยท (๐ด ยท ๐ต))) + (((๐ตโ2) / ๐ถ) โ (๐ท / ๐ถ)))) |
73 | | divsubdir 11904 |
. . . . 5
โข (((๐ตโ2) โ โ โง
๐ท โ โ โง
(๐ถ โ โ โง
๐ถ โ 0)) โ (((๐ตโ2) โ ๐ท) / ๐ถ) = (((๐ตโ2) / ๐ถ) โ (๐ท / ๐ถ))) |
74 | 24, 26, 27, 73 | syl3anc 1371 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (((๐ตโ2) โ ๐ท) / ๐ถ) = (((๐ตโ2) / ๐ถ) โ (๐ท / ๐ถ))) |
75 | 74 | eqcomd 2738 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (((๐ตโ2) / ๐ถ) โ (๐ท / ๐ถ)) = (((๐ตโ2) โ ๐ท) / ๐ถ)) |
76 | 75 | oveq2d 7421 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (((๐ถ ยท (๐ดโ2)) + (2 ยท (๐ด ยท ๐ต))) + (((๐ตโ2) / ๐ถ) โ (๐ท / ๐ถ))) = (((๐ถ ยท (๐ดโ2)) + (2 ยท (๐ด ยท ๐ต))) + (((๐ตโ2) โ ๐ท) / ๐ถ))) |
77 | 9, 72, 76 | 3eqtrd 2776 |
1
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (((((๐ถ ยท ๐ด) + ๐ต)โ2) โ ๐ท) / ๐ถ) = (((๐ถ ยท (๐ดโ2)) + (2 ยท (๐ด ยท ๐ต))) + (((๐ตโ2) โ ๐ท) / ๐ถ))) |