Metamath Proof Explorer

Theorem dvnmptdivc

Description: Function-builder for iterated derivative, division rule for constant divisor. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses dvnmptdivc.s 
|- ( ph -> S e. { RR , CC } )
dvnmptdivc.x 
|- ( ph -> X C_ S )
dvnmptdivc.a 
|- ( ( ph /\ x e. X ) -> A e. CC )
dvnmptdivc.b 
|- ( ( ph /\ x e. X /\ n e. ( 0 ... M ) ) -> B e. CC )
dvnmptdivc.dvn 
|- ( ( ph /\ n e. ( 0 ... M ) ) -> ( ( S Dn ( x e. X |-> A ) ) ` n ) = ( x e. X |-> B ) )
dvnmptdivc.c 
|- ( ph -> C e. CC )
dvnmptdivc.cne0 
|- ( ph -> C =/= 0 )
dvnmptdivc.8 
|- ( ph -> M e. NN0 )
Assertion dvnmptdivc 
|- ( ( ph /\ n e. ( 0 ... M ) ) -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` n ) = ( x e. X |-> ( B / C ) ) )

Proof

Step Hyp Ref Expression
1 dvnmptdivc.s 
 |-  ( ph -> S e. { RR , CC } )
2 dvnmptdivc.x 
 |-  ( ph -> X C_ S )
3 dvnmptdivc.a 
 |-  ( ( ph /\ x e. X ) -> A e. CC )
4 dvnmptdivc.b 
 |-  ( ( ph /\ x e. X /\ n e. ( 0 ... M ) ) -> B e. CC )
5 dvnmptdivc.dvn 
 |-  ( ( ph /\ n e. ( 0 ... M ) ) -> ( ( S Dn ( x e. X |-> A ) ) ` n ) = ( x e. X |-> B ) )
6 dvnmptdivc.c 
 |-  ( ph -> C e. CC )
7 dvnmptdivc.cne0 
 |-  ( ph -> C =/= 0 )
8 dvnmptdivc.8 
 |-  ( ph -> M e. NN0 )
9 simpr 
 |-  ( ( ph /\ n e. ( 0 ... M ) ) -> n e. ( 0 ... M ) )
10 simpl 
 |-  ( ( ph /\ n e. ( 0 ... M ) ) -> ph )
11 fveq2 
 |-  ( k = 0 -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` k ) = ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` 0 ) )
12 csbeq1 
 |-  ( k = 0 -> [_ k / n ]_ B = [_ 0 / n ]_ B )
13 12 oveq1d 
 |-  ( k = 0 -> ( [_ k / n ]_ B / C ) = ( [_ 0 / n ]_ B / C ) )
14 13 mpteq2dv 
 |-  ( k = 0 -> ( x e. X |-> ( [_ k / n ]_ B / C ) ) = ( x e. X |-> ( [_ 0 / n ]_ B / C ) ) )
15 11 14 eqeq12d 
 |-  ( k = 0 -> ( ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` k ) = ( x e. X |-> ( [_ k / n ]_ B / C ) ) <-> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` 0 ) = ( x e. X |-> ( [_ 0 / n ]_ B / C ) ) ) )
16 15 imbi2d 
 |-  ( k = 0 -> ( ( ph -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` k ) = ( x e. X |-> ( [_ k / n ]_ B / C ) ) ) <-> ( ph -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` 0 ) = ( x e. X |-> ( [_ 0 / n ]_ B / C ) ) ) ) )
17 fveq2 
 |-  ( k = j -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` k ) = ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) )
18 csbeq1 
 |-  ( k = j -> [_ k / n ]_ B = [_ j / n ]_ B )
19 18 oveq1d 
 |-  ( k = j -> ( [_ k / n ]_ B / C ) = ( [_ j / n ]_ B / C ) )
20 19 mpteq2dv 
 |-  ( k = j -> ( x e. X |-> ( [_ k / n ]_ B / C ) ) = ( x e. X |-> ( [_ j / n ]_ B / C ) ) )
21 17 20 eqeq12d 
 |-  ( k = j -> ( ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` k ) = ( x e. X |-> ( [_ k / n ]_ B / C ) ) <-> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) = ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) )
22 21 imbi2d 
 |-  ( k = j -> ( ( ph -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` k ) = ( x e. X |-> ( [_ k / n ]_ B / C ) ) ) <-> ( ph -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) = ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) ) )
