Step |
Hyp |
Ref |
Expression |
1 |
|
prmlem1.n |
โข ๐ โ โ |
2 |
|
prmlem1.gt |
โข 1 < ๐ |
3 |
|
prmlem1.2 |
โข ยฌ 2 โฅ ๐ |
4 |
|
prmlem1.3 |
โข ยฌ 3 โฅ ๐ |
5 |
|
prmlem1.lt |
โข ๐ < ; 2 5 |
6 |
|
eluzelre |
โข ( ๐ฅ โ ( โคโฅ โ 5 ) โ ๐ฅ โ โ ) |
7 |
6
|
resqcld |
โข ( ๐ฅ โ ( โคโฅ โ 5 ) โ ( ๐ฅ โ 2 ) โ โ ) |
8 |
|
eluzle |
โข ( ๐ฅ โ ( โคโฅ โ 5 ) โ 5 โค ๐ฅ ) |
9 |
|
5re |
โข 5 โ โ |
10 |
|
5nn0 |
โข 5 โ โ0 |
11 |
10
|
nn0ge0i |
โข 0 โค 5 |
12 |
|
le2sq2 |
โข ( ( ( 5 โ โ โง 0 โค 5 ) โง ( ๐ฅ โ โ โง 5 โค ๐ฅ ) ) โ ( 5 โ 2 ) โค ( ๐ฅ โ 2 ) ) |
13 |
9 11 12
|
mpanl12 |
โข ( ( ๐ฅ โ โ โง 5 โค ๐ฅ ) โ ( 5 โ 2 ) โค ( ๐ฅ โ 2 ) ) |
14 |
6 8 13
|
syl2anc |
โข ( ๐ฅ โ ( โคโฅ โ 5 ) โ ( 5 โ 2 ) โค ( ๐ฅ โ 2 ) ) |
15 |
1
|
nnrei |
โข ๐ โ โ |
16 |
9
|
resqcli |
โข ( 5 โ 2 ) โ โ |
17 |
|
5cn |
โข 5 โ โ |
18 |
17
|
sqvali |
โข ( 5 โ 2 ) = ( 5 ยท 5 ) |
19 |
|
5t5e25 |
โข ( 5 ยท 5 ) = ; 2 5 |
20 |
18 19
|
eqtri |
โข ( 5 โ 2 ) = ; 2 5 |
21 |
5 20
|
breqtrri |
โข ๐ < ( 5 โ 2 ) |
22 |
|
ltletr |
โข ( ( ๐ โ โ โง ( 5 โ 2 ) โ โ โง ( ๐ฅ โ 2 ) โ โ ) โ ( ( ๐ < ( 5 โ 2 ) โง ( 5 โ 2 ) โค ( ๐ฅ โ 2 ) ) โ ๐ < ( ๐ฅ โ 2 ) ) ) |
23 |
21 22
|
mpani |
โข ( ( ๐ โ โ โง ( 5 โ 2 ) โ โ โง ( ๐ฅ โ 2 ) โ โ ) โ ( ( 5 โ 2 ) โค ( ๐ฅ โ 2 ) โ ๐ < ( ๐ฅ โ 2 ) ) ) |
24 |
15 16 23
|
mp3an12 |
โข ( ( ๐ฅ โ 2 ) โ โ โ ( ( 5 โ 2 ) โค ( ๐ฅ โ 2 ) โ ๐ < ( ๐ฅ โ 2 ) ) ) |
25 |
7 14 24
|
sylc |
โข ( ๐ฅ โ ( โคโฅ โ 5 ) โ ๐ < ( ๐ฅ โ 2 ) ) |
26 |
|
ltnle |
โข ( ( ๐ โ โ โง ( ๐ฅ โ 2 ) โ โ ) โ ( ๐ < ( ๐ฅ โ 2 ) โ ยฌ ( ๐ฅ โ 2 ) โค ๐ ) ) |
27 |
15 7 26
|
sylancr |
โข ( ๐ฅ โ ( โคโฅ โ 5 ) โ ( ๐ < ( ๐ฅ โ 2 ) โ ยฌ ( ๐ฅ โ 2 ) โค ๐ ) ) |
28 |
25 27
|
mpbid |
โข ( ๐ฅ โ ( โคโฅ โ 5 ) โ ยฌ ( ๐ฅ โ 2 ) โค ๐ ) |
29 |
28
|
pm2.21d |
โข ( ๐ฅ โ ( โคโฅ โ 5 ) โ ( ( ๐ฅ โ 2 ) โค ๐ โ ยฌ ๐ฅ โฅ ๐ ) ) |
30 |
29
|
adantld |
โข ( ๐ฅ โ ( โคโฅ โ 5 ) โ ( ( ๐ฅ โ ( โ โ { 2 } ) โง ( ๐ฅ โ 2 ) โค ๐ ) โ ยฌ ๐ฅ โฅ ๐ ) ) |
31 |
30
|
adantl |
โข ( ( ยฌ 2 โฅ 5 โง ๐ฅ โ ( โคโฅ โ 5 ) ) โ ( ( ๐ฅ โ ( โ โ { 2 } ) โง ( ๐ฅ โ 2 ) โค ๐ ) โ ยฌ ๐ฅ โฅ ๐ ) ) |
32 |
1 2 3 4 31
|
prmlem1a |
โข ๐ โ โ |