Metamath Proof Explorer


Theorem dyadovol

Description: Volume of a dyadic rational interval. (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypothesis dyadmbl.1 F = x , y 0 x 2 y x + 1 2 y
Assertion dyadovol A B 0 vol * . A F B = 1 2 B

Proof

Step Hyp Ref Expression
1 dyadmbl.1 F = x , y 0 x 2 y x + 1 2 y
2 1 dyadval A B 0 A F B = A 2 B A + 1 2 B
3 2 fveq2d A B 0 . A F B = . A 2 B A + 1 2 B
4 df-ov A 2 B A + 1 2 B = . A 2 B A + 1 2 B
5 3 4 eqtr4di A B 0 . A F B = A 2 B A + 1 2 B
6 5 fveq2d A B 0 vol * . A F B = vol * A 2 B A + 1 2 B
7 zre A A
8 2nn 2
9 nnexpcl 2 B 0 2 B
10 8 9 mpan B 0 2 B
11 nndivre A 2 B A 2 B
12 7 10 11 syl2an A B 0 A 2 B
13 peano2re A A + 1
14 7 13 syl A A + 1
15 nndivre A + 1 2 B A + 1 2 B
16 14 10 15 syl2an A B 0 A + 1 2 B
17 7 adantr A B 0 A
18 17 lep1d A B 0 A A + 1
19 17 13 syl A B 0 A + 1
20 10 adantl A B 0 2 B
21 20 nnred A B 0 2 B
22 20 nngt0d A B 0 0 < 2 B
23 lediv1 A A + 1 2 B 0 < 2 B A A + 1 A 2 B A + 1 2 B
24 17 19 21 22 23 syl112anc A B 0 A A + 1 A 2 B A + 1 2 B
25 18 24 mpbid A B 0 A 2 B A + 1 2 B
26 ovolicc A 2 B A + 1 2 B A 2 B A + 1 2 B vol * A 2 B A + 1 2 B = A + 1 2 B A 2 B
27 12 16 25 26 syl3anc A B 0 vol * A 2 B A + 1 2 B = A + 1 2 B A 2 B
28 19 recnd A B 0 A + 1
29 17 recnd A B 0 A
30 21 recnd A B 0 2 B
31 20 nnne0d A B 0 2 B 0
32 28 29 30 31 divsubdird A B 0 A + 1 - A 2 B = A + 1 2 B A 2 B
33 ax-1cn 1
34 pncan2 A 1 A + 1 - A = 1
35 29 33 34 sylancl A B 0 A + 1 - A = 1
36 35 oveq1d A B 0 A + 1 - A 2 B = 1 2 B
37 32 36 eqtr3d A B 0 A + 1 2 B A 2 B = 1 2 B
38 6 27 37 3eqtrd A B 0 vol * . A F B = 1 2 B