Metamath Proof Explorer


Theorem mvth

Description: The Mean Value Theorem. If F is a real continuous function on [ A , B ] which is differentiable on ( A , B ) , then there is some x e. ( A , B ) such that ( RR _D F )x is equal to the average slope over [ A , B ] . This is Metamath 100 proof #75. (Contributed by Mario Carneiro, 1-Sep-2014) (Proof shortened by Mario Carneiro, 29-Dec-2016)

Ref Expression
Hypotheses mvth.a φ A
mvth.b φ B
mvth.lt φ A < B
mvth.f φ F : A B cn
mvth.d φ dom F = A B
Assertion mvth φ x A B F x = F B F A B A

Proof

Step Hyp Ref Expression
1 mvth.a φ A
2 mvth.b φ B
3 mvth.lt φ A < B
4 mvth.f φ F : A B cn
5 mvth.d φ dom F = A B
6 mptresid I A B = z A B z
7 iccssre A B A B
8 1 2 7 syl2anc φ A B
9 ax-resscn
10 cncfmptid A B z A B z : A B cn
11 8 9 10 sylancl φ z A B z : A B cn
12 6 11 eqeltrid φ I A B : A B cn
13 6 eqcomi z A B z = I A B
14 13 oveq2i dz A B z d z = D I A B
15 reelprrecn
16 15 a1i φ
17 simpr φ z z
18 17 recnd φ z z
19 1red φ z 1
20 16 dvmptid φ dz z d z = z 1
21 eqid TopOpen fld = TopOpen fld
22 21 tgioo2 topGen ran . = TopOpen fld 𝑡
23 iccntr A B int topGen ran . A B = A B
24 1 2 23 syl2anc φ int topGen ran . A B = A B
25 16 18 19 20 8 22 21 24 dvmptres2 φ dz A B z d z = z A B 1
26 14 25 eqtr3id φ D I A B = z A B 1
27 26 dmeqd φ dom I A B = dom z A B 1
28 1ex 1 V
29 eqid z A B 1 = z A B 1
30 28 29 dmmpti dom z A B 1 = A B
31 27 30 eqtrdi φ dom I A B = A B
32 1 2 3 4 12 5 31 cmvth φ x A B F B F A I A B x = I A B B I A B A F x
33 1 rexrd φ A *
34 2 rexrd φ B *
35 1 2 3 ltled φ A B
36 ubicc2 A * B * A B B A B
37 33 34 35 36 syl3anc φ B A B
38 fvresi B A B I A B B = B
39 37 38 syl φ I A B B = B
40 lbicc2 A * B * A B A A B
41 33 34 35 40 syl3anc φ A A B
42 fvresi A A B I A B A = A
43 41 42 syl φ I A B A = A
44 39 43 oveq12d φ I A B B I A B A = B A
45 44 adantr φ x A B I A B B I A B A = B A
46 45 oveq1d φ x A B I A B B I A B A F x = B A F x
47 26 fveq1d φ I A B x = z A B 1 x
48 eqidd z = x 1 = 1
49 48 29 28 fvmpt3i x A B z A B 1 x = 1
50 47 49 sylan9eq φ x A B I A B x = 1
51 50 oveq2d φ x A B F B F A I A B x = F B F A 1
52 cncff F : A B cn F : A B
53 4 52 syl φ F : A B
54 53 37 ffvelrnd φ F B
55 53 41 ffvelrnd φ F A
56 54 55 resubcld φ F B F A
57 56 recnd φ F B F A
58 57 adantr φ x A B F B F A
59 58 mulid1d φ x A B F B F A 1 = F B F A
60 51 59 eqtrd φ x A B F B F A I A B x = F B F A
61 46 60 eqeq12d φ x A B I A B B I A B A F x = F B F A I A B x B A F x = F B F A
62 2 1 resubcld φ B A
63 62 recnd φ B A
64 63 adantr φ x A B B A
65 dvf F : dom F
66 5 feq2d φ F : dom F F : A B
67 65 66 mpbii φ F : A B
68 67 ffvelrnda φ x A B F x
69 1 2 posdifd φ A < B 0 < B A
70 3 69 mpbid φ 0 < B A
71 70 gt0ne0d φ B A 0
72 71 adantr φ x A B B A 0
73 58 64 68 72 divmuld φ x A B F B F A B A = F x B A F x = F B F A
74 61 73 bitr4d φ x A B I A B B I A B A F x = F B F A I A B x F B F A B A = F x
75 eqcom F B F A I A B x = I A B B I A B A F x I A B B I A B A F x = F B F A I A B x
76 eqcom F x = F B F A B A F B F A B A = F x
77 74 75 76 3bitr4g φ x A B F B F A I A B x = I A B B I A B A F x F x = F B F A B A
78 77 rexbidva φ x A B F B F A I A B x = I A B B I A B A F x x A B F x = F B F A B A
79 32 78 mpbid φ x A B F x = F B F A B A