Step | Hyp | Ref
| Expression |
1 | | dvmptdiv.a |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐) โ ๐ด โ โ) |
2 | | dvmptdiv.c |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐) โ ๐ถ โ (โ โ
{0})) |
3 | 2 | eldifad 3925 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐) โ ๐ถ โ โ) |
4 | | eldifsn 4752 |
. . . . . . 7
โข (๐ถ โ (โ โ {0})
โ (๐ถ โ โ
โง ๐ถ โ
0)) |
5 | 2, 4 | sylib 217 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐) โ (๐ถ โ โ โง ๐ถ โ 0)) |
6 | 5 | simprd 496 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐) โ ๐ถ โ 0) |
7 | 1, 3, 6 | divrecd 11943 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐) โ (๐ด / ๐ถ) = (๐ด ยท (1 / ๐ถ))) |
8 | 7 | mpteq2dva 5210 |
. . 3
โข (๐ โ (๐ฅ โ ๐ โฆ (๐ด / ๐ถ)) = (๐ฅ โ ๐ โฆ (๐ด ยท (1 / ๐ถ)))) |
9 | 8 | oveq2d 7378 |
. 2
โข (๐ โ (๐ D (๐ฅ โ ๐ โฆ (๐ด / ๐ถ))) = (๐ D (๐ฅ โ ๐ โฆ (๐ด ยท (1 / ๐ถ))))) |
10 | | dvmptdiv.s |
. . 3
โข (๐ โ ๐ โ {โ, โ}) |
11 | | dvmptdiv.b |
. . 3
โข ((๐ โง ๐ฅ โ ๐) โ ๐ต โ ๐) |
12 | | dvmptdiv.da |
. . 3
โข (๐ โ (๐ D (๐ฅ โ ๐ โฆ ๐ด)) = (๐ฅ โ ๐ โฆ ๐ต)) |
13 | 3, 6 | reccld 11933 |
. . 3
โข ((๐ โง ๐ฅ โ ๐) โ (1 / ๐ถ) โ โ) |
14 | | 1cnd 11159 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐) โ 1 โ โ) |
15 | | dvmptdiv.d |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐) โ ๐ท โ โ) |
16 | 14, 15 | mulcld 11184 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐) โ (1 ยท ๐ท) โ โ) |
17 | 3 | sqcld 14059 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐) โ (๐ถโ2) โ โ) |
18 | 6 | neneqd 2944 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐) โ ยฌ ๐ถ = 0) |
19 | | sqeq0 14035 |
. . . . . . . 8
โข (๐ถ โ โ โ ((๐ถโ2) = 0 โ ๐ถ = 0)) |
20 | 3, 19 | syl 17 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐) โ ((๐ถโ2) = 0 โ ๐ถ = 0)) |
21 | 18, 20 | mtbird 324 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐) โ ยฌ (๐ถโ2) = 0) |
22 | 21 | neqned 2946 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐) โ (๐ถโ2) โ 0) |
23 | 16, 17, 22 | divcld 11940 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐) โ ((1 ยท ๐ท) / (๐ถโ2)) โ โ) |
24 | 23 | negcld 11508 |
. . 3
โข ((๐ โง ๐ฅ โ ๐) โ -((1 ยท ๐ท) / (๐ถโ2)) โ โ) |
25 | | 1cnd 11159 |
. . . 4
โข (๐ โ 1 โ
โ) |
26 | | dvmptdiv.dc |
. . . 4
โข (๐ โ (๐ D (๐ฅ โ ๐ โฆ ๐ถ)) = (๐ฅ โ ๐ โฆ ๐ท)) |
27 | 10, 25, 2, 15, 26 | dvrecg 25374 |
. . 3
โข (๐ โ (๐ D (๐ฅ โ ๐ โฆ (1 / ๐ถ))) = (๐ฅ โ ๐ โฆ -((1 ยท ๐ท) / (๐ถโ2)))) |
28 | 10, 1, 11, 12, 13, 24, 27 | dvmptmul 25362 |
. 2
โข (๐ โ (๐ D (๐ฅ โ ๐ โฆ (๐ด ยท (1 / ๐ถ)))) = (๐ฅ โ ๐ โฆ ((๐ต ยท (1 / ๐ถ)) + (-((1 ยท ๐ท) / (๐ถโ2)) ยท ๐ด)))) |
29 | 10, 1, 11, 12 | dvmptcl 25360 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐) โ ๐ต โ โ) |
30 | 29, 3 | mulcld 11184 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐) โ (๐ต ยท ๐ถ) โ โ) |
31 | 30, 17, 22 | divcld 11940 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐) โ ((๐ต ยท ๐ถ) / (๐ถโ2)) โ โ) |
32 | 15, 1 | mulcld 11184 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐) โ (๐ท ยท ๐ด) โ โ) |
33 | 32, 17, 22 | divcld 11940 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐) โ ((๐ท ยท ๐ด) / (๐ถโ2)) โ โ) |
34 | 31, 33 | negsubd 11527 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐) โ (((๐ต ยท ๐ถ) / (๐ถโ2)) + -((๐ท ยท ๐ด) / (๐ถโ2))) = (((๐ต ยท ๐ถ) / (๐ถโ2)) โ ((๐ท ยท ๐ด) / (๐ถโ2)))) |
35 | 29, 14, 3, 6 | div12d 11976 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐) โ (๐ต ยท (1 / ๐ถ)) = (1 ยท (๐ต / ๐ถ))) |
36 | 29, 3, 6 | divcld 11940 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐) โ (๐ต / ๐ถ) โ โ) |
37 | 36 | mullidd 11182 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐) โ (1 ยท (๐ต / ๐ถ)) = (๐ต / ๐ถ)) |
38 | 3 | sqvald 14058 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐) โ (๐ถโ2) = (๐ถ ยท ๐ถ)) |
39 | 38 | oveq2d 7378 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐) โ ((๐ต ยท ๐ถ) / (๐ถโ2)) = ((๐ต ยท ๐ถ) / (๐ถ ยท ๐ถ))) |
40 | 29, 3, 3, 6, 6 | divcan5rd 11967 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐) โ ((๐ต ยท ๐ถ) / (๐ถ ยท ๐ถ)) = (๐ต / ๐ถ)) |
41 | 39, 40 | eqtr2d 2772 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐) โ (๐ต / ๐ถ) = ((๐ต ยท ๐ถ) / (๐ถโ2))) |
42 | 35, 37, 41 | 3eqtrd 2775 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐) โ (๐ต ยท (1 / ๐ถ)) = ((๐ต ยท ๐ถ) / (๐ถโ2))) |
43 | 15 | mullidd 11182 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐) โ (1 ยท ๐ท) = ๐ท) |
44 | 43 | oveq1d 7377 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐) โ ((1 ยท ๐ท) / (๐ถโ2)) = (๐ท / (๐ถโ2))) |
45 | 44 | negeqd 11404 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐) โ -((1 ยท ๐ท) / (๐ถโ2)) = -(๐ท / (๐ถโ2))) |
46 | 45 | oveq1d 7377 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐) โ (-((1 ยท ๐ท) / (๐ถโ2)) ยท ๐ด) = (-(๐ท / (๐ถโ2)) ยท ๐ด)) |
47 | 15, 17, 22 | divcld 11940 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐) โ (๐ท / (๐ถโ2)) โ โ) |
48 | 47, 1 | mulneg1d 11617 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐) โ (-(๐ท / (๐ถโ2)) ยท ๐ด) = -((๐ท / (๐ถโ2)) ยท ๐ด)) |
49 | 15, 1, 17, 22 | div23d 11977 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐) โ ((๐ท ยท ๐ด) / (๐ถโ2)) = ((๐ท / (๐ถโ2)) ยท ๐ด)) |
50 | 49 | eqcomd 2737 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐) โ ((๐ท / (๐ถโ2)) ยท ๐ด) = ((๐ท ยท ๐ด) / (๐ถโ2))) |
51 | 50 | negeqd 11404 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐) โ -((๐ท / (๐ถโ2)) ยท ๐ด) = -((๐ท ยท ๐ด) / (๐ถโ2))) |
52 | 46, 48, 51 | 3eqtrd 2775 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐) โ (-((1 ยท ๐ท) / (๐ถโ2)) ยท ๐ด) = -((๐ท ยท ๐ด) / (๐ถโ2))) |
53 | 42, 52 | oveq12d 7380 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐) โ ((๐ต ยท (1 / ๐ถ)) + (-((1 ยท ๐ท) / (๐ถโ2)) ยท ๐ด)) = (((๐ต ยท ๐ถ) / (๐ถโ2)) + -((๐ท ยท ๐ด) / (๐ถโ2)))) |
54 | 30, 32, 17, 22 | divsubdird 11979 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐) โ (((๐ต ยท ๐ถ) โ (๐ท ยท ๐ด)) / (๐ถโ2)) = (((๐ต ยท ๐ถ) / (๐ถโ2)) โ ((๐ท ยท ๐ด) / (๐ถโ2)))) |
55 | 34, 53, 54 | 3eqtr4d 2781 |
. . 3
โข ((๐ โง ๐ฅ โ ๐) โ ((๐ต ยท (1 / ๐ถ)) + (-((1 ยท ๐ท) / (๐ถโ2)) ยท ๐ด)) = (((๐ต ยท ๐ถ) โ (๐ท ยท ๐ด)) / (๐ถโ2))) |
56 | 55 | mpteq2dva 5210 |
. 2
โข (๐ โ (๐ฅ โ ๐ โฆ ((๐ต ยท (1 / ๐ถ)) + (-((1 ยท ๐ท) / (๐ถโ2)) ยท ๐ด))) = (๐ฅ โ ๐ โฆ (((๐ต ยท ๐ถ) โ (๐ท ยท ๐ด)) / (๐ถโ2)))) |
57 | 9, 28, 56 | 3eqtrd 2775 |
1
โข (๐ โ (๐ D (๐ฅ โ ๐ โฆ (๐ด / ๐ถ))) = (๐ฅ โ ๐ โฆ (((๐ต ยท ๐ถ) โ (๐ท ยท ๐ด)) / (๐ถโ2)))) |