Metamath Proof Explorer


Theorem dyaddisjlem

Description: Lemma for dyaddisj . (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypothesis dyadmbl.1
|- F = ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. )
Assertion dyaddisjlem
|- ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) \/ ( [,] ` ( B F D ) ) C_ ( [,] ` ( A F C ) ) \/ ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) ) )

Proof

Step Hyp Ref Expression
1 dyadmbl.1
 |-  F = ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. )
2 simplll
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> A e. ZZ )
3 simplrl
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> C e. NN0 )
4 1 dyadval
 |-  ( ( A e. ZZ /\ C e. NN0 ) -> ( A F C ) = <. ( A / ( 2 ^ C ) ) , ( ( A + 1 ) / ( 2 ^ C ) ) >. )
5 2 3 4 syl2anc
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( A F C ) = <. ( A / ( 2 ^ C ) ) , ( ( A + 1 ) / ( 2 ^ C ) ) >. )
6 5 fveq2d
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( (,) ` ( A F C ) ) = ( (,) ` <. ( A / ( 2 ^ C ) ) , ( ( A + 1 ) / ( 2 ^ C ) ) >. ) )
7 df-ov
 |-  ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) = ( (,) ` <. ( A / ( 2 ^ C ) ) , ( ( A + 1 ) / ( 2 ^ C ) ) >. )
8 6 7 eqtr4di
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( (,) ` ( A F C ) ) = ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) )
9 simpllr
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> B e. ZZ )
10 simplrr
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> D e. NN0 )
11 1 dyadval
 |-  ( ( B e. ZZ /\ D e. NN0 ) -> ( B F D ) = <. ( B / ( 2 ^ D ) ) , ( ( B + 1 ) / ( 2 ^ D ) ) >. )
12 9 10 11 syl2anc
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( B F D ) = <. ( B / ( 2 ^ D ) ) , ( ( B + 1 ) / ( 2 ^ D ) ) >. )
13 12 fveq2d
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( (,) ` ( B F D ) ) = ( (,) ` <. ( B / ( 2 ^ D ) ) , ( ( B + 1 ) / ( 2 ^ D ) ) >. ) )
14 df-ov
 |-  ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) = ( (,) ` <. ( B / ( 2 ^ D ) ) , ( ( B + 1 ) / ( 2 ^ D ) ) >. )
15 13 14 eqtr4di
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( (,) ` ( B F D ) ) = ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) )
16 8 15 ineq12d
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = ( ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) i^i ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) ) )
17 incom
 |-  ( ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) i^i ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) ) = ( ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) i^i ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) )
18 16 17 eqtrdi
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = ( ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) i^i ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) ) )
19 18 adantr
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( B / ( 2 ^ D ) ) < ( A / ( 2 ^ C ) ) ) -> ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = ( ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) i^i ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) ) )
20 2 zred
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> A e. RR )
21 20 recnd
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> A e. CC )
22 2nn
 |-  2 e. NN
23 nnexpcl
 |-  ( ( 2 e. NN /\ C e. NN0 ) -> ( 2 ^ C ) e. NN )
24 22 3 23 sylancr
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( 2 ^ C ) e. NN )
25 24 nncnd
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( 2 ^ C ) e. CC )
26 nnexpcl
 |-  ( ( 2 e. NN /\ D e. NN0 ) -> ( 2 ^ D ) e. NN )
27 22 10 26 sylancr
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( 2 ^ D ) e. NN )
28 27 nncnd
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( 2 ^ D ) e. CC )
29 24 nnne0d
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( 2 ^ C ) =/= 0 )
30 21 25 28 29 div13d
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) = ( ( ( 2 ^ D ) / ( 2 ^ C ) ) x. A ) )
31 2cnd
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> 2 e. CC )
32 2ne0
 |-  2 =/= 0
33 32 a1i
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> 2 =/= 0 )
34 3 nn0zd
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> C e. ZZ )
35 10 nn0zd
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> D e. ZZ )
36 31 33 34 35 expsubd
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( 2 ^ ( D - C ) ) = ( ( 2 ^ D ) / ( 2 ^ C ) ) )
37 2z
 |-  2 e. ZZ
38 simpr
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> C <_ D )
39 znn0sub
 |-  ( ( C e. ZZ /\ D e. ZZ ) -> ( C <_ D <-> ( D - C ) e. NN0 ) )
