Metamath Proof Explorer

Theorem ovolicc2lem2

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

Ref Expression
Hypotheses ovolicc.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ovolicc.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
ovolicc.3 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
ovolicc2.4 ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
ovolicc2.5 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
ovolicc2.6 ⊢ ( 𝜑 → 𝑈 ∈ ( 𝒫 ran ( (,) ∘ 𝐹 ) ∩ Fin ) )
ovolicc2.7 ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑈 )
ovolicc2.8 ⊢ ( 𝜑 → 𝐺 : 𝑈 ⟶ ℕ )
ovolicc2.9 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑈 ) → ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑡 ) ) = 𝑡 )
ovolicc2.10 ⊢ 𝑇 = { 𝑢 ∈ 𝑈 ∣ ( 𝑢 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ }
ovolicc2.11 ⊢ ( 𝜑 → 𝐻 : 𝑇 ⟶ 𝑇 )
ovolicc2.12 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → if ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( 𝐻 ‘ 𝑡 ) )
ovolicc2.13 ⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
ovolicc2.14 ⊢ ( 𝜑 → 𝐶 ∈ 𝑇 )
ovolicc2.15 ⊢ 𝐾 = seq 1 ( ( 𝐻 ∘ 1st ) , ( ℕ × { 𝐶 } ) )
ovolicc2.16 ⊢ 𝑊 = { 𝑛 ∈ ℕ ∣ 𝐵 ∈ ( 𝐾 ‘ 𝑛 ) }
Assertion ovolicc2lem2 ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ ¬ 𝑁 ∈ 𝑊 ) ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ≤ 𝐵 )

Proof

