infcvgaux2i

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

	Ref	Expression
Hypotheses	infcvg.1	⊢ 𝑅 = { 𝑥 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = - 𝐴 }
	infcvg.2	⊢ ( 𝑦 ∈ 𝑋 → 𝐴 ∈ ℝ )
	infcvg.3	⊢ 𝑍 ∈ 𝑋
	infcvg.4	⊢ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑤 ≤ 𝑧
	infcvg.5a	⊢ 𝑆 = - sup ( 𝑅 , ℝ , < )
	infcvg.13	⊢ ( 𝑦 = 𝐶 → 𝐴 = 𝐵 )
Assertion	infcvgaux2i	⊢ ( 𝐶 ∈ 𝑋 → 𝑆 ≤ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		infcvg.1	⊢ 𝑅 = { 𝑥 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = - 𝐴 }
2		infcvg.2	⊢ ( 𝑦 ∈ 𝑋 → 𝐴 ∈ ℝ )
3		infcvg.3	⊢ 𝑍 ∈ 𝑋
4		infcvg.4	⊢ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑤 ≤ 𝑧
5		infcvg.5a	⊢ 𝑆 = - sup ( 𝑅 , ℝ , < )
6		infcvg.13	⊢ ( 𝑦 = 𝐶 → 𝐴 = 𝐵 )
7		eqid	⊢ - 𝐵 = - 𝐵
8	6	negeqd	⊢ ( 𝑦 = 𝐶 → - 𝐴 = - 𝐵 )
9	8	rspceeqv	⊢ ( ( 𝐶 ∈ 𝑋 ∧ - 𝐵 = - 𝐵 ) → ∃ 𝑦 ∈ 𝑋 - 𝐵 = - 𝐴 )
10	7 9	mpan2	⊢ ( 𝐶 ∈ 𝑋 → ∃ 𝑦 ∈ 𝑋 - 𝐵 = - 𝐴 )
11		negex	⊢ - 𝐵 ∈ V
12		eqeq1	⊢ ( 𝑥 = - 𝐵 → ( 𝑥 = - 𝐴 ↔ - 𝐵 = - 𝐴 ) )
13	12	rexbidv	⊢ ( 𝑥 = - 𝐵 → ( ∃ 𝑦 ∈ 𝑋 𝑥 = - 𝐴 ↔ ∃ 𝑦 ∈ 𝑋 - 𝐵 = - 𝐴 ) )
14	11 13 1	elab2	⊢ ( - 𝐵 ∈ 𝑅 ↔ ∃ 𝑦 ∈ 𝑋 - 𝐵 = - 𝐴 )
15	10 14	sylibr	⊢ ( 𝐶 ∈ 𝑋 → - 𝐵 ∈ 𝑅 )
16	1 2 3 4	infcvgaux1i	⊢ ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑤 ≤ 𝑧 )
17	16	suprubii	⊢ ( - 𝐵 ∈ 𝑅 → - 𝐵 ≤ sup ( 𝑅 , ℝ , < ) )
18	15 17	syl	⊢ ( 𝐶 ∈ 𝑋 → - 𝐵 ≤ sup ( 𝑅 , ℝ , < ) )
19	6	eleq1d	⊢ ( 𝑦 = 𝐶 → ( 𝐴 ∈ ℝ ↔ 𝐵 ∈ ℝ ) )
20	19 2	vtoclga	⊢ ( 𝐶 ∈ 𝑋 → 𝐵 ∈ ℝ )
21	16	suprclii	⊢ sup ( 𝑅 , ℝ , < ) ∈ ℝ
22		lenegcon1	⊢ ( ( 𝐵 ∈ ℝ ∧ sup ( 𝑅 , ℝ , < ) ∈ ℝ ) → ( - 𝐵 ≤ sup ( 𝑅 , ℝ , < ) ↔ - sup ( 𝑅 , ℝ , < ) ≤ 𝐵 ) )
23	20 21 22	sylancl	⊢ ( 𝐶 ∈ 𝑋 → ( - 𝐵 ≤ sup ( 𝑅 , ℝ , < ) ↔ - sup ( 𝑅 , ℝ , < ) ≤ 𝐵 ) )
24	18 23	mpbid	⊢ ( 𝐶 ∈ 𝑋 → - sup ( 𝑅 , ℝ , < ) ≤ 𝐵 )
25	5 24	eqbrtrid	⊢ ( 𝐶 ∈ 𝑋 → 𝑆 ≤ 𝐵 )

Metamath Proof Explorer

Theorem infcvgaux2i

Proof