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 45411
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 45335 . . . . . . . . 9 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
52, 4syl 17 . . . . . . . 8 (𝜑 → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
61, 5mpbid 231 . . . . . . 7 (𝜑 → (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
76simpld 494 . . . . . 6 (𝜑𝑄 ∈ (ℝ ↑m (0...𝑀)))
8 elmapi 8840 . . . . . 6 (𝑄 ∈ (ℝ ↑m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
97, 8syl 17 . . . . 5 (𝜑𝑄:(0...𝑀)⟶ℝ)
109adantr 480 . . . 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 45370 . . . . . . . 8 (𝜑 → (𝐼:ℝ⟶(0..^𝑀) ∧ (𝑥 ∈ ℝ → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))})))
1615simpld 494 . . . . . . 7 (𝜑𝐼:ℝ⟶(0..^𝑀))
17 fzossfz 13649 . . . . . . . 8 (0..^𝑀) ⊆ (0...𝑀)
1817a1i 11 . . . . . . 7 (𝜑 → (0..^𝑀) ⊆ (0...𝑀))
1916, 18fssd 6726 . . . . . 6 (𝜑𝐼:ℝ⟶(0...𝑀))
2019adantr 480 . . . . 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 45386 . . . . . . . . . . . 12 (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
2928simpld 494 . . . . . . . . . . 11 (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂𝑁)))
3029simprd 495 . . . . . . . . . 10 (𝜑𝑆 ∈ (𝑂𝑁))
3130adantr 480 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑆 ∈ (𝑂𝑁))
3229simpld 494 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℕ)
3332adantr 480 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑁 ∈ ℕ)
3424fourierdlem2 45335 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂𝑁) ↔ (𝑆 ∈ (ℝ ↑m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆𝑖) < (𝑆‘(𝑖 + 1))))))
3533, 34syl 17 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆 ∈ (𝑂𝑁) ↔ (𝑆 ∈ (ℝ ↑m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆𝑖) < (𝑆‘(𝑖 + 1))))))
3631, 35mpbid 231 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆 ∈ (ℝ ↑m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆𝑖) < (𝑆‘(𝑖 + 1)))))
3736simpld 494 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑆 ∈ (ℝ ↑m (0...𝑁)))
38 elmapi 8840 . . . . . . 7 (𝑆 ∈ (ℝ ↑m (0...𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
3937, 38syl 17 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
40 elfzofz 13646 . . . . . . 7 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ (0...𝑁))
4140adantl 481 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0...𝑁))
4239, 41ffvelcdmd 7078 . . . . 5 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ∈ ℝ)
4320, 42ffvelcdmd 7078 . . . 4 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆𝑗)) ∈ (0...𝑀))
4410, 43ffvelcdmd 7078 . . 3 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆𝑗))) ∈ ℝ)
4544rexrd 11262 . 2 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆𝑗))) ∈ ℝ*)
4616adantr 480 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐼:ℝ⟶(0..^𝑀))
4746, 42ffvelcdmd 7078 . . . . 5 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆𝑗)) ∈ (0..^𝑀))
48 fzofzp1 13727 . . . . 5 ((𝐼‘(𝑆𝑗)) ∈ (0..^𝑀) → ((𝐼‘(𝑆𝑗)) + 1) ∈ (0...𝑀))
4947, 48syl 17 . . . 4 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆𝑗)) + 1) ∈ (0...𝑀))
5010, 49ffvelcdmd 7078 . . 3 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ∈ ℝ)
5150rexrd 11262 . 2 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ∈ ℝ*)
5214a1i 11 . . . . 5 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < )))
53 fveq2 6882 . . . . . . . . . 10 (𝑥 = (𝑆𝑗) → (𝐸𝑥) = (𝐸‘(𝑆𝑗)))
5453fveq2d 6886 . . . . . . . . 9 (𝑥 = (𝑆𝑗) → (𝐿‘(𝐸𝑥)) = (𝐿‘(𝐸‘(𝑆𝑗))))
5554breq2d 5151 . . . . . . . 8 (𝑥 = (𝑆𝑗) → ((𝑄𝑖) ≤ (𝐿‘(𝐸𝑥)) ↔ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))))
5655rabbidv 3432 . . . . . . 7 (𝑥 = (𝑆𝑗) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))} = {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))})
5756supeq1d 9438 . . . . . 6 (𝑥 = (𝑆𝑗) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ))
5857adantl 481 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑥 = (𝑆𝑗)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ))
59 ltso 11292 . . . . . . 7 < Or ℝ
6059supex 9455 . . . . . 6 sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ V
6160a1i 11 . . . . 5 ((𝜑𝑗 ∈ (0..^𝑁)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ V)
6252, 58, 42, 61fvmptd 6996 . . . 4 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆𝑗)) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ))
6362fveq2d 6886 . . 3 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆𝑗))) = (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < )))
64 simpl 482 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝜑)
6564, 42jca 511 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝜑 ∧ (𝑆𝑗) ∈ ℝ))
66 eleq1 2813 . . . . . . . . 9 (𝑥 = (𝑆𝑗) → (𝑥 ∈ ℝ ↔ (𝑆𝑗) ∈ ℝ))
6766anbi2d 628 . . . . . . . 8 (𝑥 = (𝑆𝑗) → ((𝜑𝑥 ∈ ℝ) ↔ (𝜑 ∧ (𝑆𝑗) ∈ ℝ)))
6857, 56eleq12d 2819 . . . . . . . 8 (𝑥 = (𝑆𝑗) → (sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))} ↔ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}))
6967, 68imbi12d 344 . . . . . . 7 (𝑥 = (𝑆𝑗) → (((𝜑𝑥 ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}) ↔ ((𝜑 ∧ (𝑆𝑗) ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))})))
7015simprd 495 . . . . . . . 8 (𝜑 → (𝑥 ∈ ℝ → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}))
7170imp 406 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))})
7269, 71vtoclg 3535 . . . . . 6 ((𝑆𝑗) ∈ ℝ → ((𝜑 ∧ (𝑆𝑗) ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}))
7342, 65, 72sylc 65 . . . . 5 ((𝜑𝑗 ∈ (0..^𝑁)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))})
74 nfrab1 3443 . . . . . . 7 𝑖{𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}
75 nfcv 2895 . . . . . . 7 𝑖
76 nfcv 2895 . . . . . . 7 𝑖 <
7774, 75, 76nfsup 9443 . . . . . 6 𝑖sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < )
78 nfcv 2895 . . . . . 6 𝑖(0..^𝑀)
79 nfcv 2895 . . . . . . . 8 𝑖𝑄
8079, 77nffv 6892 . . . . . . 7 𝑖(𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ))
81 nfcv 2895 . . . . . . 7 𝑖
82 nfcv 2895 . . . . . . 7 𝑖(𝐿‘(𝐸‘(𝑆𝑗)))
8380, 81, 82nfbr 5186 . . . . . 6 𝑖(𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))
84 fveq2 6882 . . . . . . 7 (𝑖 = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) → (𝑄𝑖) = (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < )))
8584breq1d 5149 . . . . . 6 (𝑖 = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) → ((𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗))) ↔ (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))))
8677, 78, 83, 85elrabf 3672 . . . . 5 (sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ↔ (sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ (0..^𝑀) ∧ (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))))
8773, 86sylib 217 . . . 4 ((𝜑𝑗 ∈ (0..^𝑁)) → (sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ (0..^𝑀) ∧ (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))))
8887simprd 495 . . 3 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆𝑗))))
8963, 88eqbrtrd 5161 . 2 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆𝑗))) ≤ (𝐿‘(𝐸‘(𝑆𝑗))))
902ad2antrr 723 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝑀 ∈ ℕ)
911ad2antrr 723 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝑄 ∈ (𝑃𝑀))
9221ad2antrr 723 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐶 ∈ ℝ)
9322ad2antrr 723 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐷 ∈ ℝ)
9423ad2antrr 723 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐶 < 𝐷)
95 0zd 12568 . . . . . . 7 (𝜑 → 0 ∈ ℤ)
962nnzd 12583 . . . . . . 7 (𝜑𝑀 ∈ ℤ)
97 1zzd 12591 . . . . . . 7 (𝜑 → 1 ∈ ℤ)
98 0le1 11735 . . . . . . . 8 0 ≤ 1
9998a1i 11 . . . . . . 7 (𝜑 → 0 ≤ 1)
1002nnge1d 12258 . . . . . . 7 (𝜑 → 1 ≤ 𝑀)
10195, 96, 97, 99, 100elfzd 13490 . . . . . 6 (𝜑 → 1 ∈ (0...𝑀))
102101ad2antrr 723 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 1 ∈ (0...𝑀))
103 simplr 766 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝑗 ∈ (0..^𝑁))
104 fourierdlem79.z . . . . . . . 8 𝑍 = ((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)))
105 fzofzp1 13727 . . . . . . . . . . . . . 14 (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ (0...𝑁))
106105adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈ (0...𝑁))
10739, 106ffvelcdmd 7078 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
108107, 42resubcld 11640 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) ∈ ℝ)
109108rehalfcld 12457 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2) ∈ ℝ)
1109, 101ffvelcdmd 7078 . . . . . . . . . . . . 13 (𝜑 → (𝑄‘1) ∈ ℝ)
1113, 2, 1fourierdlem11 45344 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
112111simp1d 1139 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℝ)
113110, 112resubcld 11640 . . . . . . . . . . . 12 (𝜑 → ((𝑄‘1) − 𝐴) ∈ ℝ)
114113rehalfcld 12457 . . . . . . . . . . 11 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ)
115114adantr 480 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ)
116109, 115ifcld 4567 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ∈ ℝ)
11742, 116readdcld 11241 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) ∈ ℝ)
118104, 117eqeltrid 2829 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑍 ∈ ℝ)
119 2re 12284 . . . . . . . . . . . . . 14 2 ∈ ℝ
120119a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → 2 ∈ ℝ)
121 elfzoelz 13630 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℤ)
122121zred 12664 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℝ)
123122ltp1d 12142 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0..^𝑁) → 𝑗 < (𝑗 + 1))
124123adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑗 < (𝑗 + 1))
12528simprd 495 . . . . . . . . . . . . . . . . 17 (𝜑𝑆 Isom < , < ((0...𝑁), 𝐻))
126125adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑆 Isom < , < ((0...𝑁), 𝐻))
127 isorel 7316 . . . . . . . . . . . . . . . 16 ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝑗 + 1) ∈ (0...𝑁))) → (𝑗 < (𝑗 + 1) ↔ (𝑆𝑗) < (𝑆‘(𝑗 + 1))))
128126, 41, 106, 127syl12anc 834 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑗 < (𝑗 + 1) ↔ (𝑆𝑗) < (𝑆‘(𝑗 + 1))))
129124, 128mpbid 231 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) < (𝑆‘(𝑗 + 1)))
13042, 107posdifd 11799 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) < (𝑆‘(𝑗 + 1)) ↔ 0 < ((𝑆‘(𝑗 + 1)) − (𝑆𝑗))))
131129, 130mpbid 231 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → 0 < ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)))
132 2pos 12313 . . . . . . . . . . . . . 14 0 < 2
133132a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → 0 < 2)
134108, 120, 131, 133divgt0d 12147 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → 0 < (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
135109, 134elrpd 13011 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2) ∈ ℝ+)
136119a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 2 ∈ ℝ)
1372nngt0d 12259 . . . . . . . . . . . . . . . . . 18 (𝜑 → 0 < 𝑀)
138 fzolb 13636 . . . . . . . . . . . . . . . . . 18 (0 ∈ (0..^𝑀) ↔ (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
13995, 96, 137, 138syl3anbrc 1340 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ∈ (0..^𝑀))
140 0re 11214 . . . . . . . . . . . . . . . . . 18 0 ∈ ℝ
141 eleq1 2813 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 0 → (𝑖 ∈ (0..^𝑀) ↔ 0 ∈ (0..^𝑀)))
142141anbi2d 628 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 0 → ((𝜑𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 0 ∈ (0..^𝑀))))
143 fveq2 6882 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 0 → (𝑄𝑖) = (𝑄‘0))
144 oveq1 7409 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 0 → (𝑖 + 1) = (0 + 1))
145144fveq2d 6886 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 0 → (𝑄‘(𝑖 + 1)) = (𝑄‘(0 + 1)))
146143, 145breq12d 5152 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 0 → ((𝑄𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘0) < (𝑄‘(0 + 1))))
147142, 146imbi12d 344 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 0 → (((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))))
1486simprd 495 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))
149148simprd 495 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))
150149r19.21bi 3240 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
151147, 150vtoclg 3535 . . . . . . . . . . . . . . . . . 18 (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1))))
152140, 151ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))
153139, 152mpdan 684 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘0) < (𝑄‘(0 + 1)))
154148simpld 494 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵))
155154simpld 494 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘0) = 𝐴)
156 0p1e1 12332 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
157156fveq2i 6885 . . . . . . . . . . . . . . . . 17 (𝑄‘(0 + 1)) = (𝑄‘1)
158157a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘(0 + 1)) = (𝑄‘1))
159153, 155, 1583brtr3d 5170 . . . . . . . . . . . . . . 15 (𝜑𝐴 < (𝑄‘1))
160112, 110posdifd 11799 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 < (𝑄‘1) ↔ 0 < ((𝑄‘1) − 𝐴)))
161159, 160mpbid 231 . . . . . . . . . . . . . 14 (𝜑 → 0 < ((𝑄‘1) − 𝐴))
162132a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 0 < 2)
163113, 136, 161, 162divgt0d 12147 . . . . . . . . . . . . 13 (𝜑 → 0 < (((𝑄‘1) − 𝐴) / 2))
164114, 163elrpd 13011 . . . . . . . . . . . 12 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ+)
165164adantr 480 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ+)
166135, 165ifcld 4567 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ∈ ℝ+)
16742, 166ltaddrpd 13047 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) < ((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
16842, 117, 167ltled 11360 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ≤ ((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
169168, 104breqtrrdi 5181 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ≤ 𝑍)
17042, 109readdcld 11241 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) ∈ ℝ)
171 iftrue 4527 . . . . . . . . . . . . 13 (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
172171adantl 481 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
173109leidd 11778 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
174173adantr 480 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
175172, 174eqbrtrd 5161 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
176 iffalse 4530 . . . . . . . . . . . . 13 (¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) − 𝐴) / 2))
177176adantl 481 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) − 𝐴) / 2))
178113ad2antrr 723 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑄‘1) − 𝐴) ∈ ℝ)
179108adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) ∈ ℝ)
180 2rp 12977 . . . . . . . . . . . . . 14 2 ∈ ℝ+
181180a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → 2 ∈ ℝ+)
182 simpr 484 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴))
183178, 179, 182nltled 11362 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑄‘1) − 𝐴) ≤ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)))
184178, 179, 181, 183lediv1dd 13072 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑄‘1) − 𝐴) / 2) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
185177, 184eqbrtrd 5161 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
186175, 185pm2.61dan 810 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
187116, 109, 42, 186leadd2dd 11827 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) ≤ ((𝑆𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)))
18842recnd 11240 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ∈ ℂ)
189107recnd 11240 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℂ)
190188, 189addcomd 11414 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + (𝑆‘(𝑗 + 1))) = ((𝑆‘(𝑗 + 1)) + (𝑆𝑗)))
191190oveq1d 7417 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) = (((𝑆‘(𝑗 + 1)) + (𝑆𝑗)) / 2))
192191oveq1d 7417 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → ((((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = ((((𝑆‘(𝑗 + 1)) + (𝑆𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)))
193 halfaddsub 12443 . . . . . . . . . . . . . . 15 (((𝑆‘(𝑗 + 1)) ∈ ℂ ∧ (𝑆𝑗) ∈ ℂ) → (((((𝑆‘(𝑗 + 1)) + (𝑆𝑗)) / 2) + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = (𝑆‘(𝑗 + 1)) ∧ ((((𝑆‘(𝑗 + 1)) + (𝑆𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = (𝑆𝑗)))
194189, 188, 193syl2anc 583 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → (((((𝑆‘(𝑗 + 1)) + (𝑆𝑗)) / 2) + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = (𝑆‘(𝑗 + 1)) ∧ ((((𝑆‘(𝑗 + 1)) + (𝑆𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = (𝑆𝑗)))
195194simprd 495 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → ((((𝑆‘(𝑗 + 1)) + (𝑆𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = (𝑆𝑗))
196192, 195eqtrd 2764 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → ((((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = (𝑆𝑗))
197188, 189addcld 11231 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + (𝑆‘(𝑗 + 1))) ∈ ℂ)
198197halfcld 12455 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) ∈ ℂ)
199109recnd 11240 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2) ∈ ℂ)
200198, 199, 188subsub23d 44507 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → (((((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = (𝑆𝑗) ↔ ((((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (𝑆𝑗)) = (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)))
201196, 200mpbid 231 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → ((((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (𝑆𝑗)) = (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
202198, 188, 199subaddd 11587 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → (((((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (𝑆𝑗)) = (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2) ↔ ((𝑆𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = (((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2)))
203201, 202mpbid 231 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = (((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2))
204 avglt2 12449 . . . . . . . . . . . 12 (((𝑆𝑗) ∈ ℝ ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ) → ((𝑆𝑗) < (𝑆‘(𝑗 + 1)) ↔ (((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) < (𝑆‘(𝑗 + 1))))
20542, 107, 204syl2anc 583 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) < (𝑆‘(𝑗 + 1)) ↔ (((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) < (𝑆‘(𝑗 + 1))))
206129, 205mpbid 231 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) < (𝑆‘(𝑗 + 1)))
207203, 206eqbrtrd 5161 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) < (𝑆‘(𝑗 + 1)))
208117, 170, 107, 187, 207lelttrd 11370 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑆‘(𝑗 + 1)))
209104, 208eqbrtrid 5174 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑍 < (𝑆‘(𝑗 + 1)))
210107rexrd 11262 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℝ*)
211 elico2 13386 . . . . . . . 8 (((𝑆𝑗) ∈ ℝ ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ*) → (𝑍 ∈ ((𝑆𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ (𝑍 ∈ ℝ ∧ (𝑆𝑗) ≤ 𝑍𝑍 < (𝑆‘(𝑗 + 1)))))
21242, 210, 211syl2anc 583 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑍 ∈ ((𝑆𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ (𝑍 ∈ ℝ ∧ (𝑆𝑗) ≤ 𝑍𝑍 < (𝑆‘(𝑗 + 1)))))
213118, 169, 209, 212mpbir3and 1339 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑍 ∈ ((𝑆𝑗)[,)(𝑆‘(𝑗 + 1))))
214213adantr 480 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝑍 ∈ ((𝑆𝑗)[,)(𝑆‘(𝑗 + 1))))
215112ad2antrr 723 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐴 ∈ ℝ)
216111simp2d 1140 . . . . . . . . 9 (𝜑𝐵 ∈ ℝ)
217216ad2antrr 723 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐵 ∈ ℝ)
218111simp3d 1141 . . . . . . . . 9 (𝜑𝐴 < 𝐵)
219218ad2antrr 723 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐴 < 𝐵)
22042adantr 480 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝑆𝑗) ∈ ℝ)
221 simpr 484 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) = 𝐵)
222167, 104breqtrrdi 5181 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) < 𝑍)
223216, 112resubcld 11640 . . . . . . . . . . . . . 14 (𝜑 → (𝐵𝐴) ∈ ℝ)
22411, 223eqeltrid 2829 . . . . . . . . . . . . 13 (𝜑𝑇 ∈ ℝ)
225224adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑇 ∈ ℝ)
226109adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2) ∈ ℝ)
227114ad2antrr 723 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ)
228108adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) ∈ ℝ)
229113ad2antrr 723 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑄‘1) − 𝐴) ∈ ℝ)
230180a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → 2 ∈ ℝ+)
231 simpr 484 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴))
232228, 229, 230, 231ltdiv1dd 13071 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2) < (((𝑄‘1) − 𝐴) / 2))
233226, 227, 232ltled 11360 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2) ≤ (((𝑄‘1) − 𝐴) / 2))
234172, 233eqbrtrd 5161 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2))
235176adantl 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) − 𝐴) / 2))
236114leidd 11778 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ≤ (((𝑄‘1) − 𝐴) / 2))
237236adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑄‘1) − 𝐴) / 2) ≤ (((𝑄‘1) − 𝐴) / 2))
238235, 237eqbrtrd 5161 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2))
239238adantlr 712 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2))
240234, 239pm2.61dan 810 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2))
241223rehalfcld 12457 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵𝐴) / 2) ∈ ℝ)
242180a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 2 ∈ ℝ+)
243112rexrd 11262 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ ℝ*)
244216rexrd 11262 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ∈ ℝ*)
2453, 2, 1fourierdlem15 45348 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
246245, 101ffvelcdmd 7078 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑄‘1) ∈ (𝐴[,]𝐵))
247 iccleub 13377 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝑄‘1) ∈ (𝐴[,]𝐵)) → (𝑄‘1) ≤ 𝐵)
248243, 244, 246, 247syl3anc 1368 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑄‘1) ≤ 𝐵)
249110, 216, 112, 248lesub1dd 11828 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑄‘1) − 𝐴) ≤ (𝐵𝐴))
250113, 223, 242, 249lediv1dd 13072 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ≤ ((𝐵𝐴) / 2))
25111eqcomi 2733 . . . . . . . . . . . . . . . . . 18 (𝐵𝐴) = 𝑇
252251oveq1i 7412 . . . . . . . . . . . . . . . . 17 ((𝐵𝐴) / 2) = (𝑇 / 2)
253112, 216posdifd 11799 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
254218, 253mpbid 231 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 < (𝐵𝐴))
255254, 11breqtrrdi 5181 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 < 𝑇)
256224, 255elrpd 13011 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 ∈ ℝ+)
257 rphalflt 13001 . . . . . . . . . . . . . . . . . 18 (𝑇 ∈ ℝ+ → (𝑇 / 2) < 𝑇)
258256, 257syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑇 / 2) < 𝑇)
259252, 258eqbrtrid 5174 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵𝐴) / 2) < 𝑇)
260114, 241, 224, 250, 259lelttrd 11370 . . . . . . . . . . . . . . 15 (𝜑 → (((𝑄‘1) − 𝐴) / 2) < 𝑇)
261114, 224, 260ltled 11360 . . . . . . . . . . . . . 14 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ≤ 𝑇)
262261adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑄‘1) − 𝐴) / 2) ≤ 𝑇)
263116, 115, 225, 240, 262letrd 11369 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ 𝑇)
264116, 225, 42, 263leadd2dd 11827 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) ≤ ((𝑆𝑗) + 𝑇))
265104, 264eqbrtrid 5174 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑍 ≤ ((𝑆𝑗) + 𝑇))
26642rexrd 11262 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ∈ ℝ*)
26742, 225readdcld 11241 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + 𝑇) ∈ ℝ)
268 elioc2 13385 . . . . . . . . . . 11 (((𝑆𝑗) ∈ ℝ* ∧ ((𝑆𝑗) + 𝑇) ∈ ℝ) → (𝑍 ∈ ((𝑆𝑗)(,]((𝑆𝑗) + 𝑇)) ↔ (𝑍 ∈ ℝ ∧ (𝑆𝑗) < 𝑍𝑍 ≤ ((𝑆𝑗) + 𝑇))))
269266, 267, 268syl2anc 583 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑍 ∈ ((𝑆𝑗)(,]((𝑆𝑗) + 𝑇)) ↔ (𝑍 ∈ ℝ ∧ (𝑆𝑗) < 𝑍𝑍 ≤ ((𝑆𝑗) + 𝑇))))
270118, 222, 265, 269mpbir3and 1339 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑍 ∈ ((𝑆𝑗)(,]((𝑆𝑗) + 𝑇)))
271270adantr 480 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝑍 ∈ ((𝑆𝑗)(,]((𝑆𝑗) + 𝑇)))
272215, 217, 219, 11, 12, 220, 221, 271fourierdlem26 45359 . . . . . . 7 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸𝑍) = (𝐴 + (𝑍 − (𝑆𝑗))))
273104a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑍 = ((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
274273oveq1d 7417 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑍 − (𝑆𝑗)) = (((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆𝑗)))
275274oveq2d 7418 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐴 + (𝑍 − (𝑆𝑗))) = (𝐴 + (((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆𝑗))))
276275adantr 480 . . . . . . 7 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐴 + (𝑍 − (𝑆𝑗))) = (𝐴 + (((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆𝑗))))
277116recnd 11240 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ∈ ℂ)
278188, 277pncan2d 11571 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆𝑗)) = if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)))
279278oveq2d 7418 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐴 + (((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆𝑗))) = (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
280279adantr 480 . . . . . . 7 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐴 + (((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆𝑗))) = (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
281272, 276, 2803eqtrd 2768 . . . . . 6 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸𝑍) = (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
282171oveq2d 7418 . . . . . . . . . 10 (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)))
283282adantl 481 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)))
284112adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ℝ)
285284, 109readdcld 11241 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) ∈ ℝ)
286285adantr 480 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) ∈ ℝ)
287284, 115readdcld 11241 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) ∈ ℝ)
288287adantr 480 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) ∈ ℝ)
289110ad2antrr 723 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝑄‘1) ∈ ℝ)
290112ad2antrr 723 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → 𝐴 ∈ ℝ)
291226, 227, 290, 232ltadd2dd 11371 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) < (𝐴 + (((𝑄‘1) − 𝐴) / 2)))
292110recnd 11240 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘1) ∈ ℂ)
293112recnd 11240 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ ℂ)
294 halfaddsub 12443 . . . . . . . . . . . . . . . 16 (((𝑄‘1) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((((𝑄‘1) + 𝐴) / 2) + (((𝑄‘1) − 𝐴) / 2)) = (𝑄‘1) ∧ ((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) = 𝐴))
295292, 293, 294syl2anc 583 . . . . . . . . . . . . . . 15 (𝜑 → (((((𝑄‘1) + 𝐴) / 2) + (((𝑄‘1) − 𝐴) / 2)) = (𝑄‘1) ∧ ((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) = 𝐴))
296295simprd 495 . . . . . . . . . . . . . 14 (𝜑 → ((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) = 𝐴)
297296oveq1d 7417 . . . . . . . . . . . . 13 (𝜑 → (((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) + (((𝑄‘1) − 𝐴) / 2)) = (𝐴 + (((𝑄‘1) − 𝐴) / 2)))
298110, 112readdcld 11241 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑄‘1) + 𝐴) ∈ ℝ)
299298rehalfcld 12457 . . . . . . . . . . . . . . 15 (𝜑 → (((𝑄‘1) + 𝐴) / 2) ∈ ℝ)
300299recnd 11240 . . . . . . . . . . . . . 14 (𝜑 → (((𝑄‘1) + 𝐴) / 2) ∈ ℂ)
301114recnd 11240 . . . . . . . . . . . . . 14 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ∈ ℂ)
302300, 301npcand 11573 . . . . . . . . . . . . 13 (𝜑 → (((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) + (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) + 𝐴) / 2))
303297, 302eqtr3d 2766 . . . . . . . . . . . 12 (𝜑 → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) + 𝐴) / 2))
304110, 110readdcld 11241 . . . . . . . . . . . . . 14 (𝜑 → ((𝑄‘1) + (𝑄‘1)) ∈ ℝ)
305112, 110, 110, 159ltadd2dd 11371 . . . . . . . . . . . . . 14 (𝜑 → ((𝑄‘1) + 𝐴) < ((𝑄‘1) + (𝑄‘1)))
306298, 304, 242, 305ltdiv1dd 13071 . . . . . . . . . . . . 13 (𝜑 → (((𝑄‘1) + 𝐴) / 2) < (((𝑄‘1) + (𝑄‘1)) / 2))
3072922timesd 12453 . . . . . . . . . . . . . . . 16 (𝜑 → (2 · (𝑄‘1)) = ((𝑄‘1) + (𝑄‘1)))
308307eqcomd 2730 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑄‘1) + (𝑄‘1)) = (2 · (𝑄‘1)))
309308oveq1d 7417 . . . . . . . . . . . . . 14 (𝜑 → (((𝑄‘1) + (𝑄‘1)) / 2) = ((2 · (𝑄‘1)) / 2))
310 2cnd 12288 . . . . . . . . . . . . . . 15 (𝜑 → 2 ∈ ℂ)
311 2ne0 12314 . . . . . . . . . . . . . . . 16 2 ≠ 0
312311a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 2 ≠ 0)
313292, 310, 312divcan3d 11993 . . . . . . . . . . . . . 14 (𝜑 → ((2 · (𝑄‘1)) / 2) = (𝑄‘1))
314309, 313eqtrd 2764 . . . . . . . . . . . . 13 (𝜑 → (((𝑄‘1) + (𝑄‘1)) / 2) = (𝑄‘1))
315306, 314breqtrd 5165 . . . . . . . . . . . 12 (𝜑 → (((𝑄‘1) + 𝐴) / 2) < (𝑄‘1))
316303, 315eqbrtrd 5161 . . . . . . . . . . 11 (𝜑 → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) < (𝑄‘1))
317316ad2antrr 723 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) < (𝑄‘1))
318286, 288, 289, 291, 317lttrd 11373 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) < (𝑄‘1))
319283, 318eqbrtrd 5161 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1))
320176oveq2d 7418 . . . . . . . . . 10 (¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑄‘1) − 𝐴) / 2)))
321320adantl 481 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑄‘1) − 𝐴) / 2)))
322316ad2antrr 723 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) < (𝑄‘1))
323321, 322eqbrtrd 5161 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1))
324319, 323pm2.61dan 810 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1))
325324adantr 480 . . . . . 6 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1))
326281, 325eqbrtrd 5161 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸𝑍) < (𝑄‘1))
327 eqid 2724 . . . . 5 ((𝑄‘1) − ((𝐸𝑍) − 𝑍)) = ((𝑄‘1) − ((𝐸𝑍) − 𝑍))
32811, 3, 90, 91, 92, 93, 94, 24, 25, 26, 27, 12, 102, 103, 214, 326, 327fourierdlem63 45395 . . . 4 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘1))
32914a1i 11 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < )))
33057adantl 481 . . . . . . . . 9 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ 𝑥 = (𝑆𝑗)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ))
33160a1i 11 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ V)
332329, 330, 220, 331fvmptd 6996 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐼‘(𝑆𝑗)) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ))
333 fveq2 6882 . . . . . . . . . . . . 13 ((𝐸‘(𝑆𝑗)) = 𝐵 → (𝐿‘(𝐸‘(𝑆𝑗))) = (𝐿𝐵))
33413a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)))
335 iftrue 4527 . . . . . . . . . . . . . . 15 (𝑦 = 𝐵 → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝐴)
336335adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑦 = 𝐵) → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝐴)
337 ubioc1 13375 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵) → 𝐵 ∈ (𝐴(,]𝐵))
338243, 244, 218, 337syl3anc 1368 . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ (𝐴(,]𝐵))
339334, 336, 338, 112fvmptd 6996 . . . . . . . . . . . . 13 (𝜑 → (𝐿𝐵) = 𝐴)
340333, 339sylan9eqr 2786 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐿‘(𝐸‘(𝑆𝑗))) = 𝐴)
341340breq2d 5151 . . . . . . . . . . 11 ((𝜑 ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → ((𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗))) ↔ (𝑄𝑖) ≤ 𝐴))
342341rabbidv 3432 . . . . . . . . . 10 ((𝜑 ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} = {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴})
343342supeq1d 9438 . . . . . . . . 9 ((𝜑 ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}, ℝ, < ))
344343adantlr 712 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}, ℝ, < ))
345 simpl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}) → 𝜑)
346 elrabi 3670 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴} → 𝑗 ∈ (0..^𝑀))
347346adantl 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}) → 𝑗 ∈ (0..^𝑀))
348 fveq2 6882 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑗 → (𝑄𝑖) = (𝑄𝑗))
349348breq1d 5149 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → ((𝑄𝑖) ≤ 𝐴 ↔ (𝑄𝑗) ≤ 𝐴))
350349elrab 3676 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴} ↔ (𝑗 ∈ (0..^𝑀) ∧ (𝑄𝑗) ≤ 𝐴))
351350simprbi 496 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴} → (𝑄𝑗) ≤ 𝐴)
352351adantl 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}) → (𝑄𝑗) ≤ 𝐴)
353 simp3 1135 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑀) ∧ (𝑄𝑗) ≤ 𝐴) → (𝑄𝑗) ≤ 𝐴)
354112ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝐴 ∈ ℝ)
355110ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝑄‘1) ∈ ℝ)
3569adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
35718sselda 3975 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0..^𝑀)) → 𝑗 ∈ (0...𝑀))
358356, 357ffvelcdmd 7078 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑄𝑗) ∈ ℝ)
359358adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝑄𝑗) ∈ ℝ)
360159ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝐴 < (𝑄‘1))
361 1zzd 12591 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 1 ∈ ℤ)
362 elfzoelz 13630 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℤ)
363362ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝑗 ∈ ℤ)
364 1e0p1 12717 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 = (0 + 1)
365 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → ¬ 𝑗 ≤ 0)
366 0red 11215 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 0 ∈ ℝ)
367363zred 12664 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝑗 ∈ ℝ)
368366, 367ltnled 11359 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (0 < 𝑗 ↔ ¬ 𝑗 ≤ 0))
369365, 368mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 0 < 𝑗)
370 0zd 12568 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 0 ∈ ℤ)
371 zltp1le 12610 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((0 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (0 < 𝑗 ↔ (0 + 1) ≤ 𝑗))
372370, 363, 371syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (0 < 𝑗 ↔ (0 + 1) ≤ 𝑗))
373369, 372mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (0 + 1) ≤ 𝑗)
374364, 373eqbrtrid 5174 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 1 ≤ 𝑗)
375 eluz2 12826 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (ℤ‘1) ↔ (1 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 1 ≤ 𝑗))
376361, 363, 374, 375syl3anbrc 1340 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝑗 ∈ (ℤ‘1))
3779ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑄:(0...𝑀)⟶ℝ)
378 0zd 12568 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 0 ∈ ℤ)
37996ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑀 ∈ ℤ)
380 elfzelz 13499 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑙 ∈ (1...𝑗) → 𝑙 ∈ ℤ)
381380adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ∈ ℤ)
382 0red 11215 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (1...𝑗) → 0 ∈ ℝ)
383380zred 12664 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (1...𝑗) → 𝑙 ∈ ℝ)
384 1red 11213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 1 ∈ ℝ)
385 0lt1 11734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 0 < 1
386385a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 0 < 1)
387 elfzle1 13502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 1 ≤ 𝑙)
388382, 384, 383, 386, 387ltletrd 11372 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (1...𝑗) → 0 < 𝑙)
389382, 383, 388ltled 11360 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑙 ∈ (1...𝑗) → 0 ≤ 𝑙)
390389adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 0 ≤ 𝑙)
391383adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ∈ ℝ)
39296zred 12664 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑀 ∈ ℝ)
393392ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑀 ∈ ℝ)
394362zred 12664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℝ)
395394ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑗 ∈ ℝ)
396 elfzle2 13503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 𝑙𝑗)
397396adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙𝑗)
398 elfzolt2 13639 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0..^𝑀) → 𝑗 < 𝑀)
399398ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑗 < 𝑀)
400391, 395, 393, 397, 399lelttrd 11370 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 < 𝑀)
401391, 393, 400ltled 11360 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙𝑀)
402378, 379, 381, 390, 401elfzd 13490 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ∈ (0...𝑀))
403377, 402ffvelcdmd 7078 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → (𝑄𝑙) ∈ ℝ)
404403adantlr 712 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) ∧ 𝑙 ∈ (1...𝑗)) → (𝑄𝑙) ∈ ℝ)
4059ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑄:(0...𝑀)⟶ℝ)
406 0zd 12568 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ∈ ℤ)
40796ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℤ)
408 elfzelz 13499 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (1...(𝑗 − 1)) → 𝑙 ∈ ℤ)
409408adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℤ)
410 0red 11215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...(𝑗 − 1)) → 0 ∈ ℝ)
411408zred 12664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...(𝑗 − 1)) → 𝑙 ∈ ℝ)
412 1red 11213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 1 ∈ ℝ)
413385a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 0 < 1)
414 elfzle1 13502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 1 ≤ 𝑙)
415410, 412, 411, 413, 414ltletrd 11372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...(𝑗 − 1)) → 0 < 𝑙)
416410, 411, 415ltled 11360 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (1...(𝑗 − 1)) → 0 ≤ 𝑙)
417416adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ≤ 𝑙)
418409zred 12664 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℝ)
419392ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℝ)
420394ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 ∈ ℝ)
421411adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℝ)
422 peano2rem 11525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑗 ∈ ℝ → (𝑗 − 1) ∈ ℝ)
423394, 422syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 ∈ (0..^𝑀) → (𝑗 − 1) ∈ ℝ)
424423adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑗 − 1) ∈ ℝ)
425394adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 ∈ ℝ)
426 elfzle2 13503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑙 ∈ (1...(𝑗 − 1)) → 𝑙 ≤ (𝑗 − 1))
427426adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ≤ (𝑗 − 1))
428425ltm1d 12144 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑗 − 1) < 𝑗)
429421, 424, 425, 427, 428lelttrd 11370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑗)
430429adantll 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑗)
431398ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 < 𝑀)
432418, 420, 419, 430, 431lttrd 11373 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑀)
433418, 419, 432ltled 11360 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙𝑀)
434406, 407, 409, 417, 433elfzd 13490 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ (0...𝑀))
435405, 434ffvelcdmd 7078 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄𝑙) ∈ ℝ)
436409peano2zd 12667 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ∈ ℤ)
437411, 412readdcld 11241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) ∈ ℝ)
438411, 412, 415, 413addgt0d 11787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...(𝑗 − 1)) → 0 < (𝑙 + 1))
439410, 437, 438ltled 11360 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (1...(𝑗 − 1)) → 0 ≤ (𝑙 + 1))
440439adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ≤ (𝑙 + 1))
441437adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ∈ ℝ)
442437recnd 11240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) ∈ ℂ)
443 1cnd 11207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑙 ∈ (1...(𝑗 − 1)) → 1 ∈ ℂ)
444442, 443npcand 11573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑙 ∈ (1...(𝑗 − 1)) → (((𝑙 + 1) − 1) + 1) = (𝑙 + 1))
445444eqcomd 2730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) = (((𝑙 + 1) − 1) + 1))
446445adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) = (((𝑙 + 1) − 1) + 1))
447 peano2re 11385 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑙 ∈ ℝ → (𝑙 + 1) ∈ ℝ)
448 peano2rem 11525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 + 1) ∈ ℝ → ((𝑙 + 1) − 1) ∈ ℝ)
449421, 447, 4483syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((𝑙 + 1) − 1) ∈ ℝ)
450 peano2re 11385 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 − 1) ∈ ℝ → ((𝑗 − 1) + 1) ∈ ℝ)
451 peano2rem 11525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑗 − 1) + 1) ∈ ℝ → (((𝑗 − 1) + 1) − 1) ∈ ℝ)
452424, 450, 4513syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (((𝑗 − 1) + 1) − 1) ∈ ℝ)
453 1red 11213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 1 ∈ ℝ)
454 elfzel2 13497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑗 − 1) ∈ ℤ)
455454zred 12664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑗 − 1) ∈ ℝ)
456455, 412readdcld 11241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑙 ∈ (1...(𝑗 − 1)) → ((𝑗 − 1) + 1) ∈ ℝ)
457411, 455, 412, 426leadd1dd 11826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) ≤ ((𝑗 − 1) + 1))
458437, 456, 412, 457lesub1dd 11828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑙 ∈ (1...(𝑗 − 1)) → ((𝑙 + 1) − 1) ≤ (((𝑗 − 1) + 1) − 1))
459458adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((𝑙 + 1) − 1) ≤ (((𝑗 − 1) + 1) − 1))
460449, 452, 453, 459leadd1dd 11826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (((𝑙 + 1) − 1) + 1) ≤ ((((𝑗 − 1) + 1) − 1) + 1))
461 peano2zm 12603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑗 ∈ ℤ → (𝑗 − 1) ∈ ℤ)
462362, 461syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑗 ∈ (0..^𝑀) → (𝑗 − 1) ∈ ℤ)
463462peano2zd 12667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ (0..^𝑀) → ((𝑗 − 1) + 1) ∈ ℤ)
464463zcnd 12665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 ∈ (0..^𝑀) → ((𝑗 − 1) + 1) ∈ ℂ)
465 1cnd 11207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 ∈ (0..^𝑀) → 1 ∈ ℂ)
466464, 465npcand 11573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 ∈ (0..^𝑀) → ((((𝑗 − 1) + 1) − 1) + 1) = ((𝑗 − 1) + 1))
467394recnd 11240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℂ)
468467, 465npcand 11573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 ∈ (0..^𝑀) → ((𝑗 − 1) + 1) = 𝑗)
469466, 468eqtrd 2764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑗 ∈ (0..^𝑀) → ((((𝑗 − 1) + 1) − 1) + 1) = 𝑗)
470469adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((((𝑗 − 1) + 1) − 1) + 1) = 𝑗)
471460, 470breqtrd 5165 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (((𝑙 + 1) − 1) + 1) ≤ 𝑗)
472446, 471eqbrtrd 5161 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ≤ 𝑗)
473472adantll 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ≤ 𝑗)
474441, 420, 419, 473, 431lelttrd 11370 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) < 𝑀)
475441, 419, 474ltled 11360 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ≤ 𝑀)
476406, 407, 436, 440, 475elfzd 13490 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ∈ (0...𝑀))
477405, 476ffvelcdmd 7078 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄‘(𝑙 + 1)) ∈ ℝ)
478 simpll 764 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝜑)
479 0zd 12568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ∈ ℤ)
480408adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℤ)
481416adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ≤ 𝑙)
482 eluz2 12826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (ℤ‘0) ↔ (0 ∈ ℤ ∧ 𝑙 ∈ ℤ ∧ 0 ≤ 𝑙))
483479, 480, 481, 482syl3anbrc 1340 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ (ℤ‘0))
484 elfzoel2 13629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0..^𝑀) → 𝑀 ∈ ℤ)
485484adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℤ)
486485zred 12664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℝ)
487398adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 < 𝑀)
488421, 425, 486, 429, 487lttrd 11373 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑀)
489 elfzo2 13633 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (0..^𝑀) ↔ (𝑙 ∈ (ℤ‘0) ∧ 𝑀 ∈ ℤ ∧ 𝑙 < 𝑀))
490483, 485, 488, 489syl3anbrc 1340 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ (0..^𝑀))
491490adantll 711 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ (0..^𝑀))
492 eleq1 2813 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 = 𝑙 → (𝑖 ∈ (0..^𝑀) ↔ 𝑙 ∈ (0..^𝑀)))
493492anbi2d 628 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 = 𝑙 → ((𝜑𝑖 ∈ (0..^𝑀)) ↔ (𝜑𝑙 ∈ (0..^𝑀))))
494 fveq2 6882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 = 𝑙 → (𝑄𝑖) = (𝑄𝑙))
495 oveq1 7409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 = 𝑙 → (𝑖 + 1) = (𝑙 + 1))
496495fveq2d 6886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 = 𝑙 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑙 + 1)))
497494, 496breq12d 5152 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 = 𝑙 → ((𝑄𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄𝑙) < (𝑄‘(𝑙 + 1))))
498493, 497imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 = 𝑙 → (((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑𝑙 ∈ (0..^𝑀)) → (𝑄𝑙) < (𝑄‘(𝑙 + 1)))))
499498, 150chvarvv 1994 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑙 ∈ (0..^𝑀)) → (𝑄𝑙) < (𝑄‘(𝑙 + 1)))
500478, 491, 499syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄𝑙) < (𝑄‘(𝑙 + 1)))
501435, 477, 500ltled 11360 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄𝑙) ≤ (𝑄‘(𝑙 + 1)))
502501adantlr 712 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄𝑙) ≤ (𝑄‘(𝑙 + 1)))
503376, 404, 502monoord 13996 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝑄‘1) ≤ (𝑄𝑗))
504354, 355, 359, 360, 503ltletrd 11372 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝐴 < (𝑄𝑗))
505354, 359ltnled 11359 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝐴 < (𝑄𝑗) ↔ ¬ (𝑄𝑗) ≤ 𝐴))
506504, 505mpbid 231 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → ¬ (𝑄𝑗) ≤ 𝐴)
507506ex 412 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑀)) → (¬ 𝑗 ≤ 0 → ¬ (𝑄𝑗) ≤ 𝐴))
5085073adant3 1129 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑀) ∧ (𝑄𝑗) ≤ 𝐴) → (¬ 𝑗 ≤ 0 → ¬ (𝑄𝑗) ≤ 𝐴))
509353, 508mt4d 117 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑀) ∧ (𝑄𝑗) ≤ 𝐴) → 𝑗 ≤ 0)
510 elfzole1 13638 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0..^𝑀) → 0 ≤ 𝑗)
5115103ad2ant2 1131 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑀) ∧ (𝑄𝑗) ≤ 𝐴) → 0 ≤ 𝑗)
5123943ad2ant2 1131 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑀) ∧ (𝑄𝑗) ≤ 𝐴) → 𝑗 ∈ ℝ)
513 0red 11215 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑀) ∧ (𝑄𝑗) ≤ 𝐴) → 0 ∈ ℝ)
514512, 513letri3d 11354 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑀) ∧ (𝑄𝑗) ≤ 𝐴) → (𝑗 = 0 ↔ (𝑗 ≤ 0 ∧ 0 ≤ 𝑗)))
515509, 511, 514mpbir2and 710 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑀) ∧ (𝑄𝑗) ≤ 𝐴) → 𝑗 = 0)
516345, 347, 352, 515syl3anc 1368 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}) → 𝑗 = 0)
517 velsn 4637 . . . . . . . . . . . . . . 15 (𝑗 ∈ {0} ↔ 𝑗 = 0)
518516, 517sylibr 233 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}) → 𝑗 ∈ {0})
519518ralrimiva 3138 . . . . . . . . . . . . 13 (𝜑 → ∀𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}𝑗 ∈ {0})
520 dfss3 3963 . . . . . . . . . . . . 13 ({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴} ⊆ {0} ↔ ∀𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}𝑗 ∈ {0})
521519, 520sylibr 233 . . . . . . . . . . . 12 (𝜑 → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴} ⊆ {0})
522155, 112eqeltrd 2825 . . . . . . . . . . . . . . 15 (𝜑 → (𝑄‘0) ∈ ℝ)
523522, 155eqled 11315 . . . . . . . . . . . . . 14 (𝜑 → (𝑄‘0) ≤ 𝐴)
524143breq1d 5149 . . . . . . . . . . . . . . 15 (𝑖 = 0 → ((𝑄𝑖) ≤ 𝐴 ↔ (𝑄‘0) ≤ 𝐴))
525524elrab 3676 . . . . . . . . . . . . . 14 (0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴} ↔ (0 ∈ (0..^𝑀) ∧ (𝑄‘0) ≤ 𝐴))
526139, 523, 525sylanbrc 582 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴})
527526snssd 4805 . . . . . . . . . . . 12 (𝜑 → {0} ⊆ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴})
528521, 527eqssd 3992 . . . . . . . . . . 11 (𝜑 → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴} = {0})
529528supeq1d 9438 . . . . . . . . . 10 (𝜑 → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}, ℝ, < ) = sup({0}, ℝ, < ))
530 supsn 9464 . . . . . . . . . . . 12 (( < Or ℝ ∧ 0 ∈ ℝ) → sup({0}, ℝ, < ) = 0)
53159, 140, 530mp2an 689 . . . . . . . . . . 11 sup({0}, ℝ, < ) = 0
532531a1i 11 . . . . . . . . . 10 (𝜑 → sup({0}, ℝ, < ) = 0)
533529, 532eqtrd 2764 . . . . . . . . 9 (𝜑 → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}, ℝ, < ) = 0)
534533ad2antrr 723 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}, ℝ, < ) = 0)
535332, 344, 5343eqtrd 2768 . . . . . . 7 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐼‘(𝑆𝑗)) = 0)
536535oveq1d 7417 . . . . . 6 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → ((𝐼‘(𝑆𝑗)) + 1) = (0 + 1))
537536fveq2d 6886 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) = (𝑄‘(0 + 1)))
538537, 157eqtr2di 2781 . . . 4 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝑄‘1) = (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
539328, 538breqtrd 5165 . . 3 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
54065adantr 480 . . . 4 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝜑 ∧ (𝑆𝑗) ∈ ℝ))
541 simplr 766 . . . 4 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝑗 ∈ (0..^𝑁))
54213a1i 11 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)))
543 simpr 484 . . . . . . . . . . . . . . . 16 ((¬ (𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → 𝑦 = (𝐸‘(𝑆𝑗)))
544 neqne 2940 . . . . . . . . . . . . . . . . 17 (¬ (𝐸‘(𝑆𝑗)) = 𝐵 → (𝐸‘(𝑆𝑗)) ≠ 𝐵)
545544adantr 480 . . . . . . . . . . . . . . . 16 ((¬ (𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → (𝐸‘(𝑆𝑗)) ≠ 𝐵)
546543, 545eqnetrd 3000 . . . . . . . . . . . . . . 15 ((¬ (𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → 𝑦𝐵)
547546neneqd 2937 . . . . . . . . . . . . . 14 ((¬ (𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → ¬ 𝑦 = 𝐵)
548547iffalsed 4532 . . . . . . . . . . . . 13 ((¬ (𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝑦)
549548, 543eqtrd 2764 . . . . . . . . . . . 12 ((¬ (𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = (𝐸‘(𝑆𝑗)))
550549adantll 711 . . . . . . . . . . 11 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ 𝑦 = (𝐸‘(𝑆𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = (𝐸‘(𝑆𝑗)))
551112, 216, 218, 11, 12fourierdlem4 45337 . . . . . . . . . . . . . 14 (𝜑𝐸:ℝ⟶(𝐴(,]𝐵))
552551adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐸:ℝ⟶(𝐴(,]𝐵))
553552, 42ffvelcdmd 7078 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆𝑗)) ∈ (𝐴(,]𝐵))
554553adantr 480 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) ∈ (𝐴(,]𝐵))
555542, 550, 554, 554fvmptd 6996 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐿‘(𝐸‘(𝑆𝑗))) = (𝐸‘(𝑆𝑗)))
556555eqcomd 2730 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) = (𝐿‘(𝐸‘(𝑆𝑗))))
557112, 216, 218, 13fourierdlem17 45350 . . . . . . . . . . . . 13 (𝜑𝐿:(𝐴(,]𝐵)⟶(𝐴[,]𝐵))
558557adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐿:(𝐴(,]𝐵)⟶(𝐴[,]𝐵))
559112, 216iccssred 13409 . . . . . . . . . . . . 13 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
560559adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐴[,]𝐵) ⊆ ℝ)
561558, 560fssd 6726 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐿:(𝐴(,]𝐵)⟶ℝ)
562561, 553ffvelcdmd 7078 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐿‘(𝐸‘(𝑆𝑗))) ∈ ℝ)
563562adantr 480 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐿‘(𝐸‘(𝑆𝑗))) ∈ ℝ)
564556, 563eqeltrd 2825 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) ∈ ℝ)
565216ad2antrr 723 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐵 ∈ ℝ)
566243adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ℝ*)
567216adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐵 ∈ ℝ)
568 elioc2 13385 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → ((𝐸‘(𝑆𝑗)) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘(𝑆𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆𝑗)) ∧ (𝐸‘(𝑆𝑗)) ≤ 𝐵)))
569566, 567, 568syl2anc 583 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆𝑗)) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘(𝑆𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆𝑗)) ∧ (𝐸‘(𝑆𝑗)) ≤ 𝐵)))
570553, 569mpbid 231 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆𝑗)) ∧ (𝐸‘(𝑆𝑗)) ≤ 𝐵))
571570simp3d 1141 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆𝑗)) ≤ 𝐵)
572571adantr 480 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) ≤ 𝐵)
573544necomd 2988 . . . . . . . . 9 (¬ (𝐸‘(𝑆𝑗)) = 𝐵𝐵 ≠ (𝐸‘(𝑆𝑗)))
574573adantl 481 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐵 ≠ (𝐸‘(𝑆𝑗)))
575564, 565, 572, 574leneltd 11366 . . . . . . 7 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) < 𝐵)
576575adantr 480 . . . . . 6 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆𝑗)) < 𝐵)
577 oveq1 7409 . . . . . . . . . . 11 ((𝐼‘(𝑆𝑗)) = (𝑀 − 1) → ((𝐼‘(𝑆𝑗)) + 1) = ((𝑀 − 1) + 1))
5782nncnd 12226 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℂ)
579 1cnd 11207 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℂ)
580578, 579npcand 11573 . . . . . . . . . . 11 (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
581577, 580sylan9eqr 2786 . . . . . . . . . 10 ((𝜑 ∧ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆𝑗)) + 1) = 𝑀)
582581fveq2d 6886 . . . . . . . . 9 ((𝜑 ∧ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) = (𝑄𝑀))
583154simprd 495 . . . . . . . . . 10 (𝜑 → (𝑄𝑀) = 𝐵)
584583adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝑄𝑀) = 𝐵)
585582, 584eqtr2d 2765 . . . . . . . 8 ((𝜑 ∧ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → 𝐵 = (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
586585adantlr 712 . . . . . . 7 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → 𝐵 = (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
587586adantlr 712 . . . . . 6 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → 𝐵 = (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
588576, 587breqtrd 5165 . . . . 5 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
589556adantr 480 . . . . . 6 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆𝑗)) = (𝐿‘(𝐸‘(𝑆𝑗))))
590 ssrab2 4070 . . . . . . . . . . . . 13 {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ⊆ (0..^𝑀)
591 fzssz 13501 . . . . . . . . . . . . . . 15 (0...𝑀) ⊆ ℤ
59217, 591sstri 3984 . . . . . . . . . . . . . 14 (0..^𝑀) ⊆ ℤ
593 zssre 12563 . . . . . . . . . . . . . 14 ℤ ⊆ ℝ
594592, 593sstri 3984 . . . . . . . . . . . . 13 (0..^𝑀) ⊆ ℝ
595590, 594sstri 3984 . . . . . . . . . . . 12 {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ⊆ ℝ
596595a1i 11 . . . . . . . . . . 11 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ⊆ ℝ)
59756neeq1d 2992 . . . . . . . . . . . . . . 15 (𝑥 = (𝑆𝑗) → ({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))} ≠ ∅ ↔ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ≠ ∅))
59867, 597imbi12d 344 . . . . . . . . . . . . . 14 (𝑥 = (𝑆𝑗) → (((𝜑𝑥 ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))} ≠ ∅) ↔ ((𝜑 ∧ (𝑆𝑗) ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ≠ ∅)))
599139adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → 0 ∈ (0..^𝑀))
600523ad2antrr 723 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ) ∧ (𝐸𝑥) = 𝐵) → (𝑄‘0) ≤ 𝐴)
601 iftrue 4527 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸𝑥) = 𝐵 → if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)) = 𝐴)
602601eqcomd 2730 . . . . . . . . . . . . . . . . . . . 20 ((𝐸𝑥) = 𝐵𝐴 = if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
603602adantl 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ) ∧ (𝐸𝑥) = 𝐵) → 𝐴 = if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
604600, 603breqtrd 5165 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ) ∧ (𝐸𝑥) = 𝐵) → (𝑄‘0) ≤ if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
605522adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → (𝑄‘0) ∈ ℝ)
606112adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ ℝ) → 𝐴 ∈ ℝ)
607606rexrd 11262 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ ℝ) → 𝐴 ∈ ℝ*)
608216adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ ℝ) → 𝐵 ∈ ℝ)
609 iocssre 13402 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
610607, 608, 609syl2anc 583 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
611551ffvelcdmda 7077 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → (𝐸𝑥) ∈ (𝐴(,]𝐵))
612610, 611sseldd 3976 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → (𝐸𝑥) ∈ ℝ)
613155adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → (𝑄‘0) = 𝐴)
614 elioc2 13385 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → ((𝐸𝑥) ∈ (𝐴(,]𝐵) ↔ ((𝐸𝑥) ∈ ℝ ∧ 𝐴 < (𝐸𝑥) ∧ (𝐸𝑥) ≤ 𝐵)))
615607, 608, 614syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ ℝ) → ((𝐸𝑥) ∈ (𝐴(,]𝐵) ↔ ((𝐸𝑥) ∈ ℝ ∧ 𝐴 < (𝐸𝑥) ∧ (𝐸𝑥) ≤ 𝐵)))
616611, 615mpbid 231 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ ℝ) → ((𝐸𝑥) ∈ ℝ ∧ 𝐴 < (𝐸𝑥) ∧ (𝐸𝑥) ≤ 𝐵))
617616simp2d 1140 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → 𝐴 < (𝐸𝑥))
618613, 617eqbrtrd 5161 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → (𝑄‘0) < (𝐸𝑥))
619605, 612, 618ltled 11360 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → (𝑄‘0) ≤ (𝐸𝑥))
620619adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ) ∧ ¬ (𝐸𝑥) = 𝐵) → (𝑄‘0) ≤ (𝐸𝑥))
621 iffalse 4530 . . . . . . . . . . . . . . . . . . . . 21 (¬ (𝐸𝑥) = 𝐵 → if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)) = (𝐸𝑥))
622621eqcomd 2730 . . . . . . . . . . . . . . . . . . . 20 (¬ (𝐸𝑥) = 𝐵 → (𝐸𝑥) = if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
623622adantl 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ) ∧ ¬ (𝐸𝑥) = 𝐵) → (𝐸𝑥) = if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
624620, 623breqtrd 5165 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ) ∧ ¬ (𝐸𝑥) = 𝐵) → (𝑄‘0) ≤ if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
625604, 624pm2.61dan 810 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → (𝑄‘0) ≤ if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
62613a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)))
627 eqeq1 2728 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐸𝑥) → (𝑦 = 𝐵 ↔ (𝐸𝑥) = 𝐵))
628 id 22 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐸𝑥) → 𝑦 = (𝐸𝑥))
629627, 628ifbieq2d 4547 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝐸𝑥) → if(𝑦 = 𝐵, 𝐴, 𝑦) = if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
630629adantl 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 = (𝐸𝑥)) → if(𝑦 = 𝐵, 𝐴, 𝑦) = if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
631606, 612ifcld 4567 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)) ∈ ℝ)
632626, 630, 611, 631fvmptd 6996 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → (𝐿‘(𝐸𝑥)) = if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
633625, 632breqtrrd 5167 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → (𝑄‘0) ≤ (𝐿‘(𝐸𝑥)))
634143breq1d 5149 . . . . . . . . . . . . . . . . 17 (𝑖 = 0 → ((𝑄𝑖) ≤ (𝐿‘(𝐸𝑥)) ↔ (𝑄‘0) ≤ (𝐿‘(𝐸𝑥))))
635634elrab 3676 . . . . . . . . . . . . . . . 16 (0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))} ↔ (0 ∈ (0..^𝑀) ∧ (𝑄‘0) ≤ (𝐿‘(𝐸𝑥))))
636599, 633, 635sylanbrc 582 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ) → 0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))})
637 ne0i 4327 . . . . . . . . . . . . . . 15 (0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))} → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))} ≠ ∅)
638636, 637syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))} ≠ ∅)
639598, 638vtoclg 3535 . . . . . . . . . . . . 13 ((𝑆𝑗) ∈ ℝ → ((𝜑 ∧ (𝑆𝑗) ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ≠ ∅))
64042, 65, 639sylc 65 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ≠ ∅)
641640ad2antrr 723 . . . . . . . . . . 11 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ≠ ∅)
642595a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ⊆ ℝ)
643 fzofi 13937 . . . . . . . . . . . . . . 15 (0..^𝑀) ∈ Fin
644 ssfi 9170 . . . . . . . . . . . . . . 15 (((0..^𝑀) ∈ Fin ∧ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ⊆ (0..^𝑀)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ∈ Fin)
645643, 590, 644mp2an 689 . . . . . . . . . . . . . 14 {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ∈ Fin
646645a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ∈ Fin)
647 fimaxre2 12157 . . . . . . . . . . . . 13 (({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ⊆ ℝ ∧ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}𝑙𝑥)
648642, 646, 647syl2anc 583 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}𝑙𝑥)
649648ad2antrr 723 . . . . . . . . . . 11 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}𝑙𝑥)
650 0red 11215 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → 0 ∈ ℝ)
651594, 47sselid 3973 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆𝑗)) ∈ ℝ)
652 1red 11213 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑁)) → 1 ∈ ℝ)
653651, 652readdcld 11241 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆𝑗)) + 1) ∈ ℝ)
654 elfzouz 13634 . . . . . . . . . . . . . . . . . 18 ((𝐼‘(𝑆𝑗)) ∈ (0..^𝑀) → (𝐼‘(𝑆𝑗)) ∈ (ℤ‘0))
655 eluzle 12833 . . . . . . . . . . . . . . . . . 18 ((𝐼‘(𝑆𝑗)) ∈ (ℤ‘0) → 0 ≤ (𝐼‘(𝑆𝑗)))
65647, 654, 6553syl 18 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑁)) → 0 ≤ (𝐼‘(𝑆𝑗)))
657385a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑁)) → 0 < 1)
658651, 652, 656, 657addgegt0d 11785 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → 0 < ((𝐼‘(𝑆𝑗)) + 1))
659650, 653, 658ltled 11360 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0..^𝑁)) → 0 ≤ ((𝐼‘(𝑆𝑗)) + 1))
660659adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → 0 ≤ ((𝐼‘(𝑆𝑗)) + 1))
661651adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐼‘(𝑆𝑗)) ∈ ℝ)
662 1red 11213 . . . . . . . . . . . . . . . . . 18 (𝜑 → 1 ∈ ℝ)
663392, 662resubcld 11640 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 − 1) ∈ ℝ)
664663ad2antrr 723 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝑀 − 1) ∈ ℝ)
665 1red 11213 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → 1 ∈ ℝ)
666 elfzolt2 13639 . . . . . . . . . . . . . . . . . . . 20 ((𝐼‘(𝑆𝑗)) ∈ (0..^𝑀) → (𝐼‘(𝑆𝑗)) < 𝑀)
66747, 666syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆𝑗)) < 𝑀)
66843elfzelzd 13500 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆𝑗)) ∈ ℤ)
66996adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑀 ∈ ℤ)
670 zltlem1 12613 . . . . . . . . . . . . . . . . . . . 20 (((𝐼‘(𝑆𝑗)) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝐼‘(𝑆𝑗)) < 𝑀 ↔ (𝐼‘(𝑆𝑗)) ≤ (𝑀 − 1)))
671668, 669, 670syl2anc 583 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆𝑗)) < 𝑀 ↔ (𝐼‘(𝑆𝑗)) ≤ (𝑀 − 1)))
672667, 671mpbid 231 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆𝑗)) ≤ (𝑀 − 1))
673672adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐼‘(𝑆𝑗)) ≤ (𝑀 − 1))
674 neqne 2940 . . . . . . . . . . . . . . . . . . 19 (¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1) → (𝐼‘(𝑆𝑗)) ≠ (𝑀 − 1))
675674necomd 2988 . . . . . . . . . . . . . . . . . 18 (¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1) → (𝑀 − 1) ≠ (𝐼‘(𝑆𝑗)))
676675adantl 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝑀 − 1) ≠ (𝐼‘(𝑆𝑗)))
677661, 664, 673, 676leneltd 11366 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐼‘(𝑆𝑗)) < (𝑀 − 1))
678661, 664, 665, 677ltadd1dd 11823 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆𝑗)) + 1) < ((𝑀 − 1) + 1))
679580ad2antrr 723 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → ((𝑀 − 1) + 1) = 𝑀)
680678, 679breqtrd 5165 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆𝑗)) + 1) < 𝑀)
68149elfzelzd 13500 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆𝑗)) + 1) ∈ ℤ)
682681adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆𝑗)) + 1) ∈ ℤ)
683 0zd 12568 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → 0 ∈ ℤ)
68496ad2antrr 723 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → 𝑀 ∈ ℤ)
685 elfzo 13632 . . . . . . . . . . . . . . 15 ((((𝐼‘(𝑆𝑗)) + 1) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝐼‘(𝑆𝑗)) + 1) ∈ (0..^𝑀) ↔ (0 ≤ ((𝐼‘(𝑆𝑗)) + 1) ∧ ((𝐼‘(𝑆𝑗)) + 1) < 𝑀)))
686682, 683, 684, 685syl3anc 1368 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (((𝐼‘(𝑆𝑗)) + 1) ∈ (0..^𝑀) ↔ (0 ≤ ((𝐼‘(𝑆𝑗)) + 1) ∧ ((𝐼‘(𝑆𝑗)) + 1) < 𝑀)))
687660, 680, 686mpbir2and 710 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆𝑗)) + 1) ∈ (0..^𝑀))
688687adantr 480 . . . . . . . . . . . 12 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → ((𝐼‘(𝑆𝑗)) + 1) ∈ (0..^𝑀))
689 simpr 484 . . . . . . . . . . . 12 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗))))
690 fveq2 6882 . . . . . . . . . . . . . 14 (𝑖 = ((𝐼‘(𝑆𝑗)) + 1) → (𝑄𝑖) = (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
691690breq1d 5149 . . . . . . . . . . . . 13 (𝑖 = ((𝐼‘(𝑆𝑗)) + 1) → ((𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗))) ↔ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))))
692691elrab 3676 . . . . . . . . . . . 12 (((𝐼‘(𝑆𝑗)) + 1) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ↔ (((𝐼‘(𝑆𝑗)) + 1) ∈ (0..^𝑀) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))))
693688, 689, 692sylanbrc 582 . . . . . . . . . . 11 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → ((𝐼‘(𝑆𝑗)) + 1) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))})
694 suprub 12173 . . . . . . . . . . 11 ((({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ⊆ ℝ ∧ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}𝑙𝑥) ∧ ((𝐼‘(𝑆𝑗)) + 1) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}) → ((𝐼‘(𝑆𝑗)) + 1) ≤ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ))
695596, 641, 649, 693, 694syl31anc 1370 . . . . . . . . . 10 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → ((𝐼‘(𝑆𝑗)) + 1) ≤ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ))
69662eqcomd 2730 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) = (𝐼‘(𝑆𝑗)))
697696ad2antrr 723 . . . . . . . . . 10 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) = (𝐼‘(𝑆𝑗)))
698695, 697breqtrd 5165 . . . . . . . . 9 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → ((𝐼‘(𝑆𝑗)) + 1) ≤ (𝐼‘(𝑆𝑗)))
699651ltp1d 12142 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆𝑗)) < ((𝐼‘(𝑆𝑗)) + 1))
700651, 653ltnled 11359 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆𝑗)) < ((𝐼‘(𝑆𝑗)) + 1) ↔ ¬ ((𝐼‘(𝑆𝑗)) + 1) ≤ (𝐼‘(𝑆𝑗))))
701699, 700mpbid 231 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → ¬ ((𝐼‘(𝑆𝑗)) + 1) ≤ (𝐼‘(𝑆𝑗)))
702701ad2antrr 723 . . . . . . . . 9 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → ¬ ((𝐼‘(𝑆𝑗)) + 1) ≤ (𝐼‘(𝑆𝑗)))
703698, 702pm2.65da 814 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → ¬ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗))))
704562adantr 480 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐿‘(𝐸‘(𝑆𝑗))) ∈ ℝ)
70550adantr 480 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ∈ ℝ)
706704, 705ltnled 11359 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → ((𝐿‘(𝐸‘(𝑆𝑗))) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ↔ ¬ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))))
707703, 706mpbird 257 . . . . . . 7 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐿‘(𝐸‘(𝑆𝑗))) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
708707adantlr 712 . . . . . 6 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐿‘(𝐸‘(𝑆𝑗))) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
709589, 708eqbrtrd 5161 . . . . 5 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
710588, 709pm2.61dan 810 . . . 4 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
71123ad2ant1 1130 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → 𝑀 ∈ ℕ)
71213ad2ant1 1130 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → 𝑄 ∈ (𝑃𝑀))
713213ad2ant1 1130 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → 𝐶 ∈ ℝ)
714223ad2ant1 1130 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → 𝐷 ∈ ℝ)
715233ad2ant1 1130 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → 𝐶 < 𝐷)
716493adant3 1129 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → ((𝐼‘(𝑆𝑗)) + 1) ∈ (0...𝑀))
717 simp2 1134 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → 𝑗 ∈ (0..^𝑁))
71842leidd 11778 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ≤ (𝑆𝑗))
719 elico2 13386 . . . . . . . . 9 (((𝑆𝑗) ∈ ℝ ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ*) → ((𝑆𝑗) ∈ ((𝑆𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ ((𝑆𝑗) ∈ ℝ ∧ (𝑆𝑗) ≤ (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝑗 + 1)))))
72042, 210, 719syl2anc 583 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) ∈ ((𝑆𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ ((𝑆𝑗) ∈ ℝ ∧ (𝑆𝑗) ≤ (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝑗 + 1)))))
72142, 718, 129, 720mpbir3and 1339 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ∈ ((𝑆𝑗)[,)(𝑆‘(𝑗 + 1))))
7227213adant3 1129 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → (𝑆𝑗) ∈ ((𝑆𝑗)[,)(𝑆‘(𝑗 + 1))))
723 simp3 1135 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
724 eqid 2724 . . . . . 6 ((𝑄‘((𝐼‘(𝑆𝑗)) + 1)) − ((𝐸‘(𝑆𝑗)) − (𝑆𝑗))) = ((𝑄‘((𝐼‘(𝑆𝑗)) + 1)) − ((𝐸‘(𝑆𝑗)) − (𝑆𝑗)))
72511, 3, 711, 712, 713, 714, 715, 24, 25, 26, 27, 12, 716, 717, 722, 723, 724fourierdlem63 45395 . . . . 5 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
7267253adant1r 1174 . . . 4 (((𝜑 ∧ (𝑆𝑗) ∈ ℝ) ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
727540, 541, 710, 726syl3anc 1368 . . 3 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
728539, 727pm2.61dan 810 . 2 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
729 ioossioo 13416 . 2 ((((𝑄‘(𝐼‘(𝑆𝑗))) ∈ ℝ* ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ∈ ℝ*) ∧ ((𝑄‘(𝐼‘(𝑆𝑗))) ≤ (𝐿‘(𝐸‘(𝑆𝑗))) ∧ (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))) → ((𝐿‘(𝐸‘(𝑆𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆𝑗)))(,)(𝑄‘((𝐼‘(𝑆𝑗)) + 1))))
73045, 51, 89, 728, 729syl22anc 836 1 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐿‘(𝐸‘(𝑆𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆𝑗)))(,)(𝑄‘((𝐼‘(𝑆𝑗)) + 1))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  w3a 1084   = wceq 1533  wcel 2098  wne 2932  wral 3053  wrex 3062  {crab 3424  Vcvv 3466  cun 3939  wss 3941  c0 4315  ifcif 4521  {csn 4621  {cpr 4623   class class class wbr 5139  cmpt 5222   Or wor 5578  ran crn 5668  cio 6484  wf 6530  cfv 6534   Isom wiso 6535  (class class class)co 7402  m cmap 8817  Fincfn 8936  supcsup 9432  cc 11105  cr 11106  0cc0 11107  1c1 11108   + caddc 11110   · cmul 11112  *cxr 11245   < clt 11246  cle 11247  cmin 11442   / cdiv 11869  cn 12210  2c2 12265  cz 12556  cuz 12820  +crp 12972  (,)cioo 13322  (,]cioc 13323  [,)cico 13324  [,]cicc 13325  ...cfz 13482  ..^cfzo 13625  cfl 13753  chash 14288
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5276  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719  ax-inf2 9633  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3960  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-int 4942  df-iun 4990  df-iin 4991  df-br 5140  df-opab 5202  df-mpt 5223  df-tr 5257  df-id 5565  df-eprel 5571  df-po 5579  df-so 5580  df-fr 5622  df-se 5623  df-we 5624  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-pred 6291  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-isom 6543  df-riota 7358  df-ov 7405  df-oprab 7406  df-mpo 7407  df-om 7850  df-1st 7969  df-2nd 7970  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-oadd 8466  df-er 8700  df-map 8819  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-fi 9403  df-sup 9434  df-inf 9435  df-oi 9502  df-dju 9893  df-card 9931  df-pnf 11248  df-mnf 11249  df-xr 11250  df-ltxr 11251  df-le 11252  df-sub 11444  df-neg 11445  df-div 11870  df-nn 12211  df-2 12273  df-3 12274  df-n0 12471  df-xnn0 12543  df-z 12557  df-uz 12821  df-q 12931  df-rp 12973  df-xneg 13090  df-xadd 13091  df-xmul 13092  df-ioo 13326  df-ioc 13327  df-ico 13328  df-icc 13329  df-fz 13483  df-fzo 13626  df-fl 13755  df-seq 13965  df-exp 14026  df-hash 14289  df-cj 15044  df-re 15045  df-im 15046  df-sqrt 15180  df-abs 15181  df-rest 17369  df-topgen 17390  df-psmet 21222  df-xmet 21223  df-met 21224  df-bl 21225  df-mopn 21226  df-top 22720  df-topon 22737  df-bases 22773  df-cld 22847  df-ntr 22848  df-cls 22849  df-nei 22926  df-lp 22964  df-cmp 23215
This theorem is referenced by:  fourierdlem89  45421  fourierdlem90  45422  fourierdlem91  45423
  Copyright terms: Public domain W3C validator