Theorem fourierdlem79 43733

Description: 𝐸 projects every interval of the partition induced by 𝑆 on 𝐻 into a corresponding interval of the partition induced by 𝑄 on [𝐴, 𝐵]. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
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

Ref	Expression
fourierdlem79	⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐿‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))))

Distinct variable groups:   𝐴,𝑖,𝑗,𝑥   𝐴,𝑚,𝑝,𝑖   𝑦,𝐴,𝑗,𝑥   𝐵,𝑓   𝐵,𝑖,𝑘,𝑥   𝐵,𝑚,𝑝   𝑦,𝐵   𝐶,𝑖,𝑚,𝑝   𝑥,𝐶   𝐷,𝑖,𝑚,𝑝   𝑥,𝐷   𝑓,𝐸   𝑖,𝐸,𝑘,𝑥   𝑦,𝐸   𝑓,𝐻   𝑥,𝐻   𝑓,𝐼   𝑖,𝐼,𝑘,𝑥   𝑖,𝐿,𝑥   𝑖,𝑀,𝑗,𝑥   𝑚,𝑀,𝑝   𝑓,𝑁   𝑖,𝑁,𝑘,𝑥   𝑚,𝑁,𝑝   𝑦,𝑁   𝑄,𝑓,𝑗   𝑄,𝑖,𝑘,𝑥,𝑗   𝑄,𝑝   𝑆,𝑓   𝑆,𝑖,𝑘,𝑥   𝑆,𝑝   𝑦,𝑆   𝑇,𝑖,𝑘,𝑥   𝑘,𝑍,𝑥   𝜑,𝑓,𝑗   𝜑,𝑖,𝑘,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜑(𝑚,𝑝)   𝐴(𝑓,𝑘)   𝐵(𝑗)   𝐶(𝑦,𝑓,𝑗,𝑘)   𝐷(𝑦,𝑓,𝑗,𝑘)   𝑃(𝑥,𝑦,𝑓,𝑖,𝑗,𝑘,𝑚,𝑝)   𝑄(𝑦,𝑚)   𝑆(𝑗,𝑚)   𝑇(𝑦,𝑓,𝑗,𝑚,𝑝)   𝐸(𝑗,𝑚,𝑝)   𝐻(𝑦,𝑖,𝑗,𝑘,𝑚,𝑝)   𝐼(𝑦,𝑗,𝑚,𝑝)   𝐿(𝑦,𝑓,𝑗,𝑘,𝑚,𝑝)   𝑀(𝑦,𝑓,𝑘)   𝑁(𝑗)   𝑂(𝑥,𝑦,𝑓,𝑖,𝑗,𝑘,𝑚,𝑝)   𝑍(𝑦,𝑓,𝑖,𝑗,𝑚,𝑝)

Proof of Theorem fourierdlem79

Dummy variable 𝑙 is distinct from all other variables.

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107   ≠ wne 2944  ∀wral 3065  ∃wrex 3066  {crab 3069  Vcvv 3433   ∪ cun 3886   ⊆ wss 3888  ∅c0 4257  ifcif 4460  {csn 4562  {cpr 4564   class class class wbr 5075   ↦ cmpt 5158   Or wor 5503  ran crn 5591  ℩cio 6393  ⟶wf 6433  ‘cfv 6437   Isom wiso 6438  (class class class)co 7284   ↑_m cmap 8624  Fincfn 8742  supcsup 9208  ℂcc 10878  ℝcr 10879  0cc0 10880  1c1 10881   + caddc 10883   · cmul 10885  ℝ^*cxr 11017   < clt 11018   ≤ cle 11019   − cmin 11214   / cdiv 11641  ℕcn 11982  2c2 12037  ℤcz 12328  ℤ_≥cuz 12591  ℝ⁺crp 12739  (,)cioo 13088  (,]cioc 13089  [,)cico 13090  [,]cicc 13091  ...cfz 13248  ..^cfzo 13391  ⌊cfl 13519  ♯chash 14053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-inf2 9408  ax-cnex 10936  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957  ax-pre-sup 10958

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rmo 3072  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-int 4881  df-iun 4927  df-iin 4928  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-se 5546  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-isom 6446  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-om 7722  df-1st 7840  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-1o 8306  df-oadd 8310  df-er 8507  df-map 8626  df-en 8743  df-dom 8744  df-sdom 8745  df-fin 8746  df-fi 9179  df-sup 9210  df-inf 9211  df-oi 9278  df-dju 9668  df-card 9706  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-div 11642  df-nn 11983  df-2 12045  df-3 12046  df-n0 12243  df-xnn0 12315  df-z 12329  df-uz 12592  df-q 12698  df-rp 12740  df-xneg 12857  df-xadd 12858  df-xmul 12859  df-ioo 13092  df-ioc 13093  df-ico 13094  df-icc 13095  df-fz 13249  df-fzo 13392  df-fl 13521  df-seq 13731  df-exp 13792  df-hash 14054  df-cj 14819  df-re 14820  df-im 14821  df-sqrt 14955  df-abs 14956  df-rest 17142  df-topgen 17163  df-psmet 20598  df-xmet 20599  df-met 20600  df-bl 20601  df-mopn 20602  df-top 22052  df-topon 22069  df-bases 22105  df-cld 22179  df-ntr 22180  df-cls 22181  df-nei 22258  df-lp 22296  df-cmp 22547

This theorem is referenced by:  fourierdlem89  43743  fourierdlem90  43744  fourierdlem91  43745