23 fveq2 
 |-  ( k = ( j + 1 ) -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` k ) = ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` ( j + 1 ) ) )
24 csbeq1 
 |-  ( k = ( j + 1 ) -> [_ k / n ]_ B = [_ ( j + 1 ) / n ]_ B )
25 24 oveq1d 
 |-  ( k = ( j + 1 ) -> ( [_ k / n ]_ B / C ) = ( [_ ( j + 1 ) / n ]_ B / C ) )
26 25 mpteq2dv 
 |-  ( k = ( j + 1 ) -> ( x e. X |-> ( [_ k / n ]_ B / C ) ) = ( x e. X |-> ( [_ ( j + 1 ) / n ]_ B / C ) ) )
27 23 26 eqeq12d 
 |-  ( k = ( j + 1 ) -> ( ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` k ) = ( x e. X |-> ( [_ k / n ]_ B / C ) ) <-> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` ( j + 1 ) ) = ( x e. X |-> ( [_ ( j + 1 ) / n ]_ B / C ) ) ) )
28 27 imbi2d 
 |-  ( k = ( j + 1 ) -> ( ( ph -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` k ) = ( x e. X |-> ( [_ k / n ]_ B / C ) ) ) <-> ( ph -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` ( j + 1 ) ) = ( x e. X |-> ( [_ ( j + 1 ) / n ]_ B / C ) ) ) ) )
29 fveq2 
 |-  ( k = n -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` k ) = ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` n ) )
30 csbeq1a 
 |-  ( n = k -> B = [_ k / n ]_ B )
31 30 equcoms 
 |-  ( k = n -> B = [_ k / n ]_ B )
32 31 eqcomd 
 |-  ( k = n -> [_ k / n ]_ B = B )
33 32 oveq1d 
 |-  ( k = n -> ( [_ k / n ]_ B / C ) = ( B / C ) )
34 33 mpteq2dv 
 |-  ( k = n -> ( x e. X |-> ( [_ k / n ]_ B / C ) ) = ( x e. X |-> ( B / C ) ) )
35 29 34 eqeq12d 
 |-  ( k = n -> ( ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` k ) = ( x e. X |-> ( [_ k / n ]_ B / C ) ) <-> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` n ) = ( x e. X |-> ( B / C ) ) ) )
36 35 imbi2d 
 |-  ( k = n -> ( ( ph -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` k ) = ( x e. X |-> ( [_ k / n ]_ B / C ) ) ) <-> ( ph -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` n ) = ( x e. X |-> ( B / C ) ) ) ) )
37 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
38 1 37 syl 
 |-  ( ph -> S C_ CC )
39 cnex 
 |-  CC e. _V
40 39 a1i 
 |-  ( ph -> CC e. _V )
41 6 adantr 
 |-  ( ( ph /\ x e. X ) -> C e. CC )
42 7 adantr 
 |-  ( ( ph /\ x e. X ) -> C =/= 0 )
43 3 41 42 divcld 
 |-  ( ( ph /\ x e. X ) -> ( A / C ) e. CC )
44 43 fmpttd 
 |-  ( ph -> ( x e. X |-> ( A / C ) ) : X --> CC )
45 elpm2r 
 |-  ( ( ( CC e. _V /\ S e. { RR , CC } ) /\ ( ( x e. X |-> ( A / C ) ) : X --> CC /\ X C_ S ) ) -> ( x e. X |-> ( A / C ) ) e. ( CC ^pm S ) )
46 40 1 44 2 45 syl22anc 
 |-  ( ph -> ( x e. X |-> ( A / C ) ) e. ( CC ^pm S ) )
47 dvn0 
 |-  ( ( S C_ CC /\ ( x e. X |-> ( A / C ) ) e. ( CC ^pm S ) ) -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` 0 ) = ( x e. X |-> ( A / C ) ) )
48 38 46 47 syl2anc 
 |-  ( ph -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` 0 ) = ( x e. X |-> ( A / C ) ) )
49 id 
 |-  ( ph -> ph )
50 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
51 8 50 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 0 ) )
52 eluzfz1 
 |-  ( M e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... M ) )
53 51 52 syl 
 |-  ( ph -> 0 e. ( 0 ... M ) )
