Step | Hyp | Ref
| Expression |
1 | | cnelprrecn 11151 |
. . . 4
โข โ
โ {โ, โ} |
2 | 1 | a1i 11 |
. . 3
โข (๐ โ โ โ {โ,
โ}) |
3 | | 1cnd 11157 |
. . . 4
โข ((๐ โง ๐ฅ โ โ) โ 1 โ
โ) |
4 | | simpr 486 |
. . . 4
โข ((๐ โง ๐ฅ โ โ) โ ๐ฅ โ โ) |
5 | 3, 4 | subcld 11519 |
. . 3
โข ((๐ โง ๐ฅ โ โ) โ (1 โ ๐ฅ) โ
โ) |
6 | | neg1cn 12274 |
. . . 4
โข -1 โ
โ |
7 | 6 | a1i 11 |
. . 3
โข ((๐ โง ๐ฅ โ โ) โ -1 โ
โ) |
8 | | simpr 486 |
. . . 4
โข ((๐ โง ๐ฆ โ โ) โ ๐ฆ โ โ) |
9 | | lcmineqlem8.3 |
. . . . . . 7
โข (๐ โ ๐ < ๐) |
10 | | lcmineqlem8.1 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
11 | 10 | nnzd 12533 |
. . . . . . . 8
โข (๐ โ ๐ โ โค) |
12 | | lcmineqlem8.2 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
13 | 12 | nnzd 12533 |
. . . . . . . 8
โข (๐ โ ๐ โ โค) |
14 | | znnsub 12556 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โค) โ (๐ < ๐ โ (๐ โ ๐) โ โ)) |
15 | 11, 13, 14 | syl2anc 585 |
. . . . . . 7
โข (๐ โ (๐ < ๐ โ (๐ โ ๐) โ โ)) |
16 | 9, 15 | mpbid 231 |
. . . . . 6
โข (๐ โ (๐ โ ๐) โ โ) |
17 | 16 | nnnn0d 12480 |
. . . . 5
โข (๐ โ (๐ โ ๐) โ
โ0) |
18 | 17 | adantr 482 |
. . . 4
โข ((๐ โง ๐ฆ โ โ) โ (๐ โ ๐) โ
โ0) |
19 | 8, 18 | expcld 14058 |
. . 3
โข ((๐ โง ๐ฆ โ โ) โ (๐ฆโ(๐ โ ๐)) โ โ) |
20 | 12 | nncnd 12176 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
21 | 20 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ฆ โ โ) โ ๐ โ โ) |
22 | 10 | nncnd 12176 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
23 | 22 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ฆ โ โ) โ ๐ โ โ) |
24 | 21, 23 | subcld 11519 |
. . . 4
โข ((๐ โง ๐ฆ โ โ) โ (๐ โ ๐) โ โ) |
25 | | nnm1nn0 12461 |
. . . . . . 7
โข ((๐ โ ๐) โ โ โ ((๐ โ ๐) โ 1) โ
โ0) |
26 | 16, 25 | syl 17 |
. . . . . 6
โข (๐ โ ((๐ โ ๐) โ 1) โ
โ0) |
27 | 26 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ฆ โ โ) โ ((๐ โ ๐) โ 1) โ
โ0) |
28 | | expcl 13992 |
. . . . 5
โข ((๐ฆ โ โ โง ((๐ โ ๐) โ 1) โ โ0)
โ (๐ฆโ((๐ โ ๐) โ 1)) โ
โ) |
29 | 8, 27, 28 | syl2anc 585 |
. . . 4
โข ((๐ โง ๐ฆ โ โ) โ (๐ฆโ((๐ โ ๐) โ 1)) โ
โ) |
30 | 24, 29 | mulcld 11182 |
. . 3
โข ((๐ โง ๐ฆ โ โ) โ ((๐ โ ๐) ยท (๐ฆโ((๐ โ ๐) โ 1))) โ
โ) |
31 | | lcmineqlem7 40521 |
. . . 4
โข (โ
D (๐ฅ โ โ โฆ
(1 โ ๐ฅ))) = (๐ฅ โ โ โฆ
-1) |
32 | 31 | a1i 11 |
. . 3
โข (๐ โ (โ D (๐ฅ โ โ โฆ (1
โ ๐ฅ))) = (๐ฅ โ โ โฆ
-1)) |
33 | | dvexp 25333 |
. . . 4
โข ((๐ โ ๐) โ โ โ (โ D (๐ฆ โ โ โฆ (๐ฆโ(๐ โ ๐)))) = (๐ฆ โ โ โฆ ((๐ โ ๐) ยท (๐ฆโ((๐ โ ๐) โ 1))))) |
34 | 16, 33 | syl 17 |
. . 3
โข (๐ โ (โ D (๐ฆ โ โ โฆ (๐ฆโ(๐ โ ๐)))) = (๐ฆ โ โ โฆ ((๐ โ ๐) ยท (๐ฆโ((๐ โ ๐) โ 1))))) |
35 | | oveq1 7369 |
. . 3
โข (๐ฆ = (1 โ ๐ฅ) โ (๐ฆโ(๐ โ ๐)) = ((1 โ ๐ฅ)โ(๐ โ ๐))) |
36 | | oveq1 7369 |
. . . 4
โข (๐ฆ = (1 โ ๐ฅ) โ (๐ฆโ((๐ โ ๐) โ 1)) = ((1 โ ๐ฅ)โ((๐ โ ๐) โ 1))) |
37 | 36 | oveq2d 7378 |
. . 3
โข (๐ฆ = (1 โ ๐ฅ) โ ((๐ โ ๐) ยท (๐ฆโ((๐ โ ๐) โ 1))) = ((๐ โ ๐) ยท ((1 โ ๐ฅ)โ((๐ โ ๐) โ 1)))) |
38 | 2, 2, 5, 7, 19, 30, 32, 34, 35, 37 | dvmptco 25352 |
. 2
โข (๐ โ (โ D (๐ฅ โ โ โฆ ((1
โ ๐ฅ)โ(๐ โ ๐)))) = (๐ฅ โ โ โฆ (((๐ โ ๐) ยท ((1 โ ๐ฅ)โ((๐ โ ๐) โ 1))) ยท
-1))) |
39 | 20 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ โ) โ ๐ โ โ) |
40 | 22 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ โ) โ ๐ โ โ) |
41 | 39, 40 | subcld 11519 |
. . . . . 6
โข ((๐ โง ๐ฅ โ โ) โ (๐ โ ๐) โ โ) |
42 | | ax-1cn 11116 |
. . . . . . . 8
โข 1 โ
โ |
43 | | subcl 11407 |
. . . . . . . 8
โข ((1
โ โ โง ๐ฅ
โ โ) โ (1 โ ๐ฅ) โ โ) |
44 | 42, 43 | mpan 689 |
. . . . . . 7
โข (๐ฅ โ โ โ (1
โ ๐ฅ) โ
โ) |
45 | | expcl 13992 |
. . . . . . 7
โข (((1
โ ๐ฅ) โ โ
โง ((๐ โ ๐) โ 1) โ
โ0) โ ((1 โ ๐ฅ)โ((๐ โ ๐) โ 1)) โ
โ) |
46 | 44, 26, 45 | syl2anr 598 |
. . . . . 6
โข ((๐ โง ๐ฅ โ โ) โ ((1 โ ๐ฅ)โ((๐ โ ๐) โ 1)) โ
โ) |
47 | 41, 46, 7 | mul32d 11372 |
. . . . 5
โข ((๐ โง ๐ฅ โ โ) โ (((๐ โ ๐) ยท ((1 โ ๐ฅ)โ((๐ โ ๐) โ 1))) ยท -1) = (((๐ โ ๐) ยท -1) ยท ((1 โ ๐ฅ)โ((๐ โ ๐) โ 1)))) |
48 | 20, 22 | subcld 11519 |
. . . . . . . 8
โข (๐ โ (๐ โ ๐) โ โ) |
49 | 6 | a1i 11 |
. . . . . . . 8
โข (๐ โ -1 โ
โ) |
50 | 48, 49 | mulcomd 11183 |
. . . . . . 7
โข (๐ โ ((๐ โ ๐) ยท -1) = (-1 ยท (๐ โ ๐))) |
51 | 50 | oveq1d 7377 |
. . . . . 6
โข (๐ โ (((๐ โ ๐) ยท -1) ยท ((1 โ ๐ฅ)โ((๐ โ ๐) โ 1))) = ((-1 ยท (๐ โ ๐)) ยท ((1 โ ๐ฅ)โ((๐ โ ๐) โ 1)))) |
52 | 51 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ฅ โ โ) โ (((๐ โ ๐) ยท -1) ยท ((1 โ ๐ฅ)โ((๐ โ ๐) โ 1))) = ((-1 ยท (๐ โ ๐)) ยท ((1 โ ๐ฅ)โ((๐ โ ๐) โ 1)))) |
53 | 47, 52 | eqtrd 2777 |
. . . 4
โข ((๐ โง ๐ฅ โ โ) โ (((๐ โ ๐) ยท ((1 โ ๐ฅ)โ((๐ โ ๐) โ 1))) ยท -1) = ((-1 ยท
(๐ โ ๐)) ยท ((1 โ ๐ฅ)โ((๐ โ ๐) โ 1)))) |
54 | 48 | mulm1d 11614 |
. . . . . 6
โข (๐ โ (-1 ยท (๐ โ ๐)) = -(๐ โ ๐)) |
55 | 54 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ฅ โ โ) โ (-1 ยท (๐ โ ๐)) = -(๐ โ ๐)) |
56 | 55 | oveq1d 7377 |
. . . 4
โข ((๐ โง ๐ฅ โ โ) โ ((-1 ยท (๐ โ ๐)) ยท ((1 โ ๐ฅ)โ((๐ โ ๐) โ 1))) = (-(๐ โ ๐) ยท ((1 โ ๐ฅ)โ((๐ โ ๐) โ 1)))) |
57 | 53, 56 | eqtrd 2777 |
. . 3
โข ((๐ โง ๐ฅ โ โ) โ (((๐ โ ๐) ยท ((1 โ ๐ฅ)โ((๐ โ ๐) โ 1))) ยท -1) = (-(๐ โ ๐) ยท ((1 โ ๐ฅ)โ((๐ โ ๐) โ 1)))) |
58 | 57 | mpteq2dva 5210 |
. 2
โข (๐ โ (๐ฅ โ โ โฆ (((๐ โ ๐) ยท ((1 โ ๐ฅ)โ((๐ โ ๐) โ 1))) ยท -1)) = (๐ฅ โ โ โฆ (-(๐ โ ๐) ยท ((1 โ ๐ฅ)โ((๐ โ ๐) โ 1))))) |
59 | 38, 58 | eqtrd 2777 |
1
โข (๐ โ (โ D (๐ฅ โ โ โฆ ((1
โ ๐ฅ)โ(๐ โ ๐)))) = (๐ฅ โ โ โฆ (-(๐ โ ๐) ยท ((1 โ ๐ฅ)โ((๐ โ ๐) โ 1))))) |