Metamath Proof Explorer

Theorem dvivthlem1

Description: Lemma for dvivth . (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses dvivth.1 
|- ( ph -> M e. ( A (,) B ) )
dvivth.2 
|- ( ph -> N e. ( A (,) B ) )
dvivth.3 
|- ( ph -> F e. ( ( A (,) B ) -cn-> RR ) )
dvivth.4 
|- ( ph -> dom ( RR _D F ) = ( A (,) B ) )
dvivth.5 
|- ( ph -> M < N )
dvivth.6 
|- ( ph -> C e. ( ( ( RR _D F ) ` N ) [,] ( ( RR _D F ) ` M ) ) )
dvivth.7 
|- G = ( y e. ( A (,) B ) |-> ( ( F ` y ) - ( C x. y ) ) )
Assertion dvivthlem1 
|- ( ph -> E. x e. ( M [,] N ) ( ( RR _D F ) ` x ) = C )

Proof

Step Hyp Ref Expression
1 dvivth.1 
 |-  ( ph -> M e. ( A (,) B ) )
2 dvivth.2 
 |-  ( ph -> N e. ( A (,) B ) )
3 dvivth.3 
 |-  ( ph -> F e. ( ( A (,) B ) -cn-> RR ) )
4 dvivth.4 
 |-  ( ph -> dom ( RR _D F ) = ( A (,) B ) )
5 dvivth.5 
 |-  ( ph -> M < N )
6 dvivth.6 
 |-  ( ph -> C e. ( ( ( RR _D F ) ` N ) [,] ( ( RR _D F ) ` M ) ) )
7 dvivth.7 
 |-  G = ( y e. ( A (,) B ) |-> ( ( F ` y ) - ( C x. y ) ) )
8 ioossre 
 |-  ( A (,) B ) C_ RR
9 8 1 sselid 
 |-  ( ph -> M e. RR )
10 8 2 sselid 
 |-  ( ph -> N e. RR )
11 9 10 5 ltled 
 |-  ( ph -> M <_ N )
12 cncff 
 |-  ( F e. ( ( A (,) B ) -cn-> RR ) -> F : ( A (,) B ) --> RR )
13 3 12 syl 
 |-  ( ph -> F : ( A (,) B ) --> RR )
14 13 ffvelrnda 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( F ` y ) e. RR )
15 dvfre 
 |-  ( ( F : ( A (,) B ) --> RR /\ ( A (,) B ) C_ RR ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
16 13 8 15 sylancl 
 |-  ( ph -> ( RR _D F ) : dom ( RR _D F ) --> RR )
17 2 4 eleqtrrd 
 |-  ( ph -> N e. dom ( RR _D F ) )
18 16 17 ffvelrnd 
 |-  ( ph -> ( ( RR _D F ) ` N ) e. RR )
19 1 4 eleqtrrd 
 |-  ( ph -> M e. dom ( RR _D F ) )
20 16 19 ffvelrnd 
 |-  ( ph -> ( ( RR _D F ) ` M ) e. RR )
21 iccssre 
 |-  ( ( ( ( RR _D F ) ` N ) e. RR /\ ( ( RR _D F ) ` M ) e. RR ) -> ( ( ( RR _D F ) ` N ) [,] ( ( RR _D F ) ` M ) ) C_ RR )
22 18 20 21 syl2anc 
 |-  ( ph -> ( ( ( RR _D F ) ` N ) [,] ( ( RR _D F ) ` M ) ) C_ RR )
23 22 6 sseldd 
 |-  ( ph -> C e. RR )
24 23 adantr 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> C e. RR )
25 8 a1i 
 |-  ( ph -> ( A (,) B ) C_ RR )
26 25 sselda 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> y e. RR )
27 24 26 remulcld 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( C x. y ) e. RR )
28 14 27 resubcld 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( ( F ` y ) - ( C x. y ) ) e. RR )
29 28 7 fmptd 
 |-  ( ph -> G : ( A (,) B ) --> RR )
30 iccssioo2 
 |-  ( ( M e. ( A (,) B ) /\ N e. ( A (,) B ) ) -> ( M [,] N ) C_ ( A (,) B ) )
31 1 2 30 syl2anc 
 |-  ( ph -> ( M [,] N ) C_ ( A (,) B ) )
32 29 31 fssresd 
 |-  ( ph -> ( G |` ( M [,] N ) ) : ( M [,] N ) --> RR )
33 ax-resscn 
 |-  RR C_ CC
34 33 a1i 
 |-  ( ph -> RR C_ CC )
35 fss 
 |-  ( ( G : ( A (,) B ) --> RR /\ RR C_ CC ) -> G : ( A (,) B ) --> CC )
36 29 33 35 sylancl 
 |-  ( ph -> G : ( A (,) B ) --> CC )
37 7 oveq2i 
 |-  ( RR _D G ) = ( RR _D ( y e. ( A (,) B ) |-> ( ( F ` y ) - ( C x. y ) ) ) )
38 reelprrecn 
 |-  RR e. { RR , CC }
39 38 a1i 
 |-  ( ph -> RR e. { RR , CC } )
40 14 recnd 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( F ` y ) e. CC )
41 4 feq2d 
 |-  ( ph -> ( ( RR _D F ) : dom ( RR _D F ) --> RR <-> ( RR _D F ) : ( A (,) B ) --> RR ) )
42 16 41 mpbid 
 |-  ( ph -> ( RR _D F ) : ( A (,) B ) --> RR )
43 42 ffvelrnda 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( ( RR _D F ) ` y ) e. RR )
44 13 feqmptd 
 |-  ( ph -> F = ( y e. ( A (,) B ) |-> ( F ` y ) ) )
45 44 oveq2d 
 |-  ( ph -> ( RR _D F ) = ( RR _D ( y e. ( A (,) B ) |-> ( F ` y ) ) ) )
46 42 feqmptd 
 |-  ( ph -> ( RR _D F ) = ( y e. ( A (,) B ) |-> ( ( RR _D F ) ` y ) ) )
47 45 46 eqtr3d 
 |-  ( ph -> ( RR _D ( y e. ( A (,) B ) |-> ( F ` y ) ) ) = ( y e. ( A (,) B ) |-> ( ( RR _D F ) ` y ) ) )
48 27 recnd 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( C x. y ) e. CC )
49 remulcl 
 |-  ( ( C e. RR /\ y e. RR ) -> ( C x. y ) e. RR )
50 23 49 sylan 
 |-  ( ( ph /\ y e. RR ) -> ( C x. y ) e. RR )
51 50 recnd 
 |-  ( ( ph /\ y e. RR ) -> ( C x. y ) e. CC )
52 23 adantr 
 |-  ( ( ph /\ y e. RR ) -> C e. RR )
53 34 sselda 
 |-  ( ( ph /\ y e. RR ) -> y e. CC )
54 1cnd 
 |-  ( ( ph /\ y e. RR ) -> 1 e. CC )
55 39 dvmptid 
 |-  ( ph -> ( RR _D ( y e. RR |-> y ) ) = ( y e. RR |-> 1 ) )
56 23 recnd 
 |-  ( ph -> C e. CC )
57 39 53 54 55 56 dvmptcmul 
 |-  ( ph -> ( RR _D ( y e. RR |-> ( C x. y ) ) ) = ( y e. RR |-> ( C x. 1 ) ) )
58 56 mulid1d 
 |-  ( ph -> ( C x. 1 ) = C )
59 58 mpteq2dv 
 |-  ( ph -> ( y e. RR |-> ( C x. 1 ) ) = ( y e. RR |-> C ) )
60 57 59 eqtrd 
 |-  ( ph -> ( RR _D ( y e. RR |-> ( C x. y ) ) ) = ( y e. RR |-> C ) )
61 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
62 61 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
63 iooretop 
 |-  ( A (,) B ) e. ( topGen ` ran (,) )
64 63 a1i 
 |-  ( ph -> ( A (,) B ) e. ( topGen ` ran (,) ) )
65 39 51 52 60 25 62 61 64 dvmptres 
 |-  ( ph -> ( RR _D ( y e. ( A (,) B ) |-> ( C x. y ) ) ) = ( y e. ( A (,) B ) |-> C ) )
66 39 40 43 47 48 24 65 dvmptsub 
 |-  ( ph -> ( RR _D ( y e. ( A (,) B ) |-> ( ( F ` y ) - ( C x. y ) ) ) ) = ( y e. ( A (,) B ) |-> ( ( ( RR _D F ) ` y ) - C ) ) )
67 37 66 syl5eq 
 |-  ( ph -> ( RR _D G ) = ( y e. ( A (,) B ) |-> ( ( ( RR _D F ) ` y ) - C ) ) )
68 67 dmeqd 
 |-  ( ph -> dom ( RR _D G ) = dom ( y e. ( A (,) B ) |-> ( ( ( RR _D F ) ` y ) - C ) ) )
69 dmmptg 
 |-  ( A. y e. ( A (,) B ) ( ( ( RR _D F ) ` y ) - C ) e. _V -> dom ( y e. ( A (,) B ) |-> ( ( ( RR _D F ) ` y ) - C ) ) = ( A (,) B ) )
70 ovex 
 |-  ( ( ( RR _D F ) ` y ) - C ) e. _V
71 70 a1i 
 |-  ( y e. ( A (,) B ) -> ( ( ( RR _D F ) ` y ) - C ) e. _V )
72 69 71 mprg 
 |-  dom ( y e. ( A (,) B ) |-> ( ( ( RR _D F ) ` y ) - C ) ) = ( A (,) B )
73 68 72 eqtrdi 
 |-  ( ph -> dom ( RR _D G ) = ( A (,) B ) )
74 dvcn 
 |-  ( ( ( RR C_ CC /\ G : ( A (,) B ) --> CC /\ ( A (,) B ) C_ RR ) /\ dom ( RR _D G ) = ( A (,) B ) ) -> G e. ( ( A (,) B ) -cn-> CC ) )
75 34 36 25 73 74 syl31anc 
 |-  ( ph -> G e. ( ( A (,) B ) -cn-> CC ) )
76 rescncf 
 |-  ( ( M [,] N ) C_ ( A (,) B ) -> ( G e. ( ( A (,) B ) -cn-> CC ) -> ( G |` ( M [,] N ) ) e. ( ( M [,] N ) -cn-> CC ) ) )
77 31 75 76 sylc 
 |-  ( ph -> ( G |` ( M [,] N ) ) e. ( ( M [,] N ) -cn-> CC ) )
78 cncffvrn 
 |-  ( ( RR C_ CC /\ ( G |` ( M [,] N ) ) e. ( ( M [,] N ) -cn-> CC ) ) -> ( ( G |` ( M [,] N ) ) e. ( ( M [,] N ) -cn-> RR ) <-> ( G |` ( M [,] N ) ) : ( M [,] N ) --> RR ) )
