Metamath Proof Explorer

Theorem fourierdlem79

Description: E projects every interval of the partition induced by S on H into a corresponding interval of the partition induced by Q on [ A , B ] . (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step Hyp Ref Expression
1 fourierdlem79.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
2 fourierdlem79.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
3 fourierdlem79.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
4 fourierdlem79.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
5 fourierdlem79.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
6 fourierdlem79.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
7 fourierdlem79.cltd ⊢ ( 𝜑 → 𝐶 < 𝐷 )
8 fourierdlem79.o ⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
9 fourierdlem79.h ⊢ 𝐻 = ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
10 fourierdlem79.n ⊢ 𝑁 = ( ( ♯ ‘ 𝐻 ) − 1 )
11 fourierdlem79.s ⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
12 fourierdlem79.e ⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
13 fourierdlem79.l ⊢ 𝐿 = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) )
14 fourierdlem79.z ⊢ 𝑍 = ( ( 𝑆 ‘ 𝑗 ) + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) )
15 fourierdlem79.i ⊢ 𝐼 = ( 𝑥 ∈ ℝ ↦ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) )
16 2 fourierdlem2 ⊢ ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
17 3 16 syl ⊢ ( 𝜑 → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
18 4 17 mpbid ⊢ ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
19 18 simpld ⊢ ( 𝜑 → 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) )
20 elmapi ⊢ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
21 19 20 syl ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
23 2 3 4 1 12 13 15 fourierdlem37 ⊢ ( 𝜑 → ( 𝐼 : ℝ ⟶ ( 0 ..^ 𝑀 ) ∧ ( 𝑥 ∈ ℝ → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ) ) )
24 23 simpld ⊢ ( 𝜑 → 𝐼 : ℝ ⟶ ( 0 ..^ 𝑀 ) )
25 fzossfz ⊢ ( 0 ..^ 𝑀 ) ⊆ ( 0 ... 𝑀 )
26 25 a1i ⊢ ( 𝜑 → ( 0 ..^ 𝑀 ) ⊆ ( 0 ... 𝑀 ) )
27 24 26 fssd ⊢ ( 𝜑 → 𝐼 : ℝ ⟶ ( 0 ... 𝑀 ) )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐼 : ℝ ⟶ ( 0 ... 𝑀 ) )
29 1 2 3 4 5 6 7 8 9 10 11 fourierdlem54 ⊢ ( 𝜑 → ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ) ∧ 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ) )
30 29 simpld ⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ) )
31 30 simprd ⊢ ( 𝜑 → 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) )
33 30 simpld ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑁 ∈ ℕ )
35 8 fourierdlem2 ⊢ ( 𝑁 ∈ ℕ → ( 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ↔ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ) )
36 34 35 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ↔ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ) )
37 32 36 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) )
38 37 simpld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) )
39 elmapi ⊢ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) → 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ )
40 38 39 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ )
41 elfzofz ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
42 41 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
43 40 42 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) ∈ ℝ )
44 28 43 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ( 0 ... 𝑀 ) )
45 22 44 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ∈ ℝ )
46 45 rexrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ∈ ℝ* )
47 24 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐼 : ℝ ⟶ ( 0 ..^ 𝑀 ) )
48 47 43 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ( 0 ..^ 𝑀 ) )
49 fzofzp1 ⊢ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ( 0 ..^ 𝑀 ) → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ∈ ( 0 ... 𝑀 ) )
50 48 49 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ∈ ( 0 ... 𝑀 ) )
51 22 50 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ∈ ℝ )
52 51 rexrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ∈ ℝ* )
53 15 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐼 = ( 𝑥 ∈ ℝ ↦ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) ) )
54 fveq2 ⊢ ( 𝑥 = ( 𝑆 ‘ 𝑗 ) → ( 𝐸 ‘ 𝑥 ) = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) )
55 54 fveq2d ⊢ ( 𝑥 = ( 𝑆 ‘ 𝑗 ) → ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) = ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) )
56 55 breq2d ⊢ ( 𝑥 = ( 𝑆 ‘ 𝑗 ) → ( ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) ↔ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) )
57 56 rabbidv ⊢ ( 𝑥 = ( 𝑆 ‘ 𝑗 ) → { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } = { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } )
58 57 supeq1d ⊢ ( 𝑥 = ( 𝑆 ‘ 𝑗 ) → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) = sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) )
59 58 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 = ( 𝑆 ‘ 𝑗 ) ) → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) = sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) )
60 ltso ⊢ < Or ℝ
61 60 supex ⊢ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) ∈ V
62 61 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) ∈ V )
63 53 59 43 62 fvmptd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) )
64 63 fveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) = ( 𝑄 ‘ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) ) )
65 simpl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝜑 )
66 65 43 jca ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝜑 ∧ ( 𝑆 ‘ 𝑗 ) ∈ ℝ ) )
67 eleq1 ⊢ ( 𝑥 = ( 𝑆 ‘ 𝑗 ) → ( 𝑥 ∈ ℝ ↔ ( 𝑆 ‘ 𝑗 ) ∈ ℝ ) )
68 67 anbi2d ⊢ ( 𝑥 = ( 𝑆 ‘ 𝑗 ) → ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ↔ ( 𝜑 ∧ ( 𝑆 ‘ 𝑗 ) ∈ ℝ ) ) )
69 58 57 eleq12d ⊢ ( 𝑥 = ( 𝑆 ‘ 𝑗 ) → ( sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ↔ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } ) )
70 68 69 imbi12d ⊢ ( 𝑥 = ( 𝑆 ‘ 𝑗 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ) ↔ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝑗 ) ∈ ℝ ) → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } ) ) )
71 23 simprd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ) )
72 71 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } )
73 70 72 vtoclg ⊢ ( ( 𝑆 ‘ 𝑗 ) ∈ ℝ → ( ( 𝜑 ∧ ( 𝑆 ‘ 𝑗 ) ∈ ℝ ) → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } ) )
74 43 66 73 sylc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } )
75 nfrab1 ⊢ Ⅎ 𝑖 { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) }
76 nfcv ⊢ Ⅎ 𝑖 ℝ
77 nfcv ⊢ Ⅎ 𝑖 <
78 75 76 77 nfsup ⊢ Ⅎ 𝑖 sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < )
79 nfcv ⊢ Ⅎ 𝑖 ( 0 ..^ 𝑀 )
80 nfcv ⊢ Ⅎ 𝑖 𝑄
81 80 78 nffv ⊢ Ⅎ 𝑖 ( 𝑄 ‘ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) )
82 nfcv ⊢ Ⅎ 𝑖 ≤
83 nfcv ⊢ Ⅎ 𝑖 ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) )
84 81 82 83 nfbr ⊢ Ⅎ 𝑖 ( 𝑄 ‘ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) )
85 fveq2 ⊢ ( 𝑖 = sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) ) )
86 85 breq1d ⊢ ( 𝑖 = sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) → ( ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ↔ ( 𝑄 ‘ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) )
87 78 79 84 86 elrabf ⊢ ( sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } ↔ ( sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑄 ‘ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) )
88 74 87 sylib ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑄 ‘ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) )
89 88 simprd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑄 ‘ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) )
90 64 89 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) )
91 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝑀 ∈ ℕ )
92 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
93 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐶 ∈ ℝ )
94 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐷 ∈ ℝ )
95 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐶 < 𝐷 )
96 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
97 3 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
98 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
99 0le1 ⊢ 0 ≤ 1
100 99 a1i ⊢ ( 𝜑 → 0 ≤ 1 )
101 3 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝑀 )
102 96 97 98 100 101 elfzd ⊢ ( 𝜑 → 1 ∈ ( 0 ... 𝑀 ) )
103 102 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 1 ∈ ( 0 ... 𝑀 ) )
104 simplr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝑗 ∈ ( 0 ..^ 𝑁 ) )
105 fzofzp1 ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → ( 𝑗 + 1 ) ∈ ( 0 ... 𝑁 ) )
106 105 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑗 + 1 ) ∈ ( 0 ... 𝑁 ) )
107 40 106 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
108 107 43 resubcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) ∈ ℝ )
109 108 rehalfcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ∈ ℝ )
110 21 102 ffvelrnd ⊢ ( 𝜑 → ( 𝑄 ‘ 1 ) ∈ ℝ )
111 2 3 4 fourierdlem11 ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) )
112 111 simp1d ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
113 110 112 resubcld ⊢ ( 𝜑 → ( ( 𝑄 ‘ 1 ) − 𝐴 ) ∈ ℝ )
114 113 rehalfcld ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ∈ ℝ )
115 114 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ∈ ℝ )
116 109 115 ifcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ∈ ℝ )
117 43 116 readdcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) ∈ ℝ )
118 14 117 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑍 ∈ ℝ )
119 2re ⊢ 2 ∈ ℝ
120 119 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 2 ∈ ℝ )
121 elfzoelz ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → 𝑗 ∈ ℤ )
122 121 zred ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → 𝑗 ∈ ℝ )
123 122 ltp1d ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → 𝑗 < ( 𝑗 + 1 ) )
124 123 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑗 < ( 𝑗 + 1 ) )
125 29 simprd ⊢ ( 𝜑 → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
126 125 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
127 isorel ⊢ ( ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ∧ ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑗 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑗 < ( 𝑗 + 1 ) ↔ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
128 126 42 106 127 syl12anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑗 < ( 𝑗 + 1 ) ↔ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
129 124 128 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
130 43 107 posdifd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ↔ 0 < ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) )
131 129 130 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 0 < ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
132 2pos ⊢ 0 < 2
133 132 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 0 < 2 )
134 108 120 131 133 divgt0d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 0 < ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) )
135 109 134 elrpd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ∈ ℝ+ )
136 119 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
137 3 nngt0d ⊢ ( 𝜑 → 0 < 𝑀 )
138 fzolb ⊢ ( 0 ∈ ( 0 ..^ 𝑀 ) ↔ ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀 ) )
139 96 97 137 138 syl3anbrc ⊢ ( 𝜑 → 0 ∈ ( 0 ..^ 𝑀 ) )
140 0re ⊢ 0 ∈ ℝ
141 eleq1 ⊢ ( 𝑖 = 0 → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↔ 0 ∈ ( 0 ..^ 𝑀 ) ) )
142 141 anbi2d ⊢ ( 𝑖 = 0 → ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ↔ ( 𝜑 ∧ 0 ∈ ( 0 ..^ 𝑀 ) ) ) )
143 fveq2 ⊢ ( 𝑖 = 0 → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 0 ) )
144 oveq1 ⊢ ( 𝑖 = 0 → ( 𝑖 + 1 ) = ( 0 + 1 ) )
145 144 fveq2d ⊢ ( 𝑖 = 0 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( 0 + 1 ) ) )
146 143 145 breq12d ⊢ ( 𝑖 = 0 → ( ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑄 ‘ 0 ) < ( 𝑄 ‘ ( 0 + 1 ) ) ) )
147 142 146 imbi12d ⊢ ( 𝑖 = 0 → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( 𝜑 ∧ 0 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 0 ) < ( 𝑄 ‘ ( 0 + 1 ) ) ) ) )
148 18 simprd ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
149 148 simprd ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
150 149 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
151 147 150 vtoclg ⊢ ( 0 ∈ ℝ → ( ( 𝜑 ∧ 0 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 0 ) < ( 𝑄 ‘ ( 0 + 1 ) ) ) )
152 140 151 ax-mp ⊢ ( ( 𝜑 ∧ 0 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 0 ) < ( 𝑄 ‘ ( 0 + 1 ) ) )
153 139 152 mpdan ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) < ( 𝑄 ‘ ( 0 + 1 ) ) )
154 148 simpld ⊢ ( 𝜑 → ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) )
155 154 simpld ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = 𝐴 )
156 0p1e1 ⊢ ( 0 + 1 ) = 1
157 156 fveq2i ⊢ ( 𝑄 ‘ ( 0 + 1 ) ) = ( 𝑄 ‘ 1 )
158 157 a1i ⊢ ( 𝜑 → ( 𝑄 ‘ ( 0 + 1 ) ) = ( 𝑄 ‘ 1 ) )
159 153 155 158 3brtr3d ⊢ ( 𝜑 → 𝐴 < ( 𝑄 ‘ 1 ) )
160 112 110 posdifd ⊢ ( 𝜑 → ( 𝐴 < ( 𝑄 ‘ 1 ) ↔ 0 < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) )
161 159 160 mpbid ⊢ ( 𝜑 → 0 < ( ( 𝑄 ‘ 1 ) − 𝐴 ) )
162 132 a1i ⊢ ( 𝜑 → 0 < 2 )
163 113 136 161 162 divgt0d ⊢ ( 𝜑 → 0 < ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) )
164 114 163 elrpd ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ∈ ℝ+ )
165 164 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ∈ ℝ+ )
166 135 165 ifcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ∈ ℝ+ )
167 43 166 ltaddrpd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) < ( ( 𝑆 ‘ 𝑗 ) + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) )
168 43 117 167 ltled ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) ≤ ( ( 𝑆 ‘ 𝑗 ) + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) )
169 168 14 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) ≤ 𝑍 )
170 43 109 readdcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) + ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ) ∈ ℝ )
171 iftrue ⊢ ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) → if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) = ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) )
172 171 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) = ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) )
173 109 leidd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ≤ ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) )
174 173 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ≤ ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) )
175 172 174 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ≤ ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) )
176 iffalse ⊢ ( ¬ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) → if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) = ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) )
177 176 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) = ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) )
178 113 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → ( ( 𝑄 ‘ 1 ) − 𝐴 ) ∈ ℝ )
179 108 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) ∈ ℝ )
180 2rp ⊢ 2 ∈ ℝ+
181 180 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → 2 ∈ ℝ+ )
182 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → ¬ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) )
183 178 179 182 nltled ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → ( ( 𝑄 ‘ 1 ) − 𝐴 ) ≤ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
184 178 179 181 183 lediv1dd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ≤ ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) )
185 177 184 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ≤ ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) )
186 175 185 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ≤ ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) )
187 116 109 43 186 leadd2dd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ) )
188 43 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) ∈ ℂ )
189 107 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℂ )
190 188 189 addcomd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( 𝑆 ‘ 𝑗 ) ) )
191 190 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑆 ‘ 𝑗 ) + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 2 ) = ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( 𝑆 ‘ 𝑗 ) ) / 2 ) )
192 191 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( 𝑆 ‘ 𝑗 ) + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 2 ) − ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ) = ( ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( 𝑆 ‘ 𝑗 ) ) / 2 ) − ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ) )
193 halfaddsub ⊢ ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℂ ∧ ( 𝑆 ‘ 𝑗 ) ∈ ℂ ) → ( ( ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( 𝑆 ‘ 𝑗 ) ) / 2 ) + ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ) = ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∧ ( ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( 𝑆 ‘ 𝑗 ) ) / 2 ) − ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ) = ( 𝑆 ‘ 𝑗 ) ) )
194 189 188 193 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( 𝑆 ‘ 𝑗 ) ) / 2 ) + ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ) = ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∧ ( ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( 𝑆 ‘ 𝑗 ) ) / 2 ) − ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ) = ( 𝑆 ‘ 𝑗 ) ) )
195 194 simprd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) + ( 𝑆 ‘ 𝑗 ) ) / 2 ) − ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ) = ( 𝑆 ‘ 𝑗 ) )
196 192 195 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( 𝑆 ‘ 𝑗 ) + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 2 ) − ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ) = ( 𝑆 ‘ 𝑗 ) )
197 188 189 addcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∈ ℂ )
198 197 halfcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑆 ‘ 𝑗 ) + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 2 ) ∈ ℂ )
199 109 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ∈ ℂ )
200 198 199 188 subsub23d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( ( 𝑆 ‘ 𝑗 ) + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 2 ) − ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ) = ( 𝑆 ‘ 𝑗 ) ↔ ( ( ( ( 𝑆 ‘ 𝑗 ) + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 2 ) − ( 𝑆 ‘ 𝑗 ) ) = ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ) )
201 196 200 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( 𝑆 ‘ 𝑗 ) + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 2 ) − ( 𝑆 ‘ 𝑗 ) ) = ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) )
202 198 188 199 subaddd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( ( 𝑆 ‘ 𝑗 ) + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 2 ) − ( 𝑆 ‘ 𝑗 ) ) = ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ↔ ( ( 𝑆 ‘ 𝑗 ) + ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ) = ( ( ( 𝑆 ‘ 𝑗 ) + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 2 ) ) )
203 201 202 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) + ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ) = ( ( ( 𝑆 ‘ 𝑗 ) + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 2 ) )
204 avglt2 ⊢ ( ( ( 𝑆 ‘ 𝑗 ) ∈ ℝ ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ ) → ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ↔ ( ( ( 𝑆 ‘ 𝑗 ) + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 2 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
205 43 107 204 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ↔ ( ( ( 𝑆 ‘ 𝑗 ) + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 2 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
206 129 205 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑆 ‘ 𝑗 ) + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) / 2 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
207 203 206 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) + ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
208 117 170 107 187 207 lelttrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
209 14 208 eqbrtrid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑍 < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
210 107 rexrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ* )
211 elico2 ⊢ ( ( ( 𝑆 ‘ 𝑗 ) ∈ ℝ ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ* ) → ( 𝑍 ∈ ( ( 𝑆 ‘ 𝑗 ) [,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↔ ( 𝑍 ∈ ℝ ∧ ( 𝑆 ‘ 𝑗 ) ≤ 𝑍 ∧ 𝑍 < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
212 43 210 211 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑍 ∈ ( ( 𝑆 ‘ 𝑗 ) [,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↔ ( 𝑍 ∈ ℝ ∧ ( 𝑆 ‘ 𝑗 ) ≤ 𝑍 ∧ 𝑍 < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
213 118 169 209 212 mpbir3and ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑍 ∈ ( ( 𝑆 ‘ 𝑗 ) [,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
214 213 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝑍 ∈ ( ( 𝑆 ‘ 𝑗 ) [,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
215 112 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐴 ∈ ℝ )
216 111 simp2d ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
217 216 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐵 ∈ ℝ )
218 111 simp3d ⊢ ( 𝜑 → 𝐴 < 𝐵 )
219 218 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐴 < 𝐵 )
220 43 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝑆 ‘ 𝑗 ) ∈ ℝ )
221 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 )
222 167 14 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) < 𝑍 )
223 216 112 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
224 1 223 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
225 224 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑇 ∈ ℝ )
226 109 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ∈ ℝ )
227 114 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ∈ ℝ )
228 108 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) ∈ ℝ )
229 113 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → ( ( 𝑄 ‘ 1 ) − 𝐴 ) ∈ ℝ )
230 180 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → 2 ∈ ℝ+ )
231 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) )
232 228 229 230 231 ltdiv1dd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) < ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) )
233 226 227 232 ltled ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ≤ ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) )
234 172 233 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ≤ ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) )
235 176 adantl ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) = ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) )
236 114 leidd ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ≤ ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) )
237 236 adantr ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ≤ ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) )
238 235 237 eqbrtrd ⊢ ( ( 𝜑 ∧ ¬ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ≤ ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) )
239 238 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ≤ ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) )
240 234 239 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ≤ ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) )
241 223 rehalfcld ⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) / 2 ) ∈ ℝ )
242 180 a1i ⊢ ( 𝜑 → 2 ∈ ℝ+ )
243 112 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
244 216 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
245 2 3 4 fourierdlem15 ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( 𝐴 [,] 𝐵 ) )
246 245 102 ffvelrnd ⊢ ( 𝜑 → ( 𝑄 ‘ 1 ) ∈ ( 𝐴 [,] 𝐵 ) )
247 iccleub ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝑄 ‘ 1 ) ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑄 ‘ 1 ) ≤ 𝐵 )
248 243 244 246 247 syl3anc ⊢ ( 𝜑 → ( 𝑄 ‘ 1 ) ≤ 𝐵 )
249 110 216 112 248 lesub1dd ⊢ ( 𝜑 → ( ( 𝑄 ‘ 1 ) − 𝐴 ) ≤ ( 𝐵 − 𝐴 ) )
250 113 223 242 249 lediv1dd ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ≤ ( ( 𝐵 − 𝐴 ) / 2 ) )
251 1 eqcomi ⊢ ( 𝐵 − 𝐴 ) = 𝑇
252 251 oveq1i ⊢ ( ( 𝐵 − 𝐴 ) / 2 ) = ( 𝑇 / 2 )
253 112 216 posdifd ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 − 𝐴 ) ) )
254 218 253 mpbid ⊢ ( 𝜑 → 0 < ( 𝐵 − 𝐴 ) )
255 254 1 breqtrrdi ⊢ ( 𝜑 → 0 < 𝑇 )
256 224 255 elrpd ⊢ ( 𝜑 → 𝑇 ∈ ℝ+ )
257 rphalflt ⊢ ( 𝑇 ∈ ℝ+ → ( 𝑇 / 2 ) < 𝑇 )
258 256 257 syl ⊢ ( 𝜑 → ( 𝑇 / 2 ) < 𝑇 )
259 252 258 eqbrtrid ⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) / 2 ) < 𝑇 )
260 114 241 224 250 259 lelttrd ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) < 𝑇 )
261 114 224 260 ltled ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ≤ 𝑇 )
262 261 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ≤ 𝑇 )
263 116 115 225 240 262 letrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ≤ 𝑇 )
264 116 225 43 263 leadd2dd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
265 14 264 eqbrtrid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑍 ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) )
266 43 rexrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) ∈ ℝ* )
267 43 225 readdcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ ℝ )
268 elioc2 ⊢ ( ( ( 𝑆 ‘ 𝑗 ) ∈ ℝ* ∧ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ∈ ℝ ) → ( 𝑍 ∈ ( ( 𝑆 ‘ 𝑗 ) (,] ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ↔ ( 𝑍 ∈ ℝ ∧ ( 𝑆 ‘ 𝑗 ) < 𝑍 ∧ 𝑍 ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ) )
269 266 267 268 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑍 ∈ ( ( 𝑆 ‘ 𝑗 ) (,] ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ↔ ( 𝑍 ∈ ℝ ∧ ( 𝑆 ‘ 𝑗 ) < 𝑍 ∧ 𝑍 ≤ ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) ) )
270 118 222 265 269 mpbir3and ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑍 ∈ ( ( 𝑆 ‘ 𝑗 ) (,] ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) )
271 270 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝑍 ∈ ( ( 𝑆 ‘ 𝑗 ) (,] ( ( 𝑆 ‘ 𝑗 ) + 𝑇 ) ) )
272 215 217 219 1 12 220 221 271 fourierdlem26 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ 𝑍 ) = ( 𝐴 + ( 𝑍 − ( 𝑆 ‘ 𝑗 ) ) ) )
273 14 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑍 = ( ( 𝑆 ‘ 𝑗 ) + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) )
274 273 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑍 − ( 𝑆 ‘ 𝑗 ) ) = ( ( ( 𝑆 ‘ 𝑗 ) + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) − ( 𝑆 ‘ 𝑗 ) ) )
275 274 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 + ( 𝑍 − ( 𝑆 ‘ 𝑗 ) ) ) = ( 𝐴 + ( ( ( 𝑆 ‘ 𝑗 ) + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) − ( 𝑆 ‘ 𝑗 ) ) ) )
276 275 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐴 + ( 𝑍 − ( 𝑆 ‘ 𝑗 ) ) ) = ( 𝐴 + ( ( ( 𝑆 ‘ 𝑗 ) + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) − ( 𝑆 ‘ 𝑗 ) ) ) )
277 116 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ∈ ℂ )
278 188 277 pncan2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑆 ‘ 𝑗 ) + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) − ( 𝑆 ‘ 𝑗 ) ) = if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) )
279 278 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 + ( ( ( 𝑆 ‘ 𝑗 ) + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) − ( 𝑆 ‘ 𝑗 ) ) ) = ( 𝐴 + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) )
280 279 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐴 + ( ( ( 𝑆 ‘ 𝑗 ) + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) − ( 𝑆 ‘ 𝑗 ) ) ) = ( 𝐴 + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) )
281 272 276 280 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ 𝑍 ) = ( 𝐴 + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) )
282 171 oveq2d ⊢ ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) → ( 𝐴 + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) = ( 𝐴 + ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ) )
283 282 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → ( 𝐴 + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) = ( 𝐴 + ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ) )
284 112 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 ∈ ℝ )
285 284 109 readdcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 + ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ) ∈ ℝ )
286 285 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → ( 𝐴 + ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ) ∈ ℝ )
287 284 115 readdcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 + ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ∈ ℝ )
288 287 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → ( 𝐴 + ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ∈ ℝ )
289 110 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → ( 𝑄 ‘ 1 ) ∈ ℝ )
290 112 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → 𝐴 ∈ ℝ )
291 226 227 290 232 ltadd2dd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → ( 𝐴 + ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ) < ( 𝐴 + ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) )
292 110 recnd ⊢ ( 𝜑 → ( 𝑄 ‘ 1 ) ∈ ℂ )
293 112 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
294 halfaddsub ⊢ ( ( ( 𝑄 ‘ 1 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( ( ( ( 𝑄 ‘ 1 ) + 𝐴 ) / 2 ) + ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) = ( 𝑄 ‘ 1 ) ∧ ( ( ( ( 𝑄 ‘ 1 ) + 𝐴 ) / 2 ) − ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) = 𝐴 ) )
295 292 293 294 syl2anc ⊢ ( 𝜑 → ( ( ( ( ( 𝑄 ‘ 1 ) + 𝐴 ) / 2 ) + ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) = ( 𝑄 ‘ 1 ) ∧ ( ( ( ( 𝑄 ‘ 1 ) + 𝐴 ) / 2 ) − ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) = 𝐴 ) )
296 295 simprd ⊢ ( 𝜑 → ( ( ( ( 𝑄 ‘ 1 ) + 𝐴 ) / 2 ) − ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) = 𝐴 )
297 296 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( 𝑄 ‘ 1 ) + 𝐴 ) / 2 ) − ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) + ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) = ( 𝐴 + ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) )
298 110 112 readdcld ⊢ ( 𝜑 → ( ( 𝑄 ‘ 1 ) + 𝐴 ) ∈ ℝ )
299 298 rehalfcld ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 1 ) + 𝐴 ) / 2 ) ∈ ℝ )
300 299 recnd ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 1 ) + 𝐴 ) / 2 ) ∈ ℂ )
301 114 recnd ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ∈ ℂ )
302 300 301 npcand ⊢ ( 𝜑 → ( ( ( ( ( 𝑄 ‘ 1 ) + 𝐴 ) / 2 ) − ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) + ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) = ( ( ( 𝑄 ‘ 1 ) + 𝐴 ) / 2 ) )
303 297 302 eqtr3d ⊢ ( 𝜑 → ( 𝐴 + ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) = ( ( ( 𝑄 ‘ 1 ) + 𝐴 ) / 2 ) )
304 110 110 readdcld ⊢ ( 𝜑 → ( ( 𝑄 ‘ 1 ) + ( 𝑄 ‘ 1 ) ) ∈ ℝ )
305 112 110 110 159 ltadd2dd ⊢ ( 𝜑 → ( ( 𝑄 ‘ 1 ) + 𝐴 ) < ( ( 𝑄 ‘ 1 ) + ( 𝑄 ‘ 1 ) ) )
306 298 304 242 305 ltdiv1dd ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 1 ) + 𝐴 ) / 2 ) < ( ( ( 𝑄 ‘ 1 ) + ( 𝑄 ‘ 1 ) ) / 2 ) )
307 292 2timesd ⊢ ( 𝜑 → ( 2 · ( 𝑄 ‘ 1 ) ) = ( ( 𝑄 ‘ 1 ) + ( 𝑄 ‘ 1 ) ) )
308 307 eqcomd ⊢ ( 𝜑 → ( ( 𝑄 ‘ 1 ) + ( 𝑄 ‘ 1 ) ) = ( 2 · ( 𝑄 ‘ 1 ) ) )
309 308 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 1 ) + ( 𝑄 ‘ 1 ) ) / 2 ) = ( ( 2 · ( 𝑄 ‘ 1 ) ) / 2 ) )
310 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
311 2ne0 ⊢ 2 ≠ 0
312 311 a1i ⊢ ( 𝜑 → 2 ≠ 0 )
313 292 310 312 divcan3d ⊢ ( 𝜑 → ( ( 2 · ( 𝑄 ‘ 1 ) ) / 2 ) = ( 𝑄 ‘ 1 ) )
314 309 313 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 1 ) + ( 𝑄 ‘ 1 ) ) / 2 ) = ( 𝑄 ‘ 1 ) )
315 306 314 breqtrd ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 1 ) + 𝐴 ) / 2 ) < ( 𝑄 ‘ 1 ) )
316 303 315 eqbrtrd ⊢ ( 𝜑 → ( 𝐴 + ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) < ( 𝑄 ‘ 1 ) )
317 316 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → ( 𝐴 + ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) < ( 𝑄 ‘ 1 ) )
318 286 288 289 291 317 lttrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → ( 𝐴 + ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ) < ( 𝑄 ‘ 1 ) )
319 283 318 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → ( 𝐴 + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) < ( 𝑄 ‘ 1 ) )
320 176 oveq2d ⊢ ( ¬ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) → ( 𝐴 + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) = ( 𝐴 + ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) )
321 320 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → ( 𝐴 + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) = ( 𝐴 + ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) )
322 316 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → ( 𝐴 + ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) < ( 𝑄 ‘ 1 ) )
323 321 322 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) ) → ( 𝐴 + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) < ( 𝑄 ‘ 1 ) )
324 319 323 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) < ( 𝑄 ‘ 1 ) )
325 324 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐴 + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) < ( 𝑄 ‘ 1 ) )
326 281 325 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ 𝑍 ) < ( 𝑄 ‘ 1 ) )
327 eqid ⊢ ( ( 𝑄 ‘ 1 ) − ( ( 𝐸 ‘ 𝑍 ) − 𝑍 ) ) = ( ( 𝑄 ‘ 1 ) − ( ( 𝐸 ‘ 𝑍 ) − 𝑍 ) )
328 1 2 91 92 93 94 95 8 9 10 11 12 103 104 214 326 327 fourierdlem63 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ≤ ( 𝑄 ‘ 1 ) )
329 15 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐼 = ( 𝑥 ∈ ℝ ↦ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) ) )
330 58 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ 𝑥 = ( 𝑆 ‘ 𝑗 ) ) → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) = sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) )
331 61 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) ∈ V )
332 329 330 220 331 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) )
333 fveq2 ⊢ ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) = ( 𝐿 ‘ 𝐵 ) )
334 13 a1i ⊢ ( 𝜑 → 𝐿 = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) ) )
335 iftrue ⊢ ( 𝑦 = 𝐵 → if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) = 𝐴 )
336 335 adantl ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) → if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) = 𝐴 )
337 ubioc1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ( 𝐴 (,] 𝐵 ) )
338 243 244 218 337 syl3anc ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 (,] 𝐵 ) )
339 334 336 338 112 fvmptd ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐵 ) = 𝐴 )
340 333 339 sylan9eqr ⊢ ( ( 𝜑 ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) = 𝐴 )
341 340 breq2d ⊢ ( ( 𝜑 ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ↔ ( 𝑄 ‘ 𝑖 ) ≤ 𝐴 ) )
342 341 rabbidv ⊢ ( ( 𝜑 ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } = { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ 𝐴 } )
343 342 supeq1d ⊢ ( ( 𝜑 ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) = sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ 𝐴 } , ℝ , < ) )
344 343 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) = sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ 𝐴 } , ℝ , < ) )
345 simpl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ 𝐴 } ) → 𝜑 )
346 elrabi ⊢ ( 𝑗 ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ 𝐴 } → 𝑗 ∈ ( 0 ..^ 𝑀 ) )
347 346 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ 𝐴 } ) → 𝑗 ∈ ( 0 ..^ 𝑀 ) )
348 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑗 ) )
349 348 breq1d ⊢ ( 𝑖 = 𝑗 → ( ( 𝑄 ‘ 𝑖 ) ≤ 𝐴 ↔ ( 𝑄 ‘ 𝑗 ) ≤ 𝐴 ) )
350 349 elrab ⊢ ( 𝑗 ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ 𝐴 } ↔ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) ≤ 𝐴 ) )
351 350 simprbi ⊢ ( 𝑗 ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ 𝐴 } → ( 𝑄 ‘ 𝑗 ) ≤ 𝐴 )
352 351 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ 𝐴 } ) → ( 𝑄 ‘ 𝑗 ) ≤ 𝐴 )
353 simp3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) ≤ 𝐴 ) → ( 𝑄 ‘ 𝑗 ) ≤ 𝐴 )
354 112 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑗 ≤ 0 ) → 𝐴 ∈ ℝ )
355 110 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑗 ≤ 0 ) → ( 𝑄 ‘ 1 ) ∈ ℝ )
356 21 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
357 26 sselda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
358 356 357 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑗 ) ∈ ℝ )
359 358 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑗 ≤ 0 ) → ( 𝑄 ‘ 𝑗 ) ∈ ℝ )
360 159 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑗 ≤ 0 ) → 𝐴 < ( 𝑄 ‘ 1 ) )
361 1zzd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑗 ≤ 0 ) → 1 ∈ ℤ )
362 elfzoelz ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 𝑗 ∈ ℤ )
363 362 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑗 ≤ 0 ) → 𝑗 ∈ ℤ )
364 1e0p1 ⊢ 1 = ( 0 + 1 )
365 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑗 ≤ 0 ) → ¬ 𝑗 ≤ 0 )
366 0red ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑗 ≤ 0 ) → 0 ∈ ℝ )
367 363 zred ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑗 ≤ 0 ) → 𝑗 ∈ ℝ )
368 366 367 ltnled ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑗 ≤ 0 ) → ( 0 < 𝑗 ↔ ¬ 𝑗 ≤ 0 ) )
369 365 368 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑗 ≤ 0 ) → 0 < 𝑗 )
370 0zd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑗 ≤ 0 ) → 0 ∈ ℤ )
371 zltp1le ⊢ ( ( 0 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( 0 < 𝑗 ↔ ( 0 + 1 ) ≤ 𝑗 ) )
372 370 363 371 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑗 ≤ 0 ) → ( 0 < 𝑗 ↔ ( 0 + 1 ) ≤ 𝑗 ) )
373 369 372 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑗 ≤ 0 ) → ( 0 + 1 ) ≤ 𝑗 )
374 364 373 eqbrtrid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑗 ≤ 0 ) → 1 ≤ 𝑗 )
375 eluz2 ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 1 ) ↔ ( 1 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 1 ≤ 𝑗 ) )
376 361 363 374 375 syl3anbrc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑗 ≤ 0 ) → 𝑗 ∈ ( ℤ≥ ‘ 1 ) )
377 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... 𝑗 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
378 0zd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... 𝑗 ) ) → 0 ∈ ℤ )
379 97 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... 𝑗 ) ) → 𝑀 ∈ ℤ )
380 elfzelz ⊢ ( 𝑙 ∈ ( 1 ... 𝑗 ) → 𝑙 ∈ ℤ )
381 380 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... 𝑗 ) ) → 𝑙 ∈ ℤ )
382 0red ⊢ ( 𝑙 ∈ ( 1 ... 𝑗 ) → 0 ∈ ℝ )
383 380 zred ⊢ ( 𝑙 ∈ ( 1 ... 𝑗 ) → 𝑙 ∈ ℝ )
384 1red ⊢ ( 𝑙 ∈ ( 1 ... 𝑗 ) → 1 ∈ ℝ )
385 0lt1 ⊢ 0 < 1
386 385 a1i ⊢ ( 𝑙 ∈ ( 1 ... 𝑗 ) → 0 < 1 )
387 elfzle1 ⊢ ( 𝑙 ∈ ( 1 ... 𝑗 ) → 1 ≤ 𝑙 )
388 382 384 383 386 387 ltletrd ⊢ ( 𝑙 ∈ ( 1 ... 𝑗 ) → 0 < 𝑙 )
389 382 383 388 ltled ⊢ ( 𝑙 ∈ ( 1 ... 𝑗 ) → 0 ≤ 𝑙 )
390 389 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... 𝑗 ) ) → 0 ≤ 𝑙 )
391 383 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... 𝑗 ) ) → 𝑙 ∈ ℝ )
392 97 zred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
393 392 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... 𝑗 ) ) → 𝑀 ∈ ℝ )
394 362 zred ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 𝑗 ∈ ℝ )
395 394 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... 𝑗 ) ) → 𝑗 ∈ ℝ )
396 elfzle2 ⊢ ( 𝑙 ∈ ( 1 ... 𝑗 ) → 𝑙 ≤ 𝑗 )
397 396 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... 𝑗 ) ) → 𝑙 ≤ 𝑗 )
398 elfzolt2 ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 𝑗 < 𝑀 )
399 398 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... 𝑗 ) ) → 𝑗 < 𝑀 )
400 391 395 393 397 399 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... 𝑗 ) ) → 𝑙 < 𝑀 )
401 391 393 400 ltled ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... 𝑗 ) ) → 𝑙 ≤ 𝑀 )
402 378 379 381 390 401 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... 𝑗 ) ) → 𝑙 ∈ ( 0 ... 𝑀 ) )
403 377 402 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... 𝑗 ) ) → ( 𝑄 ‘ 𝑙 ) ∈ ℝ )
404 403 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑗 ≤ 0 ) ∧ 𝑙 ∈ ( 1 ... 𝑗 ) ) → ( 𝑄 ‘ 𝑙 ) ∈ ℝ )
405 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
406 0zd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 0 ∈ ℤ )
407 97 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 𝑀 ∈ ℤ )
408 elfzelz ⊢ ( 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) → 𝑙 ∈ ℤ )
409 408 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 𝑙 ∈ ℤ )
410 0red ⊢ ( 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) → 0 ∈ ℝ )
411 408 zred ⊢ ( 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) → 𝑙 ∈ ℝ )
412 1red ⊢ ( 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) → 1 ∈ ℝ )
413 385 a1i ⊢ ( 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) → 0 < 1 )
414 elfzle1 ⊢ ( 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) → 1 ≤ 𝑙 )
415 410 412 411 413 414 ltletrd ⊢ ( 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) → 0 < 𝑙 )
416 410 411 415 ltled ⊢ ( 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) → 0 ≤ 𝑙 )
417 416 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 0 ≤ 𝑙 )
418 409 zred ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 𝑙 ∈ ℝ )
419 392 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 𝑀 ∈ ℝ )
420 394 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 𝑗 ∈ ℝ )
421 411 adantl ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 𝑙 ∈ ℝ )
422 peano2rem ⊢ ( 𝑗 ∈ ℝ → ( 𝑗 − 1 ) ∈ ℝ )
423 394 422 syl ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → ( 𝑗 − 1 ) ∈ ℝ )
424 423 adantr ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → ( 𝑗 − 1 ) ∈ ℝ )
425 394 adantr ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 𝑗 ∈ ℝ )
426 elfzle2 ⊢ ( 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) → 𝑙 ≤ ( 𝑗 − 1 ) )
427 426 adantl ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 𝑙 ≤ ( 𝑗 − 1 ) )
428 425 ltm1d ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → ( 𝑗 − 1 ) < 𝑗 )
429 421 424 425 427 428 lelttrd ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 𝑙 < 𝑗 )
430 429 adantll ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 𝑙 < 𝑗 )
431 398 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 𝑗 < 𝑀 )
432 418 420 419 430 431 lttrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 𝑙 < 𝑀 )
433 418 419 432 ltled ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 𝑙 ≤ 𝑀 )
434 406 407 409 417 433 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 𝑙 ∈ ( 0 ... 𝑀 ) )
435 405 434 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → ( 𝑄 ‘ 𝑙 ) ∈ ℝ )
436 409 peano2zd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → ( 𝑙 + 1 ) ∈ ℤ )
437 411 412 readdcld ⊢ ( 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) → ( 𝑙 + 1 ) ∈ ℝ )
438 411 412 415 413 addgt0d ⊢ ( 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) → 0 < ( 𝑙 + 1 ) )
439 410 437 438 ltled ⊢ ( 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) → 0 ≤ ( 𝑙 + 1 ) )
440 439 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 0 ≤ ( 𝑙 + 1 ) )
441 437 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → ( 𝑙 + 1 ) ∈ ℝ )
442 437 recnd ⊢ ( 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) → ( 𝑙 + 1 ) ∈ ℂ )
443 1cnd ⊢ ( 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) → 1 ∈ ℂ )
444 442 443 npcand ⊢ ( 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) → ( ( ( 𝑙 + 1 ) − 1 ) + 1 ) = ( 𝑙 + 1 ) )
445 444 eqcomd ⊢ ( 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) → ( 𝑙 + 1 ) = ( ( ( 𝑙 + 1 ) − 1 ) + 1 ) )
446 445 adantl ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → ( 𝑙 + 1 ) = ( ( ( 𝑙 + 1 ) − 1 ) + 1 ) )
447 peano2re ⊢ ( 𝑙 ∈ ℝ → ( 𝑙 + 1 ) ∈ ℝ )
448 peano2rem ⊢ ( ( 𝑙 + 1 ) ∈ ℝ → ( ( 𝑙 + 1 ) − 1 ) ∈ ℝ )
449 421 447 448 3syl ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → ( ( 𝑙 + 1 ) − 1 ) ∈ ℝ )
450 peano2re ⊢ ( ( 𝑗 − 1 ) ∈ ℝ → ( ( 𝑗 − 1 ) + 1 ) ∈ ℝ )
451 peano2rem ⊢ ( ( ( 𝑗 − 1 ) + 1 ) ∈ ℝ → ( ( ( 𝑗 − 1 ) + 1 ) − 1 ) ∈ ℝ )
452 424 450 451 3syl ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → ( ( ( 𝑗 − 1 ) + 1 ) − 1 ) ∈ ℝ )
453 1red ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 1 ∈ ℝ )
454 elfzel2 ⊢ ( 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) → ( 𝑗 − 1 ) ∈ ℤ )
455 454 zred ⊢ ( 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) → ( 𝑗 − 1 ) ∈ ℝ )
456 455 412 readdcld ⊢ ( 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) → ( ( 𝑗 − 1 ) + 1 ) ∈ ℝ )
457 411 455 412 426 leadd1dd ⊢ ( 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) → ( 𝑙 + 1 ) ≤ ( ( 𝑗 − 1 ) + 1 ) )
458 437 456 412 457 lesub1dd ⊢ ( 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) → ( ( 𝑙 + 1 ) − 1 ) ≤ ( ( ( 𝑗 − 1 ) + 1 ) − 1 ) )
459 458 adantl ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → ( ( 𝑙 + 1 ) − 1 ) ≤ ( ( ( 𝑗 − 1 ) + 1 ) − 1 ) )
460 449 452 453 459 leadd1dd ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → ( ( ( 𝑙 + 1 ) − 1 ) + 1 ) ≤ ( ( ( ( 𝑗 − 1 ) + 1 ) − 1 ) + 1 ) )
461 peano2zm ⊢ ( 𝑗 ∈ ℤ → ( 𝑗 − 1 ) ∈ ℤ )
462 362 461 syl ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → ( 𝑗 − 1 ) ∈ ℤ )
463 462 peano2zd ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → ( ( 𝑗 − 1 ) + 1 ) ∈ ℤ )
464 463 zcnd ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → ( ( 𝑗 − 1 ) + 1 ) ∈ ℂ )
465 1cnd ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 1 ∈ ℂ )
466 464 465 npcand ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → ( ( ( ( 𝑗 − 1 ) + 1 ) − 1 ) + 1 ) = ( ( 𝑗 − 1 ) + 1 ) )
467 394 recnd ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 𝑗 ∈ ℂ )
468 467 465 npcand ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → ( ( 𝑗 − 1 ) + 1 ) = 𝑗 )
469 466 468 eqtrd ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → ( ( ( ( 𝑗 − 1 ) + 1 ) − 1 ) + 1 ) = 𝑗 )
470 469 adantr ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → ( ( ( ( 𝑗 − 1 ) + 1 ) − 1 ) + 1 ) = 𝑗 )
471 460 470 breqtrd ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → ( ( ( 𝑙 + 1 ) − 1 ) + 1 ) ≤ 𝑗 )
472 446 471 eqbrtrd ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → ( 𝑙 + 1 ) ≤ 𝑗 )
473 472 adantll ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → ( 𝑙 + 1 ) ≤ 𝑗 )
474 441 420 419 473 431 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → ( 𝑙 + 1 ) < 𝑀 )
475 441 419 474 ltled ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → ( 𝑙 + 1 ) ≤ 𝑀 )
476 406 407 436 440 475 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → ( 𝑙 + 1 ) ∈ ( 0 ... 𝑀 ) )
477 405 476 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → ( 𝑄 ‘ ( 𝑙 + 1 ) ) ∈ ℝ )
478 simpll ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 𝜑 )
479 0zd ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 0 ∈ ℤ )
480 408 adantl ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 𝑙 ∈ ℤ )
481 416 adantl ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 0 ≤ 𝑙 )
482 eluz2 ⊢ ( 𝑙 ∈ ( ℤ≥ ‘ 0 ) ↔ ( 0 ∈ ℤ ∧ 𝑙 ∈ ℤ ∧ 0 ≤ 𝑙 ) )
483 479 480 481 482 syl3anbrc ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 𝑙 ∈ ( ℤ≥ ‘ 0 ) )
484 elfzoel2 ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 𝑀 ∈ ℤ )
485 484 adantr ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 𝑀 ∈ ℤ )
486 485 zred ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 𝑀 ∈ ℝ )
487 398 adantr ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 𝑗 < 𝑀 )
488 421 425 486 429 487 lttrd ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 𝑙 < 𝑀 )
489 elfzo2 ⊢ ( 𝑙 ∈ ( 0 ..^ 𝑀 ) ↔ ( 𝑙 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑀 ∈ ℤ ∧ 𝑙 < 𝑀 ) )
490 483 485 488 489 syl3anbrc ⊢ ( ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 𝑙 ∈ ( 0 ..^ 𝑀 ) )
491 490 adantll ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → 𝑙 ∈ ( 0 ..^ 𝑀 ) )
492 eleq1 ⊢ ( 𝑖 = 𝑙 → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↔ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) )
493 492 anbi2d ⊢ ( 𝑖 = 𝑙 → ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ↔ ( 𝜑 ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) ) )
494 fveq2 ⊢ ( 𝑖 = 𝑙 → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑙 ) )
495 oveq1 ⊢ ( 𝑖 = 𝑙 → ( 𝑖 + 1 ) = ( 𝑙 + 1 ) )
496 495 fveq2d ⊢ ( 𝑖 = 𝑙 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( 𝑙 + 1 ) ) )
497 494 496 breq12d ⊢ ( 𝑖 = 𝑙 → ( ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑄 ‘ 𝑙 ) < ( 𝑄 ‘ ( 𝑙 + 1 ) ) ) )
498 493 497 imbi12d ⊢ ( 𝑖 = 𝑙 → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( 𝜑 ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑙 ) < ( 𝑄 ‘ ( 𝑙 + 1 ) ) ) ) )
499 498 150 chvarvv ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑙 ) < ( 𝑄 ‘ ( 𝑙 + 1 ) ) )
500 478 491 499 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → ( 𝑄 ‘ 𝑙 ) < ( 𝑄 ‘ ( 𝑙 + 1 ) ) )
501 435 477 500 ltled ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → ( 𝑄 ‘ 𝑙 ) ≤ ( 𝑄 ‘ ( 𝑙 + 1 ) ) )
502 501 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑗 ≤ 0 ) ∧ 𝑙 ∈ ( 1 ... ( 𝑗 − 1 ) ) ) → ( 𝑄 ‘ 𝑙 ) ≤ ( 𝑄 ‘ ( 𝑙 + 1 ) ) )
503 376 404 502 monoord ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑗 ≤ 0 ) → ( 𝑄 ‘ 1 ) ≤ ( 𝑄 ‘ 𝑗 ) )
504 354 355 359 360 503 ltletrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑗 ≤ 0 ) → 𝐴 < ( 𝑄 ‘ 𝑗 ) )
505 354 359 ltnled ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑗 ≤ 0 ) → ( 𝐴 < ( 𝑄 ‘ 𝑗 ) ↔ ¬ ( 𝑄 ‘ 𝑗 ) ≤ 𝐴 ) )
506 504 505 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ∧ ¬ 𝑗 ≤ 0 ) → ¬ ( 𝑄 ‘ 𝑗 ) ≤ 𝐴 )
507 506 ex ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( ¬ 𝑗 ≤ 0 → ¬ ( 𝑄 ‘ 𝑗 ) ≤ 𝐴 ) )
508 507 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) ≤ 𝐴 ) → ( ¬ 𝑗 ≤ 0 → ¬ ( 𝑄 ‘ 𝑗 ) ≤ 𝐴 ) )
509 353 508 mt4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) ≤ 𝐴 ) → 𝑗 ≤ 0 )
510 elfzole1 ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 0 ≤ 𝑗 )
511 510 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) ≤ 𝐴 ) → 0 ≤ 𝑗 )
512 394 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) ≤ 𝐴 ) → 𝑗 ∈ ℝ )
513 0red ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) ≤ 𝐴 ) → 0 ∈ ℝ )
514 512 513 letri3d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) ≤ 𝐴 ) → ( 𝑗 = 0 ↔ ( 𝑗 ≤ 0 ∧ 0 ≤ 𝑗 ) ) )
515 509 511 514 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑄 ‘ 𝑗 ) ≤ 𝐴 ) → 𝑗 = 0 )
516 345 347 352 515 syl3anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ 𝐴 } ) → 𝑗 = 0 )
517 velsn ⊢ ( 𝑗 ∈ { 0 } ↔ 𝑗 = 0 )
518 516 517 sylibr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ 𝐴 } ) → 𝑗 ∈ { 0 } )
519 518 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ 𝐴 } 𝑗 ∈ { 0 } )
520 dfss3 ⊢ ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ 𝐴 } ⊆ { 0 } ↔ ∀ 𝑗 ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ 𝐴 } 𝑗 ∈ { 0 } )
521 519 520 sylibr ⊢ ( 𝜑 → { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ 𝐴 } ⊆ { 0 } )
522 155 112 eqeltrd ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) ∈ ℝ )
523 522 155 eqled ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) ≤ 𝐴 )
524 143 breq1d ⊢ ( 𝑖 = 0 → ( ( 𝑄 ‘ 𝑖 ) ≤ 𝐴 ↔ ( 𝑄 ‘ 0 ) ≤ 𝐴 ) )
525 524 elrab ⊢ ( 0 ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ 𝐴 } ↔ ( 0 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑄 ‘ 0 ) ≤ 𝐴 ) )
526 139 523 525 sylanbrc ⊢ ( 𝜑 → 0 ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ 𝐴 } )
527 526 snssd ⊢ ( 𝜑 → { 0 } ⊆ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ 𝐴 } )
528 521 527 eqssd ⊢ ( 𝜑 → { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ 𝐴 } = { 0 } )
529 528 supeq1d ⊢ ( 𝜑 → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ 𝐴 } , ℝ , < ) = sup ( { 0 } , ℝ , < ) )
530 supsn ⊢ ( ( < Or ℝ ∧ 0 ∈ ℝ ) → sup ( { 0 } , ℝ , < ) = 0 )
531 60 140 530 mp2an ⊢ sup ( { 0 } , ℝ , < ) = 0
532 531 a1i ⊢ ( 𝜑 → sup ( { 0 } , ℝ , < ) = 0 )
533 529 532 eqtrd ⊢ ( 𝜑 → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ 𝐴 } , ℝ , < ) = 0 )
534 533 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ 𝐴 } , ℝ , < ) = 0 )
535 332 344 534 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = 0 )
536 535 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) = ( 0 + 1 ) )
537 536 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) = ( 𝑄 ‘ ( 0 + 1 ) ) )
538 537 157 eqtr2di ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝑄 ‘ 1 ) = ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) )
539 328 538 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ≤ ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) )
540 66 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝜑 ∧ ( 𝑆 ‘ 𝑗 ) ∈ ℝ ) )
541 simplr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝑗 ∈ ( 0 ..^ 𝑁 ) )
542 13 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐿 = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) ) )
543 simpr ⊢ ( ( ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) )
544 neqne ⊢ ( ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ≠ 𝐵 )
545 544 adantr ⊢ ( ( ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ≠ 𝐵 )
546 543 545 eqnetrd ⊢ ( ( ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → 𝑦 ≠ 𝐵 )
547 546 neneqd ⊢ ( ( ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → ¬ 𝑦 = 𝐵 )
548 547 iffalsed ⊢ ( ( ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) = 𝑦 )
549 548 543 eqtrd ⊢ ( ( ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) )
550 549 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ 𝑦 = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) → if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) )
551 112 216 218 1 12 fourierdlem4 ⊢ ( 𝜑 → 𝐸 : ℝ ⟶ ( 𝐴 (,] 𝐵 ) )
552 551 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐸 : ℝ ⟶ ( 𝐴 (,] 𝐵 ) )
553 552 43 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
554 553 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
555 542 550 554 554 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) = ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) )
556 555 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) )
557 112 216 218 13 fourierdlem17 ⊢ ( 𝜑 → 𝐿 : ( 𝐴 (,] 𝐵 ) ⟶ ( 𝐴 [,] 𝐵 ) )
558 557 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐿 : ( 𝐴 (,] 𝐵 ) ⟶ ( 𝐴 [,] 𝐵 ) )
559 112 216 iccssred ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
560 559 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
561 558 560 fssd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐿 : ( 𝐴 (,] 𝐵 ) ⟶ ℝ )
562 561 553 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ∈ ℝ )
563 562 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ∈ ℝ )
564 556 563 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ℝ )
565 216 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐵 ∈ ℝ )
566 243 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 ∈ ℝ* )
567 216 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐵 ∈ ℝ )
568 elioc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ( 𝐴 (,] 𝐵 ) ↔ ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ℝ ∧ 𝐴 < ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝐵 ) ) )
569 566 567 568 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ( 𝐴 (,] 𝐵 ) ↔ ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ℝ ∧ 𝐴 < ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝐵 ) ) )
570 553 569 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ℝ ∧ 𝐴 < ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝐵 ) )
571 570 simp3d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝐵 )
572 571 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ 𝐵 )
573 544 necomd ⊢ ( ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 → 𝐵 ≠ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) )
574 573 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → 𝐵 ≠ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) )
575 564 565 572 574 leneltd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) < 𝐵 )
576 575 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) < 𝐵 )
577 oveq1 ⊢ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) = ( ( 𝑀 − 1 ) + 1 ) )
578 3 nncnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
579 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
580 578 579 npcand ⊢ ( 𝜑 → ( ( 𝑀 − 1 ) + 1 ) = 𝑀 )
581 577 580 sylan9eqr ⊢ ( ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) = 𝑀 )
582 581 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) = ( 𝑄 ‘ 𝑀 ) )
583 154 simprd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = 𝐵 )
584 583 adantr ⊢ ( ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → ( 𝑄 ‘ 𝑀 ) = 𝐵 )
585 582 584 eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → 𝐵 = ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) )
586 585 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → 𝐵 = ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) )
587 586 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → 𝐵 = ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) )
588 576 587 breqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) )
589 556 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) )
590 ssrab2 ⊢ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } ⊆ ( 0 ..^ 𝑀 )
591 fzssz ⊢ ( 0 ... 𝑀 ) ⊆ ℤ
592 25 591 sstri ⊢ ( 0 ..^ 𝑀 ) ⊆ ℤ
593 zssre ⊢ ℤ ⊆ ℝ
594 592 593 sstri ⊢ ( 0 ..^ 𝑀 ) ⊆ ℝ
595 590 594 sstri ⊢ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } ⊆ ℝ
596 595 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) ∧ ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) → { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } ⊆ ℝ )
597 57 neeq1d ⊢ ( 𝑥 = ( 𝑆 ‘ 𝑗 ) → ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ≠ ∅ ↔ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } ≠ ∅ ) )
598 68 597 imbi12d ⊢ ( 𝑥 = ( 𝑆 ‘ 𝑗 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ≠ ∅ ) ↔ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝑗 ) ∈ ℝ ) → { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } ≠ ∅ ) ) )
599 139 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 0 ∈ ( 0 ..^ 𝑀 ) )
600 523 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐸 ‘ 𝑥 ) = 𝐵 ) → ( 𝑄 ‘ 0 ) ≤ 𝐴 )
601 iftrue ⊢ ( ( 𝐸 ‘ 𝑥 ) = 𝐵 → if ( ( 𝐸 ‘ 𝑥 ) = 𝐵 , 𝐴 , ( 𝐸 ‘ 𝑥 ) ) = 𝐴 )
602 601 eqcomd ⊢ ( ( 𝐸 ‘ 𝑥 ) = 𝐵 → 𝐴 = if ( ( 𝐸 ‘ 𝑥 ) = 𝐵 , 𝐴 , ( 𝐸 ‘ 𝑥 ) ) )
603 602 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐸 ‘ 𝑥 ) = 𝐵 ) → 𝐴 = if ( ( 𝐸 ‘ 𝑥 ) = 𝐵 , 𝐴 , ( 𝐸 ‘ 𝑥 ) ) )
604 600 603 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐸 ‘ 𝑥 ) = 𝐵 ) → ( 𝑄 ‘ 0 ) ≤ if ( ( 𝐸 ‘ 𝑥 ) = 𝐵 , 𝐴 , ( 𝐸 ‘ 𝑥 ) ) )
605 522 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑄 ‘ 0 ) ∈ ℝ )
606 112 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ ℝ )
607 606 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ ℝ* )
608 216 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐵 ∈ ℝ )
609 iocssre ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
610 607 608 609 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
611 551 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐸 ‘ 𝑥 ) ∈ ( 𝐴 (,] 𝐵 ) )
612 610 611 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐸 ‘ 𝑥 ) ∈ ℝ )
613 155 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑄 ‘ 0 ) = 𝐴 )
614 elioc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ( 𝐸 ‘ 𝑥 ) ∈ ( 𝐴 (,] 𝐵 ) ↔ ( ( 𝐸 ‘ 𝑥 ) ∈ ℝ ∧ 𝐴 < ( 𝐸 ‘ 𝑥 ) ∧ ( 𝐸 ‘ 𝑥 ) ≤ 𝐵 ) ) )
615 607 608 614 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐸 ‘ 𝑥 ) ∈ ( 𝐴 (,] 𝐵 ) ↔ ( ( 𝐸 ‘ 𝑥 ) ∈ ℝ ∧ 𝐴 < ( 𝐸 ‘ 𝑥 ) ∧ ( 𝐸 ‘ 𝑥 ) ≤ 𝐵 ) ) )
616 611 615 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐸 ‘ 𝑥 ) ∈ ℝ ∧ 𝐴 < ( 𝐸 ‘ 𝑥 ) ∧ ( 𝐸 ‘ 𝑥 ) ≤ 𝐵 ) )
617 616 simp2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐴 < ( 𝐸 ‘ 𝑥 ) )
618 613 617 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑄 ‘ 0 ) < ( 𝐸 ‘ 𝑥 ) )
619 605 612 618 ltled ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑄 ‘ 0 ) ≤ ( 𝐸 ‘ 𝑥 ) )
620 619 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ ( 𝐸 ‘ 𝑥 ) = 𝐵 ) → ( 𝑄 ‘ 0 ) ≤ ( 𝐸 ‘ 𝑥 ) )
621 iffalse ⊢ ( ¬ ( 𝐸 ‘ 𝑥 ) = 𝐵 → if ( ( 𝐸 ‘ 𝑥 ) = 𝐵 , 𝐴 , ( 𝐸 ‘ 𝑥 ) ) = ( 𝐸 ‘ 𝑥 ) )
622 621 eqcomd ⊢ ( ¬ ( 𝐸 ‘ 𝑥 ) = 𝐵 → ( 𝐸 ‘ 𝑥 ) = if ( ( 𝐸 ‘ 𝑥 ) = 𝐵 , 𝐴 , ( 𝐸 ‘ 𝑥 ) ) )
623 622 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ ( 𝐸 ‘ 𝑥 ) = 𝐵 ) → ( 𝐸 ‘ 𝑥 ) = if ( ( 𝐸 ‘ 𝑥 ) = 𝐵 , 𝐴 , ( 𝐸 ‘ 𝑥 ) ) )
624 620 623 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ ( 𝐸 ‘ 𝑥 ) = 𝐵 ) → ( 𝑄 ‘ 0 ) ≤ if ( ( 𝐸 ‘ 𝑥 ) = 𝐵 , 𝐴 , ( 𝐸 ‘ 𝑥 ) ) )
625 604 624 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑄 ‘ 0 ) ≤ if ( ( 𝐸 ‘ 𝑥 ) = 𝐵 , 𝐴 , ( 𝐸 ‘ 𝑥 ) ) )
626 13 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐿 = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) ) )
627 eqeq1 ⊢ ( 𝑦 = ( 𝐸 ‘ 𝑥 ) → ( 𝑦 = 𝐵 ↔ ( 𝐸 ‘ 𝑥 ) = 𝐵 ) )
628 id ⊢ ( 𝑦 = ( 𝐸 ‘ 𝑥 ) → 𝑦 = ( 𝐸 ‘ 𝑥 ) )
629 627 628 ifbieq2d ⊢ ( 𝑦 = ( 𝐸 ‘ 𝑥 ) → if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) = if ( ( 𝐸 ‘ 𝑥 ) = 𝐵 , 𝐴 , ( 𝐸 ‘ 𝑥 ) ) )
630 629 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 = ( 𝐸 ‘ 𝑥 ) ) → if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) = if ( ( 𝐸 ‘ 𝑥 ) = 𝐵 , 𝐴 , ( 𝐸 ‘ 𝑥 ) ) )
631 606 612 ifcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( ( 𝐸 ‘ 𝑥 ) = 𝐵 , 𝐴 , ( 𝐸 ‘ 𝑥 ) ) ∈ ℝ )
632 626 630 611 631 fvmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) = if ( ( 𝐸 ‘ 𝑥 ) = 𝐵 , 𝐴 , ( 𝐸 ‘ 𝑥 ) ) )
633 625 632 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑄 ‘ 0 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) )
634 143 breq1d ⊢ ( 𝑖 = 0 → ( ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) ↔ ( 𝑄 ‘ 0 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) ) )
635 634 elrab ⊢ ( 0 ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ↔ ( 0 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑄 ‘ 0 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) ) )
636 599 633 635 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 0 ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } )
637 ne0i ⊢ ( 0 ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } → { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ≠ ∅ )
638 636 637 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ≠ ∅ )
639 598 638 vtoclg ⊢ ( ( 𝑆 ‘ 𝑗 ) ∈ ℝ → ( ( 𝜑 ∧ ( 𝑆 ‘ 𝑗 ) ∈ ℝ ) → { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } ≠ ∅ ) )
640 43 66 639 sylc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } ≠ ∅ )
641 640 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) ∧ ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) → { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } ≠ ∅ )
642 595 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } ⊆ ℝ )
643 fzofi ⊢ ( 0 ..^ 𝑀 ) ∈ Fin
644 ssfi ⊢ ( ( ( 0 ..^ 𝑀 ) ∈ Fin ∧ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } ⊆ ( 0 ..^ 𝑀 ) ) → { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } ∈ Fin )
645 643 590 644 mp2an ⊢ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } ∈ Fin
646 645 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } ∈ Fin )
647 fimaxre2 ⊢ ( ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } ⊆ ℝ ∧ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } ∈ Fin ) → ∃ 𝑥 ∈ ℝ ∀ 𝑙 ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } 𝑙 ≤ 𝑥 )
648 642 646 647 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑙 ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } 𝑙 ≤ 𝑥 )
649 648 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) ∧ ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑙 ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } 𝑙 ≤ 𝑥 )
650 0red ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 0 ∈ ℝ )
651 594 48 sseldi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ℝ )
652 1red ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 1 ∈ ℝ )
653 651 652 readdcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ∈ ℝ )
654 elfzouz ⊢ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ( 0 ..^ 𝑀 ) → ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ( ℤ≥ ‘ 0 ) )
655 eluzle ⊢ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ( ℤ≥ ‘ 0 ) → 0 ≤ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) )
656 48 654 655 3syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 0 ≤ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) )
657 385 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 0 < 1 )
658 651 652 656 657 addgegt0d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 0 < ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) )
659 650 653 658 ltled ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 0 ≤ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) )
660 659 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → 0 ≤ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) )
661 651 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ℝ )
662 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
663 392 662 resubcld ⊢ ( 𝜑 → ( 𝑀 − 1 ) ∈ ℝ )
664 663 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → ( 𝑀 − 1 ) ∈ ℝ )
665 1red ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → 1 ∈ ℝ )
666 elfzolt2 ⊢ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ( 0 ..^ 𝑀 ) → ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) < 𝑀 )
667 48 666 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) < 𝑀 )
668 44 elfzelzd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ℤ )
669 97 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑀 ∈ ℤ )
670 zltlem1 ⊢ ( ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) < 𝑀 ↔ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ ( 𝑀 − 1 ) ) )
671 668 669 670 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) < 𝑀 ↔ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ ( 𝑀 − 1 ) ) )
672 667 671 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ ( 𝑀 − 1 ) )
673 672 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ≤ ( 𝑀 − 1 ) )
674 neqne ⊢ ( ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) → ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ≠ ( 𝑀 − 1 ) )
675 674 necomd ⊢ ( ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) → ( 𝑀 − 1 ) ≠ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) )
676 675 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → ( 𝑀 − 1 ) ≠ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) )
677 661 664 673 676 leneltd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) < ( 𝑀 − 1 ) )
678 661 664 665 677 ltadd1dd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) < ( ( 𝑀 − 1 ) + 1 ) )
679 580 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → ( ( 𝑀 − 1 ) + 1 ) = 𝑀 )
680 678 679 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) < 𝑀 )
681 50 elfzelzd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ∈ ℤ )
682 681 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ∈ ℤ )
683 0zd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → 0 ∈ ℤ )
684 97 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → 𝑀 ∈ ℤ )
685 elfzo ⊢ ( ( ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ∈ ( 0 ..^ 𝑀 ) ↔ ( 0 ≤ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ∧ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) < 𝑀 ) ) )
686 682 683 684 685 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → ( ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ∈ ( 0 ..^ 𝑀 ) ↔ ( 0 ≤ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ∧ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) < 𝑀 ) ) )
687 660 680 686 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ∈ ( 0 ..^ 𝑀 ) )
688 687 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) ∧ ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ∈ ( 0 ..^ 𝑀 ) )
689 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) ∧ ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) → ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) )
690 fveq2 ⊢ ( 𝑖 = ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) )
691 690 breq1d ⊢ ( 𝑖 = ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) → ( ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ↔ ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) )
692 691 elrab ⊢ ( ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } ↔ ( ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) )
693 688 689 692 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) ∧ ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } )
694 suprub ⊢ ( ( ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } ⊆ ℝ ∧ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑙 ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } 𝑙 ≤ 𝑥 ) ∧ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } ) → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ≤ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) )
695 596 641 649 693 694 syl31anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) ∧ ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ≤ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) )
696 63 eqcomd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) = ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) )
697 696 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) ∧ ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) } , ℝ , < ) = ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) )
698 695 697 breqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) ∧ ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ≤ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) )
699 651 ltp1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) )
700 651 653 ltnled ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ↔ ¬ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ≤ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) )
701 699 700 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ¬ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ≤ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) )
702 701 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) ∧ ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) → ¬ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ≤ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) )
703 698 702 pm2.65da ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → ¬ ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) )
704 562 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ∈ ℝ )
705 51 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ∈ ℝ )
706 704 705 ltnled ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ↔ ¬ ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) )
707 703 706 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) )
708 707 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) )
709 589 708 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) ∧ ¬ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝑀 − 1 ) ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) )
710 588 709 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) )
711 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) → 𝑀 ∈ ℕ )
712 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
713 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) → 𝐶 ∈ ℝ )
714 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) → 𝐷 ∈ ℝ )
715 7 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) → 𝐶 < 𝐷 )
716 50 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ∈ ( 0 ... 𝑀 ) )
717 simp2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) → 𝑗 ∈ ( 0 ..^ 𝑁 ) )
718 43 leidd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) ≤ ( 𝑆 ‘ 𝑗 ) )
719 elico2 ⊢ ( ( ( 𝑆 ‘ 𝑗 ) ∈ ℝ ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ* ) → ( ( 𝑆 ‘ 𝑗 ) ∈ ( ( 𝑆 ‘ 𝑗 ) [,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↔ ( ( 𝑆 ‘ 𝑗 ) ∈ ℝ ∧ ( 𝑆 ‘ 𝑗 ) ≤ ( 𝑆 ‘ 𝑗 ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
720 43 210 719 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑗 ) ∈ ( ( 𝑆 ‘ 𝑗 ) [,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↔ ( ( 𝑆 ‘ 𝑗 ) ∈ ℝ ∧ ( 𝑆 ‘ 𝑗 ) ≤ ( 𝑆 ‘ 𝑗 ) ∧ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
721 43 718 129 720 mpbir3and ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) ∈ ( ( 𝑆 ‘ 𝑗 ) [,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
722 721 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) → ( 𝑆 ‘ 𝑗 ) ∈ ( ( 𝑆 ‘ 𝑗 ) [,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
723 simp3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) )
724 eqid ⊢ ( ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) − ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) = ( ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) − ( ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
725 1 2 711 712 713 714 715 8 9 10 11 12 716 717 722 723 724 fourierdlem63 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ≤ ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) )
726 725 3adant1r ⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ 𝑗 ) ∈ ℝ ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ≤ ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) )
727 540 541 710 726 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ ¬ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = 𝐵 ) → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ≤ ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) )
728 539 727 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ≤ ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) )
729 ioossioo ⊢ ( ( ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ∈ ℝ* ∧ ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ∈ ℝ* ) ∧ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ≤ ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) ) → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) )
730 46 52 90 728 729 syl22anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) )