Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem79 Structured version   Visualization version   GIF version
Theorem fourierdlem79 40402
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 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem79.m (𝜑 → 𝑀 ∈ ℕ)
fourierdlem79.q (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
fourierdlem79.c (𝜑 → 𝐶 ∈ ℝ)
fourierdlem79.d (𝜑 → 𝐷 ∈ ℝ)
fourierdlem79.cltd (𝜑 → 𝐶 < 𝐷)
fourierdlem79.o 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (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.
StepHypRef Expression
1 fourierdlem79.q . . . . . . . 8 (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
2 fourierdlem79.m . . . . . . . . 9 (𝜑 → 𝑀 ∈ ℕ)
3 fourierdlem79.p . . . . . . . . . 10 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
43fourierdlem2 40326 . . . . . . . . 9 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
52, 4syl 17 . . . . . . . 8 (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
61, 5mpbid 222 . . . . . . 7 (𝜑 → (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
76simpld 475 . . . . . 6 (𝜑 → 𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)))
8 elmapi 7879 . . . . . 6 (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
97, 8syl 17 . . . . 5 (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
109adantr 481 . . . 4 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑄:(0...𝑀)⟶ℝ)
11 fourierdlem79.t . . . . . . . . 9 𝑇 = (𝐵 − 𝐴)
12 fourierdlem79.e . . . . . . . . 9 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
13 fourierdlem79.l . . . . . . . . 9 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))
14 fourierdlem79.i . . . . . . . . 9 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ))
153, 2, 1, 11, 12, 13, 14fourierdlem37 40361 . . . . . . . 8 (𝜑 → (𝐼:ℝ⟶(0..^𝑀) ∧ (𝑥 ∈ ℝ → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))})))
1615simpld 475 . . . . . . 7 (𝜑 → 𝐼:ℝ⟶(0..^𝑀))
17 fzossfz 12488 . . . . . . . 8 (0..^𝑀) ⊆ (0...𝑀)
1817a1i 11 . . . . . . 7 (𝜑 → (0..^𝑀) ⊆ (0...𝑀))
1916, 18fssd 6057 . . . . . 6 (𝜑 → 𝐼:ℝ⟶(0...𝑀))
2019adantr 481 . . . . 5 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐼:ℝ⟶(0...𝑀))
21 fourierdlem79.c . . . . . . . . . . . . 13 (𝜑 → 𝐶 ∈ ℝ)
22 fourierdlem79.d . . . . . . . . . . . . 13 (𝜑 → 𝐷 ∈ ℝ)
23 fourierdlem79.cltd . . . . . . . . . . . . 13 (𝜑 → 𝐶 < 𝐷)
24 fourierdlem79.o . . . . . . . . . . . . 13 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
25 fourierdlem79.h . . . . . . . . . . . . 13 𝐻 = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
26 fourierdlem79.n . . . . . . . . . . . . 13 𝑁 = ((#‘𝐻) − 1)
27 fourierdlem79.s . . . . . . . . . . . . 13 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
2811, 3, 2, 1, 21, 22, 23, 24, 25, 26, 27fourierdlem54 40377 . . . . . . . . . . . 12 (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
2928simpld 475 . . . . . . . . . . 11 (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)))
3029simprd 479 . . . . . . . . . 10 (𝜑 → 𝑆 ∈ (𝑂‘𝑁))
3130adantr 481 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑆 ∈ (𝑂‘𝑁))
3229simpld 475 . . . . . . . . . . 11 (𝜑 → 𝑁 ∈ ℕ)
3332adantr 481 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑁 ∈ ℕ)
3424fourierdlem2 40326 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
3533, 34syl 17 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
3631, 35mpbid 222 . . . . . . . 8 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))
3736simpld 475 . . . . . . 7 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)))
38 elmapi 7879 . . . . . . 7 (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
3937, 38syl 17 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
40 elfzofz 12485 . . . . . . 7 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ (0...𝑁))
4140adantl 482 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0...𝑁))
4239, 41ffvelrnd 6360 . . . . 5 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ ℝ)
4320, 42ffvelrnd 6360 . . . 4 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) ∈ (0...𝑀))
4410, 43ffvelrnd 6360 . . 3 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆‘𝑗))) ∈ ℝ)
4544rexrd 10089 . 2 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆‘𝑗))) ∈ ℝ*)
4616adantr 481 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐼:ℝ⟶(0..^𝑀))
4746, 42ffvelrnd 6360 . . . . 5 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) ∈ (0..^𝑀))
48 fzofzp1 12565 . . . . 5 ((𝐼‘(𝑆‘𝑗)) ∈ (0..^𝑀) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0...𝑀))
4947, 48syl 17 . . . 4 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0...𝑀))
5010, 49ffvelrnd 6360 . . 3 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ∈ ℝ)
5150rexrd 10089 . 2 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ∈ ℝ*)
5214a1i 11 . . . . 5 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < )))
53 fveq2 6191 . . . . . . . . . 10 (𝑥 = (𝑆‘𝑗) → (𝐸‘𝑥) = (𝐸‘(𝑆‘𝑗)))
5453fveq2d 6195 . . . . . . . . 9 (𝑥 = (𝑆‘𝑗) → (𝐿‘(𝐸‘𝑥)) = (𝐿‘(𝐸‘(𝑆‘𝑗))))
5554breq2d 4665 . . . . . . . 8 (𝑥 = (𝑆‘𝑗) → ((𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥)) ↔ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))))
5655rabbidv 3189 . . . . . . 7 (𝑥 = (𝑆‘𝑗) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} = {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))})
5756supeq1d 8352 . . . . . 6 (𝑥 = (𝑆‘𝑗) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ))
5857adantl 482 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 = (𝑆‘𝑗)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ))
59 ltso 10118 . . . . . . 7 < Or ℝ
6059supex 8369 . . . . . 6 sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ V
6160a1i 11 . . . . 5 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ V)
6252, 58, 42, 61fvmptd 6288 . . . 4 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ))
6362fveq2d 6195 . . 3 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆‘𝑗))) = (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )))
64 simpl 473 . . . . . . 7 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝜑)
6564, 42jca 554 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝜑 ∧ (𝑆‘𝑗) ∈ ℝ))
66 eleq1 2689 . . . . . . . . 9 (𝑥 = (𝑆‘𝑗) → (𝑥 ∈ ℝ ↔ (𝑆‘𝑗) ∈ ℝ))
6766anbi2d 740 . . . . . . . 8 (𝑥 = (𝑆‘𝑗) → ((𝜑 ∧ 𝑥 ∈ ℝ) ↔ (𝜑 ∧ (𝑆‘𝑗) ∈ ℝ)))
6857, 56eleq12d 2695 . . . . . . . 8 (𝑥 = (𝑆‘𝑗) → (sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ↔ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}))
6967, 68imbi12d 334 . . . . . . 7 (𝑥 = (𝑆‘𝑗) → (((𝜑 ∧ 𝑥 ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}) ↔ ((𝜑 ∧ (𝑆‘𝑗) ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))})))
7015simprd 479 . . . . . . . 8 (𝜑 → (𝑥 ∈ ℝ → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}))
7170imp 445 . . . . . . 7 ((𝜑 ∧ 𝑥 ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))})
7269, 71vtoclg 3266 . . . . . 6 ((𝑆‘𝑗) ∈ ℝ → ((𝜑 ∧ (𝑆‘𝑗) ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}))
7342, 65, 72sylc 65 . . . . 5 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))})
74 nfrab1 3122 . . . . . . 7 Ⅎ𝑖{𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}
75 nfcv 2764 . . . . . . 7 Ⅎ𝑖ℝ
76 nfcv 2764 . . . . . . 7 Ⅎ𝑖 <
7774, 75, 76nfsup 8357 . . . . . 6 Ⅎ𝑖sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )
78 nfcv 2764 . . . . . 6 Ⅎ𝑖(0..^𝑀)
79 nfcv 2764 . . . . . . . 8 Ⅎ𝑖𝑄
8079, 77nffv 6198 . . . . . . 7 Ⅎ𝑖(𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ))
81 nfcv 2764 . . . . . . 7 Ⅎ𝑖 ≤
82 nfcv 2764 . . . . . . 7 Ⅎ𝑖(𝐿‘(𝐸‘(𝑆‘𝑗)))
8380, 81, 82nfbr 4699 . . . . . 6 Ⅎ𝑖(𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))
84 fveq2 6191 . . . . . . 7 (𝑖 = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) → (𝑄‘𝑖) = (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )))
8584breq1d 4663 . . . . . 6 (𝑖 = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) → ((𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))) ↔ (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))))
8677, 78, 83, 85elrabf 3360 . . . . 5 (sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ↔ (sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ (0..^𝑀) ∧ (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))))
8773, 86sylib 208 . . . 4 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ (0..^𝑀) ∧ (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))))
8887simprd 479 . . 3 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))))
8963, 88eqbrtrd 4675 . 2 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆‘𝑗))) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))))
902ad2antrr 762 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝑀 ∈ ℕ)
911ad2antrr 762 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝑄 ∈ (𝑃‘𝑀))
9221ad2antrr 762 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐶 ∈ ℝ)
9322ad2antrr 762 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐷 ∈ ℝ)
9423ad2antrr 762 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐶 < 𝐷)
95 0le1 10551 . . . . . . . 8 0 ≤ 1
9695a1i 11 . . . . . . 7 (𝜑 → 0 ≤ 1)
972nnge1d 11063 . . . . . . 7 (𝜑 → 1 ≤ 𝑀)
98 1zzd 11408 . . . . . . . 8 (𝜑 → 1 ∈ ℤ)
99 0zd 11389 . . . . . . . 8 (𝜑 → 0 ∈ ℤ)
1002nnzd 11481 . . . . . . . 8 (𝜑 → 𝑀 ∈ ℤ)
101 elfz 12332 . . . . . . . 8 ((1 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (1 ∈ (0...𝑀) ↔ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
10298, 99, 100, 101syl3anc 1326 . . . . . . 7 (𝜑 → (1 ∈ (0...𝑀) ↔ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
10396, 97, 102mpbir2and 957 . . . . . 6 (𝜑 → 1 ∈ (0...𝑀))
104103ad2antrr 762 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 1 ∈ (0...𝑀))
105 simplr 792 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝑗 ∈ (0..^𝑁))
106 fourierdlem79.z . . . . . . . 8 𝑍 = ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)))
107 fzofzp1 12565 . . . . . . . . . . . . . 14 (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ (0...𝑁))
108107adantl 482 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈ (0...𝑁))
10939, 108ffvelrnd 6360 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
110109, 42resubcld 10458 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) ∈ ℝ)
111110rehalfcld 11279 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ∈ ℝ)
1129, 103ffvelrnd 6360 . . . . . . . . . . . . 13 (𝜑 → (𝑄‘1) ∈ ℝ)
1133, 2, 1fourierdlem11 40335 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
114113simp1d 1073 . . . . . . . . . . . . 13 (𝜑 → 𝐴 ∈ ℝ)
115112, 114resubcld 10458 . . . . . . . . . . . 12 (𝜑 → ((𝑄‘1) − 𝐴) ∈ ℝ)
116115rehalfcld 11279 . . . . . . . . . . 11 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ)
117116adantr 481 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ)
118111, 117ifcld 4131 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ∈ ℝ)
11942, 118readdcld 10069 . . . . . . . 8 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) ∈ ℝ)
120106, 119syl5eqel 2705 . . . . . . 7 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 ∈ ℝ)
121 2re 11090 . . . . . . . . . . . . . 14 2 ∈ ℝ
122121a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 2 ∈ ℝ)
123 elfzoelz 12470 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℤ)
124123zred 11482 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℝ)
125124ltp1d 10954 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0..^𝑁) → 𝑗 < (𝑗 + 1))
126125adantl 482 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 < (𝑗 + 1))
12728simprd 479 . . . . . . . . . . . . . . . . 17 (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝐻))
128127adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑆 Isom < , < ((0...𝑁), 𝐻))
129 isorel 6576 . . . . . . . . . . . . . . . 16 ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝑗 + 1) ∈ (0...𝑁))) → (𝑗 < (𝑗 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1))))
130128, 41, 108, 129syl12anc 1324 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 < (𝑗 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1))))
131126, 130mpbid 222 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))
13242, 109posdifd 10614 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) < (𝑆‘(𝑗 + 1)) ↔ 0 < ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗))))
133131, 132mpbid 222 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 < ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)))
134 2pos 11112 . . . . . . . . . . . . . 14 0 < 2
135134a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 < 2)
136110, 122, 133, 135divgt0d 10959 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 < (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
137111, 136elrpd 11869 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ∈ ℝ+)
138121a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 2 ∈ ℝ)
1392nngt0d 11064 . . . . . . . . . . . . . . . . . 18 (𝜑 → 0 < 𝑀)
140 fzolb 12476 . . . . . . . . . . . . . . . . . 18 (0 ∈ (0..^𝑀) ↔ (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
14199, 100, 139, 140syl3anbrc 1246 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ∈ (0..^𝑀))
142 0re 10040 . . . . . . . . . . . . . . . . . 18 0 ∈ ℝ
143 eleq1 2689 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 0 → (𝑖 ∈ (0..^𝑀) ↔ 0 ∈ (0..^𝑀)))
144143anbi2d 740 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 0 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 0 ∈ (0..^𝑀))))
145 fveq2 6191 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 0 → (𝑄‘𝑖) = (𝑄‘0))
146 oveq1 6657 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 0 → (𝑖 + 1) = (0 + 1))
147146fveq2d 6195 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 0 → (𝑄‘(𝑖 + 1)) = (𝑄‘(0 + 1)))
148145, 147breq12d 4666 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 0 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘0) < (𝑄‘(0 + 1))))
149144, 148imbi12d 334 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 0 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))))
1506simprd 479 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
151150simprd 479 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
152151r19.21bi 2932 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
153149, 152vtoclg 3266 . . . . . . . . . . . . . . . . . 18 (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1))))
154142, 153ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))
155141, 154mpdan 702 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘0) < (𝑄‘(0 + 1)))
156150simpld 475 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
157156simpld 475 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘0) = 𝐴)
158 0p1e1 11132 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
159158fveq2i 6194 . . . . . . . . . . . . . . . . 17 (𝑄‘(0 + 1)) = (𝑄‘1)
160159a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘(0 + 1)) = (𝑄‘1))
161155, 157, 1603brtr3d 4684 . . . . . . . . . . . . . . 15 (𝜑 → 𝐴 < (𝑄‘1))
162114, 112posdifd 10614 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 < (𝑄‘1) ↔ 0 < ((𝑄‘1) − 𝐴)))
163161, 162mpbid 222 . . . . . . . . . . . . . 14 (𝜑 → 0 < ((𝑄‘1) − 𝐴))
164134a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 0 < 2)
165115, 138, 163, 164divgt0d 10959 . . . . . . . . . . . . 13 (𝜑 → 0 < (((𝑄‘1) − 𝐴) / 2))
166116, 165elrpd 11869 . . . . . . . . . . . 12 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ+)
167166adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ+)
168137, 167ifcld 4131 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ∈ ℝ+)
16942, 168ltaddrpd 11905 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) < ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
17042, 119, 169ltled 10185 . . . . . . . 8 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ≤ ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
171170, 106syl6breqr 4695 . . . . . . 7 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ≤ 𝑍)
17242, 111readdcld 10069 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) ∈ ℝ)
173 iftrue 4092 . . . . . . . . . . . . 13 (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
174173adantl 482 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
175111leidd 10594 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
176175adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
177174, 176eqbrtrd 4675 . . . . . . . . . . 11 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
178 iffalse 4095 . . . . . . . . . . . . 13 (¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) − 𝐴) / 2))
179178adantl 482 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) − 𝐴) / 2))
180115ad2antrr 762 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑄‘1) − 𝐴) ∈ ℝ)
181110adantr 481 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) ∈ ℝ)
182 2rp 11837 . . . . . . . . . . . . . 14 2 ∈ ℝ+
183182a1i 11 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → 2 ∈ ℝ+)
184 simpr 477 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴))
185180, 181, 184nltled 10187 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑄‘1) − 𝐴) ≤ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)))
186180, 181, 183, 185lediv1dd 11930 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑄‘1) − 𝐴) / 2) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
187179, 186eqbrtrd 4675 . . . . . . . . . . 11 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
188177, 187pm2.61dan 832 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
189118, 111, 42, 188leadd2dd 10642 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) ≤ ((𝑆‘𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)))
19042recnd 10068 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ ℂ)
191109recnd 10068 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℂ)
192190, 191addcomd 10238 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) = ((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)))
193192oveq1d 6665 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) = (((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2))
194193oveq1d 6665 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = ((((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)))
195 halfaddsub 11265 . . . . . . . . . . . . . . 15 (((𝑆‘(𝑗 + 1)) ∈ ℂ ∧ (𝑆‘𝑗) ∈ ℂ) → (((((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘(𝑗 + 1)) ∧ ((((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘𝑗)))
196191, 190, 195syl2anc 693 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘(𝑗 + 1)) ∧ ((((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘𝑗)))
197196simprd 479 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘𝑗))
198194, 197eqtrd 2656 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘𝑗))
199190, 191addcld 10059 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) ∈ ℂ)
200199halfcld 11277 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) ∈ ℂ)
201111recnd 10068 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ∈ ℂ)
202200, 201, 190subsub23d 39499 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘𝑗) ↔ ((((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (𝑆‘𝑗)) = (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)))
203198, 202mpbid 222 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (𝑆‘𝑗)) = (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
204200, 190, 201subaddd 10410 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (𝑆‘𝑗)) = (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ↔ ((𝑆‘𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2)))
205203, 204mpbid 222 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2))
206 avglt2 11271 . . . . . . . . . . . 12 (((𝑆‘𝑗) ∈ ℝ ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ) → ((𝑆‘𝑗) < (𝑆‘(𝑗 + 1)) ↔ (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) < (𝑆‘(𝑗 + 1))))
20742, 109, 206syl2anc 693 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) < (𝑆‘(𝑗 + 1)) ↔ (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) < (𝑆‘(𝑗 + 1))))
208131, 207mpbid 222 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) < (𝑆‘(𝑗 + 1)))
209205, 208eqbrtrd 4675 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) < (𝑆‘(𝑗 + 1)))
210119, 172, 109, 189, 209lelttrd 10195 . . . . . . . 8 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑆‘(𝑗 + 1)))
211106, 210syl5eqbr 4688 . . . . . . 7 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 < (𝑆‘(𝑗 + 1)))
212109rexrd 10089 . . . . . . . 8 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℝ*)
213 elico2 12237 . . . . . . . 8 (((𝑆‘𝑗) ∈ ℝ ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ*) → (𝑍 ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ (𝑍 ∈ ℝ ∧ (𝑆‘𝑗) ≤ 𝑍 ∧ 𝑍 < (𝑆‘(𝑗 + 1)))))
21442, 212, 213syl2anc 693 . . . . . . 7 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑍 ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ (𝑍 ∈ ℝ ∧ (𝑆‘𝑗) ≤ 𝑍 ∧ 𝑍 < (𝑆‘(𝑗 + 1)))))
215120, 171, 211, 214mpbir3and 1245 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))))
216215adantr 481 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝑍 ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))))
217114ad2antrr 762 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐴 ∈ ℝ)
218113simp2d 1074 . . . . . . . . 9 (𝜑 → 𝐵 ∈ ℝ)
219218ad2antrr 762 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐵 ∈ ℝ)
220113simp3d 1075 . . . . . . . . 9 (𝜑 → 𝐴 < 𝐵)
221220ad2antrr 762 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐴 < 𝐵)
22242adantr 481 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑆‘𝑗) ∈ ℝ)
223 simpr 477 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) = 𝐵)
224169, 106syl6breqr 4695 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) < 𝑍)
225218, 114resubcld 10458 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
22611, 225syl5eqel 2705 . . . . . . . . . . . . 13 (𝜑 → 𝑇 ∈ ℝ)
227226adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑇 ∈ ℝ)
228111adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ∈ ℝ)
229116ad2antrr 762 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ)
230110adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) ∈ ℝ)
231115ad2antrr 762 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑄‘1) − 𝐴) ∈ ℝ)
232182a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → 2 ∈ ℝ+)
233 simpr 477 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴))
234230, 231, 232, 233ltdiv1dd 11929 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) < (((𝑄‘1) − 𝐴) / 2))
235228, 229, 234ltled 10185 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ≤ (((𝑄‘1) − 𝐴) / 2))
236174, 235eqbrtrd 4675 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2))
237178adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) − 𝐴) / 2))
238116leidd 10594 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ≤ (((𝑄‘1) − 𝐴) / 2))
239238adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑄‘1) − 𝐴) / 2) ≤ (((𝑄‘1) − 𝐴) / 2))
240237, 239eqbrtrd 4675 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2))
241240adantlr 751 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2))
242236, 241pm2.61dan 832 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2))
243225rehalfcld 11279 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵 − 𝐴) / 2) ∈ ℝ)
244182a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 2 ∈ ℝ+)
245114rexrd 10089 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 𝐴 ∈ ℝ*)
246218rexrd 10089 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 𝐵 ∈ ℝ*)
2473, 2, 1fourierdlem15 40339 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
248247, 103ffvelrnd 6360 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑄‘1) ∈ (𝐴[,]𝐵))
249 iccleub 12229 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝑄‘1) ∈ (𝐴[,]𝐵)) → (𝑄‘1) ≤ 𝐵)
250245, 246, 248, 249syl3anc 1326 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑄‘1) ≤ 𝐵)
251112, 218, 114, 250lesub1dd 10643 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑄‘1) − 𝐴) ≤ (𝐵 − 𝐴))
252115, 225, 244, 251lediv1dd 11930 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ≤ ((𝐵 − 𝐴) / 2))
25311eqcomi 2631 . . . . . . . . . . . . . . . . . 18 (𝐵 − 𝐴) = 𝑇
254253oveq1i 6660 . . . . . . . . . . . . . . . . 17 ((𝐵 − 𝐴) / 2) = (𝑇 / 2)
255114, 218posdifd 10614 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
256220, 255mpbid 222 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 < (𝐵 − 𝐴))
257256, 11syl6breqr 4695 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 < 𝑇)
258226, 257elrpd 11869 . . . . . . . . . . . . . . . . . 18 (𝜑 → 𝑇 ∈ ℝ+)
259 rphalflt 11860 . . . . . . . . . . . . . . . . . 18 (𝑇 ∈ ℝ+ → (𝑇 / 2) < 𝑇)
260258, 259syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑇 / 2) < 𝑇)
261254, 260syl5eqbr 4688 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵 − 𝐴) / 2) < 𝑇)
262116, 243, 226, 252, 261lelttrd 10195 . . . . . . . . . . . . . . 15 (𝜑 → (((𝑄‘1) − 𝐴) / 2) < 𝑇)
263116, 226, 262ltled 10185 . . . . . . . . . . . . . 14 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ≤ 𝑇)
264263adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑄‘1) − 𝐴) / 2) ≤ 𝑇)
265118, 117, 227, 242, 264letrd 10194 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ 𝑇)
266118, 227, 42, 265leadd2dd 10642 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) ≤ ((𝑆‘𝑗) + 𝑇))
267106, 266syl5eqbr 4688 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 ≤ ((𝑆‘𝑗) + 𝑇))
26842rexrd 10089 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ ℝ*)
26942, 227readdcld 10069 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + 𝑇) ∈ ℝ)
270 elioc2 12236 . . . . . . . . . . 11 (((𝑆‘𝑗) ∈ ℝ* ∧ ((𝑆‘𝑗) + 𝑇) ∈ ℝ) → (𝑍 ∈ ((𝑆‘𝑗)(,]((𝑆‘𝑗) + 𝑇)) ↔ (𝑍 ∈ ℝ ∧ (𝑆‘𝑗) < 𝑍 ∧ 𝑍 ≤ ((𝑆‘𝑗) + 𝑇))))
271268, 269, 270syl2anc 693 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑍 ∈ ((𝑆‘𝑗)(,]((𝑆‘𝑗) + 𝑇)) ↔ (𝑍 ∈ ℝ ∧ (𝑆‘𝑗) < 𝑍 ∧ 𝑍 ≤ ((𝑆‘𝑗) + 𝑇))))
272120, 224, 267, 271mpbir3and 1245 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 ∈ ((𝑆‘𝑗)(,]((𝑆‘𝑗) + 𝑇)))
273272adantr 481 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝑍 ∈ ((𝑆‘𝑗)(,]((𝑆‘𝑗) + 𝑇)))
274217, 219, 221, 11, 12, 222, 223, 273fourierdlem26 40350 . . . . . . 7 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘𝑍) = (𝐴 + (𝑍 − (𝑆‘𝑗))))
275106a1i 11 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 = ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
276275oveq1d 6665 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑍 − (𝑆‘𝑗)) = (((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆‘𝑗)))
277276oveq2d 6666 . . . . . . . 8 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 + (𝑍 − (𝑆‘𝑗))) = (𝐴 + (((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆‘𝑗))))
278277adantr 481 . . . . . . 7 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐴 + (𝑍 − (𝑆‘𝑗))) = (𝐴 + (((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆‘𝑗))))
279118recnd 10068 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ∈ ℂ)
280190, 279pncan2d 10394 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆‘𝑗)) = if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)))
281280oveq2d 6666 . . . . . . . 8 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 + (((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆‘𝑗))) = (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
282281adantr 481 . . . . . . 7 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐴 + (((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆‘𝑗))) = (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
283274, 278, 2823eqtrd 2660 . . . . . 6 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘𝑍) = (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
284173oveq2d 6666 . . . . . . . . . 10 (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)))
285284adantl 482 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)))
286114adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ℝ)
287286, 111readdcld 10069 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) ∈ ℝ)
288287adantr 481 . . . . . . . . . 10 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) ∈ ℝ)
289286, 117readdcld 10069 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) ∈ ℝ)
290289adantr 481 . . . . . . . . . 10 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) ∈ ℝ)
291112ad2antrr 762 . . . . . . . . . 10 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝑄‘1) ∈ ℝ)
292114ad2antrr 762 . . . . . . . . . . 11 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → 𝐴 ∈ ℝ)
293228, 229, 292, 234ltadd2dd 10196 . . . . . . . . . 10 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) < (𝐴 + (((𝑄‘1) − 𝐴) / 2)))
294112recnd 10068 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘1) ∈ ℂ)
295114recnd 10068 . . . . . . . . . . . . . . . 16 (𝜑 → 𝐴 ∈ ℂ)
296 halfaddsub 11265 . . . . . . . . . . . . . . . 16 (((𝑄‘1) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((((𝑄‘1) + 𝐴) / 2) + (((𝑄‘1) − 𝐴) / 2)) = (𝑄‘1) ∧ ((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) = 𝐴))
297294, 295, 296syl2anc 693 . . . . . . . . . . . . . . 15 (𝜑 → (((((𝑄‘1) + 𝐴) / 2) + (((𝑄‘1) − 𝐴) / 2)) = (𝑄‘1) ∧ ((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) = 𝐴))
298297simprd 479 . . . . . . . . . . . . . 14 (𝜑 → ((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) = 𝐴)
299298oveq1d 6665 . . . . . . . . . . . . 13 (𝜑 → (((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) + (((𝑄‘1) − 𝐴) / 2)) = (𝐴 + (((𝑄‘1) − 𝐴) / 2)))
300112, 114readdcld 10069 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑄‘1) + 𝐴) ∈ ℝ)
301300rehalfcld 11279 . . . . . . . . . . . . . . 15 (𝜑 → (((𝑄‘1) + 𝐴) / 2) ∈ ℝ)
302301recnd 10068 . . . . . . . . . . . . . 14 (𝜑 → (((𝑄‘1) + 𝐴) / 2) ∈ ℂ)
303116recnd 10068 . . . . . . . . . . . . . 14 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ∈ ℂ)
304302, 303npcand 10396 . . . . . . . . . . . . 13 (𝜑 → (((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) + (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) + 𝐴) / 2))
305299, 304eqtr3d 2658 . . . . . . . . . . . 12 (𝜑 → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) + 𝐴) / 2))
306112, 112readdcld 10069 . . . . . . . . . . . . . 14 (𝜑 → ((𝑄‘1) + (𝑄‘1)) ∈ ℝ)
307114, 112, 112, 161ltadd2dd 10196 . . . . . . . . . . . . . 14 (𝜑 → ((𝑄‘1) + 𝐴) < ((𝑄‘1) + (𝑄‘1)))
308300, 306, 244, 307ltdiv1dd 11929 . . . . . . . . . . . . 13 (𝜑 → (((𝑄‘1) + 𝐴) / 2) < (((𝑄‘1) + (𝑄‘1)) / 2))
3092942timesd 11275 . . . . . . . . . . . . . . . 16 (𝜑 → (2 · (𝑄‘1)) = ((𝑄‘1) + (𝑄‘1)))
310309eqcomd 2628 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑄‘1) + (𝑄‘1)) = (2 · (𝑄‘1)))
311310oveq1d 6665 . . . . . . . . . . . . . 14 (𝜑 → (((𝑄‘1) + (𝑄‘1)) / 2) = ((2 · (𝑄‘1)) / 2))
312 2cnd 11093 . . . . . . . . . . . . . . 15 (𝜑 → 2 ∈ ℂ)
313 2ne0 11113 . . . . . . . . . . . . . . . 16 2 ≠ 0
314313a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 2 ≠ 0)
315294, 312, 314divcan3d 10806 . . . . . . . . . . . . . 14 (𝜑 → ((2 · (𝑄‘1)) / 2) = (𝑄‘1))
316311, 315eqtrd 2656 . . . . . . . . . . . . 13 (𝜑 → (((𝑄‘1) + (𝑄‘1)) / 2) = (𝑄‘1))
317308, 316breqtrd 4679 . . . . . . . . . . . 12 (𝜑 → (((𝑄‘1) + 𝐴) / 2) < (𝑄‘1))
318305, 317eqbrtrd 4675 . . . . . . . . . . 11 (𝜑 → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) < (𝑄‘1))
319318ad2antrr 762 . . . . . . . . . 10 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) < (𝑄‘1))
320288, 290, 291, 293, 319lttrd 10198 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) < (𝑄‘1))
321285, 320eqbrtrd 4675 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1))
322178oveq2d 6666 . . . . . . . . . 10 (¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑄‘1) − 𝐴) / 2)))
323322adantl 482 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑄‘1) − 𝐴) / 2)))
324318ad2antrr 762 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) < (𝑄‘1))
325323, 324eqbrtrd 4675 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1))
326321, 325pm2.61dan 832 . . . . . . 7 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1))
327326adantr 481 . . . . . 6 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1))
328283, 327eqbrtrd 4675 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘𝑍) < (𝑄‘1))
329 eqid 2622 . . . . 5 ((𝑄‘1) − ((𝐸‘𝑍) − 𝑍)) = ((𝑄‘1) − ((𝐸‘𝑍) − 𝑍))
33011, 3, 90, 91, 92, 93, 94, 24, 25, 26, 27, 12, 104, 105, 216, 328, 329fourierdlem63 40386 . . . 4 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘1))
33114a1i 11 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < )))
33257adantl 482 . . . . . . . . 9 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ 𝑥 = (𝑆‘𝑗)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ))
33360a1i 11 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ V)
334331, 332, 222, 333fvmptd 6288 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐼‘(𝑆‘𝑗)) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ))
335 fveq2 6191 . . . . . . . . . . . . 13 ((𝐸‘(𝑆‘𝑗)) = 𝐵 → (𝐿‘(𝐸‘(𝑆‘𝑗))) = (𝐿‘𝐵))
33613a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)))
337 iftrue 4092 . . . . . . . . . . . . . . 15 (𝑦 = 𝐵 → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝐴)
338337adantl 482 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑦 = 𝐵) → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝐴)
339 ubioc1 12227 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → 𝐵 ∈ (𝐴(,]𝐵))
340245, 246, 220, 339syl3anc 1326 . . . . . . . . . . . . . 14 (𝜑 → 𝐵 ∈ (𝐴(,]𝐵))
341336, 338, 340, 114fvmptd 6288 . . . . . . . . . . . . 13 (𝜑 → (𝐿‘𝐵) = 𝐴)
342335, 341sylan9eqr 2678 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐿‘(𝐸‘(𝑆‘𝑗))) = 𝐴)
343342breq2d 4665 . . . . . . . . . . 11 ((𝜑 ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))) ↔ (𝑄‘𝑖) ≤ 𝐴))
344343rabbidv 3189 . . . . . . . . . 10 ((𝜑 ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} = {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴})
345344supeq1d 8352 . . . . . . . . 9 ((𝜑 ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}, ℝ, < ))
346345adantlr 751 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}, ℝ, < ))
347 simpl 473 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}) → 𝜑)
348 elrabi 3359 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} → 𝑗 ∈ (0..^𝑀))
349348adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}) → 𝑗 ∈ (0..^𝑀))
350 fveq2 6191 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑗 → (𝑄‘𝑖) = (𝑄‘𝑗))
351350breq1d 4663 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → ((𝑄‘𝑖) ≤ 𝐴 ↔ (𝑄‘𝑗) ≤ 𝐴))
352351elrab 3363 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} ↔ (𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴))
353352simprbi 480 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} → (𝑄‘𝑗) ≤ 𝐴)
354353adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}) → (𝑄‘𝑗) ≤ 𝐴)
355 simp3 1063 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → (𝑄‘𝑗) ≤ 𝐴)
356114ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝐴 ∈ ℝ)
357112ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝑄‘1) ∈ ℝ)
3589adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
35918sselda 3603 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑗 ∈ (0...𝑀))
360358, 359ffvelrnd 6360 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) ∈ ℝ)
361360adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝑄‘𝑗) ∈ ℝ)
362161ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝐴 < (𝑄‘1))
363 1zzd 11408 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 1 ∈ ℤ)
364 elfzoelz 12470 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℤ)
365364ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝑗 ∈ ℤ)
366 1e0p1 11552 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 = (0 + 1)
367 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → ¬ 𝑗 ≤ 0)
368 0red 10041 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 0 ∈ ℝ)
369365zred 11482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝑗 ∈ ℝ)
370368, 369ltnled 10184 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (0 < 𝑗 ↔ ¬ 𝑗 ≤ 0))
371367, 370mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 0 < 𝑗)
372 0zd 11389 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 0 ∈ ℤ)
373 zltp1le 11427 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((0 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (0 < 𝑗 ↔ (0 + 1) ≤ 𝑗))
374372, 365, 373syl2anc 693 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (0 < 𝑗 ↔ (0 + 1) ≤ 𝑗))
375371, 374mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (0 + 1) ≤ 𝑗)
376366, 375syl5eqbr 4688 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 1 ≤ 𝑗)
377 eluz2 11693 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (ℤ≥‘1) ↔ (1 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 1 ≤ 𝑗))
378363, 365, 376, 377syl3anbrc 1246 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝑗 ∈ (ℤ≥‘1))
3799ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑄:(0...𝑀)⟶ℝ)
380 0red 10041 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (1...𝑗) → 0 ∈ ℝ)
381 elfzelz 12342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 𝑙 ∈ ℤ)
382381zred 11482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (1...𝑗) → 𝑙 ∈ ℝ)
383 1red 10055 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 1 ∈ ℝ)
384 0lt1 10550 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 0 < 1
385384a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 0 < 1)
386 elfzle1 12344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 1 ≤ 𝑙)
387380, 383, 382, 385, 386ltletrd 10197 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (1...𝑗) → 0 < 𝑙)
388380, 382, 387ltled 10185 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑙 ∈ (1...𝑗) → 0 ≤ 𝑙)
389388adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 0 ≤ 𝑙)
390382adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ∈ ℝ)
391100zred 11482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → 𝑀 ∈ ℝ)
392391ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑀 ∈ ℝ)
393364zred 11482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℝ)
394393ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑗 ∈ ℝ)
395 elfzle2 12345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 𝑙 ≤ 𝑗)
396395adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ≤ 𝑗)
397 elfzolt2 12479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0..^𝑀) → 𝑗 < 𝑀)
398397ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑗 < 𝑀)
399390, 394, 392, 396, 398lelttrd 10195 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 < 𝑀)
400390, 392, 399ltled 10185 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ≤ 𝑀)
401381adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ∈ ℤ)
402 0zd 11389 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 0 ∈ ℤ)
403100ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑀 ∈ ℤ)
404 elfz 12332 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑙 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑙 ∈ (0...𝑀) ↔ (0 ≤ 𝑙 ∧ 𝑙 ≤ 𝑀)))
405401, 402, 403, 404syl3anc 1326 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → (𝑙 ∈ (0...𝑀) ↔ (0 ≤ 𝑙 ∧ 𝑙 ≤ 𝑀)))
406389, 400, 405mpbir2and 957 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ∈ (0...𝑀))
407379, 406ffvelrnd 6360 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → (𝑄‘𝑙) ∈ ℝ)
408407adantlr 751 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) ∧ 𝑙 ∈ (1...𝑗)) → (𝑄‘𝑙) ∈ ℝ)
4099ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑄:(0...𝑀)⟶ℝ)
410 0zd 11389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ∈ ℤ)
411100ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℤ)
412 elfzelz 12342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 𝑙 ∈ ℤ)
413412adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℤ)
414410, 411, 4133jca 1242 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑙 ∈ ℤ))
415 0red 10041 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 0 ∈ ℝ)
416412zred 11482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 𝑙 ∈ ℝ)
417 1red 10055 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑙 ∈ (1...(𝑗 − 1)) → 1 ∈ ℝ)
418384a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑙 ∈ (1...(𝑗 − 1)) → 0 < 1)
419 elfzle1 12344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑙 ∈ (1...(𝑗 − 1)) → 1 ≤ 𝑙)
420415, 417, 416, 418, 419ltletrd 10197 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 0 < 𝑙)
421415, 416, 420ltled 10185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...(𝑗 − 1)) → 0 ≤ 𝑙)
422421adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ≤ 𝑙)
423413zred 11482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℝ)
424391ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℝ)
425393ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 ∈ ℝ)
426416adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℝ)
427 peano2rem 10348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 ∈ ℝ → (𝑗 − 1) ∈ ℝ)
428393, 427syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑗 ∈ (0..^𝑀) → (𝑗 − 1) ∈ ℝ)
429428adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑗 − 1) ∈ ℝ)
430393adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 ∈ ℝ)
431 elfzle2 12345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑙 ∈ (1...(𝑗 − 1)) → 𝑙 ≤ (𝑗 − 1))
432431adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ≤ (𝑗 − 1))
433430ltm1d 10956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑗 − 1) < 𝑗)
434426, 429, 430, 432, 433lelttrd 10195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑗)
435434adantll 750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑗)
436397ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 < 𝑀)
437423, 425, 424, 435, 436lttrd 10198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑀)
438423, 424, 437ltled 10185 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ≤ 𝑀)
439414, 422, 438jca32 558 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑙 ∈ ℤ) ∧ (0 ≤ 𝑙 ∧ 𝑙 ≤ 𝑀)))
440 elfz2 12333 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑙 ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑙 ∈ ℤ) ∧ (0 ≤ 𝑙 ∧ 𝑙 ≤ 𝑀)))
441439, 440sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ (0...𝑀))
442409, 441ffvelrnd 6360 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄‘𝑙) ∈ ℝ)
443413peano2zd 11485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ∈ ℤ)
444410, 411, 4433jca 1242 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑙 + 1) ∈ ℤ))
445416, 417readdcld 10069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) ∈ ℝ)
446416, 417, 420, 418addgt0d 10602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 0 < (𝑙 + 1))
447415, 445, 446ltled 10185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...(𝑗 − 1)) → 0 ≤ (𝑙 + 1))
448447adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ≤ (𝑙 + 1))
449445adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ∈ ℝ)
450445recnd 10068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) ∈ ℂ)
451 1cnd 10056 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑙 ∈ (1...(𝑗 − 1)) → 1 ∈ ℂ)
452450, 451npcand 10396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑙 ∈ (1...(𝑗 − 1)) → (((𝑙 + 1) − 1) + 1) = (𝑙 + 1))
453452eqcomd 2628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) = (((𝑙 + 1) − 1) + 1))
454453adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) = (((𝑙 + 1) − 1) + 1))
455 peano2re 10209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑙 ∈ ℝ → (𝑙 + 1) ∈ ℝ)
456 peano2rem 10348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑙 + 1) ∈ ℝ → ((𝑙 + 1) − 1) ∈ ℝ)
457426, 455, 4563syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((𝑙 + 1) − 1) ∈ ℝ)
458 peano2re 10209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑗 − 1) ∈ ℝ → ((𝑗 − 1) + 1) ∈ ℝ)
459 peano2rem 10348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑗 − 1) + 1) ∈ ℝ → (((𝑗 − 1) + 1) − 1) ∈ ℝ)
460429, 458, 4593syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (((𝑗 − 1) + 1) − 1) ∈ ℝ)
461 1red 10055 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 1 ∈ ℝ)
462 elfzel2 12340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑗 − 1) ∈ ℤ)
463462zred 11482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑗 − 1) ∈ ℝ)
464463, 417readdcld 10069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑙 ∈ (1...(𝑗 − 1)) → ((𝑗 − 1) + 1) ∈ ℝ)
465416, 463, 417, 431leadd1dd 10641 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) ≤ ((𝑗 − 1) + 1))
466445, 464, 417, 465lesub1dd 10643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑙 ∈ (1...(𝑗 − 1)) → ((𝑙 + 1) − 1) ≤ (((𝑗 − 1) + 1) − 1))
467466adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((𝑙 + 1) − 1) ≤ (((𝑗 − 1) + 1) − 1))
468457, 460, 461, 467leadd1dd 10641 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (((𝑙 + 1) − 1) + 1) ≤ ((((𝑗 − 1) + 1) − 1) + 1))
469 peano2zm 11420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑗 ∈ ℤ → (𝑗 − 1) ∈ ℤ)
470364, 469syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑗 ∈ (0..^𝑀) → (𝑗 − 1) ∈ ℤ)
471470peano2zd 11485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑗 ∈ (0..^𝑀) → ((𝑗 − 1) + 1) ∈ ℤ)
472471zcnd 11483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ (0..^𝑀) → ((𝑗 − 1) + 1) ∈ ℂ)
473 1cnd 10056 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ (0..^𝑀) → 1 ∈ ℂ)
474472, 473npcand 10396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 ∈ (0..^𝑀) → ((((𝑗 − 1) + 1) − 1) + 1) = ((𝑗 − 1) + 1))
475393recnd 10068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℂ)
476475, 473npcand 10396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 ∈ (0..^𝑀) → ((𝑗 − 1) + 1) = 𝑗)
477474, 476eqtrd 2656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 ∈ (0..^𝑀) → ((((𝑗 − 1) + 1) − 1) + 1) = 𝑗)
478477adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((((𝑗 − 1) + 1) − 1) + 1) = 𝑗)
479468, 478breqtrd 4679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (((𝑙 + 1) − 1) + 1) ≤ 𝑗)
480454, 479eqbrtrd 4675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ≤ 𝑗)
481480adantll 750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ≤ 𝑗)
482449, 425, 424, 481, 436lelttrd 10195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) < 𝑀)
483449, 424, 482ltled 10185 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ≤ 𝑀)
484444, 448, 483jca32 558 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑙 + 1) ∈ ℤ) ∧ (0 ≤ (𝑙 + 1) ∧ (𝑙 + 1) ≤ 𝑀)))
485 elfz2 12333 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑙 + 1) ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑙 + 1) ∈ ℤ) ∧ (0 ≤ (𝑙 + 1) ∧ (𝑙 + 1) ≤ 𝑀)))
486484, 485sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ∈ (0...𝑀))
487409, 486ffvelrnd 6360 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄‘(𝑙 + 1)) ∈ ℝ)
488 simpll 790 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝜑)
489 0zd 11389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ∈ ℤ)
490412adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℤ)
491421adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ≤ 𝑙)
492 eluz2 11693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (ℤ≥‘0) ↔ (0 ∈ ℤ ∧ 𝑙 ∈ ℤ ∧ 0 ≤ 𝑙))
493489, 490, 491, 492syl3anbrc 1246 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ (ℤ≥‘0))
494 elfzoel2 12469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0..^𝑀) → 𝑀 ∈ ℤ)
495494adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℤ)
496495zred 11482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℝ)
497397adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 < 𝑀)
498426, 430, 496, 434, 497lttrd 10198 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑀)
499 elfzo2 12473 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (0..^𝑀) ↔ (𝑙 ∈ (ℤ≥‘0) ∧ 𝑀 ∈ ℤ ∧ 𝑙 < 𝑀))
500493, 495, 498, 499syl3anbrc 1246 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ (0..^𝑀))
501500adantll 750 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ (0..^𝑀))
502 eleq1 2689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 = 𝑙 → (𝑖 ∈ (0..^𝑀) ↔ 𝑙 ∈ (0..^𝑀)))
503502anbi2d 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 = 𝑙 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 𝑙 ∈ (0..^𝑀))))
504 fveq2 6191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 = 𝑙 → (𝑄‘𝑖) = (𝑄‘𝑙))
505 oveq1 6657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 = 𝑙 → (𝑖 + 1) = (𝑙 + 1))
506505fveq2d 6195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 = 𝑙 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑙 + 1)))
507504, 506breq12d 4666 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 = 𝑙 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘𝑙) < (𝑄‘(𝑙 + 1))))
508503, 507imbi12d 334 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 = 𝑙 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑙 ∈ (0..^𝑀)) → (𝑄‘𝑙) < (𝑄‘(𝑙 + 1)))))
509508, 152chvarv 2263 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ 𝑙 ∈ (0..^𝑀)) → (𝑄‘𝑙) < (𝑄‘(𝑙 + 1)))
510488, 501, 509syl2anc 693 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄‘𝑙) < (𝑄‘(𝑙 + 1)))
511442, 487, 510ltled 10185 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄‘𝑙) ≤ (𝑄‘(𝑙 + 1)))
512511adantlr 751 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄‘𝑙) ≤ (𝑄‘(𝑙 + 1)))
513378, 408, 512monoord 12831 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝑄‘1) ≤ (𝑄‘𝑗))
514356, 357, 361, 362, 513ltletrd 10197 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝐴 < (𝑄‘𝑗))
515356, 361ltnled 10184 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝐴 < (𝑄‘𝑗) ↔ ¬ (𝑄‘𝑗) ≤ 𝐴))
516514, 515mpbid 222 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → ¬ (𝑄‘𝑗) ≤ 𝐴)
517516ex 450 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (¬ 𝑗 ≤ 0 → ¬ (𝑄‘𝑗) ≤ 𝐴))
5185173adant3 1081 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → (¬ 𝑗 ≤ 0 → ¬ (𝑄‘𝑗) ≤ 𝐴))
519355, 518mt4d 152 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → 𝑗 ≤ 0)
520 elfzole1 12478 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0..^𝑀) → 0 ≤ 𝑗)
5215203ad2ant2 1083 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → 0 ≤ 𝑗)
5223933ad2ant2 1083 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → 𝑗 ∈ ℝ)
523 0red 10041 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → 0 ∈ ℝ)
524522, 523letri3d 10179 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → (𝑗 = 0 ↔ (𝑗 ≤ 0 ∧ 0 ≤ 𝑗)))
525519, 521, 524mpbir2and 957 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → 𝑗 = 0)
526347, 349, 354, 525syl3anc 1326 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}) → 𝑗 = 0)
527 velsn 4193 . . . . . . . . . . . . . . 15 (𝑗 ∈ {0} ↔ 𝑗 = 0)
528526, 527sylibr 224 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}) → 𝑗 ∈ {0})
529528ralrimiva 2966 . . . . . . . . . . . . 13 (𝜑 → ∀𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}𝑗 ∈ {0})
530 dfss3 3592 . . . . . . . . . . . . 13 ({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} ⊆ {0} ↔ ∀𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}𝑗 ∈ {0})
531529, 530sylibr 224 . . . . . . . . . . . 12 (𝜑 → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} ⊆ {0})
532157, 114eqeltrd 2701 . . . . . . . . . . . . . . 15 (𝜑 → (𝑄‘0) ∈ ℝ)
533532, 157eqled 10140 . . . . . . . . . . . . . 14 (𝜑 → (𝑄‘0) ≤ 𝐴)
534145breq1d 4663 . . . . . . . . . . . . . . 15 (𝑖 = 0 → ((𝑄‘𝑖) ≤ 𝐴 ↔ (𝑄‘0) ≤ 𝐴))
535534elrab 3363 . . . . . . . . . . . . . 14 (0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} ↔ (0 ∈ (0..^𝑀) ∧ (𝑄‘0) ≤ 𝐴))
536141, 533, 535sylanbrc 698 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴})
537536snssd 4340 . . . . . . . . . . . 12 (𝜑 → {0} ⊆ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴})
538531, 537eqssd 3620 . . . . . . . . . . 11 (𝜑 → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} = {0})
539538supeq1d 8352 . . . . . . . . . 10 (𝜑 → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}, ℝ, < ) = sup({0}, ℝ, < ))
540 supsn 8378 . . . . . . . . . . . 12 (( < Or ℝ ∧ 0 ∈ ℝ) → sup({0}, ℝ, < ) = 0)
54159, 142, 540mp2an 708 . . . . . . . . . . 11 sup({0}, ℝ, < ) = 0
542541a1i 11 . . . . . . . . . 10 (𝜑 → sup({0}, ℝ, < ) = 0)
543539, 542eqtrd 2656 . . . . . . . . 9 (𝜑 → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}, ℝ, < ) = 0)
544543ad2antrr 762 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}, ℝ, < ) = 0)
545334, 346, 5443eqtrd 2660 . . . . . . 7 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐼‘(𝑆‘𝑗)) = 0)
546545oveq1d 6665 . . . . . 6 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝐼‘(𝑆‘𝑗)) + 1) = (0 + 1))
547546fveq2d 6195 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) = (𝑄‘(0 + 1)))
548547, 159syl6req 2673 . . . 4 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑄‘1) = (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
549330, 548breqtrd 4679 . . 3 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
55065adantr 481 . . . 4 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝜑 ∧ (𝑆‘𝑗) ∈ ℝ))
551 simplr 792 . . . 4 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝑗 ∈ (0..^𝑁))
55213a1i 11 . . . . . . . . . . 11 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)))
553 simpr 477 . . . . . . . . . . . . . . . 16 ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → 𝑦 = (𝐸‘(𝑆‘𝑗)))
554 neqne 2802 . . . . . . . . . . . . . . . . 17 (¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 → (𝐸‘(𝑆‘𝑗)) ≠ 𝐵)
555554adantr 481 . . . . . . . . . . . . . . . 16 ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → (𝐸‘(𝑆‘𝑗)) ≠ 𝐵)
556553, 555eqnetrd 2861 . . . . . . . . . . . . . . 15 ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → 𝑦 ≠ 𝐵)
557556neneqd 2799 . . . . . . . . . . . . . 14 ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → ¬ 𝑦 = 𝐵)
558557iffalsed 4097 . . . . . . . . . . . . 13 ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝑦)
559558, 553eqtrd 2656 . . . . . . . . . . . 12 ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = (𝐸‘(𝑆‘𝑗)))
560559adantll 750 . . . . . . . . . . 11 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = (𝐸‘(𝑆‘𝑗)))
561114, 218, 220, 11, 12fourierdlem4 40328 . . . . . . . . . . . . . 14 (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))
562561adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐸:ℝ⟶(𝐴(,]𝐵))
563562, 42ffvelrnd 6360 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘𝑗)) ∈ (𝐴(,]𝐵))
564563adantr 481 . . . . . . . . . . 11 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) ∈ (𝐴(,]𝐵))
565552, 560, 564, 564fvmptd 6288 . . . . . . . . . 10 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐿‘(𝐸‘(𝑆‘𝑗))) = (𝐸‘(𝑆‘𝑗)))
566565eqcomd 2628 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) = (𝐿‘(𝐸‘(𝑆‘𝑗))))
567114, 218, 220, 13fourierdlem17 40341 . . . . . . . . . . . . 13 (𝜑 → 𝐿:(𝐴(,]𝐵)⟶(𝐴[,]𝐵))
568567adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐿:(𝐴(,]𝐵)⟶(𝐴[,]𝐵))
569114, 218iccssred 39727 . . . . . . . . . . . . 13 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
570569adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴[,]𝐵) ⊆ ℝ)
571568, 570fssd 6057 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐿:(𝐴(,]𝐵)⟶ℝ)
572571, 563ffvelrnd 6360 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐿‘(𝐸‘(𝑆‘𝑗))) ∈ ℝ)
573572adantr 481 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐿‘(𝐸‘(𝑆‘𝑗))) ∈ ℝ)
574566, 573eqeltrd 2701 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) ∈ ℝ)
575218ad2antrr 762 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐵 ∈ ℝ)
576245adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ℝ*)
577218adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐵 ∈ ℝ)
578 elioc2 12236 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐸‘(𝑆‘𝑗)) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘(𝑆‘𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆‘𝑗)) ∧ (𝐸‘(𝑆‘𝑗)) ≤ 𝐵)))
579576, 577, 578syl2anc 693 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘𝑗)) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘(𝑆‘𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆‘𝑗)) ∧ (𝐸‘(𝑆‘𝑗)) ≤ 𝐵)))
580563, 579mpbid 222 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆‘𝑗)) ∧ (𝐸‘(𝑆‘𝑗)) ≤ 𝐵))
581580simp3d 1075 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘𝑗)) ≤ 𝐵)
582581adantr 481 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) ≤ 𝐵)
583554necomd 2849 . . . . . . . . 9 (¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 → 𝐵 ≠ (𝐸‘(𝑆‘𝑗)))
584583adantl 482 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐵 ≠ (𝐸‘(𝑆‘𝑗)))
585574, 575, 582, 584leneltd 10191 . . . . . . 7 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) < 𝐵)
586585adantr 481 . . . . . 6 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆‘𝑗)) < 𝐵)
587 oveq1 6657 . . . . . . . . . . 11 ((𝐼‘(𝑆‘𝑗)) = (𝑀 − 1) → ((𝐼‘(𝑆‘𝑗)) + 1) = ((𝑀 − 1) + 1))
5882nncnd 11036 . . . . . . . . . . . 12 (𝜑 → 𝑀 ∈ ℂ)
589 1cnd 10056 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℂ)
590588, 589npcand 10396 . . . . . . . . . . 11 (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
591587, 590sylan9eqr 2678 . . . . . . . . . 10 ((𝜑 ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆‘𝑗)) + 1) = 𝑀)
592591fveq2d 6195 . . . . . . . . 9 ((𝜑 ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) = (𝑄‘𝑀))
593156simprd 479 . . . . . . . . . 10 (𝜑 → (𝑄‘𝑀) = 𝐵)
594593adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝑄‘𝑀) = 𝐵)
595592, 594eqtr2d 2657 . . . . . . . 8 ((𝜑 ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 𝐵 = (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
596595adantlr 751 . . . . . . 7 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 𝐵 = (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
597596adantlr 751 . . . . . 6 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 𝐵 = (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
598586, 597breqtrd 4679 . . . . 5 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
599566adantr 481 . . . . . 6 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆‘𝑗)) = (𝐿‘(𝐸‘(𝑆‘𝑗))))
600 ssrab2 3687 . . . . . . . . . . . . 13 {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ (0..^𝑀)
601 fzssz 12343 . . . . . . . . . . . . . . 15 (0...𝑀) ⊆ ℤ
60217, 601sstri 3612 . . . . . . . . . . . . . 14 (0..^𝑀) ⊆ ℤ
603 zssre 11384 . . . . . . . . . . . . . 14 ℤ ⊆ ℝ
604602, 603sstri 3612 . . . . . . . . . . . . 13 (0..^𝑀) ⊆ ℝ
605600, 604sstri 3612 . . . . . . . . . . . 12 {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ ℝ
606605a1i 11 . . . . . . . . . . 11 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ ℝ)
60756neeq1d 2853 . . . . . . . . . . . . . . 15 (𝑥 = (𝑆‘𝑗) → ({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ≠ ∅ ↔ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ≠ ∅))
60867, 607imbi12d 334 . . . . . . . . . . . . . 14 (𝑥 = (𝑆‘𝑗) → (((𝜑 ∧ 𝑥 ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ≠ ∅) ↔ ((𝜑 ∧ (𝑆‘𝑗) ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ≠ ∅)))
609141adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ∈ (0..^𝑀))
610533ad2antrr 762 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝐸‘𝑥) = 𝐵) → (𝑄‘0) ≤ 𝐴)
611 iftrue 4092 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸‘𝑥) = 𝐵 → if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)) = 𝐴)
612611eqcomd 2628 . . . . . . . . . . . . . . . . . . . 20 ((𝐸‘𝑥) = 𝐵 → 𝐴 = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
613612adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝐸‘𝑥) = 𝐵) → 𝐴 = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
614610, 613breqtrd 4679 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝐸‘𝑥) = 𝐵) → (𝑄‘0) ≤ if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
615532adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) ∈ ℝ)
616114adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ)
617616rexrd 10089 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ*)
618218adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℝ)
619 iocssre 12253 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
620617, 618, 619syl2anc 693 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
621561ffvelrnda 6359 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐸‘𝑥) ∈ (𝐴(,]𝐵))
622620, 621sseldd 3604 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐸‘𝑥) ∈ ℝ)
623157adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) = 𝐴)
624 elioc2 12236 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐸‘𝑥) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘𝑥) ∈ ℝ ∧ 𝐴 < (𝐸‘𝑥) ∧ (𝐸‘𝑥) ≤ 𝐵)))
625617, 618, 624syl2anc 693 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐸‘𝑥) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘𝑥) ∈ ℝ ∧ 𝐴 < (𝐸‘𝑥) ∧ (𝐸‘𝑥) ≤ 𝐵)))
626621, 625mpbid 222 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐸‘𝑥) ∈ ℝ ∧ 𝐴 < (𝐸‘𝑥) ∧ (𝐸‘𝑥) ≤ 𝐵))
627626simp2d 1074 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 < (𝐸‘𝑥))
628623, 627eqbrtrd 4675 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) < (𝐸‘𝑥))
629615, 622, 628ltled 10185 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) ≤ (𝐸‘𝑥))
630629adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐸‘𝑥) = 𝐵) → (𝑄‘0) ≤ (𝐸‘𝑥))
631 iffalse 4095 . . . . . . . . . . . . . . . . . . . . 21 (¬ (𝐸‘𝑥) = 𝐵 → if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)) = (𝐸‘𝑥))
632631eqcomd 2628 . . . . . . . . . . . . . . . . . . . 20 (¬ (𝐸‘𝑥) = 𝐵 → (𝐸‘𝑥) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
633632adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐸‘𝑥) = 𝐵) → (𝐸‘𝑥) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
634630, 633breqtrd 4679 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐸‘𝑥) = 𝐵) → (𝑄‘0) ≤ if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
635614, 634pm2.61dan 832 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) ≤ if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
63613a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)))
637 eqeq1 2626 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐸‘𝑥) → (𝑦 = 𝐵 ↔ (𝐸‘𝑥) = 𝐵))
638 id 22 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐸‘𝑥) → 𝑦 = (𝐸‘𝑥))
639637, 638ifbieq2d 4111 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝐸‘𝑥) → if(𝑦 = 𝐵, 𝐴, 𝑦) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
640639adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 = (𝐸‘𝑥)) → if(𝑦 = 𝐵, 𝐴, 𝑦) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
641616, 622ifcld 4131 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)) ∈ ℝ)
642636, 640, 621, 641fvmptd 6288 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐿‘(𝐸‘𝑥)) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
643635, 642breqtrrd 4681 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) ≤ (𝐿‘(𝐸‘𝑥)))
644145breq1d 4663 . . . . . . . . . . . . . . . . 17 (𝑖 = 0 → ((𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥)) ↔ (𝑄‘0) ≤ (𝐿‘(𝐸‘𝑥))))
645644elrab 3363 . . . . . . . . . . . . . . . 16 (0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ↔ (0 ∈ (0..^𝑀) ∧ (𝑄‘0) ≤ (𝐿‘(𝐸‘𝑥))))
646609, 643, 645sylanbrc 698 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))})
647 ne0i 3921 . . . . . . . . . . . . . . 15 (0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ≠ ∅)
648646, 647syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑥 ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ≠ ∅)
649608, 648vtoclg 3266 . . . . . . . . . . . . 13 ((𝑆‘𝑗) ∈ ℝ → ((𝜑 ∧ (𝑆‘𝑗) ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ≠ ∅))
65042, 65, 649sylc 65 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ≠ ∅)
651650ad2antrr 762 . . . . . . . . . . 11 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ≠ ∅)
652605a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ ℝ)
653 fzofi 12773 . . . . . . . . . . . . . . 15 (0..^𝑀) ∈ Fin
654 ssfi 8180 . . . . . . . . . . . . . . 15 (((0..^𝑀) ∈ Fin ∧ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ (0..^𝑀)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ∈ Fin)
655653, 600, 654mp2an 708 . . . . . . . . . . . . . 14 {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ∈ Fin
656655a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ∈ Fin)
657 fimaxre2 10969 . . . . . . . . . . . . 13 (({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ ℝ ∧ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}𝑙 ≤ 𝑥)
658652, 656, 657syl2anc 693 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}𝑙 ≤ 𝑥)
659658ad2antrr 762 . . . . . . . . . . 11 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}𝑙 ≤ 𝑥)
660 0red 10041 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 ∈ ℝ)
661604, 47sseldi 3601 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) ∈ ℝ)
662 1red 10055 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 1 ∈ ℝ)
663661, 662readdcld 10069 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ ℝ)
664 elfzouz 12474 . . . . . . . . . . . . . . . . . 18 ((𝐼‘(𝑆‘𝑗)) ∈ (0..^𝑀) → (𝐼‘(𝑆‘𝑗)) ∈ (ℤ≥‘0))
665 eluzle 11700 . . . . . . . . . . . . . . . . . 18 ((𝐼‘(𝑆‘𝑗)) ∈ (ℤ≥‘0) → 0 ≤ (𝐼‘(𝑆‘𝑗)))
66647, 664, 6653syl 18 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 ≤ (𝐼‘(𝑆‘𝑗)))
667384a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 < 1)
668661, 662, 666, 667addgegt0d 10601 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 < ((𝐼‘(𝑆‘𝑗)) + 1))
669660, 663, 668ltled 10185 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 ≤ ((𝐼‘(𝑆‘𝑗)) + 1))
670669adantr 481 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 0 ≤ ((𝐼‘(𝑆‘𝑗)) + 1))
671661adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐼‘(𝑆‘𝑗)) ∈ ℝ)
672 1red 10055 . . . . . . . . . . . . . . . . . 18 (𝜑 → 1 ∈ ℝ)
673391, 672resubcld 10458 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 − 1) ∈ ℝ)
674673ad2antrr 762 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝑀 − 1) ∈ ℝ)
675 1red 10055 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 1 ∈ ℝ)
676 elfzolt2 12479 . . . . . . . . . . . . . . . . . . . 20 ((𝐼‘(𝑆‘𝑗)) ∈ (0..^𝑀) → (𝐼‘(𝑆‘𝑗)) < 𝑀)
67747, 676syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) < 𝑀)
678601, 43sseldi 3601 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) ∈ ℤ)
679100adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑀 ∈ ℤ)
680 zltlem1 11430 . . . . . . . . . . . . . . . . . . . 20 (((𝐼‘(𝑆‘𝑗)) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝐼‘(𝑆‘𝑗)) < 𝑀 ↔ (𝐼‘(𝑆‘𝑗)) ≤ (𝑀 − 1)))
681678, 679, 680syl2anc 693 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆‘𝑗)) < 𝑀 ↔ (𝐼‘(𝑆‘𝑗)) ≤ (𝑀 − 1)))
682677, 681mpbid 222 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) ≤ (𝑀 − 1))
683682adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐼‘(𝑆‘𝑗)) ≤ (𝑀 − 1))
684 neqne 2802 . . . . . . . . . . . . . . . . . . 19 (¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1) → (𝐼‘(𝑆‘𝑗)) ≠ (𝑀 − 1))
685684necomd 2849 . . . . . . . . . . . . . . . . . 18 (¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1) → (𝑀 − 1) ≠ (𝐼‘(𝑆‘𝑗)))
686685adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝑀 − 1) ≠ (𝐼‘(𝑆‘𝑗)))
687671, 674, 683, 686leneltd 10191 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐼‘(𝑆‘𝑗)) < (𝑀 − 1))
688671, 674, 675, 687ltadd1dd 10638 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆‘𝑗)) + 1) < ((𝑀 − 1) + 1))
689590ad2antrr 762 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝑀 − 1) + 1) = 𝑀)
690688, 689breqtrd 4679 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆‘𝑗)) + 1) < 𝑀)
691601, 49sseldi 3601 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ ℤ)
692691adantr 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ ℤ)
693 0zd 11389 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 0 ∈ ℤ)
694100ad2antrr 762 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 𝑀 ∈ ℤ)
695 elfzo 12472 . . . . . . . . . . . . . . 15 ((((𝐼‘(𝑆‘𝑗)) + 1) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0..^𝑀) ↔ (0 ≤ ((𝐼‘(𝑆‘𝑗)) + 1) ∧ ((𝐼‘(𝑆‘𝑗)) + 1) < 𝑀)))
696692, 693, 694, 695syl3anc 1326 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0..^𝑀) ↔ (0 ≤ ((𝐼‘(𝑆‘𝑗)) + 1) ∧ ((𝐼‘(𝑆‘𝑗)) + 1) < 𝑀)))
697670, 690, 696mpbir2and 957 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0..^𝑀))
698697adantr 481 . . . . . . . . . . . 12 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0..^𝑀))
699 simpr 477 . . . . . . . . . . . 12 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))))
700 fveq2 6191 . . . . . . . . . . . . . 14 (𝑖 = ((𝐼‘(𝑆‘𝑗)) + 1) → (𝑄‘𝑖) = (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
701700breq1d 4663 . . . . . . . . . . . . 13 (𝑖 = ((𝐼‘(𝑆‘𝑗)) + 1) → ((𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))) ↔ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))))
702701elrab 3363 . . . . . . . . . . . 12 (((𝐼‘(𝑆‘𝑗)) + 1) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ↔ (((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0..^𝑀) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))))
703698, 699, 702sylanbrc 698 . . . . . . . . . . 11 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))})
704 suprub 10984 . . . . . . . . . . 11 ((({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ ℝ ∧ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}𝑙 ≤ 𝑥) ∧ ((𝐼‘(𝑆‘𝑗)) + 1) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}) → ((𝐼‘(𝑆‘𝑗)) + 1) ≤ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ))
705606, 651, 659, 703, 704syl31anc 1329 . . . . . . . . . 10 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → ((𝐼‘(𝑆‘𝑗)) + 1) ≤ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ))
70662eqcomd 2628 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) = (𝐼‘(𝑆‘𝑗)))
707706ad2antrr 762 . . . . . . . . . 10 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) = (𝐼‘(𝑆‘𝑗)))
708705, 707breqtrd 4679 . . . . . . . . 9 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → ((𝐼‘(𝑆‘𝑗)) + 1) ≤ (𝐼‘(𝑆‘𝑗)))
709661ltp1d 10954 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) < ((𝐼‘(𝑆‘𝑗)) + 1))
710661, 663ltnled 10184 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆‘𝑗)) < ((𝐼‘(𝑆‘𝑗)) + 1) ↔ ¬ ((𝐼‘(𝑆‘𝑗)) + 1) ≤ (𝐼‘(𝑆‘𝑗))))
711709, 710mpbid 222 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ¬ ((𝐼‘(𝑆‘𝑗)) + 1) ≤ (𝐼‘(𝑆‘𝑗)))
712711ad2antrr 762 . . . . . . . . 9 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → ¬ ((𝐼‘(𝑆‘𝑗)) + 1) ≤ (𝐼‘(𝑆‘𝑗)))
713708, 712pm2.65da 600 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ¬ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))))
714572adantr 481 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐿‘(𝐸‘(𝑆‘𝑗))) ∈ ℝ)
71550adantr 481 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ∈ ℝ)
716714, 715ltnled 10184 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝐿‘(𝐸‘(𝑆‘𝑗))) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ↔ ¬ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))))
717713, 716mpbird 247 . . . . . . 7 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐿‘(𝐸‘(𝑆‘𝑗))) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
718717adantlr 751 . . . . . 6 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐿‘(𝐸‘(𝑆‘𝑗))) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
719599, 718eqbrtrd 4675 . . . . 5 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
720598, 719pm2.61dan 832 . . . 4 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
72123ad2ant1 1082 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → 𝑀 ∈ ℕ)
72213ad2ant1 1082 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → 𝑄 ∈ (𝑃‘𝑀))
723213ad2ant1 1082 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → 𝐶 ∈ ℝ)
724223ad2ant1 1082 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → 𝐷 ∈ ℝ)
725233ad2ant1 1082 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → 𝐶 < 𝐷)
726493adant3 1081 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0...𝑀))
727 simp2 1062 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → 𝑗 ∈ (0..^𝑁))
72842leidd 10594 . . . . . . . 8 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ≤ (𝑆‘𝑗))
729 elico2 12237 . . . . . . . . 9 (((𝑆‘𝑗) ∈ ℝ ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ*) → ((𝑆‘𝑗) ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ ((𝑆‘𝑗) ∈ ℝ ∧ (𝑆‘𝑗) ≤ (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))))
73042, 212, 729syl2anc 693 . . . . . . . 8 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ ((𝑆‘𝑗) ∈ ℝ ∧ (𝑆‘𝑗) ≤ (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))))
73142, 728, 131, 730mpbir3and 1245 . . . . . . 7 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))))
7327313adant3 1081 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → (𝑆‘𝑗) ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))))
733 simp3 1063 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
734 eqid 2622 . . . . . 6 ((𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) − ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗))) = ((𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) − ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)))
73511, 3, 721, 722, 723, 724, 725, 24, 25, 26, 27, 12, 726, 727, 732, 733, 734fourierdlem63 40386 . . . . 5 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
7367353adant1r 1319 . . . 4 (((𝜑 ∧ (𝑆‘𝑗) ∈ ℝ) ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
737550, 551, 720, 736syl3anc 1326 . . 3 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
738549, 737pm2.61dan 832 . 2 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
739 ioossioo 12265 . 2 ((((𝑄‘(𝐼‘(𝑆‘𝑗))) ∈ ℝ* ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ∈ ℝ*) ∧ ((𝑄‘(𝐼‘(𝑆‘𝑗))) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))) ∧ (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))) → ((𝐿‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))))
74045, 51, 89, 738, 739syl22anc 1327 1 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐿‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1037   = wceq 1483   ∈ wcel 1990   ≠ wne 2794  ∀wral 2912  ∃wrex 2913  {crab 2916  Vcvv 3200   ∪ cun 3572   ⊆ wss 3574  ∅c0 3915  ifcif 4086  {csn 4177  {cpr 4179   class class class wbr 4653   ↦ cmpt 4729   Or wor 5034  ran crn 5115  ℩cio 5849  ⟶wf 5884  ‘cfv 5888   Isom wiso 5889  (class class class)co 6650   ↑𝑚 cmap 7857  Fincfn 7955  supcsup 8346  ℂcc 9934  ℝcr 9935  0cc0 9936  1c1 9937   + caddc 9939   · cmul 9941  ℝ*cxr 10073   < clt 10074   ≤ cle 10075   − cmin 10266   / cdiv 10684  ℕcn 11020  2c2 11070  ℤcz 11377  ℤ≥cuz 11687  ℝ+crp 11832  (,)cioo 12175  (,]cioc 12176  [,)cico 12177  [,]cicc 12178  ...cfz 12326  ..^cfzo 12465  ⌊cfl 12591  #chash 13117
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fi 8317  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-xnn0 11364  df-z 11378  df-uz 11688  df-q 11789  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-ioo 12179  df-ioc 12180  df-ico 12181  df-icc 12182  df-fz 12327  df-fzo 12466  df-fl 12593  df-seq 12802  df-exp 12861  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-rest 16083  df-topgen 16104  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-mopn 19742  df-top 20699  df-topon 20716  df-bases 20750  df-cld 20823  df-ntr 20824  df-cls 20825  df-nei 20902  df-lp 20940  df-cmp 21190
This theorem is referenced by:  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414
  Copyright terms: Public domain W3C validator