Metamath Proof Explorer

Theorem ovolicc2lem5

Description: Lemma for ovolicc2 . (Contributed by Mario Carneiro, 14-Jun-2014)

Ref Expression
Hypotheses ovolicc.1 ⊢φ→A∈ℝ
ovolicc.2 ⊢φ→B∈ℝ
ovolicc.3 ⊢φ→A≤B
ovolicc2.4 ⊢S=seq1+abs∘−∘F
ovolicc2.5 ⊢φ→F:ℕ⟶≤∩ℝ2
ovolicc2.6 ⊢φ→U∈𝒫ran⁡.∘F∩Fin
ovolicc2.7 ⊢φ→AB⊆⋃U
ovolicc2.8 ⊢φ→G:U⟶ℕ
ovolicc2.9 ⊢φ∧t∈U→.∘F⁡G⁡t=t
ovolicc2.10 ⊢T=u∈U|u∩AB≠∅
Assertion ovolicc2lem5 ⊢φ→B−A≤supran⁡Sℝ*<

Proof

Step Hyp Ref Expression
1 ovolicc.1 ⊢φ→A∈ℝ
2 ovolicc.2 ⊢φ→B∈ℝ
3 ovolicc.3 ⊢φ→A≤B
4 ovolicc2.4 ⊢S=seq1+abs∘−∘F
5 ovolicc2.5 ⊢φ→F:ℕ⟶≤∩ℝ2
6 ovolicc2.6 ⊢φ→U∈𝒫ran⁡.∘F∩Fin
7 ovolicc2.7 ⊢φ→AB⊆⋃U
8 ovolicc2.8 ⊢φ→G:U⟶ℕ
9 ovolicc2.9 ⊢φ∧t∈U→.∘F⁡G⁡t=t
10 ovolicc2.10 ⊢T=u∈U|u∩AB≠∅
11 1 rexrd ⊢φ→A∈ℝ*
12 2 rexrd ⊢φ→B∈ℝ*
13 lbicc2 ⊢A∈ℝ*∧B∈ℝ*∧A≤B→A∈AB
14 11 12 3 13 syl3anc ⊢φ→A∈AB
15 7 14 sseldd ⊢φ→A∈⋃U
16 eluni2 ⊢A∈⋃U↔∃z∈UA∈z
17 15 16 sylib ⊢φ→∃z∈UA∈z
18 6 elin2d ⊢φ→U∈Fin
19 10 ssrab3 ⊢T⊆U
20 ssfi ⊢U∈Fin∧T⊆U→T∈Fin
21 18 19 20 sylancl ⊢φ→T∈Fin
22 7 adantr ⊢φ∧t∈T→AB⊆⋃U
23 ineq1 ⊢u=t→u∩AB=t∩AB
24 23 neeq1d ⊢u=t→u∩AB≠∅↔t∩AB≠∅
25 24 10 elrab2 ⊢t∈T↔t∈U∧t∩AB≠∅
26 25 simplbi ⊢t∈T→t∈U
27 ffvelcdm ⊢G:U⟶ℕ∧t∈U→G⁡t∈ℕ
28 8 26 27 syl2an ⊢φ∧t∈T→G⁡t∈ℕ
29 5 ffvelcdmda ⊢φ∧G⁡t∈ℕ→F⁡G⁡t∈≤∩ℝ2
30 28 29 syldan ⊢φ∧t∈T→F⁡G⁡t∈≤∩ℝ2
31 30 elin2d ⊢φ∧t∈T→F⁡G⁡t∈ℝ2
32 xp2nd ⊢F⁡G⁡t∈ℝ2→2nd⁡F⁡G⁡t∈ℝ
33 31 32 syl ⊢φ∧t∈T→2nd⁡F⁡G⁡t∈ℝ
34 2 adantr ⊢φ∧t∈T→B∈ℝ
35 33 34 ifcld ⊢φ∧t∈T→if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈ℝ
36 25 simprbi ⊢t∈T→t∩AB≠∅
37 36 adantl ⊢φ∧t∈T→t∩AB≠∅
38 n0 ⊢t∩AB≠∅↔∃yy∈t∩AB
39 37 38 sylib ⊢φ∧t∈T→∃yy∈t∩AB
40 1 adantr ⊢φ∧t∈T∧y∈t∩AB→A∈ℝ
41 simprr ⊢φ∧t∈T∧y∈t∩AB→y∈t∩AB
42 41 elin2d ⊢φ∧t∈T∧y∈t∩AB→y∈AB
43 2 adantr ⊢φ∧t∈T∧y∈t∩AB→B∈ℝ
44 elicc2 ⊢A∈ℝ∧B∈ℝ→y∈AB↔y∈ℝ∧A≤y∧y≤B
45 1 43 44 syl2an2r ⊢φ∧t∈T∧y∈t∩AB→y∈AB↔y∈ℝ∧A≤y∧y≤B
46 42 45 mpbid ⊢φ∧t∈T∧y∈t∩AB→y∈ℝ∧A≤y∧y≤B
47 46 simp1d ⊢φ∧t∈T∧y∈t∩AB→y∈ℝ
48 31 adantrr ⊢φ∧t∈T∧y∈t∩AB→F⁡G⁡t∈ℝ2
49 48 32 syl ⊢φ∧t∈T∧y∈t∩AB→2nd⁡F⁡G⁡t∈ℝ
50 46 simp2d ⊢φ∧t∈T∧y∈t∩AB→A≤y
51 41 elin1d ⊢φ∧t∈T∧y∈t∩AB→y∈t
52 28 adantrr ⊢φ∧t∈T∧y∈t∩AB→G⁡t∈ℕ
53 fvco3 ⊢F:ℕ⟶≤∩ℝ2∧G⁡t∈ℕ→.∘F⁡G⁡t=.⁡F⁡G⁡t
54 5 52 53 syl2an2r ⊢φ∧t∈T∧y∈t∩AB→.∘F⁡G⁡t=.⁡F⁡G⁡t
55 26 9 sylan2 ⊢φ∧t∈T→.∘F⁡G⁡t=t
56 55 adantrr ⊢φ∧t∈T∧y∈t∩AB→.∘F⁡G⁡t=t
57 1st2nd2 ⊢F⁡G⁡t∈ℝ2→F⁡G⁡t=1st⁡F⁡G⁡t2nd⁡F⁡G⁡t
58 48 57 syl ⊢φ∧t∈T∧y∈t∩AB→F⁡G⁡t=1st⁡F⁡G⁡t2nd⁡F⁡G⁡t
59 58 fveq2d ⊢φ∧t∈T∧y∈t∩AB→.⁡F⁡G⁡t=.⁡1st⁡F⁡G⁡t2nd⁡F⁡G⁡t
60 df-ov ⊢1st⁡F⁡G⁡t2nd⁡F⁡G⁡t=.⁡1st⁡F⁡G⁡t2nd⁡F⁡G⁡t
61 59 60 eqtr4di ⊢φ∧t∈T∧y∈t∩AB→.⁡F⁡G⁡t=1st⁡F⁡G⁡t2nd⁡F⁡G⁡t
62 54 56 61 3eqtr3d ⊢φ∧t∈T∧y∈t∩AB→t=1st⁡F⁡G⁡t2nd⁡F⁡G⁡t
63 51 62 eleqtrd ⊢φ∧t∈T∧y∈t∩AB→y∈1st⁡F⁡G⁡t2nd⁡F⁡G⁡t
64 xp1st ⊢F⁡G⁡t∈ℝ2→1st⁡F⁡G⁡t∈ℝ
65 48 64 syl ⊢φ∧t∈T∧y∈t∩AB→1st⁡F⁡G⁡t∈ℝ
66 rexr ⊢1st⁡F⁡G⁡t∈ℝ→1st⁡F⁡G⁡t∈ℝ*
67 rexr ⊢2nd⁡F⁡G⁡t∈ℝ→2nd⁡F⁡G⁡t∈ℝ*
68 elioo2 ⊢1st⁡F⁡G⁡t∈ℝ*∧2nd⁡F⁡G⁡t∈ℝ*→y∈1st⁡F⁡G⁡t2nd⁡F⁡G⁡t↔y∈ℝ∧1st⁡F⁡G⁡t<y∧y<2nd⁡F⁡G⁡t
69 66 67 68 syl2an ⊢1st⁡F⁡G⁡t∈ℝ∧2nd⁡F⁡G⁡t∈ℝ→y∈1st⁡F⁡G⁡t2nd⁡F⁡G⁡t↔y∈ℝ∧1st⁡F⁡G⁡t<y∧y<2nd⁡F⁡G⁡t
70 65 49 69 syl2anc ⊢φ∧t∈T∧y∈t∩AB→y∈1st⁡F⁡G⁡t2nd⁡F⁡G⁡t↔y∈ℝ∧1st⁡F⁡G⁡t<y∧y<2nd⁡F⁡G⁡t
71 63 70 mpbid ⊢φ∧t∈T∧y∈t∩AB→y∈ℝ∧1st⁡F⁡G⁡t<y∧y<2nd⁡F⁡G⁡t
72 71 simp3d ⊢φ∧t∈T∧y∈t∩AB→y<2nd⁡F⁡G⁡t
73 47 49 72 ltled ⊢φ∧t∈T∧y∈t∩AB→y≤2nd⁡F⁡G⁡t
74 40 47 49 50 73 letrd ⊢φ∧t∈T∧y∈t∩AB→A≤2nd⁡F⁡G⁡t
75 74 expr ⊢φ∧t∈T→y∈t∩AB→A≤2nd⁡F⁡G⁡t
76 75 exlimdv ⊢φ∧t∈T→∃yy∈t∩AB→A≤2nd⁡F⁡G⁡t
77 39 76 mpd ⊢φ∧t∈T→A≤2nd⁡F⁡G⁡t
78 3 adantr ⊢φ∧t∈T→A≤B
79 breq2 ⊢2nd⁡F⁡G⁡t=if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB→A≤2nd⁡F⁡G⁡t↔A≤if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB
80 breq2 ⊢B=if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB→A≤B↔A≤if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB
81 79 80 ifboth ⊢A≤2nd⁡F⁡G⁡t∧A≤B→A≤if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB
82 77 78 81 syl2anc ⊢φ∧t∈T→A≤if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB
83 min2 ⊢2nd⁡F⁡G⁡t∈ℝ∧B∈ℝ→if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB≤B
84 33 34 83 syl2anc ⊢φ∧t∈T→if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB≤B
85 elicc2 ⊢A∈ℝ∧B∈ℝ→if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈AB↔if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈ℝ∧A≤if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∧if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB≤B
86 1 2 85 syl2anc ⊢φ→if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈AB↔if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈ℝ∧A≤if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∧if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB≤B
87 86 adantr ⊢φ∧t∈T→if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈AB↔if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈ℝ∧A≤if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∧if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB≤B
88 35 82 84 87 mpbir3and ⊢φ∧t∈T→if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈AB
89 22 88 sseldd ⊢φ∧t∈T→if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈⋃U
90 eluni2 ⊢if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈⋃U↔∃x∈Uif2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈x
91 89 90 sylib ⊢φ∧t∈T→∃x∈Uif2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈x
92 simprl ⊢φ∧t∈T∧x∈U∧if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈x→x∈U
93 simprr ⊢φ∧t∈T∧x∈U∧if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈x→if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈x
94 88 adantr ⊢φ∧t∈T∧x∈U∧if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈x→if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈AB
95 inelcm ⊢if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈x∧if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈AB→x∩AB≠∅
96 93 94 95 syl2anc ⊢φ∧t∈T∧x∈U∧if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈x→x∩AB≠∅
97 ineq1 ⊢u=x→u∩AB=x∩AB
98 97 neeq1d ⊢u=x→u∩AB≠∅↔x∩AB≠∅
99 98 10 elrab2 ⊢x∈T↔x∈U∧x∩AB≠∅
100 92 96 99 sylanbrc ⊢φ∧t∈T∧x∈U∧if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈x→x∈T
101 91 100 93 reximssdv ⊢φ∧t∈T→∃x∈Tif2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈x
102 101 ralrimiva ⊢φ→∀t∈T∃x∈Tif2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈x
103 eleq2 ⊢x=h⁡t→if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈x↔if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈h⁡t
104 103 ac6sfi ⊢T∈Fin∧∀t∈T∃x∈Tif2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈x→∃hh:T⟶T∧∀t∈Tif2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈h⁡t
105 21 102 104 syl2anc ⊢φ→∃hh:T⟶T∧∀t∈Tif2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈h⁡t
106 105 adantr ⊢φ∧z∈U∧A∈z→∃hh:T⟶T∧∀t∈Tif2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈h⁡t
107 2fveq3 ⊢x=t→F⁡G⁡x=F⁡G⁡t
108 107 fveq2d ⊢x=t→2nd⁡F⁡G⁡x=2nd⁡F⁡G⁡t
109 108 breq1d ⊢x=t→2nd⁡F⁡G⁡x≤B↔2nd⁡F⁡G⁡t≤B
110 109 108 ifbieq1d ⊢x=t→if2nd⁡F⁡G⁡x≤B2nd⁡F⁡G⁡xB=if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB
111 fveq2 ⊢x=t→h⁡x=h⁡t
112 110 111 eleq12d ⊢x=t→if2nd⁡F⁡G⁡x≤B2nd⁡F⁡G⁡xB∈h⁡x↔if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈h⁡t
113 112 cbvralvw ⊢∀x∈Tif2nd⁡F⁡G⁡x≤B2nd⁡F⁡G⁡xB∈h⁡x↔∀t∈Tif2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈h⁡t
114 1 adantr ⊢φ∧z∈U∧A∈z∧h:T⟶T∧∀x∈Tif2nd⁡F⁡G⁡x≤B2nd⁡F⁡G⁡xB∈h⁡x→A∈ℝ
115 2 adantr ⊢φ∧z∈U∧A∈z∧h:T⟶T∧∀x∈Tif2nd⁡F⁡G⁡x≤B2nd⁡F⁡G⁡xB∈h⁡x→B∈ℝ
116 3 adantr ⊢φ∧z∈U∧A∈z∧h:T⟶T∧∀x∈Tif2nd⁡F⁡G⁡x≤B2nd⁡F⁡G⁡xB∈h⁡x→A≤B
117 5 adantr ⊢φ∧z∈U∧A∈z∧h:T⟶T∧∀x∈Tif2nd⁡F⁡G⁡x≤B2nd⁡F⁡G⁡xB∈h⁡x→F:ℕ⟶≤∩ℝ2
118 6 adantr ⊢φ∧z∈U∧A∈z∧h:T⟶T∧∀x∈Tif2nd⁡F⁡G⁡x≤B2nd⁡F⁡G⁡xB∈h⁡x→U∈𝒫ran⁡.∘F∩Fin
119 7 adantr ⊢φ∧z∈U∧A∈z∧h:T⟶T∧∀x∈Tif2nd⁡F⁡G⁡x≤B2nd⁡F⁡G⁡xB∈h⁡x→AB⊆⋃U
120 8 adantr ⊢φ∧z∈U∧A∈z∧h:T⟶T∧∀x∈Tif2nd⁡F⁡G⁡x≤B2nd⁡F⁡G⁡xB∈h⁡x→G:U⟶ℕ
121 9 adantlr ⊢φ∧z∈U∧A∈z∧h:T⟶T∧∀x∈Tif2nd⁡F⁡G⁡x≤B2nd⁡F⁡G⁡xB∈h⁡x∧t∈U→.∘F⁡G⁡t=t
122 simprrl ⊢φ∧z∈U∧A∈z∧h:T⟶T∧∀x∈Tif2nd⁡F⁡G⁡x≤B2nd⁡F⁡G⁡xB∈h⁡x→h:T⟶T
123 simprrr ⊢φ∧z∈U∧A∈z∧h:T⟶T∧∀x∈Tif2nd⁡F⁡G⁡x≤B2nd⁡F⁡G⁡xB∈h⁡x→∀x∈Tif2nd⁡F⁡G⁡x≤B2nd⁡F⁡G⁡xB∈h⁡x
124 112 rspccva ⊢∀x∈Tif2nd⁡F⁡G⁡x≤B2nd⁡F⁡G⁡xB∈h⁡x∧t∈T→if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈h⁡t
125 123 124 sylan ⊢φ∧z∈U∧A∈z∧h:T⟶T∧∀x∈Tif2nd⁡F⁡G⁡x≤B2nd⁡F⁡G⁡xB∈h⁡x∧t∈T→if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈h⁡t
126 simprlr ⊢φ∧z∈U∧A∈z∧h:T⟶T∧∀x∈Tif2nd⁡F⁡G⁡x≤B2nd⁡F⁡G⁡xB∈h⁡x→A∈z
127 simprll ⊢φ∧z∈U∧A∈z∧h:T⟶T∧∀x∈Tif2nd⁡F⁡G⁡x≤B2nd⁡F⁡G⁡xB∈h⁡x→z∈U
128 14 adantr ⊢φ∧z∈U∧A∈z∧h:T⟶T∧∀x∈Tif2nd⁡F⁡G⁡x≤B2nd⁡F⁡G⁡xB∈h⁡x→A∈AB
129 inelcm ⊢A∈z∧A∈AB→z∩AB≠∅
130 126 128 129 syl2anc ⊢φ∧z∈U∧A∈z∧h:T⟶T∧∀x∈Tif2nd⁡F⁡G⁡x≤B2nd⁡F⁡G⁡xB∈h⁡x→z∩AB≠∅
131 ineq1 ⊢u=z→u∩AB=z∩AB
132 131 neeq1d ⊢u=z→u∩AB≠∅↔z∩AB≠∅
133 132 10 elrab2 ⊢z∈T↔z∈U∧z∩AB≠∅
134 127 130 133 sylanbrc ⊢φ∧z∈U∧A∈z∧h:T⟶T∧∀x∈Tif2nd⁡F⁡G⁡x≤B2nd⁡F⁡G⁡xB∈h⁡x→z∈T
135 eqid ⊢seq1h∘1stℕ×z=seq1h∘1stℕ×z
136 fveq2 ⊢m=n→seq1h∘1stℕ×z⁡m=seq1h∘1stℕ×z⁡n
137 136 eleq2d ⊢m=n→B∈seq1h∘1stℕ×z⁡m↔B∈seq1h∘1stℕ×z⁡n
138 137 cbvrabv ⊢m∈ℕ|B∈seq1h∘1stℕ×z⁡m=n∈ℕ|B∈seq1h∘1stℕ×z⁡n
139 eqid ⊢supm∈ℕ|B∈seq1h∘1stℕ×z⁡mℝ<=supm∈ℕ|B∈seq1h∘1stℕ×z⁡mℝ<
140 114 115 116 4 117 118 119 120 121 10 122 125 126 134 135 138 139 ovolicc2lem4 ⊢φ∧z∈U∧A∈z∧h:T⟶T∧∀x∈Tif2nd⁡F⁡G⁡x≤B2nd⁡F⁡G⁡xB∈h⁡x→B−A≤supran⁡Sℝ*<
141 140 anassrs ⊢φ∧z∈U∧A∈z∧h:T⟶T∧∀x∈Tif2nd⁡F⁡G⁡x≤B2nd⁡F⁡G⁡xB∈h⁡x→B−A≤supran⁡Sℝ*<
142 141 expr ⊢φ∧z∈U∧A∈z∧h:T⟶T→∀x∈Tif2nd⁡F⁡G⁡x≤B2nd⁡F⁡G⁡xB∈h⁡x→B−A≤supran⁡Sℝ*<
143 113 142 biimtrrid ⊢φ∧z∈U∧A∈z∧h:T⟶T→∀t∈Tif2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈h⁡t→B−A≤supran⁡Sℝ*<
144 143 expimpd ⊢φ∧z∈U∧A∈z→h:T⟶T∧∀t∈Tif2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈h⁡t→B−A≤supran⁡Sℝ*<
145 144 exlimdv ⊢φ∧z∈U∧A∈z→∃hh:T⟶T∧∀t∈Tif2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈h⁡t→B−A≤supran⁡Sℝ*<
146 106 145 mpd ⊢φ∧z∈U∧A∈z→B−A≤supran⁡Sℝ*<
147 17 146 rexlimddv ⊢φ→B−A≤supran⁡Sℝ*<