Step |
Hyp |
Ref |
Expression |
1 |
|
1z |
โข 1 โ โค |
2 |
|
nnuz |
โข โ = ( โคโฅ โ 1 ) |
3 |
|
id |
โข ( 1 โ โค โ 1 โ โค ) |
4 |
|
ax-1ne0 |
โข 1 โ 0 |
5 |
4
|
a1i |
โข ( 1 โ โค โ 1 โ 0 ) |
6 |
2
|
prodfclim1 |
โข ( 1 โ โค โ seq 1 ( ยท , ( โ ร { 1 } ) ) โ 1 ) |
7 |
|
0ss |
โข โ
โ โ |
8 |
7
|
a1i |
โข ( 1 โ โค โ โ
โ โ ) |
9 |
|
fvconst2g |
โข ( ( 1 โ โค โง ๐ โ โ ) โ ( ( โ ร { 1 } ) โ ๐ ) = 1 ) |
10 |
|
noel |
โข ยฌ ๐ โ โ
|
11 |
10
|
iffalsei |
โข if ( ๐ โ โ
, ๐ด , 1 ) = 1 |
12 |
9 11
|
eqtr4di |
โข ( ( 1 โ โค โง ๐ โ โ ) โ ( ( โ ร { 1 } ) โ ๐ ) = if ( ๐ โ โ
, ๐ด , 1 ) ) |
13 |
10
|
pm2.21i |
โข ( ๐ โ โ
โ ๐ด โ โ ) |
14 |
13
|
adantl |
โข ( ( 1 โ โค โง ๐ โ โ
) โ ๐ด โ โ ) |
15 |
2 3 5 6 8 12 14
|
zprodn0 |
โข ( 1 โ โค โ โ ๐ โ โ
๐ด = 1 ) |
16 |
1 15
|
ax-mp |
โข โ ๐ โ โ
๐ด = 1 |