Metamath Proof Explorer

Theorem ruclem3

Description: Lemma for ruc . The constructed interval [ X , Y ] always excludes M . (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 ruclem3 
|- ( ph -> ( M < X \/ Y < M ) )

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 4 readdcld 
 |-  ( ph -> ( A + B ) e. RR )
10 9 rehalfcld 
 |-  ( ph -> ( ( A + B ) / 2 ) e. RR )
11 5 10 lenltd 
 |-  ( ph -> ( M <_ ( ( A + B ) / 2 ) <-> -. ( ( A + B ) / 2 ) < M ) )
12 avglt2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( ( A + B ) / 2 ) < B ) )
13 3 4 12 syl2anc 
 |-  ( ph -> ( A < B <-> ( ( A + B ) / 2 ) < B ) )
14 8 13 mpbid 
 |-  ( ph -> ( ( A + B ) / 2 ) < B )
15 avglt1 
 |-  ( ( ( ( A + B ) / 2 ) e. RR /\ B e. RR ) -> ( ( ( A + B ) / 2 ) < B <-> ( ( A + B ) / 2 ) < ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) )
16 10 4 15 syl2anc 
 |-  ( ph -> ( ( ( A + B ) / 2 ) < B <-> ( ( A + B ) / 2 ) < ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) )
17 14 16 mpbid 
 |-  ( ph -> ( ( A + B ) / 2 ) < ( ( ( ( A + B ) / 2 ) + B ) / 2 ) )
18 10 4 readdcld 
 |-  ( ph -> ( ( ( A + B ) / 2 ) + B ) e. RR )
19 18 rehalfcld 
 |-  ( ph -> ( ( ( ( A + B ) / 2 ) + B ) / 2 ) e. RR )
20 lelttr 
 |-  ( ( M e. RR /\ ( ( A + B ) / 2 ) e. RR /\ ( ( ( ( A + B ) / 2 ) + B ) / 2 ) e. RR ) -> ( ( M <_ ( ( A + B ) / 2 ) /\ ( ( A + B ) / 2 ) < ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) -> M < ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) )
21 5 10 19 20 syl3anc 
 |-  ( ph -> ( ( M <_ ( ( A + B ) / 2 ) /\ ( ( A + B ) / 2 ) < ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) -> M < ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) )
22 17 21 mpan2d 
 |-  ( ph -> ( M <_ ( ( A + B ) / 2 ) -> M < ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) )
23 11 22 sylbird 
 |-  ( ph -> ( -. ( ( A + B ) / 2 ) < M -> M < ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) )
24 23 imp 
 |-  ( ( ph /\ -. ( ( A + B ) / 2 ) < M ) -> M < ( ( ( ( A + B ) / 2 ) + B ) / 2 ) )
25 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 ) ) )
26 25 simp2d 
 |-  ( ph -> X = if ( ( ( A + B ) / 2 ) < M , A , ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) )
27 iffalse 
 |-  ( -. ( ( A + B ) / 2 ) < M -> if ( ( ( A + B ) / 2 ) < M , A , ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) = ( ( ( ( A + B ) / 2 ) + B ) / 2 ) )
28 26 27 sylan9eq 
 |-  ( ( ph /\ -. ( ( A + B ) / 2 ) < M ) -> X = ( ( ( ( A + B ) / 2 ) + B ) / 2 ) )
29 24 28 breqtrrd 
 |-  ( ( ph /\ -. ( ( A + B ) / 2 ) < M ) -> M < X )
30 29 ex 
 |-  ( ph -> ( -. ( ( A + B ) / 2 ) < M -> M < X ) )
31 30 con1d 
 |-  ( ph -> ( -. M < X -> ( ( A + B ) / 2 ) < M ) )
32 25 simp3d 
 |-  ( ph -> Y = if ( ( ( A + B ) / 2 ) < M , ( ( A + B ) / 2 ) , B ) )
33 iftrue 
 |-  ( ( ( A + B ) / 2 ) < M -> if ( ( ( A + B ) / 2 ) < M , ( ( A + B ) / 2 ) , B ) = ( ( A + B ) / 2 ) )
34 32 33 sylan9eq 
 |-  ( ( ph /\ ( ( A + B ) / 2 ) < M ) -> Y = ( ( A + B ) / 2 ) )
35 simpr 
 |-  ( ( ph /\ ( ( A + B ) / 2 ) < M ) -> ( ( A + B ) / 2 ) < M )
36 34 35 eqbrtrd 
 |-  ( ( ph /\ ( ( A + B ) / 2 ) < M ) -> Y < M )
37 36 ex 
 |-  ( ph -> ( ( ( A + B ) / 2 ) < M -> Y < M ) )
38 31 37 syld 
 |-  ( ph -> ( -. M < X -> Y < M ) )
39 38 orrd 
 |-  ( ph -> ( M < X \/ Y < M ) )