Step | Hyp | Ref
| Expression |
1 | | oddprmdvds 16836 |
. . . 4
โข ((๐พ โ โ โง ยฌ
โ๐ โ
โ0 ๐พ =
(2โ๐)) โ
โ๐ โ (โ
โ {2})๐ โฅ ๐พ) |
2 | 1 | adantlr 714 |
. . 3
โข (((๐พ โ โ โง
((2โ๐พ) + 1) โ
โ) โง ยฌ โ๐ โ โ0 ๐พ = (2โ๐)) โ โ๐ โ (โ โ {2})๐ โฅ ๐พ) |
3 | | eldifi 4127 |
. . . . . . . 8
โข (๐ โ (โ โ {2})
โ ๐ โ
โ) |
4 | | prmnn 16611 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ) |
5 | 3, 4 | syl 17 |
. . . . . . 7
โข (๐ โ (โ โ {2})
โ ๐ โ
โ) |
6 | | simpl 484 |
. . . . . . 7
โข ((๐พ โ โ โง
((2โ๐พ) + 1) โ
โ) โ ๐พ โ
โ) |
7 | | nndivides 16207 |
. . . . . . 7
โข ((๐ โ โ โง ๐พ โ โ) โ (๐ โฅ ๐พ โ โ๐ โ โ (๐ ยท ๐) = ๐พ)) |
8 | 5, 6, 7 | syl2anr 598 |
. . . . . 6
โข (((๐พ โ โ โง
((2โ๐พ) + 1) โ
โ) โง ๐ โ
(โ โ {2})) โ (๐ โฅ ๐พ โ โ๐ โ โ (๐ ยท ๐) = ๐พ)) |
9 | | 2re 12286 |
. . . . . . . . . . . . . . . . . . 19
โข 2 โ
โ |
10 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ 2 โ
โ) |
11 | | nnnn0 12479 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ ๐ โ
โ0) |
12 | | 1le2 12421 |
. . . . . . . . . . . . . . . . . . 19
โข 1 โค
2 |
13 | 12 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ 1 โค
2) |
14 | 10, 11, 13 | expge1d 14130 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ 1 โค
(2โ๐)) |
15 | | 1zzd 12593 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ 1 โ
โค) |
16 | | 2nn 12285 |
. . . . . . . . . . . . . . . . . . . . 21
โข 2 โ
โ |
17 | 16 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ 2 โ
โ) |
18 | 17, 11 | nnexpcld 14208 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ
(2โ๐) โ
โ) |
19 | 18 | nnzd 12585 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ
(2โ๐) โ
โค) |
20 | | zleltp1 12613 |
. . . . . . . . . . . . . . . . . 18
โข ((1
โ โค โง (2โ๐) โ โค) โ (1 โค
(2โ๐) โ 1 <
((2โ๐) +
1))) |
21 | 15, 19, 20 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ (1 โค
(2โ๐) โ 1 <
((2โ๐) +
1))) |
22 | 14, 21 | mpbid 231 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ 1 <
((2โ๐) +
1)) |
23 | 18 | nncnd 12228 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ
(2โ๐) โ
โ) |
24 | | 1cnd 11209 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ 1 โ
โ) |
25 | | subneg 11509 |
. . . . . . . . . . . . . . . . . 18
โข
(((2โ๐) โ
โ โง 1 โ โ) โ ((2โ๐) โ -1) = ((2โ๐) + 1)) |
26 | 25 | breq2d 5161 |
. . . . . . . . . . . . . . . . 17
โข
(((2โ๐) โ
โ โง 1 โ โ) โ (1 < ((2โ๐) โ -1) โ 1 < ((2โ๐) + 1))) |
27 | 23, 24, 26 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (1 <
((2โ๐) โ -1)
โ 1 < ((2โ๐) +
1))) |
28 | 22, 27 | mpbird 257 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ 1 <
((2โ๐) โ
-1)) |
29 | 28 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ 1 < ((2โ๐)
โ -1)) |
30 | 29 | ad2antlr 726 |
. . . . . . . . . . . . 13
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ 1 < ((2โ๐) โ -1)) |
31 | 18 | nnred 12227 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ
(2โ๐) โ
โ) |
32 | 31 | adantl 483 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (2โ๐) โ
โ) |
33 | 16 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ 2 โ โ) |
34 | 11 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ๐ โ
โ0) |
35 | 5 | nnnn0d 12532 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (โ โ {2})
โ ๐ โ
โ0) |
36 | 35 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ๐ โ
โ0) |
37 | 34, 36 | nn0mulcld 12537 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (๐ ยท ๐) โ
โ0) |
38 | 33, 37 | nnexpcld 14208 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (2โ(๐ ยท
๐)) โ
โ) |
39 | 38 | nnred 12227 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (2โ(๐ ยท
๐)) โ
โ) |
40 | | 1red 11215 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ 1 โ โ) |
41 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ 2 โ โ) |
42 | | nnz 12579 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ ๐ โ
โค) |
43 | 42 | adantl 483 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ๐ โ
โค) |
44 | 5 | nnzd 12585 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (โ โ {2})
โ ๐ โ
โค) |
45 | 44 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ๐ โ
โค) |
46 | 43, 45 | zmulcld 12672 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (๐ ยท ๐) โ
โค) |
47 | | 1lt2 12383 |
. . . . . . . . . . . . . . . . . 18
โข 1 <
2 |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ 1 < 2) |
49 | | prmgt1 16634 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ 1 <
๐) |
50 | 3, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (โ โ {2})
โ 1 < ๐) |
51 | 50 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ 1 < ๐) |
52 | | nnre 12219 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ ๐ โ
โ) |
53 | 52 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ๐ โ
โ) |
54 | 5 | nnred 12227 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (โ โ {2})
โ ๐ โ
โ) |
55 | 54 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ๐ โ
โ) |
56 | | nngt0 12243 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ 0 <
๐) |
57 | 56 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ 0 < ๐) |
58 | | ltmulgt11 12074 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง ๐ โ โ โง 0 <
๐) โ (1 < ๐ โ ๐ < (๐ ยท ๐))) |
59 | 53, 55, 57, 58 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (1 < ๐ โ
๐ < (๐ ยท ๐))) |
60 | 51, 59 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ๐ < (๐ ยท ๐)) |
61 | | ltexp2a 14131 |
. . . . . . . . . . . . . . . . 17
โข (((2
โ โ โง ๐
โ โค โง (๐
ยท ๐) โ โค)
โง (1 < 2 โง ๐
< (๐ ยท ๐))) โ (2โ๐) < (2โ(๐ ยท ๐))) |
62 | 41, 43, 46, 48, 60, 61 | syl32anc 1379 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (2โ๐) <
(2โ(๐ ยท ๐))) |
63 | 32, 39, 40, 62 | ltadd1dd 11825 |
. . . . . . . . . . . . . . 15
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ((2โ๐) + 1)
< ((2โ(๐ ยท
๐)) + 1)) |
64 | 63 | ad2antlr 726 |
. . . . . . . . . . . . . 14
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ ((2โ๐) + 1) < ((2โ(๐ ยท ๐)) + 1)) |
65 | 23, 24 | subnegd 11578 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ
((2โ๐) โ -1) =
((2โ๐) +
1)) |
66 | 65 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ
((2โ๐) + 1) =
((2โ๐) โ
-1)) |
67 | 66 | adantl 483 |
. . . . . . . . . . . . . . 15
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ((2โ๐) + 1) =
((2โ๐) โ
-1)) |
68 | 67 | ad2antlr 726 |
. . . . . . . . . . . . . 14
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ ((2โ๐) + 1) = ((2โ๐) โ -1)) |
69 | | oveq2 7417 |
. . . . . . . . . . . . . . . 16
โข ((๐ ยท ๐) = ๐พ โ (2โ(๐ ยท ๐)) = (2โ๐พ)) |
70 | 69 | oveq1d 7424 |
. . . . . . . . . . . . . . 15
โข ((๐ ยท ๐) = ๐พ โ ((2โ(๐ ยท ๐)) + 1) = ((2โ๐พ) + 1)) |
71 | 70 | adantl 483 |
. . . . . . . . . . . . . 14
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ ((2โ(๐ ยท ๐)) + 1) = ((2โ๐พ) + 1)) |
72 | 64, 68, 71 | 3brtr3d 5180 |
. . . . . . . . . . . . 13
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ ((2โ๐) โ -1) < ((2โ๐พ) + 1)) |
73 | | neg1z 12598 |
. . . . . . . . . . . . . . . . . . . 20
โข -1 โ
โค |
74 | 73 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ -1 โ
โค) |
75 | 19, 74 | zsubcld 12671 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ
((2โ๐) โ -1)
โ โค) |
76 | 75 | adantl 483 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ((2โ๐) โ
-1) โ โค) |
77 | | fzofi 13939 |
. . . . . . . . . . . . . . . . . . 19
โข
(0..^๐) โ
Fin |
78 | 77 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (0..^๐) โ
Fin) |
79 | 19 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (2โ๐) โ
โค) |
80 | | elfzonn0 13677 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (0..^๐) โ ๐ โ โ0) |
81 | | zexpcl 14042 |
. . . . . . . . . . . . . . . . . . . 20
โข
(((2โ๐) โ
โค โง ๐ โ
โ0) โ ((2โ๐)โ๐) โ โค) |
82 | 79, 80, 81 | syl2an 597 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ (โ โ {2})
โง ๐ โ โ)
โง ๐ โ (0..^๐)) โ ((2โ๐)โ๐) โ โค) |
83 | 73 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ (โ โ {2})
โง ๐ โ โ)
โง ๐ โ (0..^๐)) โ -1 โ
โค) |
84 | | fzonnsub 13657 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (0..^๐) โ (๐ โ ๐) โ โ) |
85 | 84 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โ (โ โ {2})
โง ๐ โ โ)
โง ๐ โ (0..^๐)) โ (๐ โ ๐) โ โ) |
86 | | nnm1nn0 12513 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ ๐) โ โ โ ((๐ โ ๐) โ 1) โ
โ0) |
87 | 85, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ (โ โ {2})
โง ๐ โ โ)
โง ๐ โ (0..^๐)) โ ((๐ โ ๐) โ 1) โ
โ0) |
88 | | zexpcl 14042 |
. . . . . . . . . . . . . . . . . . . 20
โข ((-1
โ โค โง ((๐
โ ๐) โ 1)
โ โ0) โ (-1โ((๐ โ ๐) โ 1)) โ
โค) |
89 | 83, 87, 88 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ (โ โ {2})
โง ๐ โ โ)
โง ๐ โ (0..^๐)) โ (-1โ((๐ โ ๐) โ 1)) โ
โค) |
90 | 82, 89 | zmulcld 12672 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ (โ โ {2})
โง ๐ โ โ)
โง ๐ โ (0..^๐)) โ (((2โ๐)โ๐) ยท (-1โ((๐ โ ๐) โ 1))) โ
โค) |
91 | 78, 90 | fsumzcl 15681 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ฮฃ๐ โ
(0..^๐)(((2โ๐)โ๐) ยท (-1โ((๐ โ ๐) โ 1))) โ
โค) |
92 | | dvdsmul1 16221 |
. . . . . . . . . . . . . . . . 17
โข
((((2โ๐)
โ -1) โ โค โง ฮฃ๐ โ (0..^๐)(((2โ๐)โ๐) ยท (-1โ((๐ โ ๐) โ 1))) โ โค) โ
((2โ๐) โ -1)
โฅ (((2โ๐)
โ -1) ยท ฮฃ๐ โ (0..^๐)(((2โ๐)โ๐) ยท (-1โ((๐ โ ๐) โ 1))))) |
93 | 76, 91, 92 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ((2โ๐) โ
-1) โฅ (((2โ๐)
โ -1) ยท ฮฃ๐ โ (0..^๐)(((2โ๐)โ๐) ยท (-1โ((๐ โ ๐) โ 1))))) |
94 | 93 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ ((2โ๐) โ -1) โฅ (((2โ๐) โ -1) ยท
ฮฃ๐ โ (0..^๐)(((2โ๐)โ๐) ยท (-1โ((๐ โ ๐) โ 1))))) |
95 | 23 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (2โ๐) โ
โ) |
96 | | neg1cn 12326 |
. . . . . . . . . . . . . . . . . . 19
โข -1 โ
โ |
97 | 96 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ -1 โ โ) |
98 | | pwdif 15814 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ0
โง (2โ๐) โ
โ โง -1 โ โ) โ (((2โ๐)โ๐) โ (-1โ๐)) = (((2โ๐) โ -1) ยท ฮฃ๐ โ (0..^๐)(((2โ๐)โ๐) ยท (-1โ((๐ โ ๐) โ 1))))) |
99 | 36, 95, 97, 98 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (((2โ๐)โ๐) โ (-1โ๐)) = (((2โ๐) โ -1) ยท ฮฃ๐ โ (0..^๐)(((2โ๐)โ๐) ยท (-1โ((๐ โ ๐) โ 1))))) |
100 | 99 | breq2d 5161 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (((2โ๐) โ
-1) โฅ (((2โ๐)โ๐) โ (-1โ๐)) โ ((2โ๐) โ -1) โฅ (((2โ๐) โ -1) ยท
ฮฃ๐ โ (0..^๐)(((2โ๐)โ๐) ยท (-1โ((๐ โ ๐) โ 1)))))) |
101 | 100 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ (((2โ๐) โ -1) โฅ (((2โ๐)โ๐) โ (-1โ๐)) โ ((2โ๐) โ -1) โฅ (((2โ๐) โ -1) ยท
ฮฃ๐ โ (0..^๐)(((2โ๐)โ๐) ยท (-1โ((๐ โ ๐) โ 1)))))) |
102 | 94, 101 | mpbird 257 |
. . . . . . . . . . . . . 14
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ ((2โ๐) โ -1) โฅ (((2โ๐)โ๐) โ (-1โ๐))) |
103 | | 2cnd 12290 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐พ โ โ โ 2 โ
โ) |
104 | | nnnn0 12479 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐พ โ โ โ ๐พ โ
โ0) |
105 | 103, 104 | expcld 14111 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐พ โ โ โ
(2โ๐พ) โ
โ) |
106 | | 1cnd 11209 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐พ โ โ โ 1 โ
โ) |
107 | 105, 106 | subnegd 11578 |
. . . . . . . . . . . . . . . . . . 19
โข (๐พ โ โ โ
((2โ๐พ) โ -1) =
((2โ๐พ) +
1)) |
108 | 107 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . 18
โข (๐พ โ โ โ
((2โ๐พ) + 1) =
((2โ๐พ) โ
-1)) |
109 | 108 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โ ((2โ๐พ) + 1) =
((2โ๐พ) โ
-1)) |
110 | 109 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ ((2โ๐พ) + 1) = ((2โ๐พ) โ -1)) |
111 | | oveq2 7417 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐พ = (๐ ยท ๐) โ (2โ๐พ) = (2โ(๐ ยท ๐))) |
112 | 111 | eqcoms 2741 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ ยท ๐) = ๐พ โ (2โ๐พ) = (2โ(๐ ยท ๐))) |
113 | 112 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ (2โ๐พ) = (2โ(๐ ยท ๐))) |
114 | | 2cnd 12290 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ 2 โ โ) |
115 | 114, 36, 34 | expmuld 14114 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (2โ(๐ ยท
๐)) = ((2โ๐)โ๐)) |
116 | 115 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . 18
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ (2โ(๐ ยท ๐)) = ((2โ๐)โ๐)) |
117 | 113, 116 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ (2โ๐พ) = ((2โ๐)โ๐)) |
118 | | 1exp 14057 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โค โ
(1โ๐) =
1) |
119 | 44, 118 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (โ โ {2})
โ (1โ๐) =
1) |
120 | 119 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (โ โ {2})
โ 1 = (1โ๐)) |
121 | 120 | negeqd 11454 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (โ โ {2})
โ -1 = -(1โ๐)) |
122 | | 1cnd 11209 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (โ โ {2})
โ 1 โ โ) |
123 | | oddn2prm 16745 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (โ โ {2})
โ ยฌ 2 โฅ ๐) |
124 | | oexpneg 16288 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((1
โ โ โง ๐
โ โ โง ยฌ 2 โฅ ๐) โ (-1โ๐) = -(1โ๐)) |
125 | 122, 5, 123, 124 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (โ โ {2})
โ (-1โ๐) =
-(1โ๐)) |
126 | 125 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (โ โ {2})
โ -(1โ๐) =
(-1โ๐)) |
127 | 121, 126 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (โ โ {2})
โ -1 = (-1โ๐)) |
128 | 127 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ -1 = (-1โ๐)) |
129 | 128 | ad2antlr 726 |
. . . . . . . . . . . . . . . . 17
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ -1 = (-1โ๐)) |
130 | 117, 129 | oveq12d 7427 |
. . . . . . . . . . . . . . . 16
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ ((2โ๐พ) โ -1) = (((2โ๐)โ๐) โ (-1โ๐))) |
131 | 110, 130 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ ((2โ๐พ) + 1) = (((2โ๐)โ๐) โ (-1โ๐))) |
132 | 131 | breq2d 5161 |
. . . . . . . . . . . . . 14
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ (((2โ๐) โ -1) โฅ ((2โ๐พ) + 1) โ ((2โ๐) โ -1) โฅ
(((2โ๐)โ๐) โ (-1โ๐)))) |
133 | 102, 132 | mpbird 257 |
. . . . . . . . . . . . 13
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ ((2โ๐) โ -1) โฅ ((2โ๐พ) + 1)) |
134 | 30, 72, 133 | dvdsnprmd 16627 |
. . . . . . . . . . . 12
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ ยฌ ((2โ๐พ) + 1) โ โ) |
135 | 134 | pm2.21d 121 |
. . . . . . . . . . 11
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ (((2โ๐พ) + 1) โ โ โ โ๐ โ โ0
๐พ = (2โ๐))) |
136 | 135 | ex 414 |
. . . . . . . . . 10
โข ((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โ ((๐ ยท ๐) = ๐พ โ (((2โ๐พ) + 1) โ โ โ โ๐ โ โ0
๐พ = (2โ๐)))) |
137 | 136 | com23 86 |
. . . . . . . . 9
โข ((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โ (((2โ๐พ) + 1)
โ โ โ ((๐
ยท ๐) = ๐พ โ โ๐ โ โ0
๐พ = (2โ๐)))) |
138 | 137 | impancom 453 |
. . . . . . . 8
โข ((๐พ โ โ โง
((2โ๐พ) + 1) โ
โ) โ ((๐ โ
(โ โ {2}) โง ๐ โ โ) โ ((๐ ยท ๐) = ๐พ โ โ๐ โ โ0 ๐พ = (2โ๐)))) |
139 | 138 | impl 457 |
. . . . . . 7
โข ((((๐พ โ โ โง
((2โ๐พ) + 1) โ
โ) โง ๐ โ
(โ โ {2})) โง ๐ โ โ) โ ((๐ ยท ๐) = ๐พ โ โ๐ โ โ0 ๐พ = (2โ๐))) |
140 | 139 | rexlimdva 3156 |
. . . . . 6
โข (((๐พ โ โ โง
((2โ๐พ) + 1) โ
โ) โง ๐ โ
(โ โ {2})) โ (โ๐ โ โ (๐ ยท ๐) = ๐พ โ โ๐ โ โ0 ๐พ = (2โ๐))) |
141 | 8, 140 | sylbid 239 |
. . . . 5
โข (((๐พ โ โ โง
((2โ๐พ) + 1) โ
โ) โง ๐ โ
(โ โ {2})) โ (๐ โฅ ๐พ โ โ๐ โ โ0 ๐พ = (2โ๐))) |
142 | 141 | rexlimdva 3156 |
. . . 4
โข ((๐พ โ โ โง
((2โ๐พ) + 1) โ
โ) โ (โ๐
โ (โ โ {2})๐ โฅ ๐พ โ โ๐ โ โ0 ๐พ = (2โ๐))) |
143 | 142 | adantr 482 |
. . 3
โข (((๐พ โ โ โง
((2โ๐พ) + 1) โ
โ) โง ยฌ โ๐ โ โ0 ๐พ = (2โ๐)) โ (โ๐ โ (โ โ {2})๐ โฅ ๐พ โ โ๐ โ โ0 ๐พ = (2โ๐))) |
144 | 2, 143 | mpd 15 |
. 2
โข (((๐พ โ โ โง
((2โ๐พ) + 1) โ
โ) โง ยฌ โ๐ โ โ0 ๐พ = (2โ๐)) โ โ๐ โ โ0 ๐พ = (2โ๐)) |
145 | 144 | pm2.18da 799 |
1
โข ((๐พ โ โ โง
((2โ๐พ) + 1) โ
โ) โ โ๐
โ โ0 ๐พ = (2โ๐)) |