Metamath Proof Explorer


Theorem dvferm1

Description: One-sided version of dvferm . A point U which is the local maximum of its right neighborhood has derivative at most zero. (Contributed by Mario Carneiro, 24-Feb-2015) (Proof shortened by Mario Carneiro, 28-Dec-2016)

Ref Expression
Hypotheses dvferm.a φ F : X
dvferm.b φ X
dvferm.u φ U A B
dvferm.s φ A B X
dvferm.d φ U dom F
dvferm1.r φ y U B F y F U
Assertion dvferm1 φ F U 0

Proof

Step Hyp Ref Expression
1 dvferm.a φ F : X
2 dvferm.b φ X
3 dvferm.u φ U A B
4 dvferm.s φ A B X
5 dvferm.d φ U dom F
6 dvferm1.r φ y U B F y F U
7 fveq2 x = z F x = F z
8 7 oveq1d x = z F x F U = F z F U
9 oveq1 x = z x U = z U
10 8 9 oveq12d x = z F x F U x U = F z F U z U
11 eqid x X U F x F U x U = x X U F x F U x U
12 ovex F z F U z U V
13 10 11 12 fvmpt z X U x X U F x F U x U z = F z F U z U
14 13 fvoveq1d z X U x X U F x F U x U z F U = F z F U z U F U
15 id y = F U y = F U
16 14 15 breqan12rd y = F U z X U x X U F x F U x U z F U < y F z F U z U F U < F U
17 16 imbi2d y = F U z X U z U z U < u x X U F x F U x U z F U < y z U z U < u F z F U z U F U < F U
18 17 ralbidva y = F U z X U z U z U < u x X U F x F U x U z F U < y z X U z U z U < u F z F U z U F U < F U
19 18 rexbidv y = F U u + z X U z U z U < u x X U F x F U x U z F U < y u + z X U z U z U < u F z F U z U F U < F U
20 dvf F : dom F
21 ffun F : dom F Fun F
22 funfvbrb Fun F U dom F U F F U
23 20 21 22 mp2b U dom F U F F U
24 5 23 sylib φ U F F U
25 eqid TopOpen fld 𝑡 = TopOpen fld 𝑡
26 eqid TopOpen fld = TopOpen fld
27 ax-resscn
28 27 a1i φ
29 fss F : X F : X
30 1 27 29 sylancl φ F : X
31 25 26 11 28 30 2 eldv φ U F F U U int TopOpen fld 𝑡 X F U x X U F x F U x U lim U
32 24 31 mpbid φ U int TopOpen fld 𝑡 X F U x X U F x F U x U lim U
33 32 simprd φ F U x X U F x F U x U lim U
34 33 adantr φ 0 < F U F U x X U F x F U x U lim U
35 2 27 sstrdi φ X
36 4 3 sseldd φ U X
37 30 35 36 dvlem φ x X U F x F U x U
38 37 fmpttd φ x X U F x F U x U : X U
39 38 adantr φ 0 < F U x X U F x F U x U : X U
40 35 adantr φ 0 < F U X
41 40 ssdifssd φ 0 < F U X U
42 35 36 sseldd φ U
43 42 adantr φ 0 < F U U
44 39 41 43 ellimc3 φ 0 < F U F U x X U F x F U x U lim U F U y + u + z X U z U z U < u x X U F x F U x U z F U < y
45 34 44 mpbid φ 0 < F U F U y + u + z X U z U z U < u x X U F x F U x U z F U < y
46 45 simprd φ 0 < F U y + u + z X U z U z U < u x X U F x F U x U z F U < y
47 dvfre F : X X F : dom F
48 1 2 47 syl2anc φ F : dom F
49 48 5 ffvelrnd φ F U
50 49 anim1i φ 0 < F U F U 0 < F U
51 elrp F U + F U 0 < F U
52 50 51 sylibr φ 0 < F U F U +
53 19 46 52 rspcdva φ 0 < F U u + z X U z U z U < u F z F U z U F U < F U
54 1 ad3antrrr φ 0 < F U u + z X U z U z U < u F z F U z U F U < F U F : X
55 2 ad3antrrr φ 0 < F U u + z X U z U z U < u F z F U z U F U < F U X
56 3 ad3antrrr φ 0 < F U u + z X U z U z U < u F z F U z U F U < F U U A B
57 4 ad3antrrr φ 0 < F U u + z X U z U z U < u F z F U z U F U < F U A B X
58 5 ad3antrrr φ 0 < F U u + z X U z U z U < u F z F U z U F U < F U U dom F
59 6 ad3antrrr φ 0 < F U u + z X U z U z U < u F z F U z U F U < F U y U B F y F U
60 simpllr φ 0 < F U u + z X U z U z U < u F z F U z U F U < F U 0 < F U
61 simplr φ 0 < F U u + z X U z U z U < u F z F U z U F U < F U u +
62 simpr φ 0 < F U u + z X U z U z U < u F z F U z U F U < F U z X U z U z U < u F z F U z U F U < F U
63 eqid U + if B U + u B U + u 2 = U + if B U + u B U + u 2
64 54 55 56 57 58 59 60 61 62 63 dvferm1lem ¬ φ 0 < F U u + z X U z U z U < u F z F U z U F U < F U
65 64 imnani φ 0 < F U u + ¬ z X U z U z U < u F z F U z U F U < F U
66 65 nrexdv φ 0 < F U ¬ u + z X U z U z U < u F z F U z U F U < F U
67 53 66 pm2.65da φ ¬ 0 < F U
68 0re 0
69 lenlt F U 0 F U 0 ¬ 0 < F U
70 49 68 69 sylancl φ F U 0 ¬ 0 < F U
71 67 70 mpbird φ F U 0