Metamath Proof Explorer

Theorem dvconstbi

Description: The derivative of a function on S is zero iff it is a constant function. Roughly a biconditional S analogue of dvconst and dveq0 . Corresponds to integration formula " S. 0 _d x = C " in section 4.1 of LarsonHostetlerEdwards p. 278. (Contributed by Steve Rodriguez, 11-Nov-2015)

Ref Expression
Hypotheses dvconstbi.s 
|- ( ph -> S e. { RR , CC } )
dvconstbi.y 
|- ( ph -> Y : S --> CC )
dvconstbi.dy 
|- ( ph -> dom ( S _D Y ) = S )
Assertion dvconstbi 
|- ( ph -> ( ( S _D Y ) = ( S X. { 0 } ) <-> E. c e. CC Y = ( S X. { c } ) ) )

Proof

Step Hyp Ref Expression
1 dvconstbi.s 
 |-  ( ph -> S e. { RR , CC } )
2 dvconstbi.y 
 |-  ( ph -> Y : S --> CC )
3 dvconstbi.dy 
 |-  ( ph -> dom ( S _D Y ) = S )
4 elpri 
 |-  ( S e. { RR , CC } -> ( S = RR \/ S = CC ) )
5 1 4 syl 
 |-  ( ph -> ( S = RR \/ S = CC ) )
6 0re 
 |-  0 e. RR
7 eleq2 
 |-  ( S = RR -> ( 0 e. S <-> 0 e. RR ) )
8 6 7 mpbiri 
 |-  ( S = RR -> 0 e. S )
9 0cn 
 |-  0 e. CC
10 eleq2 
 |-  ( S = CC -> ( 0 e. S <-> 0 e. CC ) )
11 9 10 mpbiri 
 |-  ( S = CC -> 0 e. S )
12 8 11 jaoi 
 |-  ( ( S = RR \/ S = CC ) -> 0 e. S )
13 5 12 syl 
 |-  ( ph -> 0 e. S )
14 ffvelrn 
 |-  ( ( Y : S --> CC /\ 0 e. S ) -> ( Y ` 0 ) e. CC )
15 2 13 14 syl2anc 
 |-  ( ph -> ( Y ` 0 ) e. CC )
16 15 adantr 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) ) -> ( Y ` 0 ) e. CC )
17 2 ffnd 
 |-  ( ph -> Y Fn S )
18 17 adantr 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) ) -> Y Fn S )
19 fvex 
 |-  ( Y ` 0 ) e. _V
20 fnconstg 
 |-  ( ( Y ` 0 ) e. _V -> ( S X. { ( Y ` 0 ) } ) Fn S )
21 19 20 mp1i 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) ) -> ( S X. { ( Y ` 0 ) } ) Fn S )
22 19 fvconst2 
 |-  ( y e. S -> ( ( S X. { ( Y ` 0 ) } ) ` y ) = ( Y ` 0 ) )
23 22 adantl 
 |-  ( ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) ) /\ y e. S ) -> ( ( S X. { ( Y ` 0 ) } ) ` y ) = ( Y ` 0 ) )
24 eqid 
 |-  ( ( abs o. - ) |` ( S X. S ) ) = ( ( abs o. - ) |` ( S X. S ) )
25 1 24 sblpnf 
 |-  ( ( ph /\ 0 e. S ) -> ( 0 ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) +oo ) = S )
26 13 25 mpdan 
 |-  ( ph -> ( 0 ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) +oo ) = S )
27 26 eleq2d 
 |-  ( ph -> ( y e. ( 0 ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) +oo ) <-> y e. S ) )
28 27 biimpar 
 |-  ( ( ph /\ y e. S ) -> y e. ( 0 ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) +oo ) )
29 13 26 eleqtrrd 
 |-  ( ph -> 0 e. ( 0 ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) +oo ) )
30 1 adantr 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) ) -> S e. { RR , CC } )
31 ssidd 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) ) -> S C_ S )
32 2 adantr 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) ) -> Y : S --> CC )
33 13 adantr 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) ) -> 0 e. S )
34 pnfxr 
 |-  +oo e. RR*
35 34 a1i 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) ) -> +oo e. RR* )
36 eqid 
 |-  ( 0 ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) +oo ) = ( 0 ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) +oo )
37 26 adantr 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) ) -> ( 0 ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) +oo ) = S )
38 3 adantr 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) ) -> dom ( S _D Y ) = S )
39 37 38 eqtr4d 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) ) -> ( 0 ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) +oo ) = dom ( S _D Y ) )
40 eqimss 
 |-  ( ( 0 ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) +oo ) = dom ( S _D Y ) -> ( 0 ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) +oo ) C_ dom ( S _D Y ) )
41 39 40 syl 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) ) -> ( 0 ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) +oo ) C_ dom ( S _D Y ) )
42 6 a1i 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) ) -> 0 e. RR )
43 26 eleq2d 
 |-  ( ph -> ( x e. ( 0 ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) +oo ) <-> x e. S ) )
44 43 biimpa 
 |-  ( ( ph /\ x e. ( 0 ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) +oo ) ) -> x e. S )
45 44 3adant2 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) /\ x e. ( 0 ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) +oo ) ) -> x e. S )
46 fveq1 
 |-  ( ( S _D Y ) = ( S X. { 0 } ) -> ( ( S _D Y ) ` x ) = ( ( S X. { 0 } ) ` x ) )
47 c0ex 
 |-  0 e. _V
48 47 fvconst2 
 |-  ( x e. S -> ( ( S X. { 0 } ) ` x ) = 0 )
49 46 48 sylan9eq 
 |-  ( ( ( S _D Y ) = ( S X. { 0 } ) /\ x e. S ) -> ( ( S _D Y ) ` x ) = 0 )
50 49 9 eqeltrdi 
 |-  ( ( ( S _D Y ) = ( S X. { 0 } ) /\ x e. S ) -> ( ( S _D Y ) ` x ) e. CC )
51 50 abscld 
 |-  ( ( ( S _D Y ) = ( S X. { 0 } ) /\ x e. S ) -> ( abs ` ( ( S _D Y ) ` x ) ) e. RR )
52 49 abs00bd 
 |-  ( ( ( S _D Y ) = ( S X. { 0 } ) /\ x e. S ) -> ( abs ` ( ( S _D Y ) ` x ) ) = 0 )
