Step | Hyp | Ref
| Expression |
1 | | simp1l 1198 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ ๐ด โ โ) |
2 | | 1cnd 11209 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ 1 โ โ) |
3 | | simp2l 1200 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ ๐ต โ โ) |
4 | | simp1r 1199 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ ๐ด โ 0) |
5 | 3, 1, 4 | divcld 11990 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ (๐ต / ๐ด) โ โ) |
6 | 1, 2, 5 | subdid 11670 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ (๐ด ยท (1 โ (๐ต / ๐ด))) = ((๐ด ยท 1) โ (๐ด ยท (๐ต / ๐ด)))) |
7 | 1 | mulridd 11231 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ (๐ด ยท 1) = ๐ด) |
8 | 3, 1, 4 | divcan2d 11992 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ (๐ด ยท (๐ต / ๐ด)) = ๐ต) |
9 | 7, 8 | oveq12d 7427 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ ((๐ด ยท 1) โ (๐ด ยท (๐ต / ๐ด))) = (๐ด โ ๐ต)) |
10 | 6, 9 | eqtrd 2773 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ (๐ด ยท (1 โ (๐ต / ๐ด))) = (๐ด โ ๐ต)) |
11 | 10, 7 | oveq12d 7427 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ ((๐ด ยท (1 โ (๐ต / ๐ด)))๐น(๐ด ยท 1)) = ((๐ด โ ๐ต)๐น๐ด)) |
12 | 2, 5 | subcld 11571 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ (1 โ (๐ต / ๐ด)) โ โ) |
13 | | simp3 1139 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ ๐ด โ ๐ต) |
14 | 13 | necomd 2997 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ ๐ต โ ๐ด) |
15 | 3, 1, 4, 14 | divne1d 12001 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ (๐ต / ๐ด) โ 1) |
16 | 15 | necomd 2997 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ 1 โ (๐ต / ๐ด)) |
17 | 2, 5, 16 | subne0d 11580 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ (1 โ (๐ต / ๐ด)) โ 0) |
18 | | ax-1ne0 11179 |
. . . . . . 7
โข 1 โ
0 |
19 | 18 | a1i 11 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ 1 โ 0) |
20 | | ang.1 |
. . . . . . 7
โข ๐น = (๐ฅ โ (โ โ {0}), ๐ฆ โ (โ โ {0})
โฆ (โโ(logโ(๐ฆ / ๐ฅ)))) |
21 | 20 | angcan 26307 |
. . . . . 6
โข ((((1
โ (๐ต / ๐ด)) โ โ โง (1
โ (๐ต / ๐ด)) โ 0) โง (1 โ
โ โง 1 โ 0) โง (๐ด โ โ โง ๐ด โ 0)) โ ((๐ด ยท (1 โ (๐ต / ๐ด)))๐น(๐ด ยท 1)) = ((1 โ (๐ต / ๐ด))๐น1)) |
22 | 12, 17, 2, 19, 1, 4,
21 | syl222anc 1387 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ ((๐ด ยท (1 โ (๐ต / ๐ด)))๐น(๐ด ยท 1)) = ((1 โ (๐ต / ๐ด))๐น1)) |
23 | 11, 22 | eqtr3d 2775 |
. . . 4
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ ((๐ด โ ๐ต)๐น๐ด) = ((1 โ (๐ต / ๐ด))๐น1)) |
24 | 1, 5, 2 | subdid 11670 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ (๐ด ยท ((๐ต / ๐ด) โ 1)) = ((๐ด ยท (๐ต / ๐ด)) โ (๐ด ยท 1))) |
25 | 8, 7 | oveq12d 7427 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ ((๐ด ยท (๐ต / ๐ด)) โ (๐ด ยท 1)) = (๐ต โ ๐ด)) |
26 | 24, 25 | eqtrd 2773 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ (๐ด ยท ((๐ต / ๐ด) โ 1)) = (๐ต โ ๐ด)) |
27 | 8, 26 | oveq12d 7427 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ ((๐ด ยท (๐ต / ๐ด))๐น(๐ด ยท ((๐ต / ๐ด) โ 1))) = (๐ต๐น(๐ต โ ๐ด))) |
28 | | simp2r 1201 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ ๐ต โ 0) |
29 | 3, 1, 28, 4 | divne0d 12006 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ (๐ต / ๐ด) โ 0) |
30 | 5, 2 | subcld 11571 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ ((๐ต / ๐ด) โ 1) โ
โ) |
31 | 5, 2, 15 | subne0d 11580 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ ((๐ต / ๐ด) โ 1) โ 0) |
32 | 20 | angcan 26307 |
. . . . . 6
โข ((((๐ต / ๐ด) โ โ โง (๐ต / ๐ด) โ 0) โง (((๐ต / ๐ด) โ 1) โ โ โง ((๐ต / ๐ด) โ 1) โ 0) โง (๐ด โ โ โง ๐ด โ 0)) โ ((๐ด ยท (๐ต / ๐ด))๐น(๐ด ยท ((๐ต / ๐ด) โ 1))) = ((๐ต / ๐ด)๐น((๐ต / ๐ด) โ 1))) |
33 | 5, 29, 30, 31, 1, 4, 32 | syl222anc 1387 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ ((๐ด ยท (๐ต / ๐ด))๐น(๐ด ยท ((๐ต / ๐ด) โ 1))) = ((๐ต / ๐ด)๐น((๐ต / ๐ด) โ 1))) |
34 | 27, 33 | eqtr3d 2775 |
. . . 4
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ (๐ต๐น(๐ต โ ๐ด)) = ((๐ต / ๐ด)๐น((๐ต / ๐ด) โ 1))) |
35 | 23, 34 | oveq12d 7427 |
. . 3
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ (((๐ด โ ๐ต)๐น๐ด) + (๐ต๐น(๐ต โ ๐ด))) = (((1 โ (๐ต / ๐ด))๐น1) + ((๐ต / ๐ด)๐น((๐ต / ๐ด) โ 1)))) |
36 | 7, 8 | oveq12d 7427 |
. . . 4
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ ((๐ด ยท 1)๐น(๐ด ยท (๐ต / ๐ด))) = (๐ด๐น๐ต)) |
37 | 20 | angcan 26307 |
. . . . 5
โข (((1
โ โ โง 1 โ 0) โง ((๐ต / ๐ด) โ โ โง (๐ต / ๐ด) โ 0) โง (๐ด โ โ โง ๐ด โ 0)) โ ((๐ด ยท 1)๐น(๐ด ยท (๐ต / ๐ด))) = (1๐น(๐ต / ๐ด))) |
38 | 2, 19, 5, 29, 1, 4,
37 | syl222anc 1387 |
. . . 4
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ ((๐ด ยท 1)๐น(๐ด ยท (๐ต / ๐ด))) = (1๐น(๐ต / ๐ด))) |
39 | 36, 38 | eqtr3d 2775 |
. . 3
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ (๐ด๐น๐ต) = (1๐น(๐ต / ๐ด))) |
40 | 35, 39 | oveq12d 7427 |
. 2
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ ((((๐ด โ ๐ต)๐น๐ด) + (๐ต๐น(๐ต โ ๐ด))) + (๐ด๐น๐ต)) = ((((1 โ (๐ต / ๐ด))๐น1) + ((๐ต / ๐ด)๐น((๐ต / ๐ด) โ 1))) + (1๐น(๐ต / ๐ด)))) |
41 | 20 | ang180lem4 26317 |
. . 3
โข (((๐ต / ๐ด) โ โ โง (๐ต / ๐ด) โ 0 โง (๐ต / ๐ด) โ 1) โ ((((1 โ (๐ต / ๐ด))๐น1) + ((๐ต / ๐ด)๐น((๐ต / ๐ด) โ 1))) + (1๐น(๐ต / ๐ด))) โ {-ฯ, ฯ}) |
42 | 5, 29, 15, 41 | syl3anc 1372 |
. 2
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ ((((1 โ (๐ต / ๐ด))๐น1) + ((๐ต / ๐ด)๐น((๐ต / ๐ด) โ 1))) + (1๐น(๐ต / ๐ด))) โ {-ฯ, ฯ}) |
43 | 40, 42 | eqeltrd 2834 |
1
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ด โ ๐ต) โ ((((๐ด โ ๐ต)๐น๐ด) + (๐ต๐น(๐ต โ ๐ด))) + (๐ด๐น๐ต)) โ {-ฯ, ฯ}) |