Metamath Proof Explorer

Theorem xrsdsreclblem

Description: Lemma for xrsdsreclb . (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypothesis xrsds.d ⊢ 𝐷 = ( dist ‘ ℝ*𝑠 )
Assertion xrsdsreclblem ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) )

Proof

Step Hyp Ref Expression
1 xrsds.d ⊢ 𝐷 = ( dist ‘ ℝ*𝑠 )
2 necom ⊢ ( 𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴 )
3 xrleltne ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 < 𝐵 ↔ 𝐵 ≠ 𝐴 ) )
4 mnfxr ⊢ -∞ ∈ ℝ*
5 4 a1i ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → -∞ ∈ ℝ* )
6 simpl1 ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → 𝐴 ∈ ℝ* )
7 simpl2 ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → 𝐵 ∈ ℝ* )
8 pnfnre ⊢ +∞ ∉ ℝ
9 8 neli ⊢ ¬ +∞ ∈ ℝ
10 mnfle ⊢ ( 𝐴 ∈ ℝ* → -∞ ≤ 𝐴 )
11 6 10 syl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → -∞ ≤ 𝐴 )
12 simpl3 ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → 𝐴 < 𝐵 )
13 5 6 7 11 12 xrlelttrd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → -∞ < 𝐵 )
14 xrltne ⊢ ( ( -∞ ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ -∞ < 𝐵 ) → 𝐵 ≠ -∞ )
15 5 7 13 14 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → 𝐵 ≠ -∞ )
16 xaddpnf1 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) → ( 𝐵 +𝑒 +∞ ) = +∞ )
17 7 15 16 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → ( 𝐵 +𝑒 +∞ ) = +∞ )
18 17 eleq1d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → ( ( 𝐵 +𝑒 +∞ ) ∈ ℝ ↔ +∞ ∈ ℝ ) )
19 9 18 mtbiri ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → ¬ ( 𝐵 +𝑒 +∞ ) ∈ ℝ )
20 ngtmnft ⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 = -∞ ↔ ¬ -∞ < 𝐴 ) )
21 6 20 syl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → ( 𝐴 = -∞ ↔ ¬ -∞ < 𝐴 ) )
22 simpr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ )
23 xnegeq ⊢ ( 𝐴 = -∞ → -𝑒 𝐴 = -𝑒 -∞ )
24 xnegmnf ⊢ -𝑒 -∞ = +∞
25 23 24 eqtrdi ⊢ ( 𝐴 = -∞ → -𝑒 𝐴 = +∞ )
26 25 oveq2d ⊢ ( 𝐴 = -∞ → ( 𝐵 +𝑒 -𝑒 𝐴 ) = ( 𝐵 +𝑒 +∞ ) )
27 26 eleq1d ⊢ ( 𝐴 = -∞ → ( ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ↔ ( 𝐵 +𝑒 +∞ ) ∈ ℝ ) )
28 22 27 syl5ibcom ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → ( 𝐴 = -∞ → ( 𝐵 +𝑒 +∞ ) ∈ ℝ ) )
29 21 28 sylbird ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → ( ¬ -∞ < 𝐴 → ( 𝐵 +𝑒 +∞ ) ∈ ℝ ) )
30 19 29 mt3d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → -∞ < 𝐴 )
31 xrre2 ⊢ ( ( ( -∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( -∞ < 𝐴 ∧ 𝐴 < 𝐵 ) ) → 𝐴 ∈ ℝ )
32 5 6 7 30 12 31 syl32anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → 𝐴 ∈ ℝ )
33 pnfxr ⊢ +∞ ∈ ℝ*
34 33 a1i ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → +∞ ∈ ℝ* )
35 6 xnegcld ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → -𝑒 𝐴 ∈ ℝ* )
36 xnegpnf ⊢ -𝑒 +∞ = -∞
37 pnfge ⊢ ( 𝐵 ∈ ℝ* → 𝐵 ≤ +∞ )
38 7 37 syl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → 𝐵 ≤ +∞ )
39 6 7 34 12 38 xrltletrd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → 𝐴 < +∞ )
40 xltnegi ⊢ ( ( 𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐴 < +∞ ) → -𝑒 +∞ < -𝑒 𝐴 )
41 6 34 39 40 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → -𝑒 +∞ < -𝑒 𝐴 )
42 36 41 eqbrtrrid ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → -∞ < -𝑒 𝐴 )
43 xrltne ⊢ ( ( -∞ ∈ ℝ* ∧ -𝑒 𝐴 ∈ ℝ* ∧ -∞ < -𝑒 𝐴 ) → -𝑒 𝐴 ≠ -∞ )
44 5 35 42 43 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → -𝑒 𝐴 ≠ -∞ )
45 xaddpnf2 ⊢ ( ( -𝑒 𝐴 ∈ ℝ* ∧ -𝑒 𝐴 ≠ -∞ ) → ( +∞ +𝑒 -𝑒 𝐴 ) = +∞ )
46 35 44 45 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → ( +∞ +𝑒 -𝑒 𝐴 ) = +∞ )
47 46 eleq1d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → ( ( +∞ +𝑒 -𝑒 𝐴 ) ∈ ℝ ↔ +∞ ∈ ℝ ) )
48 9 47 mtbiri ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → ¬ ( +∞ +𝑒 -𝑒 𝐴 ) ∈ ℝ )
49 nltpnft ⊢ ( 𝐵 ∈ ℝ* → ( 𝐵 = +∞ ↔ ¬ 𝐵 < +∞ ) )
50 7 49 syl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → ( 𝐵 = +∞ ↔ ¬ 𝐵 < +∞ ) )
51 oveq1 ⊢ ( 𝐵 = +∞ → ( 𝐵 +𝑒 -𝑒 𝐴 ) = ( +∞ +𝑒 -𝑒 𝐴 ) )
52 51 eleq1d ⊢ ( 𝐵 = +∞ → ( ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ↔ ( +∞ +𝑒 -𝑒 𝐴 ) ∈ ℝ ) )
53 22 52 syl5ibcom ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → ( 𝐵 = +∞ → ( +∞ +𝑒 -𝑒 𝐴 ) ∈ ℝ ) )
54 50 53 sylbird ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → ( ¬ 𝐵 < +∞ → ( +∞ +𝑒 -𝑒 𝐴 ) ∈ ℝ ) )
55 48 54 mt3d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → 𝐵 < +∞ )
56 xrre2 ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < +∞ ) ) → 𝐵 ∈ ℝ )
57 6 7 34 12 55 56 syl32anc ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → 𝐵 ∈ ℝ )
58 32 57 jca ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
59 58 ex ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) )
60 59 3expia ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → ( ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ) )
61 60 3adant3 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 < 𝐵 → ( ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ) )
62 3 61 sylbird ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( 𝐵 ≠ 𝐴 → ( ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ) )
63 2 62 syl5bi ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 ≠ 𝐵 → ( ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ) )
64 63 3exp ⊢ ( 𝐴 ∈ ℝ* → ( 𝐵 ∈ ℝ* → ( 𝐴 ≤ 𝐵 → ( 𝐴 ≠ 𝐵 → ( ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ) ) ) )
65 64 com34 ⊢ ( 𝐴 ∈ ℝ* → ( 𝐵 ∈ ℝ* → ( 𝐴 ≠ 𝐵 → ( 𝐴 ≤ 𝐵 → ( ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) ) ) ) )
66 65 3imp1 ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐵 +𝑒 -𝑒 𝐴 ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) )