79 33 77 78 sylancr 
 |-  ( ph -> ( ( G |` ( M [,] N ) ) e. ( ( M [,] N ) -cn-> RR ) <-> ( G |` ( M [,] N ) ) : ( M [,] N ) --> RR ) )
80 32 79 mpbird 
 |-  ( ph -> ( G |` ( M [,] N ) ) e. ( ( M [,] N ) -cn-> RR ) )
81 9 10 11 80 evthicc 
 |-  ( ph -> ( E. x e. ( M [,] N ) A. z e. ( M [,] N ) ( ( G |` ( M [,] N ) ) ` z ) <_ ( ( G |` ( M [,] N ) ) ` x ) /\ E. x e. ( M [,] N ) A. z e. ( M [,] N ) ( ( G |` ( M [,] N ) ) ` x ) <_ ( ( G |` ( M [,] N ) ) ` z ) ) )
82 81 simpld 
 |-  ( ph -> E. x e. ( M [,] N ) A. z e. ( M [,] N ) ( ( G |` ( M [,] N ) ) ` z ) <_ ( ( G |` ( M [,] N ) ) ` x ) )
83 fvres 
 |-  ( z e. ( M [,] N ) -> ( ( G |` ( M [,] N ) ) ` z ) = ( G ` z ) )
84 fvres 
 |-  ( x e. ( M [,] N ) -> ( ( G |` ( M [,] N ) ) ` x ) = ( G ` x ) )
85 83 84 breqan12rd 
 |-  ( ( x e. ( M [,] N ) /\ z e. ( M [,] N ) ) -> ( ( ( G |` ( M [,] N ) ) ` z ) <_ ( ( G |` ( M [,] N ) ) ` x ) <-> ( G ` z ) <_ ( G ` x ) ) )
86 85 ralbidva 
 |-  ( x e. ( M [,] N ) -> ( A. z e. ( M [,] N ) ( ( G |` ( M [,] N ) ) ` z ) <_ ( ( G |` ( M [,] N ) ) ` x ) <-> A. z e. ( M [,] N ) ( G ` z ) <_ ( G ` x ) ) )
87 86 adantl 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> ( A. z e. ( M [,] N ) ( ( G |` ( M [,] N ) ) ` z ) <_ ( ( G |` ( M [,] N ) ) ` x ) <-> A. z e. ( M [,] N ) ( G ` z ) <_ ( G ` x ) ) )
88 ioossicc 
 |-  ( M (,) N ) C_ ( M [,] N )
89 ssralv 
 |-  ( ( M (,) N ) C_ ( M [,] N ) -> ( A. z e. ( M [,] N ) ( G ` z ) <_ ( G ` x ) -> A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) )
90 88 89 ax-mp 
 |-  ( A. z e. ( M [,] N ) ( G ` z ) <_ ( G ` x ) -> A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) )
91 87 90 syl6bi 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> ( A. z e. ( M [,] N ) ( ( G |` ( M [,] N ) ) ` z ) <_ ( ( G |` ( M [,] N ) ) ` x ) -> A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) )
92 31 sselda 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> x e. ( A (,) B ) )
93 42 ffvelrnda 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) e. RR )
94 92 93 syldan 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> ( ( RR _D F ) ` x ) e. RR )
95 94 recnd 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> ( ( RR _D F ) ` x ) e. CC )
96 95 adantr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x e. ( M (,) N ) /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( ( RR _D F ) ` x ) e. CC )
97 56 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x e. ( M (,) N ) /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> C e. CC )
98 67 fveq1d 
 |-  ( ph -> ( ( RR _D G ) ` x ) = ( ( y e. ( A (,) B ) |-> ( ( ( RR _D F ) ` y ) - C ) ) ` x ) )
99 98 adantr 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> ( ( RR _D G ) ` x ) = ( ( y e. ( A (,) B ) |-> ( ( ( RR _D F ) ` y ) - C ) ) ` x ) )
100 fveq2 
 |-  ( y = x -> ( ( RR _D F ) ` y ) = ( ( RR _D F ) ` x ) )
101 100 oveq1d 
 |-  ( y = x -> ( ( ( RR _D F ) ` y ) - C ) = ( ( ( RR _D F ) ` x ) - C ) )
102 eqid 
 |-  ( y e. ( A (,) B ) |-> ( ( ( RR _D F ) ` y ) - C ) ) = ( y e. ( A (,) B ) |-> ( ( ( RR _D F ) ` y ) - C ) )
103 ovex 
 |-  ( ( ( RR _D F ) ` x ) - C ) e. _V
104 101 102 103 fvmpt 
 |-  ( x e. ( A (,) B ) -> ( ( y e. ( A (,) B ) |-> ( ( ( RR _D F ) ` y ) - C ) ) ` x ) = ( ( ( RR _D F ) ` x ) - C ) )