54 nfv 
 |-  F/ n ( ph /\ 0 e. ( 0 ... M ) )
55 nfcv 
 |-  F/_ n ( ( S Dn ( x e. X |-> A ) ) ` 0 )
56 nfcv 
 |-  F/_ n X
57 nfcsb1v 
 |-  F/_ n [_ 0 / n ]_ B
58 56 57 nfmpt 
 |-  F/_ n ( x e. X |-> [_ 0 / n ]_ B )
59 55 58 nfeq 
 |-  F/ n ( ( S Dn ( x e. X |-> A ) ) ` 0 ) = ( x e. X |-> [_ 0 / n ]_ B )
60 54 59 nfim 
 |-  F/ n ( ( ph /\ 0 e. ( 0 ... M ) ) -> ( ( S Dn ( x e. X |-> A ) ) ` 0 ) = ( x e. X |-> [_ 0 / n ]_ B ) )
61 c0ex 
 |-  0 e. _V
62 eleq1 
 |-  ( n = 0 -> ( n e. ( 0 ... M ) <-> 0 e. ( 0 ... M ) ) )
63 62 anbi2d 
 |-  ( n = 0 -> ( ( ph /\ n e. ( 0 ... M ) ) <-> ( ph /\ 0 e. ( 0 ... M ) ) ) )
64 fveq2 
 |-  ( n = 0 -> ( ( S Dn ( x e. X |-> A ) ) ` n ) = ( ( S Dn ( x e. X |-> A ) ) ` 0 ) )
65 csbeq1a 
 |-  ( n = 0 -> B = [_ 0 / n ]_ B )
66 65 mpteq2dv 
 |-  ( n = 0 -> ( x e. X |-> B ) = ( x e. X |-> [_ 0 / n ]_ B ) )
67 64 66 eqeq12d 
 |-  ( n = 0 -> ( ( ( S Dn ( x e. X |-> A ) ) ` n ) = ( x e. X |-> B ) <-> ( ( S Dn ( x e. X |-> A ) ) ` 0 ) = ( x e. X |-> [_ 0 / n ]_ B ) ) )
68 63 67 imbi12d 
 |-  ( n = 0 -> ( ( ( ph /\ n e. ( 0 ... M ) ) -> ( ( S Dn ( x e. X |-> A ) ) ` n ) = ( x e. X |-> B ) ) <-> ( ( ph /\ 0 e. ( 0 ... M ) ) -> ( ( S Dn ( x e. X |-> A ) ) ` 0 ) = ( x e. X |-> [_ 0 / n ]_ B ) ) ) )
69 60 61 68 5 vtoclf 
 |-  ( ( ph /\ 0 e. ( 0 ... M ) ) -> ( ( S Dn ( x e. X |-> A ) ) ` 0 ) = ( x e. X |-> [_ 0 / n ]_ B ) )
70 49 53 69 syl2anc 
 |-  ( ph -> ( ( S Dn ( x e. X |-> A ) ) ` 0 ) = ( x e. X |-> [_ 0 / n ]_ B ) )
71 70 fveq1d 
 |-  ( ph -> ( ( ( S Dn ( x e. X |-> A ) ) ` 0 ) ` x ) = ( ( x e. X |-> [_ 0 / n ]_ B ) ` x ) )
