Step | Hyp | Ref
| Expression |
1 | | eleq1 2240 |
. . . . . . . 8
โข (((2
ยท ๐) + 1) = ๐ โ (((2 ยท ๐) + 1) โ
โ0 โ ๐ โ
โ0)) |
2 | | elnn0z 9268 |
. . . . . . . . 9
โข (((2
ยท ๐) + 1) โ
โ0 โ (((2 ยท ๐) + 1) โ โค โง 0 โค ((2
ยท ๐) +
1))) |
3 | | 2tnp1ge0ge0 10303 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ (0 โค
((2 ยท ๐) + 1) โ
0 โค ๐)) |
4 | 3 | biimpd 144 |
. . . . . . . . . . . 12
โข (๐ โ โค โ (0 โค
((2 ยท ๐) + 1) โ
0 โค ๐)) |
5 | 4 | imdistani 445 |
. . . . . . . . . . 11
โข ((๐ โ โค โง 0 โค ((2
ยท ๐) + 1)) โ
(๐ โ โค โง 0
โค ๐)) |
6 | 5 | expcom 116 |
. . . . . . . . . 10
โข (0 โค
((2 ยท ๐) + 1) โ
(๐ โ โค โ
(๐ โ โค โง 0
โค ๐))) |
7 | | elnn0z 9268 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (๐ โ โค
โง 0 โค ๐)) |
8 | 6, 7 | imbitrrdi 162 |
. . . . . . . . 9
โข (0 โค
((2 ยท ๐) + 1) โ
(๐ โ โค โ
๐ โ
โ0)) |
9 | 2, 8 | simplbiim 387 |
. . . . . . . 8
โข (((2
ยท ๐) + 1) โ
โ0 โ (๐ โ โค โ ๐ โ
โ0)) |
10 | 1, 9 | syl6bir 164 |
. . . . . . 7
โข (((2
ยท ๐) + 1) = ๐ โ (๐ โ โ0 โ (๐ โ โค โ ๐ โ
โ0))) |
11 | 10 | com13 80 |
. . . . . 6
โข (๐ โ โค โ (๐ โ โ0
โ (((2 ยท ๐) +
1) = ๐ โ ๐ โ
โ0))) |
12 | 11 | impcom 125 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ โค)
โ (((2 ยท ๐) +
1) = ๐ โ ๐ โ
โ0)) |
13 | 12 | pm4.71rd 394 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ โค)
โ (((2 ยท ๐) +
1) = ๐ โ (๐ โ โ0
โง ((2 ยท ๐) + 1)
= ๐))) |
14 | 13 | bicomd 141 |
. . 3
โข ((๐ โ โ0
โง ๐ โ โค)
โ ((๐ โ
โ0 โง ((2 ยท ๐) + 1) = ๐) โ ((2 ยท ๐) + 1) = ๐)) |
15 | 14 | rexbidva 2474 |
. 2
โข (๐ โ โ0
โ (โ๐ โ
โค (๐ โ
โ0 โง ((2 ยท ๐) + 1) = ๐) โ โ๐ โ โค ((2 ยท ๐) + 1) = ๐)) |
16 | | nn0ssz 9273 |
. . 3
โข
โ0 โ โค |
17 | | rexss 3224 |
. . 3
โข
(โ0 โ โค โ (โ๐ โ โ0 ((2 ยท
๐) + 1) = ๐ โ โ๐ โ โค (๐ โ โ0 โง ((2
ยท ๐) + 1) = ๐))) |
18 | 16, 17 | mp1i 10 |
. 2
โข (๐ โ โ0
โ (โ๐ โ
โ0 ((2 ยท ๐) + 1) = ๐ โ โ๐ โ โค (๐ โ โ0 โง ((2
ยท ๐) + 1) = ๐))) |
19 | | nn0z 9275 |
. . 3
โข (๐ โ โ0
โ ๐ โ
โค) |
20 | | odd2np1 11880 |
. . 3
โข (๐ โ โค โ (ยฌ 2
โฅ ๐ โ
โ๐ โ โค ((2
ยท ๐) + 1) = ๐)) |
21 | 19, 20 | syl 14 |
. 2
โข (๐ โ โ0
โ (ยฌ 2 โฅ ๐
โ โ๐ โ
โค ((2 ยท ๐) +
1) = ๐)) |
22 | 15, 18, 21 | 3bitr4rd 221 |
1
โข (๐ โ โ0
โ (ยฌ 2 โฅ ๐
โ โ๐ โ
โ0 ((2 ยท ๐) + 1) = ๐)) |