Metamath Proof Explorer

Theorem ruclem2

Description: Lemma for ruc . Ordering property for the input to D . (Contributed by Mario Carneiro, 28-May-2014)

Ref Expression
Hypotheses ruc.1 
|- ( ph -> F : NN --> RR )
ruc.2 
|- ( ph -> D = ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) ) )
ruclem1.3 
|- ( ph -> A e. RR )
ruclem1.4 
|- ( ph -> B e. RR )
ruclem1.5 
|- ( ph -> M e. RR )
ruclem1.6 
|- X = ( 1st ` ( <. A , B >. D M ) )
ruclem1.7 
|- Y = ( 2nd ` ( <. A , B >. D M ) )
ruclem2.8 
|- ( ph -> A < B )
Assertion ruclem2 
|- ( ph -> ( A <_ X /\ X < Y /\ Y <_ B ) )

Proof

Step Hyp Ref Expression
1 ruc.1 
 |-  ( ph -> F : NN --> RR )
2 ruc.2 
 |-  ( ph -> D = ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) ) )
3 ruclem1.3 
 |-  ( ph -> A e. RR )
4 ruclem1.4 
 |-  ( ph -> B e. RR )
5 ruclem1.5 
 |-  ( ph -> M e. RR )
6 ruclem1.6 
 |-  X = ( 1st ` ( <. A , B >. D M ) )
7 ruclem1.7 
 |-  Y = ( 2nd ` ( <. A , B >. D M ) )
8 ruclem2.8 
 |-  ( ph -> A < B )
9 3 leidd 
 |-  ( ph -> A <_ A )
10 3 4 readdcld 
 |-  ( ph -> ( A + B ) e. RR )
11 10 rehalfcld 
 |-  ( ph -> ( ( A + B ) / 2 ) e. RR )
12 11 4 readdcld 
 |-  ( ph -> ( ( ( A + B ) / 2 ) + B ) e. RR )
13 12 rehalfcld 
 |-  ( ph -> ( ( ( ( A + B ) / 2 ) + B ) / 2 ) e. RR )
14 avglt1 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> A < ( ( A + B ) / 2 ) ) )
15 3 4 14 syl2anc 
 |-  ( ph -> ( A < B <-> A < ( ( A + B ) / 2 ) ) )
16 8 15 mpbid 
 |-  ( ph -> A < ( ( A + B ) / 2 ) )
17 avglt2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( ( A + B ) / 2 ) < B ) )
18 3 4 17 syl2anc 
 |-  ( ph -> ( A < B <-> ( ( A + B ) / 2 ) < B ) )
19 8 18 mpbid 
 |-  ( ph -> ( ( A + B ) / 2 ) < B )
20 avglt1 
 |-  ( ( ( ( A + B ) / 2 ) e. RR /\ B e. RR ) -> ( ( ( A + B ) / 2 ) < B <-> ( ( A + B ) / 2 ) < ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) )
21 11 4 20 syl2anc 
 |-  ( ph -> ( ( ( A + B ) / 2 ) < B <-> ( ( A + B ) / 2 ) < ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) )
22 19 21 mpbid 
 |-  ( ph -> ( ( A + B ) / 2 ) < ( ( ( ( A + B ) / 2 ) + B ) / 2 ) )
23 3 11 13 16 22 lttrd 
 |-  ( ph -> A < ( ( ( ( A + B ) / 2 ) + B ) / 2 ) )
24 3 13 23 ltled 
 |-  ( ph -> A <_ ( ( ( ( A + B ) / 2 ) + B ) / 2 ) )
25 breq2 
 |-  ( A = if ( ( ( A + B ) / 2 ) < M , A , ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) -> ( A <_ A <-> A <_ if ( ( ( A + B ) / 2 ) < M , A , ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) ) )
26 breq2 
 |-  ( ( ( ( ( A + B ) / 2 ) + B ) / 2 ) = if ( ( ( A + B ) / 2 ) < M , A , ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) -> ( A <_ ( ( ( ( A + B ) / 2 ) + B ) / 2 ) <-> A <_ if ( ( ( A + B ) / 2 ) < M , A , ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) ) )
27 25 26 ifboth 
 |-  ( ( A <_ A /\ A <_ ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) -> A <_ if ( ( ( A + B ) / 2 ) < M , A , ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) )
28 9 24 27 syl2anc 
 |-  ( ph -> A <_ if ( ( ( A + B ) / 2 ) < M , A , ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) )
29 1 2 3 4 5 6 7 ruclem1 
 |-  ( ph -> ( ( <. A , B >. D M ) e. ( RR X. RR ) /\ X = if ( ( ( A + B ) / 2 ) < M , A , ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) /\ Y = if ( ( ( A + B ) / 2 ) < M , ( ( A + B ) / 2 ) , B ) ) )
