Metamath Proof Explorer

Theorem dvle2

Description: Collapsed dvle . (Contributed by metakunt, 19-Aug-2024)

Ref Expression
Hypotheses dvle2.1 
|- ( ph -> A e. RR )
dvle2.2 
|- ( ph -> B e. RR )
dvle2.3 
|- ( ph -> ( x e. ( A [,] B ) |-> E ) e. ( ( A [,] B ) -cn-> RR ) )
dvle2.4 
|- ( ph -> ( x e. ( A [,] B ) |-> G ) e. ( ( A [,] B ) -cn-> RR ) )
dvle2.5 
|- ( ph -> ( RR _D ( x e. ( A (,) B ) |-> E ) ) = ( x e. ( A (,) B ) |-> F ) )
dvle2.6 
|- ( ph -> ( RR _D ( x e. ( A (,) B ) |-> G ) ) = ( x e. ( A (,) B ) |-> H ) )
dvle2.7 
|- ( ( ph /\ x e. ( A (,) B ) ) -> F <_ H )
dvle2.8 
|- ( x = A -> E = P )
dvle2.9 
|- ( x = A -> G = Q )
dvle2.10 
|- ( x = B -> E = R )
dvle2.11 
|- ( x = B -> G = S )
dvle2.12 
|- ( ph -> P <_ Q )
dvle2.13 
|- ( ph -> A <_ B )
Assertion dvle2 
|- ( ph -> R <_ S )

Proof

Step Hyp Ref Expression
1 dvle2.1 
 |-  ( ph -> A e. RR )
2 dvle2.2 
 |-  ( ph -> B e. RR )
3 dvle2.3 
 |-  ( ph -> ( x e. ( A [,] B ) |-> E ) e. ( ( A [,] B ) -cn-> RR ) )
4 dvle2.4 
 |-  ( ph -> ( x e. ( A [,] B ) |-> G ) e. ( ( A [,] B ) -cn-> RR ) )
5 dvle2.5 
 |-  ( ph -> ( RR _D ( x e. ( A (,) B ) |-> E ) ) = ( x e. ( A (,) B ) |-> F ) )
6 dvle2.6 
 |-  ( ph -> ( RR _D ( x e. ( A (,) B ) |-> G ) ) = ( x e. ( A (,) B ) |-> H ) )
7 dvle2.7 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> F <_ H )
8 dvle2.8 
 |-  ( x = A -> E = P )
9 dvle2.9 
 |-  ( x = A -> G = Q )
10 dvle2.10 
 |-  ( x = B -> E = R )
11 dvle2.11 
 |-  ( x = B -> G = S )
12 dvle2.12 
 |-  ( ph -> P <_ Q )
13 dvle2.13 
 |-  ( ph -> A <_ B )
14 10 eleq1d 
 |-  ( x = B -> ( E e. RR <-> R e. RR ) )
15 cncff 
 |-  ( ( x e. ( A [,] B ) |-> E ) e. ( ( A [,] B ) -cn-> RR ) -> ( x e. ( A [,] B ) |-> E ) : ( A [,] B ) --> RR )
16 3 15 syl 
 |-  ( ph -> ( x e. ( A [,] B ) |-> E ) : ( A [,] B ) --> RR )
17 eqid 
 |-  ( x e. ( A [,] B ) |-> E ) = ( x e. ( A [,] B ) |-> E )
18 17 fmpt 
 |-  ( A. x e. ( A [,] B ) E e. RR <-> ( x e. ( A [,] B ) |-> E ) : ( A [,] B ) --> RR )
19 16 18 sylibr 
 |-  ( ph -> A. x e. ( A [,] B ) E e. RR )
20 2 rexrd 
 |-  ( ph -> B e. RR* )
21 2 leidd 
 |-  ( ph -> B <_ B )
22 20 13 21 3jca 
 |-  ( ph -> ( B e. RR* /\ A <_ B /\ B <_ B ) )
23 1 rexrd 
 |-  ( ph -> A e. RR* )
24 elicc1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( B e. ( A [,] B ) <-> ( B e. RR* /\ A <_ B /\ B <_ B ) ) )
25 23 20 24 syl2anc 
 |-  ( ph -> ( B e. ( A [,] B ) <-> ( B e. RR* /\ A <_ B /\ B <_ B ) ) )
26 22 25 mpbird 
 |-  ( ph -> B e. ( A [,] B ) )
27 14 19 26 rspcdva 
 |-  ( ph -> R e. RR )
28 8 eleq1d 
 |-  ( x = A -> ( E e. RR <-> P e. RR ) )
29 1 leidd 
 |-  ( ph -> A <_ A )
30 23 29 13 3jca 
 |-  ( ph -> ( A e. RR* /\ A <_ A /\ A <_ B ) )
31 elicc1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A e. ( A [,] B ) <-> ( A e. RR* /\ A <_ A /\ A <_ B ) ) )
32 23 20 31 syl2anc 
 |-  ( ph -> ( A e. ( A [,] B ) <-> ( A e. RR* /\ A <_ A /\ A <_ B ) ) )
33 30 32 mpbird 
 |-  ( ph -> A e. ( A [,] B ) )
34 28 19 33 rspcdva 
 |-  ( ph -> P e. RR )
35 27 34 resubcld 
 |-  ( ph -> ( R - P ) e. RR )
36 11 eleq1d 
 |-  ( x = B -> ( G e. RR <-> S e. RR ) )
37 cncff 
 |-  ( ( x e. ( A [,] B ) |-> G ) e. ( ( A [,] B ) -cn-> RR ) -> ( x e. ( A [,] B ) |-> G ) : ( A [,] B ) --> RR )
38 4 37 syl 
 |-  ( ph -> ( x e. ( A [,] B ) |-> G ) : ( A [,] B ) --> RR )
39 eqid 
 |-  ( x e. ( A [,] B ) |-> G ) = ( x e. ( A [,] B ) |-> G )
40 39 fmpt 
 |-  ( A. x e. ( A [,] B ) G e. RR <-> ( x e. ( A [,] B ) |-> G ) : ( A [,] B ) --> RR )
41 38 40 sylibr 
 |-  ( ph -> A. x e. ( A [,] B ) G e. RR )
42 36 41 26 rspcdva 
 |-  ( ph -> S e. RR )
43 9 eleq1d 
 |-  ( x = A -> ( G e. RR <-> Q e. RR ) )
44 43 41 33 rspcdva 
 |-  ( ph -> Q e. RR )
45 42 44 resubcld 
 |-  ( ph -> ( S - Q ) e. RR )
46 1 2 3 5 4 6 7 33 26 13 8 9 10 11 dvle 
 |-  ( ph -> ( R - P ) <_ ( S - Q ) )
47 35 34 45 44 46 12 le2addd 
 |-  ( ph -> ( ( R - P ) + P ) <_ ( ( S - Q ) + Q ) )
48 27 recnd 
 |-  ( ph -> R e. CC )
49 34 recnd 
 |-  ( ph -> P e. CC )
50 48 49 npcand 
 |-  ( ph -> ( ( R - P ) + P ) = R )
51 42 recnd 
 |-  ( ph -> S e. CC )
52 44 recnd 
 |-  ( ph -> Q e. CC )
53 51 52 npcand 
 |-  ( ph -> ( ( S - Q ) + Q ) = S )
54 50 53 breq12d 
 |-  ( ph -> ( ( ( R - P ) + P ) <_ ( ( S - Q ) + Q ) <-> R <_ S ) )
55 47 54 mpbid 
 |-  ( ph -> R <_ S )