Metamath Proof Explorer

Theorem supaddc

Description: The supremum function distributes over addition in a sense similar to that in supmul1 . (Contributed by Brendan Leahy, 25-Sep-2017)

Ref Expression
Hypotheses supadd.a1 
|- ( ph -> A C_ RR )
supadd.a2 
|- ( ph -> A =/= (/) )
supadd.a3 
|- ( ph -> E. x e. RR A. y e. A y <_ x )
supaddc.b 
|- ( ph -> B e. RR )
supaddc.c 
|- C = { z | E. v e. A z = ( v + B ) }
Assertion supaddc 
|- ( ph -> ( sup ( A , RR , < ) + B ) = sup ( C , RR , < ) )

Proof

Step Hyp Ref Expression
1 supadd.a1 
 |-  ( ph -> A C_ RR )
2 supadd.a2 
 |-  ( ph -> A =/= (/) )
3 supadd.a3 
 |-  ( ph -> E. x e. RR A. y e. A y <_ x )
4 supaddc.b 
 |-  ( ph -> B e. RR )
5 supaddc.c 
 |-  C = { z | E. v e. A z = ( v + B ) }
6 vex 
 |-  w e. _V
7 oveq1 
 |-  ( v = a -> ( v + B ) = ( a + B ) )
8 7 eqeq2d 
 |-  ( v = a -> ( z = ( v + B ) <-> z = ( a + B ) ) )
9 8 cbvrexvw 
 |-  ( E. v e. A z = ( v + B ) <-> E. a e. A z = ( a + B ) )
10 eqeq1 
 |-  ( z = w -> ( z = ( a + B ) <-> w = ( a + B ) ) )
11 10 rexbidv 
 |-  ( z = w -> ( E. a e. A z = ( a + B ) <-> E. a e. A w = ( a + B ) ) )
12 9 11 syl5bb 
 |-  ( z = w -> ( E. v e. A z = ( v + B ) <-> E. a e. A w = ( a + B ) ) )
13 6 12 5 elab2 
 |-  ( w e. C <-> E. a e. A w = ( a + B ) )
14 1 sselda 
 |-  ( ( ph /\ a e. A ) -> a e. RR )
15 1 2 3 suprcld 
 |-  ( ph -> sup ( A , RR , < ) e. RR )
16 15 adantr 
 |-  ( ( ph /\ a e. A ) -> sup ( A , RR , < ) e. RR )
17 4 adantr 
 |-  ( ( ph /\ a e. A ) -> B e. RR )
18 1 2 3 3jca 
 |-  ( ph -> ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) )
19 suprub 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ a e. A ) -> a <_ sup ( A , RR , < ) )
20 18 19 sylan 
 |-  ( ( ph /\ a e. A ) -> a <_ sup ( A , RR , < ) )
21 14 16 17 20 leadd1dd 
 |-  ( ( ph /\ a e. A ) -> ( a + B ) <_ ( sup ( A , RR , < ) + B ) )
22 breq1 
 |-  ( w = ( a + B ) -> ( w <_ ( sup ( A , RR , < ) + B ) <-> ( a + B ) <_ ( sup ( A , RR , < ) + B ) ) )
23 21 22 syl5ibrcom 
 |-  ( ( ph /\ a e. A ) -> ( w = ( a + B ) -> w <_ ( sup ( A , RR , < ) + B ) ) )
24 23 rexlimdva 
 |-  ( ph -> ( E. a e. A w = ( a + B ) -> w <_ ( sup ( A , RR , < ) + B ) ) )
25 13 24 syl5bi 
 |-  ( ph -> ( w e. C -> w <_ ( sup ( A , RR , < ) + B ) ) )
26 25 ralrimiv 
 |-  ( ph -> A. w e. C w <_ ( sup ( A , RR , < ) + B ) )
27 14 17 readdcld 
 |-  ( ( ph /\ a e. A ) -> ( a + B ) e. RR )
28 eleq1a 
 |-  ( ( a + B ) e. RR -> ( w = ( a + B ) -> w e. RR ) )
29 27 28 syl 
 |-  ( ( ph /\ a e. A ) -> ( w = ( a + B ) -> w e. RR ) )
30 29 rexlimdva 
 |-  ( ph -> ( E. a e. A w = ( a + B ) -> w e. RR ) )
31 13 30 syl5bi 
 |-  ( ph -> ( w e. C -> w e. RR ) )
32 31 ssrdv 
 |-  ( ph -> C C_ RR )
