Step |
Hyp |
Ref |
Expression |
1 |
|
etransclem22.s |
|- ( ph -> S e. { RR , CC } ) |
2 |
|
etransclem22.x |
|- ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) ) |
3 |
|
etransclem22.p |
|- ( ph -> P e. NN ) |
4 |
|
etransclem22.h |
|- H = ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) ) |
5 |
|
etransclem22.J |
|- ( ph -> J e. ( 0 ... M ) ) |
6 |
|
etransclem22.n |
|- ( ph -> N e. NN0 ) |
7 |
1 2 3 4 5 6
|
etransclem17 |
|- ( ph -> ( ( S Dn ( H ` J ) ) ` N ) = ( x e. X |-> if ( if ( J = 0 , ( P - 1 ) , P ) < N , 0 , ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) ) ) |
8 |
|
simpr |
|- ( ( ph /\ if ( J = 0 , ( P - 1 ) , P ) < N ) -> if ( J = 0 , ( P - 1 ) , P ) < N ) |
9 |
8
|
iftrued |
|- ( ( ph /\ if ( J = 0 , ( P - 1 ) , P ) < N ) -> if ( if ( J = 0 , ( P - 1 ) , P ) < N , 0 , ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) = 0 ) |
10 |
9
|
mpteq2dv |
|- ( ( ph /\ if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( x e. X |-> if ( if ( J = 0 , ( P - 1 ) , P ) < N , 0 , ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) ) = ( x e. X |-> 0 ) ) |
11 |
1 2
|
dvdmsscn |
|- ( ph -> X C_ CC ) |
12 |
|
0cnd |
|- ( ph -> 0 e. CC ) |
13 |
|
ssid |
|- CC C_ CC |
14 |
13
|
a1i |
|- ( ph -> CC C_ CC ) |
15 |
11 12 14
|
constcncfg |
|- ( ph -> ( x e. X |-> 0 ) e. ( X -cn-> CC ) ) |
16 |
15
|
adantr |
|- ( ( ph /\ if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( x e. X |-> 0 ) e. ( X -cn-> CC ) ) |
17 |
10 16
|
eqeltrd |
|- ( ( ph /\ if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( x e. X |-> if ( if ( J = 0 , ( P - 1 ) , P ) < N , 0 , ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) ) e. ( X -cn-> CC ) ) |
18 |
|
simpr |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> -. if ( J = 0 , ( P - 1 ) , P ) < N ) |
19 |
18
|
iffalsed |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> if ( if ( J = 0 , ( P - 1 ) , P ) < N , 0 , ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) = ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) |
20 |
19
|
mpteq2dv |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( x e. X |-> if ( if ( J = 0 , ( P - 1 ) , P ) < N , 0 , ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) ) = ( x e. X |-> ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) ) |
21 |
|
nfv |
|- F/ x ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) |
22 |
11 14
|
idcncfg |
|- ( ph -> ( x e. X |-> x ) e. ( X -cn-> CC ) ) |
23 |
5
|
elfzelzd |
|- ( ph -> J e. ZZ ) |
24 |
23
|
zcnd |
|- ( ph -> J e. CC ) |
25 |
11 24 14
|
constcncfg |
|- ( ph -> ( x e. X |-> J ) e. ( X -cn-> CC ) ) |
26 |
22 25
|
subcncf |
|- ( ph -> ( x e. X |-> ( x - J ) ) e. ( X -cn-> CC ) ) |
27 |
26
|
adantr |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( x e. X |-> ( x - J ) ) e. ( X -cn-> CC ) ) |
28 |
13
|
a1i |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> CC C_ CC ) |
29 |
|
nnm1nn0 |
|- ( P e. NN -> ( P - 1 ) e. NN0 ) |
30 |
3 29
|
syl |
|- ( ph -> ( P - 1 ) e. NN0 ) |
31 |
3
|
nnnn0d |
|- ( ph -> P e. NN0 ) |
32 |
30 31
|
ifcld |
|- ( ph -> if ( J = 0 , ( P - 1 ) , P ) e. NN0 ) |
33 |
32
|
faccld |
|- ( ph -> ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) e. NN ) |
34 |
33
|
nncnd |
|- ( ph -> ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) e. CC ) |
35 |
34
|
adantr |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) e. CC ) |
36 |
32
|
nn0zd |
|- ( ph -> if ( J = 0 , ( P - 1 ) , P ) e. ZZ ) |
37 |
6
|
nn0zd |
|- ( ph -> N e. ZZ ) |
38 |
36 37
|
zsubcld |
|- ( ph -> ( if ( J = 0 , ( P - 1 ) , P ) - N ) e. ZZ ) |
39 |
38
|
adantr |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( if ( J = 0 , ( P - 1 ) , P ) - N ) e. ZZ ) |
40 |
6
|
nn0red |
|- ( ph -> N e. RR ) |
41 |
40
|
adantr |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> N e. RR ) |
42 |
32
|
nn0red |
|- ( ph -> if ( J = 0 , ( P - 1 ) , P ) e. RR ) |
43 |
42
|
adantr |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> if ( J = 0 , ( P - 1 ) , P ) e. RR ) |
44 |
41 43 18
|
nltled |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> N <_ if ( J = 0 , ( P - 1 ) , P ) ) |
45 |
43 41
|
subge0d |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( 0 <_ ( if ( J = 0 , ( P - 1 ) , P ) - N ) <-> N <_ if ( J = 0 , ( P - 1 ) , P ) ) ) |
46 |
44 45
|
mpbird |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> 0 <_ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) |
47 |
|
elnn0z |
|- ( ( if ( J = 0 , ( P - 1 ) , P ) - N ) e. NN0 <-> ( ( if ( J = 0 , ( P - 1 ) , P ) - N ) e. ZZ /\ 0 <_ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) |
48 |
39 46 47
|
sylanbrc |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( if ( J = 0 , ( P - 1 ) , P ) - N ) e. NN0 ) |
49 |
48
|
faccld |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) e. NN ) |
50 |
49
|
nncnd |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) e. CC ) |
51 |
49
|
nnne0d |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) =/= 0 ) |
52 |
35 50 51
|
divcld |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) e. CC ) |
53 |
28 52 28
|
constcncfg |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( y e. CC |-> ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) e. ( CC -cn-> CC ) ) |
54 |
|
expcncf |
|- ( ( if ( J = 0 , ( P - 1 ) , P ) - N ) e. NN0 -> ( y e. CC |-> ( y ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) e. ( CC -cn-> CC ) ) |
55 |
48 54
|
syl |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( y e. CC |-> ( y ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) e. ( CC -cn-> CC ) ) |
56 |
53 55
|
mulcncf |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( y e. CC |-> ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( y ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) e. ( CC -cn-> CC ) ) |
57 |
|
oveq1 |
|- ( y = ( x - J ) -> ( y ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) = ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) |
58 |
57
|
oveq2d |
|- ( y = ( x - J ) -> ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( y ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) = ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) |
59 |
21 27 56 28 58
|
cncfcompt2 |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( x e. X |-> ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) e. ( X -cn-> CC ) ) |
60 |
20 59
|
eqeltrd |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( x e. X |-> if ( if ( J = 0 , ( P - 1 ) , P ) < N , 0 , ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) ) e. ( X -cn-> CC ) ) |
61 |
17 60
|
pm2.61dan |
|- ( ph -> ( x e. X |-> if ( if ( J = 0 , ( P - 1 ) , P ) < N , 0 , ( ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) x. ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) ) ) e. ( X -cn-> CC ) ) |
62 |
7 61
|
eqeltrd |
|- ( ph -> ( ( S Dn ( H ` J ) ) ` N ) e. ( X -cn-> CC ) ) |