Metamath Proof Explorer

Theorem dyadmaxlem

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

Ref Expression
Hypotheses dyadmbl.1 
|- F = ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. )
dyadmax.2 
|- ( ph -> A e. ZZ )
dyadmax.3 
|- ( ph -> B e. ZZ )
dyadmax.4 
|- ( ph -> C e. NN0 )
dyadmax.5 
|- ( ph -> D e. NN0 )
dyadmax.6 
|- ( ph -> -. D < C )
dyadmax.7 
|- ( ph -> ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) )
Assertion dyadmaxlem 
|- ( ph -> ( A = B /\ C = D ) )

Proof

Step Hyp Ref Expression
1 dyadmbl.1 
 |-  F = ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. )
2 dyadmax.2 
 |-  ( ph -> A e. ZZ )
3 dyadmax.3 
 |-  ( ph -> B e. ZZ )
4 dyadmax.4 
 |-  ( ph -> C e. NN0 )
5 dyadmax.5 
 |-  ( ph -> D e. NN0 )
6 dyadmax.6 
 |-  ( ph -> -. D < C )
7 dyadmax.7 
 |-  ( ph -> ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) )
8 1 dyadval 
 |-  ( ( A e. ZZ /\ C e. NN0 ) -> ( A F C ) = <. ( A / ( 2 ^ C ) ) , ( ( A + 1 ) / ( 2 ^ C ) ) >. )
9 2 4 8 syl2anc 
 |-  ( ph -> ( A F C ) = <. ( A / ( 2 ^ C ) ) , ( ( A + 1 ) / ( 2 ^ C ) ) >. )
10 9 fveq2d 
 |-  ( ph -> ( [,] ` ( A F C ) ) = ( [,] ` <. ( A / ( 2 ^ C ) ) , ( ( A + 1 ) / ( 2 ^ C ) ) >. ) )
11 df-ov 
 |-  ( ( A / ( 2 ^ C ) ) [,] ( ( A + 1 ) / ( 2 ^ C ) ) ) = ( [,] ` <. ( A / ( 2 ^ C ) ) , ( ( A + 1 ) / ( 2 ^ C ) ) >. )
12 10 11 eqtr4di 
 |-  ( ph -> ( [,] ` ( A F C ) ) = ( ( A / ( 2 ^ C ) ) [,] ( ( A + 1 ) / ( 2 ^ C ) ) ) )
13 1 dyadss 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. NN0 /\ D e. NN0 ) ) -> ( ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) -> D <_ C ) )
14 2 3 4 5 13 syl22anc 
 |-  ( ph -> ( ( [,] ` ( A F C ) ) C_ ( [,] ` ( B F D ) ) -> D <_ C ) )
15 7 14 mpd 
 |-  ( ph -> D <_ C )
16 5 nn0red 
 |-  ( ph -> D e. RR )
17 4 nn0red 
 |-  ( ph -> C e. RR )
18 16 17 eqleltd 
 |-  ( ph -> ( D = C <-> ( D <_ C /\ -. D < C ) ) )
19 15 6 18 mpbir2and 
 |-  ( ph -> D = C )
20 19 oveq2d 
 |-  ( ph -> ( B F D ) = ( B F C ) )
21 1 dyadval 
 |-  ( ( B e. ZZ /\ C e. NN0 ) -> ( B F C ) = <. ( B / ( 2 ^ C ) ) , ( ( B + 1 ) / ( 2 ^ C ) ) >. )
22 3 4 21 syl2anc 
 |-  ( ph -> ( B F C ) = <. ( B / ( 2 ^ C ) ) , ( ( B + 1 ) / ( 2 ^ C ) ) >. )
23 20 22 eqtrd 
 |-  ( ph -> ( B F D ) = <. ( B / ( 2 ^ C ) ) , ( ( B + 1 ) / ( 2 ^ C ) ) >. )
24 23 fveq2d 
 |-  ( ph -> ( [,] ` ( B F D ) ) = ( [,] ` <. ( B / ( 2 ^ C ) ) , ( ( B + 1 ) / ( 2 ^ C ) ) >. ) )
25 df-ov 
 |-  ( ( B / ( 2 ^ C ) ) [,] ( ( B + 1 ) / ( 2 ^ C ) ) ) = ( [,] ` <. ( B / ( 2 ^ C ) ) , ( ( B + 1 ) / ( 2 ^ C ) ) >. )
26 24 25 eqtr4di 
 |-  ( ph -> ( [,] ` ( B F D ) ) = ( ( B / ( 2 ^ C ) ) [,] ( ( B + 1 ) / ( 2 ^ C ) ) ) )
27 7 12 26 3sstr3d 
 |-  ( ph -> ( ( A / ( 2 ^ C ) ) [,] ( ( A + 1 ) / ( 2 ^ C ) ) ) C_ ( ( B / ( 2 ^ C ) ) [,] ( ( B + 1 ) / ( 2 ^ C ) ) ) )
