Metamath Proof Explorer

Theorem rlimsqzlem

Description: Lemma for rlimsqz and rlimsqz2 . (Contributed by Mario Carneiro, 18-Sep-2014) (Revised by Mario Carneiro, 20-May-2016)

Ref Expression
Hypotheses rlimsqzlem.m ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
rlimsqzlem.e ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
rlimsqzlem.1 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐷 )
rlimsqzlem.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
rlimsqzlem.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
rlimsqzlem.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥 ) ) → ( abs ‘ ( 𝐶 − 𝐸 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐷 ) ) )
Assertion rlimsqzlem ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐸 )

Proof

Step Hyp Ref Expression
1 rlimsqzlem.m ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
2 rlimsqzlem.e ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
3 rlimsqzlem.1 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐷 )
4 rlimsqzlem.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
5 rlimsqzlem.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
6 rlimsqzlem.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥 ) ) → ( abs ‘ ( 𝐶 − 𝐸 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐷 ) ) )
7 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ ( 𝑀 [,) +∞ ) ∧ 𝑧 ≤ 𝑥 ) ) → 𝑀 ∈ ℝ )
8 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑀 ∈ ℝ )
9 elicopnf ⊢ ( 𝑀 ∈ ℝ → ( 𝑧 ∈ ( 𝑀 [,) +∞ ) ↔ ( 𝑧 ∈ ℝ ∧ 𝑀 ≤ 𝑧 ) ) )
10 8 9 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑧 ∈ ( 𝑀 [,) +∞ ) ↔ ( 𝑧 ∈ ℝ ∧ 𝑀 ≤ 𝑧 ) ) )
11 10 simprbda ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( 𝑀 [,) +∞ ) ) → 𝑧 ∈ ℝ )
12 11 adantrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ ( 𝑀 [,) +∞ ) ∧ 𝑧 ≤ 𝑥 ) ) → 𝑧 ∈ ℝ )
13 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
14 13 4 dmmptd ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
15 rlimss ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐷 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
16 3 15 syl ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
17 14 16 eqsstrrd ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
18 17 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝐴 ⊆ ℝ )
19 18 sselda ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
20 19 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ ( 𝑀 [,) +∞ ) ∧ 𝑧 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ )
21 10 simplbda ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( 𝑀 [,) +∞ ) ) → 𝑀 ≤ 𝑧 )
22 21 adantrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ ( 𝑀 [,) +∞ ) ∧ 𝑧 ≤ 𝑥 ) ) → 𝑀 ≤ 𝑧 )
23 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ ( 𝑀 [,) +∞ ) ∧ 𝑧 ≤ 𝑥 ) ) → 𝑧 ≤ 𝑥 )
24 7 12 20 22 23 letrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ ( 𝑀 [,) +∞ ) ∧ 𝑧 ≤ 𝑥 ) ) → 𝑀 ≤ 𝑥 )
25 6 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑀 ≤ 𝑥 ) → ( abs ‘ ( 𝐶 − 𝐸 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐷 ) ) )
26 25 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑀 ≤ 𝑥 ) → ( abs ‘ ( 𝐶 − 𝐸 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐷 ) ) )
27 24 26 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ ( 𝑀 [,) +∞ ) ∧ 𝑧 ≤ 𝑥 ) ) → ( abs ‘ ( 𝐶 − 𝐸 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐷 ) ) )
28 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐸 ∈ ℂ )
29 5 28 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 − 𝐸 ) ∈ ℂ )
30 29 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( 𝐶 − 𝐸 ) ) ∈ ℝ )
31 30 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ ( 𝑀 [,) +∞ ) ∧ 𝑧 ≤ 𝑥 ) ) → ( abs ‘ ( 𝐶 − 𝐸 ) ) ∈ ℝ )
32 rlimcl ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐷 → 𝐷 ∈ ℂ )
33 3 32 syl ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐷 ∈ ℂ )
35 4 34 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 − 𝐷 ) ∈ ℂ )
36 35 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( 𝐵 − 𝐷 ) ) ∈ ℝ )
37 36 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ ( 𝑀 [,) +∞ ) ∧ 𝑧 ≤ 𝑥 ) ) → ( abs ‘ ( 𝐵 − 𝐷 ) ) ∈ ℝ )
38 rpre ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ )
39 38 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ ( 𝑀 [,) +∞ ) ∧ 𝑧 ≤ 𝑥 ) ) → 𝑦 ∈ ℝ )
40 lelttr ⊢ ( ( ( abs ‘ ( 𝐶 − 𝐸 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝐵 − 𝐷 ) ) ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( abs ‘ ( 𝐶 − 𝐸 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐷 ) ) ∧ ( abs ‘ ( 𝐵 − 𝐷 ) ) < 𝑦 ) → ( abs ‘ ( 𝐶 − 𝐸 ) ) < 𝑦 ) )
41 31 37 39 40 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ ( 𝑀 [,) +∞ ) ∧ 𝑧 ≤ 𝑥 ) ) → ( ( ( abs ‘ ( 𝐶 − 𝐸 ) ) ≤ ( abs ‘ ( 𝐵 − 𝐷 ) ) ∧ ( abs ‘ ( 𝐵 − 𝐷 ) ) < 𝑦 ) → ( abs ‘ ( 𝐶 − 𝐸 ) ) < 𝑦 ) )
42 27 41 mpand ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑧 ∈ ( 𝑀 [,) +∞ ) ∧ 𝑧 ≤ 𝑥 ) ) → ( ( abs ‘ ( 𝐵 − 𝐷 ) ) < 𝑦 → ( abs ‘ ( 𝐶 − 𝐸 ) ) < 𝑦 ) )
43 42 expr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( 𝑀 [,) +∞ ) ) → ( 𝑧 ≤ 𝑥 → ( ( abs ‘ ( 𝐵 − 𝐷 ) ) < 𝑦 → ( abs ‘ ( 𝐶 − 𝐸 ) ) < 𝑦 ) ) )
44 43 an32s ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑧 ≤ 𝑥 → ( ( abs ‘ ( 𝐵 − 𝐷 ) ) < 𝑦 → ( abs ‘ ( 𝐶 − 𝐸 ) ) < 𝑦 ) ) )
45 44 a2d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑧 ≤ 𝑥 → ( abs ‘ ( 𝐵 − 𝐷 ) ) < 𝑦 ) → ( 𝑧 ≤ 𝑥 → ( abs ‘ ( 𝐶 − 𝐸 ) ) < 𝑦 ) ) )
46 45 ralimdva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ( 𝑀 [,) +∞ ) ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝑧 ≤ 𝑥 → ( abs ‘ ( 𝐵 − 𝐷 ) ) < 𝑦 ) → ∀ 𝑥 ∈ 𝐴 ( 𝑧 ≤ 𝑥 → ( abs ‘ ( 𝐶 − 𝐸 ) ) < 𝑦 ) ) )
47 46 reximdva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑧 ∈ ( 𝑀 [,) +∞ ) ∀ 𝑥 ∈ 𝐴 ( 𝑧 ≤ 𝑥 → ( abs ‘ ( 𝐵 − 𝐷 ) ) < 𝑦 ) → ∃ 𝑧 ∈ ( 𝑀 [,) +∞ ) ∀ 𝑥 ∈ 𝐴 ( 𝑧 ≤ 𝑥 → ( abs ‘ ( 𝐶 − 𝐸 ) ) < 𝑦 ) ) )
48 47 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ( 𝑀 [,) +∞ ) ∀ 𝑥 ∈ 𝐴 ( 𝑧 ≤ 𝑥 → ( abs ‘ ( 𝐵 − 𝐷 ) ) < 𝑦 ) → ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ( 𝑀 [,) +∞ ) ∀ 𝑥 ∈ 𝐴 ( 𝑧 ≤ 𝑥 → ( abs ‘ ( 𝐶 − 𝐸 ) ) < 𝑦 ) ) )
49 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ℂ )
50 49 17 33 1 rlim3 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐷 ↔ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ( 𝑀 [,) +∞ ) ∀ 𝑥 ∈ 𝐴 ( 𝑧 ≤ 𝑥 → ( abs ‘ ( 𝐵 − 𝐷 ) ) < 𝑦 ) ) )
51 5 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐶 ∈ ℂ )
52 51 17 2 1 rlim3 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐸 ↔ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ( 𝑀 [,) +∞ ) ∀ 𝑥 ∈ 𝐴 ( 𝑧 ≤ 𝑥 → ( abs ‘ ( 𝐶 − 𝐸 ) ) < 𝑦 ) ) )
53 48 50 52 3imtr4d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐷 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐸 ) )
54 3 53 mpd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐸 )