Metamath Proof Explorer


Theorem 2tp1odd

Description: A number which is twice an integer increased by 1 is odd. (Contributed by AV, 16-Jul-2021)

Ref Expression
Assertion 2tp1odd ( ( ๐ด โˆˆ โ„ค โˆง ๐ต = ( ( 2 ยท ๐ด ) + 1 ) ) โ†’ ยฌ 2 โˆฅ ๐ต )

Proof

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 โˆฅ ๐ต )