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 ⊢φ→A⊆ℝ
supadd.a2 ⊢φ→A≠∅
supadd.a3 ⊢φ→∃x∈ℝ∀y∈Ay≤x
supaddc.b ⊢φ→B∈ℝ
supaddc.c ⊢C=z|∃v∈Az=v+B
Assertion supaddc ⊢φ→supAℝ<+B=supCℝ<

Proof

Step Hyp Ref Expression
1 supadd.a1 ⊢φ→A⊆ℝ
2 supadd.a2 ⊢φ→A≠∅
3 supadd.a3 ⊢φ→∃x∈ℝ∀y∈Ay≤x
4 supaddc.b ⊢φ→B∈ℝ
5 supaddc.c ⊢C=z|∃v∈Az=v+B
6 vex ⊢w∈V
7 oveq1 ⊢v=a→v+B=a+B
8 7 eqeq2d ⊢v=a→z=v+B↔z=a+B
9 8 cbvrexvw ⊢∃v∈Az=v+B↔∃a∈Az=a+B
10 eqeq1 ⊢z=w→z=a+B↔w=a+B
11 10 rexbidv ⊢z=w→∃a∈Az=a+B↔∃a∈Aw=a+B
12 9 11 bitrid ⊢z=w→∃v∈Az=v+B↔∃a∈Aw=a+B
13 6 12 5 elab2 ⊢w∈C↔∃a∈Aw=a+B
14 1 sselda ⊢φ∧a∈A→a∈ℝ
15 1 2 3 suprcld ⊢φ→supAℝ<∈ℝ
16 15 adantr ⊢φ∧a∈A→supAℝ<∈ℝ
17 4 adantr ⊢φ∧a∈A→B∈ℝ
18 1 2 3 3jca ⊢φ→A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x
19 suprub ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧a∈A→a≤supAℝ<
20 18 19 sylan ⊢φ∧a∈A→a≤supAℝ<
21 14 16 17 20 leadd1dd ⊢φ∧a∈A→a+B≤supAℝ<+B
22 breq1 ⊢w=a+B→w≤supAℝ<+B↔a+B≤supAℝ<+B
23 21 22 syl5ibrcom ⊢φ∧a∈A→w=a+B→w≤supAℝ<+B
24 23 rexlimdva ⊢φ→∃a∈Aw=a+B→w≤supAℝ<+B
25 13 24 biimtrid ⊢φ→w∈C→w≤supAℝ<+B
26 25 ralrimiv ⊢φ→∀w∈Cw≤supAℝ<+B
27 14 17 readdcld ⊢φ∧a∈A→a+B∈ℝ
28 eleq1a ⊢a+B∈ℝ→w=a+B→w∈ℝ
29 27 28 syl ⊢φ∧a∈A→w=a+B→w∈ℝ
30 29 rexlimdva ⊢φ→∃a∈Aw=a+B→w∈ℝ
31 13 30 biimtrid ⊢φ→w∈C→w∈ℝ
32 31 ssrdv ⊢φ→C⊆ℝ
33 ovex ⊢a+B∈V
34 33 isseti ⊢∃ww=a+B
35 34 rgenw ⊢∀a∈A∃ww=a+B
36 r19.2z ⊢A≠∅∧∀a∈A∃ww=a+B→∃a∈A∃ww=a+B
37 2 35 36 sylancl ⊢φ→∃a∈A∃ww=a+B
38 13 exbii ⊢∃ww∈C↔∃w∃a∈Aw=a+B
39 n0 ⊢C≠∅↔∃ww∈C
40 rexcom4 ⊢∃a∈A∃ww=a+B↔∃w∃a∈Aw=a+B
41 38 39 40 3bitr4i ⊢C≠∅↔∃a∈A∃ww=a+B
42 37 41 sylibr ⊢φ→C≠∅
43 15 4 readdcld ⊢φ→supAℝ<+B∈ℝ
44 brralrspcev ⊢supAℝ<+B∈ℝ∧∀w∈Cw≤supAℝ<+B→∃x∈ℝ∀w∈Cw≤x
45 43 26 44 syl2anc ⊢φ→∃x∈ℝ∀w∈Cw≤x
46 suprleub ⊢C⊆ℝ∧C≠∅∧∃x∈ℝ∀w∈Cw≤x∧supAℝ<+B∈ℝ→supCℝ<≤supAℝ<+B↔∀w∈Cw≤supAℝ<+B
47 32 42 45 43 46 syl31anc ⊢φ→supCℝ<≤supAℝ<+B↔∀w∈Cw≤supAℝ<+B
48 26 47 mpbird ⊢φ→supCℝ<≤supAℝ<+B
49 32 42 45 suprcld ⊢φ→supCℝ<∈ℝ
50 49 4 15 ltsubaddd ⊢φ→supCℝ<−B<supAℝ<↔supCℝ<<supAℝ<+B
51 50 biimpar ⊢φ∧supCℝ<<supAℝ<+B→supCℝ<−B<supAℝ<
52 49 4 resubcld ⊢φ→supCℝ<−B∈ℝ
53 suprlub ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay≤x∧supCℝ<−B∈ℝ→supCℝ<−B<supAℝ<↔∃a∈AsupCℝ<−B<a
54 1 2 3 52 53 syl31anc ⊢φ→supCℝ<−B<supAℝ<↔∃a∈AsupCℝ<−B<a
55 54 adantr ⊢φ∧supCℝ<<supAℝ<+B→supCℝ<−B<supAℝ<↔∃a∈AsupCℝ<−B<a
56 51 55 mpbid ⊢φ∧supCℝ<<supAℝ<+B→∃a∈AsupCℝ<−B<a
57 27 adantlr ⊢φ∧supCℝ<<supAℝ<+B∧a∈A→a+B∈ℝ
58 49 ad2antrr ⊢φ∧supCℝ<<supAℝ<+B∧a∈A→supCℝ<∈ℝ
59 rspe ⊢a∈A∧w=a+B→∃a∈Aw=a+B
60 59 13 sylibr ⊢a∈A∧w=a+B→w∈C
61 60 adantl ⊢φ∧a∈A∧w=a+B→w∈C
62 simplrr ⊢φ∧a∈A∧w=a+B∧w∈C→w=a+B
63 32 42 45 3jca ⊢φ→C⊆ℝ∧C≠∅∧∃x∈ℝ∀w∈Cw≤x
64 suprub ⊢C⊆ℝ∧C≠∅∧∃x∈ℝ∀w∈Cw≤x∧w∈C→w≤supCℝ<
65 63 64 sylan ⊢φ∧w∈C→w≤supCℝ<
66 65 adantlr ⊢φ∧a∈A∧w=a+B∧w∈C→w≤supCℝ<
67 62 66 eqbrtrrd ⊢φ∧a∈A∧w=a+B∧w∈C→a+B≤supCℝ<
68 61 67 mpdan ⊢φ∧a∈A∧w=a+B→a+B≤supCℝ<
69 68 expr ⊢φ∧a∈A→w=a+B→a+B≤supCℝ<
70 69 exlimdv ⊢φ∧a∈A→∃ww=a+B→a+B≤supCℝ<
71 34 70 mpi ⊢φ∧a∈A→a+B≤supCℝ<
72 71 adantlr ⊢φ∧supCℝ<<supAℝ<+B∧a∈A→a+B≤supCℝ<
73 57 58 72 lensymd ⊢φ∧supCℝ<<supAℝ<+B∧a∈A→¬supCℝ<<a+B
74 4 ad2antrr ⊢φ∧supCℝ<<supAℝ<+B∧a∈A→B∈ℝ
75 14 adantlr ⊢φ∧supCℝ<<supAℝ<+B∧a∈A→a∈ℝ
76 58 74 75 ltsubaddd ⊢φ∧supCℝ<<supAℝ<+B∧a∈A→supCℝ<−B<a↔supCℝ<<a+B
77 73 76 mtbird ⊢φ∧supCℝ<<supAℝ<+B∧a∈A→¬supCℝ<−B<a
78 77 nrexdv ⊢φ∧supCℝ<<supAℝ<+B→¬∃a∈AsupCℝ<−B<a
79 56 78 pm2.65da ⊢φ→¬supCℝ<<supAℝ<+B
80 49 43 eqleltd ⊢φ→supCℝ<=supAℝ<+B↔supCℝ<≤supAℝ<+B∧¬supCℝ<<supAℝ<+B
81 48 79 80 mpbir2and ⊢φ→supCℝ<=supAℝ<+B
82 81 eqcomd ⊢φ→supAℝ<+B=supCℝ<