33 ovex 
 |-  ( a + B ) e. _V
34 33 isseti 
 |-  E. w w = ( a + B )
35 34 rgenw 
 |-  A. a e. A E. w w = ( a + B )
36 r19.2z 
 |-  ( ( A =/= (/) /\ A. a e. A E. w w = ( a + B ) ) -> E. a e. A E. w w = ( a + B ) )
37 2 35 36 sylancl 
 |-  ( ph -> E. a e. A E. w w = ( a + B ) )
38 13 exbii 
 |-  ( E. w w e. C <-> E. w E. a e. A w = ( a + B ) )
39 n0 
 |-  ( C =/= (/) <-> E. w w e. C )
40 rexcom4 
 |-  ( E. a e. A E. w w = ( a + B ) <-> E. w E. a e. A w = ( a + B ) )
41 38 39 40 3bitr4i 
 |-  ( C =/= (/) <-> E. a e. A E. w w = ( a + B ) )
42 37 41 sylibr 
 |-  ( ph -> C =/= (/) )
43 15 4 readdcld 
 |-  ( ph -> ( sup ( A , RR , < ) + B ) e. RR )
44 brralrspcev 
 |-  ( ( ( sup ( A , RR , < ) + B ) e. RR /\ A. w e. C w <_ ( sup ( A , RR , < ) + B ) ) -> E. x e. RR A. w e. C w <_ x )
45 43 26 44 syl2anc 
 |-  ( ph -> E. x e. RR A. w e. C w <_ x )
46 suprleub 
 |-  ( ( ( C C_ RR /\ C =/= (/) /\ E. x e. RR A. w e. C w <_ x ) /\ ( sup ( A , RR , < ) + B ) e. RR ) -> ( sup ( C , RR , < ) <_ ( sup ( A , RR , < ) + B ) <-> A. w e. C w <_ ( sup ( A , RR , < ) + B ) ) )
47 32 42 45 43 46 syl31anc 
 |-  ( ph -> ( sup ( C , RR , < ) <_ ( sup ( A , RR , < ) + B ) <-> A. w e. C w <_ ( sup ( A , RR , < ) + B ) ) )
48 26 47 mpbird 
 |-  ( ph -> sup ( C , RR , < ) <_ ( sup ( A , RR , < ) + B ) )
49 32 42 45 suprcld 
 |-  ( ph -> sup ( C , RR , < ) e. RR )
50 49 4 15 ltsubaddd 
 |-  ( ph -> ( ( sup ( C , RR , < ) - B ) < sup ( A , RR , < ) <-> sup ( C , RR , < ) < ( sup ( A , RR , < ) + B ) ) )
51 50 biimpar 
 |-  ( ( ph /\ sup ( C , RR , < ) < ( sup ( A , RR , < ) + B ) ) -> ( sup ( C , RR , < ) - B ) < sup ( A , RR , < ) )
52 49 4 resubcld 
 |-  ( ph -> ( sup ( C , RR , < ) - B ) e. RR )
53 suprlub 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( sup ( C , RR , < ) - B ) e. RR ) -> ( ( sup ( C , RR , < ) - B ) < sup ( A , RR , < ) <-> E. a e. A ( sup ( C , RR , < ) - B ) < a ) )
54 1 2 3 52 53 syl31anc 
 |-  ( ph -> ( ( sup ( C , RR , < ) - B ) < sup ( A , RR , < ) <-> E. a e. A ( sup ( C , RR , < ) - B ) < a ) )
55 54 adantr 
 |-  ( ( ph /\ sup ( C , RR , < ) < ( sup ( A , RR , < ) + B ) ) -> ( ( sup ( C , RR , < ) - B ) < sup ( A , RR , < ) <-> E. a e. A ( sup ( C , RR , < ) - B ) < a ) )
56 51 55 mpbid 
 |-  ( ( ph /\ sup ( C , RR , < ) < ( sup ( A , RR , < ) + B ) ) -> E. a e. A ( sup ( C , RR , < ) - B ) < a )
57 27 adantlr 
 |-  ( ( ( ph /\ sup ( C , RR , < ) < ( sup ( A , RR , < ) + B ) ) /\ a e. A ) -> ( a + B ) e. RR )
58 49 ad2antrr 
 |-  ( ( ( ph /\ sup ( C , RR , < ) < ( sup ( A , RR , < ) + B ) ) /\ a e. A ) -> sup ( C , RR , < ) e. RR )
59 rspe 
 |-  ( ( a e. A /\ w = ( a + B ) ) -> E. a e. A w = ( a + B ) )
