Step | Hyp | Ref
| Expression |
1 | | climneg.1 |
. . 3
โข
โฒ๐๐ |
2 | | nfmpt1 5214 |
. . 3
โข
โฒ๐(๐ โ ๐ โฆ -1) |
3 | | climneg.2 |
. . 3
โข
โฒ๐๐น |
4 | | nfmpt1 5214 |
. . 3
โข
โฒ๐(๐ โ ๐ โฆ -(๐นโ๐)) |
5 | | climneg.3 |
. . 3
โข ๐ =
(โคโฅโ๐) |
6 | | climneg.4 |
. . 3
โข (๐ โ ๐ โ โค) |
7 | 5 | fvexi 6857 |
. . . . . 6
โข ๐ โ V |
8 | 7 | mptex 7174 |
. . . . 5
โข (๐ โ ๐ โฆ -1) โ V |
9 | 8 | a1i 11 |
. . . 4
โข (๐ โ (๐ โ ๐ โฆ -1) โ V) |
10 | | 1cnd 11151 |
. . . . 5
โข (๐ โ 1 โ
โ) |
11 | 10 | negcld 11500 |
. . . 4
โข (๐ โ -1 โ
โ) |
12 | | eqidd 2738 |
. . . . . 6
โข (๐ โ ๐ โ (๐ โ ๐ โฆ -1) = (๐ โ ๐ โฆ -1)) |
13 | | eqidd 2738 |
. . . . . 6
โข ((๐ โ ๐ โง ๐ = ๐) โ -1 = -1) |
14 | | id 22 |
. . . . . 6
โข (๐ โ ๐ โ ๐ โ ๐) |
15 | | 1cnd 11151 |
. . . . . . 7
โข (๐ โ ๐ โ 1 โ โ) |
16 | 15 | negcld 11500 |
. . . . . 6
โข (๐ โ ๐ โ -1 โ โ) |
17 | 12, 13, 14, 16 | fvmptd 6956 |
. . . . 5
โข (๐ โ ๐ โ ((๐ โ ๐ โฆ -1)โ๐) = -1) |
18 | 17 | adantl 483 |
. . . 4
โข ((๐ โง ๐ โ ๐) โ ((๐ โ ๐ โฆ -1)โ๐) = -1) |
19 | 5, 6, 9, 11, 18 | climconst 15426 |
. . 3
โข (๐ โ (๐ โ ๐ โฆ -1) โ -1) |
20 | 7 | mptex 7174 |
. . . 4
โข (๐ โ ๐ โฆ -(๐นโ๐)) โ V |
21 | 20 | a1i 11 |
. . 3
โข (๐ โ (๐ โ ๐ โฆ -(๐นโ๐)) โ V) |
22 | | climneg.5 |
. . 3
โข (๐ โ ๐น โ ๐ด) |
23 | | neg1cn 12268 |
. . . . . 6
โข -1 โ
โ |
24 | | eqid 2737 |
. . . . . . 7
โข (๐ โ ๐ โฆ -1) = (๐ โ ๐ โฆ -1) |
25 | 24 | fvmpt2 6960 |
. . . . . 6
โข ((๐ โ ๐ โง -1 โ โ) โ ((๐ โ ๐ โฆ -1)โ๐) = -1) |
26 | 23, 25 | mpan2 690 |
. . . . 5
โข (๐ โ ๐ โ ((๐ โ ๐ โฆ -1)โ๐) = -1) |
27 | 26, 23 | eqeltrdi 2846 |
. . . 4
โข (๐ โ ๐ โ ((๐ โ ๐ โฆ -1)โ๐) โ โ) |
28 | 27 | adantl 483 |
. . 3
โข ((๐ โง ๐ โ ๐) โ ((๐ โ ๐ โฆ -1)โ๐) โ โ) |
29 | | climneg.6 |
. . 3
โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) โ โ) |
30 | | simpr 486 |
. . . . 5
โข ((๐ โง ๐ โ ๐) โ ๐ โ ๐) |
31 | 29 | negcld 11500 |
. . . . 5
โข ((๐ โง ๐ โ ๐) โ -(๐นโ๐) โ โ) |
32 | | eqid 2737 |
. . . . . 6
โข (๐ โ ๐ โฆ -(๐นโ๐)) = (๐ โ ๐ โฆ -(๐นโ๐)) |
33 | 32 | fvmpt2 6960 |
. . . . 5
โข ((๐ โ ๐ โง -(๐นโ๐) โ โ) โ ((๐ โ ๐ โฆ -(๐นโ๐))โ๐) = -(๐นโ๐)) |
34 | 30, 31, 33 | syl2anc 585 |
. . . 4
โข ((๐ โง ๐ โ ๐) โ ((๐ โ ๐ โฆ -(๐นโ๐))โ๐) = -(๐นโ๐)) |
35 | 29 | mulm1d 11608 |
. . . 4
โข ((๐ โง ๐ โ ๐) โ (-1 ยท (๐นโ๐)) = -(๐นโ๐)) |
36 | 26 | eqcomd 2743 |
. . . . . 6
โข (๐ โ ๐ โ -1 = ((๐ โ ๐ โฆ -1)โ๐)) |
37 | 36 | adantl 483 |
. . . . 5
โข ((๐ โง ๐ โ ๐) โ -1 = ((๐ โ ๐ โฆ -1)โ๐)) |
38 | 37 | oveq1d 7373 |
. . . 4
โข ((๐ โง ๐ โ ๐) โ (-1 ยท (๐นโ๐)) = (((๐ โ ๐ โฆ -1)โ๐) ยท (๐นโ๐))) |
39 | 34, 35, 38 | 3eqtr2d 2783 |
. . 3
โข ((๐ โง ๐ โ ๐) โ ((๐ โ ๐ โฆ -(๐นโ๐))โ๐) = (((๐ โ ๐ โฆ -1)โ๐) ยท (๐นโ๐))) |
40 | 1, 2, 3, 4, 5, 6, 19, 21, 22, 28, 29, 39 | climmulf 43852 |
. 2
โข (๐ โ (๐ โ ๐ โฆ -(๐นโ๐)) โ (-1 ยท ๐ด)) |
41 | | climcl 15382 |
. . . 4
โข (๐น โ ๐ด โ ๐ด โ โ) |
42 | 22, 41 | syl 17 |
. . 3
โข (๐ โ ๐ด โ โ) |
43 | 42 | mulm1d 11608 |
. 2
โข (๐ โ (-1 ยท ๐ด) = -๐ด) |
44 | 40, 43 | breqtrd 5132 |
1
โข (๐ โ (๐ โ ๐ โฆ -(๐นโ๐)) โ -๐ด) |