Step Hyp Ref Expression
1 ovolicc.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 ovolicc.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 ovolicc.3 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
4 ovolicc2.4 ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
5 ovolicc2.5 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
6 ovolicc2.6 ⊢ ( 𝜑 → 𝑈 ∈ ( 𝒫 ran ( (,) ∘ 𝐹 ) ∩ Fin ) )
7 ovolicc2.7 ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑈 )
8 ovolicc2.8 ⊢ ( 𝜑 → 𝐺 : 𝑈 ⟶ ℕ )
9 ovolicc2.9 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑈 ) → ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑡 ) ) = 𝑡 )
10 ovolicc2.10 ⊢ 𝑇 = { 𝑢 ∈ 𝑈 ∣ ( 𝑢 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ }
11 ovolicc2.11 ⊢ ( 𝜑 → 𝐻 : 𝑇 ⟶ 𝑇 )
12 ovolicc2.12 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → if ( ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( 𝐻 ‘ 𝑡 ) )
13 ovolicc2.13 ⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
14 ovolicc2.14 ⊢ ( 𝜑 → 𝐶 ∈ 𝑇 )
15 ovolicc2.15 ⊢ 𝐾 = seq 1 ( ( 𝐻 ∘ 1st ) , ( ℕ × { 𝐶 } ) )
16 ovolicc2.16 ⊢ 𝑊 = { 𝑛 ∈ ℕ ∣ 𝐵 ∈ ( 𝐾 ‘ 𝑛 ) }
17 2 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → 𝐵 ∈ ℝ )
18 inss2 ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
19 fss ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ ) ) → 𝐹 : ℕ ⟶ ( ℝ × ℝ ) )
20 5 18 19 sylancl ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ℝ × ℝ ) )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → 𝐹 : ℕ ⟶ ( ℝ × ℝ ) )
22 8 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → 𝐺 : 𝑈 ⟶ ℕ )
23 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
24 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
25 23 15 24 14 11 algrf ⊢ ( 𝜑 → 𝐾 : ℕ ⟶ 𝑇 )
26 25 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( 𝐾 ‘ 𝑁 ) ∈ 𝑇 )
27 ineq1 ⊢ ( 𝑢 = ( 𝐾 ‘ 𝑁 ) → ( 𝑢 ∩ ( 𝐴 [,] 𝐵 ) ) = ( ( 𝐾 ‘ 𝑁 ) ∩ ( 𝐴 [,] 𝐵 ) ) )
28 27 neeq1d ⊢ ( 𝑢 = ( 𝐾 ‘ 𝑁 ) → ( ( 𝑢 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ ↔ ( ( 𝐾 ‘ 𝑁 ) ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ ) )
29 28 10 elrab2 ⊢ ( ( 𝐾 ‘ 𝑁 ) ∈ 𝑇 ↔ ( ( 𝐾 ‘ 𝑁 ) ∈ 𝑈 ∧ ( ( 𝐾 ‘ 𝑁 ) ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ ) )
30 26 29 sylib ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( ( 𝐾 ‘ 𝑁 ) ∈ 𝑈 ∧ ( ( 𝐾 ‘ 𝑁 ) ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ ) )
31 30 simpld ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( 𝐾 ‘ 𝑁 ) ∈ 𝑈 )
32 22 31 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ∈ ℕ )
33 21 32 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ∈ ( ℝ × ℝ ) )
34 xp2nd ⊢ ( ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ∈ ( ℝ × ℝ ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ∈ ℝ )
35 33 34 syl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ∈ ℝ )
36 17 35 ltnled ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ↔ ¬ ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ≤ 𝐵 ) )
37 simprl ⊢ ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) → 𝑁 ∈ ℕ )
38 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) → 𝐵 ∈ ℝ )
39 30 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) → ( ( 𝐾 ‘ 𝑁 ) ∈ 𝑈 ∧ ( ( 𝐾 ‘ 𝑁 ) ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ ) )
40 39 simprd ⊢ ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) → ( ( 𝐾 ‘ 𝑁 ) ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ )
41 n0 ⊢ ( ( ( 𝐾 ‘ 𝑁 ) ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( ( 𝐾 ‘ 𝑁 ) ∩ ( 𝐴 [,] 𝐵 ) ) )
42 40 41 sylib ⊢ ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) → ∃ 𝑥 𝑥 ∈ ( ( 𝐾 ‘ 𝑁 ) ∩ ( 𝐴 [,] 𝐵 ) ) )
43 xp1st ⊢ ( ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ∈ ( ℝ × ℝ ) → ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ∈ ℝ )
44 33 43 syl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ∈ ℝ )
45 44 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) → ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ∈ ℝ )
46 45 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) ∧ 𝑥 ∈ ( ( 𝐾 ‘ 𝑁 ) ∩ ( 𝐴 [,] 𝐵 ) ) ) → ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ∈ ℝ )
47 elin ⊢ ( 𝑥 ∈ ( ( 𝐾 ‘ 𝑁 ) ∩ ( 𝐴 [,] 𝐵 ) ) ↔ ( 𝑥 ∈ ( 𝐾 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) )
48 47 bilani ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) ∧ 𝑥 ∈ ( ( 𝐾 ‘ 𝑁 ) ∩ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑥 ∈ ( 𝐾 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) )
49 48 simprd ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) ∧ 𝑥 ∈ ( ( 𝐾 ‘ 𝑁 ) ∩ ( 𝐴 [,] 𝐵 ) ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
50 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
51 1 2 50 syl2anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
52 51 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) ∧ 𝑥 ∈ ( ( 𝐾 ‘ 𝑁 ) ∩ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
53 49 52 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) ∧ 𝑥 ∈ ( ( 𝐾 ‘ 𝑁 ) ∩ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) )
54 53 simp1d ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) ∧ 𝑥 ∈ ( ( 𝐾 ‘ 𝑁 ) ∩ ( 𝐴 [,] 𝐵 ) ) ) → 𝑥 ∈ ℝ )
55 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) ∧ 𝑥 ∈ ( ( 𝐾 ‘ 𝑁 ) ∩ ( 𝐴 [,] 𝐵 ) ) ) → 𝐵 ∈ ℝ )
56 48 simpld ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) ∧ 𝑥 ∈ ( ( 𝐾 ‘ 𝑁 ) ∩ ( 𝐴 [,] 𝐵 ) ) ) → 𝑥 ∈ ( 𝐾 ‘ 𝑁 ) )
57 39 simpld ⊢ ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) → ( 𝐾 ‘ 𝑁 ) ∈ 𝑈 )
58 1 2 3 4 5 6 7 8 9 ovolicc2lem1 ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝑁 ) ∈ 𝑈 ) → ( 𝑥 ∈ ( 𝐾 ‘ 𝑁 ) ↔ ( 𝑥 ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) )
59 57 58 syldan ⊢ ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) → ( 𝑥 ∈ ( 𝐾 ‘ 𝑁 ) ↔ ( 𝑥 ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) )
60 59 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) ∧ 𝑥 ∈ ( ( 𝐾 ‘ 𝑁 ) ∩ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑥 ∈ ( 𝐾 ‘ 𝑁 ) ↔ ( 𝑥 ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) )
61 56 60 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) ∧ 𝑥 ∈ ( ( 𝐾 ‘ 𝑁 ) ∩ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑥 ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) < 𝑥 ∧ 𝑥 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) )
62 61 simp2d ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) ∧ 𝑥 ∈ ( ( 𝐾 ‘ 𝑁 ) ∩ ( 𝐴 [,] 𝐵 ) ) ) → ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) < 𝑥 )
63 53 simp3d ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) ∧ 𝑥 ∈ ( ( 𝐾 ‘ 𝑁 ) ∩ ( 𝐴 [,] 𝐵 ) ) ) → 𝑥 ≤ 𝐵 )
64 46 54 55 62 63 ltletrd ⊢ ( ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) ∧ 𝑥 ∈ ( ( 𝐾 ‘ 𝑁 ) ∩ ( 𝐴 [,] 𝐵 ) ) ) → ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) < 𝐵 )
65 42 64 exlimddv ⊢ ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) → ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) < 𝐵 )
66 simprr ⊢ ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) → 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) )
67 1 2 3 4 5 6 7 8 9 ovolicc2lem1 ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝑁 ) ∈ 𝑈 ) → ( 𝐵 ∈ ( 𝐾 ‘ 𝑁 ) ↔ ( 𝐵 ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) < 𝐵 ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) )
68 57 67 syldan ⊢ ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) → ( 𝐵 ∈ ( 𝐾 ‘ 𝑁 ) ↔ ( 𝐵 ∈ ℝ ∧ ( 1st ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) < 𝐵 ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) )
69 38 65 66 68 mpbir3and ⊢ ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) → 𝐵 ∈ ( 𝐾 ‘ 𝑁 ) )
70 fveq2 ⊢ ( 𝑛 = 𝑁 → ( 𝐾 ‘ 𝑛 ) = ( 𝐾 ‘ 𝑁 ) )
71 70 eleq2d ⊢ ( 𝑛 = 𝑁 → ( 𝐵 ∈ ( 𝐾 ‘ 𝑛 ) ↔ 𝐵 ∈ ( 𝐾 ‘ 𝑁 ) ) )
72 71 16 elrab2 ⊢ ( 𝑁 ∈ 𝑊 ↔ ( 𝑁 ∈ ℕ ∧ 𝐵 ∈ ( 𝐾 ‘ 𝑁 ) ) )
73 37 69 72 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ) ) → 𝑁 ∈ 𝑊 )
74 73 expr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( 𝐵 < ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) → 𝑁 ∈ 𝑊 ) )
75 36 74 sylbird ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( ¬ ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ≤ 𝐵 → 𝑁 ∈ 𝑊 ) )
76 75 con1d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( ¬ 𝑁 ∈ 𝑊 → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ≤ 𝐵 ) )
77 76 impr ⊢ ( ( 𝜑 ∧ ( 𝑁 ∈ ℕ ∧ ¬ 𝑁 ∈ 𝑊 ) ) → ( 2nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ ( 𝐾 ‘ 𝑁 ) ) ) ) ≤ 𝐵 )