Step | Hyp | Ref
| Expression |
1 | | nnz 9272 |
. . . . 5
โข (๐ โ โ โ ๐ โ
โค) |
2 | | odd2np1 11878 |
. . . . 5
โข (๐ โ โค โ (ยฌ 2
โฅ ๐ โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐)) |
3 | 1, 2 | syl 14 |
. . . 4
โข (๐ โ โ โ (ยฌ 2
โฅ ๐ โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐)) |
4 | 3 | biimpa 296 |
. . 3
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐) |
5 | 4 | 3adant1 1015 |
. 2
โข ((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐) |
6 | | simpl1 1000 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ๐ด โ โ) |
7 | | simprr 531 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ((2 ยท ๐) + 1) = ๐) |
8 | | simpl2 1001 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ๐ โ โ) |
9 | 8 | nncnd 8933 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ๐ โ โ) |
10 | | 1cnd 7973 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ 1 โ
โ) |
11 | | 2z 9281 |
. . . . . . . . . . 11
โข 2 โ
โค |
12 | | simprl 529 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ๐ โ โค) |
13 | | zmulcl 9306 |
. . . . . . . . . . 11
โข ((2
โ โค โง ๐
โ โค) โ (2 ยท ๐) โ โค) |
14 | 11, 12, 13 | sylancr 414 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (2 ยท ๐) โ
โค) |
15 | 14 | zcnd 9376 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (2 ยท ๐) โ
โ) |
16 | 9, 10, 15 | subadd2d 8287 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ((๐ โ 1) = (2 ยท ๐) โ ((2 ยท ๐) + 1) = ๐)) |
17 | 7, 16 | mpbird 167 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (๐ โ 1) = (2 ยท ๐)) |
18 | | nnm1nn0 9217 |
. . . . . . . 8
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
19 | 8, 18 | syl 14 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (๐ โ 1) โ
โ0) |
20 | 17, 19 | eqeltrrd 2255 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (2 ยท ๐) โ
โ0) |
21 | 6, 20 | expcld 10654 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (๐ดโ(2 ยท ๐)) โ โ) |
22 | 21, 6 | mulneg2d 8369 |
. . . 4
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ((๐ดโ(2 ยท ๐)) ยท -๐ด) = -((๐ดโ(2 ยท ๐)) ยท ๐ด)) |
23 | | sqneg 10579 |
. . . . . . . . 9
โข (๐ด โ โ โ (-๐ดโ2) = (๐ดโ2)) |
24 | 6, 23 | syl 14 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (-๐ดโ2) = (๐ดโ2)) |
25 | 24 | oveq1d 5890 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ((-๐ดโ2)โ๐) = ((๐ดโ2)โ๐)) |
26 | 6 | negcld 8255 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ -๐ด โ โ) |
27 | | 2re 8989 |
. . . . . . . . . . 11
โข 2 โ
โ |
28 | 27 | a1i 9 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ 2 โ
โ) |
29 | 12 | zred 9375 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ๐ โ โ) |
30 | | 2pos 9010 |
. . . . . . . . . . 11
โข 0 <
2 |
31 | 30 | a1i 9 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ 0 <
2) |
32 | 20 | nn0ge0d 9232 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ 0 โค (2 ยท
๐)) |
33 | | prodge0 8811 |
. . . . . . . . . 10
โข (((2
โ โ โง ๐
โ โ) โง (0 < 2 โง 0 โค (2 ยท ๐))) โ 0 โค ๐) |
34 | 28, 29, 31, 32, 33 | syl22anc 1239 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ 0 โค ๐) |
35 | | elnn0z 9266 |
. . . . . . . . 9
โข (๐ โ โ0
โ (๐ โ โค
โง 0 โค ๐)) |
36 | 12, 34, 35 | sylanbrc 417 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ๐ โ โ0) |
37 | | 2nn0 9193 |
. . . . . . . . 9
โข 2 โ
โ0 |
38 | 37 | a1i 9 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ 2 โ
โ0) |
39 | 26, 36, 38 | expmuld 10657 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (-๐ดโ(2 ยท ๐)) = ((-๐ดโ2)โ๐)) |
40 | 6, 36, 38 | expmuld 10657 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (๐ดโ(2 ยท ๐)) = ((๐ดโ2)โ๐)) |
41 | 25, 39, 40 | 3eqtr4d 2220 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (-๐ดโ(2 ยท ๐)) = (๐ดโ(2 ยท ๐))) |
42 | 41 | oveq1d 5890 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ((-๐ดโ(2 ยท ๐)) ยท -๐ด) = ((๐ดโ(2 ยท ๐)) ยท -๐ด)) |
43 | 26, 20 | expp1d 10655 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (-๐ดโ((2 ยท ๐) + 1)) = ((-๐ดโ(2 ยท ๐)) ยท -๐ด)) |
44 | 7 | oveq2d 5891 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (-๐ดโ((2 ยท ๐) + 1)) = (-๐ดโ๐)) |
45 | 43, 44 | eqtr3d 2212 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ((-๐ดโ(2 ยท ๐)) ยท -๐ด) = (-๐ดโ๐)) |
46 | 42, 45 | eqtr3d 2212 |
. . . 4
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ((๐ดโ(2 ยท ๐)) ยท -๐ด) = (-๐ดโ๐)) |
47 | 22, 46 | eqtr3d 2212 |
. . 3
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ -((๐ดโ(2 ยท ๐)) ยท ๐ด) = (-๐ดโ๐)) |
48 | 6, 20 | expp1d 10655 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (๐ดโ((2 ยท ๐) + 1)) = ((๐ดโ(2 ยท ๐)) ยท ๐ด)) |
49 | 7 | oveq2d 5891 |
. . . . 5
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (๐ดโ((2 ยท ๐) + 1)) = (๐ดโ๐)) |
50 | 48, 49 | eqtr3d 2212 |
. . . 4
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ ((๐ดโ(2 ยท ๐)) ยท ๐ด) = (๐ดโ๐)) |
51 | 50 | negeqd 8152 |
. . 3
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ -((๐ดโ(2 ยท ๐)) ยท ๐ด) = -(๐ดโ๐)) |
52 | 47, 51 | eqtr3d 2212 |
. 2
โข (((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โค โง ((2
ยท ๐) + 1) = ๐)) โ (-๐ดโ๐) = -(๐ดโ๐)) |
53 | 5, 52 | rexlimddv 2599 |
1
โข ((๐ด โ โ โง ๐ โ โ โง ยฌ 2
โฅ ๐) โ (-๐ดโ๐) = -(๐ดโ๐)) |