infleinflem2

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

	Ref	Expression
Hypotheses	infleinflem2.a	$⊢ φ \to A \subseteq ℝ^{*}$
	infleinflem2.b	$⊢ φ \to B \subseteq ℝ^{*}$
	infleinflem2.r	$⊢ φ \to R \in ℝ$
	infleinflem2.x	$⊢ φ \to X \in B$
	infleinflem2.t	$⊢ φ \to X < R - 2$
	infleinflem2.z	$⊢ φ \to Z \in A$
	infleinflem2.l	$⊢ φ \to Z \leq X +_{𝑒} 1$
Assertion	infleinflem2	$⊢ φ \to Z < R$

Proof

Step	Hyp	Ref	Expression
1		infleinflem2.a	$⊢ φ \to A \subseteq ℝ^{*}$
2		infleinflem2.b	$⊢ φ \to B \subseteq ℝ^{*}$
3		infleinflem2.r	$⊢ φ \to R \in ℝ$
4		infleinflem2.x	$⊢ φ \to X \in B$
5		infleinflem2.t	$⊢ φ \to X < R - 2$
6		infleinflem2.z	$⊢ φ \to Z \in A$
7		infleinflem2.l	$⊢ φ \to Z \leq X +_{𝑒} 1$
8	3	adantr	$⊢ (φ \land Z = −∞) \to R \in ℝ$
9		simpr	$⊢ (φ \land Z = −∞) \to Z = −∞$
10		simpr	$⊢ (R \in ℝ \land Z = −∞) \to Z = −∞$
11		mnflt	$⊢ R \in ℝ \to −∞ < R$
12	11	adantr	$⊢ (R \in ℝ \land Z = −∞) \to −∞ < R$
13	10 12	eqbrtrd	$⊢ (R \in ℝ \land Z = −∞) \to Z < R$
14	8 9 13	syl2anc	$⊢ (φ \land Z = −∞) \to Z < R$
15		simpl	$⊢ (φ \land \neg Z = −∞) \to φ$
16		neqne	$⊢ \neg Z = −∞ \to Z \neq −∞$
17	16	adantl	$⊢ (φ \land \neg Z = −∞) \to Z \neq −∞$
18	3	adantr	$⊢ (φ \land Z \neq −∞) \to R \in ℝ$
19		id	$⊢ φ \to φ$
20	2	sselda	$⊢ (φ \land X \in B) \to X \in ℝ^{*}$
21	19 4 20	syl2anc	$⊢ φ \to X \in ℝ^{*}$
22	21	adantr	$⊢ (φ \land Z \neq −∞) \to X \in ℝ^{*}$
23	1	sselda	$⊢ (φ \land Z \in A) \to Z \in ℝ^{*}$
24	19 6 23	syl2anc	$⊢ φ \to Z \in ℝ^{*}$
25	24	adantr	$⊢ (φ \land Z \neq −∞) \to Z \in ℝ^{*}$
26		simpr	$⊢ (φ \land Z \neq −∞) \to Z \neq −∞$
27		pnfxr	$⊢ +∞ \in ℝ^{*}$
28	27	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
29		peano2rem	$⊢ R \in ℝ \to R - 1 \in ℝ$
30	29	rexrd	$⊢ R \in ℝ \to R - 1 \in ℝ^{*}$
31	3 30	syl	$⊢ φ \to R - 1 \in ℝ^{*}$
32	2 4	sseldd	$⊢ φ \to X \in ℝ^{*}$
33		id	$⊢ X \in ℝ^{} \to X \in ℝ^{}$
34		1xr	$⊢ 1 \in ℝ^{*}$
35	34	a1i	$⊢ X \in ℝ^{} \to 1 \in ℝ^{}$
36	33 35	xaddcld	$⊢ X \in ℝ^{} \to X +_{𝑒} 1 \in ℝ^{}$
37	32 36	syl	$⊢ φ \to X +_{𝑒} 1 \in ℝ^{*}$
38		oveq1	$⊢ X = −∞ \to X +_{𝑒} 1 = −∞ +_{𝑒} 1$
39		1re	$⊢ 1 \in ℝ$
40		renepnf	$⊢ 1 \in ℝ \to 1 \neq +∞$
41	39 40	ax-mp	$⊢ 1 \neq +∞$
42		xaddmnf2	$⊢ (1 \in ℝ^{*} \land 1 \neq +∞) \to −∞ +_{𝑒} 1 = −∞$
43	34 41 42	mp2an	$⊢ −∞ +_{𝑒} 1 = −∞$
44	43	a1i	$⊢ X = −∞ \to −∞ +_{𝑒} 1 = −∞$
45	38 44	eqtrd	$⊢ X = −∞ \to X +_{𝑒} 1 = −∞$
46	45	adantl	$⊢ (R \in ℝ \land X = −∞) \to X +_{𝑒} 1 = −∞$
47	29	mnfltd	$⊢ R \in ℝ \to −∞ < R - 1$
48	47	adantr	$⊢ (R \in ℝ \land X = −∞) \to −∞ < R - 1$
49	46 48	eqbrtrd	$⊢ (R \in ℝ \land X = −∞) \to X +_{𝑒} 1 < R - 1$
50	49	adantlr	$⊢ ((R \in ℝ \land X \in ℝ^{*}) \land X = −∞) \to X +_{𝑒} 1 < R - 1$
51	50	3adantl3	$⊢ ((R \in ℝ \land X \in ℝ^{*} \land X < R - 2) \land X = −∞) \to X +_{𝑒} 1 < R - 1$
52		simpl	$⊢ ((R \in ℝ \land X \in ℝ^{} \land X < R - 2) \land \neg X = −∞) \to (R \in ℝ \land X \in ℝ^{} \land X < R - 2)$
53		simpl2	$⊢ ((R \in ℝ \land X \in ℝ^{} \land X < R - 2) \land \neg X = −∞) \to X \in ℝ^{}$
54		neqne	$⊢ \neg X = −∞ \to X \neq −∞$
55	54	adantl	$⊢ ((R \in ℝ \land X \in ℝ^{*} \land X < R - 2) \land \neg X = −∞) \to X \neq −∞$
56		simp2	$⊢ (R \in ℝ \land X \in ℝ^{} \land X < R - 2) \to X \in ℝ^{}$
57	27	a1i	$⊢ (R \in ℝ \land X \in ℝ^{} \land X < R - 2) \to +∞ \in ℝ^{}$
58		id	$⊢ R \in ℝ \to R \in ℝ$
59		2re	$⊢ 2 \in ℝ$
60	59	a1i	$⊢ R \in ℝ \to 2 \in ℝ$
61	58 60	resubcld	$⊢ R \in ℝ \to R - 2 \in ℝ$
62	61	rexrd	$⊢ R \in ℝ \to R - 2 \in ℝ^{*}$
63	62	3ad2ant1	$⊢ (R \in ℝ \land X \in ℝ^{} \land X < R - 2) \to R - 2 \in ℝ^{}$
64		simp3	$⊢ (R \in ℝ \land X \in ℝ^{*} \land X < R - 2) \to X < R - 2$
65	61	ltpnfd	$⊢ R \in ℝ \to R - 2 < +∞$
66	65	3ad2ant1	$⊢ (R \in ℝ \land X \in ℝ^{*} \land X < R - 2) \to R - 2 < +∞$
67	56 63 57 64 66	xrlttrd	$⊢ (R \in ℝ \land X \in ℝ^{*} \land X < R - 2) \to X < +∞$
68	56 57 67	xrltned	$⊢ (R \in ℝ \land X \in ℝ^{*} \land X < R - 2) \to X \neq +∞$
69	68	adantr	$⊢ ((R \in ℝ \land X \in ℝ^{*} \land X < R - 2) \land \neg X = −∞) \to X \neq +∞$
70	53 55 69	xrred	$⊢ ((R \in ℝ \land X \in ℝ^{*} \land X < R - 2) \land \neg X = −∞) \to X \in ℝ$
71		id	$⊢ X \in ℝ \to X \in ℝ$
72	71	ad2antlr	$⊢ ((R \in ℝ \land X \in ℝ) \land X < R - 2) \to X \in ℝ$
73	61	ad2antrr	$⊢ ((R \in ℝ \land X \in ℝ) \land X < R - 2) \to R - 2 \in ℝ$
74		1red	$⊢ X \in ℝ \to 1 \in ℝ$
75	72 74	syl	$⊢ ((R \in ℝ \land X \in ℝ) \land X < R - 2) \to 1 \in ℝ$
76		simpr	$⊢ ((R \in ℝ \land X \in ℝ) \land X < R - 2) \to X < R - 2$
77	72 73 75 76	ltadd1dd	$⊢ ((R \in ℝ \land X \in ℝ) \land X < R - 2) \to X + 1 < R - 2 + 1$
78		recn	$⊢ R \in ℝ \to R \in ℂ$
79		id	$⊢ R \in ℂ \to R \in ℂ$
80		2cnd	$⊢ R \in ℂ \to 2 \in ℂ$
81		1cnd	$⊢ R \in ℂ \to 1 \in ℂ$
82	79 80 81	subsubd	$⊢ R \in ℂ \to R - (2 - 1) = R - 2 + 1$
83		2m1e1	$⊢ 2 - 1 = 1$
84	83	oveq2i	$⊢ R - (2 - 1) = R - 1$
85	84	a1i	$⊢ R \in ℂ \to R - (2 - 1) = R - 1$
86	82 85	eqtr3d	$⊢ R \in ℂ \to R - 2 + 1 = R - 1$
87	78 86	syl	$⊢ R \in ℝ \to R - 2 + 1 = R - 1$
88	87	ad2antrr	$⊢ ((R \in ℝ \land X \in ℝ) \land X < R - 2) \to R - 2 + 1 = R - 1$
89	77 88	breqtrd	$⊢ ((R \in ℝ \land X \in ℝ) \land X < R - 2) \to X + 1 < R - 1$
90	71 74	rexaddd	$⊢ X \in ℝ \to X +_{𝑒} 1 = X + 1$
91	90	breq1d	$⊢ X \in ℝ \to (X +_{𝑒} 1 < R - 1 \leftrightarrow X + 1 < R - 1)$
92	91	ad2antlr	$⊢ ((R \in ℝ \land X \in ℝ) \land X < R - 2) \to (X +_{𝑒} 1 < R - 1 \leftrightarrow X + 1 < R - 1)$
93	89 92	mpbird	$⊢ ((R \in ℝ \land X \in ℝ) \land X < R - 2) \to X +_{𝑒} 1 < R - 1$
94	93	an32s	$⊢ ((R \in ℝ \land X < R - 2) \land X \in ℝ) \to X +_{𝑒} 1 < R - 1$
95	94	3adantl2	$⊢ ((R \in ℝ \land X \in ℝ^{*} \land X < R - 2) \land X \in ℝ) \to X +_{𝑒} 1 < R - 1$
96	52 70 95	syl2anc	$⊢ ((R \in ℝ \land X \in ℝ^{*} \land X < R - 2) \land \neg X = −∞) \to X +_{𝑒} 1 < R - 1$
97	51 96	pm2.61dan	$⊢ (R \in ℝ \land X \in ℝ^{*} \land X < R - 2) \to X +_{𝑒} 1 < R - 1$
98	3 32 5 97	syl3anc	$⊢ φ \to X +_{𝑒} 1 < R - 1$
99	24 37 31 7 98	xrlelttrd	$⊢ φ \to Z < R - 1$
100	29	ltpnfd	$⊢ R \in ℝ \to R - 1 < +∞$
101	3 100	syl	$⊢ φ \to R - 1 < +∞$
102	24 31 28 99 101	xrlttrd	$⊢ φ \to Z < +∞$
103	24 28 102	xrltned	$⊢ φ \to Z \neq +∞$
104	103	adantr	$⊢ (φ \land Z \neq −∞) \to Z \neq +∞$
105	25 26 104	xrred	$⊢ (φ \land Z \neq −∞) \to Z \in ℝ$
106	7	adantr	$⊢ (φ \land Z \neq −∞) \to Z \leq X +_{𝑒} 1$
107		simpl3	$⊢ ((Z \in ℝ \land X \in ℝ^{*} \land Z \leq X +_{𝑒} 1) \land X = −∞) \to Z \leq X +_{𝑒} 1$
108	45	adantl	$⊢ (Z \in ℝ \land X = −∞) \to X +_{𝑒} 1 = −∞$
109		mnflt	$⊢ Z \in ℝ \to −∞ < Z$
110	109	adantr	$⊢ (Z \in ℝ \land X = −∞) \to −∞ < Z$
111	108 110	eqbrtrd	$⊢ (Z \in ℝ \land X = −∞) \to X +_{𝑒} 1 < Z$
112		mnfxr	$⊢ −∞ \in ℝ^{*}$
113	108 112	eqeltrdi	$⊢ (Z \in ℝ \land X = −∞) \to X +_{𝑒} 1 \in ℝ^{*}$
114		rexr	$⊢ Z \in ℝ \to Z \in ℝ^{*}$
115	114	adantr	$⊢ (Z \in ℝ \land X = −∞) \to Z \in ℝ^{*}$
116	113 115	xrltnled	$⊢ (Z \in ℝ \land X = −∞) \to (X +_{𝑒} 1 < Z \leftrightarrow \neg Z \leq X +_{𝑒} 1)$
117	111 116	mpbid	$⊢ (Z \in ℝ \land X = −∞) \to \neg Z \leq X +_{𝑒} 1$
118	117	3ad2antl1	$⊢ ((Z \in ℝ \land X \in ℝ^{*} \land Z \leq X +_{𝑒} 1) \land X = −∞) \to \neg Z \leq X +_{𝑒} 1$
119	107 118	pm2.65da	$⊢ (Z \in ℝ \land X \in ℝ^{*} \land Z \leq X +_{𝑒} 1) \to \neg X = −∞$
120	119	neqned	$⊢ (Z \in ℝ \land X \in ℝ^{*} \land Z \leq X +_{𝑒} 1) \to X \neq −∞$
121	105 22 106 120	syl3anc	$⊢ (φ \land Z \neq −∞) \to X \neq −∞$
122	3 21 5 68	syl3anc	$⊢ φ \to X \neq +∞$
123	122	adantr	$⊢ (φ \land Z \neq −∞) \to X \neq +∞$
124	22 121 123	xrred	$⊢ (φ \land Z \neq −∞) \to X \in ℝ$
125	5	adantr	$⊢ (φ \land Z \neq −∞) \to X < R - 2$
126	18 124 125	jca31	$⊢ (φ \land Z \neq −∞) \to ((R \in ℝ \land X \in ℝ) \land X < R - 2)$
127		simplr	$⊢ ((((R \in ℝ \land X \in ℝ) \land X < R - 2) \land Z \in ℝ) \land Z \leq X +_{𝑒} 1) \to Z \in ℝ$
128		simp-4r	$⊢ ((((R \in ℝ \land X \in ℝ) \land X < R - 2) \land Z \in ℝ) \land Z \leq X +_{𝑒} 1) \to X \in ℝ$
129	71 74	readdcld	$⊢ X \in ℝ \to X + 1 \in ℝ$
130	90 129	eqeltrd	$⊢ X \in ℝ \to X +_{𝑒} 1 \in ℝ$
131	128 130	syl	$⊢ ((((R \in ℝ \land X \in ℝ) \land X < R - 2) \land Z \in ℝ) \land Z \leq X +_{𝑒} 1) \to X +_{𝑒} 1 \in ℝ$
132	58	ad4antr	$⊢ ((((R \in ℝ \land X \in ℝ) \land X < R - 2) \land Z \in ℝ) \land Z \leq X +_{𝑒} 1) \to R \in ℝ$
133		simpr	$⊢ ((((R \in ℝ \land X \in ℝ) \land X < R - 2) \land Z \in ℝ) \land Z \leq X +_{𝑒} 1) \to Z \leq X +_{𝑒} 1$
134	130	ad3antlr	$⊢ (((R \in ℝ \land X \in ℝ) \land X < R - 2) \land Z \in ℝ) \to X +_{𝑒} 1 \in ℝ$
135	29	ad3antrrr	$⊢ (((R \in ℝ \land X \in ℝ) \land X < R - 2) \land Z \in ℝ) \to R - 1 \in ℝ$
136	58	ad3antrrr	$⊢ (((R \in ℝ \land X \in ℝ) \land X < R - 2) \land Z \in ℝ) \to R \in ℝ$
137	93	adantr	$⊢ (((R \in ℝ \land X \in ℝ) \land X < R - 2) \land Z \in ℝ) \to X +_{𝑒} 1 < R - 1$
138	136	ltm1d	$⊢ (((R \in ℝ \land X \in ℝ) \land X < R - 2) \land Z \in ℝ) \to R - 1 < R$
139	134 135 136 137 138	lttrd	$⊢ (((R \in ℝ \land X \in ℝ) \land X < R - 2) \land Z \in ℝ) \to X +_{𝑒} 1 < R$
140	139	adantr	$⊢ ((((R \in ℝ \land X \in ℝ) \land X < R - 2) \land Z \in ℝ) \land Z \leq X +_{𝑒} 1) \to X +_{𝑒} 1 < R$
141	127 131 132 133 140	lelttrd	$⊢ ((((R \in ℝ \land X \in ℝ) \land X < R - 2) \land Z \in ℝ) \land Z \leq X +_{𝑒} 1) \to Z < R$
142	126 105 106 141	syl21anc	$⊢ (φ \land Z \neq −∞) \to Z < R$
143	15 17 142	syl2anc	$⊢ (φ \land \neg Z = −∞) \to Z < R$
144	14 143	pm2.61dan	$⊢ φ \to Z < R$

Metamath Proof Explorer

Theorem infleinflem2

Proof