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 42469
Description: 𝐸 projects every interval of the partition induced by 𝑆 on 𝐻 into a corresponding interval of the partition induced by 𝑄 on [𝐴, 𝐵]. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem79.t 𝑇 = (𝐵 − 𝐴)
fourierdlem79.p 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem79.m (𝜑 → 𝑀 ∈ ℕ)
fourierdlem79.q (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
fourierdlem79.c (𝜑 → 𝐶 ∈ ℝ)
fourierdlem79.d (𝜑 → 𝐷 ∈ ℝ)
fourierdlem79.cltd (𝜑 → 𝐶 < 𝐷)
fourierdlem79.o 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem79.h 𝐻 = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
fourierdlem79.n 𝑁 = ((♯‘𝐻) − 1)
fourierdlem79.s 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
fourierdlem79.e 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
fourierdlem79.l 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))
fourierdlem79.z 𝑍 = ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)))
fourierdlem79.i 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ))
Assertion
Ref Expression
fourierdlem79 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐿‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))))
Distinct variable groups:   𝐴,𝑖,𝑗,𝑥   𝐴,𝑚,𝑝,𝑖   𝑦,𝐴,𝑗,𝑥   𝐵,𝑓   𝐵,𝑖,𝑘,𝑥   𝐵,𝑚,𝑝   𝑦,𝐵   𝐶,𝑖,𝑚,𝑝   𝑥,𝐶   𝐷,𝑖,𝑚,𝑝   𝑥,𝐷   𝑓,𝐸   𝑖,𝐸,𝑘,𝑥   𝑦,𝐸   𝑓,𝐻   𝑥,𝐻   𝑓,𝐼   𝑖,𝐼,𝑘,𝑥   𝑖,𝐿,𝑥   𝑖,𝑀,𝑗,𝑥   𝑚,𝑀,𝑝   𝑓,𝑁   𝑖,𝑁,𝑘,𝑥   𝑚,𝑁,𝑝   𝑦,𝑁   𝑄,𝑓,𝑗   𝑄,𝑖,𝑘,𝑥,𝑗   𝑄,𝑝   𝑆,𝑓   𝑆,𝑖,𝑘,𝑥   𝑆,𝑝   𝑦,𝑆   𝑇,𝑖,𝑘,𝑥   𝑘,𝑍,𝑥   𝜑,𝑓,𝑗   𝜑,𝑖,𝑘,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑚,𝑝)   𝐴(𝑓,𝑘)   𝐵(𝑗)   𝐶(𝑦,𝑓,𝑗,𝑘)   𝐷(𝑦,𝑓,𝑗,𝑘)   𝑃(𝑥,𝑦,𝑓,𝑖,𝑗,𝑘,𝑚,𝑝)   𝑄(𝑦,𝑚)   𝑆(𝑗,𝑚)   𝑇(𝑦,𝑓,𝑗,𝑚,𝑝)   𝐸(𝑗,𝑚,𝑝)   𝐻(𝑦,𝑖,𝑗,𝑘,𝑚,𝑝)   𝐼(𝑦,𝑗,𝑚,𝑝)   𝐿(𝑦,𝑓,𝑗,𝑘,𝑚,𝑝)   𝑀(𝑦,𝑓,𝑘)   𝑁(𝑗)   𝑂(𝑥,𝑦,𝑓,𝑖,𝑗,𝑘,𝑚,𝑝)   𝑍(𝑦,𝑓,𝑖,𝑗,𝑚,𝑝)
Proof of Theorem fourierdlem79
Dummy variable 𝑙 is distinct from all other variables.
StepHypRef Expression
1 fourierdlem79.q . . . . . . . 8 (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
2 fourierdlem79.m . . . . . . . . 9 (𝜑 → 𝑀 ∈ ℕ)
3 fourierdlem79.p . . . . . . . . . 10 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
43fourierdlem2 42393 . . . . . . . . 9 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
52, 4syl 17 . . . . . . . 8 (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
61, 5mpbid 234 . . . . . . 7 (𝜑 → (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
76simpld 497 . . . . . 6 (𝜑 → 𝑄 ∈ (ℝ ↑m (0...𝑀)))
8 elmapi 8427 . . . . . 6 (𝑄 ∈ (ℝ ↑m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
97, 8syl 17 . . . . 5 (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
109adantr 483 . . . 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 42428 . . . . . . . 8 (𝜑 → (𝐼:ℝ⟶(0..^𝑀) ∧ (𝑥 ∈ ℝ → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))})))
1615simpld 497 . . . . . . 7 (𝜑 → 𝐼:ℝ⟶(0..^𝑀))
17 fzossfz 13055 . . . . . . . 8 (0..^𝑀) ⊆ (0...𝑀)
1817a1i 11 . . . . . . 7 (𝜑 → (0..^𝑀) ⊆ (0...𝑀))
1916, 18fssd 6527 . . . . . 6 (𝜑 → 𝐼:ℝ⟶(0...𝑀))
2019adantr 483 . . . . 5 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐼:ℝ⟶(0...𝑀))
21 fourierdlem79.c . . . . . . . . . . . . 13 (𝜑 → 𝐶 ∈ ℝ)
22 fourierdlem79.d . . . . . . . . . . . . 13 (𝜑 → 𝐷 ∈ ℝ)
23 fourierdlem79.cltd . . . . . . . . . . . . 13 (𝜑 → 𝐶 < 𝐷)
24 fourierdlem79.o . . . . . . . . . . . . 13 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
25 fourierdlem79.h . . . . . . . . . . . . 13 𝐻 = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
26 fourierdlem79.n . . . . . . . . . . . . 13 𝑁 = ((♯‘𝐻) − 1)
27 fourierdlem79.s . . . . . . . . . . . . 13 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
2811, 3, 2, 1, 21, 22, 23, 24, 25, 26, 27fourierdlem54 42444 . . . . . . . . . . . 12 (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
2928simpld 497 . . . . . . . . . . 11 (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)))
3029simprd 498 . . . . . . . . . 10 (𝜑 → 𝑆 ∈ (𝑂‘𝑁))
3130adantr 483 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑆 ∈ (𝑂‘𝑁))
3229simpld 497 . . . . . . . . . . 11 (𝜑 → 𝑁 ∈ ℕ)
3332adantr 483 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑁 ∈ ℕ)
3424fourierdlem2 42393 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
3533, 34syl 17 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
3631, 35mpbid 234 . . . . . . . 8 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆 ∈ (ℝ ↑m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))
3736simpld 497 . . . . . . 7 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑆 ∈ (ℝ ↑m (0...𝑁)))
38 elmapi 8427 . . . . . . 7 (𝑆 ∈ (ℝ ↑m (0...𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
3937, 38syl 17 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
40 elfzofz 13052 . . . . . . 7 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ (0...𝑁))
4140adantl 484 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0...𝑁))
4239, 41ffvelrnd 6851 . . . . 5 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ ℝ)
4320, 42ffvelrnd 6851 . . . 4 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) ∈ (0...𝑀))
4410, 43ffvelrnd 6851 . . 3 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆‘𝑗))) ∈ ℝ)
4544rexrd 10690 . 2 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆‘𝑗))) ∈ ℝ*)
4616adantr 483 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐼:ℝ⟶(0..^𝑀))
4746, 42ffvelrnd 6851 . . . . 5 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) ∈ (0..^𝑀))
48 fzofzp1 13133 . . . . 5 ((𝐼‘(𝑆‘𝑗)) ∈ (0..^𝑀) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0...𝑀))
4947, 48syl 17 . . . 4 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0...𝑀))
5010, 49ffvelrnd 6851 . . 3 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ∈ ℝ)
5150rexrd 10690 . 2 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ∈ ℝ*)
5214a1i 11 . . . . 5 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < )))
53 fveq2 6669 . . . . . . . . . 10 (𝑥 = (𝑆‘𝑗) → (𝐸‘𝑥) = (𝐸‘(𝑆‘𝑗)))
5453fveq2d 6673 . . . . . . . . 9 (𝑥 = (𝑆‘𝑗) → (𝐿‘(𝐸‘𝑥)) = (𝐿‘(𝐸‘(𝑆‘𝑗))))
5554breq2d 5077 . . . . . . . 8 (𝑥 = (𝑆‘𝑗) → ((𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥)) ↔ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))))
5655rabbidv 3480 . . . . . . 7 (𝑥 = (𝑆‘𝑗) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} = {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))})
5756supeq1d 8909 . . . . . 6 (𝑥 = (𝑆‘𝑗) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ))
5857adantl 484 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 = (𝑆‘𝑗)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ))
59 ltso 10720 . . . . . . 7 < Or ℝ
6059supex 8926 . . . . . 6 sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ V
6160a1i 11 . . . . 5 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ V)
6252, 58, 42, 61fvmptd 6774 . . . 4 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ))
6362fveq2d 6673 . . 3 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆‘𝑗))) = (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )))
64 simpl 485 . . . . . . 7 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝜑)
6564, 42jca 514 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝜑 ∧ (𝑆‘𝑗) ∈ ℝ))
66 eleq1 2900 . . . . . . . . 9 (𝑥 = (𝑆‘𝑗) → (𝑥 ∈ ℝ ↔ (𝑆‘𝑗) ∈ ℝ))
6766anbi2d 630 . . . . . . . 8 (𝑥 = (𝑆‘𝑗) → ((𝜑 ∧ 𝑥 ∈ ℝ) ↔ (𝜑 ∧ (𝑆‘𝑗) ∈ ℝ)))
6857, 56eleq12d 2907 . . . . . . . 8 (𝑥 = (𝑆‘𝑗) → (sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ↔ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}))
6967, 68imbi12d 347 . . . . . . 7 (𝑥 = (𝑆‘𝑗) → (((𝜑 ∧ 𝑥 ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}) ↔ ((𝜑 ∧ (𝑆‘𝑗) ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))})))
7015simprd 498 . . . . . . . 8 (𝜑 → (𝑥 ∈ ℝ → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}))
7170imp 409 . . . . . . 7 ((𝜑 ∧ 𝑥 ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))})
7269, 71vtoclg 3567 . . . . . 6 ((𝑆‘𝑗) ∈ ℝ → ((𝜑 ∧ (𝑆‘𝑗) ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}))
7342, 65, 72sylc 65 . . . . 5 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))})
74 nfrab1 3384 . . . . . . 7 Ⅎ𝑖{𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}
75 nfcv 2977 . . . . . . 7 Ⅎ𝑖ℝ
76 nfcv 2977 . . . . . . 7 Ⅎ𝑖 <
7774, 75, 76nfsup 8914 . . . . . 6 Ⅎ𝑖sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )
78 nfcv 2977 . . . . . 6 Ⅎ𝑖(0..^𝑀)
79 nfcv 2977 . . . . . . . 8 Ⅎ𝑖𝑄
8079, 77nffv 6679 . . . . . . 7 Ⅎ𝑖(𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ))
81 nfcv 2977 . . . . . . 7 Ⅎ𝑖 ≤
82 nfcv 2977 . . . . . . 7 Ⅎ𝑖(𝐿‘(𝐸‘(𝑆‘𝑗)))
8380, 81, 82nfbr 5112 . . . . . 6 Ⅎ𝑖(𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))
84 fveq2 6669 . . . . . . 7 (𝑖 = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) → (𝑄‘𝑖) = (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )))
8584breq1d 5075 . . . . . 6 (𝑖 = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) → ((𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))) ↔ (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))))
8677, 78, 83, 85elrabf 3675 . . . . 5 (sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ↔ (sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ (0..^𝑀) ∧ (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))))
8773, 86sylib 220 . . . 4 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ (0..^𝑀) ∧ (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))))
8887simprd 498 . . 3 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))))
8963, 88eqbrtrd 5087 . 2 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆‘𝑗))) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))))
902ad2antrr 724 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝑀 ∈ ℕ)
911ad2antrr 724 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝑄 ∈ (𝑃‘𝑀))
9221ad2antrr 724 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐶 ∈ ℝ)
9322ad2antrr 724 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐷 ∈ ℝ)
9423ad2antrr 724 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐶 < 𝐷)
95 0le1 11162 . . . . . . . 8 0 ≤ 1
9695a1i 11 . . . . . . 7 (𝜑 → 0 ≤ 1)
972nnge1d 11684 . . . . . . 7 (𝜑 → 1 ≤ 𝑀)
98 1zzd 12012 . . . . . . . 8 (𝜑 → 1 ∈ ℤ)
99 0zd 11992 . . . . . . . 8 (𝜑 → 0 ∈ ℤ)
1002nnzd 12085 . . . . . . . 8 (𝜑 → 𝑀 ∈ ℤ)
101 elfz 12897 . . . . . . . 8 ((1 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (1 ∈ (0...𝑀) ↔ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
10298, 99, 100, 101syl3anc 1367 . . . . . . 7 (𝜑 → (1 ∈ (0...𝑀) ↔ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
10396, 97, 102mpbir2and 711 . . . . . 6 (𝜑 → 1 ∈ (0...𝑀))
104103ad2antrr 724 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 1 ∈ (0...𝑀))
105 simplr 767 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝑗 ∈ (0..^𝑁))
106 fourierdlem79.z . . . . . . . 8 𝑍 = ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)))
107 fzofzp1 13133 . . . . . . . . . . . . . 14 (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ (0...𝑁))
108107adantl 484 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈ (0...𝑁))
10939, 108ffvelrnd 6851 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
110109, 42resubcld 11067 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) ∈ ℝ)
111110rehalfcld 11883 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ∈ ℝ)
1129, 103ffvelrnd 6851 . . . . . . . . . . . . 13 (𝜑 → (𝑄‘1) ∈ ℝ)
1133, 2, 1fourierdlem11 42402 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
114113simp1d 1138 . . . . . . . . . . . . 13 (𝜑 → 𝐴 ∈ ℝ)
115112, 114resubcld 11067 . . . . . . . . . . . 12 (𝜑 → ((𝑄‘1) − 𝐴) ∈ ℝ)
116115rehalfcld 11883 . . . . . . . . . . 11 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ)
117116adantr 483 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ)
118111, 117ifcld 4511 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ∈ ℝ)
11942, 118readdcld 10669 . . . . . . . 8 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) ∈ ℝ)
120106, 119eqeltrid 2917 . . . . . . 7 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 ∈ ℝ)
121 2re 11710 . . . . . . . . . . . . . 14 2 ∈ ℝ
122121a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 2 ∈ ℝ)
123 elfzoelz 13037 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℤ)
124123zred 12086 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℝ)
125124ltp1d 11569 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0..^𝑁) → 𝑗 < (𝑗 + 1))
126125adantl 484 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 < (𝑗 + 1))
12728simprd 498 . . . . . . . . . . . . . . . . 17 (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝐻))
128127adantr 483 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑆 Isom < , < ((0...𝑁), 𝐻))
129 isorel 7078 . . . . . . . . . . . . . . . 16 ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝑗 + 1) ∈ (0...𝑁))) → (𝑗 < (𝑗 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1))))
130128, 41, 108, 129syl12anc 834 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 < (𝑗 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1))))
131126, 130mpbid 234 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))
13242, 109posdifd 11226 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) < (𝑆‘(𝑗 + 1)) ↔ 0 < ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗))))
133131, 132mpbid 234 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 < ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)))
134 2pos 11739 . . . . . . . . . . . . . 14 0 < 2
135134a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 < 2)
136110, 122, 133, 135divgt0d 11574 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 < (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
137111, 136elrpd 12427 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ∈ ℝ+)
138121a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 2 ∈ ℝ)
1392nngt0d 11685 . . . . . . . . . . . . . . . . . 18 (𝜑 → 0 < 𝑀)
140 fzolb 13043 . . . . . . . . . . . . . . . . . 18 (0 ∈ (0..^𝑀) ↔ (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
14199, 100, 139, 140syl3anbrc 1339 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ∈ (0..^𝑀))
142 0re 10642 . . . . . . . . . . . . . . . . . 18 0 ∈ ℝ
143 eleq1 2900 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 0 → (𝑖 ∈ (0..^𝑀) ↔ 0 ∈ (0..^𝑀)))
144143anbi2d 630 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 0 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 0 ∈ (0..^𝑀))))
145 fveq2 6669 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 0 → (𝑄‘𝑖) = (𝑄‘0))
146 oveq1 7162 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 0 → (𝑖 + 1) = (0 + 1))
147146fveq2d 6673 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 0 → (𝑄‘(𝑖 + 1)) = (𝑄‘(0 + 1)))
148145, 147breq12d 5078 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 0 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘0) < (𝑄‘(0 + 1))))
149144, 148imbi12d 347 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 0 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))))
1506simprd 498 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
151150simprd 498 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
152151r19.21bi 3208 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
153149, 152vtoclg 3567 . . . . . . . . . . . . . . . . . 18 (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1))))
154142, 153ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))
155141, 154mpdan 685 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘0) < (𝑄‘(0 + 1)))
156150simpld 497 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
157156simpld 497 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘0) = 𝐴)
158 0p1e1 11758 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
159158fveq2i 6672 . . . . . . . . . . . . . . . . 17 (𝑄‘(0 + 1)) = (𝑄‘1)
160159a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘(0 + 1)) = (𝑄‘1))
161155, 157, 1603brtr3d 5096 . . . . . . . . . . . . . . 15 (𝜑 → 𝐴 < (𝑄‘1))
162114, 112posdifd 11226 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 < (𝑄‘1) ↔ 0 < ((𝑄‘1) − 𝐴)))
163161, 162mpbid 234 . . . . . . . . . . . . . 14 (𝜑 → 0 < ((𝑄‘1) − 𝐴))
164134a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 0 < 2)
165115, 138, 163, 164divgt0d 11574 . . . . . . . . . . . . 13 (𝜑 → 0 < (((𝑄‘1) − 𝐴) / 2))
166116, 165elrpd 12427 . . . . . . . . . . . 12 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ+)
167166adantr 483 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ+)
168137, 167ifcld 4511 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ∈ ℝ+)
16942, 168ltaddrpd 12463 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) < ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
17042, 119, 169ltled 10787 . . . . . . . 8 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ≤ ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
171170, 106breqtrrdi 5107 . . . . . . 7 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ≤ 𝑍)
17242, 111readdcld 10669 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) ∈ ℝ)
173 iftrue 4472 . . . . . . . . . . . . 13 (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
174173adantl 484 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
175111leidd 11205 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
176175adantr 483 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
177174, 176eqbrtrd 5087 . . . . . . . . . . 11 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
178 iffalse 4475 . . . . . . . . . . . . 13 (¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) − 𝐴) / 2))
179178adantl 484 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) − 𝐴) / 2))
180115ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑄‘1) − 𝐴) ∈ ℝ)
181110adantr 483 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) ∈ ℝ)
182 2rp 12393 . . . . . . . . . . . . . 14 2 ∈ ℝ+
183182a1i 11 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → 2 ∈ ℝ+)
184 simpr 487 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴))
185180, 181, 184nltled 10789 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑄‘1) − 𝐴) ≤ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)))
186180, 181, 183, 185lediv1dd 12488 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑄‘1) − 𝐴) / 2) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
187179, 186eqbrtrd 5087 . . . . . . . . . . 11 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
188177, 187pm2.61dan 811 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
189118, 111, 42, 188leadd2dd 11254 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) ≤ ((𝑆‘𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)))
19042recnd 10668 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ ℂ)
191109recnd 10668 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℂ)
192190, 191addcomd 10841 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) = ((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)))
193192oveq1d 7170 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) = (((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2))
194193oveq1d 7170 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = ((((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)))
195 halfaddsub 11869 . . . . . . . . . . . . . . 15 (((𝑆‘(𝑗 + 1)) ∈ ℂ ∧ (𝑆‘𝑗) ∈ ℂ) → (((((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘(𝑗 + 1)) ∧ ((((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘𝑗)))
196191, 190, 195syl2anc 586 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘(𝑗 + 1)) ∧ ((((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘𝑗)))
197196simprd 498 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘𝑗))
198194, 197eqtrd 2856 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘𝑗))
199190, 191addcld 10659 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) ∈ ℂ)
200199halfcld 11881 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) ∈ ℂ)
201111recnd 10668 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ∈ ℂ)
202200, 201, 190subsub23d 41551 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘𝑗) ↔ ((((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (𝑆‘𝑗)) = (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)))
203198, 202mpbid 234 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (𝑆‘𝑗)) = (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))
204200, 190, 201subaddd 11014 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (𝑆‘𝑗)) = (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ↔ ((𝑆‘𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2)))
205203, 204mpbid 234 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2))
206 avglt2 11875 . . . . . . . . . . . 12 (((𝑆‘𝑗) ∈ ℝ ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ) → ((𝑆‘𝑗) < (𝑆‘(𝑗 + 1)) ↔ (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) < (𝑆‘(𝑗 + 1))))
20742, 109, 206syl2anc 586 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) < (𝑆‘(𝑗 + 1)) ↔ (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) < (𝑆‘(𝑗 + 1))))
208131, 207mpbid 234 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) < (𝑆‘(𝑗 + 1)))
209205, 208eqbrtrd 5087 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) < (𝑆‘(𝑗 + 1)))
210119, 172, 109, 189, 209lelttrd 10797 . . . . . . . 8 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑆‘(𝑗 + 1)))
211106, 210eqbrtrid 5100 . . . . . . 7 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 < (𝑆‘(𝑗 + 1)))
212109rexrd 10690 . . . . . . . 8 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℝ*)
213 elico2 12799 . . . . . . . 8 (((𝑆‘𝑗) ∈ ℝ ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ*) → (𝑍 ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ (𝑍 ∈ ℝ ∧ (𝑆‘𝑗) ≤ 𝑍 ∧ 𝑍 < (𝑆‘(𝑗 + 1)))))
21442, 212, 213syl2anc 586 . . . . . . 7 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑍 ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ (𝑍 ∈ ℝ ∧ (𝑆‘𝑗) ≤ 𝑍 ∧ 𝑍 < (𝑆‘(𝑗 + 1)))))
215120, 171, 211, 214mpbir3and 1338 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))))
216215adantr 483 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝑍 ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))))
217114ad2antrr 724 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐴 ∈ ℝ)
218113simp2d 1139 . . . . . . . . 9 (𝜑 → 𝐵 ∈ ℝ)
219218ad2antrr 724 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐵 ∈ ℝ)
220113simp3d 1140 . . . . . . . . 9 (𝜑 → 𝐴 < 𝐵)
221220ad2antrr 724 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐴 < 𝐵)
22242adantr 483 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑆‘𝑗) ∈ ℝ)
223 simpr 487 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) = 𝐵)
224169, 106breqtrrdi 5107 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) < 𝑍)
225218, 114resubcld 11067 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
22611, 225eqeltrid 2917 . . . . . . . . . . . . 13 (𝜑 → 𝑇 ∈ ℝ)
227226adantr 483 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑇 ∈ ℝ)
228111adantr 483 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ∈ ℝ)
229116ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ)
230110adantr 483 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) ∈ ℝ)
231115ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑄‘1) − 𝐴) ∈ ℝ)
232182a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → 2 ∈ ℝ+)
233 simpr 487 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴))
234230, 231, 232, 233ltdiv1dd 12487 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) < (((𝑄‘1) − 𝐴) / 2))
235228, 229, 234ltled 10787 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ≤ (((𝑄‘1) − 𝐴) / 2))
236174, 235eqbrtrd 5087 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2))
237178adantl 484 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) − 𝐴) / 2))
238116leidd 11205 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ≤ (((𝑄‘1) − 𝐴) / 2))
239238adantr 483 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑄‘1) − 𝐴) / 2) ≤ (((𝑄‘1) − 𝐴) / 2))
240237, 239eqbrtrd 5087 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2))
241240adantlr 713 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2))
242236, 241pm2.61dan 811 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2))
243225rehalfcld 11883 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵 − 𝐴) / 2) ∈ ℝ)
244182a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 2 ∈ ℝ+)
245114rexrd 10690 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 𝐴 ∈ ℝ*)
246218rexrd 10690 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 𝐵 ∈ ℝ*)
2473, 2, 1fourierdlem15 42406 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
248247, 103ffvelrnd 6851 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑄‘1) ∈ (𝐴[,]𝐵))
249 iccleub 12791 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝑄‘1) ∈ (𝐴[,]𝐵)) → (𝑄‘1) ≤ 𝐵)
250245, 246, 248, 249syl3anc 1367 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑄‘1) ≤ 𝐵)
251112, 218, 114, 250lesub1dd 11255 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑄‘1) − 𝐴) ≤ (𝐵 − 𝐴))
252115, 225, 244, 251lediv1dd 12488 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ≤ ((𝐵 − 𝐴) / 2))
25311eqcomi 2830 . . . . . . . . . . . . . . . . . 18 (𝐵 − 𝐴) = 𝑇
254253oveq1i 7165 . . . . . . . . . . . . . . . . 17 ((𝐵 − 𝐴) / 2) = (𝑇 / 2)
255114, 218posdifd 11226 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
256220, 255mpbid 234 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 < (𝐵 − 𝐴))
257256, 11breqtrrdi 5107 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 < 𝑇)
258226, 257elrpd 12427 . . . . . . . . . . . . . . . . . 18 (𝜑 → 𝑇 ∈ ℝ+)
259 rphalflt 12417 . . . . . . . . . . . . . . . . . 18 (𝑇 ∈ ℝ+ → (𝑇 / 2) < 𝑇)
260258, 259syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑇 / 2) < 𝑇)
261254, 260eqbrtrid 5100 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵 − 𝐴) / 2) < 𝑇)
262116, 243, 226, 252, 261lelttrd 10797 . . . . . . . . . . . . . . 15 (𝜑 → (((𝑄‘1) − 𝐴) / 2) < 𝑇)
263116, 226, 262ltled 10787 . . . . . . . . . . . . . 14 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ≤ 𝑇)
264263adantr 483 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑄‘1) − 𝐴) / 2) ≤ 𝑇)
265118, 117, 227, 242, 264letrd 10796 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ 𝑇)
266118, 227, 42, 265leadd2dd 11254 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) ≤ ((𝑆‘𝑗) + 𝑇))
267106, 266eqbrtrid 5100 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 ≤ ((𝑆‘𝑗) + 𝑇))
26842rexrd 10690 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ ℝ*)
26942, 227readdcld 10669 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + 𝑇) ∈ ℝ)
270 elioc2 12798 . . . . . . . . . . 11 (((𝑆‘𝑗) ∈ ℝ* ∧ ((𝑆‘𝑗) + 𝑇) ∈ ℝ) → (𝑍 ∈ ((𝑆‘𝑗)(,]((𝑆‘𝑗) + 𝑇)) ↔ (𝑍 ∈ ℝ ∧ (𝑆‘𝑗) < 𝑍 ∧ 𝑍 ≤ ((𝑆‘𝑗) + 𝑇))))
271268, 269, 270syl2anc 586 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑍 ∈ ((𝑆‘𝑗)(,]((𝑆‘𝑗) + 𝑇)) ↔ (𝑍 ∈ ℝ ∧ (𝑆‘𝑗) < 𝑍 ∧ 𝑍 ≤ ((𝑆‘𝑗) + 𝑇))))
272120, 224, 267, 271mpbir3and 1338 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 ∈ ((𝑆‘𝑗)(,]((𝑆‘𝑗) + 𝑇)))
273272adantr 483 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝑍 ∈ ((𝑆‘𝑗)(,]((𝑆‘𝑗) + 𝑇)))
274217, 219, 221, 11, 12, 222, 223, 273fourierdlem26 42417 . . . . . . 7 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘𝑍) = (𝐴 + (𝑍 − (𝑆‘𝑗))))
275106a1i 11 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 = ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
276275oveq1d 7170 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑍 − (𝑆‘𝑗)) = (((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆‘𝑗)))
277276oveq2d 7171 . . . . . . . 8 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 + (𝑍 − (𝑆‘𝑗))) = (𝐴 + (((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆‘𝑗))))
278277adantr 483 . . . . . . 7 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐴 + (𝑍 − (𝑆‘𝑗))) = (𝐴 + (((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆‘𝑗))))
279118recnd 10668 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ∈ ℂ)
280190, 279pncan2d 10998 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆‘𝑗)) = if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)))
281280oveq2d 7171 . . . . . . . 8 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 + (((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆‘𝑗))) = (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
282281adantr 483 . . . . . . 7 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐴 + (((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆‘𝑗))) = (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
283274, 278, 2823eqtrd 2860 . . . . . 6 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘𝑍) = (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
284173oveq2d 7171 . . . . . . . . . 10 (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)))
285284adantl 484 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)))
286114adantr 483 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ℝ)
287286, 111readdcld 10669 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) ∈ ℝ)
288287adantr 483 . . . . . . . . . 10 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) ∈ ℝ)
289286, 117readdcld 10669 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) ∈ ℝ)
290289adantr 483 . . . . . . . . . 10 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) ∈ ℝ)
291112ad2antrr 724 . . . . . . . . . 10 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝑄‘1) ∈ ℝ)
292114ad2antrr 724 . . . . . . . . . . 11 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → 𝐴 ∈ ℝ)
293228, 229, 292, 234ltadd2dd 10798 . . . . . . . . . 10 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) < (𝐴 + (((𝑄‘1) − 𝐴) / 2)))
294112recnd 10668 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘1) ∈ ℂ)
295114recnd 10668 . . . . . . . . . . . . . . . 16 (𝜑 → 𝐴 ∈ ℂ)
296 halfaddsub 11869 . . . . . . . . . . . . . . . 16 (((𝑄‘1) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((((𝑄‘1) + 𝐴) / 2) + (((𝑄‘1) − 𝐴) / 2)) = (𝑄‘1) ∧ ((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) = 𝐴))
297294, 295, 296syl2anc 586 . . . . . . . . . . . . . . 15 (𝜑 → (((((𝑄‘1) + 𝐴) / 2) + (((𝑄‘1) − 𝐴) / 2)) = (𝑄‘1) ∧ ((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) = 𝐴))
298297simprd 498 . . . . . . . . . . . . . 14 (𝜑 → ((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) = 𝐴)
299298oveq1d 7170 . . . . . . . . . . . . 13 (𝜑 → (((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) + (((𝑄‘1) − 𝐴) / 2)) = (𝐴 + (((𝑄‘1) − 𝐴) / 2)))
300112, 114readdcld 10669 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑄‘1) + 𝐴) ∈ ℝ)
301300rehalfcld 11883 . . . . . . . . . . . . . . 15 (𝜑 → (((𝑄‘1) + 𝐴) / 2) ∈ ℝ)
302301recnd 10668 . . . . . . . . . . . . . 14 (𝜑 → (((𝑄‘1) + 𝐴) / 2) ∈ ℂ)
303116recnd 10668 . . . . . . . . . . . . . 14 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ∈ ℂ)
304302, 303npcand 11000 . . . . . . . . . . . . 13 (𝜑 → (((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) + (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) + 𝐴) / 2))
305299, 304eqtr3d 2858 . . . . . . . . . . . 12 (𝜑 → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) + 𝐴) / 2))
306112, 112readdcld 10669 . . . . . . . . . . . . . 14 (𝜑 → ((𝑄‘1) + (𝑄‘1)) ∈ ℝ)
307114, 112, 112, 161ltadd2dd 10798 . . . . . . . . . . . . . 14 (𝜑 → ((𝑄‘1) + 𝐴) < ((𝑄‘1) + (𝑄‘1)))
308300, 306, 244, 307ltdiv1dd 12487 . . . . . . . . . . . . 13 (𝜑 → (((𝑄‘1) + 𝐴) / 2) < (((𝑄‘1) + (𝑄‘1)) / 2))
3092942timesd 11879 . . . . . . . . . . . . . . . 16 (𝜑 → (2 · (𝑄‘1)) = ((𝑄‘1) + (𝑄‘1)))
310309eqcomd 2827 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑄‘1) + (𝑄‘1)) = (2 · (𝑄‘1)))
311310oveq1d 7170 . . . . . . . . . . . . . 14 (𝜑 → (((𝑄‘1) + (𝑄‘1)) / 2) = ((2 · (𝑄‘1)) / 2))
312 2cnd 11714 . . . . . . . . . . . . . . 15 (𝜑 → 2 ∈ ℂ)
313 2ne0 11740 . . . . . . . . . . . . . . . 16 2 ≠ 0
314313a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 2 ≠ 0)
315294, 312, 314divcan3d 11420 . . . . . . . . . . . . . 14 (𝜑 → ((2 · (𝑄‘1)) / 2) = (𝑄‘1))
316311, 315eqtrd 2856 . . . . . . . . . . . . 13 (𝜑 → (((𝑄‘1) + (𝑄‘1)) / 2) = (𝑄‘1))
317308, 316breqtrd 5091 . . . . . . . . . . . 12 (𝜑 → (((𝑄‘1) + 𝐴) / 2) < (𝑄‘1))
318305, 317eqbrtrd 5087 . . . . . . . . . . 11 (𝜑 → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) < (𝑄‘1))
319318ad2antrr 724 . . . . . . . . . 10 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) < (𝑄‘1))
320288, 290, 291, 293, 319lttrd 10800 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) < (𝑄‘1))
321285, 320eqbrtrd 5087 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1))
322178oveq2d 7171 . . . . . . . . . 10 (¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑄‘1) − 𝐴) / 2)))
323322adantl 484 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑄‘1) − 𝐴) / 2)))
324318ad2antrr 724 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) < (𝑄‘1))
325323, 324eqbrtrd 5087 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1))
326321, 325pm2.61dan 811 . . . . . . 7 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1))
327326adantr 483 . . . . . 6 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1))
328283, 327eqbrtrd 5087 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘𝑍) < (𝑄‘1))
329 eqid 2821 . . . . 5 ((𝑄‘1) − ((𝐸‘𝑍) − 𝑍)) = ((𝑄‘1) − ((𝐸‘𝑍) − 𝑍))
33011, 3, 90, 91, 92, 93, 94, 24, 25, 26, 27, 12, 104, 105, 216, 328, 329fourierdlem63 42453 . . . 4 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘1))
33114a1i 11 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < )))
33257adantl 484 . . . . . . . . 9 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ 𝑥 = (𝑆‘𝑗)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ))
33360a1i 11 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ V)
334331, 332, 222, 333fvmptd 6774 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐼‘(𝑆‘𝑗)) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ))
335 fveq2 6669 . . . . . . . . . . . . 13 ((𝐸‘(𝑆‘𝑗)) = 𝐵 → (𝐿‘(𝐸‘(𝑆‘𝑗))) = (𝐿‘𝐵))
33613a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)))
337 iftrue 4472 . . . . . . . . . . . . . . 15 (𝑦 = 𝐵 → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝐴)
338337adantl 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑦 = 𝐵) → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝐴)
339 ubioc1 12789 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → 𝐵 ∈ (𝐴(,]𝐵))
340245, 246, 220, 339syl3anc 1367 . . . . . . . . . . . . . 14 (𝜑 → 𝐵 ∈ (𝐴(,]𝐵))
341336, 338, 340, 114fvmptd 6774 . . . . . . . . . . . . 13 (𝜑 → (𝐿‘𝐵) = 𝐴)
342335, 341sylan9eqr 2878 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐿‘(𝐸‘(𝑆‘𝑗))) = 𝐴)
343342breq2d 5077 . . . . . . . . . . 11 ((𝜑 ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))) ↔ (𝑄‘𝑖) ≤ 𝐴))
344343rabbidv 3480 . . . . . . . . . 10 ((𝜑 ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} = {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴})
345344supeq1d 8909 . . . . . . . . 9 ((𝜑 ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}, ℝ, < ))
346345adantlr 713 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}, ℝ, < ))
347 simpl 485 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}) → 𝜑)
348 elrabi 3674 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} → 𝑗 ∈ (0..^𝑀))
349348adantl 484 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}) → 𝑗 ∈ (0..^𝑀))
350 fveq2 6669 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑗 → (𝑄‘𝑖) = (𝑄‘𝑗))
351350breq1d 5075 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → ((𝑄‘𝑖) ≤ 𝐴 ↔ (𝑄‘𝑗) ≤ 𝐴))
352351elrab 3679 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} ↔ (𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴))
353352simprbi 499 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} → (𝑄‘𝑗) ≤ 𝐴)
354353adantl 484 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}) → (𝑄‘𝑗) ≤ 𝐴)
355 simp3 1134 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → (𝑄‘𝑗) ≤ 𝐴)
356114ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝐴 ∈ ℝ)
357112ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝑄‘1) ∈ ℝ)
3589adantr 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
35918sselda 3966 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑗 ∈ (0...𝑀))
360358, 359ffvelrnd 6851 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) ∈ ℝ)
361360adantr 483 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝑄‘𝑗) ∈ ℝ)
362161ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝐴 < (𝑄‘1))
363 1zzd 12012 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 1 ∈ ℤ)
364 elfzoelz 13037 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℤ)
365364ad2antlr 725 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝑗 ∈ ℤ)
366 1e0p1 12139 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 = (0 + 1)
367 simpr 487 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → ¬ 𝑗 ≤ 0)
368 0red 10643 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 0 ∈ ℝ)
369365zred 12086 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝑗 ∈ ℝ)
370368, 369ltnled 10786 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (0 < 𝑗 ↔ ¬ 𝑗 ≤ 0))
371367, 370mpbird 259 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 0 < 𝑗)
372 0zd 11992 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 0 ∈ ℤ)
373 zltp1le 12031 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((0 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (0 < 𝑗 ↔ (0 + 1) ≤ 𝑗))
374372, 365, 373syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (0 < 𝑗 ↔ (0 + 1) ≤ 𝑗))
375371, 374mpbid 234 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (0 + 1) ≤ 𝑗)
376366, 375eqbrtrid 5100 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 1 ≤ 𝑗)
377 eluz2 12248 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (ℤ≥‘1) ↔ (1 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 1 ≤ 𝑗))
378363, 365, 376, 377syl3anbrc 1339 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝑗 ∈ (ℤ≥‘1))
3799ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑄:(0...𝑀)⟶ℝ)
380 0red 10643 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (1...𝑗) → 0 ∈ ℝ)
381 elfzelz 12907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 𝑙 ∈ ℤ)
382381zred 12086 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (1...𝑗) → 𝑙 ∈ ℝ)
383 1red 10641 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 1 ∈ ℝ)
384 0lt1 11161 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 0 < 1
385384a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 0 < 1)
386 elfzle1 12909 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 1 ≤ 𝑙)
387380, 383, 382, 385, 386ltletrd 10799 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (1...𝑗) → 0 < 𝑙)
388380, 382, 387ltled 10787 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑙 ∈ (1...𝑗) → 0 ≤ 𝑙)
389388adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 0 ≤ 𝑙)
390382adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ∈ ℝ)
391100zred 12086 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → 𝑀 ∈ ℝ)
392391ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑀 ∈ ℝ)
393364zred 12086 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℝ)
394393ad2antlr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑗 ∈ ℝ)
395 elfzle2 12910 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 𝑙 ≤ 𝑗)
396395adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ≤ 𝑗)
397 elfzolt2 13046 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0..^𝑀) → 𝑗 < 𝑀)
398397ad2antlr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑗 < 𝑀)
399390, 394, 392, 396, 398lelttrd 10797 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 < 𝑀)
400390, 392, 399ltled 10787 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ≤ 𝑀)
401381adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ∈ ℤ)
402 0zd 11992 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 0 ∈ ℤ)
403100ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑀 ∈ ℤ)
404 elfz 12897 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑙 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑙 ∈ (0...𝑀) ↔ (0 ≤ 𝑙 ∧ 𝑙 ≤ 𝑀)))
405401, 402, 403, 404syl3anc 1367 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → (𝑙 ∈ (0...𝑀) ↔ (0 ≤ 𝑙 ∧ 𝑙 ≤ 𝑀)))
406389, 400, 405mpbir2and 711 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ∈ (0...𝑀))
407379, 406ffvelrnd 6851 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → (𝑄‘𝑙) ∈ ℝ)
408407adantlr 713 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) ∧ 𝑙 ∈ (1...𝑗)) → (𝑄‘𝑙) ∈ ℝ)
4099ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑄:(0...𝑀)⟶ℝ)
410 0zd 11992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ∈ ℤ)
411100ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℤ)
412 elfzelz 12907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 𝑙 ∈ ℤ)
413412adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℤ)
414410, 411, 4133jca 1124 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑙 ∈ ℤ))
415 0red 10643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 0 ∈ ℝ)
416412zred 12086 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 𝑙 ∈ ℝ)
417 1red 10641 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑙 ∈ (1...(𝑗 − 1)) → 1 ∈ ℝ)
418384a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑙 ∈ (1...(𝑗 − 1)) → 0 < 1)
419 elfzle1 12909 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑙 ∈ (1...(𝑗 − 1)) → 1 ≤ 𝑙)
420415, 417, 416, 418, 419ltletrd 10799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 0 < 𝑙)
421415, 416, 420ltled 10787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...(𝑗 − 1)) → 0 ≤ 𝑙)
422421adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ≤ 𝑙)
423413zred 12086 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℝ)
424391ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℝ)
425393ad2antlr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 ∈ ℝ)
426416adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℝ)
427 peano2rem 10952 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 ∈ ℝ → (𝑗 − 1) ∈ ℝ)
428393, 427syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑗 ∈ (0..^𝑀) → (𝑗 − 1) ∈ ℝ)
429428adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑗 − 1) ∈ ℝ)
430393adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 ∈ ℝ)
431 elfzle2 12910 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑙 ∈ (1...(𝑗 − 1)) → 𝑙 ≤ (𝑗 − 1))
432431adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ≤ (𝑗 − 1))
433430ltm1d 11571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑗 − 1) < 𝑗)
434426, 429, 430, 432, 433lelttrd 10797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑗)
435434adantll 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑗)
436397ad2antlr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 < 𝑀)
437423, 425, 424, 435, 436lttrd 10800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑀)
438423, 424, 437ltled 10787 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ≤ 𝑀)
439414, 422, 438jca32 518 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑙 ∈ ℤ) ∧ (0 ≤ 𝑙 ∧ 𝑙 ≤ 𝑀)))
440 elfz2 12898 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑙 ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑙 ∈ ℤ) ∧ (0 ≤ 𝑙 ∧ 𝑙 ≤ 𝑀)))
441439, 440sylibr 236 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ (0...𝑀))
442409, 441ffvelrnd 6851 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄‘𝑙) ∈ ℝ)
443413peano2zd 12089 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ∈ ℤ)
444410, 411, 4433jca 1124 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑙 + 1) ∈ ℤ))
445416, 417readdcld 10669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) ∈ ℝ)
446416, 417, 420, 418addgt0d 11214 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 0 < (𝑙 + 1))
447415, 445, 446ltled 10787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...(𝑗 − 1)) → 0 ≤ (𝑙 + 1))
448447adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ≤ (𝑙 + 1))
449445adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ∈ ℝ)
450445recnd 10668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) ∈ ℂ)
451 1cnd 10635 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑙 ∈ (1...(𝑗 − 1)) → 1 ∈ ℂ)
452450, 451npcand 11000 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑙 ∈ (1...(𝑗 − 1)) → (((𝑙 + 1) − 1) + 1) = (𝑙 + 1))
453452eqcomd 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) = (((𝑙 + 1) − 1) + 1))
454453adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) = (((𝑙 + 1) − 1) + 1))
455 peano2re 10812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑙 ∈ ℝ → (𝑙 + 1) ∈ ℝ)
456 peano2rem 10952 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑙 + 1) ∈ ℝ → ((𝑙 + 1) − 1) ∈ ℝ)
457426, 455, 4563syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((𝑙 + 1) − 1) ∈ ℝ)
458 peano2re 10812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑗 − 1) ∈ ℝ → ((𝑗 − 1) + 1) ∈ ℝ)
459 peano2rem 10952 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑗 − 1) + 1) ∈ ℝ → (((𝑗 − 1) + 1) − 1) ∈ ℝ)
460429, 458, 4593syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (((𝑗 − 1) + 1) − 1) ∈ ℝ)
461 1red 10641 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 1 ∈ ℝ)
462 elfzel2 12905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑗 − 1) ∈ ℤ)
463462zred 12086 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑗 − 1) ∈ ℝ)
464463, 417readdcld 10669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑙 ∈ (1...(𝑗 − 1)) → ((𝑗 − 1) + 1) ∈ ℝ)
465416, 463, 417, 431leadd1dd 11253 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) ≤ ((𝑗 − 1) + 1))
466445, 464, 417, 465lesub1dd 11255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑙 ∈ (1...(𝑗 − 1)) → ((𝑙 + 1) − 1) ≤ (((𝑗 − 1) + 1) − 1))
467466adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((𝑙 + 1) − 1) ≤ (((𝑗 − 1) + 1) − 1))
468457, 460, 461, 467leadd1dd 11253 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (((𝑙 + 1) − 1) + 1) ≤ ((((𝑗 − 1) + 1) − 1) + 1))
469 peano2zm 12024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑗 ∈ ℤ → (𝑗 − 1) ∈ ℤ)
470364, 469syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑗 ∈ (0..^𝑀) → (𝑗 − 1) ∈ ℤ)
471470peano2zd 12089 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑗 ∈ (0..^𝑀) → ((𝑗 − 1) + 1) ∈ ℤ)
472471zcnd 12087 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ (0..^𝑀) → ((𝑗 − 1) + 1) ∈ ℂ)
473 1cnd 10635 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ (0..^𝑀) → 1 ∈ ℂ)
474472, 473npcand 11000 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 ∈ (0..^𝑀) → ((((𝑗 − 1) + 1) − 1) + 1) = ((𝑗 − 1) + 1))
475393recnd 10668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℂ)
476475, 473npcand 11000 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 ∈ (0..^𝑀) → ((𝑗 − 1) + 1) = 𝑗)
477474, 476eqtrd 2856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 ∈ (0..^𝑀) → ((((𝑗 − 1) + 1) − 1) + 1) = 𝑗)
478477adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((((𝑗 − 1) + 1) − 1) + 1) = 𝑗)
479468, 478breqtrd 5091 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (((𝑙 + 1) − 1) + 1) ≤ 𝑗)
480454, 479eqbrtrd 5087 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ≤ 𝑗)
481480adantll 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ≤ 𝑗)
482449, 425, 424, 481, 436lelttrd 10797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) < 𝑀)
483449, 424, 482ltled 10787 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ≤ 𝑀)
484444, 448, 483jca32 518 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑙 + 1) ∈ ℤ) ∧ (0 ≤ (𝑙 + 1) ∧ (𝑙 + 1) ≤ 𝑀)))
485 elfz2 12898 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑙 + 1) ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑙 + 1) ∈ ℤ) ∧ (0 ≤ (𝑙 + 1) ∧ (𝑙 + 1) ≤ 𝑀)))
486484, 485sylibr 236 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ∈ (0...𝑀))
487409, 486ffvelrnd 6851 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄‘(𝑙 + 1)) ∈ ℝ)
488 simpll 765 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝜑)
489 0zd 11992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ∈ ℤ)
490412adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℤ)
491421adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ≤ 𝑙)
492 eluz2 12248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (ℤ≥‘0) ↔ (0 ∈ ℤ ∧ 𝑙 ∈ ℤ ∧ 0 ≤ 𝑙))
493489, 490, 491, 492syl3anbrc 1339 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ (ℤ≥‘0))
494 elfzoel2 13036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0..^𝑀) → 𝑀 ∈ ℤ)
495494adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℤ)
496495zred 12086 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℝ)
497397adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 < 𝑀)
498426, 430, 496, 434, 497lttrd 10800 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑀)
499 elfzo2 13040 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (0..^𝑀) ↔ (𝑙 ∈ (ℤ≥‘0) ∧ 𝑀 ∈ ℤ ∧ 𝑙 < 𝑀))
500493, 495, 498, 499syl3anbrc 1339 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ (0..^𝑀))
501500adantll 712 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ (0..^𝑀))
502 eleq1 2900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 = 𝑙 → (𝑖 ∈ (0..^𝑀) ↔ 𝑙 ∈ (0..^𝑀)))
503502anbi2d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 = 𝑙 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 𝑙 ∈ (0..^𝑀))))
504 fveq2 6669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 = 𝑙 → (𝑄‘𝑖) = (𝑄‘𝑙))
505 oveq1 7162 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 = 𝑙 → (𝑖 + 1) = (𝑙 + 1))
506505fveq2d 6673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 = 𝑙 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑙 + 1)))
507504, 506breq12d 5078 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 = 𝑙 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘𝑙) < (𝑄‘(𝑙 + 1))))
508503, 507imbi12d 347 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 = 𝑙 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑙 ∈ (0..^𝑀)) → (𝑄‘𝑙) < (𝑄‘(𝑙 + 1)))))
509508, 152chvarvv 2001 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ 𝑙 ∈ (0..^𝑀)) → (𝑄‘𝑙) < (𝑄‘(𝑙 + 1)))
510488, 501, 509syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄‘𝑙) < (𝑄‘(𝑙 + 1)))
511442, 487, 510ltled 10787 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄‘𝑙) ≤ (𝑄‘(𝑙 + 1)))
512511adantlr 713 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄‘𝑙) ≤ (𝑄‘(𝑙 + 1)))
513378, 408, 512monoord 13399 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝑄‘1) ≤ (𝑄‘𝑗))
514356, 357, 361, 362, 513ltletrd 10799 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝐴 < (𝑄‘𝑗))
515356, 361ltnled 10786 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝐴 < (𝑄‘𝑗) ↔ ¬ (𝑄‘𝑗) ≤ 𝐴))
516514, 515mpbid 234 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → ¬ (𝑄‘𝑗) ≤ 𝐴)
517516ex 415 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (¬ 𝑗 ≤ 0 → ¬ (𝑄‘𝑗) ≤ 𝐴))
5185173adant3 1128 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → (¬ 𝑗 ≤ 0 → ¬ (𝑄‘𝑗) ≤ 𝐴))
519355, 518mt4d 117 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → 𝑗 ≤ 0)
520 elfzole1 13045 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0..^𝑀) → 0 ≤ 𝑗)
5215203ad2ant2 1130 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → 0 ≤ 𝑗)
5223933ad2ant2 1130 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → 𝑗 ∈ ℝ)
523 0red 10643 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → 0 ∈ ℝ)
524522, 523letri3d 10781 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → (𝑗 = 0 ↔ (𝑗 ≤ 0 ∧ 0 ≤ 𝑗)))
525519, 521, 524mpbir2and 711 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → 𝑗 = 0)
526347, 349, 354, 525syl3anc 1367 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}) → 𝑗 = 0)
527 velsn 4582 . . . . . . . . . . . . . . 15 (𝑗 ∈ {0} ↔ 𝑗 = 0)
528526, 527sylibr 236 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}) → 𝑗 ∈ {0})
529528ralrimiva 3182 . . . . . . . . . . . . 13 (𝜑 → ∀𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}𝑗 ∈ {0})
530 dfss3 3955 . . . . . . . . . . . . 13 ({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} ⊆ {0} ↔ ∀𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}𝑗 ∈ {0})
531529, 530sylibr 236 . . . . . . . . . . . 12 (𝜑 → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} ⊆ {0})
532157, 114eqeltrd 2913 . . . . . . . . . . . . . . 15 (𝜑 → (𝑄‘0) ∈ ℝ)
533532, 157eqled 10742 . . . . . . . . . . . . . 14 (𝜑 → (𝑄‘0) ≤ 𝐴)
534145breq1d 5075 . . . . . . . . . . . . . . 15 (𝑖 = 0 → ((𝑄‘𝑖) ≤ 𝐴 ↔ (𝑄‘0) ≤ 𝐴))
535534elrab 3679 . . . . . . . . . . . . . 14 (0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} ↔ (0 ∈ (0..^𝑀) ∧ (𝑄‘0) ≤ 𝐴))
536141, 533, 535sylanbrc 585 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴})
537536snssd 4741 . . . . . . . . . . . 12 (𝜑 → {0} ⊆ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴})
538531, 537eqssd 3983 . . . . . . . . . . 11 (𝜑 → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} = {0})
539538supeq1d 8909 . . . . . . . . . 10 (𝜑 → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}, ℝ, < ) = sup({0}, ℝ, < ))
540 supsn 8935 . . . . . . . . . . . 12 (( < Or ℝ ∧ 0 ∈ ℝ) → sup({0}, ℝ, < ) = 0)
54159, 142, 540mp2an 690 . . . . . . . . . . 11 sup({0}, ℝ, < ) = 0
542541a1i 11 . . . . . . . . . 10 (𝜑 → sup({0}, ℝ, < ) = 0)
543539, 542eqtrd 2856 . . . . . . . . 9 (𝜑 → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}, ℝ, < ) = 0)
544543ad2antrr 724 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}, ℝ, < ) = 0)
545334, 346, 5443eqtrd 2860 . . . . . . 7 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐼‘(𝑆‘𝑗)) = 0)
546545oveq1d 7170 . . . . . 6 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝐼‘(𝑆‘𝑗)) + 1) = (0 + 1))
547546fveq2d 6673 . . . . 5 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) = (𝑄‘(0 + 1)))
548547, 159syl6req 2873 . . . 4 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑄‘1) = (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
549330, 548breqtrd 5091 . . 3 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
55065adantr 483 . . . 4 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝜑 ∧ (𝑆‘𝑗) ∈ ℝ))
551 simplr 767 . . . 4 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝑗 ∈ (0..^𝑁))
55213a1i 11 . . . . . . . . . . 11 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)))
553 simpr 487 . . . . . . . . . . . . . . . 16 ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → 𝑦 = (𝐸‘(𝑆‘𝑗)))
554 neqne 3024 . . . . . . . . . . . . . . . . 17 (¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 → (𝐸‘(𝑆‘𝑗)) ≠ 𝐵)
555554adantr 483 . . . . . . . . . . . . . . . 16 ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → (𝐸‘(𝑆‘𝑗)) ≠ 𝐵)
556553, 555eqnetrd 3083 . . . . . . . . . . . . . . 15 ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → 𝑦 ≠ 𝐵)
557556neneqd 3021 . . . . . . . . . . . . . 14 ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → ¬ 𝑦 = 𝐵)
558557iffalsed 4477 . . . . . . . . . . . . 13 ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝑦)
559558, 553eqtrd 2856 . . . . . . . . . . . 12 ((¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = (𝐸‘(𝑆‘𝑗)))
560559adantll 712 . . . . . . . . . . 11 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = (𝐸‘(𝑆‘𝑗)))
561114, 218, 220, 11, 12fourierdlem4 42395 . . . . . . . . . . . . . 14 (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))
562561adantr 483 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐸:ℝ⟶(𝐴(,]𝐵))
563562, 42ffvelrnd 6851 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘𝑗)) ∈ (𝐴(,]𝐵))
564563adantr 483 . . . . . . . . . . 11 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) ∈ (𝐴(,]𝐵))
565552, 560, 564, 564fvmptd 6774 . . . . . . . . . 10 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐿‘(𝐸‘(𝑆‘𝑗))) = (𝐸‘(𝑆‘𝑗)))
566565eqcomd 2827 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) = (𝐿‘(𝐸‘(𝑆‘𝑗))))
567114, 218, 220, 13fourierdlem17 42408 . . . . . . . . . . . . 13 (𝜑 → 𝐿:(𝐴(,]𝐵)⟶(𝐴[,]𝐵))
568567adantr 483 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐿:(𝐴(,]𝐵)⟶(𝐴[,]𝐵))
569114, 218iccssred 41778 . . . . . . . . . . . . 13 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
570569adantr 483 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴[,]𝐵) ⊆ ℝ)
571568, 570fssd 6527 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐿:(𝐴(,]𝐵)⟶ℝ)
572571, 563ffvelrnd 6851 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐿‘(𝐸‘(𝑆‘𝑗))) ∈ ℝ)
573572adantr 483 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐿‘(𝐸‘(𝑆‘𝑗))) ∈ ℝ)
574566, 573eqeltrd 2913 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) ∈ ℝ)
575218ad2antrr 724 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐵 ∈ ℝ)
576245adantr 483 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ℝ*)
577218adantr 483 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐵 ∈ ℝ)
578 elioc2 12798 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐸‘(𝑆‘𝑗)) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘(𝑆‘𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆‘𝑗)) ∧ (𝐸‘(𝑆‘𝑗)) ≤ 𝐵)))
579576, 577, 578syl2anc 586 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘𝑗)) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘(𝑆‘𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆‘𝑗)) ∧ (𝐸‘(𝑆‘𝑗)) ≤ 𝐵)))
580563, 579mpbid 234 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆‘𝑗)) ∧ (𝐸‘(𝑆‘𝑗)) ≤ 𝐵))
581580simp3d 1140 . . . . . . . . 9 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘𝑗)) ≤ 𝐵)
582581adantr 483 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) ≤ 𝐵)
583554necomd 3071 . . . . . . . . 9 (¬ (𝐸‘(𝑆‘𝑗)) = 𝐵 → 𝐵 ≠ (𝐸‘(𝑆‘𝑗)))
584583adantl 484 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐵 ≠ (𝐸‘(𝑆‘𝑗)))
585574, 575, 582, 584leneltd 10793 . . . . . . 7 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) < 𝐵)
586585adantr 483 . . . . . 6 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆‘𝑗)) < 𝐵)
587 oveq1 7162 . . . . . . . . . . 11 ((𝐼‘(𝑆‘𝑗)) = (𝑀 − 1) → ((𝐼‘(𝑆‘𝑗)) + 1) = ((𝑀 − 1) + 1))
5882nncnd 11653 . . . . . . . . . . . 12 (𝜑 → 𝑀 ∈ ℂ)
589 1cnd 10635 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℂ)
590588, 589npcand 11000 . . . . . . . . . . 11 (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
591587, 590sylan9eqr 2878 . . . . . . . . . 10 ((𝜑 ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆‘𝑗)) + 1) = 𝑀)
592591fveq2d 6673 . . . . . . . . 9 ((𝜑 ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) = (𝑄‘𝑀))
593156simprd 498 . . . . . . . . . 10 (𝜑 → (𝑄‘𝑀) = 𝐵)
594593adantr 483 . . . . . . . . 9 ((𝜑 ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝑄‘𝑀) = 𝐵)
595592, 594eqtr2d 2857 . . . . . . . 8 ((𝜑 ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 𝐵 = (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
596595adantlr 713 . . . . . . 7 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 𝐵 = (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
597596adantlr 713 . . . . . 6 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 𝐵 = (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
598586, 597breqtrd 5091 . . . . 5 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
599566adantr 483 . . . . . 6 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆‘𝑗)) = (𝐿‘(𝐸‘(𝑆‘𝑗))))
600 ssrab2 4055 . . . . . . . . . . . . 13 {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ (0..^𝑀)
601 fzssz 12908 . . . . . . . . . . . . . . 15 (0...𝑀) ⊆ ℤ
60217, 601sstri 3975 . . . . . . . . . . . . . 14 (0..^𝑀) ⊆ ℤ
603 zssre 11987 . . . . . . . . . . . . . 14 ℤ ⊆ ℝ
604602, 603sstri 3975 . . . . . . . . . . . . 13 (0..^𝑀) ⊆ ℝ
605600, 604sstri 3975 . . . . . . . . . . . 12 {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ ℝ
606605a1i 11 . . . . . . . . . . 11 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ ℝ)
60756neeq1d 3075 . . . . . . . . . . . . . . 15 (𝑥 = (𝑆‘𝑗) → ({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ≠ ∅ ↔ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ≠ ∅))
60867, 607imbi12d 347 . . . . . . . . . . . . . 14 (𝑥 = (𝑆‘𝑗) → (((𝜑 ∧ 𝑥 ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ≠ ∅) ↔ ((𝜑 ∧ (𝑆‘𝑗) ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ≠ ∅)))
609141adantr 483 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ∈ (0..^𝑀))
610533ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝐸‘𝑥) = 𝐵) → (𝑄‘0) ≤ 𝐴)
611 iftrue 4472 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸‘𝑥) = 𝐵 → if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)) = 𝐴)
612611eqcomd 2827 . . . . . . . . . . . . . . . . . . . 20 ((𝐸‘𝑥) = 𝐵 → 𝐴 = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
613612adantl 484 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝐸‘𝑥) = 𝐵) → 𝐴 = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
614610, 613breqtrd 5091 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝐸‘𝑥) = 𝐵) → (𝑄‘0) ≤ if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
615532adantr 483 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) ∈ ℝ)
616114adantr 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ)
617616rexrd 10690 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ*)
618218adantr 483 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℝ)
619 iocssre 12815 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
620617, 618, 619syl2anc 586 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
621561ffvelrnda 6850 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐸‘𝑥) ∈ (𝐴(,]𝐵))
622620, 621sseldd 3967 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐸‘𝑥) ∈ ℝ)
623157adantr 483 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) = 𝐴)
624 elioc2 12798 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → ((𝐸‘𝑥) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘𝑥) ∈ ℝ ∧ 𝐴 < (𝐸‘𝑥) ∧ (𝐸‘𝑥) ≤ 𝐵)))
625617, 618, 624syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐸‘𝑥) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘𝑥) ∈ ℝ ∧ 𝐴 < (𝐸‘𝑥) ∧ (𝐸‘𝑥) ≤ 𝐵)))
626621, 625mpbid 234 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐸‘𝑥) ∈ ℝ ∧ 𝐴 < (𝐸‘𝑥) ∧ (𝐸‘𝑥) ≤ 𝐵))
627626simp2d 1139 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 < (𝐸‘𝑥))
628623, 627eqbrtrd 5087 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) < (𝐸‘𝑥))
629615, 622, 628ltled 10787 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) ≤ (𝐸‘𝑥))
630629adantr 483 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐸‘𝑥) = 𝐵) → (𝑄‘0) ≤ (𝐸‘𝑥))
631 iffalse 4475 . . . . . . . . . . . . . . . . . . . . 21 (¬ (𝐸‘𝑥) = 𝐵 → if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)) = (𝐸‘𝑥))
632631eqcomd 2827 . . . . . . . . . . . . . . . . . . . 20 (¬ (𝐸‘𝑥) = 𝐵 → (𝐸‘𝑥) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
633632adantl 484 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐸‘𝑥) = 𝐵) → (𝐸‘𝑥) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
634630, 633breqtrd 5091 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐸‘𝑥) = 𝐵) → (𝑄‘0) ≤ if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
635614, 634pm2.61dan 811 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) ≤ if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
63613a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)))
637 eqeq1 2825 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐸‘𝑥) → (𝑦 = 𝐵 ↔ (𝐸‘𝑥) = 𝐵))
638 id 22 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐸‘𝑥) → 𝑦 = (𝐸‘𝑥))
639637, 638ifbieq2d 4491 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝐸‘𝑥) → if(𝑦 = 𝐵, 𝐴, 𝑦) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
640639adantl 484 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 = (𝐸‘𝑥)) → if(𝑦 = 𝐵, 𝐴, 𝑦) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
641616, 622ifcld 4511 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)) ∈ ℝ)
642636, 640, 621, 641fvmptd 6774 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐿‘(𝐸‘𝑥)) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)))
643635, 642breqtrrd 5093 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) ≤ (𝐿‘(𝐸‘𝑥)))
644145breq1d 5075 . . . . . . . . . . . . . . . . 17 (𝑖 = 0 → ((𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥)) ↔ (𝑄‘0) ≤ (𝐿‘(𝐸‘𝑥))))
645644elrab 3679 . . . . . . . . . . . . . . . 16 (0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ↔ (0 ∈ (0..^𝑀) ∧ (𝑄‘0) ≤ (𝐿‘(𝐸‘𝑥))))
646609, 643, 645sylanbrc 585 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))})
647 ne0i 4299 . . . . . . . . . . . . . . 15 (0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ≠ ∅)
648646, 647syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑥 ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ≠ ∅)
649608, 648vtoclg 3567 . . . . . . . . . . . . 13 ((𝑆‘𝑗) ∈ ℝ → ((𝜑 ∧ (𝑆‘𝑗) ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ≠ ∅))
65042, 65, 649sylc 65 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ≠ ∅)
651650ad2antrr 724 . . . . . . . . . . 11 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ≠ ∅)
652605a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ ℝ)
653 fzofi 13341 . . . . . . . . . . . . . . 15 (0..^𝑀) ∈ Fin
654 ssfi 8737 . . . . . . . . . . . . . . 15 (((0..^𝑀) ∈ Fin ∧ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ (0..^𝑀)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ∈ Fin)
655653, 600, 654mp2an 690 . . . . . . . . . . . . . 14 {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ∈ Fin
656655a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ∈ Fin)
657 fimaxre2 11585 . . . . . . . . . . . . 13 (({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ ℝ ∧ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}𝑙 ≤ 𝑥)
658652, 656, 657syl2anc 586 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}𝑙 ≤ 𝑥)
659658ad2antrr 724 . . . . . . . . . . 11 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}𝑙 ≤ 𝑥)
660 0red 10643 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 ∈ ℝ)
661604, 47sseldi 3964 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) ∈ ℝ)
662 1red 10641 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 1 ∈ ℝ)
663661, 662readdcld 10669 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ ℝ)
664 elfzouz 13041 . . . . . . . . . . . . . . . . . 18 ((𝐼‘(𝑆‘𝑗)) ∈ (0..^𝑀) → (𝐼‘(𝑆‘𝑗)) ∈ (ℤ≥‘0))
665 eluzle 12255 . . . . . . . . . . . . . . . . . 18 ((𝐼‘(𝑆‘𝑗)) ∈ (ℤ≥‘0) → 0 ≤ (𝐼‘(𝑆‘𝑗)))
66647, 664, 6653syl 18 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 ≤ (𝐼‘(𝑆‘𝑗)))
667384a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 < 1)
668661, 662, 666, 667addgegt0d 11212 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 < ((𝐼‘(𝑆‘𝑗)) + 1))
669660, 663, 668ltled 10787 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 ≤ ((𝐼‘(𝑆‘𝑗)) + 1))
670669adantr 483 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 0 ≤ ((𝐼‘(𝑆‘𝑗)) + 1))
671661adantr 483 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐼‘(𝑆‘𝑗)) ∈ ℝ)
672 1red 10641 . . . . . . . . . . . . . . . . . 18 (𝜑 → 1 ∈ ℝ)
673391, 672resubcld 11067 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 − 1) ∈ ℝ)
674673ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝑀 − 1) ∈ ℝ)
675 1red 10641 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 1 ∈ ℝ)
676 elfzolt2 13046 . . . . . . . . . . . . . . . . . . . 20 ((𝐼‘(𝑆‘𝑗)) ∈ (0..^𝑀) → (𝐼‘(𝑆‘𝑗)) < 𝑀)
67747, 676syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) < 𝑀)
678601, 43sseldi 3964 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) ∈ ℤ)
679100adantr 483 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑀 ∈ ℤ)
680 zltlem1 12034 . . . . . . . . . . . . . . . . . . . 20 (((𝐼‘(𝑆‘𝑗)) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝐼‘(𝑆‘𝑗)) < 𝑀 ↔ (𝐼‘(𝑆‘𝑗)) ≤ (𝑀 − 1)))
681678, 679, 680syl2anc 586 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆‘𝑗)) < 𝑀 ↔ (𝐼‘(𝑆‘𝑗)) ≤ (𝑀 − 1)))
682677, 681mpbid 234 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) ≤ (𝑀 − 1))
683682adantr 483 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐼‘(𝑆‘𝑗)) ≤ (𝑀 − 1))
684 neqne 3024 . . . . . . . . . . . . . . . . . . 19 (¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1) → (𝐼‘(𝑆‘𝑗)) ≠ (𝑀 − 1))
685684necomd 3071 . . . . . . . . . . . . . . . . . 18 (¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1) → (𝑀 − 1) ≠ (𝐼‘(𝑆‘𝑗)))
686685adantl 484 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝑀 − 1) ≠ (𝐼‘(𝑆‘𝑗)))
687671, 674, 683, 686leneltd 10793 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐼‘(𝑆‘𝑗)) < (𝑀 − 1))
688671, 674, 675, 687ltadd1dd 11250 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆‘𝑗)) + 1) < ((𝑀 − 1) + 1))
689590ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝑀 − 1) + 1) = 𝑀)
690688, 689breqtrd 5091 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆‘𝑗)) + 1) < 𝑀)
691601, 49sseldi 3964 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ ℤ)
692691adantr 483 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ ℤ)
693 0zd 11992 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 0 ∈ ℤ)
694100ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 𝑀 ∈ ℤ)
695 elfzo 13039 . . . . . . . . . . . . . . 15 ((((𝐼‘(𝑆‘𝑗)) + 1) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0..^𝑀) ↔ (0 ≤ ((𝐼‘(𝑆‘𝑗)) + 1) ∧ ((𝐼‘(𝑆‘𝑗)) + 1) < 𝑀)))
696692, 693, 694, 695syl3anc 1367 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0..^𝑀) ↔ (0 ≤ ((𝐼‘(𝑆‘𝑗)) + 1) ∧ ((𝐼‘(𝑆‘𝑗)) + 1) < 𝑀)))
697670, 690, 696mpbir2and 711 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0..^𝑀))
698697adantr 483 . . . . . . . . . . . 12 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0..^𝑀))
699 simpr 487 . . . . . . . . . . . 12 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))))
700 fveq2 6669 . . . . . . . . . . . . . 14 (𝑖 = ((𝐼‘(𝑆‘𝑗)) + 1) → (𝑄‘𝑖) = (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
701700breq1d 5075 . . . . . . . . . . . . 13 (𝑖 = ((𝐼‘(𝑆‘𝑗)) + 1) → ((𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))) ↔ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))))
702701elrab 3679 . . . . . . . . . . . 12 (((𝐼‘(𝑆‘𝑗)) + 1) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ↔ (((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0..^𝑀) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))))
703698, 699, 702sylanbrc 585 . . . . . . . . . . 11 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))})
704 suprub 11601 . . . . . . . . . . 11 ((({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ ℝ ∧ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}𝑙 ≤ 𝑥) ∧ ((𝐼‘(𝑆‘𝑗)) + 1) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}) → ((𝐼‘(𝑆‘𝑗)) + 1) ≤ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ))
705606, 651, 659, 703, 704syl31anc 1369 . . . . . . . . . 10 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → ((𝐼‘(𝑆‘𝑗)) + 1) ≤ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ))
70662eqcomd 2827 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) = (𝐼‘(𝑆‘𝑗)))
707706ad2antrr 724 . . . . . . . . . 10 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) = (𝐼‘(𝑆‘𝑗)))
708705, 707breqtrd 5091 . . . . . . . . 9 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → ((𝐼‘(𝑆‘𝑗)) + 1) ≤ (𝐼‘(𝑆‘𝑗)))
709661ltp1d 11569 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) < ((𝐼‘(𝑆‘𝑗)) + 1))
710661, 663ltnled 10786 . . . . . . . . . . 11 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆‘𝑗)) < ((𝐼‘(𝑆‘𝑗)) + 1) ↔ ¬ ((𝐼‘(𝑆‘𝑗)) + 1) ≤ (𝐼‘(𝑆‘𝑗))))
711709, 710mpbid 234 . . . . . . . . . 10 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ¬ ((𝐼‘(𝑆‘𝑗)) + 1) ≤ (𝐼‘(𝑆‘𝑗)))
712711ad2antrr 724 . . . . . . . . 9 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → ¬ ((𝐼‘(𝑆‘𝑗)) + 1) ≤ (𝐼‘(𝑆‘𝑗)))
713708, 712pm2.65da 815 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ¬ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))))
714572adantr 483 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐿‘(𝐸‘(𝑆‘𝑗))) ∈ ℝ)
71550adantr 483 . . . . . . . . 9 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ∈ ℝ)
716714, 715ltnled 10786 . . . . . . . 8 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝐿‘(𝐸‘(𝑆‘𝑗))) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ↔ ¬ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))))
717713, 716mpbird 259 . . . . . . 7 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐿‘(𝐸‘(𝑆‘𝑗))) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
718717adantlr 713 . . . . . 6 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐿‘(𝐸‘(𝑆‘𝑗))) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
719599, 718eqbrtrd 5087 . . . . 5 ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
720598, 719pm2.61dan 811 . . . 4 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
72123ad2ant1 1129 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → 𝑀 ∈ ℕ)
72213ad2ant1 1129 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → 𝑄 ∈ (𝑃‘𝑀))
723213ad2ant1 1129 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → 𝐶 ∈ ℝ)
724223ad2ant1 1129 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → 𝐷 ∈ ℝ)
725233ad2ant1 1129 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → 𝐶 < 𝐷)
726493adant3 1128 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0...𝑀))
727 simp2 1133 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → 𝑗 ∈ (0..^𝑁))
72842leidd 11205 . . . . . . . 8 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ≤ (𝑆‘𝑗))
729 elico2 12799 . . . . . . . . 9 (((𝑆‘𝑗) ∈ ℝ ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ*) → ((𝑆‘𝑗) ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ ((𝑆‘𝑗) ∈ ℝ ∧ (𝑆‘𝑗) ≤ (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))))
73042, 212, 729syl2anc 586 . . . . . . . 8 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ ((𝑆‘𝑗) ∈ ℝ ∧ (𝑆‘𝑗) ≤ (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))))
73142, 728, 131, 730mpbir3and 1338 . . . . . . 7 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))))
7327313adant3 1128 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → (𝑆‘𝑗) ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))))
733 simp3 1134 . . . . . 6 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
734 eqid 2821 . . . . . 6 ((𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) − ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗))) = ((𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) − ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗)))
73511, 3, 721, 722, 723, 724, 725, 24, 25, 26, 27, 12, 726, 727, 732, 733, 734fourierdlem63 42453 . . . . 5 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
7367353adant1r 1173 . . . 4 (((𝜑 ∧ (𝑆‘𝑗) ∈ ℝ) ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
737550, 551, 720, 736syl3anc 1367 . . 3 (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
738549, 737pm2.61dan 811 . 2 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))
739 ioossioo 12828 . 2 ((((𝑄‘(𝐼‘(𝑆‘𝑗))) ∈ ℝ* ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ∈ ℝ*) ∧ ((𝑄‘(𝐼‘(𝑆‘𝑗))) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))) ∧ (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))) → ((𝐿‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))))
74045, 51, 89, 738, 739syl22anc 836 1 ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐿‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1533   ∈ wcel 2110   ≠ wne 3016  ∀wral 3138  ∃wrex 3139  {crab 3142  Vcvv 3494   ∪ cun 3933   ⊆ wss 3935  ∅c0 4290  ifcif 4466  {csn 4566  {cpr 4568   class class class wbr 5065   ↦ cmpt 5145   Or wor 5472  ran crn 5555  ℩cio 6311  ⟶wf 6350  ‘cfv 6354   Isom wiso 6355  (class class class)co 7155   ↑m cmap 8405  Fincfn 8508  supcsup 8903  ℂcc 10534  ℝcr 10535  0cc0 10536  1c1 10537   + caddc 10539   · cmul 10541  ℝ*cxr 10673   < clt 10674   ≤ cle 10675   − cmin 10869   / cdiv 11296  ℕcn 11637  2c2 11691  ℤcz 11980  ℤ≥cuz 12242  ℝ+crp 12388  (,)cioo 12737  (,]cioc 12738  [,)cico 12739  [,]cicc 12740  ...cfz 12891  ..^cfzo 13032  ⌊cfl 13159  ♯chash 13689
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-rep 5189  ax-sep 5202  ax-nul 5209  ax-pow 5265  ax-pr 5329  ax-un 7460  ax-inf2 9103  ax-cnex 10592  ax-resscn 10593  ax-1cn 10594  ax-icn 10595  ax-addcl 10596  ax-addrcl 10597  ax-mulcl 10598  ax-mulrcl 10599  ax-mulcom 10600  ax-addass 10601  ax-mulass 10602  ax-distr 10603  ax-i2m1 10604  ax-1ne0 10605  ax-1rid 10606  ax-rnegex 10607  ax-rrecex 10608  ax-cnre 10609  ax-pre-lttri 10610  ax-pre-lttrn 10611  ax-pre-ltadd 10612  ax-pre-mulgt0 10613  ax-pre-sup 10614
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4838  df-int 4876  df-iun 4920  df-iin 4921  df-br 5066  df-opab 5128  df-mpt 5146  df-tr 5172  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-se 5514  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-isom 6363  df-riota 7113  df-ov 7158  df-oprab 7159  df-mpo 7160  df-om 7580  df-1st 7688  df-2nd 7689  df-wrecs 7946  df-recs 8007  df-rdg 8045  df-1o 8101  df-oadd 8105  df-er 8288  df-map 8407  df-en 8509  df-dom 8510  df-sdom 8511  df-fin 8512  df-fi 8874  df-sup 8905  df-inf 8906  df-oi 8973  df-dju 9329  df-card 9367  df-pnf 10676  df-mnf 10677  df-xr 10678  df-ltxr 10679  df-le 10680  df-sub 10871  df-neg 10872  df-div 11297  df-nn 11638  df-2 11699  df-3 11700  df-n0 11897  df-xnn0 11967  df-z 11981  df-uz 12243  df-q 12348  df-rp 12389  df-xneg 12506  df-xadd 12507  df-xmul 12508  df-ioo 12741  df-ioc 12742  df-ico 12743  df-icc 12744  df-fz 12892  df-fzo 13033  df-fl 13161  df-seq 13369  df-exp 13429  df-hash 13690  df-cj 14457  df-re 14458  df-im 14459  df-sqrt 14593  df-abs 14594  df-rest 16695  df-topgen 16716  df-psmet 20536  df-xmet 20537  df-met 20538  df-bl 20539  df-mopn 20540  df-top 21501  df-topon 21518  df-bases 21553  df-cld 21626  df-ntr 21627  df-cls 21628  df-nei 21705  df-lp 21743  df-cmp 21994
This theorem is referenced by:  fourierdlem89  42479  fourierdlem90  42480  fourierdlem91  42481
  Copyright terms: Public domain W3C validator