53 eqle 
 |-  ( ( ( abs ` ( ( S _D Y ) ` x ) ) e. RR /\ ( abs ` ( ( S _D Y ) ` x ) ) = 0 ) -> ( abs ` ( ( S _D Y ) ` x ) ) <_ 0 )
54 51 52 53 syl2anc 
 |-  ( ( ( S _D Y ) = ( S X. { 0 } ) /\ x e. S ) -> ( abs ` ( ( S _D Y ) ` x ) ) <_ 0 )
55 54 3adant1 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) /\ x e. S ) -> ( abs ` ( ( S _D Y ) ` x ) ) <_ 0 )
56 45 55 syld3an3 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) /\ x e. ( 0 ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) +oo ) ) -> ( abs ` ( ( S _D Y ) ` x ) ) <_ 0 )
57 56 3expa 
 |-  ( ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) ) /\ x e. ( 0 ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) +oo ) ) -> ( abs ` ( ( S _D Y ) ` x ) ) <_ 0 )
58 30 24 31 32 33 35 36 41 42 57 dvlip2 
 |-  ( ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) ) /\ ( 0 e. ( 0 ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) +oo ) /\ y e. ( 0 ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) +oo ) ) ) -> ( abs ` ( ( Y ` 0 ) - ( Y ` y ) ) ) <_ ( 0 x. ( abs ` ( 0 - y ) ) ) )
59 29 58 sylanr1 
 |-  ( ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) ) /\ ( ph /\ y e. ( 0 ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) +oo ) ) ) -> ( abs ` ( ( Y ` 0 ) - ( Y ` y ) ) ) <_ ( 0 x. ( abs ` ( 0 - y ) ) ) )
60 59 3impdi 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) /\ y e. ( 0 ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) +oo ) ) -> ( abs ` ( ( Y ` 0 ) - ( Y ` y ) ) ) <_ ( 0 x. ( abs ` ( 0 - y ) ) ) )
61 28 60 syl3an3 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) /\ ( ph /\ y e. S ) ) -> ( abs ` ( ( Y ` 0 ) - ( Y ` y ) ) ) <_ ( 0 x. ( abs ` ( 0 - y ) ) ) )
62 61 3expa 
 |-  ( ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) ) /\ ( ph /\ y e. S ) ) -> ( abs ` ( ( Y ` 0 ) - ( Y ` y ) ) ) <_ ( 0 x. ( abs ` ( 0 - y ) ) ) )
63 62 3impdi 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) /\ y e. S ) -> ( abs ` ( ( Y ` 0 ) - ( Y ` y ) ) ) <_ ( 0 x. ( abs ` ( 0 - y ) ) ) )
64 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
65 1 64 syl 
 |-  ( ph -> S C_ CC )
66 65 sseld 
 |-  ( ph -> ( y e. S -> y e. CC ) )
67 subcl 
 |-  ( ( 0 e. CC /\ y e. CC ) -> ( 0 - y ) e. CC )
