Step |
Hyp |
Ref |
Expression |
1 |
|
eleq1 |
โข ( ( 2 ยท ๐ ) = ๐ โ ( ( 2 ยท ๐ ) โ โ โ ๐ โ โ ) ) |
2 |
|
simpr |
โข ( ( ( 2 ยท ๐ ) โ โ โง ๐ โ โค ) โ ๐ โ โค ) |
3 |
|
2re |
โข 2 โ โ |
4 |
3
|
a1i |
โข ( ( ( 2 ยท ๐ ) โ โ โง ๐ โ โค ) โ 2 โ โ ) |
5 |
|
zre |
โข ( ๐ โ โค โ ๐ โ โ ) |
6 |
5
|
adantl |
โข ( ( ( 2 ยท ๐ ) โ โ โง ๐ โ โค ) โ ๐ โ โ ) |
7 |
|
0le2 |
โข 0 โค 2 |
8 |
7
|
a1i |
โข ( ( ( 2 ยท ๐ ) โ โ โง ๐ โ โค ) โ 0 โค 2 ) |
9 |
|
nngt0 |
โข ( ( 2 ยท ๐ ) โ โ โ 0 < ( 2 ยท ๐ ) ) |
10 |
9
|
adantr |
โข ( ( ( 2 ยท ๐ ) โ โ โง ๐ โ โค ) โ 0 < ( 2 ยท ๐ ) ) |
11 |
|
prodgt0 |
โข ( ( ( 2 โ โ โง ๐ โ โ ) โง ( 0 โค 2 โง 0 < ( 2 ยท ๐ ) ) ) โ 0 < ๐ ) |
12 |
4 6 8 10 11
|
syl22anc |
โข ( ( ( 2 ยท ๐ ) โ โ โง ๐ โ โค ) โ 0 < ๐ ) |
13 |
|
elnnz |
โข ( ๐ โ โ โ ( ๐ โ โค โง 0 < ๐ ) ) |
14 |
2 12 13
|
sylanbrc |
โข ( ( ( 2 ยท ๐ ) โ โ โง ๐ โ โค ) โ ๐ โ โ ) |
15 |
14
|
ex |
โข ( ( 2 ยท ๐ ) โ โ โ ( ๐ โ โค โ ๐ โ โ ) ) |
16 |
1 15
|
syl6bir |
โข ( ( 2 ยท ๐ ) = ๐ โ ( ๐ โ โ โ ( ๐ โ โค โ ๐ โ โ ) ) ) |
17 |
16
|
com13 |
โข ( ๐ โ โค โ ( ๐ โ โ โ ( ( 2 ยท ๐ ) = ๐ โ ๐ โ โ ) ) ) |
18 |
17
|
impcom |
โข ( ( ๐ โ โ โง ๐ โ โค ) โ ( ( 2 ยท ๐ ) = ๐ โ ๐ โ โ ) ) |
19 |
18
|
pm4.71rd |
โข ( ( ๐ โ โ โง ๐ โ โค ) โ ( ( 2 ยท ๐ ) = ๐ โ ( ๐ โ โ โง ( 2 ยท ๐ ) = ๐ ) ) ) |
20 |
19
|
bicomd |
โข ( ( ๐ โ โ โง ๐ โ โค ) โ ( ( ๐ โ โ โง ( 2 ยท ๐ ) = ๐ ) โ ( 2 ยท ๐ ) = ๐ ) ) |
21 |
20
|
rexbidva |
โข ( ๐ โ โ โ ( โ ๐ โ โค ( ๐ โ โ โง ( 2 ยท ๐ ) = ๐ ) โ โ ๐ โ โค ( 2 ยท ๐ ) = ๐ ) ) |
22 |
|
nnssz |
โข โ โ โค |
23 |
|
rexss |
โข ( โ โ โค โ ( โ ๐ โ โ ( 2 ยท ๐ ) = ๐ โ โ ๐ โ โค ( ๐ โ โ โง ( 2 ยท ๐ ) = ๐ ) ) ) |
24 |
22 23
|
mp1i |
โข ( ๐ โ โ โ ( โ ๐ โ โ ( 2 ยท ๐ ) = ๐ โ โ ๐ โ โค ( ๐ โ โ โง ( 2 ยท ๐ ) = ๐ ) ) ) |
25 |
|
even2n |
โข ( 2 โฅ ๐ โ โ ๐ โ โค ( 2 ยท ๐ ) = ๐ ) |
26 |
25
|
a1i |
โข ( ๐ โ โ โ ( 2 โฅ ๐ โ โ ๐ โ โค ( 2 ยท ๐ ) = ๐ ) ) |
27 |
21 24 26
|
3bitr4rd |
โข ( ๐ โ โ โ ( 2 โฅ ๐ โ โ ๐ โ โ ( 2 ยท ๐ ) = ๐ ) ) |