This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rlimdiv

Description: Limit of the quotient of two converging functions. Proposition 12-2.1(a) of Gleason p. 168. (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Hypotheses rlimadd.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
rlimadd.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
rlimadd.5 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐷 )
rlimadd.6 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐸 )
rlimdiv.7 ⊢ ( 𝜑 → 𝐸 ≠ 0 )
rlimdiv.8 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ≠ 0 )
Assertion rlimdiv ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 / 𝐶 ) ) ⇝𝑟 ( 𝐷 / 𝐸 ) )

Proof

Step Hyp Ref Expression
1 rlimadd.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2 rlimadd.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
3 rlimadd.5 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐷 )
4 rlimadd.6 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐸 )
5 rlimdiv.7 ⊢ ( 𝜑 → 𝐸 ≠ 0 )
6 rlimdiv.8 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ≠ 0 )
7 1 3 rlimmptrcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
8 2 4 rlimmptrcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
9 8 6 reccld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 1 / 𝐶 ) ∈ ℂ )
10 eldifsn ⊢ ( 𝐶 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) )
11 8 6 10 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ( ℂ ∖ { 0 } ) )
12 11 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ ( ℂ ∖ { 0 } ) )
13 rlimcl ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐸 → 𝐸 ∈ ℂ )
14 4 13 syl ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
15 eldifsn ⊢ ( 𝐸 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝐸 ∈ ℂ ∧ 𝐸 ≠ 0 ) )
16 14 5 15 sylanbrc ⊢ ( 𝜑 → 𝐸 ∈ ( ℂ ∖ { 0 } ) )
17 eldifsn ⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) )
18 reccl ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) → ( 1 / 𝑦 ) ∈ ℂ )
19 17 18 sylbi ⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → ( 1 / 𝑦 ) ∈ ℂ )
20 19 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 1 / 𝑦 ) ∈ ℂ )
21 20 fmpttd ⊢ ( 𝜑 → ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) : ( ℂ ∖ { 0 } ) ⟶ ℂ )
22 eqid ⊢ ( if ( 1 ≤ ( ( abs ‘ 𝐸 ) · 𝑧 ) , 1 , ( ( abs ‘ 𝐸 ) · 𝑧 ) ) · ( ( abs ‘ 𝐸 ) / 2 ) ) = ( if ( 1 ≤ ( ( abs ‘ 𝐸 ) · 𝑧 ) , 1 , ( ( abs ‘ 𝐸 ) · 𝑧 ) ) · ( ( abs ‘ 𝐸 ) / 2 ) )
23 22 reccn2 ⊢ ( ( 𝐸 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑧 ∈ ℝ+ ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 → ( abs ‘ ( ( 1 / 𝑣 ) − ( 1 / 𝐸 ) ) ) < 𝑧 ) )
24 16 23 sylan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 → ( abs ‘ ( ( 1 / 𝑣 ) − ( 1 / 𝐸 ) ) ) < 𝑧 ) )
25 oveq2 ⊢ ( 𝑦 = 𝑣 → ( 1 / 𝑦 ) = ( 1 / 𝑣 ) )
26 eqid ⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) = ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) )
27 ovex ⊢ ( 1 / 𝑣 ) ∈ V
28 25 26 27 fvmpt ⊢ ( 𝑣 ∈ ( ℂ ∖ { 0 } ) → ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝑣 ) = ( 1 / 𝑣 ) )
29 oveq2 ⊢ ( 𝑦 = 𝐸 → ( 1 / 𝑦 ) = ( 1 / 𝐸 ) )
30 ovex ⊢ ( 1 / 𝐸 ) ∈ V
31 29 26 30 fvmpt ⊢ ( 𝐸 ∈ ( ℂ ∖ { 0 } ) → ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝐸 ) = ( 1 / 𝐸 ) )
32 16 31 syl ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝐸 ) = ( 1 / 𝐸 ) )
33 28 32 oveqan12rd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝑣 ) − ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝐸 ) ) = ( ( 1 / 𝑣 ) − ( 1 / 𝐸 ) ) )
34 33 fveq2d ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ℂ ∖ { 0 } ) ) → ( abs ‘ ( ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝑣 ) − ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝐸 ) ) ) = ( abs ‘ ( ( 1 / 𝑣 ) − ( 1 / 𝐸 ) ) ) )
35 34 breq1d ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ℂ ∖ { 0 } ) ) → ( ( abs ‘ ( ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝑣 ) − ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝐸 ) ) ) < 𝑧 ↔ ( abs ‘ ( ( 1 / 𝑣 ) − ( 1 / 𝐸 ) ) ) < 𝑧 ) )
36 35 imbi2d ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 → ( abs ‘ ( ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝑣 ) − ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝐸 ) ) ) < 𝑧 ) ↔ ( ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 → ( abs ‘ ( ( 1 / 𝑣 ) − ( 1 / 𝐸 ) ) ) < 𝑧 ) ) )
37 36 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑣 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 → ( abs ‘ ( ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝑣 ) − ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝐸 ) ) ) < 𝑧 ) ↔ ∀ 𝑣 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 → ( abs ‘ ( ( 1 / 𝑣 ) − ( 1 / 𝐸 ) ) ) < 𝑧 ) ) )
38 37 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 → ( abs ‘ ( ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝑣 ) − ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝐸 ) ) ) < 𝑧 ) ↔ ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 → ( abs ‘ ( ( 1 / 𝑣 ) − ( 1 / 𝐸 ) ) ) < 𝑧 ) ) )
39 38 biimpar ⊢ ( ( 𝜑 ∧ ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 → ( abs ‘ ( ( 1 / 𝑣 ) − ( 1 / 𝐸 ) ) ) < 𝑧 ) ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 → ( abs ‘ ( ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝑣 ) − ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝐸 ) ) ) < 𝑧 ) )
40 24 39 syldan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ+ ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 → ( abs ‘ ( ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝑣 ) − ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝐸 ) ) ) < 𝑧 ) )
41 12 16 4 21 40 rlimcn1 ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) ⇝𝑟 ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ‘ 𝐸 ) )
42 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
43 eqidd ⊢ ( 𝜑 → ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) = ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) )
44 oveq2 ⊢ ( 𝑦 = 𝐶 → ( 1 / 𝑦 ) = ( 1 / 𝐶 ) )
45 11 42 43 44 fmptco ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 1 / 𝐶 ) ) )
46 41 45 32 3brtr3d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 1 / 𝐶 ) ) ⇝𝑟 ( 1 / 𝐸 ) )
47 7 9 3 46 rlimmul ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · ( 1 / 𝐶 ) ) ) ⇝𝑟 ( 𝐷 · ( 1 / 𝐸 ) ) )
48 7 8 6 divrecd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 / 𝐶 ) = ( 𝐵 · ( 1 / 𝐶 ) ) )
49 48 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 / 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · ( 1 / 𝐶 ) ) ) )
50 rlimcl ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐷 → 𝐷 ∈ ℂ )
51 3 50 syl ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
52 51 14 5 divrecd ⊢ ( 𝜑 → ( 𝐷 / 𝐸 ) = ( 𝐷 · ( 1 / 𝐸 ) ) )
53 47 49 52 3brtr4d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 / 𝐶 ) ) ⇝𝑟 ( 𝐷 / 𝐸 ) )