This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 xaddrid ⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 +𝑒 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 ⊢ ( 𝜑 → ∃ 𝑏 ∈ ℝ* ∃ 𝑐 ∈ ℝ* ( 𝐴 = ( 𝑏 +𝑒 𝑐 ) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶 ) )