Metamath Proof Explorer

Theorem ruclem1

Description: Lemma for ruc (the reals are uncountable). Substitutions for the function D . (Contributed by Mario Carneiro, 28-May-2014) (Revised by Fan Zheng, 6-Jun-2016)

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 ) )
Assertion 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 ) ) )

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 2 oveqd 
 |-  ( ph -> ( <. A , B >. D M ) = ( <. A , B >. ( 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 ) >. ) ) M ) )
9 3 4 opelxpd 
 |-  ( ph -> <. A , B >. e. ( RR X. RR ) )
10 simpr 
 |-  ( ( x = <. A , B >. /\ y = M ) -> y = M )
11 10 breq2d 
 |-  ( ( x = <. A , B >. /\ y = M ) -> ( m < y <-> m < M ) )
12 simpl 
 |-  ( ( x = <. A , B >. /\ y = M ) -> x = <. A , B >. )
13 12 fveq2d 
 |-  ( ( x = <. A , B >. /\ y = M ) -> ( 1st ` x ) = ( 1st ` <. A , B >. ) )
14 13 opeq1d 
 |-  ( ( x = <. A , B >. /\ y = M ) -> <. ( 1st ` x ) , m >. = <. ( 1st ` <. A , B >. ) , m >. )
15 12 fveq2d 
 |-  ( ( x = <. A , B >. /\ y = M ) -> ( 2nd ` x ) = ( 2nd ` <. A , B >. ) )
16 15 oveq2d 
 |-  ( ( x = <. A , B >. /\ y = M ) -> ( m + ( 2nd ` x ) ) = ( m + ( 2nd ` <. A , B >. ) ) )
17 16 oveq1d 
 |-  ( ( x = <. A , B >. /\ y = M ) -> ( ( m + ( 2nd ` x ) ) / 2 ) = ( ( m + ( 2nd ` <. A , B >. ) ) / 2 ) )
18 17 15 opeq12d 
 |-  ( ( x = <. A , B >. /\ y = M ) -> <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. = <. ( ( m + ( 2nd ` <. A , B >. ) ) / 2 ) , ( 2nd ` <. A , B >. ) >. )
19 11 14 18 ifbieq12d 
 |-  ( ( x = <. A , B >. /\ y = M ) -> if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) = if ( m < M , <. ( 1st ` <. A , B >. ) , m >. , <. ( ( m + ( 2nd ` <. A , B >. ) ) / 2 ) , ( 2nd ` <. A , B >. ) >. ) )
20 19 csbeq2dv 
 |-  ( ( x = <. A , B >. /\ y = M ) -> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) = [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < M , <. ( 1st ` <. A , B >. ) , m >. , <. ( ( m + ( 2nd ` <. A , B >. ) ) / 2 ) , ( 2nd ` <. A , B >. ) >. ) )
21 13 15 oveq12d 
 |-  ( ( x = <. A , B >. /\ y = M ) -> ( ( 1st ` x ) + ( 2nd ` x ) ) = ( ( 1st ` <. A , B >. ) + ( 2nd ` <. A , B >. ) ) )
22 21 oveq1d 
 |-  ( ( x = <. A , B >. /\ y = M ) -> ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) = ( ( ( 1st ` <. A , B >. ) + ( 2nd ` <. A , B >. ) ) / 2 ) )
23 22 csbeq1d 
 |-  ( ( x = <. A , B >. /\ y = M ) -> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < M , <. ( 1st ` <. A , B >. ) , m >. , <. ( ( m + ( 2nd ` <. A , B >. ) ) / 2 ) , ( 2nd ` <. A , B >. ) >. ) = [_ ( ( ( 1st ` <. A , B >. ) + ( 2nd ` <. A , B >. ) ) / 2 ) / m ]_ if ( m < M , <. ( 1st ` <. A , B >. ) , m >. , <. ( ( m + ( 2nd ` <. A , B >. ) ) / 2 ) , ( 2nd ` <. A , B >. ) >. ) )