40 34 35 39 syl2anc
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( C <_ D <-> ( D - C ) e. NN0 ) )
41 38 40 mpbid
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( D - C ) e. NN0 )
42 zexpcl
 |-  ( ( 2 e. ZZ /\ ( D - C ) e. NN0 ) -> ( 2 ^ ( D - C ) ) e. ZZ )
43 37 41 42 sylancr
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( 2 ^ ( D - C ) ) e. ZZ )
44 36 43 eqeltrrd
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( 2 ^ D ) / ( 2 ^ C ) ) e. ZZ )
45 44 2 zmulcld
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( ( 2 ^ D ) / ( 2 ^ C ) ) x. A ) e. ZZ )
46 30 45 eqeltrd
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) e. ZZ )
47 zltp1le
 |-  ( ( B e. ZZ /\ ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) e. ZZ ) -> ( B < ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) <-> ( B + 1 ) <_ ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
48 9 46 47 syl2anc
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( B < ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) <-> ( B + 1 ) <_ ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
49 9 zred
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> B e. RR )
50 20 24 nndivred
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( A / ( 2 ^ C ) ) e. RR )
51 27 nnred
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( 2 ^ D ) e. RR )
52 27 nngt0d
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> 0 < ( 2 ^ D ) )
53 ltdivmul2
 |-  ( ( B e. RR /\ ( A / ( 2 ^ C ) ) e. RR /\ ( ( 2 ^ D ) e. RR /\ 0 < ( 2 ^ D ) ) ) -> ( ( B / ( 2 ^ D ) ) < ( A / ( 2 ^ C ) ) <-> B < ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
54 49 50 51 52 53 syl112anc
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( B / ( 2 ^ D ) ) < ( A / ( 2 ^ C ) ) <-> B < ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
55 peano2re
 |-  ( B e. RR -> ( B + 1 ) e. RR )
56 49 55 syl
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( B + 1 ) e. RR )
57 ledivmul2
 |-  ( ( ( B + 1 ) e. RR /\ ( A / ( 2 ^ C ) ) e. RR /\ ( ( 2 ^ D ) e. RR /\ 0 < ( 2 ^ D ) ) ) -> ( ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( A / ( 2 ^ C ) ) <-> ( B + 1 ) <_ ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
58 56 50 51 52 57 syl112anc
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( A / ( 2 ^ C ) ) <-> ( B + 1 ) <_ ( ( A / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
59 48 54 58 3bitr4d
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( B / ( 2 ^ D ) ) < ( A / ( 2 ^ C ) ) <-> ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( A / ( 2 ^ C ) ) ) )
60 49 27 nndivred
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( B / ( 2 ^ D ) ) e. RR )
61 60 rexrd
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( B / ( 2 ^ D ) ) e. RR* )
62 56 27 nndivred
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( B + 1 ) / ( 2 ^ D ) ) e. RR )
63 62 rexrd
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( B + 1 ) / ( 2 ^ D ) ) e. RR* )
64 50 rexrd
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( A / ( 2 ^ C ) ) e. RR* )
65 peano2re
 |-  ( A e. RR -> ( A + 1 ) e. RR )
66 20 65 syl
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( A + 1 ) e. RR )
67 66 24 nndivred
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( A + 1 ) / ( 2 ^ C ) ) e. RR )
68 67 rexrd
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( A + 1 ) / ( 2 ^ C ) ) e. RR* )
69 ioodisj
 |-  ( ( ( ( ( B / ( 2 ^ D ) ) e. RR* /\ ( ( B + 1 ) / ( 2 ^ D ) ) e. RR* ) /\ ( ( A / ( 2 ^ C ) ) e. RR* /\ ( ( A + 1 ) / ( 2 ^ C ) ) e. RR* ) ) /\ ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( A / ( 2 ^ C ) ) ) -> ( ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) i^i ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) ) = (/) )
70 69 ex
 |-  ( ( ( ( B / ( 2 ^ D ) ) e. RR* /\ ( ( B + 1 ) / ( 2 ^ D ) ) e. RR* ) /\ ( ( A / ( 2 ^ C ) ) e. RR* /\ ( ( A + 1 ) / ( 2 ^ C ) ) e. RR* ) ) -> ( ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( A / ( 2 ^ C ) ) -> ( ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) i^i ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) ) = (/) ) )