72 71 adantr 
 |-  ( ( ph /\ x e. X ) -> ( ( ( S Dn ( x e. X |-> A ) ) ` 0 ) ` x ) = ( ( x e. X |-> [_ 0 / n ]_ B ) ` x ) )
73 simpr 
 |-  ( ( ph /\ x e. X ) -> x e. X )
74 simpl 
 |-  ( ( ph /\ x e. X ) -> ph )
75 53 adantr 
 |-  ( ( ph /\ x e. X ) -> 0 e. ( 0 ... M ) )
76 0re 
 |-  0 e. RR
77 nfcv 
 |-  F/_ n 0
78 nfv 
 |-  F/ n ( ph /\ x e. X /\ 0 e. ( 0 ... M ) )
79 nfcv 
 |-  F/_ n CC
80 57 79 nfel 
 |-  F/ n [_ 0 / n ]_ B e. CC
81 78 80 nfim 
 |-  F/ n ( ( ph /\ x e. X /\ 0 e. ( 0 ... M ) ) -> [_ 0 / n ]_ B e. CC )
82 62 3anbi3d 
 |-  ( n = 0 -> ( ( ph /\ x e. X /\ n e. ( 0 ... M ) ) <-> ( ph /\ x e. X /\ 0 e. ( 0 ... M ) ) ) )
83 65 eleq1d 
 |-  ( n = 0 -> ( B e. CC <-> [_ 0 / n ]_ B e. CC ) )
84 82 83 imbi12d 
 |-  ( n = 0 -> ( ( ( ph /\ x e. X /\ n e. ( 0 ... M ) ) -> B e. CC ) <-> ( ( ph /\ x e. X /\ 0 e. ( 0 ... M ) ) -> [_ 0 / n ]_ B e. CC ) ) )
85 77 81 84 4 vtoclgf 
 |-  ( 0 e. RR -> ( ( ph /\ x e. X /\ 0 e. ( 0 ... M ) ) -> [_ 0 / n ]_ B e. CC ) )
86 76 85 ax-mp 
 |-  ( ( ph /\ x e. X /\ 0 e. ( 0 ... M ) ) -> [_ 0 / n ]_ B e. CC )
87 74 73 75 86 syl3anc 
 |-  ( ( ph /\ x e. X ) -> [_ 0 / n ]_ B e. CC )
88 eqid 
 |-  ( x e. X |-> [_ 0 / n ]_ B ) = ( x e. X |-> [_ 0 / n ]_ B )
89 88 fvmpt2 
 |-  ( ( x e. X /\ [_ 0 / n ]_ B e. CC ) -> ( ( x e. X |-> [_ 0 / n ]_ B ) ` x ) = [_ 0 / n ]_ B )
90 73 87 89 syl2anc 
 |-  ( ( ph /\ x e. X ) -> ( ( x e. X |-> [_ 0 / n ]_ B ) ` x ) = [_ 0 / n ]_ B )
91 72 90 eqtr2d 
 |-  ( ( ph /\ x e. X ) -> [_ 0 / n ]_ B = ( ( ( S Dn ( x e. X |-> A ) ) ` 0 ) ` x ) )
92 3 fmpttd 
 |-  ( ph -> ( x e. X |-> A ) : X --> CC )
93 elpm2r 
 |-  ( ( ( CC e. _V /\ S e. { RR , CC } ) /\ ( ( x e. X |-> A ) : X --> CC /\ X C_ S ) ) -> ( x e. X |-> A ) e. ( CC ^pm S ) )
94 40 1 92 2 93 syl22anc 
 |-  ( ph -> ( x e. X |-> A ) e. ( CC ^pm S ) )
95 dvn0 
 |-  ( ( S C_ CC /\ ( x e. X |-> A ) e. ( CC ^pm S ) ) -> ( ( S Dn ( x e. X |-> A ) ) ` 0 ) = ( x e. X |-> A ) )
96 38 94 95 syl2anc 
 |-  ( ph -> ( ( S Dn ( x e. X |-> A ) ) ` 0 ) = ( x e. X |-> A ) )
97 96 fveq1d 
 |-  ( ph -> ( ( ( S Dn ( x e. X |-> A ) ) ` 0 ) ` x ) = ( ( x e. X |-> A ) ` x ) )
98 97 adantr 
 |-  ( ( ph /\ x e. X ) -> ( ( ( S Dn ( x e. X |-> A ) ) ` 0 ) ` x ) = ( ( x e. X |-> A ) ` x ) )
99 eqid 
 |-  ( x e. X |-> A ) = ( x e. X |-> A )
100 99 fvmpt2 
 |-  ( ( x e. X /\ A e. CC ) -> ( ( x e. X |-> A ) ` x ) = A )
101 73 3 100 syl2anc 
 |-  ( ( ph /\ x e. X ) -> ( ( x e. X |-> A ) ` x ) = A )
102 91 98 101 3eqtrrd 
 |-  ( ( ph /\ x e. X ) -> A = [_ 0 / n ]_ B )
103 102 oveq1d 
 |-  ( ( ph /\ x e. X ) -> ( A / C ) = ( [_ 0 / n ]_ B / C ) )
104 103 mpteq2dva 
 |-  ( ph -> ( x e. X |-> ( A / C ) ) = ( x e. X |-> ( [_ 0 / n ]_ B / C ) ) )
105 48 104 eqtrd 
 |-  ( ph -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` 0 ) = ( x e. X |-> ( [_ 0 / n ]_ B / C ) ) )
106 105 a1i 
 |-  ( M e. ( ZZ>= ` 0 ) -> ( ph -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` 0 ) = ( x e. X |-> ( [_ 0 / n ]_ B / C ) ) ) )