24 20 23 eqtrd 
 |-  ( ( x = <. A , B >. /\ y = M ) -> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) = [_ ( ( ( 1st ` <. A , B >. ) + ( 2nd ` <. A , B >. ) ) / 2 ) / m ]_ if ( m < M , <. ( 1st ` <. A , B >. ) , m >. , <. ( ( m + ( 2nd ` <. A , B >. ) ) / 2 ) , ( 2nd ` <. A , B >. ) >. ) )
25 eqid 
 |-  ( 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 ) >. ) ) = ( 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 ) >. ) )
26 opex 
 |-  <. ( 1st ` <. A , B >. ) , m >. e. _V
27 opex 
 |-  <. ( ( m + ( 2nd ` <. A , B >. ) ) / 2 ) , ( 2nd ` <. A , B >. ) >. e. _V
28 26 27 ifex 
 |-  if ( m < M , <. ( 1st ` <. A , B >. ) , m >. , <. ( ( m + ( 2nd ` <. A , B >. ) ) / 2 ) , ( 2nd ` <. A , B >. ) >. ) e. _V
29 28 csbex 
 |-  [_ ( ( ( 1st ` <. A , B >. ) + ( 2nd ` <. A , B >. ) ) / 2 ) / m ]_ if ( m < M , <. ( 1st ` <. A , B >. ) , m >. , <. ( ( m + ( 2nd ` <. A , B >. ) ) / 2 ) , ( 2nd ` <. A , B >. ) >. ) e. _V
30 24 25 29 ovmpoa 
 |-  ( ( <. A , B >. e. ( RR X. RR ) /\ M e. RR ) -> ( <. A , B >. ( 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 ) >. ) ) M ) = [_ ( ( ( 1st ` <. A , B >. ) + ( 2nd ` <. A , B >. ) ) / 2 ) / m ]_ if ( m < M , <. ( 1st ` <. A , B >. ) , m >. , <. ( ( m + ( 2nd ` <. A , B >. ) ) / 2 ) , ( 2nd ` <. A , B >. ) >. ) )
31 9 5 30 syl2anc 
 |-  ( ph -> ( <. A , B >. ( 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 ) >. ) ) M ) = [_ ( ( ( 1st ` <. A , B >. ) + ( 2nd ` <. A , B >. ) ) / 2 ) / m ]_ if ( m < M , <. ( 1st ` <. A , B >. ) , m >. , <. ( ( m + ( 2nd ` <. A , B >. ) ) / 2 ) , ( 2nd ` <. A , B >. ) >. ) )
32 8 31 eqtrd 
 |-  ( ph -> ( <. A , B >. D M ) = [_ ( ( ( 1st ` <. A , B >. ) + ( 2nd ` <. A , B >. ) ) / 2 ) / m ]_ if ( m < M , <. ( 1st ` <. A , B >. ) , m >. , <. ( ( m + ( 2nd ` <. A , B >. ) ) / 2 ) , ( 2nd ` <. A , B >. ) >. ) )
33 op1stg 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 1st ` <. A , B >. ) = A )
34 3 4 33 syl2anc 
 |-  ( ph -> ( 1st ` <. A , B >. ) = A )
35 op2ndg 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 2nd ` <. A , B >. ) = B )
36 3 4 35 syl2anc 
 |-  ( ph -> ( 2nd ` <. A , B >. ) = B )
37 34 36 oveq12d 
 |-  ( ph -> ( ( 1st ` <. A , B >. ) + ( 2nd ` <. A , B >. ) ) = ( A + B ) )
38 37 oveq1d 
 |-  ( ph -> ( ( ( 1st ` <. A , B >. ) + ( 2nd ` <. A , B >. ) ) / 2 ) = ( ( A + B ) / 2 ) )
39 38 csbeq1d 
 |-  ( ph -> [_ ( ( ( 1st ` <. A , B >. ) + ( 2nd ` <. A , B >. ) ) / 2 ) / m ]_ if ( m < M , <. ( 1st ` <. A , B >. ) , m >. , <. ( ( m + ( 2nd ` <. A , B >. ) ) / 2 ) , ( 2nd ` <. A , B >. ) >. ) = [_ ( ( A + B ) / 2 ) / m ]_ if ( m < M , <. ( 1st ` <. A , B >. ) , m >. , <. ( ( m + ( 2nd ` <. A , B >. ) ) / 2 ) , ( 2nd ` <. A , B >. ) >. ) )
40 ovex 
 |-  ( ( A + B ) / 2 ) e. _V
41 breq1 
 |-  ( m = ( ( A + B ) / 2 ) -> ( m < M <-> ( ( A + B ) / 2 ) < M ) )
42 opeq2 
 |-  ( m = ( ( A + B ) / 2 ) -> <. ( 1st ` <. A , B >. ) , m >. = <. ( 1st ` <. A , B >. ) , ( ( A + B ) / 2 ) >. )
43 oveq1 
 |-  ( m = ( ( A + B ) / 2 ) -> ( m + ( 2nd ` <. A , B >. ) ) = ( ( ( A + B ) / 2 ) + ( 2nd ` <. A , B >. ) ) )
44 43 oveq1d 
 |-  ( m = ( ( A + B ) / 2 ) -> ( ( m + ( 2nd ` <. A , B >. ) ) / 2 ) = ( ( ( ( A + B ) / 2 ) + ( 2nd ` <. A , B >. ) ) / 2 ) )
45 44 opeq1d 
 |-  ( m = ( ( A + B ) / 2 ) -> <. ( ( m + ( 2nd ` <. A , B >. ) ) / 2 ) , ( 2nd ` <. A , B >. ) >. = <. ( ( ( ( A + B ) / 2 ) + ( 2nd ` <. A , B >. ) ) / 2 ) , ( 2nd ` <. A , B >. ) >. )
46 41 42 45 ifbieq12d 
 |-  ( m = ( ( A + B ) / 2 ) -> if ( m < M , <. ( 1st ` <. A , B >. ) , m >. , <. ( ( m + ( 2nd ` <. A , B >. ) ) / 2 ) , ( 2nd ` <. A , B >. ) >. ) = if ( ( ( A + B ) / 2 ) < M , <. ( 1st ` <. A , B >. ) , ( ( A + B ) / 2 ) >. , <. ( ( ( ( A + B ) / 2 ) + ( 2nd ` <. A , B >. ) ) / 2 ) , ( 2nd ` <. A , B >. ) >. ) )
47 40 46 csbie 
 |-  [_ ( ( A + B ) / 2 ) / m ]_ if ( m < M , <. ( 1st ` <. A , B >. ) , m >. , <. ( ( m + ( 2nd ` <. A , B >. ) ) / 2 ) , ( 2nd ` <. A , B >. ) >. ) = if ( ( ( A + B ) / 2 ) < M , <. ( 1st ` <. A , B >. ) , ( ( A + B ) / 2 ) >. , <. ( ( ( ( A + B ) / 2 ) + ( 2nd ` <. A , B >. ) ) / 2 ) , ( 2nd ` <. A , B >. ) >. )
48 34 opeq1d 
 |-  ( ph -> <. ( 1st ` <. A , B >. ) , ( ( A + B ) / 2 ) >. = <. A , ( ( A + B ) / 2 ) >. )
49 36 oveq2d 
 |-  ( ph -> ( ( ( A + B ) / 2 ) + ( 2nd ` <. A , B >. ) ) = ( ( ( A + B ) / 2 ) + B ) )
50 49 oveq1d 
 |-  ( ph -> ( ( ( ( A + B ) / 2 ) + ( 2nd ` <. A , B >. ) ) / 2 ) = ( ( ( ( A + B ) / 2 ) + B ) / 2 ) )
