infleinflem1

Description: Lemma for infleinf , case B =/= (/) /\ -oo < inf ( B , RR* , < ) . (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	infleinflem1.a	$⊢ φ \to A \subseteq ℝ^{*}$
	infleinflem1.b	$⊢ φ \to B \subseteq ℝ^{*}$
	infleinflem1.w	$⊢ φ \to W \in ℝ^{+}$
	infleinflem1.x	$⊢ φ \to X \in B$
	infleinflem1.i	$⊢ φ \to X \leq sup (B ℝ^{*} <) +_{𝑒} (\frac{W}{2})$
	infleinflem1.z	$⊢ φ \to Z \in A$
	infleinflem1.l	$⊢ φ \to Z \leq X +_{𝑒} (\frac{W}{2})$
Assertion	infleinflem1	$⊢ φ \to sup (A ℝ^{} <) \leq sup (B ℝ^{} <) +_{𝑒} W$

Proof

Step	Hyp	Ref	Expression
1		infleinflem1.a	$⊢ φ \to A \subseteq ℝ^{*}$
2		infleinflem1.b	$⊢ φ \to B \subseteq ℝ^{*}$
3		infleinflem1.w	$⊢ φ \to W \in ℝ^{+}$
4		infleinflem1.x	$⊢ φ \to X \in B$
5		infleinflem1.i	$⊢ φ \to X \leq sup (B ℝ^{*} <) +_{𝑒} (\frac{W}{2})$
6		infleinflem1.z	$⊢ φ \to Z \in A$
7		infleinflem1.l	$⊢ φ \to Z \leq X +_{𝑒} (\frac{W}{2})$
8		infxrcl	$⊢ A \subseteq ℝ^{} \to sup (A ℝ^{} <) \in ℝ^{*}$
9	1 8	syl	$⊢ φ \to sup (A ℝ^{} <) \in ℝ^{}$
10		id	$⊢ sup (A ℝ^{} <) \in ℝ^{} \to sup (A ℝ^{} <) \in ℝ^{}$
11	9 10	syl	$⊢ φ \to sup (A ℝ^{} <) \in ℝ^{}$
12	1 6	sseldd	$⊢ φ \to Z \in ℝ^{*}$
13		infxrcl	$⊢ B \subseteq ℝ^{} \to sup (B ℝ^{} <) \in ℝ^{*}$
14	2 13	syl	$⊢ φ \to sup (B ℝ^{} <) \in ℝ^{}$
15		rpxr	$⊢ W \in ℝ^{+} \to W \in ℝ^{*}$
16	3 15	syl	$⊢ φ \to W \in ℝ^{*}$
17	14 16	xaddcld	$⊢ φ \to sup (B ℝ^{} <) +_{𝑒} W \in ℝ^{}$
18		infxrlb	$⊢ (A \subseteq ℝ^{} \land Z \in A) \to sup (A ℝ^{} <) \leq Z$
19	1 6 18	syl2anc	$⊢ φ \to sup (A ℝ^{*} <) \leq Z$
20	2	sselda	$⊢ (φ \land X \in B) \to X \in ℝ^{*}$
21	4 20	mpdan	$⊢ φ \to X \in ℝ^{*}$
22	3	rpred	$⊢ φ \to W \in ℝ$
23	22	rehalfcld	$⊢ φ \to \frac{W}{2} \in ℝ$
24	23	rexrd	$⊢ φ \to \frac{W}{2} \in ℝ^{*}$
25	21 24	xaddcld	$⊢ φ \to X +_{𝑒} (\frac{W}{2}) \in ℝ^{*}$
26		pnfge	$⊢ X +_{𝑒} (\frac{W}{2}) \in ℝ^{*} \to X +_{𝑒} (\frac{W}{2}) \leq +∞$
27	25 26	syl	$⊢ φ \to X +_{𝑒} (\frac{W}{2}) \leq +∞$
28	27	adantr	$⊢ (φ \land sup (B ℝ^{*} <) = +∞) \to X +_{𝑒} (\frac{W}{2}) \leq +∞$
29		oveq1	$⊢ sup (B ℝ^{} <) = +∞ \to sup (B ℝ^{} <) +_{𝑒} W = +∞ +_{𝑒} W$
30	29	adantl	$⊢ (φ \land sup (B ℝ^{} <) = +∞) \to sup (B ℝ^{} <) +_{𝑒} W = +∞ +_{𝑒} W$
31		rpre	$⊢ W \in ℝ^{+} \to W \in ℝ$
32		renemnf	$⊢ W \in ℝ \to W \neq −∞$
33	31 32	syl	$⊢ W \in ℝ^{+} \to W \neq −∞$
34		xaddpnf2	$⊢ (W \in ℝ^{*} \land W \neq −∞) \to +∞ +_{𝑒} W = +∞$
35	15 33 34	syl2anc	$⊢ W \in ℝ^{+} \to +∞ +_{𝑒} W = +∞$
36	3 35	syl	$⊢ φ \to +∞ +_{𝑒} W = +∞$
37	36	adantr	$⊢ (φ \land sup (B ℝ^{*} <) = +∞) \to +∞ +_{𝑒} W = +∞$
38	30 37	eqtr2d	$⊢ (φ \land sup (B ℝ^{} <) = +∞) \to +∞ = sup (B ℝ^{} <) +_{𝑒} W$
39	28 38	breqtrd	$⊢ (φ \land sup (B ℝ^{} <) = +∞) \to X +_{𝑒} (\frac{W}{2}) \leq sup (B ℝ^{} <) +_{𝑒} W$
40	2 4	sseldd	$⊢ φ \to X \in ℝ^{*}$
41	14 24	xaddcld	$⊢ φ \to sup (B ℝ^{} <) +_{𝑒} (\frac{W}{2}) \in ℝ^{}$
42		rphalfcl	$⊢ W \in ℝ^{+} \to \frac{W}{2} \in ℝ^{+}$
43	3 42	syl	$⊢ φ \to \frac{W}{2} \in ℝ^{+}$
44	43	rpxrd	$⊢ φ \to \frac{W}{2} \in ℝ^{*}$
45	40 41 44 5	xleadd1d	$⊢ φ \to X +_{𝑒} (\frac{W}{2}) \leq (sup (B ℝ^{*} <) +_{𝑒} (\frac{W}{2})) +_{𝑒} (\frac{W}{2})$
46	45	adantr	$⊢ (φ \land \neg sup (B ℝ^{} <) = +∞) \to X +_{𝑒} (\frac{W}{2}) \leq (sup (B ℝ^{} <) +_{𝑒} (\frac{W}{2})) +_{𝑒} (\frac{W}{2})$
47	14	adantr	$⊢ (φ \land \neg sup (B ℝ^{} <) = +∞) \to sup (B ℝ^{} <) \in ℝ^{*}$
48		neqne	$⊢ \neg sup (B ℝ^{} <) = +∞ \to sup (B ℝ^{} <) \neq +∞$
49	48	adantl	$⊢ (φ \land \neg sup (B ℝ^{} <) = +∞) \to sup (B ℝ^{} <) \neq +∞$
50	44	adantr	$⊢ (φ \land \neg sup (B ℝ^{} <) = +∞) \to \frac{W}{2} \in ℝ^{}$
51	3	adantr	$⊢ (φ \land \neg sup (B ℝ^{*} <) = +∞) \to W \in ℝ^{+}$
52		rpre	$⊢ \frac{W}{2} \in ℝ^{+} \to \frac{W}{2} \in ℝ$
53		renepnf	$⊢ \frac{W}{2} \in ℝ \to \frac{W}{2} \neq +∞$
54	42 52 53	3syl	$⊢ W \in ℝ^{+} \to \frac{W}{2} \neq +∞$
55	51 54	syl	$⊢ (φ \land \neg sup (B ℝ^{*} <) = +∞) \to \frac{W}{2} \neq +∞$
56		xaddass2	$⊢ ((sup (B ℝ^{} <) \in ℝ^{} \land sup (B ℝ^{} <) \neq +∞) \land (\frac{W}{2} \in ℝ^{} \land \frac{W}{2} \neq +∞) \land (\frac{W}{2} \in ℝ^{} \land \frac{W}{2} \neq +∞)) \to (sup (B ℝ^{} <) +_{𝑒} (\frac{W}{2})) +_{𝑒} (\frac{W}{2}) = sup (B ℝ^{*} <) +_{𝑒} ((\frac{W}{2}) +_{𝑒} (\frac{W}{2}))$
57	47 49 50 55 50 55 56	syl222anc	$⊢ (φ \land \neg sup (B ℝ^{} <) = +∞) \to (sup (B ℝ^{} <) +_{𝑒} (\frac{W}{2})) +_{𝑒} (\frac{W}{2}) = sup (B ℝ^{*} <) +_{𝑒} ((\frac{W}{2}) +_{𝑒} (\frac{W}{2}))$
58		rehalfcl	$⊢ W \in ℝ \to \frac{W}{2} \in ℝ$
59	58 58	rexaddd	$⊢ W \in ℝ \to (\frac{W}{2}) +_{𝑒} (\frac{W}{2}) = (\frac{W}{2}) + (\frac{W}{2})$
60		recn	$⊢ W \in ℝ \to W \in ℂ$
61		2halves	$⊢ W \in ℂ \to (\frac{W}{2}) + (\frac{W}{2}) = W$
62	60 61	syl	$⊢ W \in ℝ \to (\frac{W}{2}) + (\frac{W}{2}) = W$
63	59 62	eqtrd	$⊢ W \in ℝ \to (\frac{W}{2}) +_{𝑒} (\frac{W}{2}) = W$
64	63	oveq2d	$⊢ W \in ℝ \to sup (B ℝ^{} <) +_{𝑒} ((\frac{W}{2}) +_{𝑒} (\frac{W}{2})) = sup (B ℝ^{} <) +_{𝑒} W$
65	51 31 64	3syl	$⊢ (φ \land \neg sup (B ℝ^{} <) = +∞) \to sup (B ℝ^{} <) +_{𝑒} ((\frac{W}{2}) +_{𝑒} (\frac{W}{2})) = sup (B ℝ^{*} <) +_{𝑒} W$
66	57 65	eqtrd	$⊢ (φ \land \neg sup (B ℝ^{} <) = +∞) \to (sup (B ℝ^{} <) +_{𝑒} (\frac{W}{2})) +_{𝑒} (\frac{W}{2}) = sup (B ℝ^{*} <) +_{𝑒} W$
67	46 66	breqtrd	$⊢ (φ \land \neg sup (B ℝ^{} <) = +∞) \to X +_{𝑒} (\frac{W}{2}) \leq sup (B ℝ^{} <) +_{𝑒} W$
68	39 67	pm2.61dan	$⊢ φ \to X +_{𝑒} (\frac{W}{2}) \leq sup (B ℝ^{*} <) +_{𝑒} W$
69	12 25 17 7 68	xrletrd	$⊢ φ \to Z \leq sup (B ℝ^{*} <) +_{𝑒} W$
70	11 12 17 19 69	xrletrd	$⊢ φ \to sup (A ℝ^{} <) \leq sup (B ℝ^{} <) +_{𝑒} W$

Metamath Proof Explorer

Theorem infleinflem1

Proof