Step |
Hyp |
Ref |
Expression |
1 |
|
id |
โข ( ๐ด โ โค โ ๐ด โ โค ) |
2 |
|
oveq2 |
โข ( ๐ = ๐ด โ ( 2 ยท ๐ ) = ( 2 ยท ๐ด ) ) |
3 |
2
|
oveq1d |
โข ( ๐ = ๐ด โ ( ( 2 ยท ๐ ) + 1 ) = ( ( 2 ยท ๐ด ) + 1 ) ) |
4 |
3
|
eqeq1d |
โข ( ๐ = ๐ด โ ( ( ( 2 ยท ๐ ) + 1 ) = ( ( 2 ยท ๐ด ) + 1 ) โ ( ( 2 ยท ๐ด ) + 1 ) = ( ( 2 ยท ๐ด ) + 1 ) ) ) |
5 |
4
|
adantl |
โข ( ( ๐ด โ โค โง ๐ = ๐ด ) โ ( ( ( 2 ยท ๐ ) + 1 ) = ( ( 2 ยท ๐ด ) + 1 ) โ ( ( 2 ยท ๐ด ) + 1 ) = ( ( 2 ยท ๐ด ) + 1 ) ) ) |
6 |
|
eqidd |
โข ( ๐ด โ โค โ ( ( 2 ยท ๐ด ) + 1 ) = ( ( 2 ยท ๐ด ) + 1 ) ) |
7 |
1 5 6
|
rspcedvd |
โข ( ๐ด โ โค โ โ ๐ โ โค ( ( 2 ยท ๐ ) + 1 ) = ( ( 2 ยท ๐ด ) + 1 ) ) |
8 |
|
2z |
โข 2 โ โค |
9 |
8
|
a1i |
โข ( ๐ด โ โค โ 2 โ โค ) |
10 |
9 1
|
zmulcld |
โข ( ๐ด โ โค โ ( 2 ยท ๐ด ) โ โค ) |
11 |
10
|
peano2zd |
โข ( ๐ด โ โค โ ( ( 2 ยท ๐ด ) + 1 ) โ โค ) |
12 |
|
odd2np1 |
โข ( ( ( 2 ยท ๐ด ) + 1 ) โ โค โ ( ยฌ 2 โฅ ( ( 2 ยท ๐ด ) + 1 ) โ โ ๐ โ โค ( ( 2 ยท ๐ ) + 1 ) = ( ( 2 ยท ๐ด ) + 1 ) ) ) |
13 |
11 12
|
syl |
โข ( ๐ด โ โค โ ( ยฌ 2 โฅ ( ( 2 ยท ๐ด ) + 1 ) โ โ ๐ โ โค ( ( 2 ยท ๐ ) + 1 ) = ( ( 2 ยท ๐ด ) + 1 ) ) ) |
14 |
7 13
|
mpbird |
โข ( ๐ด โ โค โ ยฌ 2 โฅ ( ( 2 ยท ๐ด ) + 1 ) ) |
15 |
14
|
adantr |
โข ( ( ๐ด โ โค โง ๐ต = ( ( 2 ยท ๐ด ) + 1 ) ) โ ยฌ 2 โฅ ( ( 2 ยท ๐ด ) + 1 ) ) |
16 |
|
breq2 |
โข ( ๐ต = ( ( 2 ยท ๐ด ) + 1 ) โ ( 2 โฅ ๐ต โ 2 โฅ ( ( 2 ยท ๐ด ) + 1 ) ) ) |
17 |
16
|
adantl |
โข ( ( ๐ด โ โค โง ๐ต = ( ( 2 ยท ๐ด ) + 1 ) ) โ ( 2 โฅ ๐ต โ 2 โฅ ( ( 2 ยท ๐ด ) + 1 ) ) ) |
18 |
15 17
|
mtbird |
โข ( ( ๐ด โ โค โง ๐ต = ( ( 2 ยท ๐ด ) + 1 ) ) โ ยฌ 2 โฅ ๐ต ) |