Step | Hyp | Ref
| Expression |
1 | | eleq1 2250 |
. . . . . . . 8
โข ((2
ยท ๐) = ๐ โ ((2 ยท ๐) โ โ0
โ ๐ โ
โ0)) |
2 | | simpr 110 |
. . . . . . . . . 10
โข (((2
ยท ๐) โ
โ0 โง ๐
โ โค) โ ๐
โ โค) |
3 | | 2re 9002 |
. . . . . . . . . . . 12
โข 2 โ
โ |
4 | 3 | a1i 9 |
. . . . . . . . . . 11
โข (((2
ยท ๐) โ
โ0 โง ๐
โ โค) โ 2 โ โ) |
5 | | zre 9270 |
. . . . . . . . . . . 12
โข (๐ โ โค โ ๐ โ
โ) |
6 | 5 | adantl 277 |
. . . . . . . . . . 11
โข (((2
ยท ๐) โ
โ0 โง ๐
โ โค) โ ๐
โ โ) |
7 | | 2pos 9023 |
. . . . . . . . . . . 12
โข 0 <
2 |
8 | 7 | a1i 9 |
. . . . . . . . . . 11
โข (((2
ยท ๐) โ
โ0 โง ๐
โ โค) โ 0 < 2) |
9 | | nn0ge0 9214 |
. . . . . . . . . . . 12
โข ((2
ยท ๐) โ
โ0 โ 0 โค (2 ยท ๐)) |
10 | 9 | adantr 276 |
. . . . . . . . . . 11
โข (((2
ยท ๐) โ
โ0 โง ๐
โ โค) โ 0 โค (2 ยท ๐)) |
11 | | prodge0 8824 |
. . . . . . . . . . 11
โข (((2
โ โ โง ๐
โ โ) โง (0 < 2 โง 0 โค (2 ยท ๐))) โ 0 โค ๐) |
12 | 4, 6, 8, 10, 11 | syl22anc 1249 |
. . . . . . . . . 10
โข (((2
ยท ๐) โ
โ0 โง ๐
โ โค) โ 0 โค ๐) |
13 | | elnn0z 9279 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (๐ โ โค
โง 0 โค ๐)) |
14 | 2, 12, 13 | sylanbrc 417 |
. . . . . . . . 9
โข (((2
ยท ๐) โ
โ0 โง ๐
โ โค) โ ๐
โ โ0) |
15 | 14 | ex 115 |
. . . . . . . 8
โข ((2
ยท ๐) โ
โ0 โ (๐ โ โค โ ๐ โ
โ0)) |
16 | 1, 15 | syl6bir 164 |
. . . . . . 7
โข ((2
ยท ๐) = ๐ โ (๐ โ โ0 โ (๐ โ โค โ ๐ โ
โ0))) |
17 | 16 | com13 80 |
. . . . . 6
โข (๐ โ โค โ (๐ โ โ0
โ ((2 ยท ๐) =
๐ โ ๐ โ
โ0))) |
18 | 17 | impcom 125 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ โค)
โ ((2 ยท ๐) =
๐ โ ๐ โ
โ0)) |
19 | 18 | pm4.71rd 394 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ โค)
โ ((2 ยท ๐) =
๐ โ (๐ โ โ0
โง (2 ยท ๐) =
๐))) |
20 | 19 | bicomd 141 |
. . 3
โข ((๐ โ โ0
โง ๐ โ โค)
โ ((๐ โ
โ0 โง (2 ยท ๐) = ๐) โ (2 ยท ๐) = ๐)) |
21 | 20 | rexbidva 2484 |
. 2
โข (๐ โ โ0
โ (โ๐ โ
โค (๐ โ
โ0 โง (2 ยท ๐) = ๐) โ โ๐ โ โค (2 ยท ๐) = ๐)) |
22 | | nn0ssz 9284 |
. . 3
โข
โ0 โ โค |
23 | | rexss 3234 |
. . 3
โข
(โ0 โ โค โ (โ๐ โ โ0 (2 ยท ๐) = ๐ โ โ๐ โ โค (๐ โ โ0 โง (2 ยท
๐) = ๐))) |
24 | 22, 23 | mp1i 10 |
. 2
โข (๐ โ โ0
โ (โ๐ โ
โ0 (2 ยท ๐) = ๐ โ โ๐ โ โค (๐ โ โ0 โง (2 ยท
๐) = ๐))) |
25 | | even2n 11892 |
. . 3
โข (2
โฅ ๐ โ
โ๐ โ โค (2
ยท ๐) = ๐) |
26 | 25 | a1i 9 |
. 2
โข (๐ โ โ0
โ (2 โฅ ๐ โ
โ๐ โ โค (2
ยท ๐) = ๐)) |
27 | 21, 24, 26 | 3bitr4rd 221 |
1
โข (๐ โ โ0
โ (2 โฅ ๐ โ
โ๐ โ
โ0 (2 ยท ๐) = ๐)) |