# Metamath Proof Explorer

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 ${⊢}{\phi }\to {A}\subseteq ℝ$
supadd.a2 ${⊢}{\phi }\to {A}\ne \varnothing$
supadd.a3 ${⊢}{\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}$
supaddc.b ${⊢}{\phi }\to {B}\in ℝ$
supaddc.c ${⊢}{C}=\left\{{z}|\exists {v}\in {A}\phantom{\rule{.4em}{0ex}}{z}={v}+{B}\right\}$
Assertion supaddc ${⊢}{\phi }\to sup\left({A},ℝ,<\right)+{B}=sup\left({C},ℝ,<\right)$

### Proof

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