Metamath Proof Explorer


Theorem 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 bitrdi ( ( 𝐹 ∈ ( ℂ ↑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 ‘ ( 𝐵𝐶 ) ) < 𝑥 ) ) ) )