Metamath Proof Explorer

Theorem unblimceq0lem

Description: Lemma for unblimceq0 . (Contributed by Asger C. Ipsen, 12-May-2021)

Ref Expression
Hypotheses unblimceq0lem.0 ⊢φ→S⊆ℂ
unblimceq0lem.1 ⊢φ→F:S⟶ℂ
unblimceq0lem.2 ⊢φ→A∈ℂ
unblimceq0lem.3 ⊢φ→∀b∈ℝ+∀d∈ℝ+∃x∈Sx−A<d∧b≤F⁡x
Assertion unblimceq0lem ⊢φ→∀c∈ℝ+∀d∈ℝ+∃y∈Sy≠A∧y−A<d∧c≤F⁡y

Proof

Step Hyp Ref Expression
1 unblimceq0lem.0 ⊢φ→S⊆ℂ
2 unblimceq0lem.1 ⊢φ→F:S⟶ℂ
3 unblimceq0lem.2 ⊢φ→A∈ℂ
4 unblimceq0lem.3 ⊢φ→∀b∈ℝ+∀d∈ℝ+∃x∈Sx−A<d∧b≤F⁡x
5 breq1 ⊢b=ifA∈SF⁡A+cc→b≤F⁡x↔ifA∈SF⁡A+cc≤F⁡x
6 5 anbi2d ⊢b=ifA∈SF⁡A+cc→x−A<d∧b≤F⁡x↔x−A<d∧ifA∈SF⁡A+cc≤F⁡x
7 6 rexbidv ⊢b=ifA∈SF⁡A+cc→∃x∈Sx−A<d∧b≤F⁡x↔∃x∈Sx−A<d∧ifA∈SF⁡A+cc≤F⁡x
8 7 ralbidv ⊢b=ifA∈SF⁡A+cc→∀d∈ℝ+∃x∈Sx−A<d∧b≤F⁡x↔∀d∈ℝ+∃x∈Sx−A<d∧ifA∈SF⁡A+cc≤F⁡x
9 4 adantr ⊢φ∧c∈ℝ+∧d∈ℝ+→∀b∈ℝ+∀d∈ℝ+∃x∈Sx−A<d∧b≤F⁡x
10 2 ad2antrr ⊢φ∧c∈ℝ+∧d∈ℝ+∧A∈S→F:S⟶ℂ
11 simpr ⊢φ∧c∈ℝ+∧d∈ℝ+∧A∈S→A∈S
12 10 11 ffvelcdmd ⊢φ∧c∈ℝ+∧d∈ℝ+∧A∈S→F⁡A∈ℂ
13 12 abscld ⊢φ∧c∈ℝ+∧d∈ℝ+∧A∈S→F⁡A∈ℝ
14 simprl ⊢φ∧c∈ℝ+∧d∈ℝ+→c∈ℝ+
15 14 rpred ⊢φ∧c∈ℝ+∧d∈ℝ+→c∈ℝ
16 15 adantr ⊢φ∧c∈ℝ+∧d∈ℝ+∧A∈S→c∈ℝ
17 13 16 readdcld ⊢φ∧c∈ℝ+∧d∈ℝ+∧A∈S→F⁡A+c∈ℝ
18 12 absge0d ⊢φ∧c∈ℝ+∧d∈ℝ+∧A∈S→0≤F⁡A
19 14 rpgt0d ⊢φ∧c∈ℝ+∧d∈ℝ+→0<c
20 19 adantr ⊢φ∧c∈ℝ+∧d∈ℝ+∧A∈S→0<c
21 13 16 18 20 addgegt0d ⊢φ∧c∈ℝ+∧d∈ℝ+∧A∈S→0<F⁡A+c
22 17 21 elrpd ⊢φ∧c∈ℝ+∧d∈ℝ+∧A∈S→F⁡A+c∈ℝ+
23 simplrl ⊢φ∧c∈ℝ+∧d∈ℝ+∧¬A∈S→c∈ℝ+
24 22 23 ifclda ⊢φ∧c∈ℝ+∧d∈ℝ+→ifA∈SF⁡A+cc∈ℝ+
25 8 9 24 rspcdva ⊢φ∧c∈ℝ+∧d∈ℝ+→∀d∈ℝ+∃x∈Sx−A<d∧ifA∈SF⁡A+cc≤F⁡x
26 simprr ⊢φ∧c∈ℝ+∧d∈ℝ+→d∈ℝ+
27 rsp ⊢∀d∈ℝ+∃x∈Sx−A<d∧ifA∈SF⁡A+cc≤F⁡x→d∈ℝ+→∃x∈Sx−A<d∧ifA∈SF⁡A+cc≤F⁡x
28 25 26 27 sylc ⊢φ∧c∈ℝ+∧d∈ℝ+→∃x∈Sx−A<d∧ifA∈SF⁡A+cc≤F⁡x
29 simprl ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x→x∈S
30 neeq1 ⊢y=x→y≠A↔x≠A
31 fvoveq1 ⊢y=x→y−A=x−A
32 31 breq1d ⊢y=x→y−A<d↔x−A<d
33 2fveq3 ⊢y=x→F⁡y=F⁡x
34 33 breq2d ⊢y=x→c≤F⁡y↔c≤F⁡x
35 30 32 34 3anbi123d ⊢y=x→y≠A∧y−A<d∧c≤F⁡y↔x≠A∧x−A<d∧c≤F⁡x
36 35 adantl ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧y=x→y≠A∧y−A<d∧c≤F⁡y↔x≠A∧x−A<d∧c≤F⁡x
37 17 adantlr ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧A∈S→F⁡A+c∈ℝ
38 2 ad2antrr ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x→F:S⟶ℂ
39 38 29 ffvelcdmd ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x→F⁡x∈ℂ
40 39 abscld ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x→F⁡x∈ℝ
41 40 adantr ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧A∈S→F⁡x∈ℝ
42 simpr ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧A∈S→A∈S
43 42 iftrued ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧A∈S→ifA∈SF⁡A+cc=F⁡A+c
44 43 eqcomd ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧A∈S→F⁡A+c=ifA∈SF⁡A+cc
45 simprrr ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x→ifA∈SF⁡A+cc≤F⁡x
46 45 adantr ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧A∈S→ifA∈SF⁡A+cc≤F⁡x
47 44 46 eqbrtrd ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧A∈S→F⁡A+c≤F⁡x
48 37 41 47 lensymd ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧A∈S→¬F⁡x<F⁡A+c
49 2fveq3 ⊢x=A→F⁡x=F⁡A
50 49 adantl ⊢φ∧c∈ℝ+∧d∈ℝ+∧A∈S∧x=A→F⁡x=F⁡A
51 16 13 ltaddposd ⊢φ∧c∈ℝ+∧d∈ℝ+∧A∈S→0<c↔F⁡A<F⁡A+c
52 20 51 mpbid ⊢φ∧c∈ℝ+∧d∈ℝ+∧A∈S→F⁡A<F⁡A+c
53 52 adantr ⊢φ∧c∈ℝ+∧d∈ℝ+∧A∈S∧x=A→F⁡A<F⁡A+c
54 50 53 eqbrtrd ⊢φ∧c∈ℝ+∧d∈ℝ+∧A∈S∧x=A→F⁡x<F⁡A+c
55 54 ex ⊢φ∧c∈ℝ+∧d∈ℝ+∧A∈S→x=A→F⁡x<F⁡A+c
56 55 adantlr ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧A∈S→x=A→F⁡x<F⁡A+c
57 56 necon3bd ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧A∈S→¬F⁡x<F⁡A+c→x≠A
58 48 57 mpd ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧A∈S→x≠A
59 simprrl ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x→x−A<d
60 59 adantr ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧A∈S→x−A<d
61 16 adantlr ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧A∈S→c∈ℝ
62 12 adantlr ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧A∈S→F⁡A∈ℂ
63 62 absge0d ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧A∈S→0≤F⁡A
64 13 adantlr ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧A∈S→F⁡A∈ℝ
65 61 64 addge02d ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧A∈S→0≤F⁡A↔c≤F⁡A+c
66 63 65 mpbid ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧A∈S→c≤F⁡A+c
67 61 37 41 66 47 letrd ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧A∈S→c≤F⁡x
68 58 60 67 3jca ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧A∈S→x≠A∧x−A<d∧c≤F⁡x
69 simpr ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧¬A∈S→¬A∈S
70 simpr ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧¬A∈S∧x=A→x=A
71 29 adantr ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧¬A∈S→x∈S
72 71 adantr ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧¬A∈S∧x=A→x∈S
73 70 72 eqeltrrd ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧¬A∈S∧x=A→A∈S
74 73 ex ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧¬A∈S→x=A→A∈S
75 74 necon3bd ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧¬A∈S→¬A∈S→x≠A
76 69 75 mpd ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧¬A∈S→x≠A
77 59 adantr ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧¬A∈S→x−A<d
78 69 iffalsed ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧¬A∈S→ifA∈SF⁡A+cc=c
79 78 eqcomd ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧¬A∈S→c=ifA∈SF⁡A+cc
80 45 adantr ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧¬A∈S→ifA∈SF⁡A+cc≤F⁡x
81 79 80 eqbrtrd ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧¬A∈S→c≤F⁡x
82 76 77 81 3jca ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x∧¬A∈S→x≠A∧x−A<d∧c≤F⁡x
83 68 82 pm2.61dan ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x→x≠A∧x−A<d∧c≤F⁡x
84 29 36 83 rspcedvd ⊢φ∧c∈ℝ+∧d∈ℝ+∧x∈S∧x−A<d∧ifA∈SF⁡A+cc≤F⁡x→∃y∈Sy≠A∧y−A<d∧c≤F⁡y
85 28 84 rexlimddv ⊢φ∧c∈ℝ+∧d∈ℝ+→∃y∈Sy≠A∧y−A<d∧c≤F⁡y
86 85 ralrimivva ⊢φ→∀c∈ℝ+∀d∈ℝ+∃y∈Sy≠A∧y−A<d∧c≤F⁡y