105 92 104 syl 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> ( ( y e. ( A (,) B ) |-> ( ( ( RR _D F ) ` y ) - C ) ) ` x ) = ( ( ( RR _D F ) ` x ) - C ) )
106 99 105 eqtrd 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> ( ( RR _D G ) ` x ) = ( ( ( RR _D F ) ` x ) - C ) )
107 106 adantr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x e. ( M (,) N ) /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( ( RR _D G ) ` x ) = ( ( ( RR _D F ) ` x ) - C ) )
108 29 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x e. ( M (,) N ) /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> G : ( A (,) B ) --> RR )
109 8 a1i 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x e. ( M (,) N ) /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( A (,) B ) C_ RR )
110 simprl 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x e. ( M (,) N ) /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> x e. ( M (,) N ) )
111 88 31 sstrid 
 |-  ( ph -> ( M (,) N ) C_ ( A (,) B ) )
112 111 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x e. ( M (,) N ) /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( M (,) N ) C_ ( A (,) B ) )
113 92 adantr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x e. ( M (,) N ) /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> x e. ( A (,) B ) )
114 73 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x e. ( M (,) N ) /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> dom ( RR _D G ) = ( A (,) B ) )
115 113 114 eleqtrrd 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x e. ( M (,) N ) /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> x e. dom ( RR _D G ) )
116 simprr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x e. ( M (,) N ) /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) )
117 fveq2 
 |-  ( z = w -> ( G ` z ) = ( G ` w ) )
118 117 breq1d 
 |-  ( z = w -> ( ( G ` z ) <_ ( G ` x ) <-> ( G ` w ) <_ ( G ` x ) ) )
119 118 cbvralvw 
 |-  ( A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) <-> A. w e. ( M (,) N ) ( G ` w ) <_ ( G ` x ) )
120 116 119 sylib 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x e. ( M (,) N ) /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> A. w e. ( M (,) N ) ( G ` w ) <_ ( G ` x ) )
121 108 109 110 112 115 120 dvferm 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x e. ( M (,) N ) /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( ( RR _D G ) ` x ) = 0 )
122 107 121 eqtr3d 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x e. ( M (,) N ) /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( ( ( RR _D F ) ` x ) - C ) = 0 )
123 96 97 122 subeq0d 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x e. ( M (,) N ) /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( ( RR _D F ) ` x ) = C )
124 123 exp32 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> ( x e. ( M (,) N ) -> ( A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) -> ( ( RR _D F ) ` x ) = C ) ) )
125 vex 
 |-  x e. _V
126 125 elpr 
 |-  ( x e. { M , N } <-> ( x = M \/ x = N ) )
127 106 adantr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = M /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( ( RR _D G ) ` x ) = ( ( ( RR _D F ) ` x ) - C ) )
128 29 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = M /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> G : ( A (,) B ) --> RR )
129 8 a1i 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = M /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( A (,) B ) C_ RR )
130 simprl 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = M /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> x = M )
131 eliooord 
 |-  ( M e. ( A (,) B ) -> ( A < M /\ M < B ) )
132 1 131 syl 
 |-  ( ph -> ( A < M /\ M < B ) )
133 132 simpld 
 |-  ( ph -> A < M )
134 ne0i 
 |-  ( M e. ( A (,) B ) -> ( A (,) B ) =/= (/) )
135 ndmioo 
 |-  ( -. ( A e. RR* /\ B e. RR* ) -> ( A (,) B ) = (/) )
136 135 necon1ai 
 |-  ( ( A (,) B ) =/= (/) -> ( A e. RR* /\ B e. RR* ) )
137 1 134 136 3syl 
 |-  ( ph -> ( A e. RR* /\ B e. RR* ) )
138 137 simpld 
 |-  ( ph -> A e. RR* )
139 10 rexrd 
 |-  ( ph -> N e. RR* )
140 elioo2 
 |-  ( ( A e. RR* /\ N e. RR* ) -> ( M e. ( A (,) N ) <-> ( M e. RR /\ A < M /\ M < N ) ) )
141 138 139 140 syl2anc 
 |-  ( ph -> ( M e. ( A (,) N ) <-> ( M e. RR /\ A < M /\ M < N ) ) )
142 9 133 5 141 mpbir3and 
 |-  ( ph -> M e. ( A (,) N ) )
143 142 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = M /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> M e. ( A (,) N ) )
144 130 143 eqeltrd 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = M /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> x e. ( A (,) N ) )
145 137 simprd 
 |-  ( ph -> B e. RR* )
146 eliooord 
 |-  ( N e. ( A (,) B ) -> ( A < N /\ N < B ) )
147 2 146 syl 
 |-  ( ph -> ( A < N /\ N < B ) )
148 147 simprd 
 |-  ( ph -> N < B )
149 139 145 148 xrltled 
 |-  ( ph -> N <_ B )
150 iooss2 
 |-  ( ( B e. RR* /\ N <_ B ) -> ( A (,) N ) C_ ( A (,) B ) )
151 145 149 150 syl2anc 
 |-  ( ph -> ( A (,) N ) C_ ( A (,) B ) )
152 151 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = M /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( A (,) N ) C_ ( A (,) B ) )
153 92 adantr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = M /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> x e. ( A (,) B ) )
154 73 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = M /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> dom ( RR _D G ) = ( A (,) B ) )
155 153 154 eleqtrrd 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = M /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> x e. dom ( RR _D G ) )
156 simprr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = M /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) )
157 156 119 sylib 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = M /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> A. w e. ( M (,) N ) ( G ` w ) <_ ( G ` x ) )
158 130 oveq1d 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = M /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( x (,) N ) = ( M (,) N ) )
159 158 raleqdv 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = M /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( A. w e. ( x (,) N ) ( G ` w ) <_ ( G ` x ) <-> A. w e. ( M (,) N ) ( G ` w ) <_ ( G ` x ) ) )
160 157 159 mpbird 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = M /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> A. w e. ( x (,) N ) ( G ` w ) <_ ( G ` x ) )
161 128 129 144 152 155 160 dvferm1 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = M /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( ( RR _D G ) ` x ) <_ 0 )
162 127 161 eqbrtrrd 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = M /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( ( ( RR _D F ) ` x ) - C ) <_ 0 )
163 94 adantr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = M /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( ( RR _D F ) ` x ) e. RR )
164 23 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = M /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> C e. RR )
165 163 164 suble0d 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = M /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( ( ( ( RR _D F ) ` x ) - C ) <_ 0 <-> ( ( RR _D F ) ` x ) <_ C ) )
166 162 165 mpbid 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = M /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( ( RR _D F ) ` x ) <_ C )
167 elicc2 
 |-  ( ( ( ( RR _D F ) ` N ) e. RR /\ ( ( RR _D F ) ` M ) e. RR ) -> ( C e. ( ( ( RR _D F ) ` N ) [,] ( ( RR _D F ) ` M ) ) <-> ( C e. RR /\ ( ( RR _D F ) ` N ) <_ C /\ C <_ ( ( RR _D F ) ` M ) ) ) )
168 18 20 167 syl2anc 
 |-  ( ph -> ( C e. ( ( ( RR _D F ) ` N ) [,] ( ( RR _D F ) ` M ) ) <-> ( C e. RR /\ ( ( RR _D F ) ` N ) <_ C /\ C <_ ( ( RR _D F ) ` M ) ) ) )
169 6 168 mpbid 
 |-  ( ph -> ( C e. RR /\ ( ( RR _D F ) ` N ) <_ C /\ C <_ ( ( RR _D F ) ` M ) ) )
170 169 simp3d 
 |-  ( ph -> C <_ ( ( RR _D F ) ` M ) )
171 170 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = M /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> C <_ ( ( RR _D F ) ` M ) )
172 130 fveq2d 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = M /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( ( RR _D F ) ` x ) = ( ( RR _D F ) ` M ) )
173 171 172 breqtrrd 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = M /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> C <_ ( ( RR _D F ) ` x ) )
174 163 164 letri3d 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = M /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( ( ( RR _D F ) ` x ) = C <-> ( ( ( RR _D F ) ` x ) <_ C /\ C <_ ( ( RR _D F ) ` x ) ) ) )
175 166 173 174 mpbir2and 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = M /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( ( RR _D F ) ` x ) = C )
176 175 exp32 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> ( x = M -> ( A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) -> ( ( RR _D F ) ` x ) = C ) ) )
177 simprl 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = N /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> x = N )
178 177 fveq2d 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = N /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( ( RR _D F ) ` x ) = ( ( RR _D F ) ` N ) )
179 169 simp2d 
 |-  ( ph -> ( ( RR _D F ) ` N ) <_ C )
180 179 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = N /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( ( RR _D F ) ` N ) <_ C )
181 178 180 eqbrtrd 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = N /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( ( RR _D F ) ` x ) <_ C )
182 29 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = N /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> G : ( A (,) B ) --> RR )
183 8 a1i 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = N /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( A (,) B ) C_ RR )
184 9 rexrd 
 |-  ( ph -> M e. RR* )
