Metamath Proof Explorer

Theorem ftc1cnnc

Description: Choice-free proof of ftc1cn . (Contributed by Brendan Leahy, 20-Nov-2017)

Ref Expression
Hypotheses ftc1cnnc.g ⊒ 𝐺 = ( π‘₯ ∈ ( 𝐴 [,] 𝐡 ) ↦ ∫ ( 𝐴 (,) π‘₯ ) ( 𝐹 β€˜ 𝑑 ) d 𝑑 )
ftc1cnnc.a ⊒ ( πœ‘ β†’ 𝐴 ∈ ℝ )
ftc1cnnc.b ⊒ ( πœ‘ β†’ 𝐡 ∈ ℝ )
ftc1cnnc.le ⊒ ( πœ‘ β†’ 𝐴 ≀ 𝐡 )
ftc1cnnc.f ⊒ ( πœ‘ β†’ 𝐹 ∈ ( ( 𝐴 (,) 𝐡 ) –cnβ†’ β„‚ ) )
ftc1cnnc.i ⊒ ( πœ‘ β†’ 𝐹 ∈ 𝐿1 )
Assertion ftc1cnnc ( πœ‘ β†’ ( ℝ D 𝐺 ) = 𝐹 )

Proof

Step Hyp Ref Expression
1 ftc1cnnc.g ⊒ 𝐺 = ( π‘₯ ∈ ( 𝐴 [,] 𝐡 ) ↦ ∫ ( 𝐴 (,) π‘₯ ) ( 𝐹 β€˜ 𝑑 ) d 𝑑 )
2 ftc1cnnc.a ⊒ ( πœ‘ β†’ 𝐴 ∈ ℝ )
3 ftc1cnnc.b ⊒ ( πœ‘ β†’ 𝐡 ∈ ℝ )
4 ftc1cnnc.le ⊒ ( πœ‘ β†’ 𝐴 ≀ 𝐡 )
5 ftc1cnnc.f ⊒ ( πœ‘ β†’ 𝐹 ∈ ( ( 𝐴 (,) 𝐡 ) –cnβ†’ β„‚ ) )
6 ftc1cnnc.i ⊒ ( πœ‘ β†’ 𝐹 ∈ 𝐿1 )
7 dvf ⊒ ( ℝ D 𝐺 ) : dom ( ℝ D 𝐺 ) ⟢ β„‚
8 7 a1i ⊒ ( πœ‘ β†’ ( ℝ D 𝐺 ) : dom ( ℝ D 𝐺 ) ⟢ β„‚ )
9 8 ffund ⊒ ( πœ‘ β†’ Fun ( ℝ D 𝐺 ) )
10 ax-resscn ⊒ ℝ βŠ† β„‚
11 10 a1i ⊒ ( πœ‘ β†’ ℝ βŠ† β„‚ )
12 ssidd ⊒ ( πœ‘ β†’ ( 𝐴 (,) 𝐡 ) βŠ† ( 𝐴 (,) 𝐡 ) )
13 ioossre ⊒ ( 𝐴 (,) 𝐡 ) βŠ† ℝ
14 13 a1i ⊒ ( πœ‘ β†’ ( 𝐴 (,) 𝐡 ) βŠ† ℝ )
15 cncff ⊒ ( 𝐹 ∈ ( ( 𝐴 (,) 𝐡 ) –cnβ†’ β„‚ ) β†’ 𝐹 : ( 𝐴 (,) 𝐡 ) ⟢ β„‚ )
16 5 15 syl ⊒ ( πœ‘ β†’ 𝐹 : ( 𝐴 (,) 𝐡 ) ⟢ β„‚ )
17 1 2 3 4 12 14 6 16 ftc1lem2 ⊒ ( πœ‘ β†’ 𝐺 : ( 𝐴 [,] 𝐡 ) ⟢ β„‚ )
18 iccssre ⊒ ( ( 𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ) β†’ ( 𝐴 [,] 𝐡 ) βŠ† ℝ )
19 2 3 18 syl2anc ⊒ ( πœ‘ β†’ ( 𝐴 [,] 𝐡 ) βŠ† ℝ )
20 eqid ⊒ ( TopOpen β€˜ β„‚fld ) = ( TopOpen β€˜ β„‚fld )
21 20 tgioo2 ⊒ ( topGen β€˜ ran (,) ) = ( ( TopOpen β€˜ β„‚fld ) β†Ύt ℝ )
22 11 17 19 21 20 dvbssntr ⊒ ( πœ‘ β†’ dom ( ℝ D 𝐺 ) βŠ† ( ( int β€˜ ( topGen β€˜ ran (,) ) ) β€˜ ( 𝐴 [,] 𝐡 ) ) )
23 iccntr ⊒ ( ( 𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ) β†’ ( ( int β€˜ ( topGen β€˜ ran (,) ) ) β€˜ ( 𝐴 [,] 𝐡 ) ) = ( 𝐴 (,) 𝐡 ) )
24 2 3 23 syl2anc ⊒ ( πœ‘ β†’ ( ( int β€˜ ( topGen β€˜ ran (,) ) ) β€˜ ( 𝐴 [,] 𝐡 ) ) = ( 𝐴 (,) 𝐡 ) )
25 22 24 sseqtrd ⊒ ( πœ‘ β†’ dom ( ℝ D 𝐺 ) βŠ† ( 𝐴 (,) 𝐡 ) )
26 retop ⊒ ( topGen β€˜ ran (,) ) ∈ Top
27 21 26 eqeltrri ⊒ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ℝ ) ∈ Top
28 27 a1i ⊒ ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ℝ ) ∈ Top )
29 19 adantr ⊒ ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ ( 𝐴 [,] 𝐡 ) βŠ† ℝ )
30 iooretop ⊒ ( 𝐴 (,) 𝐡 ) ∈ ( topGen β€˜ ran (,) )
31 30 21 eleqtri ⊒ ( 𝐴 (,) 𝐡 ) ∈ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ℝ )
32 31 a1i ⊒ ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ ( 𝐴 (,) 𝐡 ) ∈ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ℝ ) )
33 ioossicc ⊒ ( 𝐴 (,) 𝐡 ) βŠ† ( 𝐴 [,] 𝐡 )
34 33 a1i ⊒ ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ ( 𝐴 (,) 𝐡 ) βŠ† ( 𝐴 [,] 𝐡 ) )
35 uniretop ⊒ ℝ = βˆͺ ( topGen β€˜ ran (,) )
36 21 unieqi ⊒ βˆͺ ( topGen β€˜ ran (,) ) = βˆͺ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ℝ )
37 35 36 eqtri ⊒ ℝ = βˆͺ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ℝ )
38 37 ssntr ⊒ ( ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt ℝ ) ∈ Top ∧ ( 𝐴 [,] 𝐡 ) βŠ† ℝ ) ∧ ( ( 𝐴 (,) 𝐡 ) ∈ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ℝ ) ∧ ( 𝐴 (,) 𝐡 ) βŠ† ( 𝐴 [,] 𝐡 ) ) ) β†’ ( 𝐴 (,) 𝐡 ) βŠ† ( ( int β€˜ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ℝ ) ) β€˜ ( 𝐴 [,] 𝐡 ) ) )
39 28 29 32 34 38 syl22anc ⊒ ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ ( 𝐴 (,) 𝐡 ) βŠ† ( ( int β€˜ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ℝ ) ) β€˜ ( 𝐴 [,] 𝐡 ) ) )
40 simpr ⊒ ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) )
41 39 40 sseldd ⊒ ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ 𝑐 ∈ ( ( int β€˜ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ℝ ) ) β€˜ ( 𝐴 [,] 𝐡 ) ) )
42 16 ffvelcdmda ⊒ ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ ( 𝐹 β€˜ 𝑐 ) ∈ β„‚ )
43 cnxmet ⊒ ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ )
44 13 10 sstri ⊒ ( 𝐴 (,) 𝐡 ) βŠ† β„‚
45 xmetres2 ⊒ ( ( ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ ) ∧ ( 𝐴 (,) 𝐡 ) βŠ† β„‚ ) β†’ ( ( abs ∘ βˆ’ ) β†Ύ ( ( 𝐴 (,) 𝐡 ) Γ— ( 𝐴 (,) 𝐡 ) ) ) ∈ ( ∞Met β€˜ ( 𝐴 (,) 𝐡 ) ) )
46 43 44 45 mp2an ⊒ ( ( abs ∘ βˆ’ ) β†Ύ ( ( 𝐴 (,) 𝐡 ) Γ— ( 𝐴 (,) 𝐡 ) ) ) ∈ ( ∞Met β€˜ ( 𝐴 (,) 𝐡 ) )
47 46 a1i ⊒ ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ 𝑀 ∈ ℝ+ ) β†’ ( ( abs ∘ βˆ’ ) β†Ύ ( ( 𝐴 (,) 𝐡 ) Γ— ( 𝐴 (,) 𝐡 ) ) ) ∈ ( ∞Met β€˜ ( 𝐴 (,) 𝐡 ) ) )
48 43 a1i ⊒ ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ 𝑀 ∈ ℝ+ ) β†’ ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ ) )
49 ssid ⊒ β„‚ βŠ† β„‚
50 eqid ⊒ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐴 (,) 𝐡 ) ) = ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐴 (,) 𝐡 ) )
51 20 cnfldtopon ⊒ ( TopOpen β€˜ β„‚fld ) ∈ ( TopOn β€˜ β„‚ )
52 51 toponrestid ⊒ ( TopOpen β€˜ β„‚fld ) = ( ( TopOpen β€˜ β„‚fld ) β†Ύt β„‚ )
53 20 50 52 cncfcn ⊒ ( ( ( 𝐴 (,) 𝐡 ) βŠ† β„‚ ∧ β„‚ βŠ† β„‚ ) β†’ ( ( 𝐴 (,) 𝐡 ) –cnβ†’ β„‚ ) = ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐴 (,) 𝐡 ) ) Cn ( TopOpen β€˜ β„‚fld ) ) )
54 44 49 53 mp2an ⊒ ( ( 𝐴 (,) 𝐡 ) –cnβ†’ β„‚ ) = ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐴 (,) 𝐡 ) ) Cn ( TopOpen β€˜ β„‚fld ) )
55 5 54 eleqtrdi ⊒ ( πœ‘ β†’ 𝐹 ∈ ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐴 (,) 𝐡 ) ) Cn ( TopOpen β€˜ β„‚fld ) ) )
56 resttopon ⊒ ( ( ( TopOpen β€˜ β„‚fld ) ∈ ( TopOn β€˜ β„‚ ) ∧ ( 𝐴 (,) 𝐡 ) βŠ† β„‚ ) β†’ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐴 (,) 𝐡 ) ) ∈ ( TopOn β€˜ ( 𝐴 (,) 𝐡 ) ) )
57 51 44 56 mp2an ⊒ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐴 (,) 𝐡 ) ) ∈ ( TopOn β€˜ ( 𝐴 (,) 𝐡 ) )
58 57 toponunii ⊒ ( 𝐴 (,) 𝐡 ) = βˆͺ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐴 (,) 𝐡 ) )
59 58 eleq2i ⊒ ( 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ↔ 𝑐 ∈ βˆͺ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐴 (,) 𝐡 ) ) )
60 59 biimpi ⊒ ( 𝑐 ∈ ( 𝐴 (,) 𝐡 ) β†’ 𝑐 ∈ βˆͺ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐴 (,) 𝐡 ) ) )
61 eqid ⊒ βˆͺ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐴 (,) 𝐡 ) ) = βˆͺ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐴 (,) 𝐡 ) )
62 61 cncnpi ⊒ ( ( 𝐹 ∈ ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐴 (,) 𝐡 ) ) Cn ( TopOpen β€˜ β„‚fld ) ) ∧ 𝑐 ∈ βˆͺ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐴 (,) 𝐡 ) ) ) β†’ 𝐹 ∈ ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐴 (,) 𝐡 ) ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝑐 ) )
63 55 60 62 syl2an ⊒ ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ 𝐹 ∈ ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐴 (,) 𝐡 ) ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝑐 ) )
64 eqid ⊒ ( ( abs ∘ βˆ’ ) β†Ύ ( ( 𝐴 (,) 𝐡 ) Γ— ( 𝐴 (,) 𝐡 ) ) ) = ( ( abs ∘ βˆ’ ) β†Ύ ( ( 𝐴 (,) 𝐡 ) Γ— ( 𝐴 (,) 𝐡 ) ) )
65 20 cnfldtopn ⊒ ( TopOpen β€˜ β„‚fld ) = ( MetOpen β€˜ ( abs ∘ βˆ’ ) )
66 eqid ⊒ ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ( 𝐴 (,) 𝐡 ) Γ— ( 𝐴 (,) 𝐡 ) ) ) ) = ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ( 𝐴 (,) 𝐡 ) Γ— ( 𝐴 (,) 𝐡 ) ) ) )
67 64 65 66 metrest ⊒ ( ( ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ ) ∧ ( 𝐴 (,) 𝐡 ) βŠ† β„‚ ) β†’ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐴 (,) 𝐡 ) ) = ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ( 𝐴 (,) 𝐡 ) Γ— ( 𝐴 (,) 𝐡 ) ) ) ) )
68 43 44 67 mp2an ⊒ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐴 (,) 𝐡 ) ) = ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ( 𝐴 (,) 𝐡 ) Γ— ( 𝐴 (,) 𝐡 ) ) ) )
69 68 oveq1i ⊒ ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐴 (,) 𝐡 ) ) CnP ( TopOpen β€˜ β„‚fld ) ) = ( ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ( 𝐴 (,) 𝐡 ) Γ— ( 𝐴 (,) 𝐡 ) ) ) ) CnP ( TopOpen β€˜ β„‚fld ) )
70 69 fveq1i ⊒ ( ( ( ( TopOpen β€˜ β„‚fld ) β†Ύt ( 𝐴 (,) 𝐡 ) ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝑐 ) = ( ( ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ( 𝐴 (,) 𝐡 ) Γ— ( 𝐴 (,) 𝐡 ) ) ) ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝑐 )
71 63 70 eleqtrdi ⊒ ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ 𝐹 ∈ ( ( ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ( 𝐴 (,) 𝐡 ) Γ— ( 𝐴 (,) 𝐡 ) ) ) ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝑐 ) )
72 71 adantr ⊒ ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ 𝑀 ∈ ℝ+ ) β†’ 𝐹 ∈ ( ( ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ( 𝐴 (,) 𝐡 ) Γ— ( 𝐴 (,) 𝐡 ) ) ) ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝑐 ) )
73 simpr ⊒ ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ 𝑀 ∈ ℝ+ ) β†’ 𝑀 ∈ ℝ+ )
74 66 65 metcnpi2 ⊒ ( ( ( ( ( abs ∘ βˆ’ ) β†Ύ ( ( 𝐴 (,) 𝐡 ) Γ— ( 𝐴 (,) 𝐡 ) ) ) ∈ ( ∞Met β€˜ ( 𝐴 (,) 𝐡 ) ) ∧ ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ ) ) ∧ ( 𝐹 ∈ ( ( ( MetOpen β€˜ ( ( abs ∘ βˆ’ ) β†Ύ ( ( 𝐴 (,) 𝐡 ) Γ— ( 𝐴 (,) 𝐡 ) ) ) ) CnP ( TopOpen β€˜ β„‚fld ) ) β€˜ 𝑐 ) ∧ 𝑀 ∈ ℝ+ ) ) β†’ βˆƒ 𝑣 ∈ ℝ+ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( 𝑒 ( ( abs ∘ βˆ’ ) β†Ύ ( ( 𝐴 (,) 𝐡 ) Γ— ( 𝐴 (,) 𝐡 ) ) ) 𝑐 ) < 𝑣 β†’ ( ( 𝐹 β€˜ 𝑒 ) ( abs ∘ βˆ’ ) ( 𝐹 β€˜ 𝑐 ) ) < 𝑀 ) )
75 47 48 72 73 74 syl22anc ⊒ ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ 𝑀 ∈ ℝ+ ) β†’ βˆƒ 𝑣 ∈ ℝ+ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( 𝑒 ( ( abs ∘ βˆ’ ) β†Ύ ( ( 𝐴 (,) 𝐡 ) Γ— ( 𝐴 (,) 𝐡 ) ) ) 𝑐 ) < 𝑣 β†’ ( ( 𝐹 β€˜ 𝑒 ) ( abs ∘ βˆ’ ) ( 𝐹 β€˜ 𝑐 ) ) < 𝑀 ) )
76 simpr ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) )
77 simpllr ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) )
78 76 77 ovresd ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ ( 𝑒 ( ( abs ∘ βˆ’ ) β†Ύ ( ( 𝐴 (,) 𝐡 ) Γ— ( 𝐴 (,) 𝐡 ) ) ) 𝑐 ) = ( 𝑒 ( abs ∘ βˆ’ ) 𝑐 ) )
79 elioore ⊒ ( 𝑒 ∈ ( 𝐴 (,) 𝐡 ) β†’ 𝑒 ∈ ℝ )
80 79 recnd ⊒ ( 𝑒 ∈ ( 𝐴 (,) 𝐡 ) β†’ 𝑒 ∈ β„‚ )
81 44 sseli ⊒ ( 𝑐 ∈ ( 𝐴 (,) 𝐡 ) β†’ 𝑐 ∈ β„‚ )
82 81 ad3antlr ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ 𝑐 ∈ β„‚ )
83 eqid ⊒ ( abs ∘ βˆ’ ) = ( abs ∘ βˆ’ )
84 83 cnmetdval ⊒ ( ( 𝑒 ∈ β„‚ ∧ 𝑐 ∈ β„‚ ) β†’ ( 𝑒 ( abs ∘ βˆ’ ) 𝑐 ) = ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) )
85 80 82 84 syl2an2 ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ ( 𝑒 ( abs ∘ βˆ’ ) 𝑐 ) = ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) )
86 78 85 eqtrd ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ ( 𝑒 ( ( abs ∘ βˆ’ ) β†Ύ ( ( 𝐴 (,) 𝐡 ) Γ— ( 𝐴 (,) 𝐡 ) ) ) 𝑐 ) = ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) )
87 86 breq1d ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ ( ( 𝑒 ( ( abs ∘ βˆ’ ) β†Ύ ( ( 𝐴 (,) 𝐡 ) Γ— ( 𝐴 (,) 𝐡 ) ) ) 𝑐 ) < 𝑣 ↔ ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 ) )
88 16 ad2antrr ⊒ ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) β†’ 𝐹 : ( 𝐴 (,) 𝐡 ) ⟢ β„‚ )
89 88 ffvelcdmda ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ ( 𝐹 β€˜ 𝑒 ) ∈ β„‚ )
90 42 ad2antrr ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ ( 𝐹 β€˜ 𝑐 ) ∈ β„‚ )
91 83 cnmetdval ⊒ ( ( ( 𝐹 β€˜ 𝑒 ) ∈ β„‚ ∧ ( 𝐹 β€˜ 𝑐 ) ∈ β„‚ ) β†’ ( ( 𝐹 β€˜ 𝑒 ) ( abs ∘ βˆ’ ) ( 𝐹 β€˜ 𝑐 ) ) = ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) )
92 89 90 91 syl2anc ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ ( ( 𝐹 β€˜ 𝑒 ) ( abs ∘ βˆ’ ) ( 𝐹 β€˜ 𝑐 ) ) = ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) )
93 92 breq1d ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ ( ( ( 𝐹 β€˜ 𝑒 ) ( abs ∘ βˆ’ ) ( 𝐹 β€˜ 𝑐 ) ) < 𝑀 ↔ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) )
94 87 93 imbi12d ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ ( ( ( 𝑒 ( ( abs ∘ βˆ’ ) β†Ύ ( ( 𝐴 (,) 𝐡 ) Γ— ( 𝐴 (,) 𝐡 ) ) ) 𝑐 ) < 𝑣 β†’ ( ( 𝐹 β€˜ 𝑒 ) ( abs ∘ βˆ’ ) ( 𝐹 β€˜ 𝑐 ) ) < 𝑀 ) ↔ ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) )
95 94 ralbidva ⊒ ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) β†’ ( βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( 𝑒 ( ( abs ∘ βˆ’ ) β†Ύ ( ( 𝐴 (,) 𝐡 ) Γ— ( 𝐴 (,) 𝐡 ) ) ) 𝑐 ) < 𝑣 β†’ ( ( 𝐹 β€˜ 𝑒 ) ( abs ∘ βˆ’ ) ( 𝐹 β€˜ 𝑐 ) ) < 𝑀 ) ↔ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) )
96 simprll ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) β†’ 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) )
97 eldifsni ⊒ ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) β†’ 𝑧 β‰  𝑐 )
98 96 97 syl ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) β†’ 𝑧 β‰  𝑐 )
99 19 ssdifssd ⊒ ( πœ‘ β†’ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) βŠ† ℝ )
100 99 sselda ⊒ ( ( πœ‘ ∧ 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ) β†’ 𝑧 ∈ ℝ )
101 100 ad2ant2r ⊒ ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ) β†’ 𝑧 ∈ ℝ )
102 101 ad2ant2r ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) β†’ 𝑧 ∈ ℝ )
103 elioore ⊒ ( 𝑐 ∈ ( 𝐴 (,) 𝐡 ) β†’ 𝑐 ∈ ℝ )
104 103 ad3antlr ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) β†’ 𝑐 ∈ ℝ )
105 102 104 lttri2d ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) β†’ ( 𝑧 β‰  𝑐 ↔ ( 𝑧 < 𝑐 ∨ 𝑐 < 𝑧 ) ) )
106 105 biimpa ⊒ ( ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 β‰  𝑐 ) β†’ ( 𝑧 < 𝑐 ∨ 𝑐 < 𝑧 ) )
107 fveq2 ⊒ ( 𝑠 = 𝑧 β†’ ( 𝐺 β€˜ 𝑠 ) = ( 𝐺 β€˜ 𝑧 ) )
108 107 oveq1d ⊒ ( 𝑠 = 𝑧 β†’ ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) = ( ( 𝐺 β€˜ 𝑧 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) )
109 oveq1 ⊒ ( 𝑠 = 𝑧 β†’ ( 𝑠 βˆ’ 𝑐 ) = ( 𝑧 βˆ’ 𝑐 ) )
110 108 109 oveq12d ⊒ ( 𝑠 = 𝑧 β†’ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) = ( ( ( 𝐺 β€˜ 𝑧 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑧 βˆ’ 𝑐 ) ) )
111 eqid ⊒ ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) = ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) )
112 ovex ⊒ ( ( ( 𝐺 β€˜ 𝑧 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑧 βˆ’ 𝑐 ) ) ∈ V
113 110 111 112 fvmpt ⊒ ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) β†’ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) β€˜ 𝑧 ) = ( ( ( 𝐺 β€˜ 𝑧 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑧 βˆ’ 𝑐 ) ) )
114 113 ad2antrr ⊒ ( ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) β†’ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) β€˜ 𝑧 ) = ( ( ( 𝐺 β€˜ 𝑧 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑧 βˆ’ 𝑐 ) ) )
115 114 ad2antlr ⊒ ( ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) β†’ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) β€˜ 𝑧 ) = ( ( ( 𝐺 β€˜ 𝑧 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑧 βˆ’ 𝑐 ) ) )
116 17 ad4antr ⊒ ( ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) β†’ 𝐺 : ( 𝐴 [,] 𝐡 ) ⟢ β„‚ )
117 eldifi ⊒ ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) β†’ 𝑧 ∈ ( 𝐴 [,] 𝐡 ) )
118 117 ad2antrr ⊒ ( ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) β†’ 𝑧 ∈ ( 𝐴 [,] 𝐡 ) )
119 118 ad2antlr ⊒ ( ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) β†’ 𝑧 ∈ ( 𝐴 [,] 𝐡 ) )
120 116 119 ffvelcdmd ⊒ ( ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) β†’ ( 𝐺 β€˜ 𝑧 ) ∈ β„‚ )
121 33 sseli ⊒ ( 𝑐 ∈ ( 𝐴 (,) 𝐡 ) β†’ 𝑐 ∈ ( 𝐴 [,] 𝐡 ) )
122 17 ffvelcdmda ⊒ ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 [,] 𝐡 ) ) β†’ ( 𝐺 β€˜ 𝑐 ) ∈ β„‚ )
123 121 122 sylan2 ⊒ ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ ( 𝐺 β€˜ 𝑐 ) ∈ β„‚ )
124 123 ad3antrrr ⊒ ( ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) β†’ ( 𝐺 β€˜ 𝑐 ) ∈ β„‚ )
125 102 adantr ⊒ ( ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) β†’ 𝑧 ∈ ℝ )
126 125 recnd ⊒ ( ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) β†’ 𝑧 ∈ β„‚ )
127 81 ad4antlr ⊒ ( ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) β†’ 𝑐 ∈ β„‚ )
128 ltne ⊒ ( ( 𝑧 ∈ ℝ ∧ 𝑧 < 𝑐 ) β†’ 𝑐 β‰  𝑧 )
129 128 necomd ⊒ ( ( 𝑧 ∈ ℝ ∧ 𝑧 < 𝑐 ) β†’ 𝑧 β‰  𝑐 )
130 102 129 sylan ⊒ ( ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) β†’ 𝑧 β‰  𝑐 )
131 120 124 126 127 130 div2subd ⊒ ( ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) β†’ ( ( ( 𝐺 β€˜ 𝑧 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑧 βˆ’ 𝑐 ) ) = ( ( ( 𝐺 β€˜ 𝑐 ) βˆ’ ( 𝐺 β€˜ 𝑧 ) ) / ( 𝑐 βˆ’ 𝑧 ) ) )
132 115 131 eqtrd ⊒ ( ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) β†’ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) β€˜ 𝑧 ) = ( ( ( 𝐺 β€˜ 𝑐 ) βˆ’ ( 𝐺 β€˜ 𝑧 ) ) / ( 𝑐 βˆ’ 𝑧 ) ) )
133 132 fvoveq1d ⊒ ( ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) β†’ ( abs β€˜ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) β€˜ 𝑧 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) = ( abs β€˜ ( ( ( ( 𝐺 β€˜ 𝑐 ) βˆ’ ( 𝐺 β€˜ 𝑧 ) ) / ( 𝑐 βˆ’ 𝑧 ) ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) )
134 2 ad3antrrr ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) β†’ 𝐴 ∈ ℝ )
135 3 ad3antrrr ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) β†’ 𝐡 ∈ ℝ )
136 4 ad3antrrr ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) β†’ 𝐴 ≀ 𝐡 )
137 5 ad3antrrr ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) β†’ 𝐹 ∈ ( ( 𝐴 (,) 𝐡 ) –cnβ†’ β„‚ ) )
138 6 ad3antrrr ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) β†’ 𝐹 ∈ 𝐿1 )
139 simpllr ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) β†’ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) )
140 simplrl ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) β†’ 𝑀 ∈ ℝ+ )
141 simplrr ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) β†’ 𝑣 ∈ ℝ+ )
142 simprlr ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) β†’ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) )
143 fvoveq1 ⊒ ( 𝑒 = 𝑦 β†’ ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) = ( abs β€˜ ( 𝑦 βˆ’ 𝑐 ) ) )
144 143 breq1d ⊒ ( 𝑒 = 𝑦 β†’ ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 ↔ ( abs β€˜ ( 𝑦 βˆ’ 𝑐 ) ) < 𝑣 ) )
145 144 imbrov2fvoveq ⊒ ( 𝑒 = 𝑦 β†’ ( ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ↔ ( ( abs β€˜ ( 𝑦 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑦 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) )
146 145 rspccva ⊒ ( ( βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ∧ 𝑦 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ ( ( abs β€˜ ( 𝑦 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑦 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) )
147 142 146 sylan ⊒ ( ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) ∧ 𝑦 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ ( ( abs β€˜ ( 𝑦 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑦 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) )
148 96 117 syl ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) β†’ 𝑧 ∈ ( 𝐴 [,] 𝐡 ) )
149 simprr ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) β†’ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 )
150 121 ad3antlr ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) β†’ 𝑐 ∈ ( 𝐴 [,] 𝐡 ) )
151 103 recnd ⊒ ( 𝑐 ∈ ( 𝐴 (,) 𝐡 ) β†’ 𝑐 ∈ β„‚ )
152 151 subidd ⊒ ( 𝑐 ∈ ( 𝐴 (,) 𝐡 ) β†’ ( 𝑐 βˆ’ 𝑐 ) = 0 )
153 152 abs00bd ⊒ ( 𝑐 ∈ ( 𝐴 (,) 𝐡 ) β†’ ( abs β€˜ ( 𝑐 βˆ’ 𝑐 ) ) = 0 )
154 153 ad3antlr ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) β†’ ( abs β€˜ ( 𝑐 βˆ’ 𝑐 ) ) = 0 )
155 141 rpgt0d ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) β†’ 0 < 𝑣 )
156 154 155 eqbrtrd ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) β†’ ( abs β€˜ ( 𝑐 βˆ’ 𝑐 ) ) < 𝑣 )
157 1 134 135 136 137 138 139 111 140 141 147 148 149 150 156 ftc1cnnclem ⊒ ( ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) β†’ ( abs β€˜ ( ( ( ( 𝐺 β€˜ 𝑐 ) βˆ’ ( 𝐺 β€˜ 𝑧 ) ) / ( 𝑐 βˆ’ 𝑧 ) ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 )
158 133 157 eqbrtrd ⊒ ( ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 < 𝑐 ) β†’ ( abs β€˜ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) β€˜ 𝑧 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 )
159 113 fvoveq1d ⊒ ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) β†’ ( abs β€˜ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) β€˜ 𝑧 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) = ( abs β€˜ ( ( ( ( 𝐺 β€˜ 𝑧 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑧 βˆ’ 𝑐 ) ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) )
160 159 ad2antrr ⊒ ( ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) β†’ ( abs β€˜ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) β€˜ 𝑧 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) = ( abs β€˜ ( ( ( ( 𝐺 β€˜ 𝑧 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑧 βˆ’ 𝑐 ) ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) )
161 160 ad2antlr ⊒ ( ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) ∧ 𝑐 < 𝑧 ) β†’ ( abs β€˜ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) β€˜ 𝑧 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) = ( abs β€˜ ( ( ( ( 𝐺 β€˜ 𝑧 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑧 βˆ’ 𝑐 ) ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) )
162 1 134 135 136 137 138 139 111 140 141 147 150 156 148 149 ftc1cnnclem ⊒ ( ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) ∧ 𝑐 < 𝑧 ) β†’ ( abs β€˜ ( ( ( ( 𝐺 β€˜ 𝑧 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑧 βˆ’ 𝑐 ) ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 )
163 161 162 eqbrtrd ⊒ ( ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) ∧ 𝑐 < 𝑧 ) β†’ ( abs β€˜ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) β€˜ 𝑧 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 )
164 158 163 jaodan ⊒ ( ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) ∧ ( 𝑧 < 𝑐 ∨ 𝑐 < 𝑧 ) ) β†’ ( abs β€˜ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) β€˜ 𝑧 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 )
165 106 164 syldan ⊒ ( ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) ∧ 𝑧 β‰  𝑐 ) β†’ ( abs β€˜ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) β€˜ 𝑧 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 )
166 98 165 mpdan ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) ) β†’ ( abs β€˜ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) β€˜ 𝑧 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 )
167 166 expr ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ) β†’ ( ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) β€˜ 𝑧 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) )
168 167 adantld ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ∧ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ) β†’ ( ( 𝑧 β‰  𝑐 ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) β†’ ( abs β€˜ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) β€˜ 𝑧 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) )
169 168 expr ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) ∧ 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ) β†’ ( βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) β†’ ( ( 𝑧 β‰  𝑐 ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) β†’ ( abs β€˜ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) β€˜ 𝑧 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) )
170 169 ralrimdva ⊒ ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) β†’ ( βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( abs β€˜ ( 𝑒 βˆ’ 𝑐 ) ) < 𝑣 β†’ ( abs β€˜ ( ( 𝐹 β€˜ 𝑒 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) β†’ βˆ€ 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ( ( 𝑧 β‰  𝑐 ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) β†’ ( abs β€˜ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) β€˜ 𝑧 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) )
171 95 170 sylbid ⊒ ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ ( 𝑀 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ) ) β†’ ( βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( 𝑒 ( ( abs ∘ βˆ’ ) β†Ύ ( ( 𝐴 (,) 𝐡 ) Γ— ( 𝐴 (,) 𝐡 ) ) ) 𝑐 ) < 𝑣 β†’ ( ( 𝐹 β€˜ 𝑒 ) ( abs ∘ βˆ’ ) ( 𝐹 β€˜ 𝑐 ) ) < 𝑀 ) β†’ βˆ€ 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ( ( 𝑧 β‰  𝑐 ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) β†’ ( abs β€˜ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) β€˜ 𝑧 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) )
172 171 anassrs ⊒ ( ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ 𝑀 ∈ ℝ+ ) ∧ 𝑣 ∈ ℝ+ ) β†’ ( βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( 𝑒 ( ( abs ∘ βˆ’ ) β†Ύ ( ( 𝐴 (,) 𝐡 ) Γ— ( 𝐴 (,) 𝐡 ) ) ) 𝑐 ) < 𝑣 β†’ ( ( 𝐹 β€˜ 𝑒 ) ( abs ∘ βˆ’ ) ( 𝐹 β€˜ 𝑐 ) ) < 𝑀 ) β†’ βˆ€ 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ( ( 𝑧 β‰  𝑐 ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) β†’ ( abs β€˜ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) β€˜ 𝑧 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) )
173 172 reximdva ⊒ ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ 𝑀 ∈ ℝ+ ) β†’ ( βˆƒ 𝑣 ∈ ℝ+ βˆ€ 𝑒 ∈ ( 𝐴 (,) 𝐡 ) ( ( 𝑒 ( ( abs ∘ βˆ’ ) β†Ύ ( ( 𝐴 (,) 𝐡 ) Γ— ( 𝐴 (,) 𝐡 ) ) ) 𝑐 ) < 𝑣 β†’ ( ( 𝐹 β€˜ 𝑒 ) ( abs ∘ βˆ’ ) ( 𝐹 β€˜ 𝑐 ) ) < 𝑀 ) β†’ βˆƒ 𝑣 ∈ ℝ+ βˆ€ 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ( ( 𝑧 β‰  𝑐 ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) β†’ ( abs β€˜ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) β€˜ 𝑧 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) )
174 75 173 mpd ⊒ ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ 𝑀 ∈ ℝ+ ) β†’ βˆƒ 𝑣 ∈ ℝ+ βˆ€ 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ( ( 𝑧 β‰  𝑐 ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) β†’ ( abs β€˜ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) β€˜ 𝑧 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) )
175 174 ralrimiva ⊒ ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ βˆ€ 𝑀 ∈ ℝ+ βˆƒ 𝑣 ∈ ℝ+ βˆ€ 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ( ( 𝑧 β‰  𝑐 ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) β†’ ( abs β€˜ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) β€˜ 𝑧 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) )
176 17 adantr ⊒ ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ 𝐺 : ( 𝐴 [,] 𝐡 ) ⟢ β„‚ )
177 19 10 sstrdi ⊒ ( πœ‘ β†’ ( 𝐴 [,] 𝐡 ) βŠ† β„‚ )
178 177 adantr ⊒ ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ ( 𝐴 [,] 𝐡 ) βŠ† β„‚ )
179 121 adantl ⊒ ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ 𝑐 ∈ ( 𝐴 [,] 𝐡 ) )
180 176 178 179 dvlem ⊒ ( ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) ∧ 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ) β†’ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ∈ β„‚ )
181 180 fmpttd ⊒ ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) : ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ⟢ β„‚ )
182 177 ssdifssd ⊒ ( πœ‘ β†’ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) βŠ† β„‚ )
183 182 adantr ⊒ ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) βŠ† β„‚ )
184 81 adantl ⊒ ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ 𝑐 ∈ β„‚ )
185 181 183 184 ellimc3 ⊒ ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ ( ( 𝐹 β€˜ 𝑐 ) ∈ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) limβ„‚ 𝑐 ) ↔ ( ( 𝐹 β€˜ 𝑐 ) ∈ β„‚ ∧ βˆ€ 𝑀 ∈ ℝ+ βˆƒ 𝑣 ∈ ℝ+ βˆ€ 𝑧 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ( ( 𝑧 β‰  𝑐 ∧ ( abs β€˜ ( 𝑧 βˆ’ 𝑐 ) ) < 𝑣 ) β†’ ( abs β€˜ ( ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) β€˜ 𝑧 ) βˆ’ ( 𝐹 β€˜ 𝑐 ) ) ) < 𝑀 ) ) ) )
186 42 175 185 mpbir2and ⊒ ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ ( 𝐹 β€˜ 𝑐 ) ∈ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) limβ„‚ 𝑐 ) )
187 eqid ⊒ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ℝ ) = ( ( TopOpen β€˜ β„‚fld ) β†Ύt ℝ )
188 187 20 111 11 17 19 eldv ⊒ ( πœ‘ β†’ ( 𝑐 ( ℝ D 𝐺 ) ( 𝐹 β€˜ 𝑐 ) ↔ ( 𝑐 ∈ ( ( int β€˜ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ℝ ) ) β€˜ ( 𝐴 [,] 𝐡 ) ) ∧ ( 𝐹 β€˜ 𝑐 ) ∈ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) limβ„‚ 𝑐 ) ) ) )
189 188 adantr ⊒ ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ ( 𝑐 ( ℝ D 𝐺 ) ( 𝐹 β€˜ 𝑐 ) ↔ ( 𝑐 ∈ ( ( int β€˜ ( ( TopOpen β€˜ β„‚fld ) β†Ύt ℝ ) ) β€˜ ( 𝐴 [,] 𝐡 ) ) ∧ ( 𝐹 β€˜ 𝑐 ) ∈ ( ( 𝑠 ∈ ( ( 𝐴 [,] 𝐡 ) βˆ– { 𝑐 } ) ↦ ( ( ( 𝐺 β€˜ 𝑠 ) βˆ’ ( 𝐺 β€˜ 𝑐 ) ) / ( 𝑠 βˆ’ 𝑐 ) ) ) limβ„‚ 𝑐 ) ) ) )
190 41 186 189 mpbir2and ⊒ ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ 𝑐 ( ℝ D 𝐺 ) ( 𝐹 β€˜ 𝑐 ) )
191 vex ⊒ 𝑐 ∈ V
192 fvex ⊒ ( 𝐹 β€˜ 𝑐 ) ∈ V
193 191 192 breldm ⊒ ( 𝑐 ( ℝ D 𝐺 ) ( 𝐹 β€˜ 𝑐 ) β†’ 𝑐 ∈ dom ( ℝ D 𝐺 ) )
194 190 193 syl ⊒ ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ 𝑐 ∈ dom ( ℝ D 𝐺 ) )
195 25 194 eqelssd ⊒ ( πœ‘ β†’ dom ( ℝ D 𝐺 ) = ( 𝐴 (,) 𝐡 ) )
196 df-fn ⊒ ( ( ℝ D 𝐺 ) Fn ( 𝐴 (,) 𝐡 ) ↔ ( Fun ( ℝ D 𝐺 ) ∧ dom ( ℝ D 𝐺 ) = ( 𝐴 (,) 𝐡 ) ) )
197 9 195 196 sylanbrc ⊒ ( πœ‘ β†’ ( ℝ D 𝐺 ) Fn ( 𝐴 (,) 𝐡 ) )
198 16 ffnd ⊒ ( πœ‘ β†’ 𝐹 Fn ( 𝐴 (,) 𝐡 ) )
199 9 adantr ⊒ ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ Fun ( ℝ D 𝐺 ) )
200 funbrfv ⊒ ( Fun ( ℝ D 𝐺 ) β†’ ( 𝑐 ( ℝ D 𝐺 ) ( 𝐹 β€˜ 𝑐 ) β†’ ( ( ℝ D 𝐺 ) β€˜ 𝑐 ) = ( 𝐹 β€˜ 𝑐 ) ) )
201 199 190 200 sylc ⊒ ( ( πœ‘ ∧ 𝑐 ∈ ( 𝐴 (,) 𝐡 ) ) β†’ ( ( ℝ D 𝐺 ) β€˜ 𝑐 ) = ( 𝐹 β€˜ 𝑐 ) )
202 197 198 201 eqfnfvd ⊒ ( πœ‘ β†’ ( ℝ D 𝐺 ) = 𝐹 )