28 2 zred 
 |-  ( ph -> A e. RR )
29 2nn 
 |-  2 e. NN
30 nnexpcl 
 |-  ( ( 2 e. NN /\ C e. NN0 ) -> ( 2 ^ C ) e. NN )
31 29 4 30 sylancr 
 |-  ( ph -> ( 2 ^ C ) e. NN )
32 28 31 nndivred 
 |-  ( ph -> ( A / ( 2 ^ C ) ) e. RR )
33 32 rexrd 
 |-  ( ph -> ( A / ( 2 ^ C ) ) e. RR* )
34 peano2re 
 |-  ( A e. RR -> ( A + 1 ) e. RR )
35 28 34 syl 
 |-  ( ph -> ( A + 1 ) e. RR )
36 35 31 nndivred 
 |-  ( ph -> ( ( A + 1 ) / ( 2 ^ C ) ) e. RR )
37 36 rexrd 
 |-  ( ph -> ( ( A + 1 ) / ( 2 ^ C ) ) e. RR* )
38 28 lep1d 
 |-  ( ph -> A <_ ( A + 1 ) )
39 31 nnred 
 |-  ( ph -> ( 2 ^ C ) e. RR )
40 31 nngt0d 
 |-  ( ph -> 0 < ( 2 ^ C ) )
41 lediv1 
 |-  ( ( A e. RR /\ ( A + 1 ) e. RR /\ ( ( 2 ^ C ) e. RR /\ 0 < ( 2 ^ C ) ) ) -> ( A <_ ( A + 1 ) <-> ( A / ( 2 ^ C ) ) <_ ( ( A + 1 ) / ( 2 ^ C ) ) ) )
42 28 35 39 40 41 syl112anc 
 |-  ( ph -> ( A <_ ( A + 1 ) <-> ( A / ( 2 ^ C ) ) <_ ( ( A + 1 ) / ( 2 ^ C ) ) ) )
43 38 42 mpbid 
 |-  ( ph -> ( A / ( 2 ^ C ) ) <_ ( ( A + 1 ) / ( 2 ^ C ) ) )
44 ubicc2 
 |-  ( ( ( A / ( 2 ^ C ) ) e. RR* /\ ( ( A + 1 ) / ( 2 ^ C ) ) e. RR* /\ ( A / ( 2 ^ C ) ) <_ ( ( A + 1 ) / ( 2 ^ C ) ) ) -> ( ( A + 1 ) / ( 2 ^ C ) ) e. ( ( A / ( 2 ^ C ) ) [,] ( ( A + 1 ) / ( 2 ^ C ) ) ) )
45 33 37 43 44 syl3anc 
 |-  ( ph -> ( ( A + 1 ) / ( 2 ^ C ) ) e. ( ( A / ( 2 ^ C ) ) [,] ( ( A + 1 ) / ( 2 ^ C ) ) ) )
46 27 45 sseldd 
 |-  ( ph -> ( ( A + 1 ) / ( 2 ^ C ) ) e. ( ( B / ( 2 ^ C ) ) [,] ( ( B + 1 ) / ( 2 ^ C ) ) ) )
47 3 zred 
 |-  ( ph -> B e. RR )
48 47 31 nndivred 
 |-  ( ph -> ( B / ( 2 ^ C ) ) e. RR )
49 peano2re 
 |-  ( B e. RR -> ( B + 1 ) e. RR )
50 47 49 syl 
 |-  ( ph -> ( B + 1 ) e. RR )
51 50 31 nndivred 
 |-  ( ph -> ( ( B + 1 ) / ( 2 ^ C ) ) e. RR )
52 elicc2 
 |-  ( ( ( B / ( 2 ^ C ) ) e. RR /\ ( ( B + 1 ) / ( 2 ^ C ) ) e. RR ) -> ( ( ( A + 1 ) / ( 2 ^ C ) ) e. ( ( B / ( 2 ^ C ) ) [,] ( ( B + 1 ) / ( 2 ^ C ) ) ) <-> ( ( ( A + 1 ) / ( 2 ^ C ) ) e. RR /\ ( B / ( 2 ^ C ) ) <_ ( ( A + 1 ) / ( 2 ^ C ) ) /\ ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( ( B + 1 ) / ( 2 ^ C ) ) ) ) )
53 48 51 52 syl2anc 
 |-  ( ph -> ( ( ( A + 1 ) / ( 2 ^ C ) ) e. ( ( B / ( 2 ^ C ) ) [,] ( ( B + 1 ) / ( 2 ^ C ) ) ) <-> ( ( ( A + 1 ) / ( 2 ^ C ) ) e. RR /\ ( B / ( 2 ^ C ) ) <_ ( ( A + 1 ) / ( 2 ^ C ) ) /\ ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( ( B + 1 ) / ( 2 ^ C ) ) ) ) )
