This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fourierdlem65

Description: The distance of two adjacent points in the moved partition is preserved in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem65.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem65.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
fourierdlem65.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem65.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
fourierdlem65.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
fourierdlem65.d ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 (,) +∞ ) )
fourierdlem65.o ⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem65.n ⊢ 𝑁 = ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) − 1 )
fourierdlem65.s ⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) )
fourierdlem65.e ⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
fourierdlem65.l ⊢ 𝐿 = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) )
fourierdlem65.z ⊢ 𝑍 = ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) )
Assertion fourierdlem65 ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem65.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
2 fourierdlem65.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
3 fourierdlem65.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
4 fourierdlem65.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
5 fourierdlem65.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
6 fourierdlem65.d ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 (,) +∞ ) )
7 fourierdlem65.o ⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
8 fourierdlem65.n ⊢ 𝑁 = ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) − 1 )
9 fourierdlem65.s ⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) )
10 fourierdlem65.e ⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
11 fourierdlem65.l ⊢ 𝐿 = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) )
12 fourierdlem65.z ⊢ 𝑍 = ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) )
13 11 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐿 = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) ) )
14 simpr ⊢ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) )
15 simpl ⊢ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 )
16 14 15 eqtrd ⊢ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → 𝑦 = 𝐵 )
17 16 iftrued ⊢ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) = 𝐴 )
18 17 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) = 𝐴 )
19 1 3 4 fourierdlem11 ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) )
20 19 simp1d ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
21 19 simp2d ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
22 19 simp3d ⊢ ( 𝜑 → 𝐴 < 𝐵 )
23 20 21 22 2 10 fourierdlem4 ⊢ ( 𝜑 → 𝐸 : ℝ ⟶ ( 𝐴 (,] 𝐵 ) )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐸 : ℝ ⟶ ( 𝐴 (,] 𝐵 ) )
25 ioossre ⊢ ( 𝐶 (,) +∞ ) ⊆ ℝ
26 25 6 sselid ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
27 5 rexrd ⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
28 pnfxr ⊢ +∞ ∈ ℝ*
29 28 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
30 ioogtlb ⊢ ( ( 𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐷 ∈ ( 𝐶 (,) +∞ ) ) → 𝐶 < 𝐷 )
31 27 29 6 30 syl3anc ⊢ ( 𝜑 → 𝐶 < 𝐷 )
32 id ⊢ ( 𝑦 = 𝑥 → 𝑦 = 𝑥 )
33 2 eqcomi ⊢ ( 𝐵 − 𝐴 ) = 𝑇
34 33 oveq2i ⊢ ( 𝑘 · ( 𝐵 − 𝐴 ) ) = ( 𝑘 · 𝑇 )
35 34 a1i ⊢ ( 𝑦 = 𝑥 → ( 𝑘 · ( 𝐵 − 𝐴 ) ) = ( 𝑘 · 𝑇 ) )
36 32 35 oveq12d ⊢ ( 𝑦 = 𝑥 → ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) = ( 𝑥 + ( 𝑘 · 𝑇 ) ) )
37 36 eleq1d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ↔ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
38 37 rexbidv ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
39 38 cbvrabv ⊢ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } = { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 }
40 39 uneq2i ⊢ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
41 2 1 3 4 5 26 31 7 40 8 9 fourierdlem54 ⊢ ( 𝜑 → ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ) ∧ 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) ) )
42 41 simpld ⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ) )
43 42 simprd ⊢ ( 𝜑 → 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) )
44 42 simpld ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
45 7 fourierdlem2 ⊢ ( 𝑁 ∈ ℕ → ( 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ↔ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ) )
46 44 45 syl ⊢ ( 𝜑 → ( 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ↔ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ) )
47 43 46 mpbid ⊢ ( 𝜑 → ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) )
48 47 simpld ⊢ ( 𝜑 → 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) )
49 elmapi ⊢ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) → 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ )
50 48 49 syl ⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ )
51 50 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ )
52 elfzofz ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
53 52 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
54 51 53 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) ∈ ℝ )
55 24 54 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
56 55 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
57 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐴 ∈ ℝ )
58 13 18 56 57 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) = 𝐴 )
59 58 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − 𝐴 ) )
60 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐵 ∈ ℝ )
61 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐴 < 𝐵 )
62 54 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝑆 ‘ 𝑗 ) ∈ ℝ )
63 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 )
64 fzofzp1 ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → ( 𝑗 + 1 ) ∈ ( 0 ... 𝑁 ) )
65 64 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑗 + 1 ) ∈ ( 0 ... 𝑁 ) )
66 51 65 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
67 66 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
68 elfzoelz ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → 𝑗 ∈ ℤ )
69 68 zred ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → 𝑗 ∈ ℝ )
70 69 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑗 ∈ ℝ )
71 70 ltp1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑗 < ( 𝑗 + 1 ) )
72 41 simprd ⊢ ( 𝜑 → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) )
73 72 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) )
74 isorel ⊢ ( ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) ∧ ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑗 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑗 < ( 𝑗 + 1 ) ↔ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
75 73 53 65 74 syl12anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑗 < ( 𝑗 + 1 ) ↔ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
76 71 75 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
77 76 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
78 isof1o ⊢ ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) → 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) )
79 f1ofo ⊢ ( 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) → 𝑆 : ( 0 ... 𝑁 ) –onto→ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) )
80 72 78 79 3syl ⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) –onto→ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) )
81 80 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → 𝑆 : ( 0 ... 𝑁 ) –onto→ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) )
82 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → 𝐶 ∈ ℝ )
83 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → 𝐷 ∈ ℝ )
84 21 20 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
85 2 84 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
86 85 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑇 ∈ ℝ )
87 54 86 readdcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ ℝ )
88 87 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ ℝ )
89 5 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐶 ∈ ℝ )
90 7 44 43 fourierdlem15 ⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) ⟶ ( 𝐶 [,] 𝐷 ) )
91 90 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑆 : ( 0 ... 𝑁 ) ⟶ ( 𝐶 [,] 𝐷 ) )
92 91 53 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) ∈ ( 𝐶 [,] 𝐷 ) )
93 26 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐷 ∈ ℝ )
94 elicc2 ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( ( 𝑆 ‘ 𝑗 ) ∈ ( 𝐶 [,] 𝐷 ) ↔ ( ( 𝑆 ‘ 𝑗 ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑆 ‘ 𝑗 ) ∧ ( 𝑆 ‘ 𝑗 ) ≤ 𝐷 ) ) )
95 89 93 94 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) ∈ ( 𝐶 [,] 𝐷 ) ↔ ( ( 𝑆 ‘ 𝑗 ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑆 ‘ 𝑗 ) ∧ ( 𝑆 ‘ 𝑗 ) ≤ 𝐷 ) ) )
96 92 95 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑆 ‘ 𝑗 ) ∧ ( 𝑆 ‘ 𝑗 ) ≤ 𝐷 ) )
97 96 simp2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐶 ≤ ( 𝑆 ‘ 𝑗 ) )
98 20 21 posdifd ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 − 𝐴 ) ) )
99 22 98 mpbid ⊢ ( 𝜑 → 0 < ( 𝐵 − 𝐴 ) )
100 99 2 breqtrrdi ⊢ ( 𝜑 → 0 < 𝑇 )
101 85 100 elrpd ⊢ ( 𝜑 → 𝑇 ∈ ℝ+ )
102 101 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑇 ∈ ℝ+ )
103 54 102 ltaddrpd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) < ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
104 89 54 87 97 103 lelttrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐶 < ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
105 89 87 104 ltled ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐶 ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
106 105 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → 𝐶 ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
107 66 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
108 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
109 88 107 ltnled ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ↔ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) )
110 108 109 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
111 91 65 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( 𝐶 [,] 𝐷 ) )
112 elicc2 ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( 𝐶 [,] 𝐷 ) ↔ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ 𝐷 ) ) )
113 89 93 112 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( 𝐶 [,] 𝐷 ) ↔ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ 𝐷 ) ) )
114 111 113 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ 𝐷 ) )
115 114 simp3d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ 𝐷 )
116 115 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ 𝐷 )
117 88 107 83 110 116 ltletrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) < 𝐷 )
118 88 83 117 ltled ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ≤ 𝐷 )
119 82 83 88 106 118 eliccd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ ( 𝐶 [,] 𝐷 ) )
120 119 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ ( 𝐶 [,] 𝐷 ) )
121 10 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) )
122 id ⊢ ( 𝑥 = ( 𝑆 ‘ 𝑗 ) → 𝑥 = ( 𝑆 ‘ 𝑗 ) )
123 oveq2 ⊢ ( 𝑥 = ( 𝑆 ‘ 𝑗 ) → ( 𝐵 − 𝑥 ) = ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) )
124 123 oveq1d ⊢ ( 𝑥 = ( 𝑆 ‘ 𝑗 ) → ( ( 𝐵 − 𝑥 ) / 𝑇 ) = ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
125 124 fveq2d ⊢ ( 𝑥 = ( 𝑆 ‘ 𝑗 ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) )
126 125 oveq1d ⊢ ( 𝑥 = ( 𝑆 ‘ 𝑗 ) → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) )
127 122 126 oveq12d ⊢ ( 𝑥 = ( 𝑆 ‘ 𝑗 ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) )
128 127 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 = ( 𝑆 ‘ 𝑗 ) ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) )
129 21 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐵 ∈ ℝ )
130 129 54 resubcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) ∈ ℝ )
131 130 102 rerpdivcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ∈ ℝ )
132 131 flcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) ∈ ℤ )
133 132 zred ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) ∈ ℝ )
134 133 86 remulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
135 54 134 readdcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ )
136 121 128 54 135 fvmptd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) )
137 136 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) = ( ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
138 137 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) = ( ( ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
139 54 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) ∈ ℂ )
140 134 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ∈ ℂ )
141 139 140 pncan2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) − ( 𝑆 ‘ 𝑗 ) ) = ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) )
142 141 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) = ( ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) / 𝑇 ) )
143 133 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) ∈ ℂ )
144 86 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑇 ∈ ℂ )
145 102 rpne0d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑇 ≠ 0 )
146 143 144 145 divcan4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) / 𝑇 ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) )
147 138 142 146 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) )
148 147 132 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ∈ ℤ )
149 peano2zm ⊢ ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ∈ ℤ → ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) ∈ ℤ )
150 148 149 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) ∈ ℤ )
151 150 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) ∈ ℤ )
152 33 oveq2i ⊢ ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · ( 𝐵 − 𝐴 ) ) = ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · 𝑇 )
153 152 oveq2i ⊢ ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · ( 𝐵 − 𝐴 ) ) ) = ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · 𝑇 ) )
154 153 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · ( 𝐵 − 𝐴 ) ) ) = ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · 𝑇 ) ) )
155 136 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) )
156 oveq1 ⊢ ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 → ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) = ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) )
157 156 eqcomd ⊢ ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 → ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) = ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
158 157 oveq1d ⊢ ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 → ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) = ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
159 158 fveq2d ⊢ ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) = ( ⌊ ‘ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) )
160 159 oveq1d ⊢ ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) )
161 160 oveq2d ⊢ ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 → ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) )
162 161 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) )
163 147 143 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ∈ ℂ )
164 1cnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 1 ∈ ℂ )
165 163 164 144 subdird ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · 𝑇 ) = ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) − ( 1 · 𝑇 ) ) )
166 85 recnd ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
167 166 mullidd ⊢ ( 𝜑 → ( 1 · 𝑇 ) = 𝑇 )
168 167 oveq2d ⊢ ( 𝜑 → ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) − ( 1 · 𝑇 ) ) = ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) − 𝑇 ) )
169 168 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) − ( 1 · 𝑇 ) ) = ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) − 𝑇 ) )
170 165 169 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · 𝑇 ) = ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) − 𝑇 ) )
171 170 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · 𝑇 ) ) = ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) − 𝑇 ) ) )
172 163 144 mulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) ∈ ℂ )
173 139 144 172 ppncand ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) − 𝑇 ) ) = ( ( 𝑆 ‘ 𝑗 ) + ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) ) )
174 flid ⊢ ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ∈ ℤ → ( ⌊ ‘ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) = ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
175 148 174 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ⌊ ‘ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) = ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
176 175 eqcomd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) = ( ⌊ ‘ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) )
177 176 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) = ( ( ⌊ ‘ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) )
178 177 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) + ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) ) = ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) )
179 171 173 178 3eqtrrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) = ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · 𝑇 ) ) )
180 179 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) = ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · 𝑇 ) ) )
181 155 162 180 3eqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · 𝑇 ) ) = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) )
182 154 181 63 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · ( 𝐵 − 𝐴 ) ) ) = 𝐵 )
183 1 fourierdlem2 ⊢ ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
184 3 183 syl ⊢ ( 𝜑 → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
185 4 184 mpbid ⊢ ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
186 185 simprd ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
187 186 simpld ⊢ ( 𝜑 → ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) )
188 187 simprd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = 𝐵 )
189 188 eqcomd ⊢ ( 𝜑 → 𝐵 = ( 𝑄 ‘ 𝑀 ) )
190 1 3 4 fourierdlem15 ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( 𝐴 [,] 𝐵 ) )
191 ffn ⊢ ( 𝑄 : ( 0 ... 𝑀 ) ⟶ ( 𝐴 [,] 𝐵 ) → 𝑄 Fn ( 0 ... 𝑀 ) )
192 190 191 syl ⊢ ( 𝜑 → 𝑄 Fn ( 0 ... 𝑀 ) )
193 3 nnnn0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
194 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
195 193 194 eleqtrdi ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
196 eluzfz2 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → 𝑀 ∈ ( 0 ... 𝑀 ) )
197 195 196 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... 𝑀 ) )
198 fnfvelrn ⊢ ( ( 𝑄 Fn ( 0 ... 𝑀 ) ∧ 𝑀 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 𝑀 ) ∈ ran 𝑄 )
199 192 197 198 syl2anc ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) ∈ ran 𝑄 )
200 189 199 eqeltrd ⊢ ( 𝜑 → 𝐵 ∈ ran 𝑄 )
201 200 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐵 ∈ ran 𝑄 )
202 182 201 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
203 202 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
204 oveq1 ⊢ ( 𝑘 = ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) → ( 𝑘 · ( 𝐵 − 𝐴 ) ) = ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · ( 𝐵 − 𝐴 ) ) )
205 204 oveq2d ⊢ ( 𝑘 = ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) → ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) = ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · ( 𝐵 − 𝐴 ) ) ) )
206 205 eleq1d ⊢ ( 𝑘 = ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) → ( ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ↔ ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ) )
207 206 rspcev ⊢ ( ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) ∈ ℤ ∧ ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − 1 ) · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ) → ∃ 𝑘 ∈ ℤ ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
208 151 203 207 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ∃ 𝑘 ∈ ℤ ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
209 oveq1 ⊢ ( 𝑦 = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) → ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) = ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) )
210 209 eleq1d ⊢ ( 𝑦 = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) → ( ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ↔ ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ) )
211 210 rexbidv ⊢ ( 𝑦 = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) → ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ) )
212 211 elrab ⊢ ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ↔ ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ ( 𝐶 [,] 𝐷 ) ∧ ∃ 𝑘 ∈ ℤ ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ) )
213 120 208 212 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } )
214 elun2 ⊢ ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) )
215 213 214 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) )
216 foelrn ⊢ ( ( 𝑆 : ( 0 ... 𝑁 ) –onto→ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ∧ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) → ∃ 𝑖 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) = ( 𝑆 ‘ 𝑖 ) )
217 81 215 216 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ∃ 𝑖 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) = ( 𝑆 ‘ 𝑖 ) )
218 eqcom ⊢ ( ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) = ( 𝑆 ‘ 𝑖 ) ↔ ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
219 218 rexbii ⊢ ( ∃ 𝑖 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) = ( 𝑆 ‘ 𝑖 ) ↔ ∃ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
220 217 219 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ∃ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
221 103 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ∧ ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( 𝑆 ‘ 𝑗 ) < ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
222 218 biimpri ⊢ ( ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) = ( 𝑆 ‘ 𝑖 ) )
223 222 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ∧ ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) = ( 𝑆 ‘ 𝑖 ) )
224 221 223 breqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ∧ ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) )
225 110 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ∧ ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
226 223 225 eqbrtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ∧ ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
227 224 226 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ∧ ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
228 227 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
229 simplll ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) )
230 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → 𝑖 ∈ ( 0 ... 𝑁 ) )
231 elfzelz ⊢ ( 𝑖 ∈ ( 0 ... 𝑁 ) → 𝑖 ∈ ℤ )
232 231 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑖 ∈ ℤ )
233 68 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑗 ∈ ℤ )
234 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ) → ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) )
235 73 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ) → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) )
236 53 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
237 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ) → 𝑖 ∈ ( 0 ... 𝑁 ) )
238 isorel ⊢ ( ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) ∧ ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑗 < 𝑖 ↔ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ) )
239 235 236 237 238 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ) → ( 𝑗 < 𝑖 ↔ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ) )
240 234 239 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ) → 𝑗 < 𝑖 )
241 240 adantrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑗 < 𝑖 )
242 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
243 73 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) )
244 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → 𝑖 ∈ ( 0 ... 𝑁 ) )
245 65 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑗 + 1 ) ∈ ( 0 ... 𝑁 ) )
246 isorel ⊢ ( ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) ∧ ( 𝑖 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑗 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑖 < ( 𝑗 + 1 ) ↔ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
247 243 244 245 246 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑖 < ( 𝑗 + 1 ) ↔ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
248 242 247 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → 𝑖 < ( 𝑗 + 1 ) )
249 248 adantrl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑖 < ( 𝑗 + 1 ) )
250 btwnnz ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑗 < 𝑖 ∧ 𝑖 < ( 𝑗 + 1 ) ) → ¬ 𝑖 ∈ ℤ )
251 233 241 249 250 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ¬ 𝑖 ∈ ℤ )
252 232 251 pm2.65da ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ¬ ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
253 229 230 252 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ¬ ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
254 228 253 pm2.65da ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ¬ ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
255 254 nrexdv ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ¬ ∃ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
256 255 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) → ¬ ∃ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝑆 ‘ 𝑖 ) = ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
257 220 256 condan ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
258 62 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝑆 ‘ 𝑗 ) ∈ ℝ* )
259 85 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝑇 ∈ ℝ )
260 62 259 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ ℝ )
261 elioc2 ⊢ ( ( ( 𝑆 ‘ 𝑗 ) ∈ ℝ* ∧ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ ℝ ) → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( ( 𝑆 ‘ 𝑗 ) (,] ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ↔ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ) )
262 258 260 261 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( ( 𝑆 ‘ 𝑗 ) (,] ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ↔ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ) )
263 67 77 257 262 mpbir3and ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( ( 𝑆 ‘ 𝑗 ) (,] ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) )
264 57 60 61 2 10 62 63 263 fourierdlem26 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) = ( 𝐴 + ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) )
265 264 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − 𝐴 ) = ( ( 𝐴 + ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) − 𝐴 ) )
266 57 recnd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐴 ∈ ℂ )
267 66 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℂ )
268 267 139 subcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) ∈ ℂ )
269 268 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) ∈ ℂ )
270 266 269 pncan2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝐴 + ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) − 𝐴 ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
271 59 265 270 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
272 11 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐿 = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) ) )
273 eqcom ⊢ ( 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ↔ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝑦 )
274 273 biimpi ⊢ ( 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝑦 )
275 274 adantl ⊢ ( ( ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝑦 )
276 neqne ⊢ ( ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ≠ 𝐵 )
277 276 adantr ⊢ ( ( ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ≠ 𝐵 )
278 275 277 eqnetrrd ⊢ ( ( ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → 𝑦 ≠ 𝐵 )
279 278 neneqd ⊢ ( ( ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → ¬ 𝑦 = 𝐵 )
280 279 iffalsed ⊢ ( ( ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) = 𝑦 )
281 simpr ⊢ ( ( ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) )
282 280 281 eqtrd ⊢ ( ( ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) )
283 282 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) )
284 55 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
285 272 283 284 284 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) )
286 285 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) )
287 id ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) → 𝑥 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
288 oveq2 ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) → ( 𝐵 − 𝑥 ) = ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
289 288 oveq1d ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) → ( ( 𝐵 − 𝑥 ) / 𝑇 ) = ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) )
290 289 fveq2d ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) )
291 290 oveq1d ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) )
292 287 291 oveq12d ⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) )
293 292 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) )
294 129 66 resubcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ )
295 294 102 rerpdivcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ∈ ℝ )
296 295 flcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ∈ ℤ )
297 296 zred ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ∈ ℝ )
298 297 86 remulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
299 66 298 readdcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ )
300 121 293 66 299 fvmptd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) )
301 300 136 oveq12d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) = ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) − ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) ) )
302 301 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) = ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) − ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) ) )
303 flle ⊢ ( ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ∈ ℝ → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ≤ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) )
304 295 303 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ≤ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) )
305 54 66 76 ltled ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) ≤ ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
306 54 66 129 305 lesub2dd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ≤ ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) )
307 294 130 102 306 lediv1dd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
308 297 295 131 304 307 letrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
309 308 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
310 297 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ) → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ∈ ℝ )
311 1red ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ) → 1 ∈ ℝ )
312 310 311 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ∈ ℝ )
313 131 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ) → ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ∈ ℝ )
314 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ) → ¬ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) )
315 312 313 314 nltled ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
316 315 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
317 80 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → 𝑆 : ( 0 ... 𝑁 ) –onto→ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) )
318 89 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → 𝐶 ∈ ℝ )
319 93 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → 𝐷 ∈ ℝ )
320 136 135 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ℝ )
321 129 320 resubcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ∈ ℝ )
322 54 321 readdcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) ∈ ℝ )
323 12 322 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑍 ∈ ℝ )
324 323 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → 𝑍 ∈ ℝ )
325 20 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
326 325 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 ∈ ℝ* )
327 elioc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ( 𝐴 (,] 𝐵 ) ↔ ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ℝ ∧ 𝐴 < ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝐵 ) ) )
328 326 129 327 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ( 𝐴 (,] 𝐵 ) ↔ ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ℝ ∧ 𝐴 < ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝐵 ) ) )
329 55 328 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ℝ ∧ 𝐴 < ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝐵 ) )
330 329 simp3d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝐵 )
331 129 320 subge0d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 0 ≤ ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ↔ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝐵 ) )
332 330 331 mpbird ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 0 ≤ ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) )
333 54 321 addge01d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 0 ≤ ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ↔ ( 𝑆 ‘ 𝑗 ) ≤ ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) ) )
334 332 333 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) ≤ ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) )
335 89 54 322 97 334 letrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐶 ≤ ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) )
336 335 12 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐶 ≤ 𝑍 )
337 336 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → 𝐶 ≤ 𝑍 )
338 66 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
339 295 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ∈ ℝ )
340 reflcl ⊢ ( ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ∈ ℝ → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ∈ ℝ )
341 peano2re ⊢ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ∈ ℝ → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ∈ ℝ )
342 339 340 341 3syl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ∈ ℝ )
343 129 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → 𝐵 ∈ ℝ )
344 343 324 resubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( 𝐵 − 𝑍 ) ∈ ℝ )
345 102 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → 𝑇 ∈ ℝ+ )
346 344 345 rerpdivcld ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( 𝐵 − 𝑍 ) / 𝑇 ) ∈ ℝ )
347 flltp1 ⊢ ( ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ∈ ℝ → ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) )
348 295 347 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) )
349 348 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) )
350 296 peano2zd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ∈ ℤ )
351 350 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ∈ ℤ )
352 131 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ∈ ℝ )
353 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
354 321 102 rerpdivcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) / 𝑇 ) ∈ ℝ )
355 354 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) / 𝑇 ) ∈ ℝ )
356 20 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 ∈ ℝ )
357 329 simp2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 < ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) )
358 356 320 129 357 ltsub2dd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) < ( 𝐵 − 𝐴 ) )
359 358 2 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) < 𝑇 )
360 321 86 102 359 ltdiv1dd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) / 𝑇 ) < ( 𝑇 / 𝑇 ) )
361 144 145 dividd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑇 / 𝑇 ) = 1 )
362 360 361 breqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) / 𝑇 ) < 1 )
363 362 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) / 𝑇 ) < 1 )
364 130 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) ∈ ℂ )
365 321 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ∈ ℂ )
366 364 365 144 145 divsubdird ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) − ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) / 𝑇 ) = ( ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) / 𝑇 ) ) )
367 366 eqcomd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) / 𝑇 ) ) = ( ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) − ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) / 𝑇 ) )
368 129 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐵 ∈ ℂ )
369 320 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ℂ )
370 368 139 369 nnncan1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) − ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
371 370 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) − ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) / 𝑇 ) = ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
372 367 371 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) / 𝑇 ) ) = ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
373 372 148 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) / 𝑇 ) ) ∈ ℤ )
374 373 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) / 𝑇 ) ) ∈ ℤ )
375 351 352 353 355 363 374 zltlesub ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) / 𝑇 ) ) )
376 12 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑍 = ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) )
377 376 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − 𝑍 ) = ( 𝐵 − ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) ) )
378 139 368 369 addsub12d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( 𝐵 + ( ( 𝑆 ‘ 𝑗 ) − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) )
379 368 369 139 subsub2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) = ( 𝐵 + ( ( 𝑆 ‘ 𝑗 ) − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) )
380 378 379 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( 𝐵 − ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) )
381 380 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) ) = ( 𝐵 − ( 𝐵 − ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) ) )
382 369 139 subcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) ∈ ℂ )
383 368 382 nncand ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − ( 𝐵 − ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
384 377 381 383 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − 𝑍 ) = ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
385 384 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐵 − 𝑍 ) / 𝑇 ) = ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) )
386 371 367 385 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) / 𝑇 ) ) = ( ( 𝐵 − 𝑍 ) / 𝑇 ) )
387 386 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) − ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) / 𝑇 ) ) = ( ( 𝐵 − 𝑍 ) / 𝑇 ) )
388 375 387 breqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − 𝑍 ) / 𝑇 ) )
389 339 342 346 349 388 ltletrd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) < ( ( 𝐵 − 𝑍 ) / 𝑇 ) )
390 294 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ )
391 390 344 345 ltdiv1d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) < ( 𝐵 − 𝑍 ) ↔ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) < ( ( 𝐵 − 𝑍 ) / 𝑇 ) ) )
392 389 391 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) < ( 𝐵 − 𝑍 ) )
393 324 338 343 ltsub2d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( 𝑍 < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ↔ ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) < ( 𝐵 − 𝑍 ) ) )
394 392 393 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → 𝑍 < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
395 115 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ 𝐷 )
396 324 338 319 394 395 ltletrd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → 𝑍 < 𝐷 )
397 324 319 396 ltled ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → 𝑍 ≤ 𝐷 )
398 318 319 324 337 397 eliccd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → 𝑍 ∈ ( 𝐶 [,] 𝐷 ) )
399 33 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 − 𝐴 ) = 𝑇 )
400 399 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · ( 𝐵 − 𝐴 ) ) = ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) )
401 382 144 145 divcan1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · 𝑇 ) = ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
402 400 401 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · ( 𝐵 − 𝐴 ) ) = ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
403 376 402 oveq12d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑍 + ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · ( 𝐵 − 𝐴 ) ) ) = ( ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) + ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) )
404 139 365 addcomd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) + ( 𝑆 ‘ 𝑗 ) ) )
405 404 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) + ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) + ( 𝑆 ‘ 𝑗 ) ) + ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) )
406 365 139 369 ppncand ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) + ( 𝑆 ‘ 𝑗 ) ) + ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) = ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) + ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) )
407 368 369 npcand ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) + ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) = 𝐵 )
408 406 407 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) + ( 𝑆 ‘ 𝑗 ) ) + ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) = 𝐵 )
409 403 405 408 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑍 + ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · ( 𝐵 − 𝐴 ) ) ) = 𝐵 )
410 200 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐵 ∈ ran 𝑄 )
411 409 410 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑍 + ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
412 oveq1 ⊢ ( 𝑘 = ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) → ( 𝑘 · ( 𝐵 − 𝐴 ) ) = ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · ( 𝐵 − 𝐴 ) ) )
413 412 oveq2d ⊢ ( 𝑘 = ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) → ( 𝑍 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) = ( 𝑍 + ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · ( 𝐵 − 𝐴 ) ) ) )
414 413 eleq1d ⊢ ( 𝑘 = ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) → ( ( 𝑍 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ↔ ( 𝑍 + ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ) )
415 414 rspcev ⊢ ( ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ∈ ℤ ∧ ( 𝑍 + ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ) → ∃ 𝑘 ∈ ℤ ( 𝑍 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
416 148 411 415 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ∃ 𝑘 ∈ ℤ ( 𝑍 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
417 416 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ∃ 𝑘 ∈ ℤ ( 𝑍 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
418 oveq1 ⊢ ( 𝑦 = 𝑍 → ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) = ( 𝑍 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) )
419 418 eleq1d ⊢ ( 𝑦 = 𝑍 → ( ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ↔ ( 𝑍 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ) )
420 419 rexbidv ⊢ ( 𝑦 = 𝑍 → ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑍 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ) )
421 420 elrab ⊢ ( 𝑍 ∈ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ↔ ( 𝑍 ∈ ( 𝐶 [,] 𝐷 ) ∧ ∃ 𝑘 ∈ ℤ ( 𝑍 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ) )
422 398 417 421 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → 𝑍 ∈ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } )
423 elun2 ⊢ ( 𝑍 ∈ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } → 𝑍 ∈ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) )
424 422 423 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → 𝑍 ∈ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) )
425 foelrn ⊢ ( ( 𝑆 : ( 0 ... 𝑁 ) –onto→ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ∧ 𝑍 ∈ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) → ∃ 𝑖 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑆 ‘ 𝑖 ) )
426 317 424 425 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ∃ 𝑖 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑆 ‘ 𝑖 ) )
427 54 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝑆 ‘ 𝑗 ) ∈ ℝ )
428 321 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ∈ ℝ )
429 320 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ℝ )
430 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐵 ∈ ℝ )
431 330 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝐵 )
432 276 necomd ⊢ ( ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 → 𝐵 ≠ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) )
433 432 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐵 ≠ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) )
434 429 430 431 433 leneltd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) < 𝐵 )
435 429 430 posdifd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) < 𝐵 ↔ 0 < ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) )
436 434 435 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 0 < ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) )
437 428 436 elrpd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ∈ ℝ+ )
438 427 437 ltaddrpd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝑆 ‘ 𝑗 ) < ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) )
439 438 12 breqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝑆 ‘ 𝑗 ) < 𝑍 )
440 439 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) ∧ 𝑍 = ( 𝑆 ‘ 𝑖 ) ) → ( 𝑆 ‘ 𝑗 ) < 𝑍 )
441 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) ∧ 𝑍 = ( 𝑆 ‘ 𝑖 ) ) → 𝑍 = ( 𝑆 ‘ 𝑖 ) )
442 440 441 breqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) ∧ 𝑍 = ( 𝑆 ‘ 𝑖 ) ) → ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) )
443 394 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) ∧ 𝑍 = ( 𝑆 ‘ 𝑖 ) ) → 𝑍 < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
444 441 443 eqbrtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) ∧ 𝑍 = ( 𝑆 ‘ 𝑖 ) ) → ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
445 442 444 jca ⊢ ( ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) ∧ 𝑍 = ( 𝑆 ‘ 𝑖 ) ) → ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
446 445 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( 𝑍 = ( 𝑆 ‘ 𝑖 ) → ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
447 446 reximdv ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ( ∃ 𝑖 ∈ ( 0 ... 𝑁 ) 𝑍 = ( 𝑆 ‘ 𝑖 ) → ∃ 𝑖 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
448 426 447 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) → ∃ 𝑖 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
449 316 448 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ) → ∃ 𝑖 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
450 252 nrexdv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ¬ ∃ 𝑖 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
451 450 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ) → ¬ ∃ 𝑖 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ 𝑖 ) ∧ ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
452 449 451 condan ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) )
453 309 452 jca ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ∧ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ) )
454 131 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ∈ ℝ )
455 296 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ∈ ℤ )
456 flbi ⊢ ( ( ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ∈ ℝ ∧ ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ∈ ℤ ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ↔ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ∧ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ) ) )
457 454 455 456 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ↔ ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) ≤ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ∧ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) + 1 ) ) ) )
458 453 457 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) )
459 458 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) )
460 459 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) )
461 460 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) )
462 461 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) − ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) ) = ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) − ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) ) )
463 267 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℂ )
464 139 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝑆 ‘ 𝑗 ) ∈ ℂ )
465 140 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ∈ ℂ )
466 463 464 465 pnpcan2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) − ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
467 462 466 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) − ( ( 𝑆 ‘ 𝑗 ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ 𝑗 ) ) / 𝑇 ) ) · 𝑇 ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
468 286 302 467 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
469 271 468 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) )