Theorem 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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	xlt2addrd.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
	xlt2addrd.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
	xlt2addrd.4	⊢ ( 𝜑 → 𝐵 ≠ -∞ )
	xlt2addrd.5	⊢ ( 𝜑 → 𝐶 ≠ -∞ )
	xlt2addrd.6	⊢ ( 𝜑 → 𝐴 < ( 𝐵 +𝑒 𝐶 ) )
Assertion	xlt2addrd	⊢ ( 𝜑 → ∃ 𝑏 ∈ ℝ* ∃ 𝑐 ∈ ℝ* ( 𝐴 = ( 𝑏 +𝑒 𝑐 ) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶 ) )

Proof

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