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

Metamath Proof Explorer

Theorem infleinflem2

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

Ref Expression
Hypotheses infleinflem2.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ* )
infleinflem2.b ⊢ ( 𝜑 → 𝐵 ⊆ ℝ* )
infleinflem2.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
infleinflem2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
infleinflem2.t ⊢ ( 𝜑 → 𝑋 < ( 𝑅 − 2 ) )
infleinflem2.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐴 )
infleinflem2.l ⊢ ( 𝜑 → 𝑍 ≤ ( 𝑋 +𝑒 1 ) )
Assertion infleinflem2 ( 𝜑 → 𝑍 < 𝑅 )

Proof

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