107 simp3 
 |-  ( ( j e. ( 0 ..^ M ) /\ ( ph -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) = ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) /\ ph ) -> ph )
108 simp1 
 |-  ( ( j e. ( 0 ..^ M ) /\ ( ph -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) = ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) /\ ph ) -> j e. ( 0 ..^ M ) )
109 simpr 
 |-  ( ( ( ph -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) = ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) /\ ph ) -> ph )
110 simpl 
 |-  ( ( ( ph -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) = ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) /\ ph ) -> ( ph -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) = ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) )
111 109 110 mpd 
 |-  ( ( ( ph -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) = ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) /\ ph ) -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) = ( x e. X |-> ( [_ j / n ]_ B / C ) ) )
112 111 3adant1 
 |-  ( ( j e. ( 0 ..^ M ) /\ ( ph -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) = ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) /\ ph ) -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) = ( x e. X |-> ( [_ j / n ]_ B / C ) ) )
113 38 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) = ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) -> S C_ CC )
114 46 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) = ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) -> ( x e. X |-> ( A / C ) ) e. ( CC ^pm S ) )
115 elfzofz 
 |-  ( j e. ( 0 ..^ M ) -> j e. ( 0 ... M ) )
116 elfznn0 
 |-  ( j e. ( 0 ... M ) -> j e. NN0 )
117 116 ad2antlr 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) = ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) -> j e. NN0 )
118 115 117 sylanl2 
 |-  ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) = ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) -> j e. NN0 )
119 dvnp1 
 |-  ( ( S C_ CC /\ ( x e. X |-> ( A / C ) ) e. ( CC ^pm S ) /\ j e. NN0 ) -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` ( j + 1 ) ) = ( S _D ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) ) )
120 113 114 118 119 syl3anc 
 |-  ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) = ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` ( j + 1 ) ) = ( S _D ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) ) )
121 oveq2 
 |-  ( ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) = ( x e. X |-> ( [_ j / n ]_ B / C ) ) -> ( S _D ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) ) = ( S _D ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) )
122 121 adantl 
 |-  ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) = ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) -> ( S _D ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) ) = ( S _D ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) )
123 38 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> S C_ CC )
124 46 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( x e. X |-> ( A / C ) ) e. ( CC ^pm S ) )
125 simpr 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> j e. ( 0 ... M ) )
126 125 116 syl 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> j e. NN0 )
127 115 126 sylan2 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> j e. NN0 )
128 123 124 127 119 syl3anc 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` ( j + 1 ) ) = ( S _D ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) ) )
129 128 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) = ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` ( j + 1 ) ) = ( S _D ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) ) )
130 1 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> S e. { RR , CC } )
131 simplr 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. X ) -> j e. ( 0 ... M ) )
132 49 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. X ) -> ph )
133 simpr 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. X ) -> x e. X )
134 132 133 131 3jca 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. X ) -> ( ph /\ x e. X /\ j e. ( 0 ... M ) ) )
135 nfcv 
 |-  F/_ n j
136 nfv 
 |-  F/ n ( ph /\ x e. X /\ j e. ( 0 ... M ) )
137 135 nfcsb1 
 |-  F/_ n [_ j / n ]_ B
138 137 79 nfel 
 |-  F/ n [_ j / n ]_ B e. CC
139 136 138 nfim 
 |-  F/ n ( ( ph /\ x e. X /\ j e. ( 0 ... M ) ) -> [_ j / n ]_ B e. CC )
140 eleq1 
 |-  ( n = j -> ( n e. ( 0 ... M ) <-> j e. ( 0 ... M ) ) )
141 140 3anbi3d 
 |-  ( n = j -> ( ( ph /\ x e. X /\ n e. ( 0 ... M ) ) <-> ( ph /\ x e. X /\ j e. ( 0 ... M ) ) ) )
142 csbeq1a 
 |-  ( n = j -> B = [_ j / n ]_ B )
