MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rlimcn3 Structured version   Visualization version   GIF version

Theorem rlimcn3 15574
Description: Image of a limit under a continuous map, two-arg version. Originally a subproof of rlimcn2 15575. (Contributed by SN, 27-Sep-2024.)
Hypotheses
Ref Expression
rlimcn3.1a ((𝜑𝑧𝐴) → 𝐵𝑋)
rlimcn3.1b ((𝜑𝑧𝐴) → 𝐶𝑌)
rlimcn3.1c ((𝜑𝑧𝐴) → (𝐵𝐹𝐶) ∈ ℂ)
rlimcn3.2 (𝜑 → (𝑅𝐹𝑆) ∈ ℂ)
rlimcn3.3a (𝜑 → (𝑧𝐴𝐵) ⇝𝑟 𝑅)
rlimcn3.3b (𝜑 → (𝑧𝐴𝐶) ⇝𝑟 𝑆)
rlimcn3.4 ((𝜑𝑥 ∈ ℝ+) → ∃𝑟 ∈ ℝ+𝑠 ∈ ℝ+𝑢𝑋𝑣𝑌 (((abs‘(𝑢𝑅)) < 𝑟 ∧ (abs‘(𝑣𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥))
Assertion
Ref Expression
rlimcn3 (𝜑 → (𝑧𝐴 ↦ (𝐵𝐹𝐶)) ⇝𝑟 (𝑅𝐹𝑆))
Distinct variable groups:   𝑠,𝑟,𝑥,𝑧,𝐴   𝑢,𝑟,𝑣,𝐹,𝑠,𝑥,𝑧   𝑅,𝑟,𝑠,𝑢,𝑣,𝑥,𝑧   𝐵,𝑟,𝑠,𝑢,𝑣,𝑥   𝜑,𝑟,𝑠,𝑥,𝑧   𝑆,𝑟,𝑠,𝑢,𝑣,𝑥,𝑧   𝐶,𝑟,𝑠,𝑣,𝑥   𝑢,𝑋,𝑧   𝑢,𝑌,𝑣,𝑧
Allowed substitution hints:   𝜑(𝑣,𝑢)   𝐴(𝑣,𝑢)   𝐵(𝑧)   𝐶(𝑧,𝑢)   𝑋(𝑥,𝑣,𝑠,𝑟)   𝑌(𝑥,𝑠,𝑟)

Proof of Theorem rlimcn3
Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rlimcn3.4 . . . 4 ((𝜑𝑥 ∈ ℝ+) → ∃𝑟 ∈ ℝ+𝑠 ∈ ℝ+𝑢𝑋𝑣𝑌 (((abs‘(𝑢𝑅)) < 𝑟 ∧ (abs‘(𝑣𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥))
2 rlimcn3.1a . . . . . . . . . 10 ((𝜑𝑧𝐴) → 𝐵𝑋)
32ralrimiva 3143 . . . . . . . . 9 (𝜑 → ∀𝑧𝐴 𝐵𝑋)
43adantr 479 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) → ∀𝑧𝐴 𝐵𝑋)
5 simprl 769 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) → 𝑟 ∈ ℝ+)
6 rlimcn3.3a . . . . . . . . 9 (𝜑 → (𝑧𝐴𝐵) ⇝𝑟 𝑅)
76adantr 479 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) → (𝑧𝐴𝐵) ⇝𝑟 𝑅)
84, 5, 7rlimi 15497 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) → ∃𝑎 ∈ ℝ ∀𝑧𝐴 (𝑎𝑧 → (abs‘(𝐵𝑅)) < 𝑟))
9 rlimcn3.1b . . . . . . . . . 10 ((𝜑𝑧𝐴) → 𝐶𝑌)
109ralrimiva 3143 . . . . . . . . 9 (𝜑 → ∀𝑧𝐴 𝐶𝑌)
1110adantr 479 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) → ∀𝑧𝐴 𝐶𝑌)
12 simprr 771 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) → 𝑠 ∈ ℝ+)
13 rlimcn3.3b . . . . . . . . 9 (𝜑 → (𝑧𝐴𝐶) ⇝𝑟 𝑆)
1413adantr 479 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) → (𝑧𝐴𝐶) ⇝𝑟 𝑆)
1511, 12, 14rlimi 15497 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) → ∃𝑏 ∈ ℝ ∀𝑧𝐴 (𝑏𝑧 → (abs‘(𝐶𝑆)) < 𝑠))
16 reeanv 3224 . . . . . . . 8 (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ (∀𝑧𝐴 (𝑎𝑧 → (abs‘(𝐵𝑅)) < 𝑟) ∧ ∀𝑧𝐴 (𝑏𝑧 → (abs‘(𝐶𝑆)) < 𝑠)) ↔ (∃𝑎 ∈ ℝ ∀𝑧𝐴 (𝑎𝑧 → (abs‘(𝐵𝑅)) < 𝑟) ∧ ∃𝑏 ∈ ℝ ∀𝑧𝐴 (𝑏𝑧 → (abs‘(𝐶𝑆)) < 𝑠)))
17 r19.26 3108 . . . . . . . . . 10 (∀𝑧𝐴 ((𝑎𝑧 → (abs‘(𝐵𝑅)) < 𝑟) ∧ (𝑏𝑧 → (abs‘(𝐶𝑆)) < 𝑠)) ↔ (∀𝑧𝐴 (𝑎𝑧 → (abs‘(𝐵𝑅)) < 𝑟) ∧ ∀𝑧𝐴 (𝑏𝑧 → (abs‘(𝐶𝑆)) < 𝑠)))
18 anim12 807 . . . . . . . . . . . . 13 (((𝑎𝑧 → (abs‘(𝐵𝑅)) < 𝑟) ∧ (𝑏𝑧 → (abs‘(𝐶𝑆)) < 𝑠)) → ((𝑎𝑧𝑏𝑧) → ((abs‘(𝐵𝑅)) < 𝑟 ∧ (abs‘(𝐶𝑆)) < 𝑠)))
19 simplrl 775 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ 𝑧𝐴) → 𝑎 ∈ ℝ)
20 simplrr 776 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ 𝑧𝐴) → 𝑏 ∈ ℝ)
21 eqid 2728 . . . . . . . . . . . . . . . . . . 19 (𝑧𝐴𝐵) = (𝑧𝐴𝐵)
2221, 2dmmptd 6705 . . . . . . . . . . . . . . . . . 18 (𝜑 → dom (𝑧𝐴𝐵) = 𝐴)
23 rlimss 15486 . . . . . . . . . . . . . . . . . . 19 ((𝑧𝐴𝐵) ⇝𝑟 𝑅 → dom (𝑧𝐴𝐵) ⊆ ℝ)
246, 23syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → dom (𝑧𝐴𝐵) ⊆ ℝ)
2522, 24eqsstrrd 4021 . . . . . . . . . . . . . . . . 17 (𝜑𝐴 ⊆ ℝ)
2625ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → 𝐴 ⊆ ℝ)
2726sselda 3982 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ 𝑧𝐴) → 𝑧 ∈ ℝ)
28 maxle 13210 . . . . . . . . . . . . . . 15 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑧 ↔ (𝑎𝑧𝑏𝑧)))
2919, 20, 27, 28syl3anc 1368 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ 𝑧𝐴) → (if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑧 ↔ (𝑎𝑧𝑏𝑧)))
3029imbi1d 340 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ 𝑧𝐴) → ((if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑧 → ((abs‘(𝐵𝑅)) < 𝑟 ∧ (abs‘(𝐶𝑆)) < 𝑠)) ↔ ((𝑎𝑧𝑏𝑧) → ((abs‘(𝐵𝑅)) < 𝑟 ∧ (abs‘(𝐶𝑆)) < 𝑠))))
3118, 30imbitrrid 245 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ 𝑧𝐴) → (((𝑎𝑧 → (abs‘(𝐵𝑅)) < 𝑟) ∧ (𝑏𝑧 → (abs‘(𝐶𝑆)) < 𝑠)) → (if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑧 → ((abs‘(𝐵𝑅)) < 𝑟 ∧ (abs‘(𝐶𝑆)) < 𝑠))))
3231ralimdva 3164 . . . . . . . . . . 11 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → (∀𝑧𝐴 ((𝑎𝑧 → (abs‘(𝐵𝑅)) < 𝑟) ∧ (𝑏𝑧 → (abs‘(𝐶𝑆)) < 𝑠)) → ∀𝑧𝐴 (if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑧 → ((abs‘(𝐵𝑅)) < 𝑟 ∧ (abs‘(𝐶𝑆)) < 𝑠))))
33 ifcl 4577 . . . . . . . . . . . . . . . 16 ((𝑏 ∈ ℝ ∧ 𝑎 ∈ ℝ) → if(𝑎𝑏, 𝑏, 𝑎) ∈ ℝ)
3433ancoms 457 . . . . . . . . . . . . . . 15 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → if(𝑎𝑏, 𝑏, 𝑎) ∈ ℝ)
3534ad2antlr 725 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ ∀𝑢𝑋𝑣𝑌 (((abs‘(𝑢𝑅)) < 𝑟 ∧ (abs‘(𝑣𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥)) → if(𝑎𝑏, 𝑏, 𝑎) ∈ ℝ)
362adantlr 713 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) ∧ 𝑧𝐴) → 𝐵𝑋)
379adantlr 713 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) ∧ 𝑧𝐴) → 𝐶𝑌)
3836, 37jca 510 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) ∧ 𝑧𝐴) → (𝐵𝑋𝐶𝑌))
39 fvoveq1 7449 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝐵 → (abs‘(𝑢𝑅)) = (abs‘(𝐵𝑅)))
4039breq1d 5162 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝐵 → ((abs‘(𝑢𝑅)) < 𝑟 ↔ (abs‘(𝐵𝑅)) < 𝑟))
4140anbi1d 629 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = 𝐵 → (((abs‘(𝑢𝑅)) < 𝑟 ∧ (abs‘(𝑣𝑆)) < 𝑠) ↔ ((abs‘(𝐵𝑅)) < 𝑟 ∧ (abs‘(𝑣𝑆)) < 𝑠)))
42 oveq1 7433 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 = 𝐵 → (𝑢𝐹𝑣) = (𝐵𝐹𝑣))
4342fvoveq1d 7448 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝐵 → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) = (abs‘((𝐵𝐹𝑣) − (𝑅𝐹𝑆))))
4443breq1d 5162 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = 𝐵 → ((abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥 ↔ (abs‘((𝐵𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥))
4541, 44imbi12d 343 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = 𝐵 → ((((abs‘(𝑢𝑅)) < 𝑟 ∧ (abs‘(𝑣𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥) ↔ (((abs‘(𝐵𝑅)) < 𝑟 ∧ (abs‘(𝑣𝑆)) < 𝑠) → (abs‘((𝐵𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥)))
46 fvoveq1 7449 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 = 𝐶 → (abs‘(𝑣𝑆)) = (abs‘(𝐶𝑆)))
4746breq1d 5162 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 = 𝐶 → ((abs‘(𝑣𝑆)) < 𝑠 ↔ (abs‘(𝐶𝑆)) < 𝑠))
4847anbi2d 628 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = 𝐶 → (((abs‘(𝐵𝑅)) < 𝑟 ∧ (abs‘(𝑣𝑆)) < 𝑠) ↔ ((abs‘(𝐵𝑅)) < 𝑟 ∧ (abs‘(𝐶𝑆)) < 𝑠)))
49 oveq2 7434 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 = 𝐶 → (𝐵𝐹𝑣) = (𝐵𝐹𝐶))
5049fvoveq1d 7448 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 = 𝐶 → (abs‘((𝐵𝐹𝑣) − (𝑅𝐹𝑆))) = (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))))
5150breq1d 5162 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = 𝐶 → ((abs‘((𝐵𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥 ↔ (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥))
5248, 51imbi12d 343 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = 𝐶 → ((((abs‘(𝐵𝑅)) < 𝑟 ∧ (abs‘(𝑣𝑆)) < 𝑠) → (abs‘((𝐵𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥) ↔ (((abs‘(𝐵𝑅)) < 𝑟 ∧ (abs‘(𝐶𝑆)) < 𝑠) → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥)))
5345, 52rspc2va 3623 . . . . . . . . . . . . . . . . . . 19 (((𝐵𝑋𝐶𝑌) ∧ ∀𝑢𝑋𝑣𝑌 (((abs‘(𝑢𝑅)) < 𝑟 ∧ (abs‘(𝑣𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥)) → (((abs‘(𝐵𝑅)) < 𝑟 ∧ (abs‘(𝐶𝑆)) < 𝑠) → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥))
5438, 53sylan 578 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) ∧ 𝑧𝐴) ∧ ∀𝑢𝑋𝑣𝑌 (((abs‘(𝑢𝑅)) < 𝑟 ∧ (abs‘(𝑣𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥)) → (((abs‘(𝐵𝑅)) < 𝑟 ∧ (abs‘(𝐶𝑆)) < 𝑠) → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥))
5554imim2d 57 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) ∧ 𝑧𝐴) ∧ ∀𝑢𝑋𝑣𝑌 (((abs‘(𝑢𝑅)) < 𝑟 ∧ (abs‘(𝑣𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥)) → ((if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑧 → ((abs‘(𝐵𝑅)) < 𝑟 ∧ (abs‘(𝐶𝑆)) < 𝑠)) → (if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥)))
5655an32s 650 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) ∧ ∀𝑢𝑋𝑣𝑌 (((abs‘(𝑢𝑅)) < 𝑟 ∧ (abs‘(𝑣𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥)) ∧ 𝑧𝐴) → ((if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑧 → ((abs‘(𝐵𝑅)) < 𝑟 ∧ (abs‘(𝐶𝑆)) < 𝑠)) → (if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥)))
5756ralimdva 3164 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) ∧ ∀𝑢𝑋𝑣𝑌 (((abs‘(𝑢𝑅)) < 𝑟 ∧ (abs‘(𝑣𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥)) → (∀𝑧𝐴 (if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑧 → ((abs‘(𝐵𝑅)) < 𝑟 ∧ (abs‘(𝐶𝑆)) < 𝑠)) → ∀𝑧𝐴 (if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥)))
5857adantlr 713 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ ∀𝑢𝑋𝑣𝑌 (((abs‘(𝑢𝑅)) < 𝑟 ∧ (abs‘(𝑣𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥)) → (∀𝑧𝐴 (if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑧 → ((abs‘(𝐵𝑅)) < 𝑟 ∧ (abs‘(𝐶𝑆)) < 𝑠)) → ∀𝑧𝐴 (if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥)))
59 breq1 5155 . . . . . . . . . . . . . . 15 (𝑐 = if(𝑎𝑏, 𝑏, 𝑎) → (𝑐𝑧 ↔ if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑧))
6059rspceaimv 3617 . . . . . . . . . . . . . 14 ((if(𝑎𝑏, 𝑏, 𝑎) ∈ ℝ ∧ ∀𝑧𝐴 (if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥)) → ∃𝑐 ∈ ℝ ∀𝑧𝐴 (𝑐𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥))
6135, 58, 60syl6an 682 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) ∧ ∀𝑢𝑋𝑣𝑌 (((abs‘(𝑢𝑅)) < 𝑟 ∧ (abs‘(𝑣𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥)) → (∀𝑧𝐴 (if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑧 → ((abs‘(𝐵𝑅)) < 𝑟 ∧ (abs‘(𝐶𝑆)) < 𝑠)) → ∃𝑐 ∈ ℝ ∀𝑧𝐴 (𝑐𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥)))
6261ex 411 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → (∀𝑢𝑋𝑣𝑌 (((abs‘(𝑢𝑅)) < 𝑟 ∧ (abs‘(𝑣𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥) → (∀𝑧𝐴 (if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑧 → ((abs‘(𝐵𝑅)) < 𝑟 ∧ (abs‘(𝐶𝑆)) < 𝑠)) → ∃𝑐 ∈ ℝ ∀𝑧𝐴 (𝑐𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥))))
6362com23 86 . . . . . . . . . . 11 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → (∀𝑧𝐴 (if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑧 → ((abs‘(𝐵𝑅)) < 𝑟 ∧ (abs‘(𝐶𝑆)) < 𝑠)) → (∀𝑢𝑋𝑣𝑌 (((abs‘(𝑢𝑅)) < 𝑟 ∧ (abs‘(𝑣𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥) → ∃𝑐 ∈ ℝ ∀𝑧𝐴 (𝑐𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥))))
6432, 63syld 47 . . . . . . . . . 10 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → (∀𝑧𝐴 ((𝑎𝑧 → (abs‘(𝐵𝑅)) < 𝑟) ∧ (𝑏𝑧 → (abs‘(𝐶𝑆)) < 𝑠)) → (∀𝑢𝑋𝑣𝑌 (((abs‘(𝑢𝑅)) < 𝑟 ∧ (abs‘(𝑣𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥) → ∃𝑐 ∈ ℝ ∀𝑧𝐴 (𝑐𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥))))
6517, 64biimtrrid 242 . . . . . . . . 9 (((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) → ((∀𝑧𝐴 (𝑎𝑧 → (abs‘(𝐵𝑅)) < 𝑟) ∧ ∀𝑧𝐴 (𝑏𝑧 → (abs‘(𝐶𝑆)) < 𝑠)) → (∀𝑢𝑋𝑣𝑌 (((abs‘(𝑢𝑅)) < 𝑟 ∧ (abs‘(𝑣𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥) → ∃𝑐 ∈ ℝ ∀𝑧𝐴 (𝑐𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥))))
6665rexlimdvva 3209 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ (∀𝑧𝐴 (𝑎𝑧 → (abs‘(𝐵𝑅)) < 𝑟) ∧ ∀𝑧𝐴 (𝑏𝑧 → (abs‘(𝐶𝑆)) < 𝑠)) → (∀𝑢𝑋𝑣𝑌 (((abs‘(𝑢𝑅)) < 𝑟 ∧ (abs‘(𝑣𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥) → ∃𝑐 ∈ ℝ ∀𝑧𝐴 (𝑐𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥))))
6716, 66biimtrrid 242 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) → ((∃𝑎 ∈ ℝ ∀𝑧𝐴 (𝑎𝑧 → (abs‘(𝐵𝑅)) < 𝑟) ∧ ∃𝑏 ∈ ℝ ∀𝑧𝐴 (𝑏𝑧 → (abs‘(𝐶𝑆)) < 𝑠)) → (∀𝑢𝑋𝑣𝑌 (((abs‘(𝑢𝑅)) < 𝑟 ∧ (abs‘(𝑣𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥) → ∃𝑐 ∈ ℝ ∀𝑧𝐴 (𝑐𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥))))
688, 15, 67mp2and 697 . . . . . 6 ((𝜑 ∧ (𝑟 ∈ ℝ+𝑠 ∈ ℝ+)) → (∀𝑢𝑋𝑣𝑌 (((abs‘(𝑢𝑅)) < 𝑟 ∧ (abs‘(𝑣𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥) → ∃𝑐 ∈ ℝ ∀𝑧𝐴 (𝑐𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥)))
6968rexlimdvva 3209 . . . . 5 (𝜑 → (∃𝑟 ∈ ℝ+𝑠 ∈ ℝ+𝑢𝑋𝑣𝑌 (((abs‘(𝑢𝑅)) < 𝑟 ∧ (abs‘(𝑣𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥) → ∃𝑐 ∈ ℝ ∀𝑧𝐴 (𝑐𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥)))
7069imp 405 . . . 4 ((𝜑 ∧ ∃𝑟 ∈ ℝ+𝑠 ∈ ℝ+𝑢𝑋𝑣𝑌 (((abs‘(𝑢𝑅)) < 𝑟 ∧ (abs‘(𝑣𝑆)) < 𝑠) → (abs‘((𝑢𝐹𝑣) − (𝑅𝐹𝑆))) < 𝑥)) → ∃𝑐 ∈ ℝ ∀𝑧𝐴 (𝑐𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥))
711, 70syldan 589 . . 3 ((𝜑𝑥 ∈ ℝ+) → ∃𝑐 ∈ ℝ ∀𝑧𝐴 (𝑐𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥))
7271ralrimiva 3143 . 2 (𝜑 → ∀𝑥 ∈ ℝ+𝑐 ∈ ℝ ∀𝑧𝐴 (𝑐𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥))
73 rlimcn3.1c . . . 4 ((𝜑𝑧𝐴) → (𝐵𝐹𝐶) ∈ ℂ)
7473ralrimiva 3143 . . 3 (𝜑 → ∀𝑧𝐴 (𝐵𝐹𝐶) ∈ ℂ)
75 rlimcn3.2 . . 3 (𝜑 → (𝑅𝐹𝑆) ∈ ℂ)
7674, 25, 75rlim2 15480 . 2 (𝜑 → ((𝑧𝐴 ↦ (𝐵𝐹𝐶)) ⇝𝑟 (𝑅𝐹𝑆) ↔ ∀𝑥 ∈ ℝ+𝑐 ∈ ℝ ∀𝑧𝐴 (𝑐𝑧 → (abs‘((𝐵𝐹𝐶) − (𝑅𝐹𝑆))) < 𝑥)))
7772, 76mpbird 256 1 (𝜑 → (𝑧𝐴 ↦ (𝐵𝐹𝐶)) ⇝𝑟 (𝑅𝐹𝑆))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1533  wcel 2098  wral 3058  wrex 3067  wss 3949  ifcif 4532   class class class wbr 5152  cmpt 5235  dom cdm 5682  cfv 6553  (class class class)co 7426  cc 11144  cr 11145   < clt 11286  cle 11287  cmin 11482  +crp 13014  abscabs 15221  𝑟 crli 15469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11202  ax-resscn 11203  ax-pre-lttri 11220  ax-pre-lttrn 11221
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5580  df-po 5594  df-so 5595  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-ov 7429  df-oprab 7430  df-mpo 7431  df-er 8731  df-pm 8854  df-en 8971  df-dom 8972  df-sdom 8973  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-rlim 15473
This theorem is referenced by:  rlimcn2  15575  rlimadd  15627  rlimmul  15630
  Copyright terms: Public domain W3C validator