MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  supaddc Structured version   Visualization version   GIF version

Theorem supaddc 11595
Description: The supremum function distributes over addition in a sense similar to that in supmul1 11597. (Contributed by Brendan Leahy, 25-Sep-2017.)
Hypotheses
Ref Expression
supadd.a1 (𝜑𝐴 ⊆ ℝ)
supadd.a2 (𝜑𝐴 ≠ ∅)
supadd.a3 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥)
supaddc.b (𝜑𝐵 ∈ ℝ)
supaddc.c 𝐶 = {𝑧 ∣ ∃𝑣𝐴 𝑧 = (𝑣 + 𝐵)}
Assertion
Ref Expression
supaddc (𝜑 → (sup(𝐴, ℝ, < ) + 𝐵) = sup(𝐶, ℝ, < ))
Distinct variable groups:   𝑥,𝑦,𝑧,𝑣,𝐴   𝑥,𝐵,𝑦,𝑧,𝑣   𝑥,𝐶   𝜑,𝑧,𝑣
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐶(𝑦,𝑧,𝑣)

Proof of Theorem supaddc
Dummy variables 𝑤 𝑎 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 3472 . . . . . . 7 𝑤 ∈ V
2 oveq1 7147 . . . . . . . . . 10 (𝑣 = 𝑎 → (𝑣 + 𝐵) = (𝑎 + 𝐵))
32eqeq2d 2833 . . . . . . . . 9 (𝑣 = 𝑎 → (𝑧 = (𝑣 + 𝐵) ↔ 𝑧 = (𝑎 + 𝐵)))
43cbvrexvw 3425 . . . . . . . 8 (∃𝑣𝐴 𝑧 = (𝑣 + 𝐵) ↔ ∃𝑎𝐴 𝑧 = (𝑎 + 𝐵))
5 eqeq1 2826 . . . . . . . . 9 (𝑧 = 𝑤 → (𝑧 = (𝑎 + 𝐵) ↔ 𝑤 = (𝑎 + 𝐵)))
65rexbidv 3283 . . . . . . . 8 (𝑧 = 𝑤 → (∃𝑎𝐴 𝑧 = (𝑎 + 𝐵) ↔ ∃𝑎𝐴 𝑤 = (𝑎 + 𝐵)))
74, 6syl5bb 286 . . . . . . 7 (𝑧 = 𝑤 → (∃𝑣𝐴 𝑧 = (𝑣 + 𝐵) ↔ ∃𝑎𝐴 𝑤 = (𝑎 + 𝐵)))
8 supaddc.c . . . . . . 7 𝐶 = {𝑧 ∣ ∃𝑣𝐴 𝑧 = (𝑣 + 𝐵)}
91, 7, 8elab2 3645 . . . . . 6 (𝑤𝐶 ↔ ∃𝑎𝐴 𝑤 = (𝑎 + 𝐵))
10 supadd.a1 . . . . . . . . . 10 (𝜑𝐴 ⊆ ℝ)
1110sselda 3942 . . . . . . . . 9 ((𝜑𝑎𝐴) → 𝑎 ∈ ℝ)
12 supadd.a2 . . . . . . . . . . 11 (𝜑𝐴 ≠ ∅)
13 supadd.a3 . . . . . . . . . . 11 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥)
1410, 12, 13suprcld 11591 . . . . . . . . . 10 (𝜑 → sup(𝐴, ℝ, < ) ∈ ℝ)
1514adantr 484 . . . . . . . . 9 ((𝜑𝑎𝐴) → sup(𝐴, ℝ, < ) ∈ ℝ)
16 supaddc.b . . . . . . . . . 10 (𝜑𝐵 ∈ ℝ)
1716adantr 484 . . . . . . . . 9 ((𝜑𝑎𝐴) → 𝐵 ∈ ℝ)
1810, 12, 133jca 1125 . . . . . . . . . 10 (𝜑 → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥))
19 suprub 11589 . . . . . . . . . 10 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) ∧ 𝑎𝐴) → 𝑎 ≤ sup(𝐴, ℝ, < ))
2018, 19sylan 583 . . . . . . . . 9 ((𝜑𝑎𝐴) → 𝑎 ≤ sup(𝐴, ℝ, < ))
2111, 15, 17, 20leadd1dd 11243 . . . . . . . 8 ((𝜑𝑎𝐴) → (𝑎 + 𝐵) ≤ (sup(𝐴, ℝ, < ) + 𝐵))
22 breq1 5045 . . . . . . . 8 (𝑤 = (𝑎 + 𝐵) → (𝑤 ≤ (sup(𝐴, ℝ, < ) + 𝐵) ↔ (𝑎 + 𝐵) ≤ (sup(𝐴, ℝ, < ) + 𝐵)))
2321, 22syl5ibrcom 250 . . . . . . 7 ((𝜑𝑎𝐴) → (𝑤 = (𝑎 + 𝐵) → 𝑤 ≤ (sup(𝐴, ℝ, < ) + 𝐵)))
2423rexlimdva 3270 . . . . . 6 (𝜑 → (∃𝑎𝐴 𝑤 = (𝑎 + 𝐵) → 𝑤 ≤ (sup(𝐴, ℝ, < ) + 𝐵)))
259, 24syl5bi 245 . . . . 5 (𝜑 → (𝑤𝐶𝑤 ≤ (sup(𝐴, ℝ, < ) + 𝐵)))
2625ralrimiv 3173 . . . 4 (𝜑 → ∀𝑤𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + 𝐵))
2711, 17readdcld 10659 . . . . . . . . 9 ((𝜑𝑎𝐴) → (𝑎 + 𝐵) ∈ ℝ)
28 eleq1a 2909 . . . . . . . . 9 ((𝑎 + 𝐵) ∈ ℝ → (𝑤 = (𝑎 + 𝐵) → 𝑤 ∈ ℝ))
2927, 28syl 17 . . . . . . . 8 ((𝜑𝑎𝐴) → (𝑤 = (𝑎 + 𝐵) → 𝑤 ∈ ℝ))
3029rexlimdva 3270 . . . . . . 7 (𝜑 → (∃𝑎𝐴 𝑤 = (𝑎 + 𝐵) → 𝑤 ∈ ℝ))
319, 30syl5bi 245 . . . . . 6 (𝜑 → (𝑤𝐶𝑤 ∈ ℝ))
3231ssrdv 3948 . . . . 5 (𝜑𝐶 ⊆ ℝ)
33 ovex 7173 . . . . . . . . 9 (𝑎 + 𝐵) ∈ V
3433isseti 3483 . . . . . . . 8 𝑤 𝑤 = (𝑎 + 𝐵)
3534rgenw 3142 . . . . . . 7 𝑎𝐴𝑤 𝑤 = (𝑎 + 𝐵)
36 r19.2z 4412 . . . . . . 7 ((𝐴 ≠ ∅ ∧ ∀𝑎𝐴𝑤 𝑤 = (𝑎 + 𝐵)) → ∃𝑎𝐴𝑤 𝑤 = (𝑎 + 𝐵))
3712, 35, 36sylancl 589 . . . . . 6 (𝜑 → ∃𝑎𝐴𝑤 𝑤 = (𝑎 + 𝐵))
389exbii 1849 . . . . . . 7 (∃𝑤 𝑤𝐶 ↔ ∃𝑤𝑎𝐴 𝑤 = (𝑎 + 𝐵))
39 n0 4282 . . . . . . 7 (𝐶 ≠ ∅ ↔ ∃𝑤 𝑤𝐶)
40 rexcom4 3237 . . . . . . 7 (∃𝑎𝐴𝑤 𝑤 = (𝑎 + 𝐵) ↔ ∃𝑤𝑎𝐴 𝑤 = (𝑎 + 𝐵))
4138, 39, 403bitr4i 306 . . . . . 6 (𝐶 ≠ ∅ ↔ ∃𝑎𝐴𝑤 𝑤 = (𝑎 + 𝐵))
4237, 41sylibr 237 . . . . 5 (𝜑𝐶 ≠ ∅)
4314, 16readdcld 10659 . . . . . 6 (𝜑 → (sup(𝐴, ℝ, < ) + 𝐵) ∈ ℝ)
44 brralrspcev 5102 . . . . . 6 (((sup(𝐴, ℝ, < ) + 𝐵) ∈ ℝ ∧ ∀𝑤𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + 𝐵)) → ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥)
4543, 26, 44syl2anc 587 . . . . 5 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥)
46 suprleub 11594 . . . . 5 (((𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥) ∧ (sup(𝐴, ℝ, < ) + 𝐵) ∈ ℝ) → (sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + 𝐵) ↔ ∀𝑤𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + 𝐵)))
4732, 42, 45, 43, 46syl31anc 1370 . . . 4 (𝜑 → (sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + 𝐵) ↔ ∀𝑤𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + 𝐵)))
4826, 47mpbird 260 . . 3 (𝜑 → sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + 𝐵))
4932, 42, 45suprcld 11591 . . . . . . 7 (𝜑 → sup(𝐶, ℝ, < ) ∈ ℝ)
5049, 16, 14ltsubaddd 11225 . . . . . 6 (𝜑 → ((sup(𝐶, ℝ, < ) − 𝐵) < sup(𝐴, ℝ, < ) ↔ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵)))
5150biimpar 481 . . . . 5 ((𝜑 ∧ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵)) → (sup(𝐶, ℝ, < ) − 𝐵) < sup(𝐴, ℝ, < ))
5249, 16resubcld 11057 . . . . . . 7 (𝜑 → (sup(𝐶, ℝ, < ) − 𝐵) ∈ ℝ)
53 suprlub 11592 . . . . . . 7 (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦𝑥) ∧ (sup(𝐶, ℝ, < ) − 𝐵) ∈ ℝ) → ((sup(𝐶, ℝ, < ) − 𝐵) < sup(𝐴, ℝ, < ) ↔ ∃𝑎𝐴 (sup(𝐶, ℝ, < ) − 𝐵) < 𝑎))
5410, 12, 13, 52, 53syl31anc 1370 . . . . . 6 (𝜑 → ((sup(𝐶, ℝ, < ) − 𝐵) < sup(𝐴, ℝ, < ) ↔ ∃𝑎𝐴 (sup(𝐶, ℝ, < ) − 𝐵) < 𝑎))
5554adantr 484 . . . . 5 ((𝜑 ∧ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵)) → ((sup(𝐶, ℝ, < ) − 𝐵) < sup(𝐴, ℝ, < ) ↔ ∃𝑎𝐴 (sup(𝐶, ℝ, < ) − 𝐵) < 𝑎))
5651, 55mpbid 235 . . . 4 ((𝜑 ∧ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵)) → ∃𝑎𝐴 (sup(𝐶, ℝ, < ) − 𝐵) < 𝑎)
5727adantlr 714 . . . . . . 7 (((𝜑 ∧ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵)) ∧ 𝑎𝐴) → (𝑎 + 𝐵) ∈ ℝ)
5849ad2antrr 725 . . . . . . 7 (((𝜑 ∧ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵)) ∧ 𝑎𝐴) → sup(𝐶, ℝ, < ) ∈ ℝ)
59 rspe 3290 . . . . . . . . . . . . . 14 ((𝑎𝐴𝑤 = (𝑎 + 𝐵)) → ∃𝑎𝐴 𝑤 = (𝑎 + 𝐵))
6059, 9sylibr 237 . . . . . . . . . . . . 13 ((𝑎𝐴𝑤 = (𝑎 + 𝐵)) → 𝑤𝐶)
6160adantl 485 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎𝐴𝑤 = (𝑎 + 𝐵))) → 𝑤𝐶)
62 simplrr 777 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎𝐴𝑤 = (𝑎 + 𝐵))) ∧ 𝑤𝐶) → 𝑤 = (𝑎 + 𝐵))
6332, 42, 453jca 1125 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥))
64 suprub 11589 . . . . . . . . . . . . . . 15 (((𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝐶 𝑤𝑥) ∧ 𝑤𝐶) → 𝑤 ≤ sup(𝐶, ℝ, < ))
6563, 64sylan 583 . . . . . . . . . . . . . 14 ((𝜑𝑤𝐶) → 𝑤 ≤ sup(𝐶, ℝ, < ))
6665adantlr 714 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎𝐴𝑤 = (𝑎 + 𝐵))) ∧ 𝑤𝐶) → 𝑤 ≤ sup(𝐶, ℝ, < ))
6762, 66eqbrtrrd 5066 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎𝐴𝑤 = (𝑎 + 𝐵))) ∧ 𝑤𝐶) → (𝑎 + 𝐵) ≤ sup(𝐶, ℝ, < ))
6861, 67mpdan 686 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝐴𝑤 = (𝑎 + 𝐵))) → (𝑎 + 𝐵) ≤ sup(𝐶, ℝ, < ))
6968expr 460 . . . . . . . . . 10 ((𝜑𝑎𝐴) → (𝑤 = (𝑎 + 𝐵) → (𝑎 + 𝐵) ≤ sup(𝐶, ℝ, < )))
7069exlimdv 1934 . . . . . . . . 9 ((𝜑𝑎𝐴) → (∃𝑤 𝑤 = (𝑎 + 𝐵) → (𝑎 + 𝐵) ≤ sup(𝐶, ℝ, < )))
7134, 70mpi 20 . . . . . . . 8 ((𝜑𝑎𝐴) → (𝑎 + 𝐵) ≤ sup(𝐶, ℝ, < ))
7271adantlr 714 . . . . . . 7 (((𝜑 ∧ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵)) ∧ 𝑎𝐴) → (𝑎 + 𝐵) ≤ sup(𝐶, ℝ, < ))
7357, 58, 72lensymd 10780 . . . . . 6 (((𝜑 ∧ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵)) ∧ 𝑎𝐴) → ¬ sup(𝐶, ℝ, < ) < (𝑎 + 𝐵))
7416ad2antrr 725 . . . . . . 7 (((𝜑 ∧ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵)) ∧ 𝑎𝐴) → 𝐵 ∈ ℝ)
7511adantlr 714 . . . . . . 7 (((𝜑 ∧ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵)) ∧ 𝑎𝐴) → 𝑎 ∈ ℝ)
7658, 74, 75ltsubaddd 11225 . . . . . 6 (((𝜑 ∧ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵)) ∧ 𝑎𝐴) → ((sup(𝐶, ℝ, < ) − 𝐵) < 𝑎 ↔ sup(𝐶, ℝ, < ) < (𝑎 + 𝐵)))
7773, 76mtbird 328 . . . . 5 (((𝜑 ∧ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵)) ∧ 𝑎𝐴) → ¬ (sup(𝐶, ℝ, < ) − 𝐵) < 𝑎)
7877nrexdv 3256 . . . 4 ((𝜑 ∧ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵)) → ¬ ∃𝑎𝐴 (sup(𝐶, ℝ, < ) − 𝐵) < 𝑎)
7956, 78pm2.65da 816 . . 3 (𝜑 → ¬ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵))
8049, 43eqleltd 10773 . . 3 (𝜑 → (sup(𝐶, ℝ, < ) = (sup(𝐴, ℝ, < ) + 𝐵) ↔ (sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + 𝐵) ∧ ¬ sup(𝐶, ℝ, < ) < (sup(𝐴, ℝ, < ) + 𝐵))))
8148, 79, 80mpbir2and 712 . 2 (𝜑 → sup(𝐶, ℝ, < ) = (sup(𝐴, ℝ, < ) + 𝐵))
8281eqcomd 2828 1 (𝜑 → (sup(𝐴, ℝ, < ) + 𝐵) = sup(𝐶, ℝ, < ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wex 1781  wcel 2114  {cab 2800  wne 3011  wral 3130  wrex 3131  wss 3908  c0 4265   class class class wbr 5042  (class class class)co 7140  supcsup 8892  cr 10525   + caddc 10529   < clt 10664  cle 10665  cmin 10859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-nel 3116  df-ral 3135  df-rex 3136  df-reu 3137  df-rmo 3138  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5437  df-po 5451  df-so 5452  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-sup 8894  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862
This theorem is referenced by:  supadd  11596  supsubc  41924
  Copyright terms: Public domain W3C validator