Step | Hyp | Ref
| Expression |
1 | | bj-bary1.s |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
2 | | bj-bary1.t |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
3 | 1, 2 | pncand 11569 |
. . . . . 6
โข (๐ โ ((๐ + ๐) โ ๐) = ๐) |
4 | | oveq1 7408 |
. . . . . 6
โข ((๐ + ๐) = 1 โ ((๐ + ๐) โ ๐) = (1 โ ๐)) |
5 | | pm5.31 828 |
. . . . . 6
โข ((((๐ + ๐) โ ๐) = ๐ โง ((๐ + ๐) = 1 โ ((๐ + ๐) โ ๐) = (1 โ ๐))) โ ((๐ + ๐) = 1 โ (((๐ + ๐) โ ๐) = (1 โ ๐) โง ((๐ + ๐) โ ๐) = ๐))) |
6 | 3, 4, 5 | sylancl 585 |
. . . . 5
โข (๐ โ ((๐ + ๐) = 1 โ (((๐ + ๐) โ ๐) = (1 โ ๐) โง ((๐ + ๐) โ ๐) = ๐))) |
7 | | eqtr2 2748 |
. . . . . 6
โข ((((๐ + ๐) โ ๐) = (1 โ ๐) โง ((๐ + ๐) โ ๐) = ๐) โ (1 โ ๐) = ๐) |
8 | 7 | eqcomd 2730 |
. . . . 5
โข ((((๐ + ๐) โ ๐) = (1 โ ๐) โง ((๐ + ๐) โ ๐) = ๐) โ ๐ = (1 โ ๐)) |
9 | 6, 8 | syl6 35 |
. . . 4
โข (๐ โ ((๐ + ๐) = 1 โ ๐ = (1 โ ๐))) |
10 | | oveq1 7408 |
. . . . . . . 8
โข (๐ = (1 โ ๐) โ (๐ ยท ๐ด) = ((1 โ ๐) ยท ๐ด)) |
11 | 10 | oveq1d 7416 |
. . . . . . 7
โข (๐ = (1 โ ๐) โ ((๐ ยท ๐ด) + (๐ ยท ๐ต)) = (((1 โ ๐) ยท ๐ด) + (๐ ยท ๐ต))) |
12 | | eqtr 2747 |
. . . . . . 7
โข ((๐ = ((๐ ยท ๐ด) + (๐ ยท ๐ต)) โง ((๐ ยท ๐ด) + (๐ ยท ๐ต)) = (((1 โ ๐) ยท ๐ด) + (๐ ยท ๐ต))) โ ๐ = (((1 โ ๐) ยท ๐ด) + (๐ ยท ๐ต))) |
13 | 11, 12 | sylan2 592 |
. . . . . 6
โข ((๐ = ((๐ ยท ๐ด) + (๐ ยท ๐ต)) โง ๐ = (1 โ ๐)) โ ๐ = (((1 โ ๐) ยท ๐ด) + (๐ ยท ๐ต))) |
14 | | 1cnd 11206 |
. . . . . . . . 9
โข (๐ โ 1 โ
โ) |
15 | | bj-bary1.a |
. . . . . . . . 9
โข (๐ โ ๐ด โ โ) |
16 | 14, 2, 15 | subdird 11668 |
. . . . . . . 8
โข (๐ โ ((1 โ ๐) ยท ๐ด) = ((1 ยท ๐ด) โ (๐ ยท ๐ด))) |
17 | 15 | mullidd 11229 |
. . . . . . . . 9
โข (๐ โ (1 ยท ๐ด) = ๐ด) |
18 | 17 | oveq1d 7416 |
. . . . . . . 8
โข (๐ โ ((1 ยท ๐ด) โ (๐ ยท ๐ด)) = (๐ด โ (๐ ยท ๐ด))) |
19 | 16, 18 | eqtrd 2764 |
. . . . . . 7
โข (๐ โ ((1 โ ๐) ยท ๐ด) = (๐ด โ (๐ ยท ๐ด))) |
20 | 19 | oveq1d 7416 |
. . . . . 6
โข (๐ โ (((1 โ ๐) ยท ๐ด) + (๐ ยท ๐ต)) = ((๐ด โ (๐ ยท ๐ด)) + (๐ ยท ๐ต))) |
21 | 13, 20 | sylan9eqr 2786 |
. . . . 5
โข ((๐ โง (๐ = ((๐ ยท ๐ด) + (๐ ยท ๐ต)) โง ๐ = (1 โ ๐))) โ ๐ = ((๐ด โ (๐ ยท ๐ด)) + (๐ ยท ๐ต))) |
22 | 21 | ex 412 |
. . . 4
โข (๐ โ ((๐ = ((๐ ยท ๐ด) + (๐ ยท ๐ต)) โง ๐ = (1 โ ๐)) โ ๐ = ((๐ด โ (๐ ยท ๐ด)) + (๐ ยท ๐ต)))) |
23 | 9, 22 | sylan2d 604 |
. . 3
โข (๐ โ ((๐ = ((๐ ยท ๐ด) + (๐ ยท ๐ต)) โง (๐ + ๐) = 1) โ ๐ = ((๐ด โ (๐ ยท ๐ด)) + (๐ ยท ๐ต)))) |
24 | 2, 15 | mulcld 11231 |
. . . . . 6
โข (๐ โ (๐ ยท ๐ด) โ โ) |
25 | | bj-bary1.b |
. . . . . . 7
โข (๐ โ ๐ต โ โ) |
26 | 2, 25 | mulcld 11231 |
. . . . . 6
โข (๐ โ (๐ ยท ๐ต) โ โ) |
27 | 15, 24, 26 | subadd23d 11590 |
. . . . 5
โข (๐ โ ((๐ด โ (๐ ยท ๐ด)) + (๐ ยท ๐ต)) = (๐ด + ((๐ ยท ๐ต) โ (๐ ยท ๐ด)))) |
28 | 2, 25, 15 | subdid 11667 |
. . . . . . 7
โข (๐ โ (๐ ยท (๐ต โ ๐ด)) = ((๐ ยท ๐ต) โ (๐ ยท ๐ด))) |
29 | 28 | eqcomd 2730 |
. . . . . 6
โข (๐ โ ((๐ ยท ๐ต) โ (๐ ยท ๐ด)) = (๐ ยท (๐ต โ ๐ด))) |
30 | 29 | oveq2d 7417 |
. . . . 5
โข (๐ โ (๐ด + ((๐ ยท ๐ต) โ (๐ ยท ๐ด))) = (๐ด + (๐ ยท (๐ต โ ๐ด)))) |
31 | 27, 30 | eqtrd 2764 |
. . . 4
โข (๐ โ ((๐ด โ (๐ ยท ๐ด)) + (๐ ยท ๐ต)) = (๐ด + (๐ ยท (๐ต โ ๐ด)))) |
32 | 31 | eqeq2d 2735 |
. . 3
โข (๐ โ (๐ = ((๐ด โ (๐ ยท ๐ด)) + (๐ ยท ๐ต)) โ ๐ = (๐ด + (๐ ยท (๐ต โ ๐ด))))) |
33 | 23, 32 | sylibd 238 |
. 2
โข (๐ โ ((๐ = ((๐ ยท ๐ด) + (๐ ยท ๐ต)) โง (๐ + ๐) = 1) โ ๐ = (๐ด + (๐ ยท (๐ต โ ๐ด))))) |
34 | | oveq1 7408 |
. . 3
โข (๐ = (๐ด + (๐ ยท (๐ต โ ๐ด))) โ (๐ โ ๐ด) = ((๐ด + (๐ ยท (๐ต โ ๐ด))) โ ๐ด)) |
35 | 25, 15 | subcld 11568 |
. . . . . 6
โข (๐ โ (๐ต โ ๐ด) โ โ) |
36 | 2, 35 | mulcld 11231 |
. . . . 5
โข (๐ โ (๐ ยท (๐ต โ ๐ด)) โ โ) |
37 | 15, 36 | pncan2d 11570 |
. . . 4
โข (๐ โ ((๐ด + (๐ ยท (๐ต โ ๐ด))) โ ๐ด) = (๐ ยท (๐ต โ ๐ด))) |
38 | 37 | eqeq2d 2735 |
. . 3
โข (๐ โ ((๐ โ ๐ด) = ((๐ด + (๐ ยท (๐ต โ ๐ด))) โ ๐ด) โ (๐ โ ๐ด) = (๐ ยท (๐ต โ ๐ด)))) |
39 | 34, 38 | imbitrid 243 |
. 2
โข (๐ โ (๐ = (๐ด + (๐ ยท (๐ต โ ๐ด))) โ (๐ โ ๐ด) = (๐ ยท (๐ต โ ๐ด)))) |
40 | | eqcom 2731 |
. . 3
โข ((๐ โ ๐ด) = (๐ ยท (๐ต โ ๐ด)) โ (๐ ยท (๐ต โ ๐ด)) = (๐ โ ๐ด)) |
41 | 2, 35 | mulcomd 11232 |
. . . . 5
โข (๐ โ (๐ ยท (๐ต โ ๐ด)) = ((๐ต โ ๐ด) ยท ๐)) |
42 | 41 | eqeq1d 2726 |
. . . 4
โข (๐ โ ((๐ ยท (๐ต โ ๐ด)) = (๐ โ ๐ด) โ ((๐ต โ ๐ด) ยท ๐) = (๐ โ ๐ด))) |
43 | | bj-bary1.x |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
44 | 43, 15 | subcld 11568 |
. . . . . 6
โข (๐ โ (๐ โ ๐ด) โ โ) |
45 | | bj-bary1.neq |
. . . . . . . 8
โข (๐ โ ๐ด โ ๐ต) |
46 | 45 | necomd 2988 |
. . . . . . 7
โข (๐ โ ๐ต โ ๐ด) |
47 | 25, 15, 46 | subne0d 11577 |
. . . . . 6
โข (๐ โ (๐ต โ ๐ด) โ 0) |
48 | 35, 2, 44, 47 | rdiv 12046 |
. . . . 5
โข (๐ โ (((๐ต โ ๐ด) ยท ๐) = (๐ โ ๐ด) โ ๐ = ((๐ โ ๐ด) / (๐ต โ ๐ด)))) |
49 | 48 | biimpd 228 |
. . . 4
โข (๐ โ (((๐ต โ ๐ด) ยท ๐) = (๐ โ ๐ด) โ ๐ = ((๐ โ ๐ด) / (๐ต โ ๐ด)))) |
50 | 42, 49 | sylbid 239 |
. . 3
โข (๐ โ ((๐ ยท (๐ต โ ๐ด)) = (๐ โ ๐ด) โ ๐ = ((๐ โ ๐ด) / (๐ต โ ๐ด)))) |
51 | 40, 50 | biimtrid 241 |
. 2
โข (๐ โ ((๐ โ ๐ด) = (๐ ยท (๐ต โ ๐ด)) โ ๐ = ((๐ โ ๐ด) / (๐ต โ ๐ด)))) |
52 | 33, 39, 51 | 3syld 60 |
1
โข (๐ โ ((๐ = ((๐ ยท ๐ด) + (๐ ยท ๐ต)) โง (๐ + ๐) = 1) โ ๐ = ((๐ โ ๐ด) / (๐ต โ ๐ด)))) |