Step | Hyp | Ref
| Expression |
1 | | elznn0nn 12568 |
. . 3
โข (๐ โ โค โ (๐ โ โ0 โจ
(๐ โ โ โง
-๐ โ
โ))) |
2 | | simpl 484 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0) โ ๐ด โ
โ) |
3 | | simpl 484 |
. . . . . 6
โข ((๐ต โ โ โง ๐ต โ 0) โ ๐ต โ
โ) |
4 | 2, 3 | anim12i 614 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โ (๐ด โ โ โง ๐ต โ
โ)) |
5 | | mulexp 14063 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ0)
โ ((๐ด ยท ๐ต)โ๐) = ((๐ดโ๐) ยท (๐ตโ๐))) |
6 | 5 | 3expa 1119 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ โ โ0)
โ ((๐ด ยท ๐ต)โ๐) = ((๐ดโ๐) ยท (๐ตโ๐))) |
7 | 4, 6 | sylan 581 |
. . . 4
โข ((((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง ๐ โ โ0)
โ ((๐ด ยท ๐ต)โ๐) = ((๐ดโ๐) ยท (๐ตโ๐))) |
8 | | simplll 774 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ โ โ โง -๐ โ โ)) โ ๐ด โ
โ) |
9 | | simplrl 776 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ โ โ โง -๐ โ โ)) โ ๐ต โ
โ) |
10 | 8, 9 | mulcld 11230 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ โ โ โง -๐ โ โ)) โ (๐ด ยท ๐ต) โ โ) |
11 | | recn 11196 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ) |
12 | 11 | ad2antrl 727 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ โ โ โง -๐ โ โ)) โ ๐ โ
โ) |
13 | | nnnn0 12475 |
. . . . . . 7
โข (-๐ โ โ โ -๐ โ
โ0) |
14 | 13 | ad2antll 728 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ โ โ โง -๐ โ โ)) โ -๐ โ
โ0) |
15 | | expneg2 14032 |
. . . . . 6
โข (((๐ด ยท ๐ต) โ โ โง ๐ โ โ โง -๐ โ โ0) โ ((๐ด ยท ๐ต)โ๐) = (1 / ((๐ด ยท ๐ต)โ-๐))) |
16 | 10, 12, 14, 15 | syl3anc 1372 |
. . . . 5
โข ((((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ โ โ โง -๐ โ โ)) โ ((๐ด ยท ๐ต)โ๐) = (1 / ((๐ด ยท ๐ต)โ-๐))) |
17 | | expneg2 14032 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โ โง -๐ โ โ0)
โ (๐ดโ๐) = (1 / (๐ดโ-๐))) |
18 | 8, 12, 14, 17 | syl3anc 1372 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ โ โ โง -๐ โ โ)) โ (๐ดโ๐) = (1 / (๐ดโ-๐))) |
19 | | expneg2 14032 |
. . . . . . . 8
โข ((๐ต โ โ โง ๐ โ โ โง -๐ โ โ0)
โ (๐ตโ๐) = (1 / (๐ตโ-๐))) |
20 | 9, 12, 14, 19 | syl3anc 1372 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ โ โ โง -๐ โ โ)) โ (๐ตโ๐) = (1 / (๐ตโ-๐))) |
21 | 18, 20 | oveq12d 7422 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ โ โ โง -๐ โ โ)) โ ((๐ดโ๐) ยท (๐ตโ๐)) = ((1 / (๐ดโ-๐)) ยท (1 / (๐ตโ-๐)))) |
22 | | mulexp 14063 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ โง -๐ โ โ0)
โ ((๐ด ยท ๐ต)โ-๐) = ((๐ดโ-๐) ยท (๐ตโ-๐))) |
23 | 8, 9, 14, 22 | syl3anc 1372 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ โ โ โง -๐ โ โ)) โ ((๐ด ยท ๐ต)โ-๐) = ((๐ดโ-๐) ยท (๐ตโ-๐))) |
24 | 23 | oveq2d 7420 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ โ โ โง -๐ โ โ)) โ (1 /
((๐ด ยท ๐ต)โ-๐)) = (1 / ((๐ดโ-๐) ยท (๐ตโ-๐)))) |
25 | | 1t1e1 12370 |
. . . . . . . . 9
โข (1
ยท 1) = 1 |
26 | 25 | oveq1i 7414 |
. . . . . . . 8
โข ((1
ยท 1) / ((๐ดโ-๐) ยท (๐ตโ-๐))) = (1 / ((๐ดโ-๐) ยท (๐ตโ-๐))) |
27 | 24, 26 | eqtr4di 2791 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ โ โ โง -๐ โ โ)) โ (1 /
((๐ด ยท ๐ต)โ-๐)) = ((1 ยท 1) / ((๐ดโ-๐) ยท (๐ตโ-๐)))) |
28 | | expcl 14041 |
. . . . . . . . 9
โข ((๐ด โ โ โง -๐ โ โ0)
โ (๐ดโ-๐) โ
โ) |
29 | 8, 14, 28 | syl2anc 585 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ โ โ โง -๐ โ โ)) โ (๐ดโ-๐) โ โ) |
30 | | simpllr 775 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ โ โ โง -๐ โ โ)) โ ๐ด โ 0) |
31 | | nnz 12575 |
. . . . . . . . . 10
โข (-๐ โ โ โ -๐ โ
โค) |
32 | 31 | ad2antll 728 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ โ โ โง -๐ โ โ)) โ -๐ โ
โค) |
33 | | expne0i 14056 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ด โ 0 โง -๐ โ โค) โ (๐ดโ-๐) โ 0) |
34 | 8, 30, 32, 33 | syl3anc 1372 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ โ โ โง -๐ โ โ)) โ (๐ดโ-๐) โ 0) |
35 | | expcl 14041 |
. . . . . . . . 9
โข ((๐ต โ โ โง -๐ โ โ0)
โ (๐ตโ-๐) โ
โ) |
36 | 9, 14, 35 | syl2anc 585 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ โ โ โง -๐ โ โ)) โ (๐ตโ-๐) โ โ) |
37 | | simplrr 777 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ โ โ โง -๐ โ โ)) โ ๐ต โ 0) |
38 | | expne0i 14056 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐ต โ 0 โง -๐ โ โค) โ (๐ตโ-๐) โ 0) |
39 | 9, 37, 32, 38 | syl3anc 1372 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ โ โ โง -๐ โ โ)) โ (๐ตโ-๐) โ 0) |
40 | | ax-1cn 11164 |
. . . . . . . . 9
โข 1 โ
โ |
41 | | divmuldiv 11910 |
. . . . . . . . 9
โข (((1
โ โ โง 1 โ โ) โง (((๐ดโ-๐) โ โ โง (๐ดโ-๐) โ 0) โง ((๐ตโ-๐) โ โ โง (๐ตโ-๐) โ 0))) โ ((1 / (๐ดโ-๐)) ยท (1 / (๐ตโ-๐))) = ((1 ยท 1) / ((๐ดโ-๐) ยท (๐ตโ-๐)))) |
42 | 40, 40, 41 | mpanl12 701 |
. . . . . . . 8
โข ((((๐ดโ-๐) โ โ โง (๐ดโ-๐) โ 0) โง ((๐ตโ-๐) โ โ โง (๐ตโ-๐) โ 0)) โ ((1 / (๐ดโ-๐)) ยท (1 / (๐ตโ-๐))) = ((1 ยท 1) / ((๐ดโ-๐) ยท (๐ตโ-๐)))) |
43 | 29, 34, 36, 39, 42 | syl22anc 838 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ โ โ โง -๐ โ โ)) โ ((1 /
(๐ดโ-๐)) ยท (1 / (๐ตโ-๐))) = ((1 ยท 1) / ((๐ดโ-๐) ยท (๐ตโ-๐)))) |
44 | 27, 43 | eqtr4d 2776 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ โ โ โง -๐ โ โ)) โ (1 /
((๐ด ยท ๐ต)โ-๐)) = ((1 / (๐ดโ-๐)) ยท (1 / (๐ตโ-๐)))) |
45 | 21, 44 | eqtr4d 2776 |
. . . . 5
โข ((((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ โ โ โง -๐ โ โ)) โ ((๐ดโ๐) ยท (๐ตโ๐)) = (1 / ((๐ด ยท ๐ต)โ-๐))) |
46 | 16, 45 | eqtr4d 2776 |
. . . 4
โข ((((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ โ โ โง -๐ โ โ)) โ ((๐ด ยท ๐ต)โ๐) = ((๐ดโ๐) ยท (๐ตโ๐))) |
47 | 7, 46 | jaodan 957 |
. . 3
โข ((((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง (๐ โ โ0 โจ
(๐ โ โ โง
-๐ โ โ))) โ
((๐ด ยท ๐ต)โ๐) = ((๐ดโ๐) ยท (๐ตโ๐))) |
48 | 1, 47 | sylan2b 595 |
. 2
โข ((((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0)) โง ๐ โ โค) โ ((๐ด ยท ๐ต)โ๐) = ((๐ดโ๐) ยท (๐ตโ๐))) |
49 | 48 | 3impa 1111 |
1
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ต โ 0) โง ๐ โ โค) โ ((๐ด ยท ๐ต)โ๐) = ((๐ดโ๐) ยท (๐ตโ๐))) |