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 inf (B ℝ^{*} <) +_{𝑒} (\frac{W}{2})$
	infleinflem1.z	$⊢ φ \to Z \in A$
	infleinflem1.l	$⊢ φ \to Z \leq X +_{𝑒} (\frac{W}{2})$
Assertion	infleinflem1	$⊢ φ \to inf (A ℝ^{} <) \leq inf (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 inf (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 inf (A ℝ^{} <) \in ℝ^{*}$
9	1 8	syl	$⊢ φ \to inf (A ℝ^{} <) \in ℝ^{}$
10		id	$⊢ inf (A ℝ^{} <) \in ℝ^{} \to inf (A ℝ^{} <) \in ℝ^{}$
11	9 10	syl	$⊢ φ \to inf (A ℝ^{} <) \in ℝ^{}$
12	1 6	sseldd	$⊢ φ \to Z \in ℝ^{*}$
13		infxrcl	$⊢ B \subseteq ℝ^{} \to inf (B ℝ^{} <) \in ℝ^{*}$
14	2 13	syl	$⊢ φ \to inf (B ℝ^{} <) \in ℝ^{}$
15		rpxr	$⊢ W \in ℝ^{+} \to W \in ℝ^{*}$
16	3 15	syl	$⊢ φ \to W \in ℝ^{*}$
17	14 16	xaddcld	$⊢ φ \to inf (B ℝ^{} <) +_{𝑒} W \in ℝ^{}$
18		infxrlb	$⊢ (A \subseteq ℝ^{} \land Z \in A) \to inf (A ℝ^{} <) \leq Z$
19	1 6 18	syl2anc	$⊢ φ \to inf (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 inf (B ℝ^{*} <) = +∞) \to X +_{𝑒} (\frac{W}{2}) \leq +∞$
29		oveq1	$⊢ inf (B ℝ^{} <) = +∞ \to inf (B ℝ^{} <) +_{𝑒} W = +∞ +_{𝑒} W$
30	29	adantl	$⊢ (φ \land inf (B ℝ^{} <) = +∞) \to inf (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 inf (B ℝ^{*} <) = +∞) \to +∞ +_{𝑒} W = +∞$
38	30 37	eqtr2d	$⊢ (φ \land inf (B ℝ^{} <) = +∞) \to +∞ = inf (B ℝ^{} <) +_{𝑒} W$
39	28 38	breqtrd	$⊢ (φ \land inf (B ℝ^{} <) = +∞) \to X +_{𝑒} (\frac{W}{2}) \leq inf (B ℝ^{} <) +_{𝑒} W$
40	2 4	sseldd	$⊢ φ \to X \in ℝ^{*}$
41	14 24	xaddcld	$⊢ φ \to inf (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 (inf (B ℝ^{*} <) +_{𝑒} (\frac{W}{2})) +_{𝑒} (\frac{W}{2})$
46	45	adantr	$⊢ (φ \land \neg inf (B ℝ^{} <) = +∞) \to X +_{𝑒} (\frac{W}{2}) \leq (inf (B ℝ^{} <) +_{𝑒} (\frac{W}{2})) +_{𝑒} (\frac{W}{2})$
47	14	adantr	$⊢ (φ \land \neg inf (B ℝ^{} <) = +∞) \to inf (B ℝ^{} <) \in ℝ^{*}$
48		neqne	$⊢ \neg inf (B ℝ^{} <) = +∞ \to inf (B ℝ^{} <) \neq +∞$
49	48	adantl	$⊢ (φ \land \neg inf (B ℝ^{} <) = +∞) \to inf (B ℝ^{} <) \neq +∞$
50	44	adantr	$⊢ (φ \land \neg inf (B ℝ^{} <) = +∞) \to \frac{W}{2} \in ℝ^{}$
51	3	adantr	$⊢ (φ \land \neg inf (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	51 42 52 53	4syl	$⊢ (φ \land \neg inf (B ℝ^{*} <) = +∞) \to \frac{W}{2} \neq +∞$
55		xaddass2	$⊢ ((inf (B ℝ^{} <) \in ℝ^{} \land inf (B ℝ^{} <) \neq +∞) \land (\frac{W}{2} \in ℝ^{} \land \frac{W}{2} \neq +∞) \land (\frac{W}{2} \in ℝ^{} \land \frac{W}{2} \neq +∞)) \to (inf (B ℝ^{} <) +_{𝑒} (\frac{W}{2})) +_{𝑒} (\frac{W}{2}) = inf (B ℝ^{*} <) +_{𝑒} ((\frac{W}{2}) +_{𝑒} (\frac{W}{2}))$
56	47 49 50 54 50 54 55	syl222anc	$⊢ (φ \land \neg inf (B ℝ^{} <) = +∞) \to (inf (B ℝ^{} <) +_{𝑒} (\frac{W}{2})) +_{𝑒} (\frac{W}{2}) = inf (B ℝ^{*} <) +_{𝑒} ((\frac{W}{2}) +_{𝑒} (\frac{W}{2}))$
57		rehalfcl	$⊢ W \in ℝ \to \frac{W}{2} \in ℝ$
58	57 57	rexaddd	$⊢ W \in ℝ \to (\frac{W}{2}) +_{𝑒} (\frac{W}{2}) = (\frac{W}{2}) + (\frac{W}{2})$
59		recn	$⊢ W \in ℝ \to W \in ℂ$
60		2halves	$⊢ W \in ℂ \to (\frac{W}{2}) + (\frac{W}{2}) = W$
61	59 60	syl	$⊢ W \in ℝ \to (\frac{W}{2}) + (\frac{W}{2}) = W$
62	58 61	eqtrd	$⊢ W \in ℝ \to (\frac{W}{2}) +_{𝑒} (\frac{W}{2}) = W$
63	62	oveq2d	$⊢ W \in ℝ \to inf (B ℝ^{} <) +_{𝑒} ((\frac{W}{2}) +_{𝑒} (\frac{W}{2})) = inf (B ℝ^{} <) +_{𝑒} W$
64	51 31 63	3syl	$⊢ (φ \land \neg inf (B ℝ^{} <) = +∞) \to inf (B ℝ^{} <) +_{𝑒} ((\frac{W}{2}) +_{𝑒} (\frac{W}{2})) = inf (B ℝ^{*} <) +_{𝑒} W$
65	56 64	eqtrd	$⊢ (φ \land \neg inf (B ℝ^{} <) = +∞) \to (inf (B ℝ^{} <) +_{𝑒} (\frac{W}{2})) +_{𝑒} (\frac{W}{2}) = inf (B ℝ^{*} <) +_{𝑒} W$
66	46 65	breqtrd	$⊢ (φ \land \neg inf (B ℝ^{} <) = +∞) \to X +_{𝑒} (\frac{W}{2}) \leq inf (B ℝ^{} <) +_{𝑒} W$
67	39 66	pm2.61dan	$⊢ φ \to X +_{𝑒} (\frac{W}{2}) \leq inf (B ℝ^{*} <) +_{𝑒} W$
68	12 25 17 7 67	xrletrd	$⊢ φ \to Z \leq inf (B ℝ^{*} <) +_{𝑒} W$
69	11 12 17 19 68	xrletrd	$⊢ φ \to inf (A ℝ^{} <) \leq inf (B ℝ^{} <) +_{𝑒} W$

Metamath Proof Explorer

Theorem infleinflem1

Proof