Step |
Hyp |
Ref |
Expression |
1 |
|
zofldiv2ALTV |
โข ( ๐พ โ Odd โ ( โ โ ( ๐พ / 2 ) ) = ( ( ๐พ โ 1 ) / 2 ) ) |
2 |
1
|
oveq2d |
โข ( ๐พ โ Odd โ ( 2 ยท ( โ โ ( ๐พ / 2 ) ) ) = ( 2 ยท ( ( ๐พ โ 1 ) / 2 ) ) ) |
3 |
2
|
oveq1d |
โข ( ๐พ โ Odd โ ( ( 2 ยท ( โ โ ( ๐พ / 2 ) ) ) + 1 ) = ( ( 2 ยท ( ( ๐พ โ 1 ) / 2 ) ) + 1 ) ) |
4 |
|
oddz |
โข ( ๐พ โ Odd โ ๐พ โ โค ) |
5 |
|
peano2zm |
โข ( ๐พ โ โค โ ( ๐พ โ 1 ) โ โค ) |
6 |
5
|
zcnd |
โข ( ๐พ โ โค โ ( ๐พ โ 1 ) โ โ ) |
7 |
4 6
|
syl |
โข ( ๐พ โ Odd โ ( ๐พ โ 1 ) โ โ ) |
8 |
|
2cnd |
โข ( ๐พ โ Odd โ 2 โ โ ) |
9 |
|
2ne0 |
โข 2 โ 0 |
10 |
9
|
a1i |
โข ( ๐พ โ Odd โ 2 โ 0 ) |
11 |
7 8 10
|
divcan2d |
โข ( ๐พ โ Odd โ ( 2 ยท ( ( ๐พ โ 1 ) / 2 ) ) = ( ๐พ โ 1 ) ) |
12 |
11
|
oveq1d |
โข ( ๐พ โ Odd โ ( ( 2 ยท ( ( ๐พ โ 1 ) / 2 ) ) + 1 ) = ( ( ๐พ โ 1 ) + 1 ) ) |
13 |
4
|
zcnd |
โข ( ๐พ โ Odd โ ๐พ โ โ ) |
14 |
|
npcan1 |
โข ( ๐พ โ โ โ ( ( ๐พ โ 1 ) + 1 ) = ๐พ ) |
15 |
13 14
|
syl |
โข ( ๐พ โ Odd โ ( ( ๐พ โ 1 ) + 1 ) = ๐พ ) |
16 |
3 12 15
|
3eqtrrd |
โข ( ๐พ โ Odd โ ๐พ = ( ( 2 ยท ( โ โ ( ๐พ / 2 ) ) ) + 1 ) ) |