Step | Hyp | Ref
| Expression |
1 | | oddprmdvds 16832 |
. . . 4
โข ((๐พ โ โ โง ยฌ
โ๐ โ
โ0 ๐พ =
(2โ๐)) โ
โ๐ โ (โ
โ {2})๐ โฅ ๐พ) |
2 | 1 | adantlr 713 |
. . 3
โข (((๐พ โ โ โง
((2โ๐พ) + 1) โ
โ) โง ยฌ โ๐ โ โ0 ๐พ = (2โ๐)) โ โ๐ โ (โ โ {2})๐ โฅ ๐พ) |
3 | | eldifi 4125 |
. . . . . . . 8
โข (๐ โ (โ โ {2})
โ ๐ โ
โ) |
4 | | prmnn 16607 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ) |
5 | 3, 4 | syl 17 |
. . . . . . 7
โข (๐ โ (โ โ {2})
โ ๐ โ
โ) |
6 | | simpl 483 |
. . . . . . 7
โข ((๐พ โ โ โง
((2โ๐พ) + 1) โ
โ) โ ๐พ โ
โ) |
7 | | nndivides 16203 |
. . . . . . 7
โข ((๐ โ โ โง ๐พ โ โ) โ (๐ โฅ ๐พ โ โ๐ โ โ (๐ ยท ๐) = ๐พ)) |
8 | 5, 6, 7 | syl2anr 597 |
. . . . . 6
โข (((๐พ โ โ โง
((2โ๐พ) + 1) โ
โ) โง ๐ โ
(โ โ {2})) โ (๐ โฅ ๐พ โ โ๐ โ โ (๐ ยท ๐) = ๐พ)) |
9 | | 2re 12282 |
. . . . . . . . . . . . . . . . . . 19
โข 2 โ
โ |
10 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ 2 โ
โ) |
11 | | nnnn0 12475 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ ๐ โ
โ0) |
12 | | 1le2 12417 |
. . . . . . . . . . . . . . . . . . 19
โข 1 โค
2 |
13 | 12 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ 1 โค
2) |
14 | 10, 11, 13 | expge1d 14126 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ 1 โค
(2โ๐)) |
15 | | 1zzd 12589 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ 1 โ
โค) |
16 | | 2nn 12281 |
. . . . . . . . . . . . . . . . . . . . 21
โข 2 โ
โ |
17 | 16 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ 2 โ
โ) |
18 | 17, 11 | nnexpcld 14204 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ
(2โ๐) โ
โ) |
19 | 18 | nnzd 12581 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ
(2โ๐) โ
โค) |
20 | | zleltp1 12609 |
. . . . . . . . . . . . . . . . . 18
โข ((1
โ โค โง (2โ๐) โ โค) โ (1 โค
(2โ๐) โ 1 <
((2โ๐) +
1))) |
21 | 15, 19, 20 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ (1 โค
(2โ๐) โ 1 <
((2โ๐) +
1))) |
22 | 14, 21 | mpbid 231 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ 1 <
((2โ๐) +
1)) |
23 | 18 | nncnd 12224 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ
(2โ๐) โ
โ) |
24 | | 1cnd 11205 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ 1 โ
โ) |
25 | | subneg 11505 |
. . . . . . . . . . . . . . . . . 18
โข
(((2โ๐) โ
โ โง 1 โ โ) โ ((2โ๐) โ -1) = ((2โ๐) + 1)) |
26 | 25 | breq2d 5159 |
. . . . . . . . . . . . . . . . 17
โข
(((2โ๐) โ
โ โง 1 โ โ) โ (1 < ((2โ๐) โ -1) โ 1 < ((2โ๐) + 1))) |
27 | 23, 24, 26 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (1 <
((2โ๐) โ -1)
โ 1 < ((2โ๐) +
1))) |
28 | 22, 27 | mpbird 256 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ 1 <
((2โ๐) โ
-1)) |
29 | 28 | adantl 482 |
. . . . . . . . . . . . . 14
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ 1 < ((2โ๐)
โ -1)) |
30 | 29 | ad2antlr 725 |
. . . . . . . . . . . . 13
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ 1 < ((2โ๐) โ -1)) |
31 | 18 | nnred 12223 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ
(2โ๐) โ
โ) |
32 | 31 | adantl 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (2โ๐) โ
โ) |
33 | 16 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ 2 โ โ) |
34 | 11 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ๐ โ
โ0) |
35 | 5 | nnnn0d 12528 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (โ โ {2})
โ ๐ โ
โ0) |
36 | 35 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ๐ โ
โ0) |
37 | 34, 36 | nn0mulcld 12533 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (๐ ยท ๐) โ
โ0) |
38 | 33, 37 | nnexpcld 14204 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (2โ(๐ ยท
๐)) โ
โ) |
39 | 38 | nnred 12223 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (2โ(๐ ยท
๐)) โ
โ) |
40 | | 1red 11211 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ 1 โ โ) |
41 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ 2 โ โ) |
42 | | nnz 12575 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ ๐ โ
โค) |
43 | 42 | adantl 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ๐ โ
โค) |
44 | 5 | nnzd 12581 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (โ โ {2})
โ ๐ โ
โค) |
45 | 44 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ๐ โ
โค) |
46 | 43, 45 | zmulcld 12668 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (๐ ยท ๐) โ
โค) |
47 | | 1lt2 12379 |
. . . . . . . . . . . . . . . . . 18
โข 1 <
2 |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ 1 < 2) |
49 | | prmgt1 16630 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ 1 <
๐) |
50 | 3, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (โ โ {2})
โ 1 < ๐) |
51 | 50 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ 1 < ๐) |
52 | | nnre 12215 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ ๐ โ
โ) |
53 | 52 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ๐ โ
โ) |
54 | 5 | nnred 12223 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (โ โ {2})
โ ๐ โ
โ) |
55 | 54 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ๐ โ
โ) |
56 | | nngt0 12239 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ 0 <
๐) |
57 | 56 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ 0 < ๐) |
58 | | ltmulgt11 12070 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง ๐ โ โ โง 0 <
๐) โ (1 < ๐ โ ๐ < (๐ ยท ๐))) |
59 | 53, 55, 57, 58 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (1 < ๐ โ
๐ < (๐ ยท ๐))) |
60 | 51, 59 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ๐ < (๐ ยท ๐)) |
61 | | ltexp2a 14127 |
. . . . . . . . . . . . . . . . 17
โข (((2
โ โ โง ๐
โ โค โง (๐
ยท ๐) โ โค)
โง (1 < 2 โง ๐
< (๐ ยท ๐))) โ (2โ๐) < (2โ(๐ ยท ๐))) |
62 | 41, 43, 46, 48, 60, 61 | syl32anc 1378 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (2โ๐) <
(2โ(๐ ยท ๐))) |
63 | 32, 39, 40, 62 | ltadd1dd 11821 |
. . . . . . . . . . . . . . 15
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ((2โ๐) + 1)
< ((2โ(๐ ยท
๐)) + 1)) |
64 | 63 | ad2antlr 725 |
. . . . . . . . . . . . . 14
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ ((2โ๐) + 1) < ((2โ(๐ ยท ๐)) + 1)) |
65 | 23, 24 | subnegd 11574 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ
((2โ๐) โ -1) =
((2โ๐) +
1)) |
66 | 65 | eqcomd 2738 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ
((2โ๐) + 1) =
((2โ๐) โ
-1)) |
67 | 66 | adantl 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ((2โ๐) + 1) =
((2โ๐) โ
-1)) |
68 | 67 | ad2antlr 725 |
. . . . . . . . . . . . . 14
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ ((2โ๐) + 1) = ((2โ๐) โ -1)) |
69 | | oveq2 7413 |
. . . . . . . . . . . . . . . 16
โข ((๐ ยท ๐) = ๐พ โ (2โ(๐ ยท ๐)) = (2โ๐พ)) |
70 | 69 | oveq1d 7420 |
. . . . . . . . . . . . . . 15
โข ((๐ ยท ๐) = ๐พ โ ((2โ(๐ ยท ๐)) + 1) = ((2โ๐พ) + 1)) |
71 | 70 | adantl 482 |
. . . . . . . . . . . . . 14
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ ((2โ(๐ ยท ๐)) + 1) = ((2โ๐พ) + 1)) |
72 | 64, 68, 71 | 3brtr3d 5178 |
. . . . . . . . . . . . 13
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ ((2โ๐) โ -1) < ((2โ๐พ) + 1)) |
73 | | neg1z 12594 |
. . . . . . . . . . . . . . . . . . . 20
โข -1 โ
โค |
74 | 73 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ -1 โ
โค) |
75 | 19, 74 | zsubcld 12667 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ
((2โ๐) โ -1)
โ โค) |
76 | 75 | adantl 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ((2โ๐) โ
-1) โ โค) |
77 | | fzofi 13935 |
. . . . . . . . . . . . . . . . . . 19
โข
(0..^๐) โ
Fin |
78 | 77 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (0..^๐) โ
Fin) |
79 | 19 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (2โ๐) โ
โค) |
80 | | elfzonn0 13673 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (0..^๐) โ ๐ โ โ0) |
81 | | zexpcl 14038 |
. . . . . . . . . . . . . . . . . . . 20
โข
(((2โ๐) โ
โค โง ๐ โ
โ0) โ ((2โ๐)โ๐) โ โค) |
82 | 79, 80, 81 | syl2an 596 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ (โ โ {2})
โง ๐ โ โ)
โง ๐ โ (0..^๐)) โ ((2โ๐)โ๐) โ โค) |
83 | 73 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ (โ โ {2})
โง ๐ โ โ)
โง ๐ โ (0..^๐)) โ -1 โ
โค) |
84 | | fzonnsub 13653 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (0..^๐) โ (๐ โ ๐) โ โ) |
85 | 84 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โ (โ โ {2})
โง ๐ โ โ)
โง ๐ โ (0..^๐)) โ (๐ โ ๐) โ โ) |
86 | | nnm1nn0 12509 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ ๐) โ โ โ ((๐ โ ๐) โ 1) โ
โ0) |
87 | 85, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ (โ โ {2})
โง ๐ โ โ)
โง ๐ โ (0..^๐)) โ ((๐ โ ๐) โ 1) โ
โ0) |
88 | | zexpcl 14038 |
. . . . . . . . . . . . . . . . . . . 20
โข ((-1
โ โค โง ((๐
โ ๐) โ 1)
โ โ0) โ (-1โ((๐ โ ๐) โ 1)) โ
โค) |
89 | 83, 87, 88 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ (โ โ {2})
โง ๐ โ โ)
โง ๐ โ (0..^๐)) โ (-1โ((๐ โ ๐) โ 1)) โ
โค) |
90 | 82, 89 | zmulcld 12668 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ (โ โ {2})
โง ๐ โ โ)
โง ๐ โ (0..^๐)) โ (((2โ๐)โ๐) ยท (-1โ((๐ โ ๐) โ 1))) โ
โค) |
91 | 78, 90 | fsumzcl 15677 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ฮฃ๐ โ
(0..^๐)(((2โ๐)โ๐) ยท (-1โ((๐ โ ๐) โ 1))) โ
โค) |
92 | | dvdsmul1 16217 |
. . . . . . . . . . . . . . . . 17
โข
((((2โ๐)
โ -1) โ โค โง ฮฃ๐ โ (0..^๐)(((2โ๐)โ๐) ยท (-1โ((๐ โ ๐) โ 1))) โ โค) โ
((2โ๐) โ -1)
โฅ (((2โ๐)
โ -1) ยท ฮฃ๐ โ (0..^๐)(((2โ๐)โ๐) ยท (-1โ((๐ โ ๐) โ 1))))) |
93 | 76, 91, 92 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ ((2โ๐) โ
-1) โฅ (((2โ๐)
โ -1) ยท ฮฃ๐ โ (0..^๐)(((2โ๐)โ๐) ยท (-1โ((๐ โ ๐) โ 1))))) |
94 | 93 | ad2antlr 725 |
. . . . . . . . . . . . . . 15
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ ((2โ๐) โ -1) โฅ (((2โ๐) โ -1) ยท
ฮฃ๐ โ (0..^๐)(((2โ๐)โ๐) ยท (-1โ((๐ โ ๐) โ 1))))) |
95 | 23 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (2โ๐) โ
โ) |
96 | | neg1cn 12322 |
. . . . . . . . . . . . . . . . . . 19
โข -1 โ
โ |
97 | 96 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ -1 โ โ) |
98 | | pwdif 15810 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ0
โง (2โ๐) โ
โ โง -1 โ โ) โ (((2โ๐)โ๐) โ (-1โ๐)) = (((2โ๐) โ -1) ยท ฮฃ๐ โ (0..^๐)(((2โ๐)โ๐) ยท (-1โ((๐ โ ๐) โ 1))))) |
99 | 36, 95, 97, 98 | syl3anc 1371 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (((2โ๐)โ๐) โ (-1โ๐)) = (((2โ๐) โ -1) ยท ฮฃ๐ โ (0..^๐)(((2โ๐)โ๐) ยท (-1โ((๐ โ ๐) โ 1))))) |
100 | 99 | breq2d 5159 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (((2โ๐) โ
-1) โฅ (((2โ๐)โ๐) โ (-1โ๐)) โ ((2โ๐) โ -1) โฅ (((2โ๐) โ -1) ยท
ฮฃ๐ โ (0..^๐)(((2โ๐)โ๐) ยท (-1โ((๐ โ ๐) โ 1)))))) |
101 | 100 | ad2antlr 725 |
. . . . . . . . . . . . . . 15
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ (((2โ๐) โ -1) โฅ (((2โ๐)โ๐) โ (-1โ๐)) โ ((2โ๐) โ -1) โฅ (((2โ๐) โ -1) ยท
ฮฃ๐ โ (0..^๐)(((2โ๐)โ๐) ยท (-1โ((๐ โ ๐) โ 1)))))) |
102 | 94, 101 | mpbird 256 |
. . . . . . . . . . . . . 14
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ ((2โ๐) โ -1) โฅ (((2โ๐)โ๐) โ (-1โ๐))) |
103 | | 2cnd 12286 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐พ โ โ โ 2 โ
โ) |
104 | | nnnn0 12475 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐พ โ โ โ ๐พ โ
โ0) |
105 | 103, 104 | expcld 14107 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐พ โ โ โ
(2โ๐พ) โ
โ) |
106 | | 1cnd 11205 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐พ โ โ โ 1 โ
โ) |
107 | 105, 106 | subnegd 11574 |
. . . . . . . . . . . . . . . . . . 19
โข (๐พ โ โ โ
((2โ๐พ) โ -1) =
((2โ๐พ) +
1)) |
108 | 107 | eqcomd 2738 |
. . . . . . . . . . . . . . . . . 18
โข (๐พ โ โ โ
((2โ๐พ) + 1) =
((2โ๐พ) โ
-1)) |
109 | 108 | adantr 481 |
. . . . . . . . . . . . . . . . 17
โข ((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โ ((2โ๐พ) + 1) =
((2โ๐พ) โ
-1)) |
110 | 109 | adantr 481 |
. . . . . . . . . . . . . . . 16
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ ((2โ๐พ) + 1) = ((2โ๐พ) โ -1)) |
111 | | oveq2 7413 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐พ = (๐ ยท ๐) โ (2โ๐พ) = (2โ(๐ ยท ๐))) |
112 | 111 | eqcoms 2740 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ ยท ๐) = ๐พ โ (2โ๐พ) = (2โ(๐ ยท ๐))) |
113 | 112 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ (2โ๐พ) = (2โ(๐ ยท ๐))) |
114 | | 2cnd 12286 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ 2 โ โ) |
115 | 114, 36, 34 | expmuld 14110 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ (2โ(๐ ยท
๐)) = ((2โ๐)โ๐)) |
116 | 115 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . 18
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ (2โ(๐ ยท ๐)) = ((2โ๐)โ๐)) |
117 | 113, 116 | eqtrd 2772 |
. . . . . . . . . . . . . . . . 17
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ (2โ๐พ) = ((2โ๐)โ๐)) |
118 | | 1exp 14053 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โค โ
(1โ๐) =
1) |
119 | 44, 118 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (โ โ {2})
โ (1โ๐) =
1) |
120 | 119 | eqcomd 2738 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (โ โ {2})
โ 1 = (1โ๐)) |
121 | 120 | negeqd 11450 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (โ โ {2})
โ -1 = -(1โ๐)) |
122 | | 1cnd 11205 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (โ โ {2})
โ 1 โ โ) |
123 | | oddn2prm 16741 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (โ โ {2})
โ ยฌ 2 โฅ ๐) |
124 | | oexpneg 16284 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((1
โ โ โง ๐
โ โ โง ยฌ 2 โฅ ๐) โ (-1โ๐) = -(1โ๐)) |
125 | 122, 5, 123, 124 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (โ โ {2})
โ (-1โ๐) =
-(1โ๐)) |
126 | 125 | eqcomd 2738 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (โ โ {2})
โ -(1โ๐) =
(-1โ๐)) |
127 | 121, 126 | eqtrd 2772 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (โ โ {2})
โ -1 = (-1โ๐)) |
128 | 127 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (โ โ {2})
โง ๐ โ โ)
โ -1 = (-1โ๐)) |
129 | 128 | ad2antlr 725 |
. . . . . . . . . . . . . . . . 17
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ -1 = (-1โ๐)) |
130 | 117, 129 | oveq12d 7423 |
. . . . . . . . . . . . . . . 16
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ ((2โ๐พ) โ -1) = (((2โ๐)โ๐) โ (-1โ๐))) |
131 | 110, 130 | eqtrd 2772 |
. . . . . . . . . . . . . . 15
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ ((2โ๐พ) + 1) = (((2โ๐)โ๐) โ (-1โ๐))) |
132 | 131 | breq2d 5159 |
. . . . . . . . . . . . . 14
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ (((2โ๐) โ -1) โฅ ((2โ๐พ) + 1) โ ((2โ๐) โ -1) โฅ
(((2โ๐)โ๐) โ (-1โ๐)))) |
133 | 102, 132 | mpbird 256 |
. . . . . . . . . . . . 13
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ ((2โ๐) โ -1) โฅ ((2โ๐พ) + 1)) |
134 | 30, 72, 133 | dvdsnprmd 16623 |
. . . . . . . . . . . 12
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ ยฌ ((2โ๐พ) + 1) โ โ) |
135 | 134 | pm2.21d 121 |
. . . . . . . . . . 11
โข (((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โง (๐ ยท ๐) = ๐พ) โ (((2โ๐พ) + 1) โ โ โ โ๐ โ โ0
๐พ = (2โ๐))) |
136 | 135 | ex 413 |
. . . . . . . . . 10
โข ((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โ ((๐ ยท ๐) = ๐พ โ (((2โ๐พ) + 1) โ โ โ โ๐ โ โ0
๐พ = (2โ๐)))) |
137 | 136 | com23 86 |
. . . . . . . . 9
โข ((๐พ โ โ โง (๐ โ (โ โ {2})
โง ๐ โ โ))
โ (((2โ๐พ) + 1)
โ โ โ ((๐
ยท ๐) = ๐พ โ โ๐ โ โ0
๐พ = (2โ๐)))) |
138 | 137 | impancom 452 |
. . . . . . . 8
โข ((๐พ โ โ โง
((2โ๐พ) + 1) โ
โ) โ ((๐ โ
(โ โ {2}) โง ๐ โ โ) โ ((๐ ยท ๐) = ๐พ โ โ๐ โ โ0 ๐พ = (2โ๐)))) |
139 | 138 | impl 456 |
. . . . . . 7
โข ((((๐พ โ โ โง
((2โ๐พ) + 1) โ
โ) โง ๐ โ
(โ โ {2})) โง ๐ โ โ) โ ((๐ ยท ๐) = ๐พ โ โ๐ โ โ0 ๐พ = (2โ๐))) |
140 | 139 | rexlimdva 3155 |
. . . . . 6
โข (((๐พ โ โ โง
((2โ๐พ) + 1) โ
โ) โง ๐ โ
(โ โ {2})) โ (โ๐ โ โ (๐ ยท ๐) = ๐พ โ โ๐ โ โ0 ๐พ = (2โ๐))) |
141 | 8, 140 | sylbid 239 |
. . . . 5
โข (((๐พ โ โ โง
((2โ๐พ) + 1) โ
โ) โง ๐ โ
(โ โ {2})) โ (๐ โฅ ๐พ โ โ๐ โ โ0 ๐พ = (2โ๐))) |
142 | 141 | rexlimdva 3155 |
. . . 4
โข ((๐พ โ โ โง
((2โ๐พ) + 1) โ
โ) โ (โ๐
โ (โ โ {2})๐ โฅ ๐พ โ โ๐ โ โ0 ๐พ = (2โ๐))) |
143 | 142 | adantr 481 |
. . 3
โข (((๐พ โ โ โง
((2โ๐พ) + 1) โ
โ) โง ยฌ โ๐ โ โ0 ๐พ = (2โ๐)) โ (โ๐ โ (โ โ {2})๐ โฅ ๐พ โ โ๐ โ โ0 ๐พ = (2โ๐))) |
144 | 2, 143 | mpd 15 |
. 2
โข (((๐พ โ โ โง
((2โ๐พ) + 1) โ
โ) โง ยฌ โ๐ โ โ0 ๐พ = (2โ๐)) โ โ๐ โ โ0 ๐พ = (2โ๐)) |
145 | 144 | pm2.18da 798 |
1
โข ((๐พ โ โ โง
((2โ๐พ) + 1) โ
โ) โ โ๐
โ โ0 ๐พ = (2โ๐)) |