Step |
Hyp |
Ref |
Expression |
1 |
|
etransclem20.s |
|- ( ph -> S e. { RR , CC } ) |
2 |
|
etransclem20.x |
|- ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) ) |
3 |
|
etransclem20.p |
|- ( ph -> P e. NN ) |
4 |
|
etransclem20.h |
|- H = ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) ) |
5 |
|
etransclem20.J |
|- ( ph -> J e. ( 0 ... M ) ) |
6 |
|
etransclem20.n |
|- ( ph -> N e. NN0 ) |
7 |
|
iftrue |
|- ( 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 ) |
8 |
|
0cnd |
|- ( if ( J = 0 , ( P - 1 ) , P ) < N -> 0 e. CC ) |
9 |
7 8
|
eqeltrd |
|- ( 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 ) ) ) ) e. CC ) |
10 |
9
|
adantl |
|- ( ( ( ph /\ x e. X ) /\ 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 ) ) ) ) e. CC ) |
11 |
|
simpr |
|- ( ( ( ph /\ x e. X ) /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> -. if ( J = 0 , ( P - 1 ) , P ) < N ) |
12 |
11
|
iffalsed |
|- ( ( ( ph /\ x e. X ) /\ -. 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 ) ) ) ) |
13 |
|
nnm1nn0 |
|- ( P e. NN -> ( P - 1 ) e. NN0 ) |
14 |
3 13
|
syl |
|- ( ph -> ( P - 1 ) e. NN0 ) |
15 |
3
|
nnnn0d |
|- ( ph -> P e. NN0 ) |
16 |
14 15
|
ifcld |
|- ( ph -> if ( J = 0 , ( P - 1 ) , P ) e. NN0 ) |
17 |
16
|
faccld |
|- ( ph -> ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) e. NN ) |
18 |
17
|
nncnd |
|- ( ph -> ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) e. CC ) |
19 |
18
|
adantr |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) e. CC ) |
20 |
16
|
nn0zd |
|- ( ph -> if ( J = 0 , ( P - 1 ) , P ) e. ZZ ) |
21 |
6
|
nn0zd |
|- ( ph -> N e. ZZ ) |
22 |
20 21
|
zsubcld |
|- ( ph -> ( if ( J = 0 , ( P - 1 ) , P ) - N ) e. ZZ ) |
23 |
22
|
adantr |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( if ( J = 0 , ( P - 1 ) , P ) - N ) e. ZZ ) |
24 |
6
|
nn0red |
|- ( ph -> N e. RR ) |
25 |
24
|
adantr |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> N e. RR ) |
26 |
16
|
nn0red |
|- ( ph -> if ( J = 0 , ( P - 1 ) , P ) e. RR ) |
27 |
26
|
adantr |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> if ( J = 0 , ( P - 1 ) , P ) e. RR ) |
28 |
|
simpr |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> -. if ( J = 0 , ( P - 1 ) , P ) < N ) |
29 |
25 27 28
|
nltled |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> N <_ if ( J = 0 , ( P - 1 ) , P ) ) |
30 |
27 25
|
subge0d |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( 0 <_ ( if ( J = 0 , ( P - 1 ) , P ) - N ) <-> N <_ if ( J = 0 , ( P - 1 ) , P ) ) ) |
31 |
29 30
|
mpbird |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> 0 <_ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) |
32 |
|
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 ) ) ) |
33 |
23 31 32
|
sylanbrc |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( if ( J = 0 , ( P - 1 ) , P ) - N ) e. NN0 ) |
34 |
33
|
faccld |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) e. NN ) |
35 |
34
|
nncnd |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) e. CC ) |
36 |
34
|
nnne0d |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) =/= 0 ) |
37 |
19 35 36
|
divcld |
|- ( ( ph /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) e. CC ) |
38 |
37
|
adantlr |
|- ( ( ( ph /\ x e. X ) /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ( ! ` if ( J = 0 , ( P - 1 ) , P ) ) / ( ! ` ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) ) e. CC ) |
39 |
1 2
|
dvdmsscn |
|- ( ph -> X C_ CC ) |
40 |
39
|
sselda |
|- ( ( ph /\ x e. X ) -> x e. CC ) |
41 |
|
elfzelz |
|- ( J e. ( 0 ... M ) -> J e. ZZ ) |
42 |
41
|
zcnd |
|- ( J e. ( 0 ... M ) -> J e. CC ) |
43 |
5 42
|
syl |
|- ( ph -> J e. CC ) |
44 |
43
|
adantr |
|- ( ( ph /\ x e. X ) -> J e. CC ) |
45 |
40 44
|
subcld |
|- ( ( ph /\ x e. X ) -> ( x - J ) e. CC ) |
46 |
45
|
adantr |
|- ( ( ( ph /\ x e. X ) /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( x - J ) e. CC ) |
47 |
33
|
adantlr |
|- ( ( ( ph /\ x e. X ) /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( if ( J = 0 , ( P - 1 ) , P ) - N ) e. NN0 ) |
48 |
46 47
|
expcld |
|- ( ( ( ph /\ x e. X ) /\ -. if ( J = 0 , ( P - 1 ) , P ) < N ) -> ( ( x - J ) ^ ( if ( J = 0 , ( P - 1 ) , P ) - N ) ) e. CC ) |
49 |
38 48
|
mulcld |
|- ( ( ( ph /\ x e. X ) /\ -. 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 ) ) ) e. CC ) |
50 |
12 49
|
eqeltrd |
|- ( ( ( ph /\ x e. X ) /\ -. 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 ) ) ) ) e. CC ) |
51 |
10 50
|
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. CC ) |
52 |
|
eqid |
|- ( 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 ( 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 ) ) ) ) ) |
53 |
51 52
|
fmptd |
|- ( 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 ) ) ) ) ) : X --> CC ) |
54 |
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 ) ) ) ) ) ) |
55 |
54
|
feq1d |
|- ( ph -> ( ( ( S Dn ( H ` J ) ) ` N ) : X --> CC <-> ( 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 --> CC ) ) |
56 |
53 55
|
mpbird |
|- ( ph -> ( ( S Dn ( H ` J ) ) ` N ) : X --> CC ) |