Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  limclner Structured version   Visualization version   GIF version

Theorem limclner 45068
Description: For a limit point, both from the left and from the right, of the domain, the limit of the function exits only if the left and the right limits are equal. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
limclner.k 𝐾 = (TopOpenβ€˜β„‚fld)
limclner.a (πœ‘ β†’ 𝐴 βŠ† ℝ)
limclner.j 𝐽 = (topGenβ€˜ran (,))
limclner.f (πœ‘ β†’ 𝐹:π΄βŸΆβ„‚)
limclner.blp1 (πœ‘ β†’ 𝐡 ∈ ((limPtβ€˜π½)β€˜(𝐴 ∩ (-∞(,)𝐡))))
limclner.blp2 (πœ‘ β†’ 𝐡 ∈ ((limPtβ€˜π½)β€˜(𝐴 ∩ (𝐡(,)+∞))))
limclner.l (πœ‘ β†’ 𝐿 ∈ ((𝐹 β†Ύ (-∞(,)𝐡)) limβ„‚ 𝐡))
limclner.r (πœ‘ β†’ 𝑅 ∈ ((𝐹 β†Ύ (𝐡(,)+∞)) limβ„‚ 𝐡))
limclner.lner (πœ‘ β†’ 𝐿 β‰  𝑅)
Assertion
Ref Expression
limclner (πœ‘ β†’ (𝐹 limβ„‚ 𝐡) = βˆ…)