143 142 eleq1d 
 |-  ( n = j -> ( B e. CC <-> [_ j / n ]_ B e. CC ) )
144 141 143 imbi12d 
 |-  ( n = j -> ( ( ( ph /\ x e. X /\ n e. ( 0 ... M ) ) -> B e. CC ) <-> ( ( ph /\ x e. X /\ j e. ( 0 ... M ) ) -> [_ j / n ]_ B e. CC ) ) )
145 135 139 144 4 vtoclgf 
 |-  ( j e. ( 0 ... M ) -> ( ( ph /\ x e. X /\ j e. ( 0 ... M ) ) -> [_ j / n ]_ B e. CC ) )
146 131 134 145 sylc 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. X ) -> [_ j / n ]_ B e. CC )
147 115 146 sylanl2 
 |-  ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ x e. X ) -> [_ j / n ]_ B e. CC )
148 fzofzp1 
 |-  ( j e. ( 0 ..^ M ) -> ( j + 1 ) e. ( 0 ... M ) )
149 148 ad2antlr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ x e. X ) -> ( j + 1 ) e. ( 0 ... M ) )
150 115 132 sylanl2 
 |-  ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ x e. X ) -> ph )
151 simpr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ x e. X ) -> x e. X )
152 150 151 149 3jca 
 |-  ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ x e. X ) -> ( ph /\ x e. X /\ ( j + 1 ) e. ( 0 ... M ) ) )
153 nfcv 
 |-  F/_ n ( j + 1 )
154 nfv 
 |-  F/ n ( ph /\ x e. X /\ ( j + 1 ) e. ( 0 ... M ) )
155 153 nfcsb1 
 |-  F/_ n [_ ( j + 1 ) / n ]_ B
156 155 79 nfel 
 |-  F/ n [_ ( j + 1 ) / n ]_ B e. CC
157 154 156 nfim 
 |-  F/ n ( ( ph /\ x e. X /\ ( j + 1 ) e. ( 0 ... M ) ) -> [_ ( j + 1 ) / n ]_ B e. CC )
158 eleq1 
 |-  ( n = ( j + 1 ) -> ( n e. ( 0 ... M ) <-> ( j + 1 ) e. ( 0 ... M ) ) )
159 158 3anbi3d 
 |-  ( n = ( j + 1 ) -> ( ( ph /\ x e. X /\ n e. ( 0 ... M ) ) <-> ( ph /\ x e. X /\ ( j + 1 ) e. ( 0 ... M ) ) ) )
160 csbeq1a 
 |-  ( n = ( j + 1 ) -> B = [_ ( j + 1 ) / n ]_ B )
161 160 eleq1d 
 |-  ( n = ( j + 1 ) -> ( B e. CC <-> [_ ( j + 1 ) / n ]_ B e. CC ) )
162 159 161 imbi12d 
 |-  ( n = ( j + 1 ) -> ( ( ( ph /\ x e. X /\ n e. ( 0 ... M ) ) -> B e. CC ) <-> ( ( ph /\ x e. X /\ ( j + 1 ) e. ( 0 ... M ) ) -> [_ ( j + 1 ) / n ]_ B e. CC ) ) )
163 153 157 162 4 vtoclgf 
 |-  ( ( j + 1 ) e. ( 0 ... M ) -> ( ( ph /\ x e. X /\ ( j + 1 ) e. ( 0 ... M ) ) -> [_ ( j + 1 ) / n ]_ B e. CC ) )
164 149 152 163 sylc 
 |-  ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ x e. X ) -> [_ ( j + 1 ) / n ]_ B e. CC )
165 simpl 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ph )
166 115 adantl 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> j e. ( 0 ... M ) )
167 nfv 
 |-  F/ n ( ph /\ j e. ( 0 ... M ) )
168 nfcv 
 |-  F/_ n ( ( S Dn ( x e. X |-> A ) ) ` j )
169 56 137 nfmpt 
 |-  F/_ n ( x e. X |-> [_ j / n ]_ B )
170 168 169 nfeq 
 |-  F/ n ( ( S Dn ( x e. X |-> A ) ) ` j ) = ( x e. X |-> [_ j / n ]_ B )