30 29 simp2d 
 |-  ( ph -> X = if ( ( ( A + B ) / 2 ) < M , A , ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) )
31 28 30 breqtrrd 
 |-  ( ph -> A <_ X )
32 iftrue 
 |-  ( ( ( A + B ) / 2 ) < M -> if ( ( ( A + B ) / 2 ) < M , A , ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) = A )
33 iftrue 
 |-  ( ( ( A + B ) / 2 ) < M -> if ( ( ( A + B ) / 2 ) < M , ( ( A + B ) / 2 ) , B ) = ( ( A + B ) / 2 ) )
34 32 33 breq12d 
 |-  ( ( ( A + B ) / 2 ) < M -> ( if ( ( ( A + B ) / 2 ) < M , A , ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) < if ( ( ( A + B ) / 2 ) < M , ( ( A + B ) / 2 ) , B ) <-> A < ( ( A + B ) / 2 ) ) )
35 16 34 syl5ibrcom 
 |-  ( ph -> ( ( ( A + B ) / 2 ) < M -> if ( ( ( A + B ) / 2 ) < M , A , ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) < if ( ( ( A + B ) / 2 ) < M , ( ( A + B ) / 2 ) , B ) ) )
36 avglt2 
 |-  ( ( ( ( A + B ) / 2 ) e. RR /\ B e. RR ) -> ( ( ( A + B ) / 2 ) < B <-> ( ( ( ( A + B ) / 2 ) + B ) / 2 ) < B ) )
37 11 4 36 syl2anc 
 |-  ( ph -> ( ( ( A + B ) / 2 ) < B <-> ( ( ( ( A + B ) / 2 ) + B ) / 2 ) < B ) )
38 19 37 mpbid 
 |-  ( ph -> ( ( ( ( A + B ) / 2 ) + B ) / 2 ) < B )
39 iffalse 
 |-  ( -. ( ( A + B ) / 2 ) < M -> if ( ( ( A + B ) / 2 ) < M , A , ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) = ( ( ( ( A + B ) / 2 ) + B ) / 2 ) )
40 iffalse 
 |-  ( -. ( ( A + B ) / 2 ) < M -> if ( ( ( A + B ) / 2 ) < M , ( ( A + B ) / 2 ) , B ) = B )
41 39 40 breq12d 
 |-  ( -. ( ( A + B ) / 2 ) < M -> ( if ( ( ( A + B ) / 2 ) < M , A , ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) < if ( ( ( A + B ) / 2 ) < M , ( ( A + B ) / 2 ) , B ) <-> ( ( ( ( A + B ) / 2 ) + B ) / 2 ) < B ) )
42 38 41 syl5ibrcom 
 |-  ( ph -> ( -. ( ( A + B ) / 2 ) < M -> if ( ( ( A + B ) / 2 ) < M , A , ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) < if ( ( ( A + B ) / 2 ) < M , ( ( A + B ) / 2 ) , B ) ) )
43 35 42 pm2.61d 
 |-  ( ph -> if ( ( ( A + B ) / 2 ) < M , A , ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) < if ( ( ( A + B ) / 2 ) < M , ( ( A + B ) / 2 ) , B ) )
44 29 simp3d 
 |-  ( ph -> Y = if ( ( ( A + B ) / 2 ) < M , ( ( A + B ) / 2 ) , B ) )
45 43 30 44 3brtr4d 
 |-  ( ph -> X < Y )
46 11 4 19 ltled 
 |-  ( ph -> ( ( A + B ) / 2 ) <_ B )
47 4 leidd 
 |-  ( ph -> B <_ B )
48 breq1 
 |-  ( ( ( A + B ) / 2 ) = if ( ( ( A + B ) / 2 ) < M , ( ( A + B ) / 2 ) , B ) -> ( ( ( A + B ) / 2 ) <_ B <-> if ( ( ( A + B ) / 2 ) < M , ( ( A + B ) / 2 ) , B ) <_ B ) )
49 breq1 
 |-  ( B = if ( ( ( A + B ) / 2 ) < M , ( ( A + B ) / 2 ) , B ) -> ( B <_ B <-> if ( ( ( A + B ) / 2 ) < M , ( ( A + B ) / 2 ) , B ) <_ B ) )
50 48 49 ifboth 
 |-  ( ( ( ( A + B ) / 2 ) <_ B /\ B <_ B ) -> if ( ( ( A + B ) / 2 ) < M , ( ( A + B ) / 2 ) , B ) <_ B )
51 46 47 50 syl2anc 
 |-  ( ph -> if ( ( ( A + B ) / 2 ) < M , ( ( A + B ) / 2 ) , B ) <_ B )
52 44 51 eqbrtrd 
 |-  ( ph -> Y <_ B )
53 31 45 52 3jca 
 |-  ( ph -> ( A <_ X /\ X < Y /\ Y <_ B ) )