71 61 63 64 68 70 syl22anc
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( A / ( 2 ^ C ) ) -> ( ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) i^i ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) ) = (/) ) )
72 59 71 sylbid
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( B / ( 2 ^ D ) ) < ( A / ( 2 ^ C ) ) -> ( ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) i^i ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) ) = (/) ) )
73 72 imp
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( B / ( 2 ^ D ) ) < ( A / ( 2 ^ C ) ) ) -> ( ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) i^i ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) ) = (/) )
74 19 73 eqtrd
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( B / ( 2 ^ D ) ) < ( A / ( 2 ^ C ) ) ) -> ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) )
75 74 3mix3d
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( B / ( 2 ^ D ) ) < ( A / ( 2 ^ C ) ) ) -> ( ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) \/ ( [,] ` ( B F D ) ) C_ ( [,] ` ( A F C ) ) \/ ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) ) )
76 50 adantr
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( A / ( 2 ^ C ) ) e. RR )
77 67 adantr
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( ( A + 1 ) / ( 2 ^ C ) ) e. RR )
78 simprl
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) )
79 66 recnd
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( A + 1 ) e. CC )
80 79 25 28 29 div13d
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) = ( ( ( 2 ^ D ) / ( 2 ^ C ) ) x. ( A + 1 ) ) )
81 2 peano2zd
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( A + 1 ) e. ZZ )
82 44 81 zmulcld
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( ( 2 ^ D ) / ( 2 ^ C ) ) x. ( A + 1 ) ) e. ZZ )
83 80 82 eqeltrd
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) e. ZZ )
84 zltp1le
 |-  ( ( B e. ZZ /\ ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) e. ZZ ) -> ( B < ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) <-> ( B + 1 ) <_ ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
85 9 83 84 syl2anc
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( B < ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) <-> ( B + 1 ) <_ ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
86 ltdivmul2
 |-  ( ( B e. RR /\ ( ( A + 1 ) / ( 2 ^ C ) ) e. RR /\ ( ( 2 ^ D ) e. RR /\ 0 < ( 2 ^ D ) ) ) -> ( ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) <-> B < ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
87 49 67 51 52 86 syl112anc
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) <-> B < ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
88 ledivmul2
 |-  ( ( ( B + 1 ) e. RR /\ ( ( A + 1 ) / ( 2 ^ C ) ) e. RR /\ ( ( 2 ^ D ) e. RR /\ 0 < ( 2 ^ D ) ) ) -> ( ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( ( A + 1 ) / ( 2 ^ C ) ) <-> ( B + 1 ) <_ ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
89 56 67 51 52 88 syl112anc
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( ( A + 1 ) / ( 2 ^ C ) ) <-> ( B + 1 ) <_ ( ( ( A + 1 ) / ( 2 ^ C ) ) x. ( 2 ^ D ) ) ) )
90 85 87 89 3bitr4d
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) <-> ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( ( A + 1 ) / ( 2 ^ C ) ) ) )
91 90 biimpa
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) -> ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( ( A + 1 ) / ( 2 ^ C ) ) )
92 91 adantrl
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( ( A + 1 ) / ( 2 ^ C ) ) )
93 iccss
 |-  ( ( ( ( A / ( 2 ^ C ) ) e. RR /\ ( ( A + 1 ) / ( 2 ^ C ) ) e. RR ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( ( B + 1 ) / ( 2 ^ D ) ) <_ ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( ( B / ( 2 ^ D ) ) [,] ( ( B + 1 ) / ( 2 ^ D ) ) ) C_ ( ( A / ( 2 ^ C ) ) [,] ( ( A + 1 ) / ( 2 ^ C ) ) ) )
94 76 77 78 92 93 syl22anc
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( ( B / ( 2 ^ D ) ) [,] ( ( B + 1 ) / ( 2 ^ D ) ) ) C_ ( ( A / ( 2 ^ C ) ) [,] ( ( A + 1 ) / ( 2 ^ C ) ) ) )
95 12 fveq2d
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( [,] ` ( B F D ) ) = ( [,] ` <. ( B / ( 2 ^ D ) ) , ( ( B + 1 ) / ( 2 ^ D ) ) >. ) )
96 df-ov
 |-  ( ( B / ( 2 ^ D ) ) [,] ( ( B + 1 ) / ( 2 ^ D ) ) ) = ( [,] ` <. ( B / ( 2 ^ D ) ) , ( ( B + 1 ) / ( 2 ^ D ) ) >. )
97 95 96 eqtr4di
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( [,] ` ( B F D ) ) = ( ( B / ( 2 ^ D ) ) [,] ( ( B + 1 ) / ( 2 ^ D ) ) ) )
98 97 adantr
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( [,] ` ( B F D ) ) = ( ( B / ( 2 ^ D ) ) [,] ( ( B + 1 ) / ( 2 ^ D ) ) ) )
99 5 fveq2d
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( [,] ` ( A F C ) ) = ( [,] ` <. ( A / ( 2 ^ C ) ) , ( ( A + 1 ) / ( 2 ^ C ) ) >. ) )
100 df-ov
 |-  ( ( A / ( 2 ^ C ) ) [,] ( ( A + 1 ) / ( 2 ^ C ) ) ) = ( [,] ` <. ( A / ( 2 ^ C ) ) , ( ( A + 1 ) / ( 2 ^ C ) ) >. )