171 167 170 nfim 
 |-  F/ n ( ( ph /\ j e. ( 0 ... M ) ) -> ( ( S Dn ( x e. X |-> A ) ) ` j ) = ( x e. X |-> [_ j / n ]_ B ) )
172 140 anbi2d 
 |-  ( n = j -> ( ( ph /\ n e. ( 0 ... M ) ) <-> ( ph /\ j e. ( 0 ... M ) ) ) )
173 fveq2 
 |-  ( n = j -> ( ( S Dn ( x e. X |-> A ) ) ` n ) = ( ( S Dn ( x e. X |-> A ) ) ` j ) )
174 142 mpteq2dv 
 |-  ( n = j -> ( x e. X |-> B ) = ( x e. X |-> [_ j / n ]_ B ) )
175 173 174 eqeq12d 
 |-  ( n = j -> ( ( ( S Dn ( x e. X |-> A ) ) ` n ) = ( x e. X |-> B ) <-> ( ( S Dn ( x e. X |-> A ) ) ` j ) = ( x e. X |-> [_ j / n ]_ B ) ) )
176 172 175 imbi12d 
 |-  ( n = j -> ( ( ( ph /\ n e. ( 0 ... M ) ) -> ( ( S Dn ( x e. X |-> A ) ) ` n ) = ( x e. X |-> B ) ) <-> ( ( ph /\ j e. ( 0 ... M ) ) -> ( ( S Dn ( x e. X |-> A ) ) ` j ) = ( x e. X |-> [_ j / n ]_ B ) ) ) )
177 171 176 5 chvarfv 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ( S Dn ( x e. X |-> A ) ) ` j ) = ( x e. X |-> [_ j / n ]_ B ) )
178 165 166 177 syl2anc 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( ( S Dn ( x e. X |-> A ) ) ` j ) = ( x e. X |-> [_ j / n ]_ B ) )
179 178 eqcomd 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( x e. X |-> [_ j / n ]_ B ) = ( ( S Dn ( x e. X |-> A ) ) ` j ) )
180 179 oveq2d 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( S _D ( x e. X |-> [_ j / n ]_ B ) ) = ( S _D ( ( S Dn ( x e. X |-> A ) ) ` j ) ) )
181 165 94 syl 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( x e. X |-> A ) e. ( CC ^pm S ) )
182 dvnp1 
 |-  ( ( S C_ CC /\ ( x e. X |-> A ) e. ( CC ^pm S ) /\ j e. NN0 ) -> ( ( S Dn ( x e. X |-> A ) ) ` ( j + 1 ) ) = ( S _D ( ( S Dn ( x e. X |-> A ) ) ` j ) ) )
183 123 181 127 182 syl3anc 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( ( S Dn ( x e. X |-> A ) ) ` ( j + 1 ) ) = ( S _D ( ( S Dn ( x e. X |-> A ) ) ` j ) ) )
184 183 eqcomd 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( S _D ( ( S Dn ( x e. X |-> A ) ) ` j ) ) = ( ( S Dn ( x e. X |-> A ) ) ` ( j + 1 ) ) )
185 148 adantl 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( j + 1 ) e. ( 0 ... M ) )
186 165 185 jca 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( ph /\ ( j + 1 ) e. ( 0 ... M ) ) )
187 nfv 
 |-  F/ n ( ph /\ ( j + 1 ) e. ( 0 ... M ) )
188 nfcv 
 |-  F/_ n ( ( S Dn ( x e. X |-> A ) ) ` ( j + 1 ) )
189 56 155 nfmpt 
 |-  F/_ n ( x e. X |-> [_ ( j + 1 ) / n ]_ B )
190 188 189 nfeq 
 |-  F/ n ( ( S Dn ( x e. X |-> A ) ) ` ( j + 1 ) ) = ( x e. X |-> [_ ( j + 1 ) / n ]_ B )
191 187 190 nfim 
 |-  F/ n ( ( ph /\ ( j + 1 ) e. ( 0 ... M ) ) -> ( ( S Dn ( x e. X |-> A ) ) ` ( j + 1 ) ) = ( x e. X |-> [_ ( j + 1 ) / n ]_ B ) )
192 158 anbi2d 
 |-  ( n = ( j + 1 ) -> ( ( ph /\ n e. ( 0 ... M ) ) <-> ( ph /\ ( j + 1 ) e. ( 0 ... M ) ) ) )
193 fveq2 
 |-  ( n = ( j + 1 ) -> ( ( S Dn ( x e. X |-> A ) ) ` n ) = ( ( S Dn ( x e. X |-> A ) ) ` ( j + 1 ) ) )
194 160 mpteq2dv 
 |-  ( n = ( j + 1 ) -> ( x e. X |-> B ) = ( x e. X |-> [_ ( j + 1 ) / n ]_ B ) )
195 193 194 eqeq12d 
 |-  ( n = ( j + 1 ) -> ( ( ( S Dn ( x e. X |-> A ) ) ` n ) = ( x e. X |-> B ) <-> ( ( S Dn ( x e. X |-> A ) ) ` ( j + 1 ) ) = ( x e. X |-> [_ ( j + 1 ) / n ]_ B ) ) )
196 192 195 imbi12d 
 |-  ( n = ( j + 1 ) -> ( ( ( ph /\ n e. ( 0 ... M ) ) -> ( ( S Dn ( x e. X |-> A ) ) ` n ) = ( x e. X |-> B ) ) <-> ( ( ph /\ ( j + 1 ) e. ( 0 ... M ) ) -> ( ( S Dn ( x e. X |-> A ) ) ` ( j + 1 ) ) = ( x e. X |-> [_ ( j + 1 ) / n ]_ B ) ) ) )
197 153 191 196 5 vtoclgf 
 |-  ( ( j + 1 ) e. ( 0 ... M ) -> ( ( ph /\ ( j + 1 ) e. ( 0 ... M ) ) -> ( ( S Dn ( x e. X |-> A ) ) ` ( j + 1 ) ) = ( x e. X |-> [_ ( j + 1 ) / n ]_ B ) ) )
198 185 186 197 sylc 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( ( S Dn ( x e. X |-> A ) ) ` ( j + 1 ) ) = ( x e. X |-> [_ ( j + 1 ) / n ]_ B ) )
199 180 184 198 3eqtrd 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( S _D ( x e. X |-> [_ j / n ]_ B ) ) = ( x e. X |-> [_ ( j + 1 ) / n ]_ B ) )
200 6 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> C e. CC )
201 7 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> C =/= 0 )
202 130 147 164 199 200 201 dvmptdivc 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( S _D ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) = ( x e. X |-> ( [_ ( j + 1 ) / n ]_ B / C ) ) )
203 202 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) = ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) -> ( S _D ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) = ( x e. X |-> ( [_ ( j + 1 ) / n ]_ B / C ) ) )
204 129 122 203 3eqtrd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) = ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` ( j + 1 ) ) = ( x e. X |-> ( [_ ( j + 1 ) / n ]_ B / C ) ) )
205 204 eqcomd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) = ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) -> ( x e. X |-> ( [_ ( j + 1 ) / n ]_ B / C ) ) = ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` ( j + 1 ) ) )
206 205 120 122 3eqtrrd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) = ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) -> ( S _D ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) = ( x e. X |-> ( [_ ( j + 1 ) / n ]_ B / C ) ) )
207 120 122 206 3eqtrd 
 |-  ( ( ( ph /\ j e. ( 0 ..^ M ) ) /\ ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) = ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` ( j + 1 ) ) = ( x e. X |-> ( [_ ( j + 1 ) / n ]_ B / C ) ) )
208 107 108 112 207 syl21anc 
 |-  ( ( j e. ( 0 ..^ M ) /\ ( ph -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) = ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) /\ ph ) -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` ( j + 1 ) ) = ( x e. X |-> ( [_ ( j + 1 ) / n ]_ B / C ) ) )
209 208 3exp 
 |-  ( j e. ( 0 ..^ M ) -> ( ( ph -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` j ) = ( x e. X |-> ( [_ j / n ]_ B / C ) ) ) -> ( ph -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` ( j + 1 ) ) = ( x e. X |-> ( [_ ( j + 1 ) / n ]_ B / C ) ) ) ) )
210 16 22 28 36 106 209 fzind2 
 |-  ( n e. ( 0 ... M ) -> ( ph -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` n ) = ( x e. X |-> ( B / C ) ) ) )
211 9 10 210 sylc 
 |-  ( ( ph /\ n e. ( 0 ... M ) ) -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` n ) = ( x e. X |-> ( B / C ) ) )