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	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	supadd.a2	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
	supadd.a3	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
	supaddc.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	supaddc.c	⊢ 𝐶 = { 𝑧 ∣ ∃ 𝑣 ∈ 𝐴 𝑧 = ( 𝑣 + 𝐵 ) }
Assertion	supaddc	⊢ ( 𝜑 → ( sup ( 𝐴 , ℝ , < ) + 𝐵 ) = sup ( 𝐶 , ℝ , < ) )

Proof

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