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 ( 𝜑𝐼𝑂 )