Metamath Proof Explorer

Theorem pntlemq

Description: Lemma for pntlemj . (Contributed by Mario Carneiro, 7-Jun-2016)

Ref Expression
Hypotheses pntlem1.r ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
pntlem1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
pntlem1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
pntlem1.l ⊢ ( 𝜑 → 𝐿 ∈ ( 0 (,) 1 ) )
pntlem1.d ⊢ 𝐷 = ( 𝐴 + 1 )
pntlem1.f ⊢ 𝐹 = ( ( 1 − ( 1 / 𝐷 ) ) · ( ( 𝐿 / ( 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) )
pntlem1.u ⊢ ( 𝜑 → 𝑈 ∈ ℝ+ )
pntlem1.u2 ⊢ ( 𝜑 → 𝑈 ≤ 𝐴 )
pntlem1.e ⊢ 𝐸 = ( 𝑈 / 𝐷 )
pntlem1.k ⊢ 𝐾 = ( exp ‘ ( 𝐵 / 𝐸 ) )
pntlem1.y ⊢ ( 𝜑 → ( 𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌 ) )
pntlem1.x ⊢ ( 𝜑 → ( 𝑋 ∈ ℝ+ ∧ 𝑌 < 𝑋 ) )
pntlem1.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
pntlem1.w ⊢ 𝑊 = ( ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) + ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) )
pntlem1.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑊 [,) +∞ ) )
pntlem1.m ⊢ 𝑀 = ( ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) + 1 )
pntlem1.n ⊢ 𝑁 = ( ⌊ ‘ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) )
pntlem1.U ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝑌 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑈 )
pntlem1.K ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑋 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝐾 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
pntlem1.o ⊢ 𝑂 = ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ) )
pntlem1.v ⊢ ( 𝜑 → 𝑉 ∈ ℝ+ )
pntlem1.V ⊢ ( 𝜑 → ( ( ( 𝐾 ↑ 𝐽 ) < 𝑉 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) ) ∧ ∀ 𝑢 ∈ ( 𝑉 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
pntlem1.j ⊢ ( 𝜑 → 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) )
pntlem1.i ⊢ 𝐼 = ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) )
Assertion pntlemq ( 𝜑 → 𝐼 ⊆ 𝑂 )

Proof