68 67 abscld 
 |-  ( ( 0 e. CC /\ y e. CC ) -> ( abs ` ( 0 - y ) ) e. RR )
69 9 68 mpan 
 |-  ( y e. CC -> ( abs ` ( 0 - y ) ) e. RR )
70 66 69 syl6 
 |-  ( ph -> ( y e. S -> ( abs ` ( 0 - y ) ) e. RR ) )
71 70 imp 
 |-  ( ( ph /\ y e. S ) -> ( abs ` ( 0 - y ) ) e. RR )
72 71 recnd 
 |-  ( ( ph /\ y e. S ) -> ( abs ` ( 0 - y ) ) e. CC )
73 72 mul02d 
 |-  ( ( ph /\ y e. S ) -> ( 0 x. ( abs ` ( 0 - y ) ) ) = 0 )
74 73 3adant2 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) /\ y e. S ) -> ( 0 x. ( abs ` ( 0 - y ) ) ) = 0 )
75 63 74 breqtrd 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) /\ y e. S ) -> ( abs ` ( ( Y ` 0 ) - ( Y ` y ) ) ) <_ 0 )
76 ffvelrn 
 |-  ( ( Y : S --> CC /\ y e. S ) -> ( Y ` y ) e. CC )
77 14 76 anim12dan 
 |-  ( ( Y : S --> CC /\ ( 0 e. S /\ y e. S ) ) -> ( ( Y ` 0 ) e. CC /\ ( Y ` y ) e. CC ) )
78 2 77 sylan 
 |-  ( ( ph /\ ( 0 e. S /\ y e. S ) ) -> ( ( Y ` 0 ) e. CC /\ ( Y ` y ) e. CC ) )
79 78 3impb 
 |-  ( ( ph /\ 0 e. S /\ y e. S ) -> ( ( Y ` 0 ) e. CC /\ ( Y ` y ) e. CC ) )
80 13 79 syl3an2 
 |-  ( ( ph /\ ph /\ y e. S ) -> ( ( Y ` 0 ) e. CC /\ ( Y ` y ) e. CC ) )
81 80 3anidm12 
 |-  ( ( ph /\ y e. S ) -> ( ( Y ` 0 ) e. CC /\ ( Y ` y ) e. CC ) )
82 subcl 
 |-  ( ( ( Y ` 0 ) e. CC /\ ( Y ` y ) e. CC ) -> ( ( Y ` 0 ) - ( Y ` y ) ) e. CC )
83 81 82 syl 
 |-  ( ( ph /\ y e. S ) -> ( ( Y ` 0 ) - ( Y ` y ) ) e. CC )
84 83 absge0d 
 |-  ( ( ph /\ y e. S ) -> 0 <_ ( abs ` ( ( Y ` 0 ) - ( Y ` y ) ) ) )
85 84 3adant2 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) /\ y e. S ) -> 0 <_ ( abs ` ( ( Y ` 0 ) - ( Y ` y ) ) ) )
86 83 abscld 
 |-  ( ( ph /\ y e. S ) -> ( abs ` ( ( Y ` 0 ) - ( Y ` y ) ) ) e. RR )
87 letri3 
 |-  ( ( ( abs ` ( ( Y ` 0 ) - ( Y ` y ) ) ) e. RR /\ 0 e. RR ) -> ( ( abs ` ( ( Y ` 0 ) - ( Y ` y ) ) ) = 0 <-> ( ( abs ` ( ( Y ` 0 ) - ( Y ` y ) ) ) <_ 0 /\ 0 <_ ( abs ` ( ( Y ` 0 ) - ( Y ` y ) ) ) ) ) )
88 86 6 87 sylancl 
 |-  ( ( ph /\ y e. S ) -> ( ( abs ` ( ( Y ` 0 ) - ( Y ` y ) ) ) = 0 <-> ( ( abs ` ( ( Y ` 0 ) - ( Y ` y ) ) ) <_ 0 /\ 0 <_ ( abs ` ( ( Y ` 0 ) - ( Y ` y ) ) ) ) ) )
89 88 3adant2 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) /\ y e. S ) -> ( ( abs ` ( ( Y ` 0 ) - ( Y ` y ) ) ) = 0 <-> ( ( abs ` ( ( Y ` 0 ) - ( Y ` y ) ) ) <_ 0 /\ 0 <_ ( abs ` ( ( Y ` 0 ) - ( Y ` y ) ) ) ) ) )
90 75 85 89 mpbir2and 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) /\ y e. S ) -> ( abs ` ( ( Y ` 0 ) - ( Y ` y ) ) ) = 0 )
91 83 abs00ad 
 |-  ( ( ph /\ y e. S ) -> ( ( abs ` ( ( Y ` 0 ) - ( Y ` y ) ) ) = 0 <-> ( ( Y ` 0 ) - ( Y ` y ) ) = 0 ) )
