Step |
Hyp |
Ref |
Expression |
1 |
|
nn0ge0 |
โข ( ๐ โ โ0 โ 0 โค ๐ ) |
2 |
|
nn0re |
โข ( ๐ โ โ0 โ ๐ โ โ ) |
3 |
|
nn0addge1 |
โข ( ( ๐ โ โ โง ๐ โ โ0 ) โ ๐ โค ( ๐ + ๐ ) ) |
4 |
2 3
|
mpancom |
โข ( ๐ โ โ0 โ ๐ โค ( ๐ + ๐ ) ) |
5 |
|
nn0cn |
โข ( ๐ โ โ0 โ ๐ โ โ ) |
6 |
5
|
2timesd |
โข ( ๐ โ โ0 โ ( 2 ยท ๐ ) = ( ๐ + ๐ ) ) |
7 |
4 6
|
breqtrrd |
โข ( ๐ โ โ0 โ ๐ โค ( 2 ยท ๐ ) ) |
8 |
|
nn0z |
โข ( ๐ โ โ0 โ ๐ โ โค ) |
9 |
|
0zd |
โข ( ๐ โ โ0 โ 0 โ โค ) |
10 |
|
2z |
โข 2 โ โค |
11 |
|
zmulcl |
โข ( ( 2 โ โค โง ๐ โ โค ) โ ( 2 ยท ๐ ) โ โค ) |
12 |
10 8 11
|
sylancr |
โข ( ๐ โ โ0 โ ( 2 ยท ๐ ) โ โค ) |
13 |
|
elfz |
โข ( ( ๐ โ โค โง 0 โ โค โง ( 2 ยท ๐ ) โ โค ) โ ( ๐ โ ( 0 ... ( 2 ยท ๐ ) ) โ ( 0 โค ๐ โง ๐ โค ( 2 ยท ๐ ) ) ) ) |
14 |
8 9 12 13
|
syl3anc |
โข ( ๐ โ โ0 โ ( ๐ โ ( 0 ... ( 2 ยท ๐ ) ) โ ( 0 โค ๐ โง ๐ โค ( 2 ยท ๐ ) ) ) ) |
15 |
1 7 14
|
mpbir2and |
โข ( ๐ โ โ0 โ ๐ โ ( 0 ... ( 2 ยท ๐ ) ) ) |