Proof of Theorem limclner
Dummy variables π‘Ž 𝑏 𝑒 𝑣 𝑧 𝑀 π‘₯ 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 limccl 25824 . . . . . . . . . . . . 13 ((𝐹 β†Ύ (𝐡(,)+∞)) limβ„‚ 𝐡) βŠ† β„‚
2 limclner.r . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑅 ∈ ((𝐹 β†Ύ (𝐡(,)+∞)) limβ„‚ 𝐡))
31, 2sselid 3980 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑅 ∈ β„‚)
43ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ 𝑅 ∈ β„‚)
5 limccl 25824 . . . . . . . . . . . . 13 ((𝐹 β†Ύ (-∞(,)𝐡)) limβ„‚ 𝐡) βŠ† β„‚
6 limclner.l . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐿 ∈ ((𝐹 β†Ύ (-∞(,)𝐡)) limβ„‚ 𝐡))
75, 6sselid 3980 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐿 ∈ β„‚)
87ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ 𝐿 ∈ β„‚)
94, 8subcld 11609 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (𝑅 βˆ’ 𝐿) ∈ β„‚)
10 limclner.lner . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐿 β‰  𝑅)
1110necomd 2993 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑅 β‰  𝐿)
1211ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ 𝑅 β‰  𝐿)
134, 8, 12subne0d 11618 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (𝑅 βˆ’ 𝐿) β‰  0)
149, 13absrpcld 15435 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) ∈ ℝ+)
15 4re 12334 . . . . . . . . . . 11 4 ∈ ℝ
16 4pos 12357 . . . . . . . . . . 11 0 < 4
1715, 16elrpii 13017 . . . . . . . . . 10 4 ∈ ℝ+
1817a1i 11 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ 4 ∈ ℝ+)
1914, 18rpdivcld 13073 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) ∈ ℝ+)
20 nfv 1909 . . . . . . . . . . 11 Ⅎ𝑦(πœ‘ ∧ π‘₯ ∈ β„‚)
21 nfra1 3279 . . . . . . . . . . 11 β„²π‘¦βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)
2220, 21nfan 1894 . . . . . . . . . 10 Ⅎ𝑦((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦))
23 nfv 1909 . . . . . . . . . 10 Ⅎ𝑦(((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) ∈ ℝ+ β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)))
2422, 23nfim 1891 . . . . . . . . 9 Ⅎ𝑦(((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) ∈ ℝ+ β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))))
25 ovex 7459 . . . . . . . . 9 ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) ∈ V
26 eleq1 2817 . . . . . . . . . . 11 (𝑦 = ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) β†’ (𝑦 ∈ ℝ+ ↔ ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) ∈ ℝ+))
27 oveq2 7434 . . . . . . . . . . . . 13 (𝑦 = ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) β†’ (4 Β· 𝑦) = (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)))
2827breq2d 5164 . . . . . . . . . . . 12 (𝑦 = ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) β†’ ((absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦) ↔ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))))
29282rexbidv 3217 . . . . . . . . . . 11 (𝑦 = ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) β†’ (βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦) ↔ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))))
3026, 29imbi12d 343 . . . . . . . . . 10 (𝑦 = ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) β†’ ((𝑦 ∈ ℝ+ β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦)) ↔ (((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) ∈ ℝ+ β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)))))
3130imbi2d 339 . . . . . . . . 9 (𝑦 = ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) β†’ ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (𝑦 ∈ ℝ+ β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦))) ↔ (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) ∈ ℝ+ β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))))))
32 simpll 765 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) β†’ (πœ‘ ∧ π‘₯ ∈ β„‚))
33 simpr 483 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) β†’ 𝑦 ∈ ℝ+)
34 rspa 3243 . . . . . . . . . . . 12 ((βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦) ∧ 𝑦 ∈ ℝ+) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦))
3534adantll 712 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦))
36 limclner.f . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 𝐹:π΄βŸΆβ„‚)
37 fresin 6771 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹:π΄βŸΆβ„‚ β†’ (𝐹 β†Ύ (𝐡(,)+∞)):(𝐴 ∩ (𝐡(,)+∞))βŸΆβ„‚)
3836, 37syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (𝐹 β†Ύ (𝐡(,)+∞)):(𝐴 ∩ (𝐡(,)+∞))βŸΆβ„‚)
39 inss2 4232 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 ∩ (𝐡(,)+∞)) βŠ† (𝐡(,)+∞)
40 ioosscn 13426 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐡(,)+∞) βŠ† β„‚
4139, 40sstri 3991 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∩ (𝐡(,)+∞)) βŠ† β„‚
4241a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (𝐴 ∩ (𝐡(,)+∞)) βŠ† β„‚)
43 limclner.j . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝐽 = (topGenβ€˜ran (,))
44 retop 24698 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (topGenβ€˜ran (,)) ∈ Top
4543, 44eqeltri 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝐽 ∈ Top
46 inss2 4232 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐴 ∩ (-∞(,)𝐡)) βŠ† (-∞(,)𝐡)
47 ioossre 13425 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (-∞(,)𝐡) βŠ† ℝ
4846, 47sstri 3991 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐴 ∩ (-∞(,)𝐡)) βŠ† ℝ
49 uniretop 24699 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ℝ = βˆͺ (topGenβ€˜ran (,))
5043unieqi 4924 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 βˆͺ 𝐽 = βˆͺ (topGenβ€˜ran (,))
5149, 50eqtr4i 2759 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ℝ = βˆͺ 𝐽
5251lpss 23066 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐽 ∈ Top ∧ (𝐴 ∩ (-∞(,)𝐡)) βŠ† ℝ) β†’ ((limPtβ€˜π½)β€˜(𝐴 ∩ (-∞(,)𝐡))) βŠ† ℝ)
5345, 48, 52mp2an 690 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((limPtβ€˜π½)β€˜(𝐴 ∩ (-∞(,)𝐡))) βŠ† ℝ
54 limclner.blp1 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ 𝐡 ∈ ((limPtβ€˜π½)β€˜(𝐴 ∩ (-∞(,)𝐡))))
5553, 54sselid 3980 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 𝐡 ∈ ℝ)
5655recnd 11280 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 𝐡 ∈ β„‚)
5738, 42, 56ellimc3 25828 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (𝑅 ∈ ((𝐹 β†Ύ (𝐡(,)+∞)) limβ„‚ 𝐡) ↔ (𝑅 ∈ β„‚ ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦))))
582, 57mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (𝑅 ∈ β„‚ ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)))
5958simprd 494 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦))
6059r19.21bi 3246 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑦 ∈ ℝ+) β†’ βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦))
61603ad2ant1 1130 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦))
62 simp11l 1281 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) β†’ πœ‘)
63 simp12 1201 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) β†’ 𝑧 ∈ ℝ+)
64 simp2 1134 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) β†’ 𝑣 ∈ ℝ+)
65 breq2 5156 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑒 = if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑒 ↔ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)))
6665rexbidv 3176 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑒 = if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ (βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})(absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑒 ↔ βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})(absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)))
67 inss1 4231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((limPtβ€˜πΎ)β€˜(𝐴 ∩ (𝐡(,)+∞))) ∩ ℝ) βŠ† ((limPtβ€˜πΎ)β€˜(𝐴 ∩ (𝐡(,)+∞)))
6867a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (πœ‘ β†’ (((limPtβ€˜πΎ)β€˜(𝐴 ∩ (𝐡(,)+∞))) ∩ ℝ) βŠ† ((limPtβ€˜πΎ)β€˜(𝐴 ∩ (𝐡(,)+∞))))
69 limclner.k . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝐾 = (TopOpenβ€˜β„‚fld)
7069cnfldtop 24720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝐾 ∈ Top
7170a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (πœ‘ β†’ 𝐾 ∈ Top)
72 ax-resscn 11203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ℝ βŠ† β„‚
7372a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (πœ‘ β†’ ℝ βŠ† β„‚)
74 ioossre 13425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐡(,)+∞) βŠ† ℝ
7539, 74sstri 3991 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐴 ∩ (𝐡(,)+∞)) βŠ† ℝ
7675a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (πœ‘ β†’ (𝐴 ∩ (𝐡(,)+∞)) βŠ† ℝ)
77 unicntop 24722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 β„‚ = βˆͺ (TopOpenβ€˜β„‚fld)
7869unieqi 4924 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 βˆͺ 𝐾 = βˆͺ (TopOpenβ€˜β„‚fld)
7977, 78eqtr4i 2759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 β„‚ = βˆͺ 𝐾
8069tgioo2 24739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (topGenβ€˜ran (,)) = (𝐾 β†Ύt ℝ)
8143, 80eqtri 2756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝐽 = (𝐾 β†Ύt ℝ)
8279, 81restlp 23107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐾 ∈ Top ∧ ℝ βŠ† β„‚ ∧ (𝐴 ∩ (𝐡(,)+∞)) βŠ† ℝ) β†’ ((limPtβ€˜π½)β€˜(𝐴 ∩ (𝐡(,)+∞))) = (((limPtβ€˜πΎ)β€˜(𝐴 ∩ (𝐡(,)+∞))) ∩ ℝ))
8371, 73, 76, 82syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (πœ‘ β†’ ((limPtβ€˜π½)β€˜(𝐴 ∩ (𝐡(,)+∞))) = (((limPtβ€˜πΎ)β€˜(𝐴 ∩ (𝐡(,)+∞))) ∩ ℝ))
8469eqcomi 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (TopOpenβ€˜β„‚fld) = 𝐾
8584fveq2i 6905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (limPtβ€˜(TopOpenβ€˜β„‚fld)) = (limPtβ€˜πΎ)
8685fveq1i 6903 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (𝐡(,)+∞))) = ((limPtβ€˜πΎ)β€˜(𝐴 ∩ (𝐡(,)+∞)))
8786a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (πœ‘ β†’ ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (𝐡(,)+∞))) = ((limPtβ€˜πΎ)β€˜(𝐴 ∩ (𝐡(,)+∞))))
8868, 83, 873sstr4d 4029 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ ((limPtβ€˜π½)β€˜(𝐴 ∩ (𝐡(,)+∞))) βŠ† ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (𝐡(,)+∞))))
89 limclner.blp2 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ 𝐡 ∈ ((limPtβ€˜π½)β€˜(𝐴 ∩ (𝐡(,)+∞))))
9088, 89sseldd 3983 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ 𝐡 ∈ ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (𝐡(,)+∞))))
9142, 56islpcn 45056 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ (𝐡 ∈ ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (𝐡(,)+∞))) ↔ βˆ€π‘’ ∈ ℝ+ βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})(absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑒))
9290, 91mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ βˆ€π‘’ ∈ ℝ+ βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})(absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑒)
93923ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ βˆ€π‘’ ∈ ℝ+ βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})(absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑒)
94 ifcl 4577 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ∈ ℝ+)
95943adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ∈ ℝ+)
9666, 93, 95rspcdva 3612 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})(absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣))
97 eldifi 4127 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) β†’ 𝑏 ∈ (𝐴 ∩ (𝐡(,)+∞)))
9875, 97sselid 3980 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) β†’ 𝑏 ∈ ℝ)
9973sselda 3982 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((πœ‘ ∧ 𝑏 ∈ ℝ) β†’ 𝑏 ∈ β„‚)
10056adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((πœ‘ ∧ 𝑏 ∈ ℝ) β†’ 𝐡 ∈ β„‚)
10199, 100subcld 11609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((πœ‘ ∧ 𝑏 ∈ ℝ) β†’ (𝑏 βˆ’ 𝐡) ∈ β„‚)
102101abscld 15423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((πœ‘ ∧ 𝑏 ∈ ℝ) β†’ (absβ€˜(𝑏 βˆ’ 𝐡)) ∈ ℝ)
1031023ad2antl1 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) β†’ (absβ€˜(𝑏 βˆ’ 𝐡)) ∈ ℝ)
104103adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ (absβ€˜(𝑏 βˆ’ 𝐡)) ∈ ℝ)
10595rpred 13056 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ∈ ℝ)
106105ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ∈ ℝ)
107 rpre 13022 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 ∈ ℝ+ β†’ 𝑧 ∈ ℝ)
1081073ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ 𝑧 ∈ ℝ)
109108ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ 𝑧 ∈ ℝ)
110 simpr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣))
111 rpre 13022 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑣 ∈ ℝ+ β†’ 𝑣 ∈ ℝ)
112 min1 13208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑧)
113107, 111, 112syl2an 594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑧)
1141133adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑧)
115114ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑧)
116104, 106, 109, 110, 115ltletrd 11412 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧)
1171113ad2ant3 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ 𝑣 ∈ ℝ)
118117ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ 𝑣 ∈ ℝ)
119109, 118min2d 44884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑣)
120104, 106, 118, 110, 119ltletrd 11412 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)
121116, 120jca 510 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣))
122121ex 411 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) β†’ ((absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)))
12398, 122sylan2 591 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})) β†’ ((absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)))
124123reximdva 3165 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ (βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})(absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)))
12596, 124mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣))
12662, 63, 64, 125syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) β†’ βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣))
127 nfv 1909 . . . . . . . . . . . . . . . . . . . . . . 23 Ⅎ𝑏(((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦))
128 nfre1 3280 . . . . . . . . . . . . . . . . . . . . . . 23 β„²π‘βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)
12997elin1d 4200 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) β†’ 𝑏 ∈ 𝐴)
1301293ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ 𝑏 ∈ 𝐴)
131 simp113 1301 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦))
132 eldifsni 4798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) β†’ 𝑏 β‰  𝐡)
133132adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ 𝑏 β‰  𝐡)
134 simprl 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧)
135133, 134jca 510 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ (𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧))
1361353adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ (𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧))
137 neeq1 3000 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑀 = 𝑏 β†’ (𝑀 β‰  𝐡 ↔ 𝑏 β‰  𝐡))
138 fvoveq1 7449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑀 = 𝑏 β†’ (absβ€˜(𝑀 βˆ’ 𝐡)) = (absβ€˜(𝑏 βˆ’ 𝐡)))
139138breq1d 5162 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑀 = 𝑏 β†’ ((absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧 ↔ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧))
140137, 139anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑀 = 𝑏 β†’ ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) ↔ (𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧)))
141140imbrov2fvoveq 7451 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑀 = 𝑏 β†’ (((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦) ↔ ((𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦)))
142141rspcva 3609 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑏 ∈ 𝐴 ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ ((𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦))
143142imp 405 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑏 ∈ 𝐴 ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ (𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧)) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦)
144130, 131, 136, 143syl21anc 836 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦)
145973ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ 𝑏 ∈ (𝐴 ∩ (𝐡(,)+∞)))
146623ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ πœ‘)
147 simp13 1202 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦))
148 nfv 1909 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 β„²π‘€πœ‘
149 nfra1 3279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 β„²π‘€βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)
150148, 149nfan 1894 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ⅎ𝑀(πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦))
151 elinel2 4198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞)) β†’ 𝑀 ∈ (𝐡(,)+∞))
152151fvresd 6922 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞)) β†’ ((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) = (πΉβ€˜π‘€))
153152eqcomd 2734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞)) β†’ (πΉβ€˜π‘€) = ((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€))
154153fvoveq1d 7448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞)) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝑅)) = (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)))
1551543ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞)) ∧ (𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝑅)) = (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)))
156 rspa 3243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦) ∧ 𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞))) β†’ ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦))
1571563impia 1114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦) ∧ 𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞)) ∧ (𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)
1581573adant1l 1173 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞)) ∧ (𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)
159155, 158eqbrtrd 5174 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞)) ∧ (𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝑅)) < 𝑦)
1601593exp 1116 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) β†’ (𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞)) β†’ ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝑅)) < 𝑦)))
161150, 160ralrimi 3252 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) β†’ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝑅)) < 𝑦))
162146, 147, 161syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝑅)) < 𝑦))
163132anim1i 613 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣) β†’ (𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣))
164163adantrl 714 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ (𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣))
1651643adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ (𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣))
166138breq1d 5162 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑀 = 𝑏 β†’ ((absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣 ↔ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣))
167137, 166anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑀 = 𝑏 β†’ ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) ↔ (𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)))
168167imbrov2fvoveq 7451 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑀 = 𝑏 β†’ (((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝑅)) < 𝑦) ↔ ((𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)))
169168rspcva 3609 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑏 ∈ (𝐴 ∩ (𝐡(,)+∞)) ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝑅)) < 𝑦)) β†’ ((𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))
170169imp 405 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑏 ∈ (𝐴 ∩ (𝐡(,)+∞)) ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ (𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)
171145, 162, 165, 170syl21anc 836 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)
172 rspe 3244 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏 ∈ 𝐴 ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))
173130, 144, 171, 172syl12anc 835 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))
1741733exp 1116 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) β†’ (𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) β†’ (((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))))
175127, 128, 174rexlimd 3261 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) β†’ (βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)))
176126, 175mpd 15 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))
1771763exp 1116 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (𝑣 ∈ ℝ+ β†’ (βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))))
178177rexlimdv 3150 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)))
17961, 178mpd 15 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))
1801793exp 1116 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑦 ∈ ℝ+) β†’ (𝑧 ∈ ℝ+ β†’ (βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))))
181180rexlimdv 3150 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑦 ∈ ℝ+) β†’ (βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)))
182181imp 405 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))
183182adantllr 717 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))
184183ad2antrr 724 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))
1853ad6antr 734 . . . . . . . . . . . . . . . . . . 19 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ 𝑅 ∈ β„‚)
1867ad6antr 734 . . . . . . . . . . . . . . . . . . 19 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ 𝐿 ∈ β„‚)
187185, 186subcld 11609 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (𝑅 βˆ’ 𝐿) ∈ β„‚)
188187abscld 15423 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) ∈ ℝ)
189 simp-6l 785 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ πœ‘)
190 simplr 767 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ 𝑏 ∈ 𝐴)
19136ffvelcdmda 7099 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑏 ∈ 𝐴) β†’ (πΉβ€˜π‘) ∈ β„‚)
192189, 190, 191syl2anc 582 . . . . . . . . . . . . . . . . . . . . . 22 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (πΉβ€˜π‘) ∈ β„‚)
193185, 192subcld 11609 . . . . . . . . . . . . . . . . . . . . 21 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (𝑅 βˆ’ (πΉβ€˜π‘)) ∈ β„‚)
194193abscld 15423 . . . . . . . . . . . . . . . . . . . 20 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜(𝑅 βˆ’ (πΉβ€˜π‘))) ∈ ℝ)
195 simp-6r 786 . . . . . . . . . . . . . . . . . . . . . 22 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ π‘₯ ∈ β„‚)
196192, 195subcld 11609 . . . . . . . . . . . . . . . . . . . . 21 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ ((πΉβ€˜π‘) βˆ’ π‘₯) ∈ β„‚)
197196abscld 15423 . . . . . . . . . . . . . . . . . . . 20 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) ∈ ℝ)
198194, 197readdcld 11281 . . . . . . . . . . . . . . . . . . 19 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ ((absβ€˜(𝑅 βˆ’ (πΉβ€˜π‘))) + (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯))) ∈ ℝ)
199 simp-4r 782 . . . . . . . . . . . . . . . . . . . . . 22 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ π‘Ž ∈ 𝐴)
20036ffvelcdmda 7099 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ (πΉβ€˜π‘Ž) ∈ β„‚)
201189, 199, 200syl2anc 582 . . . . . . . . . . . . . . . . . . . . 21 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (πΉβ€˜π‘Ž) ∈ β„‚)
202195, 201subcld 11609 . . . . . . . . . . . . . . . . . . . 20 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (π‘₯ βˆ’ (πΉβ€˜π‘Ž)) ∈ β„‚)
203202abscld 15423 . . . . . . . . . . . . . . . . . . 19 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜(π‘₯ βˆ’ (πΉβ€˜π‘Ž))) ∈ ℝ)
204198, 203readdcld 11281 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (((absβ€˜(𝑅 βˆ’ (πΉβ€˜π‘))) + (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯))) + (absβ€˜(π‘₯ βˆ’ (πΉβ€˜π‘Ž)))) ∈ ℝ)
205201, 186subcld 11609 . . . . . . . . . . . . . . . . . . 19 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ ((πΉβ€˜π‘Ž) βˆ’ 𝐿) ∈ β„‚)
206205abscld 15423 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) ∈ ℝ)
207204, 206readdcld 11281 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ ((((absβ€˜(𝑅 βˆ’ (πΉβ€˜π‘))) + (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯))) + (absβ€˜(π‘₯ βˆ’ (πΉβ€˜π‘Ž)))) + (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿))) ∈ ℝ)
20815a1i 11 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ 4 ∈ ℝ)
209 rpre 13022 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℝ+ β†’ 𝑦 ∈ ℝ)
210209ad5antlr 733 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ 𝑦 ∈ ℝ)
211208, 210remulcld 11282 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (4 Β· 𝑦) ∈ ℝ)
212185, 192, 195, 201, 186absnpncan3d 44718 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) ≀ ((((absβ€˜(𝑅 βˆ’ (πΉβ€˜π‘))) + (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯))) + (absβ€˜(π‘₯ βˆ’ (πΉβ€˜π‘Ž)))) + (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿))))
213185, 192abssubd 15440 . . . . . . . . . . . . . . . . . . 19 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜(𝑅 βˆ’ (πΉβ€˜π‘))) = (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)))
214 simprr 771 . . . . . . . . . . . . . . . . . . 19 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)
215213, 214eqbrtrd 5174 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜(𝑅 βˆ’ (πΉβ€˜π‘))) < 𝑦)
216 simprl 769 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦)
217 simp-5r 784 . . . . . . . . . . . . . . . . . . . . 21 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) β†’ π‘₯ ∈ β„‚)
218200ad5ant14 756 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) β†’ (πΉβ€˜π‘Ž) ∈ β„‚)
219218adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) β†’ (πΉβ€˜π‘Ž) ∈ β„‚)
220217, 219abssubd 15440 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) β†’ (absβ€˜(π‘₯ βˆ’ (πΉβ€˜π‘Ž))) = (absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)))
221 simplrl 775 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦)
222220, 221eqbrtrd 5174 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) β†’ (absβ€˜(π‘₯ βˆ’ (πΉβ€˜π‘Ž))) < 𝑦)
223222adantr 479 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜(π‘₯ βˆ’ (πΉβ€˜π‘Ž))) < 𝑦)
224 simplrr 776 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)
225224adantr 479 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)
226194, 197, 203, 206, 210, 215, 216, 223, 225lt4addmuld 44717 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ ((((absβ€˜(𝑅 βˆ’ (πΉβ€˜π‘))) + (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯))) + (absβ€˜(π‘₯ βˆ’ (πΉβ€˜π‘Ž)))) + (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿))) < (4 Β· 𝑦))
227188, 207, 211, 212, 226lelttrd 11410 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦))
228227ex 411 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) β†’ (((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦)))
229228adantl3r 748 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) β†’ (((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦)))
230229reximdva 3165 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) β†’ (βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦) β†’ βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦)))
231184, 230mpd 15 . . . . . . . . . . . 12 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) β†’ βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦))
232 fresin 6771 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:π΄βŸΆβ„‚ β†’ (𝐹 β†Ύ (-∞(,)𝐡)):(𝐴 ∩ (-∞(,)𝐡))βŸΆβ„‚)
23336, 232syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (𝐹 β†Ύ (-∞(,)𝐡)):(𝐴 ∩ (-∞(,)𝐡))βŸΆβ„‚)
234 ioosscn 13426 . . . . . . . . . . . . . . . . . . . . . . . 24 (-∞(,)𝐡) βŠ† β„‚
23546, 234sstri 3991 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐴 ∩ (-∞(,)𝐡)) βŠ† β„‚
236235a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (𝐴 ∩ (-∞(,)𝐡)) βŠ† β„‚)
237233, 236, 56ellimc3 25828 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝐿 ∈ ((𝐹 β†Ύ (-∞(,)𝐡)) limβ„‚ 𝐡) ↔ (𝐿 ∈ β„‚ ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦))))
2386, 237mpbid 231 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (𝐿 ∈ β„‚ ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)))
239238simprd 494 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦))
240239r19.21bi 3246 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑦 ∈ ℝ+) β†’ βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦))
2412403ad2ant1 1130 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦))
242 simp11l 1281 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) β†’ πœ‘)
243 simp12 1201 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) β†’ 𝑧 ∈ ℝ+)
244 simp2 1134 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) β†’ 𝑣 ∈ ℝ+)
245 breq2 5156 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑒 = if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑒 ↔ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)))
246245rexbidv 3176 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 = if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ (βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})(absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑒 ↔ βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})(absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)))
247 inss1 4231 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((limPtβ€˜πΎ)β€˜(𝐴 ∩ (-∞(,)𝐡))) ∩ ℝ) βŠ† ((limPtβ€˜πΎ)β€˜(𝐴 ∩ (-∞(,)𝐡)))
248247a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ (((limPtβ€˜πΎ)β€˜(𝐴 ∩ (-∞(,)𝐡))) ∩ ℝ) βŠ† ((limPtβ€˜πΎ)β€˜(𝐴 ∩ (-∞(,)𝐡))))
24948a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ (𝐴 ∩ (-∞(,)𝐡)) βŠ† ℝ)
25079, 81restlp 23107 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐾 ∈ Top ∧ ℝ βŠ† β„‚ ∧ (𝐴 ∩ (-∞(,)𝐡)) βŠ† ℝ) β†’ ((limPtβ€˜π½)β€˜(𝐴 ∩ (-∞(,)𝐡))) = (((limPtβ€˜πΎ)β€˜(𝐴 ∩ (-∞(,)𝐡))) ∩ ℝ))
25171, 73, 249, 250syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ ((limPtβ€˜π½)β€˜(𝐴 ∩ (-∞(,)𝐡))) = (((limPtβ€˜πΎ)β€˜(𝐴 ∩ (-∞(,)𝐡))) ∩ ℝ))
25285fveq1i 6903 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (-∞(,)𝐡))) = ((limPtβ€˜πΎ)β€˜(𝐴 ∩ (-∞(,)𝐡)))
253252a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (-∞(,)𝐡))) = ((limPtβ€˜πΎ)β€˜(𝐴 ∩ (-∞(,)𝐡))))
254248, 251, 2533sstr4d 4029 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ ((limPtβ€˜π½)β€˜(𝐴 ∩ (-∞(,)𝐡))) βŠ† ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (-∞(,)𝐡))))
255254, 54sseldd 3983 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 𝐡 ∈ ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (-∞(,)𝐡))))
256236, 56islpcn 45056 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ (𝐡 ∈ ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (-∞(,)𝐡))) ↔ βˆ€π‘’ ∈ ℝ+ βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})(absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑒))
257255, 256mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ βˆ€π‘’ ∈ ℝ+ βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})(absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑒)
2582573ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ βˆ€π‘’ ∈ ℝ+ βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})(absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑒)
259246, 258, 95rspcdva 3612 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})(absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣))
260 eldifi 4127 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) β†’ π‘Ž ∈ (𝐴 ∩ (-∞(,)𝐡)))
26148, 260sselid 3980 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) β†’ π‘Ž ∈ ℝ)
26273sselda 3982 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ π‘Ž ∈ β„‚)
26356adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ 𝐡 ∈ β„‚)
264262, 263subcld 11609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ (π‘Ž βˆ’ 𝐡) ∈ β„‚)
265264abscld 15423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ (absβ€˜(π‘Ž βˆ’ 𝐡)) ∈ ℝ)
2662653ad2antl1 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) β†’ (absβ€˜(π‘Ž βˆ’ 𝐡)) ∈ ℝ)
267266adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ (absβ€˜(π‘Ž βˆ’ 𝐡)) ∈ ℝ)
268105ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ∈ ℝ)
269108ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ 𝑧 ∈ ℝ)
270 simpr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣))
271114ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑧)
272267, 268, 269, 270, 271ltletrd 11412 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧)
273117ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ 𝑣 ∈ ℝ)
274 min2 13209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑣)
275107, 111, 274syl2an 594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑣)
2762753adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑣)
277276ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑣)
278267, 268, 273, 270, 277ltletrd 11412 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)
279272, 278jca 510 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣))
280279ex 411 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) β†’ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)))
281261, 280sylan2 591 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})) β†’ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)))
282281reximdva 3165 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ (βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})(absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)))
283259, 282mpd 15 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣))
284242, 243, 244, 283syl3anc 1368 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) β†’ βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣))
285 nfv 1909 . . . . . . . . . . . . . . . . . . . . 21 β„²π‘Ž(((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦))
286 nfre1 3280 . . . . . . . . . . . . . . . . . . . . 21 β„²π‘Žβˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)
287260elin1d 4200 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) β†’ π‘Ž ∈ 𝐴)
2882873ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ π‘Ž ∈ 𝐴)
289 simp113 1301 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦))
290 eldifsni 4798 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) β†’ π‘Ž β‰  𝐡)
291290adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ π‘Ž β‰  𝐡)
292 simprl 769 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧)
293291, 292jca 510 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ (π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧))
2942933adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ (π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧))
295 neeq1 3000 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑀 = π‘Ž β†’ (𝑀 β‰  𝐡 ↔ π‘Ž β‰  𝐡))
296 fvoveq1 7449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑀 = π‘Ž β†’ (absβ€˜(𝑀 βˆ’ 𝐡)) = (absβ€˜(π‘Ž βˆ’ 𝐡)))
297296breq1d 5162 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑀 = π‘Ž β†’ ((absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧 ↔ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧))
298295, 297anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑀 = π‘Ž β†’ ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) ↔ (π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧)))
299298imbrov2fvoveq 7451 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑀 = π‘Ž β†’ (((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦) ↔ ((π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦)))
300299rspcva 3609 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘Ž ∈ 𝐴 ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ ((π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦))
301300imp 405 . . . . . . . . . . . . . . . . . . . . . . . 24 (((π‘Ž ∈ 𝐴 ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ (π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧)) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦)
302288, 289, 294, 301syl21anc 836 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦)
3032603ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ π‘Ž ∈ (𝐴 ∩ (-∞(,)𝐡)))
3042423ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ πœ‘)
305 simp13 1202 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦))
306 nfra1 3279 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 β„²π‘€βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)
307148, 306nfan 1894 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ⅎ𝑀(πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦))
308 elinel2 4198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡)) β†’ 𝑀 ∈ (-∞(,)𝐡))
309308fvresd 6922 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡)) β†’ ((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) = (πΉβ€˜π‘€))
310309eqcomd 2734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡)) β†’ (πΉβ€˜π‘€) = ((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€))
311310fvoveq1d 7448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡)) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝐿)) = (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)))
3123113ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡)) ∧ (𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝐿)) = (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)))
313 rspa 3243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦) ∧ 𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡))) β†’ ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦))
3143133impia 1114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦) ∧ 𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡)) ∧ (𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)
3153143adant1l 1173 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡)) ∧ (𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)
316312, 315eqbrtrd 5174 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡)) ∧ (𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝐿)) < 𝑦)
3173163exp 1116 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) β†’ (𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡)) β†’ ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝐿)) < 𝑦)))
318307, 317ralrimi 3252 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) β†’ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝐿)) < 𝑦))
319304, 305, 318syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝐿)) < 𝑦))
320290anim1i 613 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣) β†’ (π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣))
321320adantrl 714 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ (π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣))
3223213adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ (π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣))
323296breq1d 5162 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑀 = π‘Ž β†’ ((absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣 ↔ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣))
324295, 323anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑀 = π‘Ž β†’ ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) ↔ (π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)))
325324imbrov2fvoveq 7451 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑀 = π‘Ž β†’ (((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝐿)) < 𝑦) ↔ ((π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)))
326325rspcva 3609 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘Ž ∈ (𝐴 ∩ (-∞(,)𝐡)) ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝐿)) < 𝑦)) β†’ ((π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))
327326imp 405 . . . . . . . . . . . . . . . . . . . . . . . 24 (((π‘Ž ∈ (𝐴 ∩ (-∞(,)𝐡)) ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ (π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)
328303, 319, 322, 327syl21anc 836 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)
329 rspe 3244 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘Ž ∈ 𝐴 ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))
330288, 302, 328, 329syl12anc 835 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))
3313303exp 1116 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) β†’ (π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) β†’ (((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))))
332285, 286, 331rexlimd 3261 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) β†’ (βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)))
333284, 332mpd 15 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))
3343333exp 1116 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (𝑣 ∈ ℝ+ β†’ (βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))))
335334rexlimdv 3150 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)))
336241, 335mpd 15 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))
3373363exp 1116 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑦 ∈ ℝ+) β†’ (𝑧 ∈ ℝ+ β†’ (βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))))
338337rexlimdv 3150 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑦 ∈ ℝ+) β†’ (βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)))
339338imp 405 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))
340339adantllr 717 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))
341231, 340reximddv3 3169 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦))
34232, 33, 35, 341syl21anc 836 . . . . . . . . . 10 ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦))
343342ex 411 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (𝑦 ∈ ℝ+ β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦)))
34424, 25, 31, 343vtoclf 3551 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) ∈ ℝ+ β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))))
34519, 344mpd 15 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)))
346 simpr 483 . . . . . . . . . . . 12 ((πœ‘ ∧ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)))
347 abssubrp 44686 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ β„‚ ∧ 𝐿 ∈ β„‚ ∧ 𝑅 β‰  𝐿) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) ∈ ℝ+)
3483, 7, 11, 347syl3anc 1368 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) ∈ ℝ+)
349348rpcnd 13058 . . . . . . . . . . . . . 14 (πœ‘ β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) ∈ β„‚)
350349adantr 479 . . . . . . . . . . . . 13 ((πœ‘ ∧ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) ∈ β„‚)
351 4cn 12335 . . . . . . . . . . . . . 14 4 ∈ β„‚
352351a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))) β†’ 4 ∈ β„‚)
353 4ne0 12358 . . . . . . . . . . . . . 14 4 β‰  0
354353a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))) β†’ 4 β‰  0)
355350, 352, 354divcan2d 12030 . . . . . . . . . . . 12 ((πœ‘ ∧ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))) β†’ (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)) = (absβ€˜(𝑅 βˆ’ 𝐿)))
356346, 355breqtrd 5178 . . . . . . . . . . 11 ((πœ‘ ∧ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (absβ€˜(𝑅 βˆ’ 𝐿)))
357356ex 411 . . . . . . . . . 10 (πœ‘ β†’ ((absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (absβ€˜(𝑅 βˆ’ 𝐿))))
358357a1d 25 . . . . . . . . 9 (πœ‘ β†’ ((π‘Ž ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) β†’ ((absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (absβ€˜(𝑅 βˆ’ 𝐿)))))
359358ad2antrr 724 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ ((π‘Ž ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) β†’ ((absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (absβ€˜(𝑅 βˆ’ 𝐿)))))
360359rexlimdvv 3208 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (absβ€˜(𝑅 βˆ’ 𝐿))))
361345, 360mpd 15 . . . . . 6 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (absβ€˜(𝑅 βˆ’ 𝐿)))
3629abscld 15423 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) ∈ ℝ)
363362ltnrd 11386 . . . . . 6 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ Β¬ (absβ€˜(𝑅 βˆ’ 𝐿)) < (absβ€˜(𝑅 βˆ’ 𝐿)))
364361, 363pm2.65da 815 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ β„‚) β†’ Β¬ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦))
365364ex 411 . . . 4 (πœ‘ β†’ (π‘₯ ∈ β„‚ β†’ Β¬ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)))
366 imnan 398 . . . 4 ((π‘₯ ∈ β„‚ β†’ Β¬ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ↔ Β¬ (π‘₯ ∈ β„‚ ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)))
367365, 366sylib 217 . . 3 (πœ‘ β†’ Β¬ (π‘₯ ∈ β„‚ ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)))
368 limclner.a . . . . 5 (πœ‘ β†’ 𝐴 βŠ† ℝ)
369368, 73sstrd 3992 . . . 4 (πœ‘ β†’ 𝐴 βŠ† β„‚)
37036, 369, 56ellimc3 25828 . . 3 (πœ‘ β†’ (π‘₯ ∈ (𝐹 limβ„‚ 𝐡) ↔ (π‘₯ ∈ β„‚ ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦))))
371367, 370mtbird 324 . 2 (πœ‘ β†’ Β¬ π‘₯ ∈ (𝐹 limβ„‚ 𝐡))
372371eq0rdv 4408 1 (πœ‘ β†’ (𝐹 limβ„‚ 𝐡) = βˆ…)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 394   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   β‰  wne 2937  βˆ€wral 3058  βˆƒwrex 3067   βˆ– cdif 3946   ∩ cin 3948   βŠ† wss 3949  βˆ…c0 4326  ifcif 4532  {csn 4632  βˆͺ cuni 4912   class class class wbr 5152  ran crn 5683   β†Ύ cres 5684  βŸΆwf 6549  β€˜cfv 6553  (class class class)co 7426  β„‚cc 11144  β„cr 11145  0cc0 11146   + caddc 11149   Β· cmul 11151  +∞cpnf 11283  -∞cmnf 11284   < clt 11286   ≀ cle 11287   βˆ’ cmin 11482   / cdiv 11909  4c4 12307  β„+crp 13014  (,)cioo 13364  abscabs 15221   β†Ύt crest 17409  TopOpenctopn 17410  topGenctg 17426  β„‚fldccnfld 21286  Topctop 22815  limPtclp 23058   limβ„‚ climc 25811
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-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11202  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223  ax-pre-sup 11224
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-rmo 3374  df-reu 3375  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-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-tp 4637  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-iin 5003  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  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-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  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-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7877  df-1st 7999  df-2nd 8000  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-1o 8493  df-er 8731  df-map 8853  df-pm 8854  df-en 8971  df-dom 8972  df-sdom 8973  df-fin 8974  df-fi 9442  df-sup 9473  df-inf 9474  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-div 11910  df-nn 12251  df-2 12313  df-3 12314  df-4 12315  df-5 12316  df-6 12317  df-7 12318  df-8 12319  df-9 12320  df-n0 12511  df-z 12597  df-dec 12716  df-uz 12861  df-q 12971  df-rp 13015  df-xneg 13132  df-xadd 13133  df-xmul 13134  df-ioo 13368  df-fz 13525  df-seq 14007  df-exp 14067  df-cj 15086  df-re 15087  df-im 15088  df-sqrt 15222  df-abs 15223  df-struct 17123  df-slot 17158  df-ndx 17170  df-base 17188  df-plusg 17253  df-mulr 17254  df-starv 17255  df-tset 17259  df-ple 17260  df-ds 17262  df-unif 17263  df-rest 17411  df-topn 17412  df-topgen 17432  df-psmet 21278  df-xmet 21279  df-met 21280  df-bl 21281  df-mopn 21282  df-cnfld 21287  df-top 22816  df-topon 22833  df-topsp 22855  df-bases 22869  df-cld 22943  df-ntr 22944  df-cls 22945  df-nei 23022  df-lp 23060  df-cnp 23152  df-xms 24246  df-ms 24247  df-limc 25815
This theorem is referenced by:  limclr  45072  jumpncnp  45315
  Copyright terms: Public domain W3C validator