Step | Hyp | Ref
| Expression |
1 | | bj-bary1.b |
. . . . . . . . . 10
โข (๐ โ ๐ต โ โ) |
2 | | bj-bary1.a |
. . . . . . . . . 10
โข (๐ โ ๐ด โ โ) |
3 | 1, 2 | mulcld 11233 |
. . . . . . . . 9
โข (๐ โ (๐ต ยท ๐ด) โ โ) |
4 | | bj-bary1.x |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
5 | 4, 2 | mulcld 11233 |
. . . . . . . . 9
โข (๐ โ (๐ ยท ๐ด) โ โ) |
6 | 3, 5 | subcld 11570 |
. . . . . . . 8
โข (๐ โ ((๐ต ยท ๐ด) โ (๐ ยท ๐ด)) โ โ) |
7 | 4, 1 | mulcld 11233 |
. . . . . . . 8
โข (๐ โ (๐ ยท ๐ต) โ โ) |
8 | 2, 1 | mulcld 11233 |
. . . . . . . 8
โข (๐ โ (๐ด ยท ๐ต) โ โ) |
9 | 6, 7, 8 | addsub12d 11593 |
. . . . . . 7
โข (๐ โ (((๐ต ยท ๐ด) โ (๐ ยท ๐ด)) + ((๐ ยท ๐ต) โ (๐ด ยท ๐ต))) = ((๐ ยท ๐ต) + (((๐ต ยท ๐ด) โ (๐ ยท ๐ด)) โ (๐ด ยท ๐ต)))) |
10 | 3, 5, 8 | sub32d 11602 |
. . . . . . . . 9
โข (๐ โ (((๐ต ยท ๐ด) โ (๐ ยท ๐ด)) โ (๐ด ยท ๐ต)) = (((๐ต ยท ๐ด) โ (๐ด ยท ๐ต)) โ (๐ ยท ๐ด))) |
11 | 1, 2 | bj-subcom 36184 |
. . . . . . . . . 10
โข (๐ โ ((๐ต ยท ๐ด) โ (๐ด ยท ๐ต)) = 0) |
12 | 11 | oveq1d 7423 |
. . . . . . . . 9
โข (๐ โ (((๐ต ยท ๐ด) โ (๐ด ยท ๐ต)) โ (๐ ยท ๐ด)) = (0 โ (๐ ยท ๐ด))) |
13 | 10, 12 | eqtrd 2772 |
. . . . . . . 8
โข (๐ โ (((๐ต ยท ๐ด) โ (๐ ยท ๐ด)) โ (๐ด ยท ๐ต)) = (0 โ (๐ ยท ๐ด))) |
14 | 13 | oveq2d 7424 |
. . . . . . 7
โข (๐ โ ((๐ ยท ๐ต) + (((๐ต ยท ๐ด) โ (๐ ยท ๐ด)) โ (๐ด ยท ๐ต))) = ((๐ ยท ๐ต) + (0 โ (๐ ยท ๐ด)))) |
15 | 9, 14 | eqtrd 2772 |
. . . . . 6
โข (๐ โ (((๐ต ยท ๐ด) โ (๐ ยท ๐ด)) + ((๐ ยท ๐ต) โ (๐ด ยท ๐ต))) = ((๐ ยท ๐ต) + (0 โ (๐ ยท ๐ด)))) |
16 | | 0cnd 11206 |
. . . . . . 7
โข (๐ โ 0 โ
โ) |
17 | 7, 16, 5 | addsubassd 11590 |
. . . . . 6
โข (๐ โ (((๐ ยท ๐ต) + 0) โ (๐ ยท ๐ด)) = ((๐ ยท ๐ต) + (0 โ (๐ ยท ๐ด)))) |
18 | 7 | addridd 11413 |
. . . . . . 7
โข (๐ โ ((๐ ยท ๐ต) + 0) = (๐ ยท ๐ต)) |
19 | 18 | oveq1d 7423 |
. . . . . 6
โข (๐ โ (((๐ ยท ๐ต) + 0) โ (๐ ยท ๐ด)) = ((๐ ยท ๐ต) โ (๐ ยท ๐ด))) |
20 | 15, 17, 19 | 3eqtr2d 2778 |
. . . . 5
โข (๐ โ (((๐ต ยท ๐ด) โ (๐ ยท ๐ด)) + ((๐ ยท ๐ต) โ (๐ด ยท ๐ต))) = ((๐ ยท ๐ต) โ (๐ ยท ๐ด))) |
21 | 1, 4, 2 | subdird 11670 |
. . . . . 6
โข (๐ โ ((๐ต โ ๐) ยท ๐ด) = ((๐ต ยท ๐ด) โ (๐ ยท ๐ด))) |
22 | 4, 2, 1 | subdird 11670 |
. . . . . 6
โข (๐ โ ((๐ โ ๐ด) ยท ๐ต) = ((๐ ยท ๐ต) โ (๐ด ยท ๐ต))) |
23 | 21, 22 | oveq12d 7426 |
. . . . 5
โข (๐ โ (((๐ต โ ๐) ยท ๐ด) + ((๐ โ ๐ด) ยท ๐ต)) = (((๐ต ยท ๐ด) โ (๐ ยท ๐ด)) + ((๐ ยท ๐ต) โ (๐ด ยท ๐ต)))) |
24 | 4, 1, 2 | subdid 11669 |
. . . . 5
โข (๐ โ (๐ ยท (๐ต โ ๐ด)) = ((๐ ยท ๐ต) โ (๐ ยท ๐ด))) |
25 | 20, 23, 24 | 3eqtr4rd 2783 |
. . . 4
โข (๐ โ (๐ ยท (๐ต โ ๐ด)) = (((๐ต โ ๐) ยท ๐ด) + ((๐ โ ๐ด) ยท ๐ต))) |
26 | 25 | oveq1d 7423 |
. . 3
โข (๐ โ ((๐ ยท (๐ต โ ๐ด)) / (๐ต โ ๐ด)) = ((((๐ต โ ๐) ยท ๐ด) + ((๐ โ ๐ด) ยท ๐ต)) / (๐ต โ ๐ด))) |
27 | 1, 4 | subcld 11570 |
. . . . 5
โข (๐ โ (๐ต โ ๐) โ โ) |
28 | 27, 2 | mulcld 11233 |
. . . 4
โข (๐ โ ((๐ต โ ๐) ยท ๐ด) โ โ) |
29 | 4, 2 | subcld 11570 |
. . . . 5
โข (๐ โ (๐ โ ๐ด) โ โ) |
30 | 29, 1 | mulcld 11233 |
. . . 4
โข (๐ โ ((๐ โ ๐ด) ยท ๐ต) โ โ) |
31 | 1, 2 | subcld 11570 |
. . . 4
โข (๐ โ (๐ต โ ๐ด) โ โ) |
32 | | bj-bary1.neq |
. . . . . 6
โข (๐ โ ๐ด โ ๐ต) |
33 | 32 | necomd 2996 |
. . . . 5
โข (๐ โ ๐ต โ ๐ด) |
34 | 1, 2, 33 | subne0d 11579 |
. . . 4
โข (๐ โ (๐ต โ ๐ด) โ 0) |
35 | 28, 30, 31, 34 | divdird 12027 |
. . 3
โข (๐ โ ((((๐ต โ ๐) ยท ๐ด) + ((๐ โ ๐ด) ยท ๐ต)) / (๐ต โ ๐ด)) = ((((๐ต โ ๐) ยท ๐ด) / (๐ต โ ๐ด)) + (((๐ โ ๐ด) ยท ๐ต) / (๐ต โ ๐ด)))) |
36 | 26, 35 | eqtrd 2772 |
. 2
โข (๐ โ ((๐ ยท (๐ต โ ๐ด)) / (๐ต โ ๐ด)) = ((((๐ต โ ๐) ยท ๐ด) / (๐ต โ ๐ด)) + (((๐ โ ๐ด) ยท ๐ต) / (๐ต โ ๐ด)))) |
37 | 4, 31, 34 | divcan4d 11995 |
. 2
โข (๐ โ ((๐ ยท (๐ต โ ๐ด)) / (๐ต โ ๐ด)) = ๐) |
38 | 27, 2, 31, 34 | div23d 12026 |
. . 3
โข (๐ โ (((๐ต โ ๐) ยท ๐ด) / (๐ต โ ๐ด)) = (((๐ต โ ๐) / (๐ต โ ๐ด)) ยท ๐ด)) |
39 | 29, 1, 31, 34 | div23d 12026 |
. . 3
โข (๐ โ (((๐ โ ๐ด) ยท ๐ต) / (๐ต โ ๐ด)) = (((๐ โ ๐ด) / (๐ต โ ๐ด)) ยท ๐ต)) |
40 | 38, 39 | oveq12d 7426 |
. 2
โข (๐ โ ((((๐ต โ ๐) ยท ๐ด) / (๐ต โ ๐ด)) + (((๐ โ ๐ด) ยท ๐ต) / (๐ต โ ๐ด))) = ((((๐ต โ ๐) / (๐ต โ ๐ด)) ยท ๐ด) + (((๐ โ ๐ด) / (๐ต โ ๐ด)) ยท ๐ต))) |
41 | 36, 37, 40 | 3eqtr3d 2780 |
1
โข (๐ โ ๐ = ((((๐ต โ ๐) / (๐ต โ ๐ด)) ยท ๐ด) + (((๐ โ ๐ด) / (๐ต โ ๐ด)) ยท ๐ต))) |