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 44921
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 25754 . . . . . . . . . . . . 13 ((𝐹 β†Ύ (𝐡(,)+∞)) limβ„‚ 𝐡) βŠ† β„‚
2 limclner.r . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑅 ∈ ((𝐹 β†Ύ (𝐡(,)+∞)) limβ„‚ 𝐡))
31, 2sselid 3975 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑅 ∈ β„‚)
43ad2antrr 723 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ 𝑅 ∈ β„‚)
5 limccl 25754 . . . . . . . . . . . . 13 ((𝐹 β†Ύ (-∞(,)𝐡)) limβ„‚ 𝐡) βŠ† β„‚
6 limclner.l . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐿 ∈ ((𝐹 β†Ύ (-∞(,)𝐡)) limβ„‚ 𝐡))
75, 6sselid 3975 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐿 ∈ β„‚)
87ad2antrr 723 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ 𝐿 ∈ β„‚)
94, 8subcld 11572 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (𝑅 βˆ’ 𝐿) ∈ β„‚)
10 limclner.lner . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐿 β‰  𝑅)
1110necomd 2990 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑅 β‰  𝐿)
1211ad2antrr 723 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ 𝑅 β‰  𝐿)
134, 8, 12subne0d 11581 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (𝑅 βˆ’ 𝐿) β‰  0)
149, 13absrpcld 15398 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) ∈ ℝ+)
15 4re 12297 . . . . . . . . . . 11 4 ∈ ℝ
16 4pos 12320 . . . . . . . . . . 11 0 < 4
1715, 16elrpii 12980 . . . . . . . . . 10 4 ∈ ℝ+
1817a1i 11 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ 4 ∈ ℝ+)
1914, 18rpdivcld 13036 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) ∈ ℝ+)
20 nfv 1909 . . . . . . . . . . 11 Ⅎ𝑦(πœ‘ ∧ π‘₯ ∈ β„‚)
21 nfra1 3275 . . . . . . . . . . 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 7437 . . . . . . . . 9 ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) ∈ V
26 eleq1 2815 . . . . . . . . . . 11 (𝑦 = ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) β†’ (𝑦 ∈ ℝ+ ↔ ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) ∈ ℝ+))
27 oveq2 7412 . . . . . . . . . . . . 13 (𝑦 = ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) β†’ (4 Β· 𝑦) = (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)))
2827breq2d 5153 . . . . . . . . . . . 12 (𝑦 = ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) β†’ ((absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦) ↔ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))))
29282rexbidv 3213 . . . . . . . . . . 11 (𝑦 = ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) β†’ (βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦) ↔ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))))
3026, 29imbi12d 344 . . . . . . . . . 10 (𝑦 = ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) β†’ ((𝑦 ∈ ℝ+ β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦)) ↔ (((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) ∈ ℝ+ β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)))))
3130imbi2d 340 . . . . . . . . 9 (𝑦 = ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) β†’ ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (𝑦 ∈ ℝ+ β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦))) ↔ (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) ∈ ℝ+ β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))))))
32 simpll 764 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) β†’ (πœ‘ ∧ π‘₯ ∈ β„‚))
33 simpr 484 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) β†’ 𝑦 ∈ ℝ+)
34 rspa 3239 . . . . . . . . . . . 12 ((βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦) ∧ 𝑦 ∈ ℝ+) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦))
3534adantll 711 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦))
36 limclner.f . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 𝐹:π΄βŸΆβ„‚)
37 fresin 6753 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹:π΄βŸΆβ„‚ β†’ (𝐹 β†Ύ (𝐡(,)+∞)):(𝐴 ∩ (𝐡(,)+∞))βŸΆβ„‚)
3836, 37syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (𝐹 β†Ύ (𝐡(,)+∞)):(𝐴 ∩ (𝐡(,)+∞))βŸΆβ„‚)
39 inss2 4224 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 ∩ (𝐡(,)+∞)) βŠ† (𝐡(,)+∞)
40 ioosscn 13389 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐡(,)+∞) βŠ† β„‚
4139, 40sstri 3986 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∩ (𝐡(,)+∞)) βŠ† β„‚
4241a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (𝐴 ∩ (𝐡(,)+∞)) βŠ† β„‚)
43 limclner.j . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝐽 = (topGenβ€˜ran (,))
44 retop 24628 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (topGenβ€˜ran (,)) ∈ Top
4543, 44eqeltri 2823 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝐽 ∈ Top
46 inss2 4224 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐴 ∩ (-∞(,)𝐡)) βŠ† (-∞(,)𝐡)
47 ioossre 13388 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (-∞(,)𝐡) βŠ† ℝ
4846, 47sstri 3986 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐴 ∩ (-∞(,)𝐡)) βŠ† ℝ
49 uniretop 24629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ℝ = βˆͺ (topGenβ€˜ran (,))
5043unieqi 4914 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 βˆͺ 𝐽 = βˆͺ (topGenβ€˜ran (,))
5149, 50eqtr4i 2757 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ℝ = βˆͺ 𝐽
5251lpss 22996 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐽 ∈ Top ∧ (𝐴 ∩ (-∞(,)𝐡)) βŠ† ℝ) β†’ ((limPtβ€˜π½)β€˜(𝐴 ∩ (-∞(,)𝐡))) βŠ† ℝ)
5345, 48, 52mp2an 689 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((limPtβ€˜π½)β€˜(𝐴 ∩ (-∞(,)𝐡))) βŠ† ℝ
54 limclner.blp1 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ 𝐡 ∈ ((limPtβ€˜π½)β€˜(𝐴 ∩ (-∞(,)𝐡))))
5553, 54sselid 3975 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 𝐡 ∈ ℝ)
5655recnd 11243 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 𝐡 ∈ β„‚)
5738, 42, 56ellimc3 25758 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (𝑅 ∈ ((𝐹 β†Ύ (𝐡(,)+∞)) limβ„‚ 𝐡) ↔ (𝑅 ∈ β„‚ ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦))))
582, 57mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (𝑅 ∈ β„‚ ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)))
5958simprd 495 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦))
6059r19.21bi 3242 . . . . . . . . . . . . . . . . . . . 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 5145 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑒 = if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑒 ↔ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)))
6665rexbidv 3172 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑒 = if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ (βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})(absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑒 ↔ βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})(absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)))
67 inss1 4223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((limPtβ€˜πΎ)β€˜(𝐴 ∩ (𝐡(,)+∞))) ∩ ℝ) βŠ† ((limPtβ€˜πΎ)β€˜(𝐴 ∩ (𝐡(,)+∞)))
6867a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (πœ‘ β†’ (((limPtβ€˜πΎ)β€˜(𝐴 ∩ (𝐡(,)+∞))) ∩ ℝ) βŠ† ((limPtβ€˜πΎ)β€˜(𝐴 ∩ (𝐡(,)+∞))))
69 limclner.k . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝐾 = (TopOpenβ€˜β„‚fld)
7069cnfldtop 24650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝐾 ∈ Top
7170a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (πœ‘ β†’ 𝐾 ∈ Top)
72 ax-resscn 11166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ℝ βŠ† β„‚
7372a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (πœ‘ β†’ ℝ βŠ† β„‚)
74 ioossre 13388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐡(,)+∞) βŠ† ℝ
7539, 74sstri 3986 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐴 ∩ (𝐡(,)+∞)) βŠ† ℝ
7675a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (πœ‘ β†’ (𝐴 ∩ (𝐡(,)+∞)) βŠ† ℝ)
77 unicntop 24652 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 β„‚ = βˆͺ (TopOpenβ€˜β„‚fld)
7869unieqi 4914 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 βˆͺ 𝐾 = βˆͺ (TopOpenβ€˜β„‚fld)
7977, 78eqtr4i 2757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 β„‚ = βˆͺ 𝐾
8069tgioo2 24669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (topGenβ€˜ran (,)) = (𝐾 β†Ύt ℝ)
8143, 80eqtri 2754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝐽 = (𝐾 β†Ύt ℝ)
8279, 81restlp 23037 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐾 ∈ Top ∧ ℝ βŠ† β„‚ ∧ (𝐴 ∩ (𝐡(,)+∞)) βŠ† ℝ) β†’ ((limPtβ€˜π½)β€˜(𝐴 ∩ (𝐡(,)+∞))) = (((limPtβ€˜πΎ)β€˜(𝐴 ∩ (𝐡(,)+∞))) ∩ ℝ))
8371, 73, 76, 82syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (πœ‘ β†’ ((limPtβ€˜π½)β€˜(𝐴 ∩ (𝐡(,)+∞))) = (((limPtβ€˜πΎ)β€˜(𝐴 ∩ (𝐡(,)+∞))) ∩ ℝ))
8469eqcomi 2735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (TopOpenβ€˜β„‚fld) = 𝐾
8584fveq2i 6887 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (limPtβ€˜(TopOpenβ€˜β„‚fld)) = (limPtβ€˜πΎ)
8685fveq1i 6885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (𝐡(,)+∞))) = ((limPtβ€˜πΎ)β€˜(𝐴 ∩ (𝐡(,)+∞)))
8786a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (πœ‘ β†’ ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (𝐡(,)+∞))) = ((limPtβ€˜πΎ)β€˜(𝐴 ∩ (𝐡(,)+∞))))
8868, 83, 873sstr4d 4024 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ ((limPtβ€˜π½)β€˜(𝐴 ∩ (𝐡(,)+∞))) βŠ† ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (𝐡(,)+∞))))
89 limclner.blp2 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ 𝐡 ∈ ((limPtβ€˜π½)β€˜(𝐴 ∩ (𝐡(,)+∞))))
9088, 89sseldd 3978 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ 𝐡 ∈ ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (𝐡(,)+∞))))
9142, 56islpcn 44909 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ (𝐡 ∈ ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (𝐡(,)+∞))) ↔ βˆ€π‘’ ∈ ℝ+ βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})(absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑒))
9290, 91mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ βˆ€π‘’ ∈ ℝ+ βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})(absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑒)
93923ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ βˆ€π‘’ ∈ ℝ+ βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})(absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑒)
94 ifcl 4568 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ∈ ℝ+)
95943adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ∈ ℝ+)
9666, 93, 95rspcdva 3607 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ βˆƒπ‘ ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})(absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣))
97 eldifi 4121 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) β†’ 𝑏 ∈ (𝐴 ∩ (𝐡(,)+∞)))
9875, 97sselid 3975 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) β†’ 𝑏 ∈ ℝ)
9973sselda 3977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((πœ‘ ∧ 𝑏 ∈ ℝ) β†’ 𝑏 ∈ β„‚)
10056adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((πœ‘ ∧ 𝑏 ∈ ℝ) β†’ 𝐡 ∈ β„‚)
10199, 100subcld 11572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((πœ‘ ∧ 𝑏 ∈ ℝ) β†’ (𝑏 βˆ’ 𝐡) ∈ β„‚)
102101abscld 15386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((πœ‘ ∧ 𝑏 ∈ ℝ) β†’ (absβ€˜(𝑏 βˆ’ 𝐡)) ∈ ℝ)
1031023ad2antl1 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) β†’ (absβ€˜(𝑏 βˆ’ 𝐡)) ∈ ℝ)
104103adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ (absβ€˜(𝑏 βˆ’ 𝐡)) ∈ ℝ)
10595rpred 13019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ∈ ℝ)
106105ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ∈ ℝ)
107 rpre 12985 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 ∈ ℝ+ β†’ 𝑧 ∈ ℝ)
1081073ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ 𝑧 ∈ ℝ)
109108ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ 𝑧 ∈ ℝ)
110 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣))
111 rpre 12985 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑣 ∈ ℝ+ β†’ 𝑣 ∈ ℝ)
112 min1 13171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑧)
113107, 111, 112syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑧)
1141133adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑧)
115114ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑧)
116104, 106, 109, 110, 115ltletrd 11375 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧)
1171113ad2ant3 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ 𝑣 ∈ ℝ)
118117ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ 𝑣 ∈ ℝ)
119109, 118min2d 44737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑣)
120104, 106, 118, 110, 119ltletrd 11375 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)
121116, 120jca 511 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣))
122121ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ℝ) β†’ ((absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)))
12398, 122sylan2 592 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡})) β†’ ((absβ€˜(𝑏 βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)))
124123reximdva 3162 . . . . . . . . . . . . . . . . . . . . . . . 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 3276 . . . . . . . . . . . . . . . . . . . . . . 23 β„²π‘βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)
12997elin1d 4193 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) β†’ 𝑏 ∈ 𝐴)
1301293ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ 𝑏 ∈ 𝐴)
131 simp113 1301 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦))
132 eldifsni 4788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) β†’ 𝑏 β‰  𝐡)
133132adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ 𝑏 β‰  𝐡)
134 simprl 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧)
135133, 134jca 511 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ (𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧))
1361353adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ (𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧))
137 neeq1 2997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑀 = 𝑏 β†’ (𝑀 β‰  𝐡 ↔ 𝑏 β‰  𝐡))
138 fvoveq1 7427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑀 = 𝑏 β†’ (absβ€˜(𝑀 βˆ’ 𝐡)) = (absβ€˜(𝑏 βˆ’ 𝐡)))
139138breq1d 5151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑀 = 𝑏 β†’ ((absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧 ↔ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧))
140137, 139anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑀 = 𝑏 β†’ ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) ↔ (𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧)))
141140imbrov2fvoveq 7429 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑀 = 𝑏 β†’ (((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦) ↔ ((𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦)))
142141rspcva 3604 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑏 ∈ 𝐴 ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ ((𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦))
143142imp 406 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑏 ∈ 𝐴 ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ (𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧)) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦)
144130, 131, 136, 143syl21anc 835 . . . . . . . . . . . . . . . . . . . . . . . . 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 3275 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 β„²π‘€βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)
150148, 149nfan 1894 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Ⅎ𝑀(πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦))
151 elinel2 4191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞)) β†’ 𝑀 ∈ (𝐡(,)+∞))
152151fvresd 6904 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞)) β†’ ((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) = (πΉβ€˜π‘€))
153152eqcomd 2732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞)) β†’ (πΉβ€˜π‘€) = ((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€))
154153fvoveq1d 7426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞)) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝑅)) = (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)))
1551543ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞)) ∧ (𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝑅)) = (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)))
156 rspa 3239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦) ∧ 𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞))) β†’ ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦))
1571563impia 1114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦) ∧ 𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞)) ∧ (𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)
1581573adant1l 1173 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞)) ∧ (𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)
159155, 158eqbrtrd 5163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞)) ∧ (𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝑅)) < 𝑦)
1601593exp 1116 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) β†’ (𝑀 ∈ (𝐴 ∩ (𝐡(,)+∞)) β†’ ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝑅)) < 𝑦)))
161150, 160ralrimi 3248 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) β†’ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝑅)) < 𝑦))
162146, 147, 161syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝑅)) < 𝑦))
163132anim1i 614 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣) β†’ (𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣))
164163adantrl 713 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ (𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣))
1651643adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ (𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣))
166138breq1d 5151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑀 = 𝑏 β†’ ((absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣 ↔ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣))
167137, 166anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑀 = 𝑏 β†’ ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) ↔ (𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)))
168167imbrov2fvoveq 7429 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑀 = 𝑏 β†’ (((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝑅)) < 𝑦) ↔ ((𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)))
169168rspcva 3604 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑏 ∈ (𝐴 ∩ (𝐡(,)+∞)) ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝑅)) < 𝑦)) β†’ ((𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))
170169imp 406 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑏 ∈ (𝐴 ∩ (𝐡(,)+∞)) ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ (𝑏 β‰  𝐡 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)
171145, 162, 165, 170syl21anc 835 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)
172 rspe 3240 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑏 ∈ 𝐴 ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))
173130, 144, 171, 172syl12anc 834 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) ∧ 𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) ∧ ((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣)) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))
1741733exp 1116 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦)) β†’ (𝑏 ∈ ((𝐴 ∩ (𝐡(,)+∞)) βˆ– {𝐡}) β†’ (((absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(𝑏 βˆ’ 𝐡)) < 𝑣) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))))
175127, 128, 174rexlimd 3257 . . . . . . . . . . . . . . . . . . . . . 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 3147 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (𝐡(,)+∞))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (𝐡(,)+∞))β€˜π‘€) βˆ’ 𝑅)) < 𝑦) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)))
17961, 178mpd 15 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))
1801793exp 1116 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑦 ∈ ℝ+) β†’ (𝑧 ∈ ℝ+ β†’ (βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))))
181180rexlimdv 3147 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑦 ∈ ℝ+) β†’ (βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)))
182181imp 406 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))
183182adantllr 716 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))
184183ad2antrr 723 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) β†’ βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦))
1853ad6antr 733 . . . . . . . . . . . . . . . . . . 19 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ 𝑅 ∈ β„‚)
1867ad6antr 733 . . . . . . . . . . . . . . . . . . 19 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ 𝐿 ∈ β„‚)
187185, 186subcld 11572 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (𝑅 βˆ’ 𝐿) ∈ β„‚)
188187abscld 15386 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) ∈ ℝ)
189 simp-6l 784 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ πœ‘)
190 simplr 766 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ 𝑏 ∈ 𝐴)
19136ffvelcdmda 7079 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑏 ∈ 𝐴) β†’ (πΉβ€˜π‘) ∈ β„‚)
192189, 190, 191syl2anc 583 . . . . . . . . . . . . . . . . . . . . . 22 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (πΉβ€˜π‘) ∈ β„‚)
193185, 192subcld 11572 . . . . . . . . . . . . . . . . . . . . 21 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (𝑅 βˆ’ (πΉβ€˜π‘)) ∈ β„‚)
194193abscld 15386 . . . . . . . . . . . . . . . . . . . 20 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜(𝑅 βˆ’ (πΉβ€˜π‘))) ∈ ℝ)
195 simp-6r 785 . . . . . . . . . . . . . . . . . . . . . 22 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ π‘₯ ∈ β„‚)
196192, 195subcld 11572 . . . . . . . . . . . . . . . . . . . . 21 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ ((πΉβ€˜π‘) βˆ’ π‘₯) ∈ β„‚)
197196abscld 15386 . . . . . . . . . . . . . . . . . . . 20 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) ∈ ℝ)
198194, 197readdcld 11244 . . . . . . . . . . . . . . . . . . 19 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ ((absβ€˜(𝑅 βˆ’ (πΉβ€˜π‘))) + (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯))) ∈ ℝ)
199 simp-4r 781 . . . . . . . . . . . . . . . . . . . . . 22 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ π‘Ž ∈ 𝐴)
20036ffvelcdmda 7079 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘Ž ∈ 𝐴) β†’ (πΉβ€˜π‘Ž) ∈ β„‚)
201189, 199, 200syl2anc 583 . . . . . . . . . . . . . . . . . . . . 21 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (πΉβ€˜π‘Ž) ∈ β„‚)
202195, 201subcld 11572 . . . . . . . . . . . . . . . . . . . 20 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (π‘₯ βˆ’ (πΉβ€˜π‘Ž)) ∈ β„‚)
203202abscld 15386 . . . . . . . . . . . . . . . . . . 19 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜(π‘₯ βˆ’ (πΉβ€˜π‘Ž))) ∈ ℝ)
204198, 203readdcld 11244 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (((absβ€˜(𝑅 βˆ’ (πΉβ€˜π‘))) + (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯))) + (absβ€˜(π‘₯ βˆ’ (πΉβ€˜π‘Ž)))) ∈ ℝ)
205201, 186subcld 11572 . . . . . . . . . . . . . . . . . . 19 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ ((πΉβ€˜π‘Ž) βˆ’ 𝐿) ∈ β„‚)
206205abscld 15386 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) ∈ ℝ)
207204, 206readdcld 11244 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ ((((absβ€˜(𝑅 βˆ’ (πΉβ€˜π‘))) + (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯))) + (absβ€˜(π‘₯ βˆ’ (πΉβ€˜π‘Ž)))) + (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿))) ∈ ℝ)
20815a1i 11 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ 4 ∈ ℝ)
209 rpre 12985 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℝ+ β†’ 𝑦 ∈ ℝ)
210209ad5antlr 732 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ 𝑦 ∈ ℝ)
211208, 210remulcld 11245 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (4 Β· 𝑦) ∈ ℝ)
212185, 192, 195, 201, 186absnpncan3d 44571 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) ≀ ((((absβ€˜(𝑅 βˆ’ (πΉβ€˜π‘))) + (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯))) + (absβ€˜(π‘₯ βˆ’ (πΉβ€˜π‘Ž)))) + (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿))))
213185, 192abssubd 15403 . . . . . . . . . . . . . . . . . . 19 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜(𝑅 βˆ’ (πΉβ€˜π‘))) = (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)))
214 simprr 770 . . . . . . . . . . . . . . . . . . 19 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)
215213, 214eqbrtrd 5163 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜(𝑅 βˆ’ (πΉβ€˜π‘))) < 𝑦)
216 simprl 768 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦)
217 simp-5r 783 . . . . . . . . . . . . . . . . . . . . 21 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) β†’ π‘₯ ∈ β„‚)
218200ad5ant14 755 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) β†’ (πΉβ€˜π‘Ž) ∈ β„‚)
219218adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) β†’ (πΉβ€˜π‘Ž) ∈ β„‚)
220217, 219abssubd 15403 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) β†’ (absβ€˜(π‘₯ βˆ’ (πΉβ€˜π‘Ž))) = (absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)))
221 simplrl 774 . . . . . . . . . . . . . . . . . . . 20 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦)
222220, 221eqbrtrd 5163 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) β†’ (absβ€˜(π‘₯ βˆ’ (πΉβ€˜π‘Ž))) < 𝑦)
223222adantr 480 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜(π‘₯ βˆ’ (πΉβ€˜π‘Ž))) < 𝑦)
224 simplrr 775 . . . . . . . . . . . . . . . . . . 19 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)
225224adantr 480 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)
226194, 197, 203, 206, 210, 215, 216, 223, 225lt4addmuld 44570 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ ((((absβ€˜(𝑅 βˆ’ (πΉβ€˜π‘))) + (absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯))) + (absβ€˜(π‘₯ βˆ’ (πΉβ€˜π‘Ž)))) + (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿))) < (4 Β· 𝑦))
227188, 207, 211, 212, 226lelttrd 11373 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦))
228227ex 412 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) β†’ (((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦)))
229228adantl3r 747 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑏 ∈ 𝐴) β†’ (((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦)))
230229reximdva 3162 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) β†’ (βˆƒπ‘ ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘) βˆ’ 𝑅)) < 𝑦) β†’ βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦)))
231184, 230mpd 15 . . . . . . . . . . . 12 ((((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ π‘Ž ∈ 𝐴) ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) β†’ βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦))
232 fresin 6753 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:π΄βŸΆβ„‚ β†’ (𝐹 β†Ύ (-∞(,)𝐡)):(𝐴 ∩ (-∞(,)𝐡))βŸΆβ„‚)
23336, 232syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (𝐹 β†Ύ (-∞(,)𝐡)):(𝐴 ∩ (-∞(,)𝐡))βŸΆβ„‚)
234 ioosscn 13389 . . . . . . . . . . . . . . . . . . . . . . . 24 (-∞(,)𝐡) βŠ† β„‚
23546, 234sstri 3986 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐴 ∩ (-∞(,)𝐡)) βŠ† β„‚
236235a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (𝐴 ∩ (-∞(,)𝐡)) βŠ† β„‚)
237233, 236, 56ellimc3 25758 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝐿 ∈ ((𝐹 β†Ύ (-∞(,)𝐡)) limβ„‚ 𝐡) ↔ (𝐿 ∈ β„‚ ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦))))
2386, 237mpbid 231 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (𝐿 ∈ β„‚ ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)))
239238simprd 495 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦))
240239r19.21bi 3242 . . . . . . . . . . . . . . . . . 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 5145 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑒 = if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑒 ↔ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)))
246245rexbidv 3172 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 = if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ (βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})(absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑒 ↔ βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})(absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)))
247 inss1 4223 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((limPtβ€˜πΎ)β€˜(𝐴 ∩ (-∞(,)𝐡))) ∩ ℝ) βŠ† ((limPtβ€˜πΎ)β€˜(𝐴 ∩ (-∞(,)𝐡)))
248247a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ (((limPtβ€˜πΎ)β€˜(𝐴 ∩ (-∞(,)𝐡))) ∩ ℝ) βŠ† ((limPtβ€˜πΎ)β€˜(𝐴 ∩ (-∞(,)𝐡))))
24948a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ (𝐴 ∩ (-∞(,)𝐡)) βŠ† ℝ)
25079, 81restlp 23037 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐾 ∈ Top ∧ ℝ βŠ† β„‚ ∧ (𝐴 ∩ (-∞(,)𝐡)) βŠ† ℝ) β†’ ((limPtβ€˜π½)β€˜(𝐴 ∩ (-∞(,)𝐡))) = (((limPtβ€˜πΎ)β€˜(𝐴 ∩ (-∞(,)𝐡))) ∩ ℝ))
25171, 73, 249, 250syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ ((limPtβ€˜π½)β€˜(𝐴 ∩ (-∞(,)𝐡))) = (((limPtβ€˜πΎ)β€˜(𝐴 ∩ (-∞(,)𝐡))) ∩ ℝ))
25285fveq1i 6885 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (-∞(,)𝐡))) = ((limPtβ€˜πΎ)β€˜(𝐴 ∩ (-∞(,)𝐡)))
253252a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (-∞(,)𝐡))) = ((limPtβ€˜πΎ)β€˜(𝐴 ∩ (-∞(,)𝐡))))
254248, 251, 2533sstr4d 4024 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ ((limPtβ€˜π½)β€˜(𝐴 ∩ (-∞(,)𝐡))) βŠ† ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (-∞(,)𝐡))))
255254, 54sseldd 3978 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 𝐡 ∈ ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (-∞(,)𝐡))))
256236, 56islpcn 44909 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ (𝐡 ∈ ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(𝐴 ∩ (-∞(,)𝐡))) ↔ βˆ€π‘’ ∈ ℝ+ βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})(absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑒))
257255, 256mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ βˆ€π‘’ ∈ ℝ+ βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})(absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑒)
2582573ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ βˆ€π‘’ ∈ ℝ+ βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})(absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑒)
259246, 258, 95rspcdva 3607 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ βˆƒπ‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})(absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣))
260 eldifi 4121 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) β†’ π‘Ž ∈ (𝐴 ∩ (-∞(,)𝐡)))
26148, 260sselid 3975 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) β†’ π‘Ž ∈ ℝ)
26273sselda 3977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ π‘Ž ∈ β„‚)
26356adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ 𝐡 ∈ β„‚)
264262, 263subcld 11572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ (π‘Ž βˆ’ 𝐡) ∈ β„‚)
265264abscld 15386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ (absβ€˜(π‘Ž βˆ’ 𝐡)) ∈ ℝ)
2662653ad2antl1 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) β†’ (absβ€˜(π‘Ž βˆ’ 𝐡)) ∈ ℝ)
267266adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ (absβ€˜(π‘Ž βˆ’ 𝐡)) ∈ ℝ)
268105ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ∈ ℝ)
269108ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ 𝑧 ∈ ℝ)
270 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣))
271114ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑧)
272267, 268, 269, 270, 271ltletrd 11375 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧)
273117ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ 𝑣 ∈ ℝ)
274 min2 13172 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑣)
275107, 111, 274syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑣)
2762753adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑣)
277276ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ if(𝑧 ≀ 𝑣, 𝑧, 𝑣) ≀ 𝑣)
278267, 268, 273, 270, 277ltletrd 11375 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)
279272, 278jca 511 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣)) β†’ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣))
280279ex 412 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ℝ) β†’ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)))
281261, 280sylan2 592 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑧 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡})) β†’ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < if(𝑧 ≀ 𝑣, 𝑧, 𝑣) β†’ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)))
282281reximdva 3162 . . . . . . . . . . . . . . . . . . . . . 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 3276 . . . . . . . . . . . . . . . . . . . . 21 β„²π‘Žβˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)
287260elin1d 4193 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) β†’ π‘Ž ∈ 𝐴)
2882873ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ π‘Ž ∈ 𝐴)
289 simp113 1301 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦))
290 eldifsni 4788 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) β†’ π‘Ž β‰  𝐡)
291290adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ π‘Ž β‰  𝐡)
292 simprl 768 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧)
293291, 292jca 511 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ (π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧))
2942933adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ (π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧))
295 neeq1 2997 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑀 = π‘Ž β†’ (𝑀 β‰  𝐡 ↔ π‘Ž β‰  𝐡))
296 fvoveq1 7427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑀 = π‘Ž β†’ (absβ€˜(𝑀 βˆ’ 𝐡)) = (absβ€˜(π‘Ž βˆ’ 𝐡)))
297296breq1d 5151 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑀 = π‘Ž β†’ ((absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧 ↔ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧))
298295, 297anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑀 = π‘Ž β†’ ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) ↔ (π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧)))
299298imbrov2fvoveq 7429 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑀 = π‘Ž β†’ (((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦) ↔ ((π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦)))
300299rspcva 3604 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘Ž ∈ 𝐴 ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ ((π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦))
301300imp 406 . . . . . . . . . . . . . . . . . . . . . . . 24 (((π‘Ž ∈ 𝐴 ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ (π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧)) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦)
302288, 289, 294, 301syl21anc 835 . . . . . . . . . . . . . . . . . . . . . . 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 3275 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 β„²π‘€βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)
307148, 306nfan 1894 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ⅎ𝑀(πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦))
308 elinel2 4191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡)) β†’ 𝑀 ∈ (-∞(,)𝐡))
309308fvresd 6904 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡)) β†’ ((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) = (πΉβ€˜π‘€))
310309eqcomd 2732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡)) β†’ (πΉβ€˜π‘€) = ((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€))
311310fvoveq1d 7426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡)) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝐿)) = (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)))
3123113ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡)) ∧ (𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝐿)) = (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)))
313 rspa 3239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦) ∧ 𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡))) β†’ ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦))
3143133impia 1114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦) ∧ 𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡)) ∧ (𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)
3153143adant1l 1173 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡)) ∧ (𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)
316312, 315eqbrtrd 5163 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ 𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡)) ∧ (𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝐿)) < 𝑦)
3173163exp 1116 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) β†’ (𝑀 ∈ (𝐴 ∩ (-∞(,)𝐡)) β†’ ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝐿)) < 𝑦)))
318307, 317ralrimi 3248 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) β†’ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝐿)) < 𝑦))
319304, 305, 318syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝐿)) < 𝑦))
320290anim1i 614 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣) β†’ (π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣))
321320adantrl 713 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ (π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣))
3223213adant1 1127 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ (π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣))
323296breq1d 5151 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑀 = π‘Ž β†’ ((absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣 ↔ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣))
324295, 323anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑀 = π‘Ž β†’ ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) ↔ (π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)))
325324imbrov2fvoveq 7429 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑀 = π‘Ž β†’ (((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝐿)) < 𝑦) ↔ ((π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)))
326325rspcva 3604 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘Ž ∈ (𝐴 ∩ (-∞(,)𝐡)) ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝐿)) < 𝑦)) β†’ ((π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))
327326imp 406 . . . . . . . . . . . . . . . . . . . . . . . 24 (((π‘Ž ∈ (𝐴 ∩ (-∞(,)𝐡)) ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ (π‘Ž β‰  𝐡 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)
328303, 319, 322, 327syl21anc 835 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)
329 rspe 3240 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘Ž ∈ 𝐴 ∧ ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))
330288, 302, 328, 329syl12anc 834 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) ∧ π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) ∧ ((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣)) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))
3313303exp 1116 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑣 ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦)) β†’ (π‘Ž ∈ ((𝐴 ∩ (-∞(,)𝐡)) βˆ– {𝐡}) β†’ (((absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑧 ∧ (absβ€˜(π‘Ž βˆ’ 𝐡)) < 𝑣) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))))
332285, 286, 331rexlimd 3257 . . . . . . . . . . . . . . . . . . . 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 3147 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (βˆƒπ‘£ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴 ∩ (-∞(,)𝐡))((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑣) β†’ (absβ€˜(((𝐹 β†Ύ (-∞(,)𝐡))β€˜π‘€) βˆ’ 𝐿)) < 𝑦) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)))
336241, 335mpd 15 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+ ∧ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))
3373363exp 1116 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑦 ∈ ℝ+) β†’ (𝑧 ∈ ℝ+ β†’ (βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))))
338337rexlimdv 3147 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑦 ∈ ℝ+) β†’ (βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦)))
339338imp 406 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))
340339adantllr 716 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘Ž ∈ 𝐴 ((absβ€˜((πΉβ€˜π‘Ž) βˆ’ π‘₯)) < 𝑦 ∧ (absβ€˜((πΉβ€˜π‘Ž) βˆ’ 𝐿)) < 𝑦))
341231, 340reximddv3 44397 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ 𝑦 ∈ ℝ+) ∧ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦))
34232, 33, 35, 341syl21anc 835 . . . . . . . . . 10 ((((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ∧ 𝑦 ∈ ℝ+) β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦))
343342ex 412 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (𝑦 ∈ ℝ+ β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· 𝑦)))
34424, 25, 31, 343vtoclf 3546 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (((absβ€˜(𝑅 βˆ’ 𝐿)) / 4) ∈ ℝ+ β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))))
34519, 344mpd 15 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)))
346 simpr 484 . . . . . . . . . . . 12 ((πœ‘ ∧ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)))
347 abssubrp 44539 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ β„‚ ∧ 𝐿 ∈ β„‚ ∧ 𝑅 β‰  𝐿) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) ∈ ℝ+)
3483, 7, 11, 347syl3anc 1368 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) ∈ ℝ+)
349348rpcnd 13021 . . . . . . . . . . . . . 14 (πœ‘ β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) ∈ β„‚)
350349adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) ∈ β„‚)
351 4cn 12298 . . . . . . . . . . . . . 14 4 ∈ β„‚
352351a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))) β†’ 4 ∈ β„‚)
353 4ne0 12321 . . . . . . . . . . . . . 14 4 β‰  0
354353a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))) β†’ 4 β‰  0)
355350, 352, 354divcan2d 11993 . . . . . . . . . . . 12 ((πœ‘ ∧ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))) β†’ (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)) = (absβ€˜(𝑅 βˆ’ 𝐿)))
356346, 355breqtrd 5167 . . . . . . . . . . 11 ((πœ‘ ∧ (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4))) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (absβ€˜(𝑅 βˆ’ 𝐿)))
357356ex 412 . . . . . . . . . 10 (πœ‘ β†’ ((absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (absβ€˜(𝑅 βˆ’ 𝐿))))
358357a1d 25 . . . . . . . . 9 (πœ‘ β†’ ((π‘Ž ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) β†’ ((absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (absβ€˜(𝑅 βˆ’ 𝐿)))))
359358ad2antrr 723 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ ((π‘Ž ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) β†’ ((absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (absβ€˜(𝑅 βˆ’ 𝐿)))))
360359rexlimdvv 3204 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (βˆƒπ‘Ž ∈ 𝐴 βˆƒπ‘ ∈ 𝐴 (absβ€˜(𝑅 βˆ’ 𝐿)) < (4 Β· ((absβ€˜(𝑅 βˆ’ 𝐿)) / 4)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (absβ€˜(𝑅 βˆ’ 𝐿))))
361345, 360mpd 15 . . . . . 6 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) < (absβ€˜(𝑅 βˆ’ 𝐿)))
3629abscld 15386 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ (absβ€˜(𝑅 βˆ’ 𝐿)) ∈ ℝ)
363362ltnrd 11349 . . . . . 6 (((πœ‘ ∧ π‘₯ ∈ β„‚) ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) β†’ Β¬ (absβ€˜(𝑅 βˆ’ 𝐿)) < (absβ€˜(𝑅 βˆ’ 𝐿)))
364361, 363pm2.65da 814 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ β„‚) β†’ Β¬ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦))
365364ex 412 . . . 4 (πœ‘ β†’ (π‘₯ ∈ β„‚ β†’ Β¬ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)))
366 imnan 399 . . . 4 ((π‘₯ ∈ β„‚ β†’ Β¬ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)) ↔ Β¬ (π‘₯ ∈ β„‚ ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)))
367365, 366sylib 217 . . 3 (πœ‘ β†’ Β¬ (π‘₯ ∈ β„‚ ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦)))
368 limclner.a . . . . 5 (πœ‘ β†’ 𝐴 βŠ† ℝ)
369368, 73sstrd 3987 . . . 4 (πœ‘ β†’ 𝐴 βŠ† β„‚)
37036, 369, 56ellimc3 25758 . . 3 (πœ‘ β†’ (π‘₯ ∈ (𝐹 limβ„‚ 𝐡) ↔ (π‘₯ ∈ β„‚ ∧ βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ 𝐴 ((𝑀 β‰  𝐡 ∧ (absβ€˜(𝑀 βˆ’ 𝐡)) < 𝑧) β†’ (absβ€˜((πΉβ€˜π‘€) βˆ’ π‘₯)) < 𝑦))))
371367, 370mtbird 325 . 2 (πœ‘ β†’ Β¬ π‘₯ ∈ (𝐹 limβ„‚ 𝐡))
372371eq0rdv 4399 1 (πœ‘ β†’ (𝐹 limβ„‚ 𝐡) = βˆ…)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   β‰  wne 2934  βˆ€wral 3055  βˆƒwrex 3064   βˆ– cdif 3940   ∩ cin 3942   βŠ† wss 3943  βˆ…c0 4317  ifcif 4523  {csn 4623  βˆͺ cuni 4902   class class class wbr 5141  ran crn 5670   β†Ύ cres 5671  βŸΆwf 6532  β€˜cfv 6536  (class class class)co 7404  β„‚cc 11107  β„cr 11108  0cc0 11109   + caddc 11112   Β· cmul 11114  +∞cpnf 11246  -∞cmnf 11247   < clt 11249   ≀ cle 11250   βˆ’ cmin 11445   / cdiv 11872  4c4 12270  β„+crp 12977  (,)cioo 13327  abscabs 15184   β†Ύt crest 17372  TopOpenctopn 17373  topGenctg 17389  β„‚fldccnfld 21235  Topctop 22745  limPtclp 22988   limβ„‚ climc 25741
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 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7721  ax-cnex 11165  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186  ax-pre-sup 11187
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-iin 4993  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6293  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6488  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8264  df-wrecs 8295  df-recs 8369  df-rdg 8408  df-1o 8464  df-er 8702  df-map 8821  df-pm 8822  df-en 8939  df-dom 8940  df-sdom 8941  df-fin 8942  df-fi 9405  df-sup 9436  df-inf 9437  df-pnf 11251  df-mnf 11252  df-xr 11253  df-ltxr 11254  df-le 11255  df-sub 11447  df-neg 11448  df-div 11873  df-nn 12214  df-2 12276  df-3 12277  df-4 12278  df-5 12279  df-6 12280  df-7 12281  df-8 12282  df-9 12283  df-n0 12474  df-z 12560  df-dec 12679  df-uz 12824  df-q 12934  df-rp 12978  df-xneg 13095  df-xadd 13096  df-xmul 13097  df-ioo 13331  df-fz 13488  df-seq 13970  df-exp 14030  df-cj 15049  df-re 15050  df-im 15051  df-sqrt 15185  df-abs 15186  df-struct 17086  df-slot 17121  df-ndx 17133  df-base 17151  df-plusg 17216  df-mulr 17217  df-starv 17218  df-tset 17222  df-ple 17223  df-ds 17225  df-unif 17226  df-rest 17374  df-topn 17375  df-topgen 17395  df-psmet 21227  df-xmet 21228  df-met 21229  df-bl 21230  df-mopn 21231  df-cnfld 21236  df-top 22746  df-topon 22763  df-topsp 22785  df-bases 22799  df-cld 22873  df-ntr 22874  df-cls 22875  df-nei 22952  df-lp 22990  df-cnp 23082  df-xms 24176  df-ms 24177  df-limc 25745
This theorem is referenced by:  limclr  44925  jumpncnp  45168
  Copyright terms: Public domain W3C validator