Step | Hyp | Ref
| Expression |
1 | | oddz 45976 |
. . . . . 6
โข (๐ โ Odd โ ๐ โ
โค) |
2 | | odd2np1ALTV 46019 |
. . . . . 6
โข (๐ โ โค โ (๐ โ Odd โ โ๐ โ โค ((2 ยท
๐) + 1) = ๐)) |
3 | 1, 2 | syl 17 |
. . . . 5
โข (๐ โ Odd โ (๐ โ Odd โ โ๐ โ โค ((2 ยท
๐) + 1) = ๐)) |
4 | 3 | biimpd 228 |
. . . 4
โข (๐ โ Odd โ (๐ โ Odd โ โ๐ โ โค ((2 ยท
๐) + 1) = ๐)) |
5 | 4 | pm2.43i 52 |
. . 3
โข (๐ โ Odd โ โ๐ โ โค ((2 ยท
๐) + 1) = ๐) |
6 | 5 | 3ad2ant3 1135 |
. 2
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โ โ๐ โ โค ((2 ยท
๐) + 1) = ๐) |
7 | | simpl1 1191 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ ๐ด โ โ) |
8 | | simpl2 1192 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ ๐ด โ 0) |
9 | | 2z 12559 |
. . . . . . 7
โข 2 โ
โค |
10 | | simprl 769 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ ๐ โ โค) |
11 | | zmulcl 12576 |
. . . . . . 7
โข ((2
โ โค โง ๐
โ โค) โ (2 ยท ๐) โ โค) |
12 | 9, 10, 11 | sylancr 587 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ (2 ยท ๐) โ โค) |
13 | 7, 8, 12 | expclzd 14081 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ (๐ดโ(2 ยท ๐)) โ โ) |
14 | 13, 7 | mulneg2d 11633 |
. . . 4
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ ((๐ดโ(2 ยท ๐)) ยท -๐ด) = -((๐ดโ(2 ยท ๐)) ยท ๐ด)) |
15 | | sqneg 14046 |
. . . . . . . . 9
โข (๐ด โ โ โ (-๐ดโ2) = (๐ดโ2)) |
16 | 7, 15 | syl 17 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ (-๐ดโ2) = (๐ดโ2)) |
17 | 16 | oveq1d 7392 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ ((-๐ดโ2)โ๐) = ((๐ดโ2)โ๐)) |
18 | 7 | negcld 11523 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ -๐ด โ โ) |
19 | 7, 8 | negne0d 11534 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ -๐ด โ 0) |
20 | 9 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = ๐) โ 2 โ
โค) |
21 | | simpl 483 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = ๐) โ ๐ โ โค) |
22 | 20, 21 | jca 512 |
. . . . . . . . . 10
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = ๐) โ (2 โ โค โง
๐ โ
โค)) |
23 | 22 | adantl 482 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ (2 โ โค โง ๐ โ
โค)) |
24 | 18, 19, 23 | jca31 515 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ ((-๐ด โ โ โง -๐ด โ 0) โง (2 โ โค โง ๐ โ
โค))) |
25 | | expmulz 14039 |
. . . . . . . 8
โข (((-๐ด โ โ โง -๐ด โ 0) โง (2 โ โค
โง ๐ โ โค))
โ (-๐ดโ(2 ยท
๐)) = ((-๐ดโ2)โ๐)) |
26 | 24, 25 | syl 17 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ (-๐ดโ(2 ยท ๐)) = ((-๐ดโ2)โ๐)) |
27 | 7, 8, 23 | jca31 515 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ ((๐ด โ โ โง ๐ด โ 0) โง (2 โ โค โง ๐ โ
โค))) |
28 | | expmulz 14039 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด โ 0) โง (2 โ โค
โง ๐ โ โค))
โ (๐ดโ(2 ยท
๐)) = ((๐ดโ2)โ๐)) |
29 | 27, 28 | syl 17 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ (๐ดโ(2 ยท ๐)) = ((๐ดโ2)โ๐)) |
30 | 17, 26, 29 | 3eqtr4d 2781 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ (-๐ดโ(2 ยท ๐)) = (๐ดโ(2 ยท ๐))) |
31 | 30 | oveq1d 7392 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ ((-๐ดโ(2 ยท ๐)) ยท -๐ด) = ((๐ดโ(2 ยท ๐)) ยท -๐ด)) |
32 | 18, 19, 12 | expp1zd 14085 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ (-๐ดโ((2 ยท ๐) + 1)) = ((-๐ดโ(2 ยท ๐)) ยท -๐ด)) |
33 | | simprr 771 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ ((2 ยท ๐) + 1) = ๐) |
34 | 33 | oveq2d 7393 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ (-๐ดโ((2 ยท ๐) + 1)) = (-๐ดโ๐)) |
35 | 32, 34 | eqtr3d 2773 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ ((-๐ดโ(2 ยท ๐)) ยท -๐ด) = (-๐ดโ๐)) |
36 | 31, 35 | eqtr3d 2773 |
. . . 4
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ ((๐ดโ(2 ยท ๐)) ยท -๐ด) = (-๐ดโ๐)) |
37 | 14, 36 | eqtr3d 2773 |
. . 3
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ -((๐ดโ(2 ยท ๐)) ยท ๐ด) = (-๐ดโ๐)) |
38 | 7, 8, 12 | expp1zd 14085 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ (๐ดโ((2 ยท ๐) + 1)) = ((๐ดโ(2 ยท ๐)) ยท ๐ด)) |
39 | 33 | oveq2d 7393 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ (๐ดโ((2 ยท ๐) + 1)) = (๐ดโ๐)) |
40 | 38, 39 | eqtr3d 2773 |
. . . 4
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ ((๐ดโ(2 ยท ๐)) ยท ๐ด) = (๐ดโ๐)) |
41 | 40 | negeqd 11419 |
. . 3
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ -((๐ดโ(2 ยท ๐)) ยท ๐ด) = -(๐ดโ๐)) |
42 | 37, 41 | eqtr3d 2773 |
. 2
โข (((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โง (๐ โ โค โง ((2 ยท ๐) + 1) = ๐)) โ (-๐ดโ๐) = -(๐ดโ๐)) |
43 | 6, 42 | rexlimddv 3160 |
1
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ โ Odd ) โ (-๐ดโ๐) = -(๐ดโ๐)) |