Step | Hyp | Ref
| Expression |
1 | | nnz 12456 |
. . . . 5
โข (๐ โ โ โ ๐ โ
โค) |
2 | | odd2np1 16158 |
. . . . 5
โข (๐ โ โค โ (ยฌ 2
โฅ ๐ โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐)) |
3 | 1, 2 | syl 17 |
. . . 4
โข (๐ โ โ โ (ยฌ 2
โฅ ๐ โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐)) |
4 | 3 | biimpa 478 |
. . 3
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐) |
5 | 4 | 3adant1 1131 |
. 2
โข ((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐) |
6 | | simpl1 1192 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ๐ด โ โ) |
7 | | simprr 772 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ((2 ยท ๐) + 1) = ๐) |
8 | | simpl2 1193 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ๐ โ โ) |
9 | 8 | nncnd 12103 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ๐ โ โ) |
10 | | 1cnd 11084 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ 1 โ
โ) |
11 | | 2z 12466 |
. . . . . . . . . . 11
โข 2 โ
โค |
12 | | simprl 770 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ๐ โ โค) |
13 | | zmulcl 12483 |
. . . . . . . . . . 11
โข ((2
โ โค โง ๐
โ โค) โ (2 ยท ๐) โ โค) |
14 | 11, 12, 13 | sylancr 588 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (2 ยท ๐) โ
โค) |
15 | 14 | zcnd 12541 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (2 ยท ๐) โ
โ) |
16 | 9, 10, 15 | subadd2d 11465 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ((๐ โ 1) = (2 ยท ๐) โ ((2 ยท ๐) + 1) = ๐)) |
17 | 7, 16 | mpbird 257 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (๐ โ 1) = (2 ยท ๐)) |
18 | | nnm1nn0 12388 |
. . . . . . . 8
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
19 | 8, 18 | syl 17 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (๐ โ 1) โ
โ0) |
20 | 17, 19 | eqeltrrd 2840 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (2 ยท ๐) โ
โ0) |
21 | 6, 20 | expcld 13978 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (๐ดโ(2 ยท ๐)) โ โ) |
22 | 21, 6 | mulneg2d 11543 |
. . . 4
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ((๐ดโ(2 ยท ๐)) ยท -๐ด) = -((๐ดโ(2 ยท ๐)) ยท ๐ด)) |
23 | | sqneg 13950 |
. . . . . . . . 9
โข (๐ด โ โ โ (-๐ดโ2) = (๐ดโ2)) |
24 | 6, 23 | syl 17 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (-๐ดโ2) = (๐ดโ2)) |
25 | 24 | oveq1d 7365 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ((-๐ดโ2)โ๐) = ((๐ดโ2)โ๐)) |
26 | 6 | negcld 11433 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ -๐ด โ โ) |
27 | | 2rp 12849 |
. . . . . . . . . . 11
โข 2 โ
โ+ |
28 | 27 | a1i 11 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ 2 โ
โ+) |
29 | 12 | zred 12540 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ๐ โ โ) |
30 | 20 | nn0ge0d 12410 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ 0 โค (2 ยท
๐)) |
31 | 28, 29, 30 | prodge0rd 12951 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ 0 โค ๐) |
32 | | elnn0z 12446 |
. . . . . . . . 9
โข (๐ โ โ0
โ (๐ โ โค
โง 0 โค ๐)) |
33 | 12, 31, 32 | sylanbrc 584 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ๐ โ โ0) |
34 | | 2nn0 12364 |
. . . . . . . . 9
โข 2 โ
โ0 |
35 | 34 | a1i 11 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ 2 โ
โ0) |
36 | 26, 33, 35 | expmuld 13981 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (-๐ดโ(2 ยท ๐)) = ((-๐ดโ2)โ๐)) |
37 | 6, 33, 35 | expmuld 13981 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (๐ดโ(2 ยท ๐)) = ((๐ดโ2)โ๐)) |
38 | 25, 36, 37 | 3eqtr4d 2788 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (-๐ดโ(2 ยท ๐)) = (๐ดโ(2 ยท ๐))) |
39 | 38 | oveq1d 7365 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ((-๐ดโ(2 ยท ๐)) ยท -๐ด) = ((๐ดโ(2 ยท ๐)) ยท -๐ด)) |
40 | 26, 20 | expp1d 13979 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (-๐ดโ((2 ยท ๐) + 1)) = ((-๐ดโ(2 ยท ๐)) ยท -๐ด)) |
41 | 7 | oveq2d 7366 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (-๐ดโ((2 ยท ๐) + 1)) = (-๐ดโ๐)) |
42 | 40, 41 | eqtr3d 2780 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ((-๐ดโ(2 ยท ๐)) ยท -๐ด) = (-๐ดโ๐)) |
43 | 39, 42 | eqtr3d 2780 |
. . . 4
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ((๐ดโ(2 ยท ๐)) ยท -๐ด) = (-๐ดโ๐)) |
44 | 22, 43 | eqtr3d 2780 |
. . 3
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ -((๐ดโ(2 ยท ๐)) ยท ๐ด) = (-๐ดโ๐)) |
45 | 6, 20 | expp1d 13979 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (๐ดโ((2 ยท ๐) + 1)) = ((๐ดโ(2 ยท ๐)) ยท ๐ด)) |
46 | 7 | oveq2d 7366 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (๐ดโ((2 ยท ๐) + 1)) = (๐ดโ๐)) |
47 | 45, 46 | eqtr3d 2780 |
. . . 4
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ((๐ดโ(2 ยท ๐)) ยท ๐ด) = (๐ดโ๐)) |
48 | 47 | negeqd 11329 |
. . 3
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ -((๐ดโ(2 ยท ๐)) ยท ๐ด) = -(๐ดโ๐)) |
49 | 44, 48 | eqtr3d 2780 |
. 2
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (-๐ดโ๐) = -(๐ดโ๐)) |
50 | 5, 49 | rexlimddv 3157 |
1
โข ((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โ (-๐ดโ๐) = -(๐ดโ๐)) |