rlim

Description: Express the predicate: The limit of complex number function F is C , or F converges to C , in the real sense. This means that for any real x , no matter how small, there always exists a number y such that the absolute difference of any number in the function beyond y and the limit is less than x . (Contributed by Mario Carneiro, 16-Sep-2014) (Revised by Mario Carneiro, 28-Apr-2015)

	Ref	Expression
Hypotheses	rlim.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
	rlim.2	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	rlim.4	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) = 𝐵 )
Assertion	rlim	⊢ ( 𝜑 → ( 𝐹 ⇝_𝑟 𝐶 ↔ ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		rlim.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
2		rlim.2	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3		rlim.4	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) = 𝐵 )
4		rlimrel	⊢ Rel ⇝_𝑟
5	4	brrelex2i	⊢ ( 𝐹 ⇝_𝑟 𝐶 → 𝐶 ∈ V )
6	5	a1i	⊢ ( 𝜑 → ( 𝐹 ⇝_𝑟 𝐶 → 𝐶 ∈ V ) )
7		elex	⊢ ( 𝐶 ∈ ℂ → 𝐶 ∈ V )
8	7	ad2antrl	⊢ ( ( 𝐹 ∈ ( ℂ ↑_pm ℝ ) ∧ ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) → 𝐶 ∈ V )
9	8	a1i	⊢ ( 𝜑 → ( ( 𝐹 ∈ ( ℂ ↑_pm ℝ ) ∧ ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) → 𝐶 ∈ V ) )
10		cnex	⊢ ℂ ∈ V
11		reex	⊢ ℝ ∈ V
12		elpm2r	⊢ ( ( ( ℂ ∈ V ∧ ℝ ∈ V ) ∧ ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ) → 𝐹 ∈ ( ℂ ↑_pm ℝ ) )
13	10 11 12	mpanl12	⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) → 𝐹 ∈ ( ℂ ↑_pm ℝ ) )
14	1 2 13	syl2anc	⊢ ( 𝜑 → 𝐹 ∈ ( ℂ ↑_pm ℝ ) )
15		eleq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ∈ ( ℂ ↑_pm ℝ ) ↔ 𝐹 ∈ ( ℂ ↑_pm ℝ ) ) )
16		eleq1	⊢ ( 𝑤 = 𝐶 → ( 𝑤 ∈ ℂ ↔ 𝐶 ∈ ℂ ) )
17	15 16	bi2anan9	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐶 ) → ( ( 𝑓 ∈ ( ℂ ↑_pm ℝ ) ∧ 𝑤 ∈ ℂ ) ↔ ( 𝐹 ∈ ( ℂ ↑_pm ℝ ) ∧ 𝐶 ∈ ℂ ) ) )
18		simpl	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐶 ) → 𝑓 = 𝐹 )
19	18	dmeqd	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐶 ) → dom 𝑓 = dom 𝐹 )
20		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
21		oveq12	⊢ ( ( ( 𝑓 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑤 = 𝐶 ) → ( ( 𝑓 ‘ 𝑧 ) − 𝑤 ) = ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) )
22	20 21	sylan	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐶 ) → ( ( 𝑓 ‘ 𝑧 ) − 𝑤 ) = ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) )
23	22	fveq2d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐶 ) → ( abs ‘ ( ( 𝑓 ‘ 𝑧 ) − 𝑤 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) )
24	23	breq1d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐶 ) → ( ( abs ‘ ( ( 𝑓 ‘ 𝑧 ) − 𝑤 ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) )
25	24	imbi2d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐶 ) → ( ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑧 ) − 𝑤 ) ) < 𝑥 ) ↔ ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) )
26	19 25	raleqbidv	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐶 ) → ( ∀ 𝑧 ∈ dom 𝑓 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑧 ) − 𝑤 ) ) < 𝑥 ) ↔ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) )
27	26	rexbidv	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐶 ) → ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝑓 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑧 ) − 𝑤 ) ) < 𝑥 ) ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) )
28	27	ralbidv	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐶 ) → ( ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝑓 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑧 ) − 𝑤 ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) )
29	17 28	anbi12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐶 ) → ( ( ( 𝑓 ∈ ( ℂ ↑_pm ℝ ) ∧ 𝑤 ∈ ℂ ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝑓 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑧 ) − 𝑤 ) ) < 𝑥 ) ) ↔ ( ( 𝐹 ∈ ( ℂ ↑_pm ℝ ) ∧ 𝐶 ∈ ℂ ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) )
30		df-rlim	⊢ ⇝_𝑟 = { ⟨ 𝑓 , 𝑤 ⟩ ∣ ( ( 𝑓 ∈ ( ℂ ↑_pm ℝ ) ∧ 𝑤 ∈ ℂ ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝑓 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑧 ) − 𝑤 ) ) < 𝑥 ) ) }
31	29 30	brabga	⊢ ( ( 𝐹 ∈ ( ℂ ↑_pm ℝ ) ∧ 𝐶 ∈ V ) → ( 𝐹 ⇝_𝑟 𝐶 ↔ ( ( 𝐹 ∈ ( ℂ ↑_pm ℝ ) ∧ 𝐶 ∈ ℂ ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) )
32		anass	⊢ ( ( ( 𝐹 ∈ ( ℂ ↑_pm ℝ ) ∧ 𝐶 ∈ ℂ ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ↔ ( 𝐹 ∈ ( ℂ ↑_pm ℝ ) ∧ ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) )
33	31 32	syl6bb	⊢ ( ( 𝐹 ∈ ( ℂ ↑_pm ℝ ) ∧ 𝐶 ∈ V ) → ( 𝐹 ⇝_𝑟 𝐶 ↔ ( 𝐹 ∈ ( ℂ ↑_pm ℝ ) ∧ ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) ) )
34	33	ex	⊢ ( 𝐹 ∈ ( ℂ ↑_pm ℝ ) → ( 𝐶 ∈ V → ( 𝐹 ⇝_𝑟 𝐶 ↔ ( 𝐹 ∈ ( ℂ ↑_pm ℝ ) ∧ ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) ) ) )
35	14 34	syl	⊢ ( 𝜑 → ( 𝐶 ∈ V → ( 𝐹 ⇝_𝑟 𝐶 ↔ ( 𝐹 ∈ ( ℂ ↑_pm ℝ ) ∧ ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) ) ) )
36	6 9 35	pm5.21ndd	⊢ ( 𝜑 → ( 𝐹 ⇝_𝑟 𝐶 ↔ ( 𝐹 ∈ ( ℂ ↑_pm ℝ ) ∧ ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) ) )
37	14	biantrurd	⊢ ( 𝜑 → ( ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ↔ ( 𝐹 ∈ ( ℂ ↑_pm ℝ ) ∧ ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) ) )
38	1	fdmd	⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
39	38	raleqdv	⊢ ( 𝜑 → ( ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) )
40	3	fvoveq1d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) = ( abs ‘ ( 𝐵 − 𝐶 ) ) )
41	40	breq1d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ↔ ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) )
42	41	imbi2d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ↔ ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
43	42	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
44	39 43	bitrd	⊢ ( 𝜑 → ( ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
45	44	rexbidv	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
46	45	ralbidv	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) )
47	46	anbi2d	⊢ ( 𝜑 → ( ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ↔ ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) ) )
48	36 37 47	3bitr2d	⊢ ( 𝜑 → ( 𝐹 ⇝_𝑟 𝐶 ↔ ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) ) )

Metamath Proof Explorer

Theorem rlim

Proof