Step | Hyp | Ref
| Expression |
1 | | eleq1 2815 |
. . . . . . . 8
โข ((2
ยท ๐) = ๐ โ ((2 ยท ๐) โ โ โ ๐ โ
โ)) |
2 | | simpr 484 |
. . . . . . . . . 10
โข (((2
ยท ๐) โ โ
โง ๐ โ โค)
โ ๐ โ
โค) |
3 | | 2re 12290 |
. . . . . . . . . . . 12
โข 2 โ
โ |
4 | 3 | a1i 11 |
. . . . . . . . . . 11
โข (((2
ยท ๐) โ โ
โง ๐ โ โค)
โ 2 โ โ) |
5 | | zre 12566 |
. . . . . . . . . . . 12
โข (๐ โ โค โ ๐ โ
โ) |
6 | 5 | adantl 481 |
. . . . . . . . . . 11
โข (((2
ยท ๐) โ โ
โง ๐ โ โค)
โ ๐ โ
โ) |
7 | | 0le2 12318 |
. . . . . . . . . . . 12
โข 0 โค
2 |
8 | 7 | a1i 11 |
. . . . . . . . . . 11
โข (((2
ยท ๐) โ โ
โง ๐ โ โค)
โ 0 โค 2) |
9 | | nngt0 12247 |
. . . . . . . . . . . 12
โข ((2
ยท ๐) โ โ
โ 0 < (2 ยท ๐)) |
10 | 9 | adantr 480 |
. . . . . . . . . . 11
โข (((2
ยท ๐) โ โ
โง ๐ โ โค)
โ 0 < (2 ยท ๐)) |
11 | | prodgt0 12065 |
. . . . . . . . . . 11
โข (((2
โ โ โง ๐
โ โ) โง (0 โค 2 โง 0 < (2 ยท ๐))) โ 0 < ๐) |
12 | 4, 6, 8, 10, 11 | syl22anc 836 |
. . . . . . . . . 10
โข (((2
ยท ๐) โ โ
โง ๐ โ โค)
โ 0 < ๐) |
13 | | elnnz 12572 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ โ โค โง 0 <
๐)) |
14 | 2, 12, 13 | sylanbrc 582 |
. . . . . . . . 9
โข (((2
ยท ๐) โ โ
โง ๐ โ โค)
โ ๐ โ
โ) |
15 | 14 | ex 412 |
. . . . . . . 8
โข ((2
ยท ๐) โ โ
โ (๐ โ โค
โ ๐ โ
โ)) |
16 | 1, 15 | syl6bir 254 |
. . . . . . 7
โข ((2
ยท ๐) = ๐ โ (๐ โ โ โ (๐ โ โค โ ๐ โ โ))) |
17 | 16 | com13 88 |
. . . . . 6
โข (๐ โ โค โ (๐ โ โ โ ((2
ยท ๐) = ๐ โ ๐ โ โ))) |
18 | 17 | impcom 407 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โค) โ ((2
ยท ๐) = ๐ โ ๐ โ โ)) |
19 | 18 | pm4.71rd 562 |
. . . 4
โข ((๐ โ โ โง ๐ โ โค) โ ((2
ยท ๐) = ๐ โ (๐ โ โ โง (2 ยท ๐) = ๐))) |
20 | 19 | bicomd 222 |
. . 3
โข ((๐ โ โ โง ๐ โ โค) โ ((๐ โ โ โง (2
ยท ๐) = ๐) โ (2 ยท ๐) = ๐)) |
21 | 20 | rexbidva 3170 |
. 2
โข (๐ โ โ โ
(โ๐ โ โค
(๐ โ โ โง (2
ยท ๐) = ๐) โ โ๐ โ โค (2 ยท
๐) = ๐)) |
22 | | nnssz 12584 |
. . 3
โข โ
โ โค |
23 | | rexss 4050 |
. . 3
โข (โ
โ โค โ (โ๐ โ โ (2 ยท ๐) = ๐ โ โ๐ โ โค (๐ โ โ โง (2 ยท ๐) = ๐))) |
24 | 22, 23 | mp1i 13 |
. 2
โข (๐ โ โ โ
(โ๐ โ โ (2
ยท ๐) = ๐ โ โ๐ โ โค (๐ โ โ โง (2
ยท ๐) = ๐))) |
25 | | even2n 16292 |
. . 3
โข (2
โฅ ๐ โ
โ๐ โ โค (2
ยท ๐) = ๐) |
26 | 25 | a1i 11 |
. 2
โข (๐ โ โ โ (2
โฅ ๐ โ
โ๐ โ โค (2
ยท ๐) = ๐)) |
27 | 21, 24, 26 | 3bitr4rd 312 |
1
โข (๐ โ โ โ (2
โฅ ๐ โ
โ๐ โ โ (2
ยท ๐) = ๐)) |