185 elioo2 
 |-  ( ( M e. RR* /\ B e. RR* ) -> ( N e. ( M (,) B ) <-> ( N e. RR /\ M < N /\ N < B ) ) )
186 184 145 185 syl2anc 
 |-  ( ph -> ( N e. ( M (,) B ) <-> ( N e. RR /\ M < N /\ N < B ) ) )
187 10 5 148 186 mpbir3and 
 |-  ( ph -> N e. ( M (,) B ) )
188 187 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = N /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> N e. ( M (,) B ) )
189 177 188 eqeltrd 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = N /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> x e. ( M (,) B ) )
190 138 184 133 xrltled 
 |-  ( ph -> A <_ M )
191 iooss1 
 |-  ( ( A e. RR* /\ A <_ M ) -> ( M (,) B ) C_ ( A (,) B ) )
192 138 190 191 syl2anc 
 |-  ( ph -> ( M (,) B ) C_ ( A (,) B ) )
193 192 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = N /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( M (,) B ) C_ ( A (,) B ) )
194 92 adantr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = N /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> x e. ( A (,) B ) )
195 73 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = N /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> dom ( RR _D G ) = ( A (,) B ) )
196 194 195 eleqtrrd 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = N /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> x e. dom ( RR _D G ) )
197 simprr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = N /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) )
198 197 119 sylib 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = N /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> A. w e. ( M (,) N ) ( G ` w ) <_ ( G ` x ) )
199 177 oveq2d 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = N /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( M (,) x ) = ( M (,) N ) )
200 199 raleqdv 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = N /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( A. w e. ( M (,) x ) ( G ` w ) <_ ( G ` x ) <-> A. w e. ( M (,) N ) ( G ` w ) <_ ( G ` x ) ) )
201 198 200 mpbird 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = N /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> A. w e. ( M (,) x ) ( G ` w ) <_ ( G ` x ) )
202 182 183 189 193 196 201 dvferm2 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = N /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> 0 <_ ( ( RR _D G ) ` x ) )
203 106 adantr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = N /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( ( RR _D G ) ` x ) = ( ( ( RR _D F ) ` x ) - C ) )
204 202 203 breqtrd 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = N /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> 0 <_ ( ( ( RR _D F ) ` x ) - C ) )
205 94 adantr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = N /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( ( RR _D F ) ` x ) e. RR )
206 23 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = N /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> C e. RR )
207 205 206 subge0d 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = N /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( 0 <_ ( ( ( RR _D F ) ` x ) - C ) <-> C <_ ( ( RR _D F ) ` x ) ) )
208 204 207 mpbid 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = N /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> C <_ ( ( RR _D F ) ` x ) )
209 205 206 letri3d 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = N /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( ( ( RR _D F ) ` x ) = C <-> ( ( ( RR _D F ) ` x ) <_ C /\ C <_ ( ( RR _D F ) ` x ) ) ) )
210 181 208 209 mpbir2and 
 |-  ( ( ( ph /\ x e. ( M [,] N ) ) /\ ( x = N /\ A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) ) ) -> ( ( RR _D F ) ` x ) = C )
