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 ffvelrnda ⊢ φ ∧ 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 ffvelrnd ⊢ φ ∧ N ∈ ℕ → G ⁡ K ⁡ N ∈ ℕ
33 21 32 ffvelrnd ⊢ φ ∧ 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 simpr ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ∧ x ∈ K ⁡ N ∩ A B → x ∈ K ⁡ N ∩ A B
48 elin ⊢ x ∈ K ⁡ N ∩ A B ↔ x ∈ K ⁡ N ∧ x ∈ A B
49 47 48 sylib ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ∧ x ∈ K ⁡ N ∩ A B → x ∈ K ⁡ N ∧ x ∈ A B
50 49 simprd ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ∧ x ∈ K ⁡ N ∩ A B → x ∈ A B
51 elicc2 ⊢ A ∈ ℝ ∧ B ∈ ℝ → x ∈ A B ↔ x ∈ ℝ ∧ A ≤ x ∧ x ≤ B
52 1 2 51 syl2anc ⊢ φ → x ∈ A B ↔ x ∈ ℝ ∧ A ≤ x ∧ x ≤ B
53 52 ad2antrr ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ∧ x ∈ K ⁡ N ∩ A B → x ∈ A B ↔ x ∈ ℝ ∧ A ≤ x ∧ x ≤ B
54 50 53 mpbid ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ∧ x ∈ K ⁡ N ∩ A B → x ∈ ℝ ∧ A ≤ x ∧ x ≤ B
55 54 simp1d ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ∧ x ∈ K ⁡ N ∩ A B → x ∈ ℝ
56 2 ad2antrr ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ∧ x ∈ K ⁡ N ∩ A B → B ∈ ℝ
57 49 simpld ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ∧ x ∈ K ⁡ N ∩ A B → x ∈ K ⁡ N
58 39 simpld ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ 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 ∈ ℝ ∧ 1 st ⁡ F ⁡ G ⁡ K ⁡ N < x ∧ x < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N
60 58 59 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
61 60 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
62 57 61 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
63 62 simp2d ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ∧ x ∈ K ⁡ N ∩ A B → 1 st ⁡ F ⁡ G ⁡ K ⁡ N < x
64 54 simp3d ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ∧ x ∈ K ⁡ N ∩ A B → x ≤ B
65 46 55 56 63 64 ltletrd ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ∧ x ∈ K ⁡ N ∩ A B → 1 st ⁡ F ⁡ G ⁡ K ⁡ N < B
66 42 65 exlimddv ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N → 1 st ⁡ F ⁡ G ⁡ K ⁡ N < B
67 simprr ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N → B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N
68 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
69 58 68 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
70 38 66 67 69 mpbir3and ⊢ φ ∧ N ∈ ℕ ∧ B < 2 nd ⁡ 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 < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N → N ∈ W
75 74 expr ⊢ φ ∧ N ∈ ℕ → B < 2 nd ⁡ F ⁡ G ⁡ K ⁡ N → N ∈ W
76 36 75 sylbird ⊢ φ ∧ N ∈ ℕ → ¬ 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ≤ B → N ∈ W
77 76 con1d ⊢ φ ∧ N ∈ ℕ → ¬ N ∈ W → 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ≤ B
78 77 impr ⊢ φ ∧ N ∈ ℕ ∧ ¬ N ∈ W → 2 nd ⁡ F ⁡ G ⁡ K ⁡ N ≤ B