Metamath Proof Explorer

Theorem ovolicc2lem2

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≠∅
ovolicc2.11 ⊢φ→H:T⟶T
ovolicc2.12 ⊢φ∧t∈T→if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈H⁡t
ovolicc2.13 ⊢φ→A∈C
ovolicc2.14 ⊢φ→C∈T
ovolicc2.15 ⊢K=seq1H∘1stℕ×C
ovolicc2.16 ⊢W=n∈ℕ|B∈K⁡n
Assertion ovolicc2lem2 ⊢φ∧N∈ℕ∧¬N∈W→2nd⁡F⁡G⁡K⁡N≤B

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 ovolicc2.11 ⊢φ→H:T⟶T
12 ovolicc2.12 ⊢φ∧t∈T→if2nd⁡F⁡G⁡t≤B2nd⁡F⁡G⁡tB∈H⁡t
13 ovolicc2.13 ⊢φ→A∈C
14 ovolicc2.14 ⊢φ→C∈T
15 ovolicc2.15 ⊢K=seq1H∘1stℕ×C
16 ovolicc2.16 ⊢W=n∈ℕ|B∈K⁡n
17 2 adantr ⊢φ∧N∈ℕ→B∈ℝ
18 inss2 ⊢≤∩ℝ2⊆ℝ2
19 fss ⊢F:ℕ⟶≤∩ℝ2∧≤∩ℝ2⊆ℝ2→F:ℕ⟶ℝ2
20 5 18 19 sylancl ⊢φ→F:ℕ⟶ℝ2
21 20 adantr ⊢φ∧N∈ℕ→F:ℕ⟶ℝ2
22 8 adantr ⊢φ∧N∈ℕ→G:U⟶ℕ
23 nnuz ⊢ℕ=ℤ≥1
24 1zzd ⊢φ→1∈ℤ
25 23 15 24 14 11 algrf ⊢φ→K:ℕ⟶T
26 25 ffvelcdmda ⊢φ∧N∈ℕ→K⁡N∈T
27 ineq1 ⊢u=K⁡N→u∩AB=K⁡N∩AB
28 27 neeq1d ⊢u=K⁡N→u∩AB≠∅↔K⁡N∩AB≠∅
29 28 10 elrab2 ⊢K⁡N∈T↔K⁡N∈U∧K⁡N∩AB≠∅
30 26 29 sylib ⊢φ∧N∈ℕ→K⁡N∈U∧K⁡N∩AB≠∅
31 30 simpld ⊢φ∧N∈ℕ→K⁡N∈U
32 22 31 ffvelcdmd ⊢φ∧N∈ℕ→G⁡K⁡N∈ℕ
33 21 32 ffvelcdmd ⊢φ∧N∈ℕ→F⁡G⁡K⁡N∈ℝ2
34 xp2nd ⊢F⁡G⁡K⁡N∈ℝ2→2nd⁡F⁡G⁡K⁡N∈ℝ
35 33 34 syl ⊢φ∧N∈ℕ→2nd⁡F⁡G⁡K⁡N∈ℝ
36 17 35 ltnled ⊢φ∧N∈ℕ→B<2nd⁡F⁡G⁡K⁡N↔¬2nd⁡F⁡G⁡K⁡N≤B
37 simprl ⊢φ∧N∈ℕ∧B<2nd⁡F⁡G⁡K⁡N→N∈ℕ
38 2 adantr ⊢φ∧N∈ℕ∧B<2nd⁡F⁡G⁡K⁡N→B∈ℝ
39 30 adantrr ⊢φ∧N∈ℕ∧B<2nd⁡F⁡G⁡K⁡N→K⁡N∈U∧K⁡N∩AB≠∅
40 39 simprd ⊢φ∧N∈ℕ∧B<2nd⁡F⁡G⁡K⁡N→K⁡N∩AB≠∅
41 n0 ⊢K⁡N∩AB≠∅↔∃xx∈K⁡N∩AB
42 40 41 sylib ⊢φ∧N∈ℕ∧B<2nd⁡F⁡G⁡K⁡N→∃xx∈K⁡N∩AB
43 xp1st ⊢F⁡G⁡K⁡N∈ℝ2→1st⁡F⁡G⁡K⁡N∈ℝ
44 33 43 syl ⊢φ∧N∈ℕ→1st⁡F⁡G⁡K⁡N∈ℝ
45 44 adantrr ⊢φ∧N∈ℕ∧B<2nd⁡F⁡G⁡K⁡N→1st⁡F⁡G⁡K⁡N∈ℝ
46 45 adantr ⊢φ∧N∈ℕ∧B<2nd⁡F⁡G⁡K⁡N∧x∈K⁡N∩AB→1st⁡F⁡G⁡K⁡N∈ℝ
47 simpr ⊢φ∧N∈ℕ∧B<2nd⁡F⁡G⁡K⁡N∧x∈K⁡N∩AB→x∈K⁡N∩AB
48 elin ⊢x∈K⁡N∩AB↔x∈K⁡N∧x∈AB
49 47 48 sylib ⊢φ∧N∈ℕ∧B<2nd⁡F⁡G⁡K⁡N∧x∈K⁡N∩AB→x∈K⁡N∧x∈AB
50 49 simprd ⊢φ∧N∈ℕ∧B<2nd⁡F⁡G⁡K⁡N∧x∈K⁡N∩AB→x∈AB
51 elicc2 ⊢A∈ℝ∧B∈ℝ→x∈AB↔x∈ℝ∧A≤x∧x≤B
52 1 2 51 syl2anc ⊢φ→x∈AB↔x∈ℝ∧A≤x∧x≤B
53 52 ad2antrr ⊢φ∧N∈ℕ∧B<2nd⁡F⁡G⁡K⁡N∧x∈K⁡N∩AB→x∈AB↔x∈ℝ∧A≤x∧x≤B
54 50 53 mpbid ⊢φ∧N∈ℕ∧B<2nd⁡F⁡G⁡K⁡N∧x∈K⁡N∩AB→x∈ℝ∧A≤x∧x≤B
55 54 simp1d ⊢φ∧N∈ℕ∧B<2nd⁡F⁡G⁡K⁡N∧x∈K⁡N∩AB→x∈ℝ
56 2 ad2antrr ⊢φ∧N∈ℕ∧B<2nd⁡F⁡G⁡K⁡N∧x∈K⁡N∩AB→B∈ℝ
57 49 simpld ⊢φ∧N∈ℕ∧B<2nd⁡F⁡G⁡K⁡N∧x∈K⁡N∩AB→x∈K⁡N
58 39 simpld ⊢φ∧N∈ℕ∧B<2nd⁡F⁡G⁡K⁡N→K⁡N∈U
59 1 2 3 4 5 6 7 8 9 ovolicc2lem1 ⊢φ∧K⁡N∈U→x∈K⁡N↔x∈ℝ∧1st⁡F⁡G⁡K⁡N<x∧x<2nd⁡F⁡G⁡K⁡N
60 58 59 syldan ⊢φ∧N∈ℕ∧B<2nd⁡F⁡G⁡K⁡N→x∈K⁡N↔x∈ℝ∧1st⁡F⁡G⁡K⁡N<x∧x<2nd⁡F⁡G⁡K⁡N
61 60 adantr ⊢φ∧N∈ℕ∧B<2nd⁡F⁡G⁡K⁡N∧x∈K⁡N∩AB→x∈K⁡N↔x∈ℝ∧1st⁡F⁡G⁡K⁡N<x∧x<2nd⁡F⁡G⁡K⁡N
62 57 61 mpbid ⊢φ∧N∈ℕ∧B<2nd⁡F⁡G⁡K⁡N∧x∈K⁡N∩AB→x∈ℝ∧1st⁡F⁡G⁡K⁡N<x∧x<2nd⁡F⁡G⁡K⁡N
63 62 simp2d ⊢φ∧N∈ℕ∧B<2nd⁡F⁡G⁡K⁡N∧x∈K⁡N∩AB→1st⁡F⁡G⁡K⁡N<x
64 54 simp3d ⊢φ∧N∈ℕ∧B<2nd⁡F⁡G⁡K⁡N∧x∈K⁡N∩AB→x≤B
65 46 55 56 63 64 ltletrd ⊢φ∧N∈ℕ∧B<2nd⁡F⁡G⁡K⁡N∧x∈K⁡N∩AB→1st⁡F⁡G⁡K⁡N<B
66 42 65 exlimddv ⊢φ∧N∈ℕ∧B<2nd⁡F⁡G⁡K⁡N→1st⁡F⁡G⁡K⁡N<B
67 simprr ⊢φ∧N∈ℕ∧B<2nd⁡F⁡G⁡K⁡N→B<2nd⁡F⁡G⁡K⁡N
68 1 2 3 4 5 6 7 8 9 ovolicc2lem1 ⊢φ∧K⁡N∈U→B∈K⁡N↔B∈ℝ∧1st⁡F⁡G⁡K⁡N<B∧B<2nd⁡F⁡G⁡K⁡N
69 58 68 syldan ⊢φ∧N∈ℕ∧B<2nd⁡F⁡G⁡K⁡N→B∈K⁡N↔B∈ℝ∧1st⁡F⁡G⁡K⁡N<B∧B<2nd⁡F⁡G⁡K⁡N
70 38 66 67 69 mpbir3and ⊢φ∧N∈ℕ∧B<2nd⁡F⁡G⁡K⁡N→B∈K⁡N
71 fveq2 ⊢n=N→K⁡n=K⁡N
72 71 eleq2d ⊢n=N→B∈K⁡n↔B∈K⁡N
73 72 16 elrab2 ⊢N∈W↔N∈ℕ∧B∈K⁡N
74 37 70 73 sylanbrc ⊢φ∧N∈ℕ∧B<2nd⁡F⁡G⁡K⁡N→N∈W
75 74 expr ⊢φ∧N∈ℕ→B<2nd⁡F⁡G⁡K⁡N→N∈W
76 36 75 sylbird ⊢φ∧N∈ℕ→¬2nd⁡F⁡G⁡K⁡N≤B→N∈W
77 76 con1d ⊢φ∧N∈ℕ→¬N∈W→2nd⁡F⁡G⁡K⁡N≤B
78 77 impr ⊢φ∧N∈ℕ∧¬N∈W→2nd⁡F⁡G⁡K⁡N≤B