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 = seq 1 + abs ∘ − ∘ F
ovolicc2.5 ⊢ φ → F : ℕ ⟶ ≤ ∩ ℝ 2
ovolicc2.6 ⊢ φ → U ∈ 𝒫 ran ⁡ . ∘ F ∩ Fin
ovolicc2.7 ⊢ φ → A B ⊆ ⋃ U
ovolicc2.8 ⊢ φ → G : U ⟶ ℕ
ovolicc2.9 ⊢ φ ∧ t ∈ U → . ∘ F ⁡ G ⁡ t = t
ovolicc2.10 ⊢ T = u ∈ U | u ∩ A B ≠ ∅
ovolicc2.11 ⊢ φ → H : T ⟶ T
ovolicc2.12 ⊢ φ ∧ t ∈ T → if 2 nd ⁡ F ⁡ G ⁡ t ≤ B 2 nd ⁡ F ⁡ G ⁡ t B ∈ H ⁡ t
ovolicc2.13 ⊢ φ → A ∈ C
ovolicc2.14 ⊢ φ → C ∈ T
ovolicc2.15 ⊢ K = seq 1 H ∘ 1 st ℕ × C
ovolicc2.16 ⊢ W = n ∈ ℕ | B ∈ K ⁡ n
Assertion ovolicc2lem2 ⊢ φ ∧ N ∈ ℕ ∧ ¬ N ∈ W → 2 nd ⁡ 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 = seq 1 + abs ∘ − ∘ F
5 ovolicc2.5 ⊢ φ → F : ℕ ⟶ ≤ ∩ ℝ 2
6 ovolicc2.6 ⊢ φ → U ∈ 𝒫 ran ⁡ . ∘ F ∩ Fin
7 ovolicc2.7 ⊢ φ → A B ⊆ ⋃ U
8 ovolicc2.8 ⊢ φ → G : U ⟶ ℕ
9 ovolicc2.9 ⊢ φ ∧ t ∈ U → . ∘ F ⁡ G ⁡ t = t
10 ovolicc2.10 ⊢ T = u ∈ U | u ∩ A B ≠ ∅
11 ovolicc2.11 ⊢ φ → H : T ⟶ T
12 ovolicc2.12 ⊢ φ ∧ t ∈ T → if 2 nd ⁡ F ⁡ G ⁡ t ≤ B 2 nd ⁡ F ⁡ G ⁡ t B ∈ H ⁡ t
13 ovolicc2.13 ⊢ φ → A ∈ C
14 ovolicc2.14 ⊢ φ → C ∈ T
15 ovolicc2.15 ⊢ K = seq 1 H ∘ 1 st ℕ × 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 ∩ A B = K ⁡ N ∩ A B
28 27 neeq1d ⊢ u = K ⁡ N → u ∩ A B ≠ ∅ ↔ K ⁡ N ∩ A B ≠ ∅
29 28 10 elrab2 ⊢ K ⁡ N ∈ T ↔ K ⁡ N ∈ U ∧ K ⁡ N ∩ A B ≠ ∅
30 26 29 sylib ⊢ φ ∧ N ∈ ℕ → K ⁡ N ∈ U ∧ K ⁡ N ∩ A B ≠ ∅
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 → 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ∈ ℝ
35 33 34 syl ⊢ φ ∧ N ∈ ℕ → 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ∈ ℝ
36 17 35 ltnled ⊢ φ ∧ N ∈ ℕ → B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ↔ ¬ 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ≤ B
37 simprl ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N → N ∈ ℕ
38 2 adantr ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N → B ∈ ℝ
39 30 adantrr ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N → K ⁡ N ∈ U ∧ K ⁡ N ∩ A B ≠ ∅
40 39 simprd ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N → K ⁡ N ∩ A B ≠ ∅
41 n0 ⊢ K ⁡ N ∩ A B ≠ ∅ ↔ ∃ x x ∈ K ⁡ N ∩ A B
42 40 41 sylib ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N → ∃ x x ∈ K ⁡ N ∩ A B
43 xp1st ⊢ F ⁡ G ⁡ K ⁡ N ∈ ℝ 2 → 1 st ⁡ F ⁡ G ⁡ K ⁡ N ∈ ℝ
44 33 43 syl ⊢ φ ∧ N ∈ ℕ → 1 st ⁡ F ⁡ G ⁡ K ⁡ N ∈ ℝ
45 44 adantrr ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N → 1 st ⁡ F ⁡ G ⁡ K ⁡ N ∈ ℝ
46 45 adantr ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ∧ x ∈ K ⁡ N ∩ A B → 1 st ⁡ F ⁡ G ⁡ K ⁡ N ∈ ℝ
47 elin ⊢ x ∈ K ⁡ N ∩ A B ↔ x ∈ K ⁡ N ∧ x ∈ A B
48 47 bilani ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ∧ x ∈ K ⁡ N ∩ A B → x ∈ K ⁡ N ∧ x ∈ A B
49 48 simprd ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ∧ x ∈ K ⁡ N ∩ A B → x ∈ A B
50 elicc2 ⊢ A ∈ ℝ ∧ B ∈ ℝ → x ∈ A B ↔ x ∈ ℝ ∧ A ≤ x ∧ x ≤ B
51 1 2 50 syl2anc ⊢ φ → x ∈ A B ↔ x ∈ ℝ ∧ A ≤ x ∧ x ≤ B
52 51 ad2antrr ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ∧ x ∈ K ⁡ N ∩ A B → x ∈ A B ↔ x ∈ ℝ ∧ A ≤ x ∧ x ≤ B
53 49 52 mpbid ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ∧ x ∈ K ⁡ N ∩ A B → x ∈ ℝ ∧ A ≤ x ∧ x ≤ B
54 53 simp1d ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ∧ x ∈ K ⁡ N ∩ A B → x ∈ ℝ
55 2 ad2antrr ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ∧ x ∈ K ⁡ N ∩ A B → B ∈ ℝ
56 48 simpld ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ∧ x ∈ K ⁡ N ∩ A B → x ∈ K ⁡ N
57 39 simpld ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N → K ⁡ N ∈ U
58 1 2 3 4 5 6 7 8 9 ovolicc2lem1 ⊢ φ ∧ K ⁡ N ∈ U → x ∈ K ⁡ N ↔ x ∈ ℝ ∧ 1 st ⁡ F ⁡ G ⁡ K ⁡ N < x ∧ x < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N
59 57 58 syldan ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N → x ∈ K ⁡ N ↔ x ∈ ℝ ∧ 1 st ⁡ F ⁡ G ⁡ K ⁡ N < x ∧ x < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N
60 59 adantr ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ∧ x ∈ K ⁡ N ∩ A B → x ∈ K ⁡ N ↔ x ∈ ℝ ∧ 1 st ⁡ F ⁡ G ⁡ K ⁡ N < x ∧ x < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N
61 56 60 mpbid ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ∧ x ∈ K ⁡ N ∩ A B → x ∈ ℝ ∧ 1 st ⁡ F ⁡ G ⁡ K ⁡ N < x ∧ x < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N
62 61 simp2d ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ∧ x ∈ K ⁡ N ∩ A B → 1 st ⁡ F ⁡ G ⁡ K ⁡ N < x
63 53 simp3d ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ∧ x ∈ K ⁡ N ∩ A B → x ≤ B
64 46 54 55 62 63 ltletrd ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ∧ x ∈ K ⁡ N ∩ A B → 1 st ⁡ F ⁡ G ⁡ K ⁡ N < B
65 42 64 exlimddv ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N → 1 st ⁡ F ⁡ G ⁡ K ⁡ N < B
66 simprr ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N → B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N
67 1 2 3 4 5 6 7 8 9 ovolicc2lem1 ⊢ φ ∧ K ⁡ N ∈ U → B ∈ K ⁡ N ↔ B ∈ ℝ ∧ 1 st ⁡ F ⁡ G ⁡ K ⁡ N < B ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N
68 57 67 syldan ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N → B ∈ K ⁡ N ↔ B ∈ ℝ ∧ 1 st ⁡ F ⁡ G ⁡ K ⁡ N < B ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N
69 38 65 66 68 mpbir3and ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N → B ∈ K ⁡ N
70 fveq2 ⊢ n = N → K ⁡ n = K ⁡ N
71 70 eleq2d ⊢ n = N → B ∈ K ⁡ n ↔ B ∈ K ⁡ N
72 71 16 elrab2 ⊢ N ∈ W ↔ N ∈ ℕ ∧ B ∈ K ⁡ N
73 37 69 72 sylanbrc ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N → N ∈ W
74 73 expr ⊢ φ ∧ N ∈ ℕ → B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N → N ∈ W
75 36 74 sylbird ⊢ φ ∧ N ∈ ℕ → ¬ 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ≤ B → N ∈ W
76 75 con1d ⊢ φ ∧ N ∈ ℕ → ¬ N ∈ W → 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ≤ B
77 76 impr ⊢ φ ∧ N ∈ ℕ ∧ ¬ N ∈ W → 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ≤ B