Step Hyp Ref Expression
1 pntlem1.r ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
2 pntlem1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
3 pntlem1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
4 pntlem1.l ⊢ ( 𝜑 → 𝐿 ∈ ( 0 (,) 1 ) )
5 pntlem1.d ⊢ 𝐷 = ( 𝐴 + 1 )
6 pntlem1.f ⊢ 𝐹 = ( ( 1 − ( 1 / 𝐷 ) ) · ( ( 𝐿 / ( 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) )
7 pntlem1.u ⊢ ( 𝜑 → 𝑈 ∈ ℝ+ )
8 pntlem1.u2 ⊢ ( 𝜑 → 𝑈 ≤ 𝐴 )
9 pntlem1.e ⊢ 𝐸 = ( 𝑈 / 𝐷 )
10 pntlem1.k ⊢ 𝐾 = ( exp ‘ ( 𝐵 / 𝐸 ) )
11 pntlem1.y ⊢ ( 𝜑 → ( 𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌 ) )
12 pntlem1.x ⊢ ( 𝜑 → ( 𝑋 ∈ ℝ+ ∧ 𝑌 < 𝑋 ) )
13 pntlem1.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
14 pntlem1.w ⊢ 𝑊 = ( ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) + ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) )
15 pntlem1.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑊 [,) +∞ ) )
16 pntlem1.m ⊢ 𝑀 = ( ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) + 1 )
17 pntlem1.n ⊢ 𝑁 = ( ⌊ ‘ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) )
18 pntlem1.U ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝑌 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑈 )
19 pntlem1.K ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑋 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝐾 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
20 pntlem1.o ⊢ 𝑂 = ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ) )
21 pntlem1.v ⊢ ( 𝜑 → 𝑉 ∈ ℝ+ )
22 pntlem1.V ⊢ ( 𝜑 → ( ( ( 𝐾 ↑ 𝐽 ) < 𝑉 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) ) ∧ ∀ 𝑢 ∈ ( 𝑉 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
23 pntlem1.j ⊢ ( 𝜑 → 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) )
24 pntlem1.i ⊢ 𝐼 = ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) )
25 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 pntlemb ⊢ ( 𝜑 → ( 𝑍 ∈ ℝ+ ∧ ( 1 < 𝑍 ∧ e ≤ ( √ ‘ 𝑍 ) ∧ ( √ ‘ 𝑍 ) ≤ ( 𝑍 / 𝑌 ) ) ∧ ( ( 4 / ( 𝐿 · 𝐸 ) ) ≤ ( √ ‘ 𝑍 ) ∧ ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) + 2 ) ≤ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ∧ ( ( 𝑈 · 3 ) + 𝐶 ) ≤ ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) )
26 25 simp1d ⊢ ( 𝜑 → 𝑍 ∈ ℝ+ )
27 1 2 3 4 5 6 7 8 9 10 pntlemc ⊢ ( 𝜑 → ( 𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+ ∧ ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) ) )
28 27 simp2d ⊢ ( 𝜑 → 𝐾 ∈ ℝ+ )
29 elfzoelz ⊢ ( 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐽 ∈ ℤ )
30 23 29 syl ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
31 30 peano2zd ⊢ ( 𝜑 → ( 𝐽 + 1 ) ∈ ℤ )
32 28 31 rpexpcld ⊢ ( 𝜑 → ( 𝐾 ↑ ( 𝐽 + 1 ) ) ∈ ℝ+ )
33 26 32 rpdivcld ⊢ ( 𝜑 → ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ∈ ℝ+ )
34 33 rpred ⊢ ( 𝜑 → ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ∈ ℝ )
35 34 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) ∈ ℤ )
36 1rp ⊢ 1 ∈ ℝ+
37 1 2 3 4 5 6 pntlemd ⊢ ( 𝜑 → ( 𝐿 ∈ ℝ+ ∧ 𝐷 ∈ ℝ+ ∧ 𝐹 ∈ ℝ+ ) )
38 37 simp1d ⊢ ( 𝜑 → 𝐿 ∈ ℝ+ )
39 27 simp1d ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
40 38 39 rpmulcld ⊢ ( 𝜑 → ( 𝐿 · 𝐸 ) ∈ ℝ+ )
41 rpaddcl ⊢ ( ( 1 ∈ ℝ+ ∧ ( 𝐿 · 𝐸 ) ∈ ℝ+ ) → ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℝ+ )
42 36 40 41 sylancr ⊢ ( 𝜑 → ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℝ+ )
43 42 21 rpmulcld ⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ∈ ℝ+ )
44 26 43 rpdivcld ⊢ ( 𝜑 → ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ∈ ℝ+ )
45 44 rpred ⊢ ( 𝜑 → ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ∈ ℝ )
46 45 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ∈ ℤ )
47 43 rpred ⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ∈ ℝ )
48 32 rpred ⊢ ( 𝜑 → ( 𝐾 ↑ ( 𝐽 + 1 ) ) ∈ ℝ )
49 22 simpld ⊢ ( 𝜑 → ( ( 𝐾 ↑ 𝐽 ) < 𝑉 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) ) )
50 49 simprd ⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) )
51 28 rpcnd ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
52 28 30 rpexpcld ⊢ ( 𝜑 → ( 𝐾 ↑ 𝐽 ) ∈ ℝ+ )
53 52 rpcnd ⊢ ( 𝜑 → ( 𝐾 ↑ 𝐽 ) ∈ ℂ )
54 51 53 mulcomd ⊢ ( 𝜑 → ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) = ( ( 𝐾 ↑ 𝐽 ) · 𝐾 ) )
55 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 pntlemg ⊢ ( 𝜑 → ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ≤ ( 𝑁 − 𝑀 ) ) )
56 55 simp1d ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
57 elfzouz ⊢ ( 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐽 ∈ ( ℤ≥ ‘ 𝑀 ) )
58 23 57 syl ⊢ ( 𝜑 → 𝐽 ∈ ( ℤ≥ ‘ 𝑀 ) )
59 eluznn ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝐽 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐽 ∈ ℕ )
60 56 58 59 syl2anc ⊢ ( 𝜑 → 𝐽 ∈ ℕ )
61 60 nnnn0d ⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
62 51 61 expp1d ⊢ ( 𝜑 → ( 𝐾 ↑ ( 𝐽 + 1 ) ) = ( ( 𝐾 ↑ 𝐽 ) · 𝐾 ) )
63 54 62 eqtr4d ⊢ ( 𝜑 → ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) = ( 𝐾 ↑ ( 𝐽 + 1 ) ) )
64 50 63 breqtrd ⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) < ( 𝐾 ↑ ( 𝐽 + 1 ) ) )
65 47 48 64 ltled ⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ≤ ( 𝐾 ↑ ( 𝐽 + 1 ) ) )
66 43 32 26 lediv2d ⊢ ( 𝜑 → ( ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ≤ ( 𝐾 ↑ ( 𝐽 + 1 ) ) ↔ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ≤ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) )
67 65 66 mpbid ⊢ ( 𝜑 → ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ≤ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) )
68 flwordi ⊢ ( ( ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ∈ ℝ ∧ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ∈ ℝ ∧ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ≤ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) → ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) ≤ ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) )
69 34 45 67 68 syl3anc ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) ≤ ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) )
70 eluz2 ⊢ ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) ) ↔ ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) ∈ ℤ ∧ ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ∈ ℤ ∧ ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) ≤ ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) )
71 35 46 69 70 syl3anbrc ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) ) )
72 eluzp1p1 ⊢ ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) ) → ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) + 1 ) ) )
73 fzss1 ⊢ ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) + 1 ) ) → ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ) ⊆ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ) )
74 71 72 73 3syl ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ) ⊆ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ) )
75 26 21 rpdivcld ⊢ ( 𝜑 → ( 𝑍 / 𝑉 ) ∈ ℝ+ )
76 75 rpred ⊢ ( 𝜑 → ( 𝑍 / 𝑉 ) ∈ ℝ )
77 76 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ∈ ℤ )
78 26 52 rpdivcld ⊢ ( 𝜑 → ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ∈ ℝ+ )
79 78 rpred ⊢ ( 𝜑 → ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ∈ ℝ )
80 79 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ) ∈ ℤ )
81 52 rpred ⊢ ( 𝜑 → ( 𝐾 ↑ 𝐽 ) ∈ ℝ )
82 21 rpred ⊢ ( 𝜑 → 𝑉 ∈ ℝ )
83 49 simpld ⊢ ( 𝜑 → ( 𝐾 ↑ 𝐽 ) < 𝑉 )
84 81 82 83 ltled ⊢ ( 𝜑 → ( 𝐾 ↑ 𝐽 ) ≤ 𝑉 )
85 52 21 26 lediv2d ⊢ ( 𝜑 → ( ( 𝐾 ↑ 𝐽 ) ≤ 𝑉 ↔ ( 𝑍 / 𝑉 ) ≤ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ) )
86 84 85 mpbid ⊢ ( 𝜑 → ( 𝑍 / 𝑉 ) ≤ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) )
87 flwordi ⊢ ( ( ( 𝑍 / 𝑉 ) ∈ ℝ ∧ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ∈ ℝ ∧ ( 𝑍 / 𝑉 ) ≤ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ) → ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ≤ ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ) )
88 76 79 86 87 syl3anc ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ≤ ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ) )
89 eluz2 ⊢ ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ) ↔ ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ∈ ℤ ∧ ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ) ∈ ℤ ∧ ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ≤ ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ) ) )
90 77 80 88 89 syl3anbrc ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ) )
91 fzss2 ⊢ ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ) → ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ) ⊆ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ) ) )
92 90 91 syl ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ) ⊆ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ) ) )
93 74 92 sstrd ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ) ⊆ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ) ) )
94 93 24 20 3sstr4g ⊢ ( 𝜑 → 𝐼 ⊆ 𝑂 )