101 99 100 eqtr4di
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( [,] ` ( A F C ) ) = ( ( A / ( 2 ^ C ) ) [,] ( ( A + 1 ) / ( 2 ^ C ) ) ) )
102 101 adantr
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( [,] ` ( A F C ) ) = ( ( A / ( 2 ^ C ) ) [,] ( ( A + 1 ) / ( 2 ^ C ) ) ) )
103 94 98 102 3sstr4d
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( [,] ` ( B F D ) ) C_ ( [,] ` ( A F C ) ) )
104 103 3mix2d
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) ) -> ( ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) \/ ( [,] ` ( B F D ) ) C_ ( [,] ` ( A F C ) ) \/ ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) ) )
105 104 anassrs
 |-  ( ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) /\ ( B / ( 2 ^ D ) ) < ( ( A + 1 ) / ( 2 ^ C ) ) ) -> ( ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) \/ ( [,] ` ( B F D ) ) C_ ( [,] ` ( A F C ) ) \/ ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) ) )
106 16 adantr
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) -> ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = ( ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) i^i ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) ) )
107 ioodisj
 |-  ( ( ( ( ( A / ( 2 ^ C ) ) e. RR* /\ ( ( A + 1 ) / ( 2 ^ C ) ) e. RR* ) /\ ( ( B / ( 2 ^ D ) ) e. RR* /\ ( ( B + 1 ) / ( 2 ^ D ) ) e. RR* ) ) /\ ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) -> ( ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) i^i ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) ) = (/) )
108 107 ex
 |-  ( ( ( ( A / ( 2 ^ C ) ) e. RR* /\ ( ( A + 1 ) / ( 2 ^ C ) ) e. RR* ) /\ ( ( B / ( 2 ^ D ) ) e. RR* /\ ( ( B + 1 ) / ( 2 ^ D ) ) e. RR* ) ) -> ( ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) -> ( ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) i^i ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) ) = (/) ) )
109 64 68 61 63 108 syl22anc
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) -> ( ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) i^i ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) ) = (/) ) )
110 109 imp
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) -> ( ( ( A / ( 2 ^ C ) ) (,) ( ( A + 1 ) / ( 2 ^ C ) ) ) i^i ( ( B / ( 2 ^ D ) ) (,) ( ( B + 1 ) / ( 2 ^ D ) ) ) ) = (/) )
111 106 110 eqtrd
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) -> ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) )
112 111 3mix3d
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) -> ( ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) \/ ( [,] ` ( B F D ) ) C_ ( [,] ` ( A F C ) ) \/ ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) ) )
113 112 adantlr
 |-  ( ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) /\ ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) -> ( ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) \/ ( [,] ` ( B F D ) ) C_ ( [,] ` ( A F C ) ) \/ ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) ) )
114 60 adantr
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) -> ( B / ( 2 ^ D ) ) e. RR )
115 67 adantr
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) -> ( ( A + 1 ) / ( 2 ^ C ) ) e. RR )
116 105 113 114 115 ltlecasei
 |-  ( ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) /\ ( A / ( 2 ^ C ) ) <_ ( B / ( 2 ^ D ) ) ) -> ( ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) \/ ( [,] ` ( B F D ) ) C_ ( [,] ` ( A F C ) ) \/ ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) ) )
117 75 116 60 50 ltlecasei
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) /\ C <_ D ) -> ( ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) \/ ( [,] ` ( B F D ) ) C_ ( [,] ` ( A F C ) ) \/ ( ( (,) ` ( A F C ) ) i^i ( (,) ` ( B F D ) ) ) = (/) ) )