60 59 13 sylibr 
 |-  ( ( a e. A /\ w = ( a + B ) ) -> w e. C )
61 60 adantl 
 |-  ( ( ph /\ ( a e. A /\ w = ( a + B ) ) ) -> w e. C )
62 simplrr 
 |-  ( ( ( ph /\ ( a e. A /\ w = ( a + B ) ) ) /\ w e. C ) -> w = ( a + B ) )
63 32 42 45 3jca 
 |-  ( ph -> ( C C_ RR /\ C =/= (/) /\ E. x e. RR A. w e. C w <_ x ) )
64 suprub 
 |-  ( ( ( C C_ RR /\ C =/= (/) /\ E. x e. RR A. w e. C w <_ x ) /\ w e. C ) -> w <_ sup ( C , RR , < ) )
65 63 64 sylan 
 |-  ( ( ph /\ w e. C ) -> w <_ sup ( C , RR , < ) )
66 65 adantlr 
 |-  ( ( ( ph /\ ( a e. A /\ w = ( a + B ) ) ) /\ w e. C ) -> w <_ sup ( C , RR , < ) )
67 62 66 eqbrtrrd 
 |-  ( ( ( ph /\ ( a e. A /\ w = ( a + B ) ) ) /\ w e. C ) -> ( a + B ) <_ sup ( C , RR , < ) )
68 61 67 mpdan 
 |-  ( ( ph /\ ( a e. A /\ w = ( a + B ) ) ) -> ( a + B ) <_ sup ( C , RR , < ) )
69 68 expr 
 |-  ( ( ph /\ a e. A ) -> ( w = ( a + B ) -> ( a + B ) <_ sup ( C , RR , < ) ) )
70 69 exlimdv 
 |-  ( ( ph /\ a e. A ) -> ( E. w w = ( a + B ) -> ( a + B ) <_ sup ( C , RR , < ) ) )
71 34 70 mpi 
 |-  ( ( ph /\ a e. A ) -> ( a + B ) <_ sup ( C , RR , < ) )
72 71 adantlr 
 |-  ( ( ( ph /\ sup ( C , RR , < ) < ( sup ( A , RR , < ) + B ) ) /\ a e. A ) -> ( a + B ) <_ sup ( C , RR , < ) )
73 57 58 72 lensymd 
 |-  ( ( ( ph /\ sup ( C , RR , < ) < ( sup ( A , RR , < ) + B ) ) /\ a e. A ) -> -. sup ( C , RR , < ) < ( a + B ) )
74 4 ad2antrr 
 |-  ( ( ( ph /\ sup ( C , RR , < ) < ( sup ( A , RR , < ) + B ) ) /\ a e. A ) -> B e. RR )
75 14 adantlr 
 |-  ( ( ( ph /\ sup ( C , RR , < ) < ( sup ( A , RR , < ) + B ) ) /\ a e. A ) -> a e. RR )
76 58 74 75 ltsubaddd 
 |-  ( ( ( ph /\ sup ( C , RR , < ) < ( sup ( A , RR , < ) + B ) ) /\ a e. A ) -> ( ( sup ( C , RR , < ) - B ) < a <-> sup ( C , RR , < ) < ( a + B ) ) )
77 73 76 mtbird 
 |-  ( ( ( ph /\ sup ( C , RR , < ) < ( sup ( A , RR , < ) + B ) ) /\ a e. A ) -> -. ( sup ( C , RR , < ) - B ) < a )
78 77 nrexdv 
 |-  ( ( ph /\ sup ( C , RR , < ) < ( sup ( A , RR , < ) + B ) ) -> -. E. a e. A ( sup ( C , RR , < ) - B ) < a )
79 56 78 pm2.65da 
 |-  ( ph -> -. sup ( C , RR , < ) < ( sup ( A , RR , < ) + B ) )
80 49 43 eqleltd 
 |-  ( ph -> ( sup ( C , RR , < ) = ( sup ( A , RR , < ) + B ) <-> ( sup ( C , RR , < ) <_ ( sup ( A , RR , < ) + B ) /\ -. sup ( C , RR , < ) < ( sup ( A , RR , < ) + B ) ) ) )
81 48 79 80 mpbir2and 
 |-  ( ph -> sup ( C , RR , < ) = ( sup ( A , RR , < ) + B ) )
82 81 eqcomd 
 |-  ( ph -> ( sup ( A , RR , < ) + B ) = sup ( C , RR , < ) )