54 46 53 mpbid 
 |-  ( ph -> ( ( ( A + 1 ) / ( 2 ^ C ) ) e. RR /\ ( B / ( 2 ^ C ) ) <_ ( ( A + 1 ) / ( 2 ^ C ) ) /\ ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( ( B + 1 ) / ( 2 ^ C ) ) ) )
55 54 simp3d 
 |-  ( ph -> ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( ( B + 1 ) / ( 2 ^ C ) ) )
56 lediv1 
 |-  ( ( ( A + 1 ) e. RR /\ ( B + 1 ) e. RR /\ ( ( 2 ^ C ) e. RR /\ 0 < ( 2 ^ C ) ) ) -> ( ( A + 1 ) <_ ( B + 1 ) <-> ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( ( B + 1 ) / ( 2 ^ C ) ) ) )
57 35 50 39 40 56 syl112anc 
 |-  ( ph -> ( ( A + 1 ) <_ ( B + 1 ) <-> ( ( A + 1 ) / ( 2 ^ C ) ) <_ ( ( B + 1 ) / ( 2 ^ C ) ) ) )
58 55 57 mpbird 
 |-  ( ph -> ( A + 1 ) <_ ( B + 1 ) )
59 1red 
 |-  ( ph -> 1 e. RR )
60 28 47 59 leadd1d 
 |-  ( ph -> ( A <_ B <-> ( A + 1 ) <_ ( B + 1 ) ) )
61 58 60 mpbird 
 |-  ( ph -> A <_ B )
62 lbicc2 
 |-  ( ( ( A / ( 2 ^ C ) ) e. RR* /\ ( ( A + 1 ) / ( 2 ^ C ) ) e. RR* /\ ( A / ( 2 ^ C ) ) <_ ( ( A + 1 ) / ( 2 ^ C ) ) ) -> ( A / ( 2 ^ C ) ) e. ( ( A / ( 2 ^ C ) ) [,] ( ( A + 1 ) / ( 2 ^ C ) ) ) )
63 33 37 43 62 syl3anc 
 |-  ( ph -> ( A / ( 2 ^ C ) ) e. ( ( A / ( 2 ^ C ) ) [,] ( ( A + 1 ) / ( 2 ^ C ) ) ) )
64 27 63 sseldd 
 |-  ( ph -> ( A / ( 2 ^ C ) ) e. ( ( B / ( 2 ^ C ) ) [,] ( ( B + 1 ) / ( 2 ^ C ) ) ) )
65 elicc2 
 |-  ( ( ( B / ( 2 ^ C ) ) e. RR /\ ( ( B + 1 ) / ( 2 ^ C ) ) e. RR ) -> ( ( A / ( 2 ^ C ) ) e. ( ( B / ( 2 ^ C ) ) [,] ( ( B + 1 ) / ( 2 ^ C ) ) ) <-> ( ( A / ( 2 ^ C ) ) e. RR /\ ( B / ( 2 ^ C ) ) <_ ( A / ( 2 ^ C ) ) /\ ( A / ( 2 ^ C ) ) <_ ( ( B + 1 ) / ( 2 ^ C ) ) ) ) )
66 48 51 65 syl2anc 
 |-  ( ph -> ( ( A / ( 2 ^ C ) ) e. ( ( B / ( 2 ^ C ) ) [,] ( ( B + 1 ) / ( 2 ^ C ) ) ) <-> ( ( A / ( 2 ^ C ) ) e. RR /\ ( B / ( 2 ^ C ) ) <_ ( A / ( 2 ^ C ) ) /\ ( A / ( 2 ^ C ) ) <_ ( ( B + 1 ) / ( 2 ^ C ) ) ) ) )
67 64 66 mpbid 
 |-  ( ph -> ( ( A / ( 2 ^ C ) ) e. RR /\ ( B / ( 2 ^ C ) ) <_ ( A / ( 2 ^ C ) ) /\ ( A / ( 2 ^ C ) ) <_ ( ( B + 1 ) / ( 2 ^ C ) ) ) )
68 67 simp2d 
 |-  ( ph -> ( B / ( 2 ^ C ) ) <_ ( A / ( 2 ^ C ) ) )
69 lediv1 
 |-  ( ( B e. RR /\ A e. RR /\ ( ( 2 ^ C ) e. RR /\ 0 < ( 2 ^ C ) ) ) -> ( B <_ A <-> ( B / ( 2 ^ C ) ) <_ ( A / ( 2 ^ C ) ) ) )
70 47 28 39 40 69 syl112anc 
 |-  ( ph -> ( B <_ A <-> ( B / ( 2 ^ C ) ) <_ ( A / ( 2 ^ C ) ) ) )
71 68 70 mpbird 
 |-  ( ph -> B <_ A )
72 28 47 letri3d 
 |-  ( ph -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )
73 61 71 72 mpbir2and 
 |-  ( ph -> A = B )
74 19 eqcomd 
 |-  ( ph -> C = D )
75 73 74 jca 
 |-  ( ph -> ( A = B /\ C = D ) )