Step |
Hyp |
Ref |
Expression |
1 |
|
etransclem32.s |
โข ( ๐ โ ๐ โ { โ , โ } ) |
2 |
|
etransclem32.x |
โข ( ๐ โ ๐ โ ( ( TopOpen โ โfld ) โพt ๐ ) ) |
3 |
|
etransclem32.p |
โข ( ๐ โ ๐ โ โ ) |
4 |
|
etransclem32.m |
โข ( ๐ โ ๐ โ โ0 ) |
5 |
|
etransclem32.f |
โข ๐น = ( ๐ฅ โ ๐ โฆ ( ( ๐ฅ โ ( ๐ โ 1 ) ) ยท โ ๐ โ ( 1 ... ๐ ) ( ( ๐ฅ โ ๐ ) โ ๐ ) ) ) |
6 |
|
etransclem32.n |
โข ( ๐ โ ๐ โ โ0 ) |
7 |
|
etransclem32.ngt |
โข ( ๐ โ ( ( ๐ ยท ๐ ) + ( ๐ โ 1 ) ) < ๐ ) |
8 |
|
etransclem32.h |
โข ๐ป = ( ๐ โ ( 0 ... ๐ ) โฆ ( ๐ฅ โ ๐ โฆ ( ( ๐ฅ โ ๐ ) โ if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) ) ) ) |
9 |
|
etransclem11 |
โข ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) = ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) |
10 |
1 2 3 4 5 6 8 9
|
etransclem30 |
โข ( ๐ โ ( ( ๐ D๐ ๐น ) โ ๐ ) = ( ๐ฅ โ ๐ โฆ ฮฃ ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) ( ( ( ! โ ๐ ) / โ ๐ โ ( 0 ... ๐ ) ( ! โ ( ๐ โ ๐ ) ) ) ยท โ ๐ โ ( 0 ... ๐ ) ( ( ( ๐ D๐ ( ๐ป โ ๐ ) ) โ ( ๐ โ ๐ ) ) โ ๐ฅ ) ) ) ) |
11 |
|
simpr |
โข ( ( ๐ โง ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) ) โ ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) ) |
12 |
9 6
|
etransclem12 |
โข ( ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) = { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) |
13 |
12
|
adantr |
โข ( ( ๐ โง ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) ) โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) = { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) |
14 |
11 13
|
eleqtrd |
โข ( ( ๐ โง ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) ) โ ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) |
15 |
14
|
adantlr |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) ) โ ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) |
16 |
|
nfv |
โข โฒ ๐ ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) |
17 |
|
nfre1 |
โข โฒ ๐ โ ๐ โ ( 0 ... ๐ ) if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) |
18 |
17
|
nfn |
โข โฒ ๐ ยฌ โ ๐ โ ( 0 ... ๐ ) if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) |
19 |
16 18
|
nfan |
โข โฒ ๐ ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ยฌ โ ๐ โ ( 0 ... ๐ ) if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) |
20 |
|
fzssre |
โข ( 0 ... ๐ ) โ โ |
21 |
|
rabid |
โข ( ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } โ ( ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โง ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ ) ) |
22 |
21
|
simplbi |
โข ( ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } โ ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) ) |
23 |
|
elmapi |
โข ( ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โ ๐ : ( 0 ... ๐ ) โถ ( 0 ... ๐ ) ) |
24 |
22 23
|
syl |
โข ( ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } โ ๐ : ( 0 ... ๐ ) โถ ( 0 ... ๐ ) ) |
25 |
24
|
adantl |
โข ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ : ( 0 ... ๐ ) โถ ( 0 ... ๐ ) ) |
26 |
25
|
ffvelcdmda |
โข ( ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) ) โ ( ๐ โ ๐ ) โ ( 0 ... ๐ ) ) |
27 |
20 26
|
sselid |
โข ( ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) ) โ ( ๐ โ ๐ ) โ โ ) |
28 |
27
|
adantlr |
โข ( ( ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ยฌ โ ๐ โ ( 0 ... ๐ ) if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) โง ๐ โ ( 0 ... ๐ ) ) โ ( ๐ โ ๐ ) โ โ ) |
29 |
|
nnm1nn0 |
โข ( ๐ โ โ โ ( ๐ โ 1 ) โ โ0 ) |
30 |
3 29
|
syl |
โข ( ๐ โ ( ๐ โ 1 ) โ โ0 ) |
31 |
30
|
nn0red |
โข ( ๐ โ ( ๐ โ 1 ) โ โ ) |
32 |
3
|
nnred |
โข ( ๐ โ ๐ โ โ ) |
33 |
31 32
|
ifcld |
โข ( ๐ โ if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) โ โ ) |
34 |
33
|
ad3antrrr |
โข ( ( ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ยฌ โ ๐ โ ( 0 ... ๐ ) if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) โง ๐ โ ( 0 ... ๐ ) ) โ if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) โ โ ) |
35 |
|
ralnex |
โข ( โ ๐ โ ( 0 ... ๐ ) ยฌ if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) โ ยฌ โ ๐ โ ( 0 ... ๐ ) if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) |
36 |
35
|
biimpri |
โข ( ยฌ โ ๐ โ ( 0 ... ๐ ) if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) โ โ ๐ โ ( 0 ... ๐ ) ยฌ if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) |
37 |
36
|
r19.21bi |
โข ( ( ยฌ โ ๐ โ ( 0 ... ๐ ) if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) โง ๐ โ ( 0 ... ๐ ) ) โ ยฌ if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) |
38 |
37
|
adantll |
โข ( ( ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ยฌ โ ๐ โ ( 0 ... ๐ ) if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) โง ๐ โ ( 0 ... ๐ ) ) โ ยฌ if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) |
39 |
28 34 38
|
nltled |
โข ( ( ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ยฌ โ ๐ โ ( 0 ... ๐ ) if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) โง ๐ โ ( 0 ... ๐ ) ) โ ( ๐ โ ๐ ) โค if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) ) |
40 |
39
|
ex |
โข ( ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ยฌ โ ๐ โ ( 0 ... ๐ ) if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) โ ( ๐ โ ( 0 ... ๐ ) โ ( ๐ โ ๐ ) โค if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) ) ) |
41 |
19 40
|
ralrimi |
โข ( ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ยฌ โ ๐ โ ( 0 ... ๐ ) if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) โ โ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) โค if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) ) |
42 |
21
|
simprbi |
โข ( ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } โ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ ) |
43 |
|
fveq2 |
โข ( ๐ = ๐ โ ( ๐ โ ๐ ) = ( ๐ โ ๐ ) ) |
44 |
43
|
cbvsumv |
โข ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) |
45 |
42 44
|
eqtr3di |
โข ( ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } โ ๐ = ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) ) |
46 |
45
|
ad2antlr |
โข ( ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง โ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) โค if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) ) โ ๐ = ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) ) |
47 |
|
fveq2 |
โข ( ๐ = โ โ ( ๐ โ ๐ ) = ( ๐ โ โ ) ) |
48 |
47
|
cbvsumv |
โข ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ฮฃ โ โ ( 0 ... ๐ ) ( ๐ โ โ ) |
49 |
|
fzfid |
โข ( ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง โ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) โค if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) ) โ ( 0 ... ๐ ) โ Fin ) |
50 |
25
|
ffvelcdmda |
โข ( ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง โ โ ( 0 ... ๐ ) ) โ ( ๐ โ โ ) โ ( 0 ... ๐ ) ) |
51 |
20 50
|
sselid |
โข ( ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง โ โ ( 0 ... ๐ ) ) โ ( ๐ โ โ ) โ โ ) |
52 |
51
|
adantlr |
โข ( ( ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง โ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) โค if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) ) โง โ โ ( 0 ... ๐ ) ) โ ( ๐ โ โ ) โ โ ) |
53 |
31 32
|
ifcld |
โข ( ๐ โ if ( โ = 0 , ( ๐ โ 1 ) , ๐ ) โ โ ) |
54 |
53
|
ad3antrrr |
โข ( ( ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง โ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) โค if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) ) โง โ โ ( 0 ... ๐ ) ) โ if ( โ = 0 , ( ๐ โ 1 ) , ๐ ) โ โ ) |
55 |
|
eqeq1 |
โข ( ๐ = โ โ ( ๐ = 0 โ โ = 0 ) ) |
56 |
55
|
ifbid |
โข ( ๐ = โ โ if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) = if ( โ = 0 , ( ๐ โ 1 ) , ๐ ) ) |
57 |
47 56
|
breq12d |
โข ( ๐ = โ โ ( ( ๐ โ ๐ ) โค if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) โ ( ๐ โ โ ) โค if ( โ = 0 , ( ๐ โ 1 ) , ๐ ) ) ) |
58 |
57
|
rspccva |
โข ( ( โ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) โค if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) โง โ โ ( 0 ... ๐ ) ) โ ( ๐ โ โ ) โค if ( โ = 0 , ( ๐ โ 1 ) , ๐ ) ) |
59 |
58
|
adantll |
โข ( ( ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง โ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) โค if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) ) โง โ โ ( 0 ... ๐ ) ) โ ( ๐ โ โ ) โค if ( โ = 0 , ( ๐ โ 1 ) , ๐ ) ) |
60 |
49 52 54 59
|
fsumle |
โข ( ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง โ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) โค if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) ) โ ฮฃ โ โ ( 0 ... ๐ ) ( ๐ โ โ ) โค ฮฃ โ โ ( 0 ... ๐ ) if ( โ = 0 , ( ๐ โ 1 ) , ๐ ) ) |
61 |
|
nn0uz |
โข โ0 = ( โคโฅ โ 0 ) |
62 |
4 61
|
eleqtrdi |
โข ( ๐ โ ๐ โ ( โคโฅ โ 0 ) ) |
63 |
3
|
nnnn0d |
โข ( ๐ โ ๐ โ โ0 ) |
64 |
30 63
|
ifcld |
โข ( ๐ โ if ( โ = 0 , ( ๐ โ 1 ) , ๐ ) โ โ0 ) |
65 |
64
|
adantr |
โข ( ( ๐ โง โ โ ( 0 ... ๐ ) ) โ if ( โ = 0 , ( ๐ โ 1 ) , ๐ ) โ โ0 ) |
66 |
65
|
nn0cnd |
โข ( ( ๐ โง โ โ ( 0 ... ๐ ) ) โ if ( โ = 0 , ( ๐ โ 1 ) , ๐ ) โ โ ) |
67 |
|
iftrue |
โข ( โ = 0 โ if ( โ = 0 , ( ๐ โ 1 ) , ๐ ) = ( ๐ โ 1 ) ) |
68 |
62 66 67
|
fsum1p |
โข ( ๐ โ ฮฃ โ โ ( 0 ... ๐ ) if ( โ = 0 , ( ๐ โ 1 ) , ๐ ) = ( ( ๐ โ 1 ) + ฮฃ โ โ ( ( 0 + 1 ) ... ๐ ) if ( โ = 0 , ( ๐ โ 1 ) , ๐ ) ) ) |
69 |
|
0p1e1 |
โข ( 0 + 1 ) = 1 |
70 |
69
|
oveq1i |
โข ( ( 0 + 1 ) ... ๐ ) = ( 1 ... ๐ ) |
71 |
70
|
a1i |
โข ( ๐ โ ( ( 0 + 1 ) ... ๐ ) = ( 1 ... ๐ ) ) |
72 |
71
|
sumeq1d |
โข ( ๐ โ ฮฃ โ โ ( ( 0 + 1 ) ... ๐ ) if ( โ = 0 , ( ๐ โ 1 ) , ๐ ) = ฮฃ โ โ ( 1 ... ๐ ) if ( โ = 0 , ( ๐ โ 1 ) , ๐ ) ) |
73 |
|
0red |
โข ( โ โ ( 1 ... ๐ ) โ 0 โ โ ) |
74 |
|
1red |
โข ( โ โ ( 1 ... ๐ ) โ 1 โ โ ) |
75 |
|
elfzelz |
โข ( โ โ ( 1 ... ๐ ) โ โ โ โค ) |
76 |
75
|
zred |
โข ( โ โ ( 1 ... ๐ ) โ โ โ โ ) |
77 |
|
0lt1 |
โข 0 < 1 |
78 |
77
|
a1i |
โข ( โ โ ( 1 ... ๐ ) โ 0 < 1 ) |
79 |
|
elfzle1 |
โข ( โ โ ( 1 ... ๐ ) โ 1 โค โ ) |
80 |
73 74 76 78 79
|
ltletrd |
โข ( โ โ ( 1 ... ๐ ) โ 0 < โ ) |
81 |
80
|
gt0ne0d |
โข ( โ โ ( 1 ... ๐ ) โ โ โ 0 ) |
82 |
81
|
neneqd |
โข ( โ โ ( 1 ... ๐ ) โ ยฌ โ = 0 ) |
83 |
82
|
iffalsed |
โข ( โ โ ( 1 ... ๐ ) โ if ( โ = 0 , ( ๐ โ 1 ) , ๐ ) = ๐ ) |
84 |
83
|
adantl |
โข ( ( ๐ โง โ โ ( 1 ... ๐ ) ) โ if ( โ = 0 , ( ๐ โ 1 ) , ๐ ) = ๐ ) |
85 |
84
|
sumeq2dv |
โข ( ๐ โ ฮฃ โ โ ( 1 ... ๐ ) if ( โ = 0 , ( ๐ โ 1 ) , ๐ ) = ฮฃ โ โ ( 1 ... ๐ ) ๐ ) |
86 |
|
fzfid |
โข ( ๐ โ ( 1 ... ๐ ) โ Fin ) |
87 |
3
|
nncnd |
โข ( ๐ โ ๐ โ โ ) |
88 |
|
fsumconst |
โข ( ( ( 1 ... ๐ ) โ Fin โง ๐ โ โ ) โ ฮฃ โ โ ( 1 ... ๐ ) ๐ = ( ( โฏ โ ( 1 ... ๐ ) ) ยท ๐ ) ) |
89 |
86 87 88
|
syl2anc |
โข ( ๐ โ ฮฃ โ โ ( 1 ... ๐ ) ๐ = ( ( โฏ โ ( 1 ... ๐ ) ) ยท ๐ ) ) |
90 |
|
hashfz1 |
โข ( ๐ โ โ0 โ ( โฏ โ ( 1 ... ๐ ) ) = ๐ ) |
91 |
4 90
|
syl |
โข ( ๐ โ ( โฏ โ ( 1 ... ๐ ) ) = ๐ ) |
92 |
91
|
oveq1d |
โข ( ๐ โ ( ( โฏ โ ( 1 ... ๐ ) ) ยท ๐ ) = ( ๐ ยท ๐ ) ) |
93 |
89 92
|
eqtrd |
โข ( ๐ โ ฮฃ โ โ ( 1 ... ๐ ) ๐ = ( ๐ ยท ๐ ) ) |
94 |
72 85 93
|
3eqtrd |
โข ( ๐ โ ฮฃ โ โ ( ( 0 + 1 ) ... ๐ ) if ( โ = 0 , ( ๐ โ 1 ) , ๐ ) = ( ๐ ยท ๐ ) ) |
95 |
94
|
oveq2d |
โข ( ๐ โ ( ( ๐ โ 1 ) + ฮฃ โ โ ( ( 0 + 1 ) ... ๐ ) if ( โ = 0 , ( ๐ โ 1 ) , ๐ ) ) = ( ( ๐ โ 1 ) + ( ๐ ยท ๐ ) ) ) |
96 |
30
|
nn0cnd |
โข ( ๐ โ ( ๐ โ 1 ) โ โ ) |
97 |
4 63
|
nn0mulcld |
โข ( ๐ โ ( ๐ ยท ๐ ) โ โ0 ) |
98 |
97
|
nn0cnd |
โข ( ๐ โ ( ๐ ยท ๐ ) โ โ ) |
99 |
96 98
|
addcomd |
โข ( ๐ โ ( ( ๐ โ 1 ) + ( ๐ ยท ๐ ) ) = ( ( ๐ ยท ๐ ) + ( ๐ โ 1 ) ) ) |
100 |
68 95 99
|
3eqtrd |
โข ( ๐ โ ฮฃ โ โ ( 0 ... ๐ ) if ( โ = 0 , ( ๐ โ 1 ) , ๐ ) = ( ( ๐ ยท ๐ ) + ( ๐ โ 1 ) ) ) |
101 |
100
|
ad2antrr |
โข ( ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง โ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) โค if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) ) โ ฮฃ โ โ ( 0 ... ๐ ) if ( โ = 0 , ( ๐ โ 1 ) , ๐ ) = ( ( ๐ ยท ๐ ) + ( ๐ โ 1 ) ) ) |
102 |
60 101
|
breqtrd |
โข ( ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง โ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) โค if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) ) โ ฮฃ โ โ ( 0 ... ๐ ) ( ๐ โ โ ) โค ( ( ๐ ยท ๐ ) + ( ๐ โ 1 ) ) ) |
103 |
48 102
|
eqbrtrid |
โข ( ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง โ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) โค if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) ) โ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) โค ( ( ๐ ยท ๐ ) + ( ๐ โ 1 ) ) ) |
104 |
46 103
|
eqbrtrd |
โข ( ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง โ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) โค if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) ) โ ๐ โค ( ( ๐ ยท ๐ ) + ( ๐ โ 1 ) ) ) |
105 |
41 104
|
syldan |
โข ( ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ยฌ โ ๐ โ ( 0 ... ๐ ) if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) โ ๐ โค ( ( ๐ ยท ๐ ) + ( ๐ โ 1 ) ) ) |
106 |
97 30
|
nn0addcld |
โข ( ๐ โ ( ( ๐ ยท ๐ ) + ( ๐ โ 1 ) ) โ โ0 ) |
107 |
106
|
nn0red |
โข ( ๐ โ ( ( ๐ ยท ๐ ) + ( ๐ โ 1 ) ) โ โ ) |
108 |
6
|
nn0red |
โข ( ๐ โ ๐ โ โ ) |
109 |
107 108
|
ltnled |
โข ( ๐ โ ( ( ( ๐ ยท ๐ ) + ( ๐ โ 1 ) ) < ๐ โ ยฌ ๐ โค ( ( ๐ ยท ๐ ) + ( ๐ โ 1 ) ) ) ) |
110 |
7 109
|
mpbid |
โข ( ๐ โ ยฌ ๐ โค ( ( ๐ ยท ๐ ) + ( ๐ โ 1 ) ) ) |
111 |
110
|
ad2antrr |
โข ( ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ยฌ โ ๐ โ ( 0 ... ๐ ) if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) โ ยฌ ๐ โค ( ( ๐ ยท ๐ ) + ( ๐ โ 1 ) ) ) |
112 |
105 111
|
condan |
โข ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ โ ๐ โ ( 0 ... ๐ ) if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) |
113 |
112
|
adantlr |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ โ ๐ โ ( 0 ... ๐ ) if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) |
114 |
|
nfv |
โข โฒ ๐ ( ๐ โง ๐ฅ โ ๐ ) |
115 |
|
nfcv |
โข โฒ ๐ ( 0 ... ๐ ) |
116 |
115
|
nfsum1 |
โข โฒ ๐ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) |
117 |
116
|
nfeq1 |
โข โฒ ๐ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ |
118 |
|
nfcv |
โข โฒ ๐ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) |
119 |
117 118
|
nfrabw |
โข โฒ ๐ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } |
120 |
119
|
nfcri |
โข โฒ ๐ ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } |
121 |
114 120
|
nfan |
โข โฒ ๐ ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) |
122 |
|
nfv |
โข โฒ ๐ ๐ โ ( 0 ... ๐ ) |
123 |
|
nfv |
โข โฒ ๐ if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) |
124 |
121 122 123
|
nf3an |
โข โฒ ๐ ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) โง if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) |
125 |
|
nfcv |
โข โฒ ๐ ( ( ( ๐ D๐ ( ๐ป โ ๐ ) ) โ ( ๐ โ ๐ ) ) โ ๐ฅ ) |
126 |
|
fzfid |
โข ( ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) โง if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) โ ( 0 ... ๐ ) โ Fin ) |
127 |
1
|
ad3antrrr |
โข ( ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) ) โ ๐ โ { โ , โ } ) |
128 |
2
|
ad3antrrr |
โข ( ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) ) โ ๐ โ ( ( TopOpen โ โfld ) โพt ๐ ) ) |
129 |
3
|
ad3antrrr |
โข ( ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) ) โ ๐ โ โ ) |
130 |
|
etransclem5 |
โข ( ๐ โ ( 0 ... ๐ ) โฆ ( ๐ฅ โ ๐ โฆ ( ( ๐ฅ โ ๐ ) โ if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) ) ) ) = ( ๐ โ ( 0 ... ๐ ) โฆ ( ๐ฆ โ ๐ โฆ ( ( ๐ฆ โ ๐ ) โ if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) ) ) ) |
131 |
8 130
|
eqtri |
โข ๐ป = ( ๐ โ ( 0 ... ๐ ) โฆ ( ๐ฆ โ ๐ โฆ ( ( ๐ฆ โ ๐ ) โ if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) ) ) ) |
132 |
|
simpr |
โข ( ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) ) โ ๐ โ ( 0 ... ๐ ) ) |
133 |
24
|
ad2antlr |
โข ( ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) ) โ ๐ : ( 0 ... ๐ ) โถ ( 0 ... ๐ ) ) |
134 |
|
simpr |
โข ( ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) ) โ ๐ โ ( 0 ... ๐ ) ) |
135 |
133 134
|
ffvelcdmd |
โข ( ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) ) โ ( ๐ โ ๐ ) โ ( 0 ... ๐ ) ) |
136 |
135
|
adantllr |
โข ( ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) ) โ ( ๐ โ ๐ ) โ ( 0 ... ๐ ) ) |
137 |
|
elfznn0 |
โข ( ( ๐ โ ๐ ) โ ( 0 ... ๐ ) โ ( ๐ โ ๐ ) โ โ0 ) |
138 |
136 137
|
syl |
โข ( ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) ) โ ( ๐ โ ๐ ) โ โ0 ) |
139 |
127 128 129 131 132 138
|
etransclem20 |
โข ( ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) ) โ ( ( ๐ D๐ ( ๐ป โ ๐ ) ) โ ( ๐ โ ๐ ) ) : ๐ โถ โ ) |
140 |
|
simpllr |
โข ( ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) ) โ ๐ฅ โ ๐ ) |
141 |
139 140
|
ffvelcdmd |
โข ( ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) ) โ ( ( ( ๐ D๐ ( ๐ป โ ๐ ) ) โ ( ๐ โ ๐ ) ) โ ๐ฅ ) โ โ ) |
142 |
141
|
3ad2antl1 |
โข ( ( ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) โง if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) โง ๐ โ ( 0 ... ๐ ) ) โ ( ( ( ๐ D๐ ( ๐ป โ ๐ ) ) โ ( ๐ โ ๐ ) ) โ ๐ฅ ) โ โ ) |
143 |
|
fveq2 |
โข ( ๐ = ๐ โ ( ๐ป โ ๐ ) = ( ๐ป โ ๐ ) ) |
144 |
143
|
oveq2d |
โข ( ๐ = ๐ โ ( ๐ D๐ ( ๐ป โ ๐ ) ) = ( ๐ D๐ ( ๐ป โ ๐ ) ) ) |
145 |
144 43
|
fveq12d |
โข ( ๐ = ๐ โ ( ( ๐ D๐ ( ๐ป โ ๐ ) ) โ ( ๐ โ ๐ ) ) = ( ( ๐ D๐ ( ๐ป โ ๐ ) ) โ ( ๐ โ ๐ ) ) ) |
146 |
145
|
fveq1d |
โข ( ๐ = ๐ โ ( ( ( ๐ D๐ ( ๐ป โ ๐ ) ) โ ( ๐ โ ๐ ) ) โ ๐ฅ ) = ( ( ( ๐ D๐ ( ๐ป โ ๐ ) ) โ ( ๐ โ ๐ ) ) โ ๐ฅ ) ) |
147 |
|
simp2 |
โข ( ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) โง if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) โ ๐ โ ( 0 ... ๐ ) ) |
148 |
1
|
ad2antrr |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ โ { โ , โ } ) |
149 |
148
|
3ad2ant1 |
โข ( ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) โง if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) โ ๐ โ { โ , โ } ) |
150 |
2
|
ad2antrr |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ โ ( ( TopOpen โ โfld ) โพt ๐ ) ) |
151 |
150
|
3ad2ant1 |
โข ( ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) โง if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) โ ๐ โ ( ( TopOpen โ โfld ) โพt ๐ ) ) |
152 |
3
|
ad2antrr |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ โ โ ) |
153 |
152
|
3ad2ant1 |
โข ( ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) โง if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) โ ๐ โ โ ) |
154 |
|
etransclem5 |
โข ( ๐ โ ( 0 ... ๐ ) โฆ ( ๐ฅ โ ๐ โฆ ( ( ๐ฅ โ ๐ ) โ if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) ) ) ) = ( โ โ ( 0 ... ๐ ) โฆ ( ๐ฆ โ ๐ โฆ ( ( ๐ฆ โ โ ) โ if ( โ = 0 , ( ๐ โ 1 ) , ๐ ) ) ) ) |
155 |
8 154
|
eqtri |
โข ๐ป = ( โ โ ( 0 ... ๐ ) โฆ ( ๐ฆ โ ๐ โฆ ( ( ๐ฆ โ โ ) โ if ( โ = 0 , ( ๐ โ 1 ) , ๐ ) ) ) ) |
156 |
26
|
elfzelzd |
โข ( ( ( ๐ โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) ) โ ( ๐ โ ๐ ) โ โค ) |
157 |
156
|
adantllr |
โข ( ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) ) โ ( ๐ โ ๐ ) โ โค ) |
158 |
157
|
3adant3 |
โข ( ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) โง if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) โ ( ๐ โ ๐ ) โ โค ) |
159 |
|
simp3 |
โข ( ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) โง if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) โ if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) |
160 |
149 151 153 155 147 158 159
|
etransclem19 |
โข ( ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) โง if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) โ ( ( ๐ D๐ ( ๐ป โ ๐ ) ) โ ( ๐ โ ๐ ) ) = ( ๐ฆ โ ๐ โฆ 0 ) ) |
161 |
|
eqidd |
โข ( ( ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) โง if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) โง ๐ฆ = ๐ฅ ) โ 0 = 0 ) |
162 |
|
simp1lr |
โข ( ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) โง if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) โ ๐ฅ โ ๐ ) |
163 |
|
0red |
โข ( ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) โง if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) โ 0 โ โ ) |
164 |
160 161 162 163
|
fvmptd |
โข ( ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) โง if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) โ ( ( ( ๐ D๐ ( ๐ป โ ๐ ) ) โ ( ๐ โ ๐ ) ) โ ๐ฅ ) = 0 ) |
165 |
124 125 126 142 146 147 164
|
fprod0 |
โข ( ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โง ๐ โ ( 0 ... ๐ ) โง if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) ) โ โ ๐ โ ( 0 ... ๐ ) ( ( ( ๐ D๐ ( ๐ป โ ๐ ) ) โ ( ๐ โ ๐ ) ) โ ๐ฅ ) = 0 ) |
166 |
165
|
rexlimdv3a |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ( โ ๐ โ ( 0 ... ๐ ) if ( ๐ = 0 , ( ๐ โ 1 ) , ๐ ) < ( ๐ โ ๐ ) โ โ ๐ โ ( 0 ... ๐ ) ( ( ( ๐ D๐ ( ๐ป โ ๐ ) ) โ ( ๐ โ ๐ ) ) โ ๐ฅ ) = 0 ) ) |
167 |
113 166
|
mpd |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ โ ๐ โ ( 0 ... ๐ ) ( ( ( ๐ D๐ ( ๐ป โ ๐ ) ) โ ( ๐ โ ๐ ) ) โ ๐ฅ ) = 0 ) |
168 |
15 167
|
syldan |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) ) โ โ ๐ โ ( 0 ... ๐ ) ( ( ( ๐ D๐ ( ๐ป โ ๐ ) ) โ ( ๐ โ ๐ ) ) โ ๐ฅ ) = 0 ) |
169 |
168
|
oveq2d |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) ) โ ( ( ( ! โ ๐ ) / โ ๐ โ ( 0 ... ๐ ) ( ! โ ( ๐ โ ๐ ) ) ) ยท โ ๐ โ ( 0 ... ๐ ) ( ( ( ๐ D๐ ( ๐ป โ ๐ ) ) โ ( ๐ โ ๐ ) ) โ ๐ฅ ) ) = ( ( ( ! โ ๐ ) / โ ๐ โ ( 0 ... ๐ ) ( ! โ ( ๐ โ ๐ ) ) ) ยท 0 ) ) |
170 |
6
|
faccld |
โข ( ๐ โ ( ! โ ๐ ) โ โ ) |
171 |
170
|
nncnd |
โข ( ๐ โ ( ! โ ๐ ) โ โ ) |
172 |
171
|
adantr |
โข ( ( ๐ โง ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) ) โ ( ! โ ๐ ) โ โ ) |
173 |
|
fzfid |
โข ( ( ๐ โง ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) ) โ ( 0 ... ๐ ) โ Fin ) |
174 |
|
simpll |
โข ( ( ( ๐ โง ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) ) โง ๐ โ ( 0 ... ๐ ) ) โ ๐ ) |
175 |
14
|
adantr |
โข ( ( ( ๐ โง ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) ) โง ๐ โ ( 0 ... ๐ ) ) โ ๐ โ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) |
176 |
|
simpr |
โข ( ( ( ๐ โง ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) ) โง ๐ โ ( 0 ... ๐ ) ) โ ๐ โ ( 0 ... ๐ ) ) |
177 |
174 175 176 135
|
syl21anc |
โข ( ( ( ๐ โง ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) ) โง ๐ โ ( 0 ... ๐ ) ) โ ( ๐ โ ๐ ) โ ( 0 ... ๐ ) ) |
178 |
177 137
|
syl |
โข ( ( ( ๐ โง ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) ) โง ๐ โ ( 0 ... ๐ ) ) โ ( ๐ โ ๐ ) โ โ0 ) |
179 |
178
|
faccld |
โข ( ( ( ๐ โง ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) ) โง ๐ โ ( 0 ... ๐ ) ) โ ( ! โ ( ๐ โ ๐ ) ) โ โ ) |
180 |
179
|
nncnd |
โข ( ( ( ๐ โง ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) ) โง ๐ โ ( 0 ... ๐ ) ) โ ( ! โ ( ๐ โ ๐ ) ) โ โ ) |
181 |
173 180
|
fprodcl |
โข ( ( ๐ โง ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) ) โ โ ๐ โ ( 0 ... ๐ ) ( ! โ ( ๐ โ ๐ ) ) โ โ ) |
182 |
179
|
nnne0d |
โข ( ( ( ๐ โง ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) ) โง ๐ โ ( 0 ... ๐ ) ) โ ( ! โ ( ๐ โ ๐ ) ) โ 0 ) |
183 |
173 180 182
|
fprodn0 |
โข ( ( ๐ โง ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) ) โ โ ๐ โ ( 0 ... ๐ ) ( ! โ ( ๐ โ ๐ ) ) โ 0 ) |
184 |
172 181 183
|
divcld |
โข ( ( ๐ โง ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) ) โ ( ( ! โ ๐ ) / โ ๐ โ ( 0 ... ๐ ) ( ! โ ( ๐ โ ๐ ) ) ) โ โ ) |
185 |
184
|
mul01d |
โข ( ( ๐ โง ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) ) โ ( ( ( ! โ ๐ ) / โ ๐ โ ( 0 ... ๐ ) ( ! โ ( ๐ โ ๐ ) ) ) ยท 0 ) = 0 ) |
186 |
185
|
adantlr |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) ) โ ( ( ( ! โ ๐ ) / โ ๐ โ ( 0 ... ๐ ) ( ! โ ( ๐ โ ๐ ) ) ) ยท 0 ) = 0 ) |
187 |
169 186
|
eqtrd |
โข ( ( ( ๐ โง ๐ฅ โ ๐ ) โง ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) ) โ ( ( ( ! โ ๐ ) / โ ๐ โ ( 0 ... ๐ ) ( ! โ ( ๐ โ ๐ ) ) ) ยท โ ๐ โ ( 0 ... ๐ ) ( ( ( ๐ D๐ ( ๐ป โ ๐ ) ) โ ( ๐ โ ๐ ) ) โ ๐ฅ ) ) = 0 ) |
188 |
187
|
sumeq2dv |
โข ( ( ๐ โง ๐ฅ โ ๐ ) โ ฮฃ ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) ( ( ( ! โ ๐ ) / โ ๐ โ ( 0 ... ๐ ) ( ! โ ( ๐ โ ๐ ) ) ) ยท โ ๐ โ ( 0 ... ๐ ) ( ( ( ๐ D๐ ( ๐ป โ ๐ ) ) โ ( ๐ โ ๐ ) ) โ ๐ฅ ) ) = ฮฃ ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) 0 ) |
189 |
|
eqid |
โข ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) = ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) |
190 |
189 6
|
etransclem16 |
โข ( ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) โ Fin ) |
191 |
190
|
olcd |
โข ( ๐ โ ( ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) โ ( โคโฅ โ ๐ด ) โจ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) โ Fin ) ) |
192 |
191
|
adantr |
โข ( ( ๐ โง ๐ฅ โ ๐ ) โ ( ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) โ ( โคโฅ โ ๐ด ) โจ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) โ Fin ) ) |
193 |
|
sumz |
โข ( ( ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) โ ( โคโฅ โ ๐ด ) โจ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) โ Fin ) โ ฮฃ ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) 0 = 0 ) |
194 |
192 193
|
syl |
โข ( ( ๐ โง ๐ฅ โ ๐ ) โ ฮฃ ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) 0 = 0 ) |
195 |
188 194
|
eqtrd |
โข ( ( ๐ โง ๐ฅ โ ๐ ) โ ฮฃ ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) ( ( ( ! โ ๐ ) / โ ๐ โ ( 0 ... ๐ ) ( ! โ ( ๐ โ ๐ ) ) ) ยท โ ๐ โ ( 0 ... ๐ ) ( ( ( ๐ D๐ ( ๐ป โ ๐ ) ) โ ( ๐ โ ๐ ) ) โ ๐ฅ ) ) = 0 ) |
196 |
195
|
mpteq2dva |
โข ( ๐ โ ( ๐ฅ โ ๐ โฆ ฮฃ ๐ โ ( ( ๐ โ โ0 โฆ { ๐ โ ( ( 0 ... ๐ ) โm ( 0 ... ๐ ) ) โฃ ฮฃ ๐ โ ( 0 ... ๐ ) ( ๐ โ ๐ ) = ๐ } ) โ ๐ ) ( ( ( ! โ ๐ ) / โ ๐ โ ( 0 ... ๐ ) ( ! โ ( ๐ โ ๐ ) ) ) ยท โ ๐ โ ( 0 ... ๐ ) ( ( ( ๐ D๐ ( ๐ป โ ๐ ) ) โ ( ๐ โ ๐ ) ) โ ๐ฅ ) ) ) = ( ๐ฅ โ ๐ โฆ 0 ) ) |
197 |
10 196
|
eqtrd |
โข ( ๐ โ ( ( ๐ D๐ ๐น ) โ ๐ ) = ( ๐ฅ โ ๐ โฆ 0 ) ) |