Metamath Proof Explorer

Theorem fourierdlem63

Description: The upper bound of intervals in the moved partition are mapped to points that are not greater than the corresponding upper bounds in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem63.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
fourierdlem63.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem63.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem63.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
fourierdlem63.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
fourierdlem63.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
fourierdlem63.cltd ⊢ ( 𝜑 → 𝐶 < 𝐷 )
fourierdlem63.o ⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem63.h ⊢ 𝐻 = ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
fourierdlem63.n ⊢ 𝑁 = ( ( ♯ ‘ 𝐻 ) − 1 )
fourierdlem63.s ⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
fourierdlem63.e ⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
fourierdlem63.k ⊢ ( 𝜑 → 𝐾 ∈ ( 0 ... 𝑀 ) )
fourierdlem63.j ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ 𝑁 ) )
fourierdlem63.y ⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝑆 ‘ 𝐽 ) [,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
fourierdlem63.eyltqk ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑌 ) < ( 𝑄 ‘ 𝐾 ) )
fourierdlem63.x ⊢ 𝑋 = ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) )
Assertion fourierdlem63 ( 𝜑 → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ≤ ( 𝑄 ‘ 𝐾 ) )

Proof

Step Hyp Ref Expression
1 fourierdlem63.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
2 fourierdlem63.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
3 fourierdlem63.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
4 fourierdlem63.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
5 fourierdlem63.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
6 fourierdlem63.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
7 fourierdlem63.cltd ⊢ ( 𝜑 → 𝐶 < 𝐷 )
8 fourierdlem63.o ⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
9 fourierdlem63.h ⊢ 𝐻 = ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
10 fourierdlem63.n ⊢ 𝑁 = ( ( ♯ ‘ 𝐻 ) − 1 )
11 fourierdlem63.s ⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
12 fourierdlem63.e ⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
13 fourierdlem63.k ⊢ ( 𝜑 → 𝐾 ∈ ( 0 ... 𝑀 ) )
14 fourierdlem63.j ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ 𝑁 ) )
15 fourierdlem63.y ⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝑆 ‘ 𝐽 ) [,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
16 fourierdlem63.eyltqk ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑌 ) < ( 𝑄 ‘ 𝐾 ) )
17 fourierdlem63.x ⊢ 𝑋 = ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) )
18 12 a1i ⊢ ( 𝜑 → 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) )
19 id ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
20 oveq2 ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → ( 𝐵 − 𝑥 ) = ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
21 20 oveq1d ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → ( ( 𝐵 − 𝑥 ) / 𝑇 ) = ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) )
22 21 fveq2d ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) )
23 22 oveq1d ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) )
24 19 23 oveq12d ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) )
25 24 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) )
26 1 2 3 4 5 6 7 8 9 10 11 fourierdlem54 ⊢ ( 𝜑 → ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ) ∧ 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ) )
27 26 simpld ⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ) )
28 27 simprd ⊢ ( 𝜑 → 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) )
29 27 simpld ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
30 8 fourierdlem2 ⊢ ( 𝑁 ∈ ℕ → ( 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ↔ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ) )
31 29 30 syl ⊢ ( 𝜑 → ( 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ↔ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ) )
32 28 31 mpbid ⊢ ( 𝜑 → ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) )
33 32 simpld ⊢ ( 𝜑 → 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) )
34 elmapi ⊢ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) → 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ )
35 33 34 syl ⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ )
36 fzofzp1 ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) )
37 14 36 syl ⊢ ( 𝜑 → ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) )
38 35 37 ffvelrnd ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ )
39 2 3 4 fourierdlem11 ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) )
40 39 simp2d ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
41 40 38 resubcld ⊢ ( 𝜑 → ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℝ )
42 39 simp1d ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
43 40 42 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
44 1 43 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
45 39 simp3d ⊢ ( 𝜑 → 𝐴 < 𝐵 )
46 42 40 posdifd ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 − 𝐴 ) ) )
47 45 46 mpbid ⊢ ( 𝜑 → 0 < ( 𝐵 − 𝐴 ) )
48 47 1 breqtrrdi ⊢ ( 𝜑 → 0 < 𝑇 )
49 48 gt0ne0d ⊢ ( 𝜑 → 𝑇 ≠ 0 )
50 41 44 49 redivcld ⊢ ( 𝜑 → ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ∈ ℝ )
51 50 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) ∈ ℤ )
52 51 zred ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) ∈ ℝ )
53 52 44 remulcld ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
54 38 53 readdcld ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ )
55 18 25 38 54 fvmptd ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) )
56 55 54 eqeltrd ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℝ )
57 2 fourierdlem2 ⊢ ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
58 3 57 syl ⊢ ( 𝜑 → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
59 4 58 mpbid ⊢ ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
60 59 simpld ⊢ ( 𝜑 → 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) )
61 elmapi ⊢ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
62 60 61 syl ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
63 62 13 ffvelrnd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐾 ) ∈ ℝ )
64 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝐶 ∈ ℝ )
65 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝐷 ∈ ℝ )
66 42 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
67 iocssre ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
68 66 40 67 syl2anc ⊢ ( 𝜑 → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
69 42 40 45 1 12 fourierdlem4 ⊢ ( 𝜑 → 𝐸 : ℝ ⟶ ( 𝐴 (,] 𝐵 ) )
70 elfzofz ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → 𝐽 ∈ ( 0 ... 𝑁 ) )
71 14 70 syl ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ... 𝑁 ) )
72 35 71 ffvelrnd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐽 ) ∈ ℝ )
73 38 rexrd ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ* )
74 elico2 ⊢ ( ( ( 𝑆 ‘ 𝐽 ) ∈ ℝ ∧ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ* ) → ( 𝑌 ∈ ( ( 𝑆 ‘ 𝐽 ) [,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ↔ ( 𝑌 ∈ ℝ ∧ ( 𝑆 ‘ 𝐽 ) ≤ 𝑌 ∧ 𝑌 < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
75 72 73 74 syl2anc ⊢ ( 𝜑 → ( 𝑌 ∈ ( ( 𝑆 ‘ 𝐽 ) [,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ↔ ( 𝑌 ∈ ℝ ∧ ( 𝑆 ‘ 𝐽 ) ≤ 𝑌 ∧ 𝑌 < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
76 15 75 mpbid ⊢ ( 𝜑 → ( 𝑌 ∈ ℝ ∧ ( 𝑆 ‘ 𝐽 ) ≤ 𝑌 ∧ 𝑌 < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
77 76 simp1d ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
78 69 77 ffvelrnd ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑌 ) ∈ ( 𝐴 (,] 𝐵 ) )
79 68 78 sseldd ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑌 ) ∈ ℝ )
80 79 77 resubcld ⊢ ( 𝜑 → ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ∈ ℝ )
81 63 80 resubcld ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) ∈ ℝ )
82 81 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) ∈ ℝ )
83 icossicc ⊢ ( ( 𝑆 ‘ 𝐽 ) [,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑆 ‘ 𝐽 ) [,] ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
84 5 rexrd ⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
85 6 rexrd ⊢ ( 𝜑 → 𝐷 ∈ ℝ* )
86 8 29 28 fourierdlem15 ⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) ⟶ ( 𝐶 [,] 𝐷 ) )
87 84 85 86 14 fourierdlem8 ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐽 ) [,] ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( 𝐶 [,] 𝐷 ) )
88 83 87 sstrid ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐽 ) [,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( 𝐶 [,] 𝐷 ) )
89 88 15 sseldd ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐶 [,] 𝐷 ) )
90 elicc2 ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( 𝑌 ∈ ( 𝐶 [,] 𝐷 ) ↔ ( 𝑌 ∈ ℝ ∧ 𝐶 ≤ 𝑌 ∧ 𝑌 ≤ 𝐷 ) ) )
91 5 6 90 syl2anc ⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝐶 [,] 𝐷 ) ↔ ( 𝑌 ∈ ℝ ∧ 𝐶 ≤ 𝑌 ∧ 𝑌 ≤ 𝐷 ) ) )
92 89 91 mpbid ⊢ ( 𝜑 → ( 𝑌 ∈ ℝ ∧ 𝐶 ≤ 𝑌 ∧ 𝑌 ≤ 𝐷 ) )
93 92 simp2d ⊢ ( 𝜑 → 𝐶 ≤ 𝑌 )
94 63 79 resubcld ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐾 ) − ( 𝐸 ‘ 𝑌 ) ) ∈ ℝ )
95 79 63 posdifd ⊢ ( 𝜑 → ( ( 𝐸 ‘ 𝑌 ) < ( 𝑄 ‘ 𝐾 ) ↔ 0 < ( ( 𝑄 ‘ 𝐾 ) − ( 𝐸 ‘ 𝑌 ) ) ) )
96 16 95 mpbid ⊢ ( 𝜑 → 0 < ( ( 𝑄 ‘ 𝐾 ) − ( 𝐸 ‘ 𝑌 ) ) )
97 94 96 elrpd ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐾 ) − ( 𝐸 ‘ 𝑌 ) ) ∈ ℝ+ )
98 77 97 ltaddrpd ⊢ ( 𝜑 → 𝑌 < ( 𝑌 + ( ( 𝑄 ‘ 𝐾 ) − ( 𝐸 ‘ 𝑌 ) ) ) )
99 63 recnd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐾 ) ∈ ℂ )
100 79 recnd ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑌 ) ∈ ℂ )
101 77 recnd ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
102 99 100 101 subsub3d ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) = ( ( ( 𝑄 ‘ 𝐾 ) + 𝑌 ) − ( 𝐸 ‘ 𝑌 ) ) )
103 99 101 addcomd ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐾 ) + 𝑌 ) = ( 𝑌 + ( 𝑄 ‘ 𝐾 ) ) )
104 103 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 𝐾 ) + 𝑌 ) − ( 𝐸 ‘ 𝑌 ) ) = ( ( 𝑌 + ( 𝑄 ‘ 𝐾 ) ) − ( 𝐸 ‘ 𝑌 ) ) )
105 101 99 100 addsubassd ⊢ ( 𝜑 → ( ( 𝑌 + ( 𝑄 ‘ 𝐾 ) ) − ( 𝐸 ‘ 𝑌 ) ) = ( 𝑌 + ( ( 𝑄 ‘ 𝐾 ) − ( 𝐸 ‘ 𝑌 ) ) ) )
106 102 104 105 3eqtrrd ⊢ ( 𝜑 → ( 𝑌 + ( ( 𝑄 ‘ 𝐾 ) − ( 𝐸 ‘ 𝑌 ) ) ) = ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) )
107 98 106 breqtrd ⊢ ( 𝜑 → 𝑌 < ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) )
108 5 77 81 93 107 lelttrd ⊢ ( 𝜑 → 𝐶 < ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) )
109 5 81 108 ltled ⊢ ( 𝜑 → 𝐶 ≤ ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) )
110 109 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝐶 ≤ ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) )
111 38 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ )
112 63 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑄 ‘ 𝐾 ) ∈ ℝ )
113 56 38 resubcld ⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℝ )
114 113 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℝ )
115 112 114 resubcld ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ∈ ℝ )
116 76 simp3d ⊢ ( 𝜑 → 𝑌 < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
117 77 38 116 ltled ⊢ ( 𝜑 → 𝑌 ≤ ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
118 42 40 45 1 12 77 38 117 fourierdlem7 ⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ≤ ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) )
119 113 80 63 118 lesub2dd ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) ≤ ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
120 119 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) ≤ ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
121 99 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑄 ‘ 𝐾 ) ∈ ℂ )
122 56 recnd ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℂ )
123 122 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℂ )
124 111 recnd ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℂ )
125 121 123 124 subsubd ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = ( ( ( 𝑄 ‘ 𝐾 ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) + ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
126 99 122 subcld ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐾 ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ∈ ℂ )
127 38 recnd ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℂ )
128 126 127 addcomd ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 𝐾 ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) + ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( 𝑄 ‘ 𝐾 ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) )
129 128 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( ( 𝑄 ‘ 𝐾 ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) + ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( 𝑄 ‘ 𝐾 ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) )
130 125 129 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( 𝑄 ‘ 𝐾 ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) )
131 simpr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
132 56 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℝ )
133 112 132 sublt0d ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( ( 𝑄 ‘ 𝐾 ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) < 0 ↔ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
134 131 133 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑄 ‘ 𝐾 ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) < 0 )
135 112 132 resubcld ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑄 ‘ 𝐾 ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ∈ ℝ )
136 ltaddneg ⊢ ( ( ( ( 𝑄 ‘ 𝐾 ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ∈ ℝ ∧ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ ) → ( ( ( 𝑄 ‘ 𝐾 ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) < 0 ↔ ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( 𝑄 ‘ 𝐾 ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
137 135 111 136 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( ( 𝑄 ‘ 𝐾 ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) < 0 ↔ ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( 𝑄 ‘ 𝐾 ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
138 134 137 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( 𝑄 ‘ 𝐾 ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
139 130 138 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
140 82 115 111 120 139 lelttrd ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
141 86 37 ffvelrnd ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ( 𝐶 [,] 𝐷 ) )
142 elicc2 ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ( 𝐶 [,] 𝐷 ) ↔ ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∧ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ 𝐷 ) ) )
143 5 6 142 syl2anc ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ( 𝐶 [,] 𝐷 ) ↔ ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∧ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ 𝐷 ) ) )
144 141 143 mpbid ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∧ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ 𝐷 ) )
145 144 simp3d ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ 𝐷 )
146 145 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ 𝐷 )
147 82 111 65 140 146 ltletrd ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) < 𝐷 )
148 82 65 147 ltled ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) ≤ 𝐷 )
149 64 65 82 110 148 eliccd ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) ∈ ( 𝐶 [,] 𝐷 ) )
150 id ⊢ ( 𝑥 = 𝑌 → 𝑥 = 𝑌 )
151 oveq2 ⊢ ( 𝑥 = 𝑌 → ( 𝐵 − 𝑥 ) = ( 𝐵 − 𝑌 ) )
152 151 oveq1d ⊢ ( 𝑥 = 𝑌 → ( ( 𝐵 − 𝑥 ) / 𝑇 ) = ( ( 𝐵 − 𝑌 ) / 𝑇 ) )
153 152 fveq2d ⊢ ( 𝑥 = 𝑌 → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) )
154 153 oveq1d ⊢ ( 𝑥 = 𝑌 → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) )
155 150 154 oveq12d ⊢ ( 𝑥 = 𝑌 → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑌 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) ) )
156 155 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑌 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) ) )
157 40 77 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝑌 ) ∈ ℝ )
158 157 44 49 redivcld ⊢ ( 𝜑 → ( ( 𝐵 − 𝑌 ) / 𝑇 ) ∈ ℝ )
159 158 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) ∈ ℤ )
160 159 zred ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) ∈ ℝ )
161 160 44 remulcld ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
162 77 161 readdcld ⊢ ( 𝜑 → ( 𝑌 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ )
163 18 156 77 162 fvmptd ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑌 ) = ( 𝑌 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) ) )
164 163 oveq1d ⊢ ( 𝜑 → ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) = ( ( 𝑌 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) ) − 𝑌 ) )
165 164 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) / 𝑇 ) = ( ( ( 𝑌 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) ) − 𝑌 ) / 𝑇 ) )
166 161 recnd ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) ∈ ℂ )
167 101 166 pncan2d ⊢ ( 𝜑 → ( ( 𝑌 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) ) − 𝑌 ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) )
168 167 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑌 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) ) − 𝑌 ) / 𝑇 ) = ( ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) / 𝑇 ) )
169 160 recnd ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) ∈ ℂ )
170 44 recnd ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
171 169 170 49 divcan4d ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) / 𝑇 ) = ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) )
172 165 168 171 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) / 𝑇 ) = ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) )
173 172 159 eqeltrd ⊢ ( 𝜑 → ( ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) / 𝑇 ) ∈ ℤ )
174 80 recnd ⊢ ( 𝜑 → ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ∈ ℂ )
175 174 170 49 divcan1d ⊢ ( 𝜑 → ( ( ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) / 𝑇 ) · 𝑇 ) = ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) )
176 175 oveq2d ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) + ( ( ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) / 𝑇 ) · 𝑇 ) ) = ( ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) + ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) )
177 99 174 npcand ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) + ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) = ( 𝑄 ‘ 𝐾 ) )
178 176 177 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) + ( ( ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) / 𝑇 ) · 𝑇 ) ) = ( 𝑄 ‘ 𝐾 ) )
179 ffun ⊢ ( 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ → Fun 𝑄 )
180 62 179 syl ⊢ ( 𝜑 → Fun 𝑄 )
181 62 fdmd ⊢ ( 𝜑 → dom 𝑄 = ( 0 ... 𝑀 ) )
182 13 181 eleqtrrd ⊢ ( 𝜑 → 𝐾 ∈ dom 𝑄 )
183 fvelrn ⊢ ( ( Fun 𝑄 ∧ 𝐾 ∈ dom 𝑄 ) → ( 𝑄 ‘ 𝐾 ) ∈ ran 𝑄 )
184 180 182 183 syl2anc ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐾 ) ∈ ran 𝑄 )
185 178 184 eqeltrd ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) + ( ( ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) / 𝑇 ) · 𝑇 ) ) ∈ ran 𝑄 )
186 oveq1 ⊢ ( 𝑘 = ( ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) / 𝑇 ) → ( 𝑘 · 𝑇 ) = ( ( ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) / 𝑇 ) · 𝑇 ) )
187 186 oveq2d ⊢ ( 𝑘 = ( ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) / 𝑇 ) → ( ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) + ( 𝑘 · 𝑇 ) ) = ( ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) + ( ( ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) / 𝑇 ) · 𝑇 ) ) )
188 187 eleq1d ⊢ ( 𝑘 = ( ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) / 𝑇 ) → ( ( ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) + ( ( ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) / 𝑇 ) · 𝑇 ) ) ∈ ran 𝑄 ) )
189 188 rspcev ⊢ ( ( ( ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) / 𝑇 ) ∈ ℤ ∧ ( ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) + ( ( ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) / 𝑇 ) · 𝑇 ) ) ∈ ran 𝑄 ) → ∃ 𝑘 ∈ ℤ ( ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 )
190 173 185 189 syl2anc ⊢ ( 𝜑 → ∃ 𝑘 ∈ ℤ ( ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 )
191 190 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ∃ 𝑘 ∈ ℤ ( ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 )
192 oveq1 ⊢ ( 𝑥 = ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) = ( ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) + ( 𝑘 · 𝑇 ) ) )
193 192 eleq1d ⊢ ( 𝑥 = ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) → ( ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
194 193 rexbidv ⊢ ( 𝑥 = ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) → ( ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
195 194 elrab ⊢ ( ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) ∈ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ↔ ( ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) ∈ ( 𝐶 [,] 𝐷 ) ∧ ∃ 𝑘 ∈ ℤ ( ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
196 149 191 195 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) ∈ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
197 elun2 ⊢ ( ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) ∈ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } → ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) ∈ ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) )
198 196 197 syl ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑄 ‘ 𝐾 ) − ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ) ∈ ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) )
199 198 17 9 3eltr4g ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑋 ∈ 𝐻 )
200 elfzelz ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 ∈ ℤ )
201 200 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ 𝑗 ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑗 ∈ ℤ )
202 elfzoelz ⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → 𝐽 ∈ ℤ )
203 14 202 syl ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
204 203 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ 𝑗 ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝐽 ∈ ℤ )
205 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ 𝑗 ) ) → ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ 𝑗 ) )
206 26 simprd ⊢ ( 𝜑 → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
207 206 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ 𝑗 ) ) → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
208 71 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ 𝑗 ) ) → 𝐽 ∈ ( 0 ... 𝑁 ) )
209 simplr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ 𝑗 ) ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
210 isorel ⊢ ( ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ∧ ( 𝐽 ∈ ( 0 ... 𝑁 ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝐽 < 𝑗 ↔ ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ 𝑗 ) ) )
211 207 208 209 210 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ 𝑗 ) ) → ( 𝐽 < 𝑗 ↔ ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ 𝑗 ) ) )
212 205 211 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ 𝑗 ) ) → 𝐽 < 𝑗 )
213 212 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ 𝑗 ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝐽 < 𝑗 )
214 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
215 206 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
216 simplr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
217 37 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) )
218 isorel ⊢ ( ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ∧ ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑗 < ( 𝐽 + 1 ) ↔ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
219 215 216 217 218 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝑗 < ( 𝐽 + 1 ) ↔ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
220 214 219 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → 𝑗 < ( 𝐽 + 1 ) )
221 220 adantrl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ 𝑗 ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑗 < ( 𝐽 + 1 ) )
222 btwnnz ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐽 < 𝑗 ∧ 𝑗 < ( 𝐽 + 1 ) ) → ¬ 𝑗 ∈ ℤ )
223 204 213 221 222 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ 𝑗 ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ¬ 𝑗 ∈ ℤ )
224 201 223 pm2.65da ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ¬ ( ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ 𝑗 ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
225 224 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ¬ ( ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ 𝑗 ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
226 72 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑗 ) = 𝑋 ) → ( 𝑆 ‘ 𝐽 ) ∈ ℝ )
227 77 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑗 ) = 𝑋 ) → 𝑌 ∈ ℝ )
228 35 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) ∈ ℝ )
229 228 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑗 ) = 𝑋 ) → ( 𝑆 ‘ 𝑗 ) ∈ ℝ )
230 76 simp2d ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐽 ) ≤ 𝑌 )
231 230 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑗 ) = 𝑋 ) → ( 𝑆 ‘ 𝐽 ) ≤ 𝑌 )
232 107 17 breqtrrdi ⊢ ( 𝜑 → 𝑌 < 𝑋 )
233 232 adantr ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝑗 ) = 𝑋 ) → 𝑌 < 𝑋 )
234 eqcom ⊢ ( 𝑋 = ( 𝑆 ‘ 𝑗 ) ↔ ( 𝑆 ‘ 𝑗 ) = 𝑋 )
235 234 biimpri ⊢ ( ( 𝑆 ‘ 𝑗 ) = 𝑋 → 𝑋 = ( 𝑆 ‘ 𝑗 ) )
236 235 adantl ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝑗 ) = 𝑋 ) → 𝑋 = ( 𝑆 ‘ 𝑗 ) )
237 233 236 breqtrd ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝑗 ) = 𝑋 ) → 𝑌 < ( 𝑆 ‘ 𝑗 ) )
238 237 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑗 ) = 𝑋 ) → 𝑌 < ( 𝑆 ‘ 𝑗 ) )
239 226 227 229 231 238 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑗 ) = 𝑋 ) → ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ 𝑗 ) )
240 239 adantllr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑗 ) = 𝑋 ) → ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ 𝑗 ) )
241 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ∧ ( 𝑆 ‘ 𝑗 ) = 𝑋 ) → ( 𝑆 ‘ 𝑗 ) = 𝑋 )
242 17 140 eqbrtrid ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑋 < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
243 242 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ∧ ( 𝑆 ‘ 𝑗 ) = 𝑋 ) → 𝑋 < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
244 241 243 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ∧ ( 𝑆 ‘ 𝑗 ) = 𝑋 ) → ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
245 244 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑗 ) = 𝑋 ) → ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
246 240 245 jca ⊢ ( ( ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑗 ) = 𝑋 ) → ( ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ 𝑗 ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
247 225 246 mtand ⊢ ( ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ¬ ( 𝑆 ‘ 𝑗 ) = 𝑋 )
248 247 nrexdv ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ¬ ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑗 ) = 𝑋 )
249 isof1o ⊢ ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) → 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ 𝐻 )
250 206 249 syl ⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ 𝐻 )
251 f1ofo ⊢ ( 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ 𝐻 → 𝑆 : ( 0 ... 𝑁 ) –onto→ 𝐻 )
252 250 251 syl ⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) –onto→ 𝐻 )
253 foelrn ⊢ ( ( 𝑆 : ( 0 ... 𝑁 ) –onto→ 𝐻 ∧ 𝑋 ∈ 𝐻 ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 𝑋 = ( 𝑆 ‘ 𝑗 ) )
254 252 253 sylan ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐻 ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 𝑋 = ( 𝑆 ‘ 𝑗 ) )
255 234 rexbii ⊢ ( ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 𝑋 = ( 𝑆 ‘ 𝑗 ) ↔ ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑗 ) = 𝑋 )
256 254 255 sylib ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐻 ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑗 ) = 𝑋 )
257 256 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ∧ 𝑋 ∈ 𝐻 ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑗 ) = 𝑋 )
258 248 257 mtand ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ¬ 𝑋 ∈ 𝐻 )
259 199 258 pm2.65da ⊢ ( 𝜑 → ¬ ( 𝑄 ‘ 𝐾 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
260 56 63 259 nltled ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ≤ ( 𝑄 ‘ 𝐾 ) )