Metamath Proof Explorer

Theorem infcvgaux2i

Description: Auxiliary theorem for applications of supcvg . (Contributed by NM, 4-Mar-2008)

Ref Expression
Hypotheses infcvg.1 ⊢ R = x | ∃ y ∈ X x = − A
infcvg.2 ⊢ y ∈ X → A ∈ ℝ
infcvg.3 ⊢ Z ∈ X
infcvg.4 ⊢ ∃ z ∈ ℝ ∀ w ∈ R w ≤ z
infcvg.5a ⊢ S = − sup R ℝ <
infcvg.13 ⊢ y = C → A = B
Assertion infcvgaux2i ⊢ C ∈ X → S ≤ B

Proof

Step Hyp Ref Expression
1 infcvg.1 ⊢ R = x | ∃ y ∈ X x = − A
2 infcvg.2 ⊢ y ∈ X → A ∈ ℝ
3 infcvg.3 ⊢ Z ∈ X
4 infcvg.4 ⊢ ∃ z ∈ ℝ ∀ w ∈ R w ≤ z
5 infcvg.5a ⊢ S = − sup R ℝ <
6 infcvg.13 ⊢ y = C → A = B
7 eqid ⊢ − B = − B
8 6 negeqd ⊢ y = C → − A = − B
9 8 rspceeqv ⊢ C ∈ X ∧ − B = − B → ∃ y ∈ X − B = − A
10 7 9 mpan2 ⊢ C ∈ X → ∃ y ∈ X − B = − A
11 negex ⊢ − B ∈ V
12 eqeq1 ⊢ x = − B → x = − A ↔ − B = − A
13 12 rexbidv ⊢ x = − B → ∃ y ∈ X x = − A ↔ ∃ y ∈ X − B = − A
14 11 13 1 elab2 ⊢ − B ∈ R ↔ ∃ y ∈ X − B = − A
15 10 14 sylibr ⊢ C ∈ X → − B ∈ R
16 1 2 3 4 infcvgaux1i ⊢ R ⊆ ℝ ∧ R ≠ ∅ ∧ ∃ z ∈ ℝ ∀ w ∈ R w ≤ z
17 16 suprubii ⊢ − B ∈ R → − B ≤ sup R ℝ <
18 15 17 syl ⊢ C ∈ X → − B ≤ sup R ℝ <
19 6 eleq1d ⊢ y = C → A ∈ ℝ ↔ B ∈ ℝ
20 19 2 vtoclga ⊢ C ∈ X → B ∈ ℝ
21 16 suprclii ⊢ sup R ℝ < ∈ ℝ
22 lenegcon1 ⊢ B ∈ ℝ ∧ sup R ℝ < ∈ ℝ → − B ≤ sup R ℝ < ↔ − sup R ℝ < ≤ B
23 20 21 22 sylancl ⊢ C ∈ X → − B ≤ sup R ℝ < ↔ − sup R ℝ < ≤ B
24 18 23 mpbid ⊢ C ∈ X → − sup R ℝ < ≤ B
25 5 24 eqbrtrid ⊢ C ∈ X → S ≤ B