51 50 36 opeq12d 
 |-  ( ph -> <. ( ( ( ( A + B ) / 2 ) + ( 2nd ` <. A , B >. ) ) / 2 ) , ( 2nd ` <. A , B >. ) >. = <. ( ( ( ( A + B ) / 2 ) + B ) / 2 ) , B >. )
52 48 51 ifeq12d 
 |-  ( ph -> if ( ( ( A + B ) / 2 ) < M , <. ( 1st ` <. A , B >. ) , ( ( A + B ) / 2 ) >. , <. ( ( ( ( A + B ) / 2 ) + ( 2nd ` <. A , B >. ) ) / 2 ) , ( 2nd ` <. A , B >. ) >. ) = if ( ( ( A + B ) / 2 ) < M , <. A , ( ( A + B ) / 2 ) >. , <. ( ( ( ( A + B ) / 2 ) + B ) / 2 ) , B >. ) )
53 47 52 syl5eq 
 |-  ( ph -> [_ ( ( A + B ) / 2 ) / m ]_ if ( m < M , <. ( 1st ` <. A , B >. ) , m >. , <. ( ( m + ( 2nd ` <. A , B >. ) ) / 2 ) , ( 2nd ` <. A , B >. ) >. ) = if ( ( ( A + B ) / 2 ) < M , <. A , ( ( A + B ) / 2 ) >. , <. ( ( ( ( A + B ) / 2 ) + B ) / 2 ) , B >. ) )
54 39 53 eqtrd 
 |-  ( ph -> [_ ( ( ( 1st ` <. A , B >. ) + ( 2nd ` <. A , B >. ) ) / 2 ) / m ]_ if ( m < M , <. ( 1st ` <. A , B >. ) , m >. , <. ( ( m + ( 2nd ` <. A , B >. ) ) / 2 ) , ( 2nd ` <. A , B >. ) >. ) = if ( ( ( A + B ) / 2 ) < M , <. A , ( ( A + B ) / 2 ) >. , <. ( ( ( ( A + B ) / 2 ) + B ) / 2 ) , B >. ) )
55 32 54 eqtrd 
 |-  ( ph -> ( <. A , B >. D M ) = if ( ( ( A + B ) / 2 ) < M , <. A , ( ( A + B ) / 2 ) >. , <. ( ( ( ( A + B ) / 2 ) + B ) / 2 ) , B >. ) )
56 3 4 readdcld 
 |-  ( ph -> ( A + B ) e. RR )
57 56 rehalfcld 
 |-  ( ph -> ( ( A + B ) / 2 ) e. RR )
58 3 57 opelxpd 
 |-  ( ph -> <. A , ( ( A + B ) / 2 ) >. e. ( RR X. RR ) )
59 57 4 readdcld 
 |-  ( ph -> ( ( ( A + B ) / 2 ) + B ) e. RR )
60 59 rehalfcld 
 |-  ( ph -> ( ( ( ( A + B ) / 2 ) + B ) / 2 ) e. RR )
61 60 4 opelxpd 
 |-  ( ph -> <. ( ( ( ( A + B ) / 2 ) + B ) / 2 ) , B >. e. ( RR X. RR ) )
62 58 61 ifcld 
 |-  ( ph -> if ( ( ( A + B ) / 2 ) < M , <. A , ( ( A + B ) / 2 ) >. , <. ( ( ( ( A + B ) / 2 ) + B ) / 2 ) , B >. ) e. ( RR X. RR ) )
63 55 62 eqeltrd 
 |-  ( ph -> ( <. A , B >. D M ) e. ( RR X. RR ) )
64 55 fveq2d 
 |-  ( ph -> ( 1st ` ( <. A , B >. D M ) ) = ( 1st ` if ( ( ( A + B ) / 2 ) < M , <. A , ( ( A + B ) / 2 ) >. , <. ( ( ( ( A + B ) / 2 ) + B ) / 2 ) , B >. ) ) )
65 fvif 
 |-  ( 1st ` if ( ( ( A + B ) / 2 ) < M , <. A , ( ( A + B ) / 2 ) >. , <. ( ( ( ( A + B ) / 2 ) + B ) / 2 ) , B >. ) ) = if ( ( ( A + B ) / 2 ) < M , ( 1st ` <. A , ( ( A + B ) / 2 ) >. ) , ( 1st ` <. ( ( ( ( A + B ) / 2 ) + B ) / 2 ) , B >. ) )
66 op1stg 
 |-  ( ( A e. RR /\ ( ( A + B ) / 2 ) e. _V ) -> ( 1st ` <. A , ( ( A + B ) / 2 ) >. ) = A )
67 3 40 66 sylancl 
 |-  ( ph -> ( 1st ` <. A , ( ( A + B ) / 2 ) >. ) = A )
68 ovex 
 |-  ( ( ( ( A + B ) / 2 ) + B ) / 2 ) e. _V
69 op1stg 
 |-  ( ( ( ( ( ( A + B ) / 2 ) + B ) / 2 ) e. _V /\ B e. RR ) -> ( 1st ` <. ( ( ( ( A + B ) / 2 ) + B ) / 2 ) , B >. ) = ( ( ( ( A + B ) / 2 ) + B ) / 2 ) )
70 68 4 69 sylancr 
 |-  ( ph -> ( 1st ` <. ( ( ( ( A + B ) / 2 ) + B ) / 2 ) , B >. ) = ( ( ( ( A + B ) / 2 ) + B ) / 2 ) )
71 67 70 ifeq12d 
 |-  ( ph -> if ( ( ( A + B ) / 2 ) < M , ( 1st ` <. A , ( ( A + B ) / 2 ) >. ) , ( 1st ` <. ( ( ( ( A + B ) / 2 ) + B ) / 2 ) , B >. ) ) = if ( ( ( A + B ) / 2 ) < M , A , ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) )
72 65 71 syl5eq 
 |-  ( ph -> ( 1st ` if ( ( ( A + B ) / 2 ) < M , <. A , ( ( A + B ) / 2 ) >. , <. ( ( ( ( A + B ) / 2 ) + B ) / 2 ) , B >. ) ) = if ( ( ( A + B ) / 2 ) < M , A , ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) )
73 64 72 eqtrd 
 |-  ( ph -> ( 1st ` ( <. A , B >. D M ) ) = if ( ( ( A + B ) / 2 ) < M , A , ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) )
74 6 73 syl5eq 
 |-  ( ph -> X = if ( ( ( A + B ) / 2 ) < M , A , ( ( ( ( A + B ) / 2 ) + B ) / 2 ) ) )
75 55 fveq2d 
 |-  ( ph -> ( 2nd ` ( <. A , B >. D M ) ) = ( 2nd ` if ( ( ( A + B ) / 2 ) < M , <. A , ( ( A + B ) / 2 ) >. , <. ( ( ( ( A + B ) / 2 ) + B ) / 2 ) , B >. ) ) )
76 fvif 
 |-  ( 2nd ` if ( ( ( A + B ) / 2 ) < M , <. A , ( ( A + B ) / 2 ) >. , <. ( ( ( ( A + B ) / 2 ) + B ) / 2 ) , B >. ) ) = if ( ( ( A + B ) / 2 ) < M , ( 2nd ` <. A , ( ( A + B ) / 2 ) >. ) , ( 2nd ` <. ( ( ( ( A + B ) / 2 ) + B ) / 2 ) , B >. ) )
77 op2ndg 
 |-  ( ( A e. RR /\ ( ( A + B ) / 2 ) e. _V ) -> ( 2nd ` <. A , ( ( A + B ) / 2 ) >. ) = ( ( A + B ) / 2 ) )
78 3 40 77 sylancl 
 |-  ( ph -> ( 2nd ` <. A , ( ( A + B ) / 2 ) >. ) = ( ( A + B ) / 2 ) )
79 op2ndg 
 |-  ( ( ( ( ( ( A + B ) / 2 ) + B ) / 2 ) e. _V /\ B e. RR ) -> ( 2nd ` <. ( ( ( ( A + B ) / 2 ) + B ) / 2 ) , B >. ) = B )
80 68 4 79 sylancr 
 |-  ( ph -> ( 2nd ` <. ( ( ( ( A + B ) / 2 ) + B ) / 2 ) , B >. ) = B )
81 78 80 ifeq12d 
 |-  ( ph -> if ( ( ( A + B ) / 2 ) < M , ( 2nd ` <. A , ( ( A + B ) / 2 ) >. ) , ( 2nd ` <. ( ( ( ( A + B ) / 2 ) + B ) / 2 ) , B >. ) ) = if ( ( ( A + B ) / 2 ) < M , ( ( A + B ) / 2 ) , B ) )
82 76 81 syl5eq 
 |-  ( ph -> ( 2nd ` if ( ( ( A + B ) / 2 ) < M , <. A , ( ( A + B ) / 2 ) >. , <. ( ( ( ( A + B ) / 2 ) + B ) / 2 ) , B >. ) ) = if ( ( ( A + B ) / 2 ) < M , ( ( A + B ) / 2 ) , B ) )
83 75 82 eqtrd 
 |-  ( ph -> ( 2nd ` ( <. A , B >. D M ) ) = if ( ( ( A + B ) / 2 ) < M , ( ( A + B ) / 2 ) , B ) )
84 7 83 syl5eq 
 |-  ( ph -> Y = if ( ( ( A + B ) / 2 ) < M , ( ( A + B ) / 2 ) , B ) )
85 63 74 84 3jca 
 |-  ( 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 ) ) )