xlt2addrd

Description: If the right-hand side of a 'less than' relationship is an addition, then we can express the left-hand side as an addition, too, where each term is respectively less than each term of the original right side. (Contributed by Thierry Arnoux, 15-Mar-2017)

	Ref	Expression
Hypotheses	xlt2addrd.1	$⊢ φ \to A \in ℝ$
	xlt2addrd.2	$⊢ φ \to B \in ℝ^{*}$
	xlt2addrd.3	$⊢ φ \to C \in ℝ^{*}$
	xlt2addrd.4	$⊢ φ \to B \neq −∞$
	xlt2addrd.5	$⊢ φ \to C \neq −∞$
	xlt2addrd.6	$⊢ φ \to A < B +_{𝑒} C$
Assertion	xlt2addrd	$⊢ φ \to \exists b \in ℝ^{} \exists c \in ℝ^{} (A = b +_{𝑒} c \land b < B \land c < C)$

Proof

Step	Hyp	Ref	Expression
1		xlt2addrd.1	$⊢ φ \to A \in ℝ$
2		xlt2addrd.2	$⊢ φ \to B \in ℝ^{*}$
3		xlt2addrd.3	$⊢ φ \to C \in ℝ^{*}$
4		xlt2addrd.4	$⊢ φ \to B \neq −∞$
5		xlt2addrd.5	$⊢ φ \to C \neq −∞$
6		xlt2addrd.6	$⊢ φ \to A < B +_{𝑒} C$
7	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
8	7	ad2antrr	$⊢ ((φ \land B = +∞) \land C = +∞) \to A \in ℝ^{*}$
9		0xr	$⊢ 0 \in ℝ^{*}$
10	9	a1i	$⊢ ((φ \land B = +∞) \land C = +∞) \to 0 \in ℝ^{*}$
11		xaddid1	$⊢ A \in ℝ^{*} \to A +_{𝑒} 0 = A$
12	11	eqcomd	$⊢ A \in ℝ^{*} \to A = A +_{𝑒} 0$
13	8 12	syl	$⊢ ((φ \land B = +∞) \land C = +∞) \to A = A +_{𝑒} 0$
14	1	ad2antrr	$⊢ ((φ \land B = +∞) \land C = +∞) \to A \in ℝ$
15		ltpnf	$⊢ A \in ℝ \to A < +∞$
16	14 15	syl	$⊢ ((φ \land B = +∞) \land C = +∞) \to A < +∞$
17		simplr	$⊢ ((φ \land B = +∞) \land C = +∞) \to B = +∞$
18	16 17	breqtrrd	$⊢ ((φ \land B = +∞) \land C = +∞) \to A < B$
19		0ltpnf	$⊢ 0 < +∞$
20		simpr	$⊢ ((φ \land B = +∞) \land C = +∞) \to C = +∞$
21	19 20	breqtrrid	$⊢ ((φ \land B = +∞) \land C = +∞) \to 0 < C$
22		oveq1	$⊢ b = A \to b +_{𝑒} c = A +_{𝑒} c$
23	22	eqeq2d	$⊢ b = A \to (A = b +_{𝑒} c \leftrightarrow A = A +_{𝑒} c)$
24		breq1	$⊢ b = A \to (b < B \leftrightarrow A < B)$
25	23 24	3anbi12d	$⊢ b = A \to ((A = b +_{𝑒} c \land b < B \land c < C) \leftrightarrow (A = A +_{𝑒} c \land A < B \land c < C))$
26		oveq2	$⊢ c = 0 \to A +_{𝑒} c = A +_{𝑒} 0$
27	26	eqeq2d	$⊢ c = 0 \to (A = A +_{𝑒} c \leftrightarrow A = A +_{𝑒} 0)$
28		breq1	$⊢ c = 0 \to (c < C \leftrightarrow 0 < C)$
29	27 28	3anbi13d	$⊢ c = 0 \to ((A = A +_{𝑒} c \land A < B \land c < C) \leftrightarrow (A = A +_{𝑒} 0 \land A < B \land 0 < C))$
30	25 29	rspc2ev	$⊢ (A \in ℝ^{} \land 0 \in ℝ^{} \land (A = A +_{𝑒} 0 \land A < B \land 0 < C)) \to \exists b \in ℝ^{} \exists c \in ℝ^{} (A = b +_{𝑒} c \land b < B \land c < C)$
31	8 10 13 18 21 30	syl113anc	$⊢ ((φ \land B = +∞) \land C = +∞) \to \exists b \in ℝ^{} \exists c \in ℝ^{} (A = b +_{𝑒} c \land b < B \land c < C)$
32	7	ad2antrr	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to A \in ℝ^{*}$
33	3	ad2antrr	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to C \in ℝ^{*}$
34		1xr	$⊢ 1 \in ℝ^{*}$
35	34	a1i	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to 1 \in ℝ^{*}$
36	35	xnegcld	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to - 1 \in ℝ^{*}$
37	33 36	xaddcld	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to C +_{𝑒} (- 1) \in ℝ^{*}$
38	37	xnegcld	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to - (C +_{𝑒} (- 1)) \in ℝ^{*}$
39	32 38	xaddcld	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to A +_{𝑒} (- (C +_{𝑒} (- 1))) \in ℝ^{*}$
40	1	ad2antrr	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to A \in ℝ$
41	40	renemnfd	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to A \neq −∞$
42		xrnepnf	$⊢ (C \in ℝ^{*} \land C \neq +∞) \leftrightarrow (C \in ℝ \lor C = −∞)$
43	42	biimpi	$⊢ (C \in ℝ^{*} \land C \neq +∞) \to (C \in ℝ \lor C = −∞)$
44	33 43	sylancom	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to (C \in ℝ \lor C = −∞)$
45	44	orcomd	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to (C = −∞ \lor C \in ℝ)$
46	5	ad2antrr	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to C \neq −∞$
47	46	neneqd	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to \neg C = −∞$
48		pm2.53	$⊢ (C = −∞ \lor C \in ℝ) \to (\neg C = −∞ \to C \in ℝ)$
49	45 47 48	sylc	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to C \in ℝ$
50		1re	$⊢ 1 \in ℝ$
51		rexsub	$⊢ (C \in ℝ \land 1 \in ℝ) \to C +_{𝑒} (- 1) = C - 1$
52	49 50 51	sylancl	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to C +_{𝑒} (- 1) = C - 1$
53		resubcl	$⊢ (C \in ℝ \land 1 \in ℝ) \to C - 1 \in ℝ$
54	49 50 53	sylancl	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to C - 1 \in ℝ$
55	52 54	eqeltrd	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to C +_{𝑒} (- 1) \in ℝ$
56		rexneg	$⊢ C +_{𝑒} (- 1) \in ℝ \to - (C +_{𝑒} (- 1)) = - (C +_{𝑒} (- 1))$
57	55 56	syl	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to - (C +_{𝑒} (- 1)) = - (C +_{𝑒} (- 1))$
58	55	renegcld	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to - (C +_{𝑒} (- 1)) \in ℝ$
59	57 58	eqeltrd	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to - (C +_{𝑒} (- 1)) \in ℝ$
60	59	renemnfd	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to - (C +_{𝑒} (- 1)) \neq −∞$
61	55	renemnfd	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to C +_{𝑒} (- 1) \neq −∞$
62		xaddass	$⊢ ((A \in ℝ^{} \land A \neq −∞) \land (- (C +_{𝑒} (- 1)) \in ℝ^{} \land - (C +_{𝑒} (- 1)) \neq −∞) \land (C +_{𝑒} (- 1) \in ℝ^{*} \land C +_{𝑒} (- 1) \neq −∞)) \to (A +_{𝑒} (- (C +_{𝑒} (- 1)))) +_{𝑒} (C +_{𝑒} (- 1)) = A +_{𝑒} ((- (C +_{𝑒} (- 1))) +_{𝑒} (C +_{𝑒} (- 1)))$
63	32 41 38 60 37 61 62	syl222anc	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to (A +_{𝑒} (- (C +_{𝑒} (- 1)))) +_{𝑒} (C +_{𝑒} (- 1)) = A +_{𝑒} ((- (C +_{𝑒} (- 1))) +_{𝑒} (C +_{𝑒} (- 1)))$
64		xaddcom	$⊢ (- (C +_{𝑒} (- 1)) \in ℝ^{} \land C +_{𝑒} (- 1) \in ℝ^{}) \to (- (C +_{𝑒} (- 1))) +_{𝑒} (C +_{𝑒} (- 1)) = (C +_{𝑒} (- 1)) +_{𝑒} (- (C +_{𝑒} (- 1)))$
65	38 37 64	syl2anc	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to (- (C +_{𝑒} (- 1))) +_{𝑒} (C +_{𝑒} (- 1)) = (C +_{𝑒} (- 1)) +_{𝑒} (- (C +_{𝑒} (- 1)))$
66		xnegid	$⊢ C +_{𝑒} (- 1) \in ℝ^{*} \to (C +_{𝑒} (- 1)) +_{𝑒} (- (C +_{𝑒} (- 1))) = 0$
67	37 66	syl	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to (C +_{𝑒} (- 1)) +_{𝑒} (- (C +_{𝑒} (- 1))) = 0$
68	65 67	eqtrd	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to (- (C +_{𝑒} (- 1))) +_{𝑒} (C +_{𝑒} (- 1)) = 0$
69	68	oveq2d	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to A +_{𝑒} ((- (C +_{𝑒} (- 1))) +_{𝑒} (C +_{𝑒} (- 1))) = A +_{𝑒} 0$
70	32 11	syl	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to A +_{𝑒} 0 = A$
71	63 69 70	3eqtrrd	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to A = (A +_{𝑒} (- (C +_{𝑒} (- 1)))) +_{𝑒} (C +_{𝑒} (- 1))$
72	40 54	resubcld	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to A - (C - 1) \in ℝ$
73		ltpnf	$⊢ A - (C - 1) \in ℝ \to A - (C - 1) < +∞$
74	72 73	syl	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to A - (C - 1) < +∞$
75		rexsub	$⊢ (A \in ℝ \land C +_{𝑒} (- 1) \in ℝ) \to A +_{𝑒} (- (C +_{𝑒} (- 1))) = A - (C +_{𝑒} (- 1))$
76	40 55 75	syl2anc	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to A +_{𝑒} (- (C +_{𝑒} (- 1))) = A - (C +_{𝑒} (- 1))$
77	52	oveq2d	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to A - (C +_{𝑒} (- 1)) = A - (C - 1)$
78	76 77	eqtrd	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to A +_{𝑒} (- (C +_{𝑒} (- 1))) = A - (C - 1)$
79		simplr	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to B = +∞$
80	74 78 79	3brtr4d	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to A +_{𝑒} (- (C +_{𝑒} (- 1))) < B$
81	49	ltm1d	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to C - 1 < C$
82	52 81	eqbrtrd	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to C +_{𝑒} (- 1) < C$
83		oveq1	$⊢ b = A +_{𝑒} (- (C +_{𝑒} (- 1))) \to b +_{𝑒} c = (A +_{𝑒} (- (C +_{𝑒} (- 1)))) +_{𝑒} c$
84	83	eqeq2d	$⊢ b = A +_{𝑒} (- (C +_{𝑒} (- 1))) \to (A = b +_{𝑒} c \leftrightarrow A = (A +_{𝑒} (- (C +_{𝑒} (- 1)))) +_{𝑒} c)$
85		breq1	$⊢ b = A +_{𝑒} (- (C +_{𝑒} (- 1))) \to (b < B \leftrightarrow A +_{𝑒} (- (C +_{𝑒} (- 1))) < B)$
86	84 85	3anbi12d	$⊢ b = A +_{𝑒} (- (C +_{𝑒} (- 1))) \to ((A = b +_{𝑒} c \land b < B \land c < C) \leftrightarrow (A = (A +_{𝑒} (- (C +_{𝑒} (- 1)))) +_{𝑒} c \land A +_{𝑒} (- (C +_{𝑒} (- 1))) < B \land c < C))$
87		oveq2	$⊢ c = C +_{𝑒} (- 1) \to (A +_{𝑒} (- (C +_{𝑒} (- 1)))) +_{𝑒} c = (A +_{𝑒} (- (C +_{𝑒} (- 1)))) +_{𝑒} (C +_{𝑒} (- 1))$
88	87	eqeq2d	$⊢ c = C +_{𝑒} (- 1) \to (A = (A +_{𝑒} (- (C +_{𝑒} (- 1)))) +_{𝑒} c \leftrightarrow A = (A +_{𝑒} (- (C +_{𝑒} (- 1)))) +_{𝑒} (C +_{𝑒} (- 1)))$
89		breq1	$⊢ c = C +_{𝑒} (- 1) \to (c < C \leftrightarrow C +_{𝑒} (- 1) < C)$
90	88 89	3anbi13d	$⊢ c = C +_{𝑒} (- 1) \to ((A = (A +_{𝑒} (- (C +_{𝑒} (- 1)))) +_{𝑒} c \land A +_{𝑒} (- (C +_{𝑒} (- 1))) < B \land c < C) \leftrightarrow (A = (A +_{𝑒} (- (C +_{𝑒} (- 1)))) +_{𝑒} (C +_{𝑒} (- 1)) \land A +_{𝑒} (- (C +_{𝑒} (- 1))) < B \land C +_{𝑒} (- 1) < C))$
91	86 90	rspc2ev	$⊢ (A +_{𝑒} (- (C +_{𝑒} (- 1))) \in ℝ^{} \land C +_{𝑒} (- 1) \in ℝ^{} \land (A = (A +_{𝑒} (- (C +_{𝑒} (- 1)))) +_{𝑒} (C +_{𝑒} (- 1)) \land A +_{𝑒} (- (C +_{𝑒} (- 1))) < B \land C +_{𝑒} (- 1) < C)) \to \exists b \in ℝ^{} \exists c \in ℝ^{} (A = b +_{𝑒} c \land b < B \land c < C)$
92	39 37 71 80 82 91	syl113anc	$⊢ ((φ \land B = +∞) \land C \neq +∞) \to \exists b \in ℝ^{} \exists c \in ℝ^{} (A = b +_{𝑒} c \land b < B \land c < C)$
93	31 92	pm2.61dane	$⊢ (φ \land B = +∞) \to \exists b \in ℝ^{} \exists c \in ℝ^{} (A = b +_{𝑒} c \land b < B \land c < C)$
94	2	ad2antrr	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to B \in ℝ^{*}$
95	34	a1i	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to 1 \in ℝ^{*}$
96	95	xnegcld	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to - 1 \in ℝ^{*}$
97	94 96	xaddcld	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to B +_{𝑒} (- 1) \in ℝ^{*}$
98	7	ad2antrr	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to A \in ℝ^{*}$
99	97	xnegcld	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to - (B +_{𝑒} (- 1)) \in ℝ^{*}$
100	98 99	xaddcld	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to A +_{𝑒} (- (B +_{𝑒} (- 1))) \in ℝ^{*}$
101		xaddcom	$⊢ (B +_{𝑒} (- 1) \in ℝ^{} \land A +_{𝑒} (- (B +_{𝑒} (- 1))) \in ℝ^{}) \to (B +_{𝑒} (- 1)) +_{𝑒} (A +_{𝑒} (- (B +_{𝑒} (- 1)))) = (A +_{𝑒} (- (B +_{𝑒} (- 1)))) +_{𝑒} (B +_{𝑒} (- 1))$
102	97 100 101	syl2anc	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to (B +_{𝑒} (- 1)) +_{𝑒} (A +_{𝑒} (- (B +_{𝑒} (- 1)))) = (A +_{𝑒} (- (B +_{𝑒} (- 1)))) +_{𝑒} (B +_{𝑒} (- 1))$
103	1	ad2antrr	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to A \in ℝ$
104	103	renemnfd	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to A \neq −∞$
105		simplr	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to B \neq +∞$
106		xrnepnf	$⊢ (B \in ℝ^{*} \land B \neq +∞) \leftrightarrow (B \in ℝ \lor B = −∞)$
107	106	biimpi	$⊢ (B \in ℝ^{*} \land B \neq +∞) \to (B \in ℝ \lor B = −∞)$
108	94 105 107	syl2anc	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to (B \in ℝ \lor B = −∞)$
109	108	orcomd	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to (B = −∞ \lor B \in ℝ)$
110	4	ad2antrr	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to B \neq −∞$
111	110	neneqd	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to \neg B = −∞$
112		pm2.53	$⊢ (B = −∞ \lor B \in ℝ) \to (\neg B = −∞ \to B \in ℝ)$
113	109 111 112	sylc	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to B \in ℝ$
114		rexsub	$⊢ (B \in ℝ \land 1 \in ℝ) \to B +_{𝑒} (- 1) = B - 1$
115	113 50 114	sylancl	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to B +_{𝑒} (- 1) = B - 1$
116		resubcl	$⊢ (B \in ℝ \land 1 \in ℝ) \to B - 1 \in ℝ$
117	113 50 116	sylancl	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to B - 1 \in ℝ$
118	115 117	eqeltrd	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to B +_{𝑒} (- 1) \in ℝ$
119		rexneg	$⊢ B +_{𝑒} (- 1) \in ℝ \to - (B +_{𝑒} (- 1)) = - (B +_{𝑒} (- 1))$
120	118 119	syl	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to - (B +_{𝑒} (- 1)) = - (B +_{𝑒} (- 1))$
121	118	renegcld	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to - (B +_{𝑒} (- 1)) \in ℝ$
122	120 121	eqeltrd	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to - (B +_{𝑒} (- 1)) \in ℝ$
123	122	renemnfd	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to - (B +_{𝑒} (- 1)) \neq −∞$
124	118	renemnfd	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to B +_{𝑒} (- 1) \neq −∞$
125		xaddass	$⊢ ((A \in ℝ^{} \land A \neq −∞) \land (- (B +_{𝑒} (- 1)) \in ℝ^{} \land - (B +_{𝑒} (- 1)) \neq −∞) \land (B +_{𝑒} (- 1) \in ℝ^{*} \land B +_{𝑒} (- 1) \neq −∞)) \to (A +_{𝑒} (- (B +_{𝑒} (- 1)))) +_{𝑒} (B +_{𝑒} (- 1)) = A +_{𝑒} ((- (B +_{𝑒} (- 1))) +_{𝑒} (B +_{𝑒} (- 1)))$
126	98 104 99 123 97 124 125	syl222anc	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to (A +_{𝑒} (- (B +_{𝑒} (- 1)))) +_{𝑒} (B +_{𝑒} (- 1)) = A +_{𝑒} ((- (B +_{𝑒} (- 1))) +_{𝑒} (B +_{𝑒} (- 1)))$
127		xaddcom	$⊢ (- (B +_{𝑒} (- 1)) \in ℝ^{} \land B +_{𝑒} (- 1) \in ℝ^{}) \to (- (B +_{𝑒} (- 1))) +_{𝑒} (B +_{𝑒} (- 1)) = (B +_{𝑒} (- 1)) +_{𝑒} (- (B +_{𝑒} (- 1)))$
128	99 97 127	syl2anc	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to (- (B +_{𝑒} (- 1))) +_{𝑒} (B +_{𝑒} (- 1)) = (B +_{𝑒} (- 1)) +_{𝑒} (- (B +_{𝑒} (- 1)))$
129		xnegid	$⊢ B +_{𝑒} (- 1) \in ℝ^{*} \to (B +_{𝑒} (- 1)) +_{𝑒} (- (B +_{𝑒} (- 1))) = 0$
130	97 129	syl	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to (B +_{𝑒} (- 1)) +_{𝑒} (- (B +_{𝑒} (- 1))) = 0$
131	128 130	eqtrd	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to (- (B +_{𝑒} (- 1))) +_{𝑒} (B +_{𝑒} (- 1)) = 0$
132	131	oveq2d	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to A +_{𝑒} ((- (B +_{𝑒} (- 1))) +_{𝑒} (B +_{𝑒} (- 1))) = A +_{𝑒} 0$
133	98 11	syl	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to A +_{𝑒} 0 = A$
134	132 133	eqtrd	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to A +_{𝑒} ((- (B +_{𝑒} (- 1))) +_{𝑒} (B +_{𝑒} (- 1))) = A$
135	102 126 134	3eqtrrd	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to A = (B +_{𝑒} (- 1)) +_{𝑒} (A +_{𝑒} (- (B +_{𝑒} (- 1))))$
136	113	ltm1d	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to B - 1 < B$
137	115 136	eqbrtrd	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to B +_{𝑒} (- 1) < B$
138	103 117	resubcld	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to A - (B - 1) \in ℝ$
139		ltpnf	$⊢ A - (B - 1) \in ℝ \to A - (B - 1) < +∞$
140	138 139	syl	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to A - (B - 1) < +∞$
141		rexsub	$⊢ (A \in ℝ \land B +_{𝑒} (- 1) \in ℝ) \to A +_{𝑒} (- (B +_{𝑒} (- 1))) = A - (B +_{𝑒} (- 1))$
142	103 118 141	syl2anc	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to A +_{𝑒} (- (B +_{𝑒} (- 1))) = A - (B +_{𝑒} (- 1))$
143	115	oveq2d	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to A - (B +_{𝑒} (- 1)) = A - (B - 1)$
144	142 143	eqtrd	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to A +_{𝑒} (- (B +_{𝑒} (- 1))) = A - (B - 1)$
145		simpr	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to C = +∞$
146	140 144 145	3brtr4d	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to A +_{𝑒} (- (B +_{𝑒} (- 1))) < C$
147		oveq1	$⊢ b = B +_{𝑒} (- 1) \to b +_{𝑒} c = (B +_{𝑒} (- 1)) +_{𝑒} c$
148	147	eqeq2d	$⊢ b = B +_{𝑒} (- 1) \to (A = b +_{𝑒} c \leftrightarrow A = (B +_{𝑒} (- 1)) +_{𝑒} c)$
149		breq1	$⊢ b = B +_{𝑒} (- 1) \to (b < B \leftrightarrow B +_{𝑒} (- 1) < B)$
150	148 149	3anbi12d	$⊢ b = B +_{𝑒} (- 1) \to ((A = b +_{𝑒} c \land b < B \land c < C) \leftrightarrow (A = (B +_{𝑒} (- 1)) +_{𝑒} c \land B +_{𝑒} (- 1) < B \land c < C))$
151		oveq2	$⊢ c = A +_{𝑒} (- (B +_{𝑒} (- 1))) \to (B +_{𝑒} (- 1)) +_{𝑒} c = (B +_{𝑒} (- 1)) +_{𝑒} (A +_{𝑒} (- (B +_{𝑒} (- 1))))$
152	151	eqeq2d	$⊢ c = A +_{𝑒} (- (B +_{𝑒} (- 1))) \to (A = (B +_{𝑒} (- 1)) +_{𝑒} c \leftrightarrow A = (B +_{𝑒} (- 1)) +_{𝑒} (A +_{𝑒} (- (B +_{𝑒} (- 1)))))$
153		breq1	$⊢ c = A +_{𝑒} (- (B +_{𝑒} (- 1))) \to (c < C \leftrightarrow A +_{𝑒} (- (B +_{𝑒} (- 1))) < C)$
154	152 153	3anbi13d	$⊢ c = A +_{𝑒} (- (B +_{𝑒} (- 1))) \to ((A = (B +_{𝑒} (- 1)) +_{𝑒} c \land B +_{𝑒} (- 1) < B \land c < C) \leftrightarrow (A = (B +_{𝑒} (- 1)) +_{𝑒} (A +_{𝑒} (- (B +_{𝑒} (- 1)))) \land B +_{𝑒} (- 1) < B \land A +_{𝑒} (- (B +_{𝑒} (- 1))) < C))$
155	150 154	rspc2ev	$⊢ (B +_{𝑒} (- 1) \in ℝ^{} \land A +_{𝑒} (- (B +_{𝑒} (- 1))) \in ℝ^{} \land (A = (B +_{𝑒} (- 1)) +_{𝑒} (A +_{𝑒} (- (B +_{𝑒} (- 1)))) \land B +_{𝑒} (- 1) < B \land A +_{𝑒} (- (B +_{𝑒} (- 1))) < C)) \to \exists b \in ℝ^{} \exists c \in ℝ^{} (A = b +_{𝑒} c \land b < B \land c < C)$
156	97 100 135 137 146 155	syl113anc	$⊢ ((φ \land B \neq +∞) \land C = +∞) \to \exists b \in ℝ^{} \exists c \in ℝ^{} (A = b +_{𝑒} c \land b < B \land c < C)$
157	1	ad2antrr	$⊢ ((φ \land B \neq +∞) \land C \neq +∞) \to A \in ℝ$
158	2	ad2antrr	$⊢ ((φ \land B \neq +∞) \land C \neq +∞) \to B \in ℝ^{*}$
159		simplr	$⊢ ((φ \land B \neq +∞) \land C \neq +∞) \to B \neq +∞$
160	158 159 107	syl2anc	$⊢ ((φ \land B \neq +∞) \land C \neq +∞) \to (B \in ℝ \lor B = −∞)$
161	160	orcomd	$⊢ ((φ \land B \neq +∞) \land C \neq +∞) \to (B = −∞ \lor B \in ℝ)$
162	4	ad2antrr	$⊢ ((φ \land B \neq +∞) \land C \neq +∞) \to B \neq −∞$
163	162	neneqd	$⊢ ((φ \land B \neq +∞) \land C \neq +∞) \to \neg B = −∞$
164	161 163 112	sylc	$⊢ ((φ \land B \neq +∞) \land C \neq +∞) \to B \in ℝ$
165	3	ad2antrr	$⊢ ((φ \land B \neq +∞) \land C \neq +∞) \to C \in ℝ^{*}$
166	165 43	sylancom	$⊢ ((φ \land B \neq +∞) \land C \neq +∞) \to (C \in ℝ \lor C = −∞)$
167	166	orcomd	$⊢ ((φ \land B \neq +∞) \land C \neq +∞) \to (C = −∞ \lor C \in ℝ)$
168	5	ad2antrr	$⊢ ((φ \land B \neq +∞) \land C \neq +∞) \to C \neq −∞$
169	168	neneqd	$⊢ ((φ \land B \neq +∞) \land C \neq +∞) \to \neg C = −∞$
170	167 169 48	sylc	$⊢ ((φ \land B \neq +∞) \land C \neq +∞) \to C \in ℝ$
171	6	ad2antrr	$⊢ ((φ \land B \neq +∞) \land C \neq +∞) \to A < B +_{𝑒} C$
172		rexadd	$⊢ (B \in ℝ \land C \in ℝ) \to B +_{𝑒} C = B + C$
173	164 170 172	syl2anc	$⊢ ((φ \land B \neq +∞) \land C \neq +∞) \to B +_{𝑒} C = B + C$
174	171 173	breqtrd	$⊢ ((φ \land B \neq +∞) \land C \neq +∞) \to A < B + C$
175	157 164 170 174	lt2addrd	$⊢ ((φ \land B \neq +∞) \land C \neq +∞) \to \exists b \in ℝ \exists c \in ℝ (A = b + c \land b < B \land c < C)$
176		rexadd	$⊢ (b \in ℝ \land c \in ℝ) \to b +_{𝑒} c = b + c$
177	176	eqeq2d	$⊢ (b \in ℝ \land c \in ℝ) \to (A = b +_{𝑒} c \leftrightarrow A = b + c)$
178	177	3anbi1d	$⊢ (b \in ℝ \land c \in ℝ) \to ((A = b +_{𝑒} c \land b < B \land c < C) \leftrightarrow (A = b + c \land b < B \land c < C))$
179	178	2rexbiia	$⊢ \exists b \in ℝ \exists c \in ℝ (A = b +_{𝑒} c \land b < B \land c < C) \leftrightarrow \exists b \in ℝ \exists c \in ℝ (A = b + c \land b < B \land c < C)$
180	175 179	sylibr	$⊢ ((φ \land B \neq +∞) \land C \neq +∞) \to \exists b \in ℝ \exists c \in ℝ (A = b +_{𝑒} c \land b < B \land c < C)$
181		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
182		ssrexv	$⊢ ℝ \subseteq ℝ^{} \to (\exists c \in ℝ (A = b +_{𝑒} c \land b < B \land c < C) \to \exists c \in ℝ^{} (A = b +_{𝑒} c \land b < B \land c < C))$
183	181 182	ax-mp	$⊢ \exists c \in ℝ (A = b +_{𝑒} c \land b < B \land c < C) \to \exists c \in ℝ^{*} (A = b +_{𝑒} c \land b < B \land c < C)$
184	183	reximi	$⊢ \exists b \in ℝ \exists c \in ℝ (A = b +_{𝑒} c \land b < B \land c < C) \to \exists b \in ℝ \exists c \in ℝ^{*} (A = b +_{𝑒} c \land b < B \land c < C)$
185		ssrexv	$⊢ ℝ \subseteq ℝ^{} \to (\exists b \in ℝ \exists c \in ℝ^{} (A = b +_{𝑒} c \land b < B \land c < C) \to \exists b \in ℝ^{} \exists c \in ℝ^{} (A = b +_{𝑒} c \land b < B \land c < C))$
186	181 185	ax-mp	$⊢ \exists b \in ℝ \exists c \in ℝ^{} (A = b +_{𝑒} c \land b < B \land c < C) \to \exists b \in ℝ^{} \exists c \in ℝ^{*} (A = b +_{𝑒} c \land b < B \land c < C)$
187	180 184 186	3syl	$⊢ ((φ \land B \neq +∞) \land C \neq +∞) \to \exists b \in ℝ^{} \exists c \in ℝ^{} (A = b +_{𝑒} c \land b < B \land c < C)$
188	156 187	pm2.61dane	$⊢ (φ \land B \neq +∞) \to \exists b \in ℝ^{} \exists c \in ℝ^{} (A = b +_{𝑒} c \land b < B \land c < C)$
189	93 188	pm2.61dane	$⊢ φ \to \exists b \in ℝ^{} \exists c \in ℝ^{} (A = b +_{𝑒} c \land b < B \land c < C)$

Metamath Proof Explorer

Theorem xlt2addrd

Proof