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 41329
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 41253 . . . . . . . . 9 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
52, 4syl 17 . . . . . . . 8 (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
61, 5mpbid 224 . . . . . . 7 (𝜑 → (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
76simpld 490 . . . . . 6 (𝜑 → 𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)))
8 elmapi 8162 . . . . . 6 (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
97, 8syl 17 . . . . 5 (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
109adantr 474 . . . 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 41288 . . . . . . . 8 (𝜑 → (𝐼:ℝ⟶(0..^𝑀) ∧ (𝑥 ∈ ℝ → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))})))
1615simpld 490 . . . . . . 7 (𝜑 → 𝐼:ℝ⟶(0..^𝑀))
17 fzossfz 12807 . . . . . . . 8 (0..^𝑀) ⊆ (0...𝑀)
1817a1i 11 . . . . . . 7 (𝜑 → (0..^𝑀) ⊆ (0...𝑀))
1916, 18fssd 6305 . . . . . 6 (𝜑 → 𝐼:ℝ⟶(0...𝑀))
2019adantr 474 . . . . 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 41304 . . . . . . . . . . . 12 (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
2928simpld 490 . . . . . . . . . . 11 (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)))
3029simprd 491 . . . . . . . . . 10 (𝜑 → 𝑆 ∈ (𝑂‘𝑁))
3130adantr 474 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑆 ∈ (𝑂‘𝑁))
3229simpld 490 . . . . . . . . . . 11 (𝜑 → 𝑁 ∈ ℕ)
3332adantr 474 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑁 ∈ ℕ)
3424fourierdlem2 41253 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
3533, 34syl 17 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
3631, 35mpbid 224 . . . . . . . 8 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))
3736simpld 490 . . . . . . 7 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)))
38 elmapi 8162 . . . . . . 7 (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
3937, 38syl 17 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
40 elfzofz 12804 . . . . . . 7 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ (0...𝑁))
4140adantl 475 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0...𝑁))
4239, 41ffvelrnd 6624 . . . . 5 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ ℝ)
4320, 42ffvelrnd 6624 . . . 4 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) ∈ (0...𝑀))
4410, 43ffvelrnd 6624 . . 3 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆‘𝑗))) ∈ ℝ)
4544rexrd 10426 . 2 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆‘𝑗))) ∈ ℝ*)
4616adantr 474 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐼:ℝ⟶(0..^𝑀))
4746, 42ffvelrnd 6624 . . . . 5 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) ∈ (0..^𝑀))
48 fzofzp1 12884 . . . . 5 ((𝐼‘(𝑆‘𝑗)) ∈ (0..^𝑀) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0...𝑀))
4947, 48syl 17 . . . 4 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0...𝑀))
5010, 49ffvelrnd 6624 . . 3 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ∈ ℝ)
5150rexrd 10426 . 2 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ∈ ℝ*)
5214a1i 11 . . . . 5 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < )))
53 fveq2 6446 . . . . . . . . . 10 (𝑥 = (𝑆‘𝑗) → (𝐸‘𝑥) = (𝐸‘(𝑆‘𝑗)))
5453fveq2d 6450 . . . . . . . . 9 (𝑥 = (𝑆‘𝑗) → (𝐿‘(𝐸‘𝑥)) = (𝐿‘(𝐸‘(𝑆‘𝑗))))
5554breq2d 4898 . . . . . . . 8 (𝑥 = (𝑆‘𝑗) → ((𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥)) ↔ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))))
5655rabbidv 3386 . . . . . . 7 (𝑥 = (𝑆‘𝑗) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} = {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))})
5756supeq1d 8640 . . . . . 6 (𝑥 = (𝑆‘𝑗) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ))
5857adantl 475 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 = (𝑆‘𝑗)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ))
59 ltso 10457 . . . . . . 7 < Or ℝ
6059supex 8657 . . . . . 6 sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ V
6160a1i 11 . . . . 5 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ V)
6252, 58, 42, 61fvmptd 6548 . . . 4 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ))
6362fveq2d 6450 . . 3 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆‘𝑗))) = (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )))
64 simpl 476 . . . . . . 7 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝜑)
6564, 42jca 507 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝜑 ∧ (𝑆‘𝑗) ∈ ℝ))
66 eleq1 2847 . . . . . . . . 9 (𝑥 = (𝑆‘𝑗) → (𝑥 ∈ ℝ ↔ (𝑆‘𝑗) ∈ ℝ))
6766anbi2d 622 . . . . . . . 8 (𝑥 = (𝑆‘𝑗) → ((𝜑 ∧ 𝑥 ∈ ℝ) ↔ (𝜑 ∧ (𝑆‘𝑗) ∈ ℝ)))
6857, 56eleq12d 2853 . . . . . . . 8 (𝑥 = (𝑆‘𝑗) → (sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ↔ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}))
6967, 68imbi12d 336 . . . . . . 7 (𝑥 = (𝑆‘𝑗) → (((𝜑 ∧ 𝑥 ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}) ↔ ((𝜑 ∧ (𝑆‘𝑗) ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))})))
7015simprd 491 . . . . . . . 8 (𝜑 → (𝑥 ∈ ℝ → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}))
7170imp 397 . . . . . . 7 ((𝜑 ∧ 𝑥 ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))})
7269, 71vtoclg 3467 . . . . . 6 ((𝑆‘𝑗) ∈ ℝ → ((𝜑 ∧ (𝑆‘𝑗) ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}))
7342, 65, 72sylc 65 . . . . 5 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))})
74 nfrab1 3309 . . . . . . 7 Ⅎ𝑖{𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}
75 nfcv 2934 . . . . . . 7 Ⅎ𝑖ℝ
76 nfcv 2934 . . . . . . 7 Ⅎ𝑖 <
7774, 75, 76nfsup 8645 . . . . . 6 Ⅎ𝑖sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )
78 nfcv 2934 . . . . . 6 Ⅎ𝑖(0..^𝑀)
79 nfcv 2934 . . . . . . . 8 Ⅎ𝑖𝑄
8079, 77nffv 6456 . . . . . . 7 Ⅎ𝑖(𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ))
81 nfcv 2934 . . . . . . 7 Ⅎ𝑖 ≤
82 nfcv 2934 . . . . . . 7 Ⅎ𝑖(𝐿‘(𝐸‘(𝑆‘𝑗)))
8380, 81, 82nfbr 4933 . . . . . 6 Ⅎ𝑖(𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))
84 fveq2 6446 . . . . . . 7 (𝑖 = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) → (𝑄‘𝑖) = (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )))
8584breq1d 4896 . . . . . 6 (𝑖 = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) → ((𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))) ↔ (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))))
8677, 78, 83, 85elrabf 3568 . . . . 5 (sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ↔ (sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ (0..^𝑀) ∧ (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))))
8773, 86sylib 210 . . . 4 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ (0..^𝑀) ∧ (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))))
8887simprd 491 . . 3 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))))
8963, 88eqbrtrd 4908 . 2 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆‘𝑗))) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))))
902ad2antrr 716 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝑀 ∈ ℕ)
911ad2antrr 716 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝑄 ∈ (𝑃‘𝑀))
9221ad2antrr 716 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐶 ∈ ℝ)
9322ad2antrr 716 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐷 ∈ ℝ)
9423ad2antrr 716 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐶 < 𝐷)
95 0le1 10898 . . . . . . . 8 0 ≤ 1
9695a1i 11 . . . . . . 7 (𝜑 → 0 ≤ 1)
972nnge1d 11423 . . . . . . 7 (𝜑 → 1 ≤ 𝑀)
98 1zzd 11760 . . . . . . . 8 (𝜑 → 1 ∈ ℤ)
99 0zd 11740 . . . . . . . 8 (𝜑 → 0 ∈ ℤ)
1002nnzd 11833 . . . . . . . 8 (𝜑 → 𝑀 ∈ ℤ)
101 elfz 12649 . . . . . . . 8 ((1 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (1 ∈ (0...𝑀) ↔ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
10298, 99, 100, 101syl3anc 1439 . . . . . . 7 (𝜑 → (1 ∈ (0...𝑀) ↔ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
10396, 97, 102mpbir2and 703 . . . . . 6 (𝜑 → 1 ∈ (0...𝑀))
104103ad2antrr 716 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 1 ∈ (0...𝑀))
105 simplr 759 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝑗 ∈ (0..^𝑁))
106 fourierdlem79.z . . . . . . . 8 𝑍 = ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)))
107 fzofzp1 12884 . . . . . . . . . . . . . 14 (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ (0...𝑁))
108107adantl 475 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈ (0...𝑁))
10939, 108ffvelrnd 6624 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
110109, 42resubcld 10803 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) ∈ ℝ)
111110rehalfcld 11629 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ∈ ℝ)
1129, 103ffvelrnd 6624 . . . . . . . . . . . . 13 (𝜑 → (𝑄‘1) ∈ ℝ)
1133, 2, 1fourierdlem11 41262 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
114113simp1d 1133 . . . . . . . . . . . . 13 (𝜑 → 𝐴 ∈ ℝ)
115112, 114resubcld 10803 . . . . . . . . . . . 12 (𝜑 → ((𝑄‘1) − 𝐴) ∈ ℝ)
116115rehalfcld 11629 . . . . . . . . . . 11 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ)
117116adantr 474 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ)
118111, 117ifcld 4352 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ∈ ℝ)
11942, 118readdcld 10406 . . . . . . . 8 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) ∈ ℝ)
120106, 119syl5eqel 2863 . . . . . . 7 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 ∈ ℝ)
121 2re 11449 . . . . . . . . . . . . . 14 2 ∈ ℝ
122121a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 2 ∈ ℝ)
123 elfzoelz 12789 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℤ)
124123zred 11834 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℝ)
125124ltp1d 11308 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0..^𝑁) → 𝑗 < (𝑗 + 1))
126125adantl 475 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 < (𝑗 + 1))
12728simprd 491 . . . . . . . . . . . . . . . . 17 (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝐻))
128127adantr 474 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑆 Isom < , < ((0...𝑁), 𝐻))
129 isorel 6848 . . . . . . . . . . . . . . . 16 ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝑗 + 1) ∈ (0...𝑁))) → (𝑗 < (𝑗 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1))))
130128, 41, 108, 129syl12anc 827 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 < (𝑗 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1))))
131126, 130mpbid 224 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))
13242, 109posdifd 10962 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) < (𝑆‘(𝑗 + 1)) ↔ 0 < ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗))))
133131, 132mpbid 224 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 < ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)))
134 2pos 11485 . . . . . . . . . . . . . 14 0 < 2
135134a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 < 2)
136110, 122, 133, 135divgt0d 11313 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 < (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
137111, 136elrpd 12178 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ∈ ℝ+)
138121a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 2 ∈ ℝ)
1392nngt0d 11424 . . . . . . . . . . . . . . . . . 18 (𝜑 → 0 < 𝑀)
140 fzolb 12795 . . . . . . . . . . . . . . . . . 18 (0 ∈ (0..^𝑀) ↔ (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
14199, 100, 139, 140syl3anbrc 1400 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ∈ (0..^𝑀))
142 0re 10378 . . . . . . . . . . . . . . . . . 18 0 ∈ ℝ
143 eleq1 2847 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 0 → (𝑖 ∈ (0..^𝑀) ↔ 0 ∈ (0..^𝑀)))
144143anbi2d 622 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 0 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 0 ∈ (0..^𝑀))))
145 fveq2 6446 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 0 → (𝑄‘𝑖) = (𝑄‘0))
146 oveq1 6929 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 0 → (𝑖 + 1) = (0 + 1))
147146fveq2d 6450 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 0 → (𝑄‘(𝑖 + 1)) = (𝑄‘(0 + 1)))
148145, 147breq12d 4899 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 0 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘0) < (𝑄‘(0 + 1))))
149144, 148imbi12d 336 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 0 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))))
1506simprd 491 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
151150simprd 491 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
152151r19.21bi 3114 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
153149, 152vtoclg 3467 . . . . . . . . . . . . . . . . . 18 (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1))))
154142, 153ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))
155141, 154mpdan 677 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘0) < (𝑄‘(0 + 1)))
156150simpld 490 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
157156simpld 490 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘0) = 𝐴)
158 0p1e1 11504 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
159158fveq2i 6449 . . . . . . . . . . . . . . . . 17 (𝑄‘(0 + 1)) = (𝑄‘1)
160159a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘(0 + 1)) = (𝑄‘1))
161155, 157, 1603brtr3d 4917 . . . . . . . . . . . . . . 15 (𝜑 → 𝐴 < (𝑄‘1))
162114, 112posdifd 10962 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 < (𝑄‘1) ↔ 0 < ((𝑄‘1) − 𝐴)))
163161, 162mpbid 224 . . . . . . . . . . . . . 14 (𝜑 → 0 < ((𝑄‘1) − 𝐴))
164134a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 0 < 2)
165115, 138, 163, 164divgt0d 11313 . . . . . . . . . . . . 13 (𝜑 → 0 < (((𝑄‘1) − 𝐴) / 2))
166116, 165elrpd 12178 . . . . . . . . . . . 12 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ+)
167166adantr 474 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ+)
168137, 167ifcld 4352 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ∈ ℝ+)
16942, 168ltaddrpd 12214 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) < ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
17042, 119, 169ltled 10524 . . . . . . . 8 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ≤ ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
171170, 106syl6breqr 4928 . . . . . . 7 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ≤ 𝑍)
17242, 111readdcld 10406 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) ∈ ℝ)
173 iftrue 4313 . . . . . . . . . . . . 13 (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
174173adantl 475 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
175111leidd 10941 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
176175adantr 474 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
177174, 176eqbrtrd 4908 . . . . . . . . . . 11 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
178 iffalse 4316 . . . . . . . . . . . . 13 (¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) − 𝐴) / 2))
179178adantl 475 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) − 𝐴) / 2))
180115ad2antrr 716 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑄‘1) − 𝐴) ∈ ℝ)
181110adantr 474 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) ∈ ℝ)
182 2rp 12142 . . . . . . . . . . . . . 14 2 ∈ ℝ+
183182a1i 11 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → 2 ∈ ℝ+)
184 simpr 479 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴))
185180, 181, 184nltled 10526 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑄‘1) − 𝐴) ≤ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)))
186180, 181, 183, 185lediv1dd 12239 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑄‘1) − 𝐴) / 2) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
187179, 186eqbrtrd 4908 . . . . . . . . . . 11 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
188177, 187pm2.61dan 803 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
189118, 111, 42, 188leadd2dd 10990 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) ≤ ((𝑆‘𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)))
19042recnd 10405 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ ℂ)
191109recnd 10405 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℂ)
192190, 191addcomd 10578 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) = ((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)))
193192oveq1d 6937 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) = (((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2))
194193oveq1d 6937 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = ((((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)))
195 halfaddsub 11615 . . . . . . . . . . . . . . 15 (((𝑆‘(𝑗 + 1)) ∈ ℂ ∧ (𝑆‘𝑗) ∈ ℂ) → (((((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘(𝑗 + 1)) ∧ ((((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘𝑗)))
196191, 190, 195syl2anc 579 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘(𝑗 + 1)) ∧ ((((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘𝑗)))
197196simprd 491 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘𝑗))
198194, 197eqtrd 2814 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘𝑗))
199190, 191addcld 10396 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) ∈ ℂ)
200199halfcld 11627 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) ∈ ℂ)
201111recnd 10405 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ∈ ℂ)
202200, 201, 190subsub23d 40409 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘𝑗) ↔ ((((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (𝑆‘𝑗)) = (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)))
203198, 202mpbid 224 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (𝑆‘𝑗)) = (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
204200, 190, 201subaddd 10752 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (𝑆‘𝑗)) = (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ↔ ((𝑆‘𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2)))
205203, 204mpbid 224 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2))
206 avglt2 11621 . . . . . . . . . . . 12 (((𝑆‘𝑗) ∈ ℝ ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ) → ((𝑆‘𝑗) < (𝑆‘(𝑗 + 1)) ↔ (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) < (𝑆‘(𝑗 + 1))))
20742, 109, 206syl2anc 579 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) < (𝑆‘(𝑗 + 1)) ↔ (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) < (𝑆‘(𝑗 + 1))))
208131, 207mpbid 224 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) < (𝑆‘(𝑗 + 1)))
209205, 208eqbrtrd 4908 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) < (𝑆‘(𝑗 + 1)))
210119, 172, 109, 189, 209lelttrd 10534 . . . . . . . 8 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑆‘(𝑗 + 1)))
211106, 210syl5eqbr 4921 . . . . . . 7 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 < (𝑆‘(𝑗 + 1)))
212109rexrd 10426 . . . . . . . 8 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℝ*)
213 elico2 12549 . . . . . . . 8 (((𝑆‘𝑗) ∈ ℝ ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ*) → (𝑍 ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ (𝑍 ∈ ℝ ∧ (𝑆‘𝑗) ≤ 𝑍 ∧ 𝑍 < (𝑆‘(𝑗 + 1)))))
21442, 212, 213syl2anc 579 . . . . . . 7 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑍 ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ (𝑍 ∈ ℝ ∧ (𝑆‘𝑗) ≤ 𝑍 ∧ 𝑍 < (𝑆‘(𝑗 + 1)))))
215120, 171, 211, 214mpbir3and 1399 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))))
216215adantr 474 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝑍 ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))))
217114ad2antrr 716 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐴 ∈ ℝ)
218113simp2d 1134 . . . . . . . . 9 (𝜑 → 𝐵 ∈ ℝ)
219218ad2antrr 716 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐵 ∈ ℝ)
220113simp3d 1135 . . . . . . . . 9 (𝜑 → 𝐴 < 𝐵)
221220ad2antrr 716 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐴 < 𝐵)
22242adantr 474 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑆‘𝑗) ∈ ℝ)
223 simpr 479 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) = 𝐵)
224169, 106syl6breqr 4928 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) < 𝑍)
225218, 114resubcld 10803 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
22611, 225syl5eqel 2863 . . . . . . . . . . . . 13 (𝜑 → 𝑇 ∈ ℝ)
227226adantr 474 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑇 ∈ ℝ)
228111adantr 474 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ∈ ℝ)
229116ad2antrr 716 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ)
230110adantr 474 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) ∈ ℝ)
231115ad2antrr 716 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑄‘1) − 𝐴) ∈ ℝ)
232182a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → 2 ∈ ℝ+)
233 simpr 479 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴))
234230, 231, 232, 233ltdiv1dd 12238 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) < (((𝑄‘1) − 𝐴) / 2))
235228, 229, 234ltled 10524 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ≤ (((𝑄‘1) − 𝐴) / 2))
236174, 235eqbrtrd 4908 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2))
237178adantl 475 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) − 𝐴) / 2))
238116leidd 10941 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ≤ (((𝑄‘1) − 𝐴) / 2))
239238adantr 474 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑄‘1) − 𝐴) / 2) ≤ (((𝑄‘1) − 𝐴) / 2))
240237, 239eqbrtrd 4908 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2))
241240adantlr 705 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2))
242236, 241pm2.61dan 803 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2))
243225rehalfcld 11629 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵 − 𝐴) / 2) ∈ ℝ)
244182a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 2 ∈ ℝ+)
245114rexrd 10426 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 𝐴 ∈ ℝ*)
246218rexrd 10426 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 𝐵 ∈ ℝ*)
2473, 2, 1fourierdlem15 41266 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
248247, 103ffvelrnd 6624 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑄‘1) ∈ (𝐴[,]𝐵))
249 iccleub 12541 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝑄‘1) ∈ (𝐴[,]𝐵)) → (𝑄‘1) ≤ 𝐵)
250245, 246, 248, 249syl3anc 1439 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑄‘1) ≤ 𝐵)
251112, 218, 114, 250lesub1dd 10991 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑄‘1) − 𝐴) ≤ (𝐵 − 𝐴))
252115, 225, 244, 251lediv1dd 12239 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ≤ ((𝐵 − 𝐴) / 2))
25311eqcomi 2787 . . . . . . . . . . . . . . . . . 18 (𝐵 − 𝐴) = 𝑇
254253oveq1i 6932 . . . . . . . . . . . . . . . . 17 ((𝐵 − 𝐴) / 2) = (𝑇 / 2)
255114, 218posdifd 10962 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
256220, 255mpbid 224 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 < (𝐵 − 𝐴))
257256, 11syl6breqr 4928 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 < 𝑇)
258226, 257elrpd 12178 . . . . . . . . . . . . . . . . . 18 (𝜑 → 𝑇 ∈ ℝ+)
259 rphalflt 12168 . . . . . . . . . . . . . . . . . 18 (𝑇 ∈ ℝ+ → (𝑇 / 2) < 𝑇)
260258, 259syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑇 / 2) < 𝑇)
261254, 260syl5eqbr 4921 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵 − 𝐴) / 2) < 𝑇)
262116, 243, 226, 252, 261lelttrd 10534 . . . . . . . . . . . . . . 15 (𝜑 → (((𝑄‘1) − 𝐴) / 2) < 𝑇)
263116, 226, 262ltled 10524 . . . . . . . . . . . . . 14 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ≤ 𝑇)
264263adantr 474 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑄‘1) − 𝐴) / 2) ≤ 𝑇)
265118, 117, 227, 242, 264letrd 10533 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ 𝑇)
266118, 227, 42, 265leadd2dd 10990 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) ≤ ((𝑆‘𝑗) + 𝑇))
267106, 266syl5eqbr 4921 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 ≤ ((𝑆‘𝑗) + 𝑇))
26842rexrd 10426 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ ℝ*)
26942, 227readdcld 10406 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + 𝑇) ∈ ℝ)
270 elioc2 12548 . . . . . . . . . . 11 (((𝑆‘𝑗) ∈ ℝ* ∧ ((𝑆‘𝑗) + 𝑇) ∈ ℝ) → (𝑍 ∈ ((𝑆‘𝑗)(,]((𝑆‘𝑗) + 𝑇)) ↔ (𝑍 ∈ ℝ ∧ (𝑆‘𝑗) < 𝑍 ∧ 𝑍 ≤ ((𝑆‘𝑗) + 𝑇))))
271268, 269, 270syl2anc 579 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑍 ∈ ((𝑆‘𝑗)(,]((𝑆‘𝑗) + 𝑇)) ↔ (𝑍 ∈ ℝ ∧ (𝑆‘𝑗) < 𝑍 ∧ 𝑍 ≤ ((𝑆‘𝑗) + 𝑇))))
272120, 224, 267, 271mpbir3and 1399 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 ∈ ((𝑆‘𝑗)(,]((𝑆‘𝑗) + 𝑇)))
273272adantr 474 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝑍 ∈ ((𝑆‘𝑗)(,]((𝑆‘𝑗) + 𝑇)))
274217, 219, 221, 11, 12, 222, 223, 273fourierdlem26 41277 . . . . . . 7 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘𝑍) = (𝐴 + (𝑍 − (𝑆‘𝑗))))
275106a1i 11 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 = ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
276275oveq1d 6937 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑍 − (𝑆‘𝑗)) = (((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆‘𝑗)))
277276oveq2d 6938 . . . . . . . 8 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 + (𝑍 − (𝑆‘𝑗))) = (𝐴 + (((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆‘𝑗))))
278277adantr 474 . . . . . . 7 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐴 + (𝑍 − (𝑆‘𝑗))) = (𝐴 + (((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆‘𝑗))))
279118recnd 10405 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ∈ ℂ)
280190, 279pncan2d 10736 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆‘𝑗)) = if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)))
281280oveq2d 6938 . . . . . . . 8 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 + (((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆‘𝑗))) = (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
282281adantr 474 . . . . . . 7 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐴 + (((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆‘𝑗))) = (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
283274, 278, 2823eqtrd 2818 . . . . . 6 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘𝑍) = (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
284173oveq2d 6938 . . . . . . . . . 10 (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)))
285284adantl 475 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)))
286114adantr 474 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ℝ)
287286, 111readdcld 10406 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) ∈ ℝ)
288287adantr 474 . . . . . . . . . 10 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) ∈ ℝ)
289286, 117readdcld 10406 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) ∈ ℝ)
290289adantr 474 . . . . . . . . . 10 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) ∈ ℝ)
291112ad2antrr 716 . . . . . . . . . 10 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝑄‘1) ∈ ℝ)
292114ad2antrr 716 . . . . . . . . . . 11 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → 𝐴 ∈ ℝ)
293228, 229, 292, 234ltadd2dd 10535 . . . . . . . . . 10 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) < (𝐴 + (((𝑄‘1) − 𝐴) / 2)))
294112recnd 10405 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘1) ∈ ℂ)
295114recnd 10405 . . . . . . . . . . . . . . . 16 (𝜑 → 𝐴 ∈ ℂ)
296 halfaddsub 11615 . . . . . . . . . . . . . . . 16 (((𝑄‘1) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((((𝑄‘1) + 𝐴) / 2) + (((𝑄‘1) − 𝐴) / 2)) = (𝑄‘1) ∧ ((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) = 𝐴))
297294, 295, 296syl2anc 579 . . . . . . . . . . . . . . 15 (𝜑 → (((((𝑄‘1) + 𝐴) / 2) + (((𝑄‘1) − 𝐴) / 2)) = (𝑄‘1) ∧ ((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) = 𝐴))
298297simprd 491 . . . . . . . . . . . . . 14 (𝜑 → ((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) = 𝐴)
299298oveq1d 6937 . . . . . . . . . . . . 13 (𝜑 → (((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) + (((𝑄‘1) − 𝐴) / 2)) = (𝐴 + (((𝑄‘1) − 𝐴) / 2)))
300112, 114readdcld 10406 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑄‘1) + 𝐴) ∈ ℝ)
301300rehalfcld 11629 . . . . . . . . . . . . . . 15 (𝜑 → (((𝑄‘1) + 𝐴) / 2) ∈ ℝ)
302301recnd 10405 . . . . . . . . . . . . . 14 (𝜑 → (((𝑄‘1) + 𝐴) / 2) ∈ ℂ)
303116recnd 10405 . . . . . . . . . . . . . 14 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ∈ ℂ)
304302, 303npcand 10738 . . . . . . . . . . . . 13 (𝜑 → (((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) + (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) + 𝐴) / 2))
305299, 304eqtr3d 2816 . . . . . . . . . . . 12 (𝜑 → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) + 𝐴) / 2))
306112, 112readdcld 10406 . . . . . . . . . . . . . 14 (𝜑 → ((𝑄‘1) + (𝑄‘1)) ∈ ℝ)
307114, 112, 112, 161ltadd2dd 10535 . . . . . . . . . . . . . 14 (𝜑 → ((𝑄‘1) + 𝐴) < ((𝑄‘1) + (𝑄‘1)))
308300, 306, 244, 307ltdiv1dd 12238 . . . . . . . . . . . . 13 (𝜑 → (((𝑄‘1) + 𝐴) / 2) < (((𝑄‘1) + (𝑄‘1)) / 2))
3092942timesd 11625 . . . . . . . . . . . . . . . 16 (𝜑 → (2 · (𝑄‘1)) = ((𝑄‘1) + (𝑄‘1)))
310309eqcomd 2784 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑄‘1) + (𝑄‘1)) = (2 · (𝑄‘1)))
311310oveq1d 6937 . . . . . . . . . . . . . 14 (𝜑 → (((𝑄‘1) + (𝑄‘1)) / 2) = ((2 · (𝑄‘1)) / 2))
312 2cnd 11453 . . . . . . . . . . . . . . 15 (𝜑 → 2 ∈ ℂ)
313 2ne0 11486 . . . . . . . . . . . . . . . 16 2 ≠ 0
314313a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 2 ≠ 0)
315294, 312, 314divcan3d 11156 . . . . . . . . . . . . . 14 (𝜑 → ((2 · (𝑄‘1)) / 2) = (𝑄‘1))
316311, 315eqtrd 2814 . . . . . . . . . . . . 13 (𝜑 → (((𝑄‘1) + (𝑄‘1)) / 2) = (𝑄‘1))
317308, 316breqtrd 4912 . . . . . . . . . . . 12 (𝜑 → (((𝑄‘1) + 𝐴) / 2) < (𝑄‘1))
318305, 317eqbrtrd 4908 . . . . . . . . . . 11 (𝜑 → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) < (𝑄‘1))
319318ad2antrr 716 . . . . . . . . . 10 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) < (𝑄‘1))
320288, 290, 291, 293, 319lttrd 10537 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) < (𝑄‘1))
321285, 320eqbrtrd 4908 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1))
322178oveq2d 6938 . . . . . . . . . 10 (¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑄‘1) − 𝐴) / 2)))
323322adantl 475 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑄‘1) − 𝐴) / 2)))
324318ad2antrr 716 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) < (𝑄‘1))
325323, 324eqbrtrd 4908 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1))
326321, 325pm2.61dan 803 . . . . . . 7 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1))
327326adantr 474 . . . . . 6 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1))
328283, 327eqbrtrd 4908 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘𝑍) < (𝑄‘1))
329 eqid 2778 . . . . 5 ((𝑄‘1) − ((𝐸‘𝑍) − 𝑍)) = ((𝑄‘1) − ((𝐸‘𝑍) − 𝑍))
33011, 3, 90, 91, 92, 93, 94, 24, 25, 26, 27, 12, 104, 105, 216, 328, 329fourierdlem63 41313 . . . 4 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘1))
33114a1i 11 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < )))
33257adantl 475 . . . . . . . . 9 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ 𝑥 = (𝑆‘𝑗)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ))
33360a1i 11 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ V)
334331, 332, 222, 333fvmptd 6548 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐼‘(𝑆‘𝑗)) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ))
335 fveq2 6446 . . . . . . . . . . . . 13 ((𝐸‘(𝑆‘𝑗)) = 𝐵 → (𝐿‘(𝐸‘(𝑆‘𝑗))) = (𝐿‘𝐵))
33613a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)))
337 iftrue 4313 . . . . . . . . . . . . . . 15 (𝑦 = 𝐵 → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝐴)
338337adantl 475 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑦 = 𝐵) → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝐴)
339 ubioc1 12539 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → 𝐵 ∈ (𝐴(,]𝐵))
340245, 246, 220, 339syl3anc 1439 . . . . . . . . . . . . . 14 (𝜑 → 𝐵 ∈ (𝐴(,]𝐵))
341336, 338, 340, 114fvmptd 6548 . . . . . . . . . . . . 13 (𝜑 → (𝐿‘𝐵) = 𝐴)
342335, 341sylan9eqr 2836 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐿‘(𝐸‘(𝑆‘𝑗))) = 𝐴)
343342breq2d 4898 . . . . . . . . . . 11 ((𝜑 ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))) ↔ (𝑄‘𝑖) ≤ 𝐴))
344343rabbidv 3386 . . . . . . . . . 10 ((𝜑 ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} = {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴})
345344supeq1d 8640 . . . . . . . . 9 ((𝜑 ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}, ℝ, < ))
346345adantlr 705 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}, ℝ, < ))
347 simpl 476 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}) → 𝜑)
348 elrabi 3567 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} → 𝑗 ∈ (0..^𝑀))
349348adantl 475 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}) → 𝑗 ∈ (0..^𝑀))
350 fveq2 6446 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑗 → (𝑄‘𝑖) = (𝑄‘𝑗))
351350breq1d 4896 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → ((𝑄‘𝑖) ≤ 𝐴 ↔ (𝑄‘𝑗) ≤ 𝐴))
352351elrab 3572 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} ↔ (𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴))
353352simprbi 492 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} → (𝑄‘𝑗) ≤ 𝐴)
354353adantl 475 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}) → (𝑄‘𝑗) ≤ 𝐴)
355 simp3 1129 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → (𝑄‘𝑗) ≤ 𝐴)
356114ad2antrr 716 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝐴 ∈ ℝ)
357112ad2antrr 716 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝑄‘1) ∈ ℝ)
3589adantr 474 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
35918sselda 3821 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑗 ∈ (0...𝑀))
360358, 359ffvelrnd 6624 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) ∈ ℝ)
361360adantr 474 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝑄‘𝑗) ∈ ℝ)
362161ad2antrr 716 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝐴 < (𝑄‘1))
363 1zzd 11760 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 1 ∈ ℤ)
364 elfzoelz 12789 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℤ)
365364ad2antlr 717 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝑗 ∈ ℤ)
366 1e0p1 11888 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 = (0 + 1)
367 simpr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → ¬ 𝑗 ≤ 0)
368 0red 10380 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 0 ∈ ℝ)
369365zred 11834 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝑗 ∈ ℝ)
370368, 369ltnled 10523 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (0 < 𝑗 ↔ ¬ 𝑗 ≤ 0))
371367, 370mpbird 249 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 0 < 𝑗)
372 0zd 11740 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 0 ∈ ℤ)
373 zltp1le 11779 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((0 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (0 < 𝑗 ↔ (0 + 1) ≤ 𝑗))
374372, 365, 373syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (0 < 𝑗 ↔ (0 + 1) ≤ 𝑗))
375371, 374mpbid 224 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (0 + 1) ≤ 𝑗)
376366, 375syl5eqbr 4921 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 1 ≤ 𝑗)
377 eluz2 11998 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (ℤ≥‘1) ↔ (1 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 1 ≤ 𝑗))
378363, 365, 376, 377syl3anbrc 1400 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝑗 ∈ (ℤ≥‘1))
3799ad2antrr 716 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑄:(0...𝑀)⟶ℝ)
380 0red 10380 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (1...𝑗) → 0 ∈ ℝ)
381 elfzelz 12659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 𝑙 ∈ ℤ)
382381zred 11834 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (1...𝑗) → 𝑙 ∈ ℝ)
383 1red 10377 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 1 ∈ ℝ)
384 0lt1 10897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 0 < 1
385384a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 0 < 1)
386 elfzle1 12661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 1 ≤ 𝑙)
387380, 383, 382, 385, 386ltletrd 10536 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (1...𝑗) → 0 < 𝑙)
388380, 382, 387ltled 10524 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑙 ∈ (1...𝑗) → 0 ≤ 𝑙)
389388adantl 475 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 0 ≤ 𝑙)
390382adantl 475 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ∈ ℝ)
391100zred 11834 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → 𝑀 ∈ ℝ)
392391ad2antrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑀 ∈ ℝ)
393364zred 11834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℝ)
394393ad2antlr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑗 ∈ ℝ)
395 elfzle2 12662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 𝑙 ≤ 𝑗)
396395adantl 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ≤ 𝑗)
397 elfzolt2 12798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0..^𝑀) → 𝑗 < 𝑀)
398397ad2antlr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑗 < 𝑀)
399390, 394, 392, 396, 398lelttrd 10534 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 < 𝑀)
400390, 392, 399ltled 10524 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ≤ 𝑀)
401381adantl 475 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ∈ ℤ)
402 0zd 11740 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 0 ∈ ℤ)
403100ad2antrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑀 ∈ ℤ)
404 elfz 12649 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑙 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑙 ∈ (0...𝑀) ↔ (0 ≤ 𝑙 ∧ 𝑙 ≤ 𝑀)))
405401, 402, 403, 404syl3anc 1439 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → (𝑙 ∈ (0...𝑀) ↔ (0 ≤ 𝑙 ∧ 𝑙 ≤ 𝑀)))
406389, 400, 405mpbir2and 703 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ∈ (0...𝑀))
407379, 406ffvelrnd 6624 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → (𝑄‘𝑙) ∈ ℝ)
408407adantlr 705 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) ∧ 𝑙 ∈ (1...𝑗)) → (𝑄‘𝑙) ∈ ℝ)
4099ad2antrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑄:(0...𝑀)⟶ℝ)
410 0zd 11740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ∈ ℤ)
411100ad2antrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℤ)
412 elfzelz 12659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 𝑙 ∈ ℤ)
413412adantl 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℤ)
414410, 411, 4133jca 1119 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑙 ∈ ℤ))
415 0red 10380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 0 ∈ ℝ)
416412zred 11834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 𝑙 ∈ ℝ)
417 1red 10377 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑙 ∈ (1...(𝑗 − 1)) → 1 ∈ ℝ)
418384a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑙 ∈ (1...(𝑗 − 1)) → 0 < 1)
419 elfzle1 12661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑙 ∈ (1...(𝑗 − 1)) → 1 ≤ 𝑙)
420415, 417, 416, 418, 419ltletrd 10536 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 0 < 𝑙)
421415, 416, 420ltled 10524 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...(𝑗 − 1)) → 0 ≤ 𝑙)
422421adantl 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ≤ 𝑙)
423413zred 11834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℝ)
424391ad2antrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℝ)
425393ad2antlr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 ∈ ℝ)
426416adantl 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℝ)
427 peano2rem 10690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 ∈ ℝ → (𝑗 − 1) ∈ ℝ)
428393, 427syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑗 ∈ (0..^𝑀) → (𝑗 − 1) ∈ ℝ)
429428adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑗 − 1) ∈ ℝ)
430393adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 ∈ ℝ)
431 elfzle2 12662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑙 ∈ (1...(𝑗 − 1)) → 𝑙 ≤ (𝑗 − 1))
432431adantl 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ≤ (𝑗 − 1))
433430ltm1d 11310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑗 − 1) < 𝑗)
434426, 429, 430, 432, 433lelttrd 10534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑗)
435434adantll 704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑗)
436397ad2antlr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 < 𝑀)
437423, 425, 424, 435, 436lttrd 10537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑀)
438423, 424, 437ltled 10524 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ≤ 𝑀)
439414, 422, 438jca32 511 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑙 ∈ ℤ) ∧ (0 ≤ 𝑙 ∧ 𝑙 ≤ 𝑀)))
440 elfz2 12650 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑙 ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑙 ∈ ℤ) ∧ (0 ≤ 𝑙 ∧ 𝑙 ≤ 𝑀)))
441439, 440sylibr 226 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ (0...𝑀))
442409, 441ffvelrnd 6624 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄‘𝑙) ∈ ℝ)
443413peano2zd 11837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ∈ ℤ)
444410, 411, 4433jca 1119 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑙 + 1) ∈ ℤ))
445416, 417readdcld 10406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) ∈ ℝ)
446416, 417, 420, 418addgt0d 10950 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 0 < (𝑙 + 1))
447415, 445, 446ltled 10524 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...(𝑗 − 1)) → 0 ≤ (𝑙 + 1))
448447adantl 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ≤ (𝑙 + 1))
449445adantl 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ∈ ℝ)
450445recnd 10405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) ∈ ℂ)
451 1cnd 10371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑙 ∈ (1...(𝑗 − 1)) → 1 ∈ ℂ)
452450, 451npcand 10738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑙 ∈ (1...(𝑗 − 1)) → (((𝑙 + 1) − 1) + 1) = (𝑙 + 1))
453452eqcomd 2784 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) = (((𝑙 + 1) − 1) + 1))
454453adantl 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) = (((𝑙 + 1) − 1) + 1))
455 peano2re 10549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑙 ∈ ℝ → (𝑙 + 1) ∈ ℝ)
456 peano2rem 10690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑙 + 1) ∈ ℝ → ((𝑙 + 1) − 1) ∈ ℝ)
457426, 455, 4563syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((𝑙 + 1) − 1) ∈ ℝ)
458 peano2re 10549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑗 − 1) ∈ ℝ → ((𝑗 − 1) + 1) ∈ ℝ)
459 peano2rem 10690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑗 − 1) + 1) ∈ ℝ → (((𝑗 − 1) + 1) − 1) ∈ ℝ)
460429, 458, 4593syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (((𝑗 − 1) + 1) − 1) ∈ ℝ)
461 1red 10377 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 1 ∈ ℝ)
462 elfzel2 12657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑗 − 1) ∈ ℤ)
463462zred 11834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑗 − 1) ∈ ℝ)
464463, 417readdcld 10406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑙 ∈ (1...(𝑗 − 1)) → ((𝑗 − 1) + 1) ∈ ℝ)
465416, 463, 417, 431leadd1dd 10989 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) ≤ ((𝑗 − 1) + 1))
466445, 464, 417, 465lesub1dd 10991 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑙 ∈ (1...(𝑗 − 1)) → ((𝑙 + 1) − 1) ≤ (((𝑗 − 1) + 1) − 1))
467466adantl 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((𝑙 + 1) − 1) ≤ (((𝑗 − 1) + 1) − 1))
468457, 460, 461, 467leadd1dd 10989 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (((𝑙 + 1) − 1) + 1) ≤ ((((𝑗 − 1) + 1) − 1) + 1))
469 peano2zm 11772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑗 ∈ ℤ → (𝑗 − 1) ∈ ℤ)
470364, 469syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑗 ∈ (0..^𝑀) → (𝑗 − 1) ∈ ℤ)
471470peano2zd 11837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑗 ∈ (0..^𝑀) → ((𝑗 − 1) + 1) ∈ ℤ)
472471zcnd 11835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ (0..^𝑀) → ((𝑗 − 1) + 1) ∈ ℂ)
473 1cnd 10371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ (0..^𝑀) → 1 ∈ ℂ)
474472, 473npcand 10738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 ∈ (0..^𝑀) → ((((𝑗 − 1) + 1) − 1) + 1) = ((𝑗 − 1) + 1))
475393recnd 10405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℂ)
476475, 473npcand 10738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 ∈ (0..^𝑀) → ((𝑗 − 1) + 1) = 𝑗)
477474, 476eqtrd 2814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 ∈ (0..^𝑀) → ((((𝑗 − 1) + 1) − 1) + 1) = 𝑗)
478477adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((((𝑗 − 1) + 1) − 1) + 1) = 𝑗)
479468, 478breqtrd 4912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (((𝑙 + 1) − 1) + 1) ≤ 𝑗)
480454, 479eqbrtrd 4908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ≤ 𝑗)
481480adantll 704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ≤ 𝑗)
482449, 425, 424, 481, 436lelttrd 10534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) < 𝑀)
483449, 424, 482ltled 10524 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ≤ 𝑀)
484444, 448, 483jca32 511 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑙 + 1) ∈ ℤ) ∧ (0 ≤ (𝑙 + 1) ∧ (𝑙 + 1) ≤ 𝑀)))
485 elfz2 12650 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑙 + 1) ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑙 + 1) ∈ ℤ) ∧ (0 ≤ (𝑙 + 1) ∧ (𝑙 + 1) ≤ 𝑀)))
486484, 485sylibr 226 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ∈ (0...𝑀))
487409, 486ffvelrnd 6624 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄‘(𝑙 + 1)) ∈ ℝ)
488 simpll 757 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝜑)
489 0zd 11740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ∈ ℤ)
490412adantl 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℤ)
491421adantl 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ≤ 𝑙)
492 eluz2 11998 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (ℤ≥‘0) ↔ (0 ∈ ℤ ∧ 𝑙 ∈ ℤ ∧ 0 ≤ 𝑙))
493489, 490, 491, 492syl3anbrc 1400 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ (ℤ≥‘0))
494 elfzoel2 12788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0..^𝑀) → 𝑀 ∈ ℤ)
495494adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℤ)
496495zred 11834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℝ)
497397adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 < 𝑀)
498426, 430, 496, 434, 497lttrd 10537 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑀)
499 elfzo2 12792 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (0..^𝑀) ↔ (𝑙 ∈ (ℤ≥‘0) ∧ 𝑀 ∈ ℤ ∧ 𝑙 < 𝑀))
500493, 495, 498, 499syl3anbrc 1400 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ (0..^𝑀))
501500adantll 704 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ (0..^𝑀))
502 eleq1 2847 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 = 𝑙 → (𝑖 ∈ (0..^𝑀) ↔ 𝑙 ∈ (0..^𝑀)))
503502anbi2d 622 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 = 𝑙 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 𝑙 ∈ (0..^𝑀))))
504 fveq2 6446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 = 𝑙 → (𝑄‘𝑖) = (𝑄‘𝑙))
505 oveq1 6929 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 = 𝑙 → (𝑖 + 1) = (𝑙 + 1))
506505fveq2d 6450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 = 𝑙 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑙 + 1)))
507504, 506breq12d 4899 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 = 𝑙 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘𝑙) < (𝑄‘(𝑙 + 1))))
508503, 507imbi12d 336 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 = 𝑙 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑙 ∈ (0..^𝑀)) → (𝑄‘𝑙) < (𝑄‘(𝑙 + 1)))))
509508, 152chvarv 2361 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ 𝑙 ∈ (0..^𝑀)) → (𝑄‘𝑙) < (𝑄‘(𝑙 + 1)))
510488, 501, 509syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄‘𝑙) < (𝑄‘(𝑙 + 1)))
511442, 487, 510ltled 10524 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄‘𝑙) ≤ (𝑄‘(𝑙 + 1)))
512511adantlr 705 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄‘𝑙) ≤ (𝑄‘(𝑙 + 1)))
513378, 408, 512monoord 13149 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝑄‘1) ≤ (𝑄‘𝑗))
514356, 357, 361, 362, 513ltletrd 10536 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝐴 < (𝑄‘𝑗))
515356, 361ltnled 10523 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝐴 < (𝑄‘𝑗) ↔ ¬ (𝑄‘𝑗) ≤ 𝐴))
516514, 515mpbid 224 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → ¬ (𝑄‘𝑗) ≤ 𝐴)
517516ex 403 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (¬ 𝑗 ≤ 0 → ¬ (𝑄‘𝑗) ≤ 𝐴))
5185173adant3 1123 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → (¬ 𝑗 ≤ 0 → ¬ (𝑄‘𝑗) ≤ 𝐴))
519355, 518mt4d 154 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → 𝑗 ≤ 0)
520 elfzole1 12797 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0..^𝑀) → 0 ≤ 𝑗)
5215203ad2ant2 1125 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → 0 ≤ 𝑗)
5223933ad2ant2 1125 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → 𝑗 ∈ ℝ)
523 0red 10380 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → 0 ∈ ℝ)
524522, 523letri3d 10518 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → (𝑗 = 0 ↔ (𝑗 ≤ 0 ∧ 0 ≤ 𝑗)))
525519, 521, 524mpbir2and 703 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → 𝑗 = 0)
526347, 349, 354, 525syl3anc 1439 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}) → 𝑗 = 0)
527 velsn 4414 . . . . . . . . . . . . . . 15 (𝑗 ∈ {0} ↔ 𝑗 = 0)
528526, 527sylibr 226 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}) → 𝑗 ∈ {0})
529528ralrimiva 3148 . . . . . . . . . . . . 13 (𝜑 → ∀𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}𝑗 ∈ {0})
530 dfss3 3810 . . . . . . . . . . . . 13 ({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} ⊆ {0} ↔ ∀𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}𝑗 ∈ {0})
531529, 530sylibr 226 . . . . . . . . . . . 12 (𝜑 → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} ⊆ {0})
532157, 114eqeltrd 2859 . . . . . . . . . . . . . . 15 (𝜑 → (𝑄‘0) ∈ ℝ)
533532, 157eqled 10479 . . . . . . . . . . . . . 14 (𝜑 → (𝑄‘0) ≤ 𝐴)
534145breq1d 4896 . . . . . . . . . . . . . . 15 (𝑖 = 0 → ((𝑄‘𝑖) ≤ 𝐴 ↔ (𝑄‘0) ≤ 𝐴))
535534elrab 3572 . . . . . . . . . . . . . 14 (0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} ↔ (0 ∈ (0..^𝑀) ∧ (𝑄‘0) ≤ 𝐴))
536141, 533, 535sylanbrc 578 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴})
537536snssd 4571 . . . . . . . . . . . 12 (𝜑 → {0} ⊆ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴})
538531, 537eqssd 3838 . . . . . . . . . . 11 (𝜑 → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} = {0})
539538supeq1d 8640 . . . . . . . . . 10 (𝜑 → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}, ℝ, < ) = sup({0}, ℝ, < ))
540 supsn 8666 . . . . . . . . . . . 12 (( < Or ℝ ∧ 0 ∈ ℝ) → sup({0}, ℝ, < ) = 0)
54159, 142, 540mp2an 682 . . . . . . . . . . 11 sup({0}, ℝ, < ) = 0
542541a1i 11 . . . . . . . . . 10 (𝜑 → sup({0}, ℝ, < ) = 0)
543539, 542eqtrd 2814 . . . . . . . . 9 (𝜑 → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}, ℝ, < ) = 0)
544543ad2antrr 716 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}, ℝ, < ) = 0)
545334, 346, 5443eqtrd 2818 . . . . . . 7 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐼‘(𝑆‘𝑗)) = 0)
546545oveq1d 6937 . . . . . 6 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝐼‘(𝑆‘𝑗)) + 1) = (0 + 1))
547546fveq2d 6450 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) = (𝑄‘(0 + 1)))
548547, 159syl6req 2831 . . . 4 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑄‘1) = (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
549330, 548breqtrd 4912 . . 3 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
55065adantr 474 . . . 4 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝜑 ∧ (𝑆‘𝑗) ∈ ℝ))
551 simplr 759 . . . 4 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝑗 ∈ (0..^𝑁))
55213a1i 11 . . . . . . . . . . 11 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)))
553 simpr 479 . . . . . . . . . . . . . . . 16 ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → 𝑦 = (𝐸‘(𝑆‘𝑗)))
554 neqne 2977 . . . . . . . . . . . . . . . . 17 (¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 → (𝐸‘(𝑆‘𝑗)) ≠ 𝐵)
555554adantr 474 . . . . . . . . . . . . . . . 16 ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → (𝐸‘(𝑆‘𝑗)) ≠ 𝐵)
556553, 555eqnetrd 3036 . . . . . . . . . . . . . . 15 ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → 𝑦 ≠ 𝐵)
557556neneqd 2974 . . . . . . . . . . . . . 14 ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → ¬ 𝑦 = 𝐵)
558557iffalsed 4318 . . . . . . . . . . . . 13 ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝑦)
559558, 553eqtrd 2814 . . . . . . . . . . . 12 ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = (𝐸‘(𝑆‘𝑗)))
560559adantll 704 . . . . . . . . . . 11 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = (𝐸‘(𝑆‘𝑗)))
561114, 218, 220, 11, 12fourierdlem4 41255 . . . . . . . . . . . . . 14 (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))
562561adantr 474 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐸:ℝ⟶(𝐴(,]𝐵))
563562, 42ffvelrnd 6624 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘𝑗)) ∈ (𝐴(,]𝐵))
564563adantr 474 . . . . . . . . . . 11 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) ∈ (𝐴(,]𝐵))
565552, 560, 564, 564fvmptd 6548 . . . . . . . . . 10 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐿‘(𝐸‘(𝑆‘𝑗))) = (𝐸‘(𝑆‘𝑗)))
566565eqcomd 2784 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) = (𝐿‘(𝐸‘(𝑆‘𝑗))))
567114, 218, 220, 13fourierdlem17 41268 . . . . . . . . . . . . 13 (𝜑 → 𝐿:(𝐴(,]𝐵)⟶(𝐴[,]𝐵))
568567adantr 474 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐿:(𝐴(,]𝐵)⟶(𝐴[,]𝐵))
569114, 218iccssred 40639 . . . . . . . . . . . . 13 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
570569adantr 474 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴[,]𝐵) ⊆ ℝ)
571568, 570fssd 6305 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐿:(𝐴(,]𝐵)⟶ℝ)
572571, 563ffvelrnd 6624 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐿‘(𝐸‘(𝑆‘𝑗))) ∈ ℝ)
573572adantr 474 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐿‘(𝐸‘(𝑆‘𝑗))) ∈ ℝ)
574566, 573eqeltrd 2859 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) ∈ ℝ)
575218ad2antrr 716 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐵 ∈ ℝ)
576245adantr 474 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ℝ*)
577218adantr 474 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐵 ∈ ℝ)
578 elioc2 12548 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐸‘(𝑆‘𝑗)) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘(𝑆‘𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆‘𝑗)) ∧ (𝐸‘(𝑆‘𝑗)) ≤ 𝐵)))
579576, 577, 578syl2anc 579 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘𝑗)) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘(𝑆‘𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆‘𝑗)) ∧ (𝐸‘(𝑆‘𝑗)) ≤ 𝐵)))
580563, 579mpbid 224 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆‘𝑗)) ∧ (𝐸‘(𝑆‘𝑗)) ≤ 𝐵))
581580simp3d 1135 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘𝑗)) ≤ 𝐵)
582581adantr 474 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) ≤ 𝐵)
583554necomd 3024 . . . . . . . . 9 (¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 → 𝐵 ≠ (𝐸‘(𝑆‘𝑗)))
584583adantl 475 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐵 ≠ (𝐸‘(𝑆‘𝑗)))
585574, 575, 582, 584leneltd 10530 . . . . . . 7 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) < 𝐵)
586585adantr 474 . . . . . 6 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆‘𝑗)) < 𝐵)
587 oveq1 6929 . . . . . . . . . . 11 ((𝐼‘(𝑆‘𝑗)) = (𝑀 − 1) → ((𝐼‘(𝑆‘𝑗)) + 1) = ((𝑀 − 1) + 1))
5882nncnd 11392 . . . . . . . . . . . 12 (𝜑 → 𝑀 ∈ ℂ)
589 1cnd 10371 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℂ)
590588, 589npcand 10738 . . . . . . . . . . 11 (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
591587, 590sylan9eqr 2836 . . . . . . . . . 10 ((𝜑 ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆‘𝑗)) + 1) = 𝑀)
592591fveq2d 6450 . . . . . . . . 9 ((𝜑 ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) = (𝑄‘𝑀))
593156simprd 491 . . . . . . . . . 10 (𝜑 → (𝑄‘𝑀) = 𝐵)
594593adantr 474 . . . . . . . . 9 ((𝜑 ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝑄‘𝑀) = 𝐵)
595592, 594eqtr2d 2815 . . . . . . . 8 ((𝜑 ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 𝐵 = (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
596595adantlr 705 . . . . . . 7 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 𝐵 = (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
597596adantlr 705 . . . . . 6 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 𝐵 = (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
598586, 597breqtrd 4912 . . . . 5 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
599566adantr 474 . . . . . 6 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆‘𝑗)) = (𝐿‘(𝐸‘(𝑆‘𝑗))))
600 ssrab2 3908 . . . . . . . . . . . . 13 {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ (0..^𝑀)
601 fzssz 12660 . . . . . . . . . . . . . . 15 (0...𝑀) ⊆ ℤ
60217, 601sstri 3830 . . . . . . . . . . . . . 14 (0..^𝑀) ⊆ ℤ
603 zssre 11735 . . . . . . . . . . . . . 14 ℤ ⊆ ℝ
604602, 603sstri 3830 . . . . . . . . . . . . 13 (0..^𝑀) ⊆ ℝ
605600, 604sstri 3830 . . . . . . . . . . . 12 {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ ℝ
606605a1i 11 . . . . . . . . . . 11 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ ℝ)
60756neeq1d 3028 . . . . . . . . . . . . . . 15 (𝑥 = (𝑆‘𝑗) → ({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ≠ ∅ ↔ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ≠ ∅))
60867, 607imbi12d 336 . . . . . . . . . . . . . 14 (𝑥 = (𝑆‘𝑗) → (((𝜑 ∧ 𝑥 ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ≠ ∅) ↔ ((𝜑 ∧ (𝑆‘𝑗) ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ≠ ∅)))
609141adantr 474 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ∈ (0..^𝑀))
610533ad2antrr 716 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝐸‘𝑥) = 𝐵) → (𝑄‘0) ≤ 𝐴)
611 iftrue 4313 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸‘𝑥) = 𝐵 → if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)) = 𝐴)
612611eqcomd 2784 . . . . . . . . . . . . . . . . . . . 20 ((𝐸‘𝑥) = 𝐵 → 𝐴 = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
613612adantl 475 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝐸‘𝑥) = 𝐵) → 𝐴 = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
614610, 613breqtrd 4912 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝐸‘𝑥) = 𝐵) → (𝑄‘0) ≤ if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
615532adantr 474 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) ∈ ℝ)
616114adantr 474 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ)
617616rexrd 10426 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ*)
618218adantr 474 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℝ)
619 iocssre 12565 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
620617, 618, 619syl2anc 579 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
621561ffvelrnda 6623 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐸‘𝑥) ∈ (𝐴(,]𝐵))
622620, 621sseldd 3822 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐸‘𝑥) ∈ ℝ)
623157adantr 474 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) = 𝐴)
624 elioc2 12548 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐸‘𝑥) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘𝑥) ∈ ℝ ∧ 𝐴 < (𝐸‘𝑥) ∧ (𝐸‘𝑥) ≤ 𝐵)))
625617, 618, 624syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐸‘𝑥) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘𝑥) ∈ ℝ ∧ 𝐴 < (𝐸‘𝑥) ∧ (𝐸‘𝑥) ≤ 𝐵)))
626621, 625mpbid 224 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐸‘𝑥) ∈ ℝ ∧ 𝐴 < (𝐸‘𝑥) ∧ (𝐸‘𝑥) ≤ 𝐵))
627626simp2d 1134 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 < (𝐸‘𝑥))
628623, 627eqbrtrd 4908 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) < (𝐸‘𝑥))
629615, 622, 628ltled 10524 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) ≤ (𝐸‘𝑥))
630629adantr 474 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐸‘𝑥) = 𝐵) → (𝑄‘0) ≤ (𝐸‘𝑥))
631 iffalse 4316 . . . . . . . . . . . . . . . . . . . . 21 (¬ (𝐸‘𝑥) = 𝐵 → if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)) = (𝐸‘𝑥))
632631eqcomd 2784 . . . . . . . . . . . . . . . . . . . 20 (¬ (𝐸‘𝑥) = 𝐵 → (𝐸‘𝑥) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
633632adantl 475 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐸‘𝑥) = 𝐵) → (𝐸‘𝑥) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
634630, 633breqtrd 4912 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐸‘𝑥) = 𝐵) → (𝑄‘0) ≤ if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
635614, 634pm2.61dan 803 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) ≤ if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
63613a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)))
637 eqeq1 2782 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐸‘𝑥) → (𝑦 = 𝐵 ↔ (𝐸‘𝑥) = 𝐵))
638 id 22 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐸‘𝑥) → 𝑦 = (𝐸‘𝑥))
639637, 638ifbieq2d 4332 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝐸‘𝑥) → if(𝑦 = 𝐵, 𝐴, 𝑦) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
640639adantl 475 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 = (𝐸‘𝑥)) → if(𝑦 = 𝐵, 𝐴, 𝑦) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
641616, 622ifcld 4352 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)) ∈ ℝ)
642636, 640, 621, 641fvmptd 6548 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐿‘(𝐸‘𝑥)) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
643635, 642breqtrrd 4914 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) ≤ (𝐿‘(𝐸‘𝑥)))
644145breq1d 4896 . . . . . . . . . . . . . . . . 17 (𝑖 = 0 → ((𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥)) ↔ (𝑄‘0) ≤ (𝐿‘(𝐸‘𝑥))))
645644elrab 3572 . . . . . . . . . . . . . . . 16 (0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ↔ (0 ∈ (0..^𝑀) ∧ (𝑄‘0) ≤ (𝐿‘(𝐸‘𝑥))))
646609, 643, 645sylanbrc 578 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))})
647 ne0i 4149 . . . . . . . . . . . . . . 15 (0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ≠ ∅)
648646, 647syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑥 ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ≠ ∅)
649608, 648vtoclg 3467 . . . . . . . . . . . . 13 ((𝑆‘𝑗) ∈ ℝ → ((𝜑 ∧ (𝑆‘𝑗) ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ≠ ∅))
65042, 65, 649sylc 65 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ≠ ∅)
651650ad2antrr 716 . . . . . . . . . . 11 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ≠ ∅)
652605a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ ℝ)
653 fzofi 13092 . . . . . . . . . . . . . . 15 (0..^𝑀) ∈ Fin
654 ssfi 8468 . . . . . . . . . . . . . . 15 (((0..^𝑀) ∈ Fin ∧ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ (0..^𝑀)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ∈ Fin)
655653, 600, 654mp2an 682 . . . . . . . . . . . . . 14 {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ∈ Fin
656655a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ∈ Fin)
657 fimaxre2 11323 . . . . . . . . . . . . 13 (({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ ℝ ∧ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}𝑙 ≤ 𝑥)
658652, 656, 657syl2anc 579 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}𝑙 ≤ 𝑥)
659658ad2antrr 716 . . . . . . . . . . 11 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}𝑙 ≤ 𝑥)
660 0red 10380 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 ∈ ℝ)
661604, 47sseldi 3819 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) ∈ ℝ)
662 1red 10377 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 1 ∈ ℝ)
663661, 662readdcld 10406 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ ℝ)
664 elfzouz 12793 . . . . . . . . . . . . . . . . . 18 ((𝐼‘(𝑆‘𝑗)) ∈ (0..^𝑀) → (𝐼‘(𝑆‘𝑗)) ∈ (ℤ≥‘0))
665 eluzle 12005 . . . . . . . . . . . . . . . . . 18 ((𝐼‘(𝑆‘𝑗)) ∈ (ℤ≥‘0) → 0 ≤ (𝐼‘(𝑆‘𝑗)))
66647, 664, 6653syl 18 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 ≤ (𝐼‘(𝑆‘𝑗)))
667384a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 < 1)
668661, 662, 666, 667addgegt0d 10948 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 < ((𝐼‘(𝑆‘𝑗)) + 1))
669660, 663, 668ltled 10524 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 ≤ ((𝐼‘(𝑆‘𝑗)) + 1))
670669adantr 474 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 0 ≤ ((𝐼‘(𝑆‘𝑗)) + 1))
671661adantr 474 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐼‘(𝑆‘𝑗)) ∈ ℝ)
672 1red 10377 . . . . . . . . . . . . . . . . . 18 (𝜑 → 1 ∈ ℝ)
673391, 672resubcld 10803 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 − 1) ∈ ℝ)
674673ad2antrr 716 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝑀 − 1) ∈ ℝ)
675 1red 10377 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 1 ∈ ℝ)
676 elfzolt2 12798 . . . . . . . . . . . . . . . . . . . 20 ((𝐼‘(𝑆‘𝑗)) ∈ (0..^𝑀) → (𝐼‘(𝑆‘𝑗)) < 𝑀)
67747, 676syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) < 𝑀)
678601, 43sseldi 3819 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) ∈ ℤ)
679100adantr 474 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑀 ∈ ℤ)
680 zltlem1 11782 . . . . . . . . . . . . . . . . . . . 20 (((𝐼‘(𝑆‘𝑗)) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝐼‘(𝑆‘𝑗)) < 𝑀 ↔ (𝐼‘(𝑆‘𝑗)) ≤ (𝑀 − 1)))
681678, 679, 680syl2anc 579 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆‘𝑗)) < 𝑀 ↔ (𝐼‘(𝑆‘𝑗)) ≤ (𝑀 − 1)))
682677, 681mpbid 224 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) ≤ (𝑀 − 1))
683682adantr 474 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐼‘(𝑆‘𝑗)) ≤ (𝑀 − 1))
684 neqne 2977 . . . . . . . . . . . . . . . . . . 19 (¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1) → (𝐼‘(𝑆‘𝑗)) ≠ (𝑀 − 1))
685684necomd 3024 . . . . . . . . . . . . . . . . . 18 (¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1) → (𝑀 − 1) ≠ (𝐼‘(𝑆‘𝑗)))
686685adantl 475 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝑀 − 1) ≠ (𝐼‘(𝑆‘𝑗)))
687671, 674, 683, 686leneltd 10530 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐼‘(𝑆‘𝑗)) < (𝑀 − 1))
688671, 674, 675, 687ltadd1dd 10986 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆‘𝑗)) + 1) < ((𝑀 − 1) + 1))
689590ad2antrr 716 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝑀 − 1) + 1) = 𝑀)
690688, 689breqtrd 4912 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆‘𝑗)) + 1) < 𝑀)
691601, 49sseldi 3819 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ ℤ)
692691adantr 474 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ ℤ)
693 0zd 11740 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 0 ∈ ℤ)
694100ad2antrr 716 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 𝑀 ∈ ℤ)
695 elfzo 12791 . . . . . . . . . . . . . . 15 ((((𝐼‘(𝑆‘𝑗)) + 1) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0..^𝑀) ↔ (0 ≤ ((𝐼‘(𝑆‘𝑗)) + 1) ∧ ((𝐼‘(𝑆‘𝑗)) + 1) < 𝑀)))
696692, 693, 694, 695syl3anc 1439 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0..^𝑀) ↔ (0 ≤ ((𝐼‘(𝑆‘𝑗)) + 1) ∧ ((𝐼‘(𝑆‘𝑗)) + 1) < 𝑀)))
697670, 690, 696mpbir2and 703 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0..^𝑀))
698697adantr 474 . . . . . . . . . . . 12 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0..^𝑀))
699 simpr 479 . . . . . . . . . . . 12 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))))
700 fveq2 6446 . . . . . . . . . . . . . 14 (𝑖 = ((𝐼‘(𝑆‘𝑗)) + 1) → (𝑄‘𝑖) = (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
701700breq1d 4896 . . . . . . . . . . . . 13 (𝑖 = ((𝐼‘(𝑆‘𝑗)) + 1) → ((𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))) ↔ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))))
702701elrab 3572 . . . . . . . . . . . 12 (((𝐼‘(𝑆‘𝑗)) + 1) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ↔ (((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0..^𝑀) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))))
703698, 699, 702sylanbrc 578 . . . . . . . . . . 11 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))})
704 suprub 11338 . . . . . . . . . . 11 ((({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ ℝ ∧ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}𝑙 ≤ 𝑥) ∧ ((𝐼‘(𝑆‘𝑗)) + 1) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}) → ((𝐼‘(𝑆‘𝑗)) + 1) ≤ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ))
705606, 651, 659, 703, 704syl31anc 1441 . . . . . . . . . 10 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → ((𝐼‘(𝑆‘𝑗)) + 1) ≤ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ))
70662eqcomd 2784 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) = (𝐼‘(𝑆‘𝑗)))
707706ad2antrr 716 . . . . . . . . . 10 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) = (𝐼‘(𝑆‘𝑗)))
708705, 707breqtrd 4912 . . . . . . . . 9 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → ((𝐼‘(𝑆‘𝑗)) + 1) ≤ (𝐼‘(𝑆‘𝑗)))
709661ltp1d 11308 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) < ((𝐼‘(𝑆‘𝑗)) + 1))
710661, 663ltnled 10523 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆‘𝑗)) < ((𝐼‘(𝑆‘𝑗)) + 1) ↔ ¬ ((𝐼‘(𝑆‘𝑗)) + 1) ≤ (𝐼‘(𝑆‘𝑗))))
711709, 710mpbid 224 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ¬ ((𝐼‘(𝑆‘𝑗)) + 1) ≤ (𝐼‘(𝑆‘𝑗)))
712711ad2antrr 716 . . . . . . . . 9 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → ¬ ((𝐼‘(𝑆‘𝑗)) + 1) ≤ (𝐼‘(𝑆‘𝑗)))
713708, 712pm2.65da 807 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ¬ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))))
714572adantr 474 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐿‘(𝐸‘(𝑆‘𝑗))) ∈ ℝ)
71550adantr 474 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ∈ ℝ)
716714, 715ltnled 10523 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝐿‘(𝐸‘(𝑆‘𝑗))) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ↔ ¬ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))))
717713, 716mpbird 249 . . . . . . 7 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐿‘(𝐸‘(𝑆‘𝑗))) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
718717adantlr 705 . . . . . 6 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐿‘(𝐸‘(𝑆‘𝑗))) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
719599, 718eqbrtrd 4908 . . . . 5 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
720598, 719pm2.61dan 803 . . . 4 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
72123ad2ant1 1124 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → 𝑀 ∈ ℕ)
72213ad2ant1 1124 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → 𝑄 ∈ (𝑃‘𝑀))
723213ad2ant1 1124 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → 𝐶 ∈ ℝ)
724223ad2ant1 1124 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → 𝐷 ∈ ℝ)
725233ad2ant1 1124 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → 𝐶 < 𝐷)
726493adant3 1123 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0...𝑀))
727 simp2 1128 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → 𝑗 ∈ (0..^𝑁))
72842leidd 10941 . . . . . . . 8 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ≤ (𝑆‘𝑗))
729 elico2 12549 . . . . . . . . 9 (((𝑆‘𝑗) ∈ ℝ ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ*) → ((𝑆‘𝑗) ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ ((𝑆‘𝑗) ∈ ℝ ∧ (𝑆‘𝑗) ≤ (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))))
73042, 212, 729syl2anc 579 . . . . . . . 8 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ ((𝑆‘𝑗) ∈ ℝ ∧ (𝑆‘𝑗) ≤ (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))))
73142, 728, 131, 730mpbir3and 1399 . . . . . . 7 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))))
7327313adant3 1123 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → (𝑆‘𝑗) ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))))
733 simp3 1129 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
734 eqid 2778 . . . . . 6 ((𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) − ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗))) = ((𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) − ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)))
73511, 3, 721, 722, 723, 724, 725, 24, 25, 26, 27, 12, 726, 727, 732, 733, 734fourierdlem63 41313 . . . . 5 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
7367353adant1r 1180 . . . 4 (((𝜑 ∧ (𝑆‘𝑗) ∈ ℝ) ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
737550, 551, 720, 736syl3anc 1439 . . 3 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
738549, 737pm2.61dan 803 . 2 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
739 ioossioo 12578 . 2 ((((𝑄‘(𝐼‘(𝑆‘𝑗))) ∈ ℝ* ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ∈ ℝ*) ∧ ((𝑄‘(𝐼‘(𝑆‘𝑗))) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))) ∧ (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))) → ((𝐿‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))))
74045, 51, 89, 738, 739syl22anc 829 1 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐿‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386   ∧ w3a 1071   = wceq 1601   ∈ wcel 2107   ≠ wne 2969  ∀wral 3090  ∃wrex 3091  {crab 3094  Vcvv 3398   ∪ cun 3790   ⊆ wss 3792  ∅c0 4141  ifcif 4307  {csn 4398  {cpr 4400   class class class wbr 4886   ↦ cmpt 4965   Or wor 5273  ran crn 5356  ℩cio 6097  ⟶wf 6131  ‘cfv 6135   Isom wiso 6136  (class class class)co 6922   ↑𝑚 cmap 8140  Fincfn 8241  supcsup 8634  ℂcc 10270  ℝcr 10271  0cc0 10272  1c1 10273   + caddc 10275   · cmul 10277  ℝ*cxr 10410   < clt 10411   ≤ cle 10412   − cmin 10606   / cdiv 11032  ℕcn 11374  2c2 11430  ℤcz 11728  ℤ≥cuz 11992  ℝ+crp 12137  (,)cioo 12487  (,]cioc 12488  [,)cico 12489  [,]cicc 12490  ...cfz 12643  ..^cfzo 12784  ⌊cfl 12910  ♯chash 13435
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-inf2 8835  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349  ax-pre-sup 10350
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-int 4711  df-iun 4755  df-iin 4756  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-se 5315  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-isom 6144  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-1st 7445  df-2nd 7446  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-oadd 7847  df-er 8026  df-map 8142  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-fi 8605  df-sup 8636  df-inf 8637  df-oi 8704  df-card 9098  df-cda 9325  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-nn 11375  df-2 11438  df-3 11439  df-n0 11643  df-xnn0 11715  df-z 11729  df-uz 11993  df-q 12096  df-rp 12138  df-xneg 12257  df-xadd 12258  df-xmul 12259  df-ioo 12491  df-ioc 12492  df-ico 12493  df-icc 12494  df-fz 12644  df-fzo 12785  df-fl 12912  df-seq 13120  df-exp 13179  df-hash 13436  df-cj 14246  df-re 14247  df-im 14248  df-sqrt 14382  df-abs 14383  df-rest 16469  df-topgen 16490  df-psmet 20134  df-xmet 20135  df-met 20136  df-bl 20137  df-mopn 20138  df-top 21106  df-topon 21123  df-bases 21158  df-cld 21231  df-ntr 21232  df-cls 21233  df-nei 21310  df-lp 21348  df-cmp 21599
This theorem is referenced by:  fourierdlem89  41339  fourierdlem90  41340  fourierdlem91  41341
  Copyright terms: Public domain W3C validator