92 91 3adant2 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) /\ y e. S ) -> ( ( abs ` ( ( Y ` 0 ) - ( Y ` y ) ) ) = 0 <-> ( ( Y ` 0 ) - ( Y ` y ) ) = 0 ) )
93 90 92 mpbid 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) /\ y e. S ) -> ( ( Y ` 0 ) - ( Y ` y ) ) = 0 )
94 subeq0 
 |-  ( ( ( Y ` 0 ) e. CC /\ ( Y ` y ) e. CC ) -> ( ( ( Y ` 0 ) - ( Y ` y ) ) = 0 <-> ( Y ` 0 ) = ( Y ` y ) ) )
95 81 94 syl 
 |-  ( ( ph /\ y e. S ) -> ( ( ( Y ` 0 ) - ( Y ` y ) ) = 0 <-> ( Y ` 0 ) = ( Y ` y ) ) )
96 95 3adant2 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) /\ y e. S ) -> ( ( ( Y ` 0 ) - ( Y ` y ) ) = 0 <-> ( Y ` 0 ) = ( Y ` y ) ) )
97 93 96 mpbid 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) /\ y e. S ) -> ( Y ` 0 ) = ( Y ` y ) )
98 97 3expa 
 |-  ( ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) ) /\ y e. S ) -> ( Y ` 0 ) = ( Y ` y ) )
99 23 98 eqtr2d 
 |-  ( ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) ) /\ y e. S ) -> ( Y ` y ) = ( ( S X. { ( Y ` 0 ) } ) ` y ) )
100 18 21 99 eqfnfvd 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) ) -> Y = ( S X. { ( Y ` 0 ) } ) )
101 sneq 
 |-  ( x = ( Y ` 0 ) -> { x } = { ( Y ` 0 ) } )
102 101 xpeq2d 
 |-  ( x = ( Y ` 0 ) -> ( S X. { x } ) = ( S X. { ( Y ` 0 ) } ) )
103 102 rspceeqv 
 |-  ( ( ( Y ` 0 ) e. CC /\ Y = ( S X. { ( Y ` 0 ) } ) ) -> E. x e. CC Y = ( S X. { x } ) )
104 16 100 103 syl2anc 
 |-  ( ( ph /\ ( S _D Y ) = ( S X. { 0 } ) ) -> E. x e. CC Y = ( S X. { x } ) )
105 104 ex 
 |-  ( ph -> ( ( S _D Y ) = ( S X. { 0 } ) -> E. x e. CC Y = ( S X. { x } ) ) )
106 oveq2 
 |-  ( Y = ( S X. { x } ) -> ( S _D Y ) = ( S _D ( S X. { x } ) ) )
107 106 3ad2ant3 
 |-  ( ( ph /\ x e. CC /\ Y = ( S X. { x } ) ) -> ( S _D Y ) = ( S _D ( S X. { x } ) ) )
108 dvsconst 
 |-  ( ( S e. { RR , CC } /\ x e. CC ) -> ( S _D ( S X. { x } ) ) = ( S X. { 0 } ) )
109 1 108 sylan 
 |-  ( ( ph /\ x e. CC ) -> ( S _D ( S X. { x } ) ) = ( S X. { 0 } ) )
110 109 3adant3 
 |-  ( ( ph /\ x e. CC /\ Y = ( S X. { x } ) ) -> ( S _D ( S X. { x } ) ) = ( S X. { 0 } ) )
111 107 110 eqtrd 
 |-  ( ( ph /\ x e. CC /\ Y = ( S X. { x } ) ) -> ( S _D Y ) = ( S X. { 0 } ) )
112 111 rexlimdv3a 
 |-  ( ph -> ( E. x e. CC Y = ( S X. { x } ) -> ( S _D Y ) = ( S X. { 0 } ) ) )
113 105 112 impbid 
 |-  ( ph -> ( ( S _D Y ) = ( S X. { 0 } ) <-> E. x e. CC Y = ( S X. { x } ) ) )
114 sneq 
 |-  ( c = x -> { c } = { x } )
115 114 xpeq2d 
 |-  ( c = x -> ( S X. { c } ) = ( S X. { x } ) )
116 115 eqeq2d 
 |-  ( c = x -> ( Y = ( S X. { c } ) <-> Y = ( S X. { x } ) ) )
117 116 cbvrexvw 
 |-  ( E. c e. CC Y = ( S X. { c } ) <-> E. x e. CC Y = ( S X. { x } ) )
118 113 117 bitr4di 
 |-  ( ph -> ( ( S _D Y ) = ( S X. { 0 } ) <-> E. c e. CC Y = ( S X. { c } ) ) )