211 210 exp32 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> ( x = N -> ( A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) -> ( ( RR _D F ) ` x ) = C ) ) )
212 176 211 jaod 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> ( ( x = M \/ x = N ) -> ( A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) -> ( ( RR _D F ) ` x ) = C ) ) )
213 126 212 syl5bi 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> ( x e. { M , N } -> ( A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) -> ( ( RR _D F ) ` x ) = C ) ) )
214 elun 
 |-  ( x e. ( ( M (,) N ) u. { M , N } ) <-> ( x e. ( M (,) N ) \/ x e. { M , N } ) )
215 prunioo 
 |-  ( ( M e. RR* /\ N e. RR* /\ M <_ N ) -> ( ( M (,) N ) u. { M , N } ) = ( M [,] N ) )
216 184 139 11 215 syl3anc 
 |-  ( ph -> ( ( M (,) N ) u. { M , N } ) = ( M [,] N ) )
217 216 eleq2d 
 |-  ( ph -> ( x e. ( ( M (,) N ) u. { M , N } ) <-> x e. ( M [,] N ) ) )
218 214 217 bitr3id 
 |-  ( ph -> ( ( x e. ( M (,) N ) \/ x e. { M , N } ) <-> x e. ( M [,] N ) ) )
219 218 biimpar 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> ( x e. ( M (,) N ) \/ x e. { M , N } ) )
220 124 213 219 mpjaod 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> ( A. z e. ( M (,) N ) ( G ` z ) <_ ( G ` x ) -> ( ( RR _D F ) ` x ) = C ) )
221 91 220 syld 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> ( A. z e. ( M [,] N ) ( ( G |` ( M [,] N ) ) ` z ) <_ ( ( G |` ( M [,] N ) ) ` x ) -> ( ( RR _D F ) ` x ) = C ) )
222 221 reximdva 
 |-  ( ph -> ( E. x e. ( M [,] N ) A. z e. ( M [,] N ) ( ( G |` ( M [,] N ) ) ` z ) <_ ( ( G |` ( M [,] N ) ) ` x ) -> E. x e. ( M [,] N ) ( ( RR _D F ) ` x ) = C ) )
223 82 222 mpd 
 |-  ( ph -> E. x e. ( M [,] N ) ( ( RR _D F ) ` x ) = C )