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	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝑗 ) ∈ ℝ )
44	28 43	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ( 0 ... 𝑀 ) )
45	22 44	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ∈ ℝ )
46	45	rexrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ∈ ℝ* )
47	24	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐼 : ℝ ⟶ ( 0 ..^ 𝑀 ) )
48	47 43	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ( 0 ..^ 𝑀 ) )
49		fzofzp1	⊢ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ∈ ( 0 ..^ 𝑀 ) → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ∈ ( 0 ... 𝑀 ) )
50	48 49	syl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ∈ ( 0 ... 𝑀 ) )
51	22 50	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
108	107 43	resubcld	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) ∈ ℝ )
109	108	rehalfcld	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) ∈ ℝ )
110	21 102	ffvelcdmd	⊢ ( 𝜑 → ( 𝑄 ‘ 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	ffvelcdmd	⊢ ( 𝜑 → ( 𝑄 ‘ 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	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 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	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 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	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 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	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐸 ‘ 𝑥 ) ∈ ( 𝐴 (,] 𝐵 ) )
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	sselid	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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 ) ) ) )