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 φ S
dvconstbi.y φ Y : S
dvconstbi.dy φ dom Y S = S
Assertion dvconstbi φ S D Y = S × 0 c Y = S × c

Proof

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