Step | Hyp | Ref
| Expression |
1 | | elznn0nn 12520 |
. . 3
โข (๐ต โ โค โ (๐ต โ โ0 โจ
(๐ต โ โ โง
-๐ต โ
โ))) |
2 | | expcllem.1 |
. . . . . . 7
โข ๐น โ
โ |
3 | | expcllem.2 |
. . . . . . 7
โข ((๐ฅ โ ๐น โง ๐ฆ โ ๐น) โ (๐ฅ ยท ๐ฆ) โ ๐น) |
4 | | expcllem.3 |
. . . . . . 7
โข 1 โ
๐น |
5 | 2, 3, 4 | expcllem 13985 |
. . . . . 6
โข ((๐ด โ ๐น โง ๐ต โ โ0) โ (๐ดโ๐ต) โ ๐น) |
6 | 5 | ex 414 |
. . . . 5
โข (๐ด โ ๐น โ (๐ต โ โ0 โ (๐ดโ๐ต) โ ๐น)) |
7 | 6 | adantr 482 |
. . . 4
โข ((๐ด โ ๐น โง ๐ด โ 0) โ (๐ต โ โ0 โ (๐ดโ๐ต) โ ๐น)) |
8 | | simpll 766 |
. . . . . . . 8
โข (((๐ด โ ๐น โง ๐ด โ 0) โง (๐ต โ โ โง -๐ต โ โ)) โ ๐ด โ ๐น) |
9 | 2, 8 | sselid 3947 |
. . . . . . 7
โข (((๐ด โ ๐น โง ๐ด โ 0) โง (๐ต โ โ โง -๐ต โ โ)) โ ๐ด โ โ) |
10 | | simprl 770 |
. . . . . . . 8
โข (((๐ด โ ๐น โง ๐ด โ 0) โง (๐ต โ โ โง -๐ต โ โ)) โ ๐ต โ โ) |
11 | 10 | recnd 11190 |
. . . . . . 7
โข (((๐ด โ ๐น โง ๐ด โ 0) โง (๐ต โ โ โง -๐ต โ โ)) โ ๐ต โ โ) |
12 | | nnnn0 12427 |
. . . . . . . 8
โข (-๐ต โ โ โ -๐ต โ
โ0) |
13 | 12 | ad2antll 728 |
. . . . . . 7
โข (((๐ด โ ๐น โง ๐ด โ 0) โง (๐ต โ โ โง -๐ต โ โ)) โ -๐ต โ
โ0) |
14 | | expneg2 13983 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ โง -๐ต โ โ0)
โ (๐ดโ๐ต) = (1 / (๐ดโ-๐ต))) |
15 | 9, 11, 13, 14 | syl3anc 1372 |
. . . . . 6
โข (((๐ด โ ๐น โง ๐ด โ 0) โง (๐ต โ โ โง -๐ต โ โ)) โ (๐ดโ๐ต) = (1 / (๐ดโ-๐ต))) |
16 | | difss 4096 |
. . . . . . . 8
โข (๐น โ {0}) โ ๐น |
17 | | simpl 484 |
. . . . . . . . . 10
โข (((๐ด โ ๐น โง ๐ด โ 0) โง (๐ต โ โ โง -๐ต โ โ)) โ (๐ด โ ๐น โง ๐ด โ 0)) |
18 | | eldifsn 4752 |
. . . . . . . . . 10
โข (๐ด โ (๐น โ {0}) โ (๐ด โ ๐น โง ๐ด โ 0)) |
19 | 17, 18 | sylibr 233 |
. . . . . . . . 9
โข (((๐ด โ ๐น โง ๐ด โ 0) โง (๐ต โ โ โง -๐ต โ โ)) โ ๐ด โ (๐น โ {0})) |
20 | 16, 2 | sstri 3958 |
. . . . . . . . . 10
โข (๐น โ {0}) โ
โ |
21 | 16 | sseli 3945 |
. . . . . . . . . . . 12
โข (๐ฅ โ (๐น โ {0}) โ ๐ฅ โ ๐น) |
22 | 16 | sseli 3945 |
. . . . . . . . . . . 12
โข (๐ฆ โ (๐น โ {0}) โ ๐ฆ โ ๐น) |
23 | 21, 22, 3 | syl2an 597 |
. . . . . . . . . . 11
โข ((๐ฅ โ (๐น โ {0}) โง ๐ฆ โ (๐น โ {0})) โ (๐ฅ ยท ๐ฆ) โ ๐น) |
24 | | eldifsn 4752 |
. . . . . . . . . . . . 13
โข (๐ฅ โ (๐น โ {0}) โ (๐ฅ โ ๐น โง ๐ฅ โ 0)) |
25 | 2 | sseli 3945 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ ๐น โ ๐ฅ โ โ) |
26 | 25 | anim1i 616 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ ๐น โง ๐ฅ โ 0) โ (๐ฅ โ โ โง ๐ฅ โ 0)) |
27 | 24, 26 | sylbi 216 |
. . . . . . . . . . . 12
โข (๐ฅ โ (๐น โ {0}) โ (๐ฅ โ โ โง ๐ฅ โ 0)) |
28 | | eldifsn 4752 |
. . . . . . . . . . . . 13
โข (๐ฆ โ (๐น โ {0}) โ (๐ฆ โ ๐น โง ๐ฆ โ 0)) |
29 | 2 | sseli 3945 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ ๐น โ ๐ฆ โ โ) |
30 | 29 | anim1i 616 |
. . . . . . . . . . . . 13
โข ((๐ฆ โ ๐น โง ๐ฆ โ 0) โ (๐ฆ โ โ โง ๐ฆ โ 0)) |
31 | 28, 30 | sylbi 216 |
. . . . . . . . . . . 12
โข (๐ฆ โ (๐น โ {0}) โ (๐ฆ โ โ โง ๐ฆ โ 0)) |
32 | | mulne0 11804 |
. . . . . . . . . . . 12
โข (((๐ฅ โ โ โง ๐ฅ โ 0) โง (๐ฆ โ โ โง ๐ฆ โ 0)) โ (๐ฅ ยท ๐ฆ) โ 0) |
33 | 27, 31, 32 | syl2an 597 |
. . . . . . . . . . 11
โข ((๐ฅ โ (๐น โ {0}) โง ๐ฆ โ (๐น โ {0})) โ (๐ฅ ยท ๐ฆ) โ 0) |
34 | | eldifsn 4752 |
. . . . . . . . . . 11
โข ((๐ฅ ยท ๐ฆ) โ (๐น โ {0}) โ ((๐ฅ ยท ๐ฆ) โ ๐น โง (๐ฅ ยท ๐ฆ) โ 0)) |
35 | 23, 33, 34 | sylanbrc 584 |
. . . . . . . . . 10
โข ((๐ฅ โ (๐น โ {0}) โง ๐ฆ โ (๐น โ {0})) โ (๐ฅ ยท ๐ฆ) โ (๐น โ {0})) |
36 | | ax-1ne0 11127 |
. . . . . . . . . . 11
โข 1 โ
0 |
37 | | eldifsn 4752 |
. . . . . . . . . . 11
โข (1 โ
(๐น โ {0}) โ (1
โ ๐น โง 1 โ
0)) |
38 | 4, 36, 37 | mpbir2an 710 |
. . . . . . . . . 10
โข 1 โ
(๐น โ
{0}) |
39 | 20, 35, 38 | expcllem 13985 |
. . . . . . . . 9
โข ((๐ด โ (๐น โ {0}) โง -๐ต โ โ0) โ (๐ดโ-๐ต) โ (๐น โ {0})) |
40 | 19, 13, 39 | syl2anc 585 |
. . . . . . . 8
โข (((๐ด โ ๐น โง ๐ด โ 0) โง (๐ต โ โ โง -๐ต โ โ)) โ (๐ดโ-๐ต) โ (๐น โ {0})) |
41 | 16, 40 | sselid 3947 |
. . . . . . 7
โข (((๐ด โ ๐น โง ๐ด โ 0) โง (๐ต โ โ โง -๐ต โ โ)) โ (๐ดโ-๐ต) โ ๐น) |
42 | | eldifsn 4752 |
. . . . . . . . 9
โข ((๐ดโ-๐ต) โ (๐น โ {0}) โ ((๐ดโ-๐ต) โ ๐น โง (๐ดโ-๐ต) โ 0)) |
43 | 40, 42 | sylib 217 |
. . . . . . . 8
โข (((๐ด โ ๐น โง ๐ด โ 0) โง (๐ต โ โ โง -๐ต โ โ)) โ ((๐ดโ-๐ต) โ ๐น โง (๐ดโ-๐ต) โ 0)) |
44 | 43 | simprd 497 |
. . . . . . 7
โข (((๐ด โ ๐น โง ๐ด โ 0) โง (๐ต โ โ โง -๐ต โ โ)) โ (๐ดโ-๐ต) โ 0) |
45 | | neeq1 3007 |
. . . . . . . . 9
โข (๐ฅ = (๐ดโ-๐ต) โ (๐ฅ โ 0 โ (๐ดโ-๐ต) โ 0)) |
46 | | oveq2 7370 |
. . . . . . . . . 10
โข (๐ฅ = (๐ดโ-๐ต) โ (1 / ๐ฅ) = (1 / (๐ดโ-๐ต))) |
47 | 46 | eleq1d 2823 |
. . . . . . . . 9
โข (๐ฅ = (๐ดโ-๐ต) โ ((1 / ๐ฅ) โ ๐น โ (1 / (๐ดโ-๐ต)) โ ๐น)) |
48 | 45, 47 | imbi12d 345 |
. . . . . . . 8
โข (๐ฅ = (๐ดโ-๐ต) โ ((๐ฅ โ 0 โ (1 / ๐ฅ) โ ๐น) โ ((๐ดโ-๐ต) โ 0 โ (1 / (๐ดโ-๐ต)) โ ๐น))) |
49 | | expcl2lem.4 |
. . . . . . . . 9
โข ((๐ฅ โ ๐น โง ๐ฅ โ 0) โ (1 / ๐ฅ) โ ๐น) |
50 | 49 | ex 414 |
. . . . . . . 8
โข (๐ฅ โ ๐น โ (๐ฅ โ 0 โ (1 / ๐ฅ) โ ๐น)) |
51 | 48, 50 | vtoclga 3537 |
. . . . . . 7
โข ((๐ดโ-๐ต) โ ๐น โ ((๐ดโ-๐ต) โ 0 โ (1 / (๐ดโ-๐ต)) โ ๐น)) |
52 | 41, 44, 51 | sylc 65 |
. . . . . 6
โข (((๐ด โ ๐น โง ๐ด โ 0) โง (๐ต โ โ โง -๐ต โ โ)) โ (1 / (๐ดโ-๐ต)) โ ๐น) |
53 | 15, 52 | eqeltrd 2838 |
. . . . 5
โข (((๐ด โ ๐น โง ๐ด โ 0) โง (๐ต โ โ โง -๐ต โ โ)) โ (๐ดโ๐ต) โ ๐น) |
54 | 53 | ex 414 |
. . . 4
โข ((๐ด โ ๐น โง ๐ด โ 0) โ ((๐ต โ โ โง -๐ต โ โ) โ (๐ดโ๐ต) โ ๐น)) |
55 | 7, 54 | jaod 858 |
. . 3
โข ((๐ด โ ๐น โง ๐ด โ 0) โ ((๐ต โ โ0 โจ (๐ต โ โ โง -๐ต โ โ)) โ (๐ดโ๐ต) โ ๐น)) |
56 | 1, 55 | biimtrid 241 |
. 2
โข ((๐ด โ ๐น โง ๐ด โ 0) โ (๐ต โ โค โ (๐ดโ๐ต) โ ๐น)) |
57 | 56 | 3impia 1118 |
1
โข ((๐ด โ ๐น โง ๐ด โ 0 โง ๐ต โ โค) โ (๐ดโ๐ต) โ ๐น) |