Step | Hyp | Ref
| Expression |
1 | | bj-bary1.s |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
2 | | bj-bary1.a |
. . . . . . . . 9
โข (๐ โ ๐ด โ โ) |
3 | 1, 2 | mulcld 11234 |
. . . . . . . 8
โข (๐ โ (๐ ยท ๐ด) โ โ) |
4 | | bj-bary1.t |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
5 | | bj-bary1.b |
. . . . . . . . 9
โข (๐ โ ๐ต โ โ) |
6 | 4, 5 | mulcld 11234 |
. . . . . . . 8
โข (๐ โ (๐ ยท ๐ต) โ โ) |
7 | 3, 6 | addcomd 11416 |
. . . . . . 7
โข (๐ โ ((๐ ยท ๐ด) + (๐ ยท ๐ต)) = ((๐ ยท ๐ต) + (๐ ยท ๐ด))) |
8 | 7 | eqeq2d 2744 |
. . . . . 6
โข (๐ โ (๐ = ((๐ ยท ๐ด) + (๐ ยท ๐ต)) โ ๐ = ((๐ ยท ๐ต) + (๐ ยท ๐ด)))) |
9 | 8 | biimpd 228 |
. . . . 5
โข (๐ โ (๐ = ((๐ ยท ๐ด) + (๐ ยท ๐ต)) โ ๐ = ((๐ ยท ๐ต) + (๐ ยท ๐ด)))) |
10 | 1, 4 | addcomd 11416 |
. . . . . . 7
โข (๐ โ (๐ + ๐) = (๐ + ๐)) |
11 | 10 | eqeq1d 2735 |
. . . . . 6
โข (๐ โ ((๐ + ๐) = 1 โ (๐ + ๐) = 1)) |
12 | 11 | biimpd 228 |
. . . . 5
โข (๐ โ ((๐ + ๐) = 1 โ (๐ + ๐) = 1)) |
13 | | bj-bary1.x |
. . . . . 6
โข (๐ โ ๐ โ โ) |
14 | | bj-bary1.neq |
. . . . . . 7
โข (๐ โ ๐ด โ ๐ต) |
15 | 14 | necomd 2997 |
. . . . . 6
โข (๐ โ ๐ต โ ๐ด) |
16 | 5, 2, 13, 15, 4, 1 | bj-bary1lem1 36192 |
. . . . 5
โข (๐ โ ((๐ = ((๐ ยท ๐ต) + (๐ ยท ๐ด)) โง (๐ + ๐) = 1) โ ๐ = ((๐ โ ๐ต) / (๐ด โ ๐ต)))) |
17 | 9, 12, 16 | syl2and 609 |
. . . 4
โข (๐ โ ((๐ = ((๐ ยท ๐ด) + (๐ ยท ๐ต)) โง (๐ + ๐) = 1) โ ๐ = ((๐ โ ๐ต) / (๐ด โ ๐ต)))) |
18 | 13, 5, 2, 5, 14 | div2subd 12040 |
. . . . 5
โข (๐ โ ((๐ โ ๐ต) / (๐ด โ ๐ต)) = ((๐ต โ ๐) / (๐ต โ ๐ด))) |
19 | 18 | eqeq2d 2744 |
. . . 4
โข (๐ โ (๐ = ((๐ โ ๐ต) / (๐ด โ ๐ต)) โ ๐ = ((๐ต โ ๐) / (๐ต โ ๐ด)))) |
20 | 17, 19 | sylibd 238 |
. . 3
โข (๐ โ ((๐ = ((๐ ยท ๐ด) + (๐ ยท ๐ต)) โง (๐ + ๐) = 1) โ ๐ = ((๐ต โ ๐) / (๐ต โ ๐ด)))) |
21 | 2, 5, 13, 14, 1, 4 | bj-bary1lem1 36192 |
. . 3
โข (๐ โ ((๐ = ((๐ ยท ๐ด) + (๐ ยท ๐ต)) โง (๐ + ๐) = 1) โ ๐ = ((๐ โ ๐ด) / (๐ต โ ๐ด)))) |
22 | 20, 21 | jcad 514 |
. 2
โข (๐ โ ((๐ = ((๐ ยท ๐ด) + (๐ ยท ๐ต)) โง (๐ + ๐) = 1) โ (๐ = ((๐ต โ ๐) / (๐ต โ ๐ด)) โง ๐ = ((๐ โ ๐ด) / (๐ต โ ๐ด))))) |
23 | 2, 5, 13, 14 | bj-bary1lem 36191 |
. . . 4
โข (๐ โ ๐ = ((((๐ต โ ๐) / (๐ต โ ๐ด)) ยท ๐ด) + (((๐ โ ๐ด) / (๐ต โ ๐ด)) ยท ๐ต))) |
24 | | oveq1 7416 |
. . . . . 6
โข (๐ = ((๐ต โ ๐) / (๐ต โ ๐ด)) โ (๐ ยท ๐ด) = (((๐ต โ ๐) / (๐ต โ ๐ด)) ยท ๐ด)) |
25 | | oveq1 7416 |
. . . . . 6
โข (๐ = ((๐ โ ๐ด) / (๐ต โ ๐ด)) โ (๐ ยท ๐ต) = (((๐ โ ๐ด) / (๐ต โ ๐ด)) ยท ๐ต)) |
26 | 24, 25 | oveqan12d 7428 |
. . . . 5
โข ((๐ = ((๐ต โ ๐) / (๐ต โ ๐ด)) โง ๐ = ((๐ โ ๐ด) / (๐ต โ ๐ด))) โ ((๐ ยท ๐ด) + (๐ ยท ๐ต)) = ((((๐ต โ ๐) / (๐ต โ ๐ด)) ยท ๐ด) + (((๐ โ ๐ด) / (๐ต โ ๐ด)) ยท ๐ต))) |
27 | 26 | a1i 11 |
. . . 4
โข (๐ โ ((๐ = ((๐ต โ ๐) / (๐ต โ ๐ด)) โง ๐ = ((๐ โ ๐ด) / (๐ต โ ๐ด))) โ ((๐ ยท ๐ด) + (๐ ยท ๐ต)) = ((((๐ต โ ๐) / (๐ต โ ๐ด)) ยท ๐ด) + (((๐ โ ๐ด) / (๐ต โ ๐ด)) ยท ๐ต)))) |
28 | | eqtr3 2759 |
. . . 4
โข ((๐ = ((((๐ต โ ๐) / (๐ต โ ๐ด)) ยท ๐ด) + (((๐ โ ๐ด) / (๐ต โ ๐ด)) ยท ๐ต)) โง ((๐ ยท ๐ด) + (๐ ยท ๐ต)) = ((((๐ต โ ๐) / (๐ต โ ๐ด)) ยท ๐ด) + (((๐ โ ๐ด) / (๐ต โ ๐ด)) ยท ๐ต))) โ ๐ = ((๐ ยท ๐ด) + (๐ ยท ๐ต))) |
29 | 23, 27, 28 | syl6an 683 |
. . 3
โข (๐ โ ((๐ = ((๐ต โ ๐) / (๐ต โ ๐ด)) โง ๐ = ((๐ โ ๐ด) / (๐ต โ ๐ด))) โ ๐ = ((๐ ยท ๐ด) + (๐ ยท ๐ต)))) |
30 | | oveq12 7418 |
. . . 4
โข ((๐ = ((๐ต โ ๐) / (๐ต โ ๐ด)) โง ๐ = ((๐ โ ๐ด) / (๐ต โ ๐ด))) โ (๐ + ๐) = (((๐ต โ ๐) / (๐ต โ ๐ด)) + ((๐ โ ๐ด) / (๐ต โ ๐ด)))) |
31 | 5, 13 | subcld 11571 |
. . . . . . 7
โข (๐ โ (๐ต โ ๐) โ โ) |
32 | 13, 2 | subcld 11571 |
. . . . . . 7
โข (๐ โ (๐ โ ๐ด) โ โ) |
33 | 5, 2 | subcld 11571 |
. . . . . . 7
โข (๐ โ (๐ต โ ๐ด) โ โ) |
34 | 5, 2, 15 | subne0d 11580 |
. . . . . . 7
โข (๐ โ (๐ต โ ๐ด) โ 0) |
35 | 31, 32, 33, 34 | divdird 12028 |
. . . . . 6
โข (๐ โ (((๐ต โ ๐) + (๐ โ ๐ด)) / (๐ต โ ๐ด)) = (((๐ต โ ๐) / (๐ต โ ๐ด)) + ((๐ โ ๐ด) / (๐ต โ ๐ด)))) |
36 | 5, 13, 2 | npncand 11595 |
. . . . . . 7
โข (๐ โ ((๐ต โ ๐) + (๐ โ ๐ด)) = (๐ต โ ๐ด)) |
37 | 33, 34, 36 | diveq1bd 12038 |
. . . . . 6
โข (๐ โ (((๐ต โ ๐) + (๐ โ ๐ด)) / (๐ต โ ๐ด)) = 1) |
38 | 35, 37 | eqtr3d 2775 |
. . . . 5
โข (๐ โ (((๐ต โ ๐) / (๐ต โ ๐ด)) + ((๐ โ ๐ด) / (๐ต โ ๐ด))) = 1) |
39 | 38 | eqeq2d 2744 |
. . . 4
โข (๐ โ ((๐ + ๐) = (((๐ต โ ๐) / (๐ต โ ๐ด)) + ((๐ โ ๐ด) / (๐ต โ ๐ด))) โ (๐ + ๐) = 1)) |
40 | 30, 39 | imbitrid 243 |
. . 3
โข (๐ โ ((๐ = ((๐ต โ ๐) / (๐ต โ ๐ด)) โง ๐ = ((๐ โ ๐ด) / (๐ต โ ๐ด))) โ (๐ + ๐) = 1)) |
41 | 29, 40 | jcad 514 |
. 2
โข (๐ โ ((๐ = ((๐ต โ ๐) / (๐ต โ ๐ด)) โง ๐ = ((๐ โ ๐ด) / (๐ต โ ๐ด))) โ (๐ = ((๐ ยท ๐ด) + (๐ ยท ๐ต)) โง (๐ + ๐) = 1))) |
42 | 22, 41 | impbid 211 |
1
โข (๐ โ ((๐ = ((๐ ยท ๐ด) + (๐ ยท ๐ต)) โง (๐ + ๐) = 1) โ (๐ = ((๐ต โ ๐) / (๐ต โ ๐ด)) โง ๐ = ((๐ โ ๐ด) / (๐ต โ ๐ด))))) |