Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem79 Structured version   Visualization version   GIF version

Theorem fourierdlem79 40874
 Description: 𝐸 projects every interval of the partition induced by 𝑆 on 𝐻 into a corresponding interval of the partition induced by 𝑄 on [𝐴, 𝐵]. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem79.t 𝑇 = (𝐵𝐴)
fourierdlem79.p 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem79.m (𝜑𝑀 ∈ ℕ)
fourierdlem79.q (𝜑𝑄 ∈ (𝑃𝑀))
fourierdlem79.c (𝜑𝐶 ∈ ℝ)
fourierdlem79.d (𝜑𝐷 ∈ ℝ)
fourierdlem79.cltd (𝜑𝐶 < 𝐷)
fourierdlem79.o 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem79.h 𝐻 = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
fourierdlem79.n 𝑁 = ((♯‘𝐻) − 1)
fourierdlem79.s 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
fourierdlem79.e 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
fourierdlem79.l 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))
fourierdlem79.z 𝑍 = ((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)))
fourierdlem79.i 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ))
Assertion
Ref Expression
fourierdlem79 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐿‘(𝐸‘(𝑆𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆𝑗)))(,)(𝑄‘((𝐼‘(𝑆𝑗)) + 1))))
Distinct variable groups:   𝐴,𝑖,𝑗,𝑥   𝐴,𝑚,𝑝,𝑖   𝑦,𝐴,𝑗,𝑥   𝐵,𝑓   𝐵,𝑖,𝑘,𝑥   𝐵,𝑚,𝑝   𝑦,𝐵   𝐶,𝑖,𝑚,𝑝   𝑥,𝐶   𝐷,𝑖,𝑚,𝑝   𝑥,𝐷   𝑓,𝐸   𝑖,𝐸,𝑘,𝑥   𝑦,𝐸   𝑓,𝐻   𝑥,𝐻   𝑓,𝐼   𝑖,𝐼,𝑘,𝑥   𝑖,𝐿,𝑥   𝑖,𝑀,𝑗,𝑥   𝑚,𝑀,𝑝   𝑓,𝑁   𝑖,𝑁,𝑘,𝑥   𝑚,𝑁,𝑝   𝑦,𝑁   𝑄,𝑓,𝑗   𝑄,𝑖,𝑘,𝑥,𝑗   𝑄,𝑝   𝑆,𝑓   𝑆,𝑖,𝑘,𝑥   𝑆,𝑝   𝑦,𝑆   𝑇,𝑖,𝑘,𝑥   𝑘,𝑍,𝑥   𝜑,𝑓,𝑗   𝜑,𝑖,𝑘,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑚,𝑝)   𝐴(𝑓,𝑘)   𝐵(𝑗)   𝐶(𝑦,𝑓,𝑗,𝑘)   𝐷(𝑦,𝑓,𝑗,𝑘)   𝑃(𝑥,𝑦,𝑓,𝑖,𝑗,𝑘,𝑚,𝑝)   𝑄(𝑦,𝑚)   𝑆(𝑗,𝑚)   𝑇(𝑦,𝑓,𝑗,𝑚,𝑝)   𝐸(𝑗,𝑚,𝑝)   𝐻(𝑦,𝑖,𝑗,𝑘,𝑚,𝑝)   𝐼(𝑦,𝑗,𝑚,𝑝)   𝐿(𝑦,𝑓,𝑗,𝑘,𝑚,𝑝)   𝑀(𝑦,𝑓,𝑘)   𝑁(𝑗)   𝑂(𝑥,𝑦,𝑓,𝑖,𝑗,𝑘,𝑚,𝑝)   𝑍(𝑦,𝑓,𝑖,𝑗,𝑚,𝑝)

Proof of Theorem fourierdlem79
Dummy variable 𝑙 is distinct from all other variables.
StepHypRef Expression
1 fourierdlem79.q . . . . . . . 8 (𝜑𝑄 ∈ (𝑃𝑀))
2 fourierdlem79.m . . . . . . . . 9 (𝜑𝑀 ∈ ℕ)
3 fourierdlem79.p . . . . . . . . . 10 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
43fourierdlem2 40798 . . . . . . . . 9 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
52, 4syl 17 . . . . . . . 8 (𝜑 → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
61, 5mpbid 222 . . . . . . 7 (𝜑 → (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
76simpld 477 . . . . . 6 (𝜑𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)))
8 elmapi 8033 . . . . . 6 (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
97, 8syl 17 . . . . 5 (𝜑𝑄:(0...𝑀)⟶ℝ)
109adantr 472 . . . 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 40833 . . . . . . . 8 (𝜑 → (𝐼:ℝ⟶(0..^𝑀) ∧ (𝑥 ∈ ℝ → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))})))
1615simpld 477 . . . . . . 7 (𝜑𝐼:ℝ⟶(0..^𝑀))
17 fzossfz 12653 . . . . . . . 8 (0..^𝑀) ⊆ (0...𝑀)
1817a1i 11 . . . . . . 7 (𝜑 → (0..^𝑀) ⊆ (0...𝑀))
1916, 18fssd 6206 . . . . . 6 (𝜑𝐼:ℝ⟶(0...𝑀))
2019adantr 472 . . . . 5 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐼:ℝ⟶(0...𝑀))
21 fourierdlem79.c . . . . . . . . . . . . 13 (𝜑𝐶 ∈ ℝ)
22 fourierdlem79.d . . . . . . . . . . . . 13 (𝜑𝐷 ∈ ℝ)
23 fourierdlem79.cltd . . . . . . . . . . . . 13 (𝜑𝐶 < 𝐷)
24 fourierdlem79.o . . . . . . . . . . . . 13 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
25 fourierdlem79.h . . . . . . . . . . . . 13 𝐻 = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
26 fourierdlem79.n . . . . . . . . . . . . 13 𝑁 = ((♯‘𝐻) − 1)
27 fourierdlem79.s . . . . . . . . . . . . 13 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
2811, 3, 2, 1, 21, 22, 23, 24, 25, 26, 27fourierdlem54 40849 . . . . . . . . . . . 12 (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
2928simpld 477 . . . . . . . . . . 11 (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂𝑁)))
3029simprd 482 . . . . . . . . . 10 (𝜑𝑆 ∈ (𝑂𝑁))
3130adantr 472 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑆 ∈ (𝑂𝑁))
3229simpld 477 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℕ)
3332adantr 472 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑁 ∈ ℕ)
3424fourierdlem2 40798 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂𝑁) ↔ (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆𝑖) < (𝑆‘(𝑖 + 1))))))
3533, 34syl 17 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆 ∈ (𝑂𝑁) ↔ (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆𝑖) < (𝑆‘(𝑖 + 1))))))
3631, 35mpbid 222 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆𝑖) < (𝑆‘(𝑖 + 1)))))
3736simpld 477 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)))
38 elmapi 8033 . . . . . . 7 (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
3937, 38syl 17 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
40 elfzofz 12650 . . . . . . 7 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ (0...𝑁))
4140adantl 473 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0...𝑁))
4239, 41ffvelrnd 6511 . . . . 5 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ∈ ℝ)
4320, 42ffvelrnd 6511 . . . 4 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆𝑗)) ∈ (0...𝑀))
4410, 43ffvelrnd 6511 . . 3 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆𝑗))) ∈ ℝ)
4544rexrd 10252 . 2 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆𝑗))) ∈ ℝ*)
4616adantr 472 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐼:ℝ⟶(0..^𝑀))
4746, 42ffvelrnd 6511 . . . . 5 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆𝑗)) ∈ (0..^𝑀))
48 fzofzp1 12730 . . . . 5 ((𝐼‘(𝑆𝑗)) ∈ (0..^𝑀) → ((𝐼‘(𝑆𝑗)) + 1) ∈ (0...𝑀))
4947, 48syl 17 . . . 4 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆𝑗)) + 1) ∈ (0...𝑀))
5010, 49ffvelrnd 6511 . . 3 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ∈ ℝ)
5150rexrd 10252 . 2 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ∈ ℝ*)
5214a1i 11 . . . . 5 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < )))
53 fveq2 6340 . . . . . . . . . 10 (𝑥 = (𝑆𝑗) → (𝐸𝑥) = (𝐸‘(𝑆𝑗)))
5453fveq2d 6344 . . . . . . . . 9 (𝑥 = (𝑆𝑗) → (𝐿‘(𝐸𝑥)) = (𝐿‘(𝐸‘(𝑆𝑗))))
5554breq2d 4804 . . . . . . . 8 (𝑥 = (𝑆𝑗) → ((𝑄𝑖) ≤ (𝐿‘(𝐸𝑥)) ↔ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))))
5655rabbidv 3317 . . . . . . 7 (𝑥 = (𝑆𝑗) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))} = {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))})
5756supeq1d 8505 . . . . . 6 (𝑥 = (𝑆𝑗) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ))
5857adantl 473 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑥 = (𝑆𝑗)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ))
59 ltso 10281 . . . . . . 7 < Or ℝ
6059supex 8522 . . . . . 6 sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ V
6160a1i 11 . . . . 5 ((𝜑𝑗 ∈ (0..^𝑁)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ V)
6252, 58, 42, 61fvmptd 6438 . . . 4 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆𝑗)) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ))
6362fveq2d 6344 . . 3 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆𝑗))) = (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < )))
64 simpl 474 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝜑)
6564, 42jca 555 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝜑 ∧ (𝑆𝑗) ∈ ℝ))
66 eleq1 2815 . . . . . . . . 9 (𝑥 = (𝑆𝑗) → (𝑥 ∈ ℝ ↔ (𝑆𝑗) ∈ ℝ))
6766anbi2d 742 . . . . . . . 8 (𝑥 = (𝑆𝑗) → ((𝜑𝑥 ∈ ℝ) ↔ (𝜑 ∧ (𝑆𝑗) ∈ ℝ)))
6857, 56eleq12d 2821 . . . . . . . 8 (𝑥 = (𝑆𝑗) → (sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))} ↔ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}))
6967, 68imbi12d 333 . . . . . . 7 (𝑥 = (𝑆𝑗) → (((𝜑𝑥 ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}) ↔ ((𝜑 ∧ (𝑆𝑗) ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))})))
7015simprd 482 . . . . . . . 8 (𝜑 → (𝑥 ∈ ℝ → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}))
7170imp 444 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))})
7269, 71vtoclg 3394 . . . . . 6 ((𝑆𝑗) ∈ ℝ → ((𝜑 ∧ (𝑆𝑗) ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}))
7342, 65, 72sylc 65 . . . . 5 ((𝜑𝑗 ∈ (0..^𝑁)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))})
74 nfrab1 3249 . . . . . . 7 𝑖{𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}
75 nfcv 2890 . . . . . . 7 𝑖
76 nfcv 2890 . . . . . . 7 𝑖 <
7774, 75, 76nfsup 8510 . . . . . 6 𝑖sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < )
78 nfcv 2890 . . . . . 6 𝑖(0..^𝑀)
79 nfcv 2890 . . . . . . . 8 𝑖𝑄
8079, 77nffv 6347 . . . . . . 7 𝑖(𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ))
81 nfcv 2890 . . . . . . 7 𝑖
82 nfcv 2890 . . . . . . 7 𝑖(𝐿‘(𝐸‘(𝑆𝑗)))
8380, 81, 82nfbr 4839 . . . . . 6 𝑖(𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))
84 fveq2 6340 . . . . . . 7 (𝑖 = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) → (𝑄𝑖) = (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < )))
8584breq1d 4802 . . . . . 6 (𝑖 = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) → ((𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗))) ↔ (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))))
8677, 78, 83, 85elrabf 3488 . . . . 5 (sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ↔ (sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ (0..^𝑀) ∧ (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))))
8773, 86sylib 208 . . . 4 ((𝜑𝑗 ∈ (0..^𝑁)) → (sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ (0..^𝑀) ∧ (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))))
8887simprd 482 . . 3 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆𝑗))))
8963, 88eqbrtrd 4814 . 2 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆𝑗))) ≤ (𝐿‘(𝐸‘(𝑆𝑗))))
902ad2antrr 764 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝑀 ∈ ℕ)
911ad2antrr 764 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝑄 ∈ (𝑃𝑀))
9221ad2antrr 764 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐶 ∈ ℝ)
9322ad2antrr 764 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐷 ∈ ℝ)
9423ad2antrr 764 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐶 < 𝐷)
95 0le1 10714 . . . . . . . 8 0 ≤ 1
9695a1i 11 . . . . . . 7 (𝜑 → 0 ≤ 1)
972nnge1d 11226 . . . . . . 7 (𝜑 → 1 ≤ 𝑀)
98 1zzd 11571 . . . . . . . 8 (𝜑 → 1 ∈ ℤ)
99 0zd 11552 . . . . . . . 8 (𝜑 → 0 ∈ ℤ)
1002nnzd 11644 . . . . . . . 8 (𝜑𝑀 ∈ ℤ)
101 elfz 12496 . . . . . . . 8 ((1 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (1 ∈ (0...𝑀) ↔ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
10298, 99, 100, 101syl3anc 1463 . . . . . . 7 (𝜑 → (1 ∈ (0...𝑀) ↔ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
10396, 97, 102mpbir2and 995 . . . . . 6 (𝜑 → 1 ∈ (0...𝑀))
104103ad2antrr 764 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 1 ∈ (0...𝑀))
105 simplr 809 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝑗 ∈ (0..^𝑁))
106 fourierdlem79.z . . . . . . . 8 𝑍 = ((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)))
107 fzofzp1 12730 . . . . . . . . . . . . . 14 (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ (0...𝑁))
108107adantl 473 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈ (0...𝑁))
10939, 108ffvelrnd 6511 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
110109, 42resubcld 10621 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) ∈ ℝ)
111110rehalfcld 11442 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2) ∈ ℝ)
1129, 103ffvelrnd 6511 . . . . . . . . . . . . 13 (𝜑 → (𝑄‘1) ∈ ℝ)
1133, 2, 1fourierdlem11 40807 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
114113simp1d 1134 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℝ)
115112, 114resubcld 10621 . . . . . . . . . . . 12 (𝜑 → ((𝑄‘1) − 𝐴) ∈ ℝ)
116115rehalfcld 11442 . . . . . . . . . . 11 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ)
117116adantr 472 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ)
118111, 117ifcld 4263 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ∈ ℝ)
11942, 118readdcld 10232 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) ∈ ℝ)
120106, 119syl5eqel 2831 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑍 ∈ ℝ)
121 2re 11253 . . . . . . . . . . . . . 14 2 ∈ ℝ
122121a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → 2 ∈ ℝ)
123 elfzoelz 12635 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℤ)
124123zred 11645 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℝ)
125124ltp1d 11117 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0..^𝑁) → 𝑗 < (𝑗 + 1))
126125adantl 473 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑗 < (𝑗 + 1))
12728simprd 482 . . . . . . . . . . . . . . . . 17 (𝜑𝑆 Isom < , < ((0...𝑁), 𝐻))
128127adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑆 Isom < , < ((0...𝑁), 𝐻))
129 isorel 6727 . . . . . . . . . . . . . . . 16 ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝑗 + 1) ∈ (0...𝑁))) → (𝑗 < (𝑗 + 1) ↔ (𝑆𝑗) < (𝑆‘(𝑗 + 1))))
130128, 41, 108, 129syl12anc 1461 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑗 < (𝑗 + 1) ↔ (𝑆𝑗) < (𝑆‘(𝑗 + 1))))
131126, 130mpbid 222 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) < (𝑆‘(𝑗 + 1)))
13242, 109posdifd 10777 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) < (𝑆‘(𝑗 + 1)) ↔ 0 < ((𝑆‘(𝑗 + 1)) − (𝑆𝑗))))
133131, 132mpbid 222 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → 0 < ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)))
134 2pos 11275 . . . . . . . . . . . . . 14 0 < 2
135134a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → 0 < 2)
136110, 122, 133, 135divgt0d 11122 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → 0 < (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
137111, 136elrpd 12033 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2) ∈ ℝ+)
138121a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 2 ∈ ℝ)
1392nngt0d 11227 . . . . . . . . . . . . . . . . . 18 (𝜑 → 0 < 𝑀)
140 fzolb 12641 . . . . . . . . . . . . . . . . . 18 (0 ∈ (0..^𝑀) ↔ (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
14199, 100, 139, 140syl3anbrc 1407 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ∈ (0..^𝑀))
142 0re 10203 . . . . . . . . . . . . . . . . . 18 0 ∈ ℝ
143 eleq1 2815 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 0 → (𝑖 ∈ (0..^𝑀) ↔ 0 ∈ (0..^𝑀)))
144143anbi2d 742 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 0 → ((𝜑𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 0 ∈ (0..^𝑀))))
145 fveq2 6340 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 0 → (𝑄𝑖) = (𝑄‘0))
146 oveq1 6808 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 0 → (𝑖 + 1) = (0 + 1))
147146fveq2d 6344 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 0 → (𝑄‘(𝑖 + 1)) = (𝑄‘(0 + 1)))
148145, 147breq12d 4805 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 0 → ((𝑄𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘0) < (𝑄‘(0 + 1))))
149144, 148imbi12d 333 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 0 → (((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))))
1506simprd 482 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))
151150simprd 482 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))
152151r19.21bi 3058 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
153149, 152vtoclg 3394 . . . . . . . . . . . . . . . . . 18 (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1))))
154142, 153ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))
155141, 154mpdan 705 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘0) < (𝑄‘(0 + 1)))
156150simpld 477 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵))
157156simpld 477 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘0) = 𝐴)
158 0p1e1 11295 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
159158fveq2i 6343 . . . . . . . . . . . . . . . . 17 (𝑄‘(0 + 1)) = (𝑄‘1)
160159a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘(0 + 1)) = (𝑄‘1))
161155, 157, 1603brtr3d 4823 . . . . . . . . . . . . . . 15 (𝜑𝐴 < (𝑄‘1))
162114, 112posdifd 10777 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 < (𝑄‘1) ↔ 0 < ((𝑄‘1) − 𝐴)))
163161, 162mpbid 222 . . . . . . . . . . . . . 14 (𝜑 → 0 < ((𝑄‘1) − 𝐴))
164134a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 0 < 2)
165115, 138, 163, 164divgt0d 11122 . . . . . . . . . . . . 13 (𝜑 → 0 < (((𝑄‘1) − 𝐴) / 2))
166116, 165elrpd 12033 . . . . . . . . . . . 12 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ+)
167166adantr 472 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ+)
168137, 167ifcld 4263 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ∈ ℝ+)
16942, 168ltaddrpd 12069 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) < ((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
17042, 119, 169ltled 10348 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ≤ ((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
171170, 106syl6breqr 4834 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ≤ 𝑍)
17242, 111readdcld 10232 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) ∈ ℝ)
173 iftrue 4224 . . . . . . . . . . . . 13 (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
174173adantl 473 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
175111leidd 10757 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
176175adantr 472 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
177174, 176eqbrtrd 4814 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
178 iffalse 4227 . . . . . . . . . . . . 13 (¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) − 𝐴) / 2))
179178adantl 473 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) − 𝐴) / 2))
180115ad2antrr 764 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑄‘1) − 𝐴) ∈ ℝ)
181110adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) ∈ ℝ)
182 2rp 12001 . . . . . . . . . . . . . 14 2 ∈ ℝ+
183182a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → 2 ∈ ℝ+)
184 simpr 479 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴))
185180, 181, 184nltled 10350 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑄‘1) − 𝐴) ≤ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)))
186180, 181, 183, 185lediv1dd 12094 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑄‘1) − 𝐴) / 2) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
187179, 186eqbrtrd 4814 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
188177, 187pm2.61dan 867 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
189118, 111, 42, 188leadd2dd 10805 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) ≤ ((𝑆𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)))
19042recnd 10231 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ∈ ℂ)
191109recnd 10231 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℂ)
192190, 191addcomd 10401 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + (𝑆‘(𝑗 + 1))) = ((𝑆‘(𝑗 + 1)) + (𝑆𝑗)))
193192oveq1d 6816 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) = (((𝑆‘(𝑗 + 1)) + (𝑆𝑗)) / 2))
194193oveq1d 6816 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → ((((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = ((((𝑆‘(𝑗 + 1)) + (𝑆𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)))
195 halfaddsub 11428 . . . . . . . . . . . . . . 15 (((𝑆‘(𝑗 + 1)) ∈ ℂ ∧ (𝑆𝑗) ∈ ℂ) → (((((𝑆‘(𝑗 + 1)) + (𝑆𝑗)) / 2) + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = (𝑆‘(𝑗 + 1)) ∧ ((((𝑆‘(𝑗 + 1)) + (𝑆𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = (𝑆𝑗)))
196191, 190, 195syl2anc 696 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → (((((𝑆‘(𝑗 + 1)) + (𝑆𝑗)) / 2) + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = (𝑆‘(𝑗 + 1)) ∧ ((((𝑆‘(𝑗 + 1)) + (𝑆𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = (𝑆𝑗)))
197196simprd 482 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → ((((𝑆‘(𝑗 + 1)) + (𝑆𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = (𝑆𝑗))
198194, 197eqtrd 2782 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → ((((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = (𝑆𝑗))
199190, 191addcld 10222 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + (𝑆‘(𝑗 + 1))) ∈ ℂ)
200199halfcld 11440 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) ∈ ℂ)
201111recnd 10231 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2) ∈ ℂ)
202200, 201, 190subsub23d 39967 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → (((((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = (𝑆𝑗) ↔ ((((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (𝑆𝑗)) = (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)))
203198, 202mpbid 222 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → ((((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (𝑆𝑗)) = (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
204200, 190, 201subaddd 10573 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → (((((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (𝑆𝑗)) = (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2) ↔ ((𝑆𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = (((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2)))
205203, 204mpbid 222 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = (((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2))
206 avglt2 11434 . . . . . . . . . . . 12 (((𝑆𝑗) ∈ ℝ ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ) → ((𝑆𝑗) < (𝑆‘(𝑗 + 1)) ↔ (((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) < (𝑆‘(𝑗 + 1))))
20742, 109, 206syl2anc 696 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) < (𝑆‘(𝑗 + 1)) ↔ (((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) < (𝑆‘(𝑗 + 1))))
208131, 207mpbid 222 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) < (𝑆‘(𝑗 + 1)))
209205, 208eqbrtrd 4814 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) < (𝑆‘(𝑗 + 1)))
210119, 172, 109, 189, 209lelttrd 10358 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑆‘(𝑗 + 1)))
211106, 210syl5eqbr 4827 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑍 < (𝑆‘(𝑗 + 1)))
212109rexrd 10252 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℝ*)
213 elico2 12401 . . . . . . . 8 (((𝑆𝑗) ∈ ℝ ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ*) → (𝑍 ∈ ((𝑆𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ (𝑍 ∈ ℝ ∧ (𝑆𝑗) ≤ 𝑍𝑍 < (𝑆‘(𝑗 + 1)))))
21442, 212, 213syl2anc 696 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑍 ∈ ((𝑆𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ (𝑍 ∈ ℝ ∧ (𝑆𝑗) ≤ 𝑍𝑍 < (𝑆‘(𝑗 + 1)))))
215120, 171, 211, 214mpbir3and 1406 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑍 ∈ ((𝑆𝑗)[,)(𝑆‘(𝑗 + 1))))
216215adantr 472 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝑍 ∈ ((𝑆𝑗)[,)(𝑆‘(𝑗 + 1))))
217114ad2antrr 764 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐴 ∈ ℝ)
218113simp2d 1135 . . . . . . . . 9 (𝜑𝐵 ∈ ℝ)
219218ad2antrr 764 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐵 ∈ ℝ)
220113simp3d 1136 . . . . . . . . 9 (𝜑𝐴 < 𝐵)
221220ad2antrr 764 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐴 < 𝐵)
22242adantr 472 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝑆𝑗) ∈ ℝ)
223 simpr 479 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) = 𝐵)
224169, 106syl6breqr 4834 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) < 𝑍)
225218, 114resubcld 10621 . . . . . . . . . . . . . 14 (𝜑 → (𝐵𝐴) ∈ ℝ)
22611, 225syl5eqel 2831 . . . . . . . . . . . . 13 (𝜑𝑇 ∈ ℝ)
227226adantr 472 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑇 ∈ ℝ)
228111adantr 472 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2) ∈ ℝ)
229116ad2antrr 764 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ)
230110adantr 472 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) ∈ ℝ)
231115ad2antrr 764 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑄‘1) − 𝐴) ∈ ℝ)
232182a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → 2 ∈ ℝ+)
233 simpr 479 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴))
234230, 231, 232, 233ltdiv1dd 12093 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2) < (((𝑄‘1) − 𝐴) / 2))
235228, 229, 234ltled 10348 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2) ≤ (((𝑄‘1) − 𝐴) / 2))
236174, 235eqbrtrd 4814 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2))
237178adantl 473 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) − 𝐴) / 2))
238116leidd 10757 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ≤ (((𝑄‘1) − 𝐴) / 2))
239238adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑄‘1) − 𝐴) / 2) ≤ (((𝑄‘1) − 𝐴) / 2))
240237, 239eqbrtrd 4814 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2))
241240adantlr 753 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2))
242236, 241pm2.61dan 867 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2))
243225rehalfcld 11442 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵𝐴) / 2) ∈ ℝ)
244182a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 2 ∈ ℝ+)
245114rexrd 10252 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ ℝ*)
246218rexrd 10252 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ∈ ℝ*)
2473, 2, 1fourierdlem15 40811 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
248247, 103ffvelrnd 6511 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑄‘1) ∈ (𝐴[,]𝐵))
249 iccleub 12393 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝑄‘1) ∈ (𝐴[,]𝐵)) → (𝑄‘1) ≤ 𝐵)
250245, 246, 248, 249syl3anc 1463 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑄‘1) ≤ 𝐵)
251112, 218, 114, 250lesub1dd 10806 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑄‘1) − 𝐴) ≤ (𝐵𝐴))
252115, 225, 244, 251lediv1dd 12094 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ≤ ((𝐵𝐴) / 2))
25311eqcomi 2757 . . . . . . . . . . . . . . . . . 18 (𝐵𝐴) = 𝑇
254253oveq1i 6811 . . . . . . . . . . . . . . . . 17 ((𝐵𝐴) / 2) = (𝑇 / 2)
255114, 218posdifd 10777 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
256220, 255mpbid 222 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 < (𝐵𝐴))
257256, 11syl6breqr 4834 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 < 𝑇)
258226, 257elrpd 12033 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 ∈ ℝ+)
259 rphalflt 12024 . . . . . . . . . . . . . . . . . 18 (𝑇 ∈ ℝ+ → (𝑇 / 2) < 𝑇)
260258, 259syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑇 / 2) < 𝑇)
261254, 260syl5eqbr 4827 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵𝐴) / 2) < 𝑇)
262116, 243, 226, 252, 261lelttrd 10358 . . . . . . . . . . . . . . 15 (𝜑 → (((𝑄‘1) − 𝐴) / 2) < 𝑇)
263116, 226, 262ltled 10348 . . . . . . . . . . . . . 14 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ≤ 𝑇)
264263adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑄‘1) − 𝐴) / 2) ≤ 𝑇)
265118, 117, 227, 242, 264letrd 10357 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ 𝑇)
266118, 227, 42, 265leadd2dd 10805 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) ≤ ((𝑆𝑗) + 𝑇))
267106, 266syl5eqbr 4827 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑍 ≤ ((𝑆𝑗) + 𝑇))
26842rexrd 10252 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ∈ ℝ*)
26942, 227readdcld 10232 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + 𝑇) ∈ ℝ)
270 elioc2 12400 . . . . . . . . . . 11 (((𝑆𝑗) ∈ ℝ* ∧ ((𝑆𝑗) + 𝑇) ∈ ℝ) → (𝑍 ∈ ((𝑆𝑗)(,]((𝑆𝑗) + 𝑇)) ↔ (𝑍 ∈ ℝ ∧ (𝑆𝑗) < 𝑍𝑍 ≤ ((𝑆𝑗) + 𝑇))))
271268, 269, 270syl2anc 696 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑍 ∈ ((𝑆𝑗)(,]((𝑆𝑗) + 𝑇)) ↔ (𝑍 ∈ ℝ ∧ (𝑆𝑗) < 𝑍𝑍 ≤ ((𝑆𝑗) + 𝑇))))
272120, 224, 267, 271mpbir3and 1406 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑍 ∈ ((𝑆𝑗)(,]((𝑆𝑗) + 𝑇)))
273272adantr 472 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝑍 ∈ ((𝑆𝑗)(,]((𝑆𝑗) + 𝑇)))
274217, 219, 221, 11, 12, 222, 223, 273fourierdlem26 40822 . . . . . . 7 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸𝑍) = (𝐴 + (𝑍 − (𝑆𝑗))))
275106a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑍 = ((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
276275oveq1d 6816 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑍 − (𝑆𝑗)) = (((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆𝑗)))
277276oveq2d 6817 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐴 + (𝑍 − (𝑆𝑗))) = (𝐴 + (((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆𝑗))))
278277adantr 472 . . . . . . 7 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐴 + (𝑍 − (𝑆𝑗))) = (𝐴 + (((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆𝑗))))
279118recnd 10231 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ∈ ℂ)
280190, 279pncan2d 10557 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆𝑗)) = if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)))
281280oveq2d 6817 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐴 + (((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆𝑗))) = (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
282281adantr 472 . . . . . . 7 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐴 + (((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆𝑗))) = (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
283274, 278, 2823eqtrd 2786 . . . . . 6 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸𝑍) = (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
284173oveq2d 6817 . . . . . . . . . 10 (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)))
285284adantl 473 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)))
286114adantr 472 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ℝ)
287286, 111readdcld 10232 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) ∈ ℝ)
288287adantr 472 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) ∈ ℝ)
289286, 117readdcld 10232 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) ∈ ℝ)
290289adantr 472 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) ∈ ℝ)
291112ad2antrr 764 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝑄‘1) ∈ ℝ)
292114ad2antrr 764 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → 𝐴 ∈ ℝ)
293228, 229, 292, 234ltadd2dd 10359 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) < (𝐴 + (((𝑄‘1) − 𝐴) / 2)))
294112recnd 10231 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘1) ∈ ℂ)
295114recnd 10231 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ ℂ)
296 halfaddsub 11428 . . . . . . . . . . . . . . . 16 (((𝑄‘1) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((((𝑄‘1) + 𝐴) / 2) + (((𝑄‘1) − 𝐴) / 2)) = (𝑄‘1) ∧ ((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) = 𝐴))
297294, 295, 296syl2anc 696 . . . . . . . . . . . . . . 15 (𝜑 → (((((𝑄‘1) + 𝐴) / 2) + (((𝑄‘1) − 𝐴) / 2)) = (𝑄‘1) ∧ ((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) = 𝐴))
298297simprd 482 . . . . . . . . . . . . . 14 (𝜑 → ((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) = 𝐴)
299298oveq1d 6816 . . . . . . . . . . . . 13 (𝜑 → (((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) + (((𝑄‘1) − 𝐴) / 2)) = (𝐴 + (((𝑄‘1) − 𝐴) / 2)))
300112, 114readdcld 10232 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑄‘1) + 𝐴) ∈ ℝ)
301300rehalfcld 11442 . . . . . . . . . . . . . . 15 (𝜑 → (((𝑄‘1) + 𝐴) / 2) ∈ ℝ)
302301recnd 10231 . . . . . . . . . . . . . 14 (𝜑 → (((𝑄‘1) + 𝐴) / 2) ∈ ℂ)
303116recnd 10231 . . . . . . . . . . . . . 14 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ∈ ℂ)
304302, 303npcand 10559 . . . . . . . . . . . . 13 (𝜑 → (((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) + (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) + 𝐴) / 2))
305299, 304eqtr3d 2784 . . . . . . . . . . . 12 (𝜑 → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) + 𝐴) / 2))
306112, 112readdcld 10232 . . . . . . . . . . . . . 14 (𝜑 → ((𝑄‘1) + (𝑄‘1)) ∈ ℝ)
307114, 112, 112, 161ltadd2dd 10359 . . . . . . . . . . . . . 14 (𝜑 → ((𝑄‘1) + 𝐴) < ((𝑄‘1) + (𝑄‘1)))
308300, 306, 244, 307ltdiv1dd 12093 . . . . . . . . . . . . 13 (𝜑 → (((𝑄‘1) + 𝐴) / 2) < (((𝑄‘1) + (𝑄‘1)) / 2))
3092942timesd 11438 . . . . . . . . . . . . . . . 16 (𝜑 → (2 · (𝑄‘1)) = ((𝑄‘1) + (𝑄‘1)))
310309eqcomd 2754 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑄‘1) + (𝑄‘1)) = (2 · (𝑄‘1)))
311310oveq1d 6816 . . . . . . . . . . . . . 14 (𝜑 → (((𝑄‘1) + (𝑄‘1)) / 2) = ((2 · (𝑄‘1)) / 2))
312 2cnd 11256 . . . . . . . . . . . . . . 15 (𝜑 → 2 ∈ ℂ)
313 2ne0 11276 . . . . . . . . . . . . . . . 16 2 ≠ 0
314313a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 2 ≠ 0)
315294, 312, 314divcan3d 10969 . . . . . . . . . . . . . 14 (𝜑 → ((2 · (𝑄‘1)) / 2) = (𝑄‘1))
316311, 315eqtrd 2782 . . . . . . . . . . . . 13 (𝜑 → (((𝑄‘1) + (𝑄‘1)) / 2) = (𝑄‘1))
317308, 316breqtrd 4818 . . . . . . . . . . . 12 (𝜑 → (((𝑄‘1) + 𝐴) / 2) < (𝑄‘1))
318305, 317eqbrtrd 4814 . . . . . . . . . . 11 (𝜑 → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) < (𝑄‘1))
319318ad2antrr 764 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) < (𝑄‘1))
320288, 290, 291, 293, 319lttrd 10361 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) < (𝑄‘1))
321285, 320eqbrtrd 4814 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1))
322178oveq2d 6817 . . . . . . . . . 10 (¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑄‘1) − 𝐴) / 2)))
323322adantl 473 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑄‘1) − 𝐴) / 2)))
324318ad2antrr 764 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) < (𝑄‘1))
325323, 324eqbrtrd 4814 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1))
326321, 325pm2.61dan 867 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1))
327326adantr 472 . . . . . 6 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1))
328283, 327eqbrtrd 4814 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸𝑍) < (𝑄‘1))
329 eqid 2748 . . . . 5 ((𝑄‘1) − ((𝐸𝑍) − 𝑍)) = ((𝑄‘1) − ((𝐸𝑍) − 𝑍))
33011, 3, 90, 91, 92, 93, 94, 24, 25, 26, 27, 12, 104, 105, 216, 328, 329fourierdlem63 40858 . . . 4 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘1))
33114a1i 11 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < )))
33257adantl 473 . . . . . . . . 9 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ 𝑥 = (𝑆𝑗)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ))
33360a1i 11 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ V)
334331, 332, 222, 333fvmptd 6438 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐼‘(𝑆𝑗)) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ))
335 fveq2 6340 . . . . . . . . . . . . 13 ((𝐸‘(𝑆𝑗)) = 𝐵 → (𝐿‘(𝐸‘(𝑆𝑗))) = (𝐿𝐵))
33613a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)))
337 iftrue 4224 . . . . . . . . . . . . . . 15 (𝑦 = 𝐵 → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝐴)
338337adantl 473 . . . . . . . . . . . . . 14 ((𝜑𝑦 = 𝐵) → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝐴)
339 ubioc1 12391 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵) → 𝐵 ∈ (𝐴(,]𝐵))
340245, 246, 220, 339syl3anc 1463 . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ (𝐴(,]𝐵))
341336, 338, 340, 114fvmptd 6438 . . . . . . . . . . . . 13 (𝜑 → (𝐿𝐵) = 𝐴)
342335, 341sylan9eqr 2804 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐿‘(𝐸‘(𝑆𝑗))) = 𝐴)
343342breq2d 4804 . . . . . . . . . . 11 ((𝜑 ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → ((𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗))) ↔ (𝑄𝑖) ≤ 𝐴))
344343rabbidv 3317 . . . . . . . . . 10 ((𝜑 ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} = {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴})
345344supeq1d 8505 . . . . . . . . 9 ((𝜑 ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}, ℝ, < ))
346345adantlr 753 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}, ℝ, < ))
347 simpl 474 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}) → 𝜑)
348 elrabi 3487 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴} → 𝑗 ∈ (0..^𝑀))
349348adantl 473 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}) → 𝑗 ∈ (0..^𝑀))
350 fveq2 6340 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑗 → (𝑄𝑖) = (𝑄𝑗))
351350breq1d 4802 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → ((𝑄𝑖) ≤ 𝐴 ↔ (𝑄𝑗) ≤ 𝐴))
352351elrab 3492 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴} ↔ (𝑗 ∈ (0..^𝑀) ∧ (𝑄𝑗) ≤ 𝐴))
353352simprbi 483 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴} → (𝑄𝑗) ≤ 𝐴)
354353adantl 473 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}) → (𝑄𝑗) ≤ 𝐴)
355 simp3 1130 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑀) ∧ (𝑄𝑗) ≤ 𝐴) → (𝑄𝑗) ≤ 𝐴)
356114ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝐴 ∈ ℝ)
357112ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝑄‘1) ∈ ℝ)
3589adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
35918sselda 3732 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0..^𝑀)) → 𝑗 ∈ (0...𝑀))
360358, 359ffvelrnd 6511 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑄𝑗) ∈ ℝ)
361360adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝑄𝑗) ∈ ℝ)
362161ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝐴 < (𝑄‘1))
363 1zzd 11571 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 1 ∈ ℤ)
364 elfzoelz 12635 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℤ)
365364ad2antlr 765 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝑗 ∈ ℤ)
366 1e0p1 11715 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 = (0 + 1)
367 simpr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → ¬ 𝑗 ≤ 0)
368 0red 10204 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 0 ∈ ℝ)
369365zred 11645 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝑗 ∈ ℝ)
370368, 369ltnled 10347 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (0 < 𝑗 ↔ ¬ 𝑗 ≤ 0))
371367, 370mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 0 < 𝑗)
372 0zd 11552 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 0 ∈ ℤ)
373 zltp1le 11590 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((0 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (0 < 𝑗 ↔ (0 + 1) ≤ 𝑗))
374372, 365, 373syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (0 < 𝑗 ↔ (0 + 1) ≤ 𝑗))
375371, 374mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (0 + 1) ≤ 𝑗)
376366, 375syl5eqbr 4827 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 1 ≤ 𝑗)
377 eluz2 11856 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (ℤ‘1) ↔ (1 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 1 ≤ 𝑗))
378363, 365, 376, 377syl3anbrc 1407 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝑗 ∈ (ℤ‘1))
3799ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑄:(0...𝑀)⟶ℝ)
380 0red 10204 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (1...𝑗) → 0 ∈ ℝ)
381 elfzelz 12506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 𝑙 ∈ ℤ)
382381zred 11645 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (1...𝑗) → 𝑙 ∈ ℝ)
383 1red 10218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 1 ∈ ℝ)
384 0lt1 10713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 0 < 1
385384a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 0 < 1)
386 elfzle1 12508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 1 ≤ 𝑙)
387380, 383, 382, 385, 386ltletrd 10360 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (1...𝑗) → 0 < 𝑙)
388380, 382, 387ltled 10348 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑙 ∈ (1...𝑗) → 0 ≤ 𝑙)
389388adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 0 ≤ 𝑙)
390382adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ∈ ℝ)
391100zred 11645 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑀 ∈ ℝ)
392391ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑀 ∈ ℝ)
393364zred 11645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℝ)
394393ad2antlr 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑗 ∈ ℝ)
395 elfzle2 12509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 𝑙𝑗)
396395adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙𝑗)
397 elfzolt2 12644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0..^𝑀) → 𝑗 < 𝑀)
398397ad2antlr 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑗 < 𝑀)
399390, 394, 392, 396, 398lelttrd 10358 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 < 𝑀)
400390, 392, 399ltled 10348 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙𝑀)
401381adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ∈ ℤ)
402 0zd 11552 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 0 ∈ ℤ)
403100ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑀 ∈ ℤ)
404 elfz 12496 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑙 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑙 ∈ (0...𝑀) ↔ (0 ≤ 𝑙𝑙𝑀)))
405401, 402, 403, 404syl3anc 1463 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → (𝑙 ∈ (0...𝑀) ↔ (0 ≤ 𝑙𝑙𝑀)))
406389, 400, 405mpbir2and 995 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ∈ (0...𝑀))
407379, 406ffvelrnd 6511 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → (𝑄𝑙) ∈ ℝ)
408407adantlr 753 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) ∧ 𝑙 ∈ (1...𝑗)) → (𝑄𝑙) ∈ ℝ)
4099ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑄:(0...𝑀)⟶ℝ)
410 0zd 11552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ∈ ℤ)
411100ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℤ)
412 elfzelz 12506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 𝑙 ∈ ℤ)
413412adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℤ)
414410, 411, 4133jca 1403 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑙 ∈ ℤ))
415 0red 10204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 0 ∈ ℝ)
416412zred 11645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 𝑙 ∈ ℝ)
417 1red 10218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑙 ∈ (1...(𝑗 − 1)) → 1 ∈ ℝ)
418384a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑙 ∈ (1...(𝑗 − 1)) → 0 < 1)
419 elfzle1 12508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑙 ∈ (1...(𝑗 − 1)) → 1 ≤ 𝑙)
420415, 417, 416, 418, 419ltletrd 10360 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 0 < 𝑙)
421415, 416, 420ltled 10348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...(𝑗 − 1)) → 0 ≤ 𝑙)
422421adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ≤ 𝑙)
423413zred 11645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℝ)
424391ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℝ)
425393ad2antlr 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 ∈ ℝ)
426416adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℝ)
427 peano2rem 10511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 ∈ ℝ → (𝑗 − 1) ∈ ℝ)
428393, 427syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑗 ∈ (0..^𝑀) → (𝑗 − 1) ∈ ℝ)
429428adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑗 − 1) ∈ ℝ)
430393adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 ∈ ℝ)
431 elfzle2 12509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑙 ∈ (1...(𝑗 − 1)) → 𝑙 ≤ (𝑗 − 1))
432431adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ≤ (𝑗 − 1))
433430ltm1d 11119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑗 − 1) < 𝑗)
434426, 429, 430, 432, 433lelttrd 10358 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑗)
435434adantll 752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑗)
436397ad2antlr 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 < 𝑀)
437423, 425, 424, 435, 436lttrd 10361 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑀)
438423, 424, 437ltled 10348 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙𝑀)
439414, 422, 438jca32 559 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑙 ∈ ℤ) ∧ (0 ≤ 𝑙𝑙𝑀)))
440 elfz2 12497 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑙 ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑙 ∈ ℤ) ∧ (0 ≤ 𝑙𝑙𝑀)))
441439, 440sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ (0...𝑀))
442409, 441ffvelrnd 6511 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄𝑙) ∈ ℝ)
443413peano2zd 11648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ∈ ℤ)
444410, 411, 4433jca 1403 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑙 + 1) ∈ ℤ))
445416, 417readdcld 10232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) ∈ ℝ)
446416, 417, 420, 418addgt0d 10765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 0 < (𝑙 + 1))
447415, 445, 446ltled 10348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...(𝑗 − 1)) → 0 ≤ (𝑙 + 1))
448447adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ≤ (𝑙 + 1))
449445adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ∈ ℝ)
450445recnd 10231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) ∈ ℂ)
451 1cnd 10219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑙 ∈ (1...(𝑗 − 1)) → 1 ∈ ℂ)
452450, 451npcand 10559 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑙 ∈ (1...(𝑗 − 1)) → (((𝑙 + 1) − 1) + 1) = (𝑙 + 1))
453452eqcomd 2754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) = (((𝑙 + 1) − 1) + 1))
454453adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) = (((𝑙 + 1) − 1) + 1))
455 peano2re 10372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑙 ∈ ℝ → (𝑙 + 1) ∈ ℝ)
456 peano2rem 10511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑙 + 1) ∈ ℝ → ((𝑙 + 1) − 1) ∈ ℝ)
457426, 455, 4563syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((𝑙 + 1) − 1) ∈ ℝ)
458 peano2re 10372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑗 − 1) ∈ ℝ → ((𝑗 − 1) + 1) ∈ ℝ)
459 peano2rem 10511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑗 − 1) + 1) ∈ ℝ → (((𝑗 − 1) + 1) − 1) ∈ ℝ)
460429, 458, 4593syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (((𝑗 − 1) + 1) − 1) ∈ ℝ)
461 1red 10218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 1 ∈ ℝ)
462 elfzel2 12504 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑗 − 1) ∈ ℤ)
463462zred 11645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑗 − 1) ∈ ℝ)
464463, 417readdcld 10232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑙 ∈ (1...(𝑗 − 1)) → ((𝑗 − 1) + 1) ∈ ℝ)
465416, 463, 417, 431leadd1dd 10804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) ≤ ((𝑗 − 1) + 1))
466445, 464, 417, 465lesub1dd 10806 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑙 ∈ (1...(𝑗 − 1)) → ((𝑙 + 1) − 1) ≤ (((𝑗 − 1) + 1) − 1))
467466adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((𝑙 + 1) − 1) ≤ (((𝑗 − 1) + 1) − 1))
468457, 460, 461, 467leadd1dd 10804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (((𝑙 + 1) − 1) + 1) ≤ ((((𝑗 − 1) + 1) − 1) + 1))
469 peano2zm 11583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑗 ∈ ℤ → (𝑗 − 1) ∈ ℤ)
470364, 469syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑗 ∈ (0..^𝑀) → (𝑗 − 1) ∈ ℤ)
471470peano2zd 11648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑗 ∈ (0..^𝑀) → ((𝑗 − 1) + 1) ∈ ℤ)
472471zcnd 11646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ (0..^𝑀) → ((𝑗 − 1) + 1) ∈ ℂ)
473 1cnd 10219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ (0..^𝑀) → 1 ∈ ℂ)
474472, 473npcand 10559 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 ∈ (0..^𝑀) → ((((𝑗 − 1) + 1) − 1) + 1) = ((𝑗 − 1) + 1))
475393recnd 10231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℂ)
476475, 473npcand 10559 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 ∈ (0..^𝑀) → ((𝑗 − 1) + 1) = 𝑗)
477474, 476eqtrd 2782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 ∈ (0..^𝑀) → ((((𝑗 − 1) + 1) − 1) + 1) = 𝑗)
478477adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((((𝑗 − 1) + 1) − 1) + 1) = 𝑗)
479468, 478breqtrd 4818 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (((𝑙 + 1) − 1) + 1) ≤ 𝑗)
480454, 479eqbrtrd 4814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ≤ 𝑗)
481480adantll 752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ≤ 𝑗)
482449, 425, 424, 481, 436lelttrd 10358 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) < 𝑀)
483449, 424, 482ltled 10348 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ≤ 𝑀)
484444, 448, 483jca32 559 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑙 + 1) ∈ ℤ) ∧ (0 ≤ (𝑙 + 1) ∧ (𝑙 + 1) ≤ 𝑀)))
485 elfz2 12497 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑙 + 1) ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑙 + 1) ∈ ℤ) ∧ (0 ≤ (𝑙 + 1) ∧ (𝑙 + 1) ≤ 𝑀)))
486484, 485sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ∈ (0...𝑀))
487409, 486ffvelrnd 6511 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄‘(𝑙 + 1)) ∈ ℝ)
488 simpll 807 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝜑)
489 0zd 11552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ∈ ℤ)
490412adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℤ)
491421adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ≤ 𝑙)
492 eluz2 11856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (ℤ‘0) ↔ (0 ∈ ℤ ∧ 𝑙 ∈ ℤ ∧ 0 ≤ 𝑙))
493489, 490, 491, 492syl3anbrc 1407 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ (ℤ‘0))
494 elfzoel2 12634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0..^𝑀) → 𝑀 ∈ ℤ)
495494adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℤ)
496495zred 11645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℝ)
497397adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 < 𝑀)
498426, 430, 496, 434, 497lttrd 10361 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑀)
499 elfzo2 12638 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (0..^𝑀) ↔ (𝑙 ∈ (ℤ‘0) ∧ 𝑀 ∈ ℤ ∧ 𝑙 < 𝑀))
500493, 495, 498, 499syl3anbrc 1407 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ (0..^𝑀))
501500adantll 752 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ (0..^𝑀))
502 eleq1 2815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 = 𝑙 → (𝑖 ∈ (0..^𝑀) ↔ 𝑙 ∈ (0..^𝑀)))
503502anbi2d 742 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 = 𝑙 → ((𝜑𝑖 ∈ (0..^𝑀)) ↔ (𝜑𝑙 ∈ (0..^𝑀))))
504 fveq2 6340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 = 𝑙 → (𝑄𝑖) = (𝑄𝑙))
505 oveq1 6808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 = 𝑙 → (𝑖 + 1) = (𝑙 + 1))
506505fveq2d 6344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 = 𝑙 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑙 + 1)))
507504, 506breq12d 4805 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 = 𝑙 → ((𝑄𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄𝑙) < (𝑄‘(𝑙 + 1))))
508503, 507imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 = 𝑙 → (((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑𝑙 ∈ (0..^𝑀)) → (𝑄𝑙) < (𝑄‘(𝑙 + 1)))))
509508, 152chvarv 2396 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑙 ∈ (0..^𝑀)) → (𝑄𝑙) < (𝑄‘(𝑙 + 1)))
510488, 501, 509syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄𝑙) < (𝑄‘(𝑙 + 1)))
511442, 487, 510ltled 10348 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄𝑙) ≤ (𝑄‘(𝑙 + 1)))
512511adantlr 753 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄𝑙) ≤ (𝑄‘(𝑙 + 1)))
513378, 408, 512monoord 12996 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝑄‘1) ≤ (𝑄𝑗))
514356, 357, 361, 362, 513ltletrd 10360 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝐴 < (𝑄𝑗))
515356, 361ltnled 10347 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝐴 < (𝑄𝑗) ↔ ¬ (𝑄𝑗) ≤ 𝐴))
516514, 515mpbid 222 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → ¬ (𝑄𝑗) ≤ 𝐴)
517516ex 449 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑀)) → (¬ 𝑗 ≤ 0 → ¬ (𝑄𝑗) ≤ 𝐴))
5185173adant3 1124 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑀) ∧ (𝑄𝑗) ≤ 𝐴) → (¬ 𝑗 ≤ 0 → ¬ (𝑄𝑗) ≤ 𝐴))
519355, 518mt4d 152 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑀) ∧ (𝑄𝑗) ≤ 𝐴) → 𝑗 ≤ 0)
520 elfzole1 12643 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0..^𝑀) → 0 ≤ 𝑗)
5215203ad2ant2 1126 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑀) ∧ (𝑄𝑗) ≤ 𝐴) → 0 ≤ 𝑗)
5223933ad2ant2 1126 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑀) ∧ (𝑄𝑗) ≤ 𝐴) → 𝑗 ∈ ℝ)
523 0red 10204 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑀) ∧ (𝑄𝑗) ≤ 𝐴) → 0 ∈ ℝ)
524522, 523letri3d 10342 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑀) ∧ (𝑄𝑗) ≤ 𝐴) → (𝑗 = 0 ↔ (𝑗 ≤ 0 ∧ 0 ≤ 𝑗)))
525519, 521, 524mpbir2and 995 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑀) ∧ (𝑄𝑗) ≤ 𝐴) → 𝑗 = 0)
526347, 349, 354, 525syl3anc 1463 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}) → 𝑗 = 0)
527 velsn 4325 . . . . . . . . . . . . . . 15 (𝑗 ∈ {0} ↔ 𝑗 = 0)
528526, 527sylibr 224 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}) → 𝑗 ∈ {0})
529528ralrimiva 3092 . . . . . . . . . . . . 13 (𝜑 → ∀𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}𝑗 ∈ {0})
530 dfss3 3721 . . . . . . . . . . . . 13 ({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴} ⊆ {0} ↔ ∀𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}𝑗 ∈ {0})
531529, 530sylibr 224 . . . . . . . . . . . 12 (𝜑 → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴} ⊆ {0})
532157, 114eqeltrd 2827 . . . . . . . . . . . . . . 15 (𝜑 → (𝑄‘0) ∈ ℝ)
533532, 157eqled 10303 . . . . . . . . . . . . . 14 (𝜑 → (𝑄‘0) ≤ 𝐴)
534145breq1d 4802 . . . . . . . . . . . . . . 15 (𝑖 = 0 → ((𝑄𝑖) ≤ 𝐴 ↔ (𝑄‘0) ≤ 𝐴))
535534elrab 3492 . . . . . . . . . . . . . 14 (0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴} ↔ (0 ∈ (0..^𝑀) ∧ (𝑄‘0) ≤ 𝐴))
536141, 533, 535sylanbrc 701 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴})
537536snssd 4473 . . . . . . . . . . . 12 (𝜑 → {0} ⊆ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴})
538531, 537eqssd 3749 . . . . . . . . . . 11 (𝜑 → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴} = {0})
539538supeq1d 8505 . . . . . . . . . 10 (𝜑 → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}, ℝ, < ) = sup({0}, ℝ, < ))
540 supsn 8531 . . . . . . . . . . . 12 (( < Or ℝ ∧ 0 ∈ ℝ) → sup({0}, ℝ, < ) = 0)
54159, 142, 540mp2an 710 . . . . . . . . . . 11 sup({0}, ℝ, < ) = 0
542541a1i 11 . . . . . . . . . 10 (𝜑 → sup({0}, ℝ, < ) = 0)
543539, 542eqtrd 2782 . . . . . . . . 9 (𝜑 → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}, ℝ, < ) = 0)
544543ad2antrr 764 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}, ℝ, < ) = 0)
545334, 346, 5443eqtrd 2786 . . . . . . 7 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐼‘(𝑆𝑗)) = 0)
546545oveq1d 6816 . . . . . 6 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → ((𝐼‘(𝑆𝑗)) + 1) = (0 + 1))
547546fveq2d 6344 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) = (𝑄‘(0 + 1)))
548547, 159syl6req 2799 . . . 4 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝑄‘1) = (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
549330, 548breqtrd 4818 . . 3 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
55065adantr 472 . . . 4 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝜑 ∧ (𝑆𝑗) ∈ ℝ))
551 simplr 809 . . . 4 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝑗 ∈ (0..^𝑁))
55213a1i 11 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)))
553 simpr 479 . . . . . . . . . . . . . . . 16 ((¬ (𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → 𝑦 = (𝐸‘(𝑆𝑗)))
554 neqne 2928 . . . . . . . . . . . . . . . . 17 (¬ (𝐸‘(𝑆𝑗)) = 𝐵 → (𝐸‘(𝑆𝑗)) ≠ 𝐵)
555554adantr 472 . . . . . . . . . . . . . . . 16 ((¬ (𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → (𝐸‘(𝑆𝑗)) ≠ 𝐵)
556553, 555eqnetrd 2987 . . . . . . . . . . . . . . 15 ((¬ (𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → 𝑦𝐵)
557556neneqd 2925 . . . . . . . . . . . . . 14 ((¬ (𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → ¬ 𝑦 = 𝐵)
558557iffalsed 4229 . . . . . . . . . . . . 13 ((¬ (𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝑦)
559558, 553eqtrd 2782 . . . . . . . . . . . 12 ((¬ (𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = (𝐸‘(𝑆𝑗)))
560559adantll 752 . . . . . . . . . . 11 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ 𝑦 = (𝐸‘(𝑆𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = (𝐸‘(𝑆𝑗)))
561114, 218, 220, 11, 12fourierdlem4 40800 . . . . . . . . . . . . . 14 (𝜑𝐸:ℝ⟶(𝐴(,]𝐵))
562561adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐸:ℝ⟶(𝐴(,]𝐵))
563562, 42ffvelrnd 6511 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆𝑗)) ∈ (𝐴(,]𝐵))
564563adantr 472 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) ∈ (𝐴(,]𝐵))
565552, 560, 564, 564fvmptd 6438 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐿‘(𝐸‘(𝑆𝑗))) = (𝐸‘(𝑆𝑗)))
566565eqcomd 2754 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) = (𝐿‘(𝐸‘(𝑆𝑗))))
567114, 218, 220, 13fourierdlem17 40813 . . . . . . . . . . . . 13 (𝜑𝐿:(𝐴(,]𝐵)⟶(𝐴[,]𝐵))
568567adantr 472 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐿:(𝐴(,]𝐵)⟶(𝐴[,]𝐵))
569114, 218iccssred 40199 . . . . . . . . . . . . 13 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
570569adantr 472 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐴[,]𝐵) ⊆ ℝ)
571568, 570fssd 6206 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐿:(𝐴(,]𝐵)⟶ℝ)
572571, 563ffvelrnd 6511 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐿‘(𝐸‘(𝑆𝑗))) ∈ ℝ)
573572adantr 472 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐿‘(𝐸‘(𝑆𝑗))) ∈ ℝ)
574566, 573eqeltrd 2827 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) ∈ ℝ)
575218ad2antrr 764 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐵 ∈ ℝ)
576245adantr 472 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ℝ*)
577218adantr 472 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐵 ∈ ℝ)
578 elioc2 12400 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → ((𝐸‘(𝑆𝑗)) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘(𝑆𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆𝑗)) ∧ (𝐸‘(𝑆𝑗)) ≤ 𝐵)))
579576, 577, 578syl2anc 696 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆𝑗)) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘(𝑆𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆𝑗)) ∧ (𝐸‘(𝑆𝑗)) ≤ 𝐵)))
580563, 579mpbid 222 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆𝑗)) ∧ (𝐸‘(𝑆𝑗)) ≤ 𝐵))
581580simp3d 1136 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆𝑗)) ≤ 𝐵)
582581adantr 472 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) ≤ 𝐵)
583554necomd 2975 . . . . . . . . 9 (¬ (𝐸‘(𝑆𝑗)) = 𝐵𝐵 ≠ (𝐸‘(𝑆𝑗)))
584583adantl 473 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐵 ≠ (𝐸‘(𝑆𝑗)))
585574, 575, 582, 584leneltd 10354 . . . . . . 7 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) < 𝐵)
586585adantr 472 . . . . . 6 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆𝑗)) < 𝐵)
587 oveq1 6808 . . . . . . . . . . 11 ((𝐼‘(𝑆𝑗)) = (𝑀 − 1) → ((𝐼‘(𝑆𝑗)) + 1) = ((𝑀 − 1) + 1))
5882nncnd 11199 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℂ)
589 1cnd 10219 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℂ)
590588, 589npcand 10559 . . . . . . . . . . 11 (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
591587, 590sylan9eqr 2804 . . . . . . . . . 10 ((𝜑 ∧ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆𝑗)) + 1) = 𝑀)
592591fveq2d 6344 . . . . . . . . 9 ((𝜑 ∧ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) = (𝑄𝑀))
593156simprd 482 . . . . . . . . . 10 (𝜑 → (𝑄𝑀) = 𝐵)
594593adantr 472 . . . . . . . . 9 ((𝜑 ∧ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝑄𝑀) = 𝐵)
595592, 594eqtr2d 2783 . . . . . . . 8 ((𝜑 ∧ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → 𝐵 = (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
596595adantlr 753 . . . . . . 7 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → 𝐵 = (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
597596adantlr 753 . . . . . 6 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → 𝐵 = (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
598586, 597breqtrd 4818 . . . . 5 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
599566adantr 472 . . . . . 6 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆𝑗)) = (𝐿‘(𝐸‘(𝑆𝑗))))
600 ssrab2 3816 . . . . . . . . . . . . 13 {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ⊆ (0..^𝑀)
601 fzssz 12507 . . . . . . . . . . . . . . 15 (0...𝑀) ⊆ ℤ
60217, 601sstri 3741 . . . . . . . . . . . . . 14 (0..^𝑀) ⊆ ℤ
603 zssre 11547 . . . . . . . . . . . . . 14 ℤ ⊆ ℝ
604602, 603sstri 3741 . . . . . . . . . . . . 13 (0..^𝑀) ⊆ ℝ
605600, 604sstri 3741 . . . . . . . . . . . 12 {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ⊆ ℝ
606605a1i 11 . . . . . . . . . . 11 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ⊆ ℝ)
60756neeq1d 2979 . . . . . . . . . . . . . . 15 (𝑥 = (𝑆𝑗) → ({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))} ≠ ∅ ↔ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ≠ ∅))
60867, 607imbi12d 333 . . . . . . . . . . . . . 14 (𝑥 = (𝑆𝑗) → (((𝜑𝑥 ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))} ≠ ∅) ↔ ((𝜑 ∧ (𝑆𝑗) ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ≠ ∅)))
609141adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → 0 ∈ (0..^𝑀))
610533ad2antrr 764 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ) ∧ (𝐸𝑥) = 𝐵) → (𝑄‘0) ≤ 𝐴)
611 iftrue 4224 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸𝑥) = 𝐵 → if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)) = 𝐴)
612611eqcomd 2754 . . . . . . . . . . . . . . . . . . . 20 ((𝐸𝑥) = 𝐵𝐴 = if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
613612adantl 473 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ) ∧ (𝐸𝑥) = 𝐵) → 𝐴 = if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
614610, 613breqtrd 4818 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ) ∧ (𝐸𝑥) = 𝐵) → (𝑄‘0) ≤ if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
615532adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → (𝑄‘0) ∈ ℝ)
616114adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ ℝ) → 𝐴 ∈ ℝ)
617616rexrd 10252 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ ℝ) → 𝐴 ∈ ℝ*)
618218adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ ℝ) → 𝐵 ∈ ℝ)
619 iocssre 12417 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
620617, 618, 619syl2anc 696 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
621561ffvelrnda 6510 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → (𝐸𝑥) ∈ (𝐴(,]𝐵))
622620, 621sseldd 3733 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → (𝐸𝑥) ∈ ℝ)
623157adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → (𝑄‘0) = 𝐴)
624 elioc2 12400 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → ((𝐸𝑥) ∈ (𝐴(,]𝐵) ↔ ((𝐸𝑥) ∈ ℝ ∧ 𝐴 < (𝐸𝑥) ∧ (𝐸𝑥) ≤ 𝐵)))
625617, 618, 624syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ ℝ) → ((𝐸𝑥) ∈ (𝐴(,]𝐵) ↔ ((𝐸𝑥) ∈ ℝ ∧ 𝐴 < (𝐸𝑥) ∧ (𝐸𝑥) ≤ 𝐵)))
626621, 625mpbid 222 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ ℝ) → ((𝐸𝑥) ∈ ℝ ∧ 𝐴 < (𝐸𝑥) ∧ (𝐸𝑥) ≤ 𝐵))
627626simp2d 1135 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → 𝐴 < (𝐸𝑥))
628623, 627eqbrtrd 4814 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → (𝑄‘0) < (𝐸𝑥))
629615, 622, 628ltled 10348 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → (𝑄‘0) ≤ (𝐸𝑥))
630629adantr 472 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ) ∧ ¬ (𝐸𝑥) = 𝐵) → (𝑄‘0) ≤ (𝐸𝑥))
631 iffalse 4227 . . . . . . . . . . . . . . . . . . . . 21 (¬ (𝐸𝑥) = 𝐵 → if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)) = (𝐸𝑥))
632631eqcomd 2754 . . . . . . . . . . . . . . . . . . . 20 (¬ (𝐸𝑥) = 𝐵 → (𝐸𝑥) = if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
633632adantl 473 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ) ∧ ¬ (𝐸𝑥) = 𝐵) → (𝐸𝑥) = if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
634630, 633breqtrd 4818 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ) ∧ ¬ (𝐸𝑥) = 𝐵) → (𝑄‘0) ≤ if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
635614, 634pm2.61dan 867 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → (𝑄‘0) ≤ if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
63613a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)))
637 eqeq1 2752 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐸𝑥) → (𝑦 = 𝐵 ↔ (𝐸𝑥) = 𝐵))
638 id 22 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐸𝑥) → 𝑦 = (𝐸𝑥))
639637, 638ifbieq2d 4243 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝐸𝑥) → if(𝑦 = 𝐵, 𝐴, 𝑦) = if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
640639adantl 473 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 = (𝐸𝑥)) → if(𝑦 = 𝐵, 𝐴, 𝑦) = if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
641616, 622ifcld 4263 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)) ∈ ℝ)
642636, 640, 621, 641fvmptd 6438 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → (𝐿‘(𝐸𝑥)) = if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
643635, 642breqtrrd 4820 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → (𝑄‘0) ≤ (𝐿‘(𝐸𝑥)))
644145breq1d 4802 . . . . . . . . . . . . . . . . 17 (𝑖 = 0 → ((𝑄𝑖) ≤ (𝐿‘(𝐸𝑥)) ↔ (𝑄‘0) ≤ (𝐿‘(𝐸𝑥))))
645644elrab 3492 . . . . . . . . . . . . . . . 16 (0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))} ↔ (0 ∈ (0..^𝑀) ∧ (𝑄‘0) ≤ (𝐿‘(𝐸𝑥))))
646609, 643, 645sylanbrc 701 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ) → 0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))})
647 ne0i 4052 . . . . . . . . . . . . . . 15 (0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))} → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))} ≠ ∅)
648646, 647syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))} ≠ ∅)
649608, 648vtoclg 3394 . . . . . . . . . . . . 13 ((𝑆𝑗) ∈ ℝ → ((𝜑 ∧ (𝑆𝑗) ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ≠ ∅))
65042, 65, 649sylc 65 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ≠ ∅)
651650ad2antrr 764 . . . . . . . . . . 11 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ≠ ∅)
652605a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ⊆ ℝ)
653 fzofi 12938 . . . . . . . . . . . . . . 15 (0..^𝑀) ∈ Fin
654 ssfi 8333 . . . . . . . . . . . . . . 15 (((0..^𝑀) ∈ Fin ∧ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ⊆ (0..^𝑀)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ∈ Fin)
655653, 600, 654mp2an 710 . . . . . . . . . . . . . 14 {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ∈ Fin
656655a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ∈ Fin)
657 fimaxre2 11132 . . . . . . . . . . . . 13 (({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ⊆ ℝ ∧ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}𝑙𝑥)
658652, 656, 657syl2anc 696 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}𝑙𝑥)
659658ad2antrr 764 . . . . . . . . . . 11 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}𝑙𝑥)
660 0red 10204 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → 0 ∈ ℝ)
661604, 47sseldi 3730 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆𝑗)) ∈ ℝ)
662 1red 10218 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑁)) → 1 ∈ ℝ)
663661, 662readdcld 10232 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆𝑗)) + 1) ∈ ℝ)
664 elfzouz 12639 . . . . . . . . . . . . . . . . . 18 ((𝐼‘(𝑆𝑗)) ∈ (0..^𝑀) → (𝐼‘(𝑆𝑗)) ∈ (ℤ‘0))
665 eluzle 11863 . . . . . . . . . . . . . . . . . 18 ((𝐼‘(𝑆𝑗)) ∈ (ℤ‘0) → 0 ≤ (𝐼‘(𝑆𝑗)))
66647, 664, 6653syl 18 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑁)) → 0 ≤ (𝐼‘(𝑆𝑗)))
667384a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑁)) → 0 < 1)
668661, 662, 666, 667addgegt0d 10764 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → 0 < ((𝐼‘(𝑆𝑗)) + 1))
669660, 663, 668ltled 10348 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0..^𝑁)) → 0 ≤ ((𝐼‘(𝑆𝑗)) + 1))
670669adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → 0 ≤ ((𝐼‘(𝑆𝑗)) + 1))
671661adantr 472 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐼‘(𝑆𝑗)) ∈ ℝ)
672 1red 10218 . . . . . . . . . . . . . . . . . 18 (𝜑 → 1 ∈ ℝ)
673391, 672resubcld 10621 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 − 1) ∈ ℝ)
674673ad2antrr 764 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝑀 − 1) ∈ ℝ)
675 1red 10218 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → 1 ∈ ℝ)
676 elfzolt2 12644 . . . . . . . . . . . . . . . . . . . 20 ((𝐼‘(𝑆𝑗)) ∈ (0..^𝑀) → (𝐼‘(𝑆𝑗)) < 𝑀)
67747, 676syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆𝑗)) < 𝑀)
678601, 43sseldi 3730 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆𝑗)) ∈ ℤ)
679100adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑀 ∈ ℤ)
680 zltlem1 11593 . . . . . . . . . . . . . . . . . . . 20 (((𝐼‘(𝑆𝑗)) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝐼‘(𝑆𝑗)) < 𝑀 ↔ (𝐼‘(𝑆𝑗)) ≤ (𝑀 − 1)))
681678, 679, 680syl2anc 696 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆𝑗)) < 𝑀 ↔ (𝐼‘(𝑆𝑗)) ≤ (𝑀 − 1)))
682677, 681mpbid 222 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆𝑗)) ≤ (𝑀 − 1))
683682adantr 472 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐼‘(𝑆𝑗)) ≤ (𝑀 − 1))
684 neqne 2928 . . . . . . . . . . . . . . . . . . 19 (¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1) → (𝐼‘(𝑆𝑗)) ≠ (𝑀 − 1))
685684necomd 2975 . . . . . . . . . . . . . . . . . 18 (¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1) → (𝑀 − 1) ≠ (𝐼‘(𝑆𝑗)))
686685adantl 473 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝑀 − 1) ≠ (𝐼‘(𝑆𝑗)))
687671, 674, 683, 686leneltd 10354 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐼‘(𝑆𝑗)) < (𝑀 − 1))
688671, 674, 675, 687ltadd1dd 10801 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆𝑗)) + 1) < ((𝑀 − 1) + 1))
689590ad2antrr 764 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → ((𝑀 − 1) + 1) = 𝑀)
690688, 689breqtrd 4818 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆𝑗)) + 1) < 𝑀)
691601, 49sseldi 3730 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆𝑗)) + 1) ∈ ℤ)
692691adantr 472 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆𝑗)) + 1) ∈ ℤ)
693 0zd 11552 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → 0 ∈ ℤ)
694100ad2antrr 764 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → 𝑀 ∈ ℤ)
695 elfzo 12637 . . . . . . . . . . . . . . 15 ((((𝐼‘(𝑆𝑗)) + 1) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝐼‘(𝑆𝑗)) + 1) ∈ (0..^𝑀) ↔ (0 ≤ ((𝐼‘(𝑆𝑗)) + 1) ∧ ((𝐼‘(𝑆𝑗)) + 1) < 𝑀)))
696692, 693, 694, 695syl3anc 1463 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (((𝐼‘(𝑆𝑗)) + 1) ∈ (0..^𝑀) ↔ (0 ≤ ((𝐼‘(𝑆𝑗)) + 1) ∧ ((𝐼‘(𝑆𝑗)) + 1) < 𝑀)))
697670, 690, 696mpbir2and 995 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆𝑗)) + 1) ∈ (0..^𝑀))
698697adantr 472 . . . . . . . . . . . 12 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → ((𝐼‘(𝑆𝑗)) + 1) ∈ (0..^𝑀))
699 simpr 479 . . . . . . . . . . . 12 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗))))
700 fveq2 6340 . . . . . . . . . . . . . 14 (𝑖 = ((𝐼‘(𝑆𝑗)) + 1) → (𝑄𝑖) = (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
701700breq1d 4802 . . . . . . . . . . . . 13 (𝑖 = ((𝐼‘(𝑆𝑗)) + 1) → ((𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗))) ↔ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))))
702701elrab 3492 . . . . . . . . . . . 12 (((𝐼‘(𝑆𝑗)) + 1) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ↔ (((𝐼‘(𝑆𝑗)) + 1) ∈ (0..^𝑀) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))))
703698, 699, 702sylanbrc 701 . . . . . . . . . . 11 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → ((𝐼‘(𝑆𝑗)) + 1) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))})
704 suprub 11147 . . . . . . . . . . 11 ((({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ⊆ ℝ ∧ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}𝑙𝑥) ∧ ((𝐼‘(𝑆𝑗)) + 1) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}) → ((𝐼‘(𝑆𝑗)) + 1) ≤ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ))
705606, 651, 659, 703, 704syl31anc 1466 . . . . . . . . . 10 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → ((𝐼‘(𝑆𝑗)) + 1) ≤ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ))
70662eqcomd 2754 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) = (𝐼‘(𝑆𝑗)))
707706ad2antrr 764 . . . . . . . . . 10 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) = (𝐼‘(𝑆𝑗)))
708705, 707breqtrd 4818 . . . . . . . . 9 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → ((𝐼‘(𝑆𝑗)) + 1) ≤ (𝐼‘(𝑆𝑗)))
709661ltp1d 11117 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆𝑗)) < ((𝐼‘(𝑆𝑗)) + 1))
710661, 663ltnled 10347 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆𝑗)) < ((𝐼‘(𝑆𝑗)) + 1) ↔ ¬ ((𝐼‘(𝑆𝑗)) + 1) ≤ (𝐼‘(𝑆𝑗))))
711709, 710mpbid 222 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → ¬ ((𝐼‘(𝑆𝑗)) + 1) ≤ (𝐼‘(𝑆𝑗)))
712711ad2antrr 764 . . . . . . . . 9 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → ¬ ((𝐼‘(𝑆𝑗)) + 1) ≤ (𝐼‘(𝑆𝑗)))
713708, 712pm2.65da 601 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → ¬ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗))))
714572adantr 472 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐿‘(𝐸‘(𝑆𝑗))) ∈ ℝ)
71550adantr 472 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ∈ ℝ)
716714, 715ltnled 10347 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → ((𝐿‘(𝐸‘(𝑆𝑗))) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ↔ ¬ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))))
717713, 716mpbird 247 . . . . . . 7 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐿‘(𝐸‘(𝑆𝑗))) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
718717adantlr 753 . . . . . 6 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐿‘(𝐸‘(𝑆𝑗))) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
719599, 718eqbrtrd 4814 . . . . 5 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
720598, 719pm2.61dan 867 . . . 4 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
72123ad2ant1 1125 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → 𝑀 ∈ ℕ)
72213ad2ant1 1125 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → 𝑄 ∈ (𝑃𝑀))
723213ad2ant1 1125 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → 𝐶 ∈ ℝ)
724223ad2ant1 1125 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → 𝐷 ∈ ℝ)
725233ad2ant1 1125 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → 𝐶 < 𝐷)
726493adant3 1124 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → ((𝐼‘(𝑆𝑗)) + 1) ∈ (0...𝑀))
727 simp2 1129 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → 𝑗 ∈ (0..^𝑁))
72842leidd 10757 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ≤ (𝑆𝑗))
729 elico2 12401 . . . . . . . . 9 (((𝑆𝑗) ∈ ℝ ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ*) → ((𝑆𝑗) ∈ ((𝑆𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ ((𝑆𝑗) ∈ ℝ ∧ (𝑆𝑗) ≤ (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝑗 + 1)))))
73042, 212, 729syl2anc 696 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) ∈ ((𝑆𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ ((𝑆𝑗) ∈ ℝ ∧ (𝑆𝑗) ≤ (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝑗 + 1)))))
73142, 728, 131, 730mpbir3and 1406 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ∈ ((𝑆𝑗)[,)(𝑆‘(𝑗 + 1))))
7327313adant3 1124 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → (𝑆𝑗) ∈ ((𝑆𝑗)[,)(𝑆‘(𝑗 + 1))))
733 simp3 1130 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
734 eqid 2748 . . . . . 6 ((𝑄‘((𝐼‘(𝑆𝑗)) + 1)) − ((𝐸‘(𝑆𝑗)) − (𝑆𝑗))) = ((𝑄‘((𝐼‘(𝑆𝑗)) + 1)) − ((𝐸‘(𝑆𝑗)) − (𝑆𝑗)))
73511, 3, 721, 722, 723, 724, 725, 24, 25, 26, 27, 12, 726, 727, 732, 733, 734fourierdlem63 40858 . . . . 5 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
7367353adant1r 1168 . . . 4 (((𝜑 ∧ (𝑆𝑗) ∈ ℝ) ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
737550, 551, 720, 736syl3anc 1463 . . 3 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
738549, 737pm2.61dan 867 . 2 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
739 ioossioo 12429 . 2 ((((𝑄‘(𝐼‘(𝑆𝑗))) ∈ ℝ* ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ∈ ℝ*) ∧ ((𝑄‘(𝐼‘(𝑆𝑗))) ≤ (𝐿‘(𝐸‘(𝑆𝑗))) ∧ (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))) → ((𝐿‘(𝐸‘(𝑆𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆𝑗)))(,)(𝑄‘((𝐼‘(𝑆𝑗)) + 1))))
74045, 51, 89, 738, 739syl22anc 1464 1 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐿‘(𝐸‘(𝑆𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆𝑗)))(,)(𝑄‘((𝐼‘(𝑆𝑗)) + 1))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072   = wceq 1620   ∈ wcel 2127   ≠ wne 2920  ∀wral 3038  ∃wrex 3039  {crab 3042  Vcvv 3328   ∪ cun 3701   ⊆ wss 3703  ∅c0 4046  ifcif 4218  {csn 4309  {cpr 4311   class class class wbr 4792   ↦ cmpt 4869   Or wor 5174  ran crn 5255  ℩cio 5998  ⟶wf 6033  ‘cfv 6037   Isom wiso 6038  (class class class)co 6801   ↑𝑚 cmap 8011  Fincfn 8109  supcsup 8499  ℂcc 10097  ℝcr 10098  0cc0 10099  1c1 10100   + caddc 10102   · cmul 10104  ℝ*cxr 10236   < clt 10237   ≤ cle 10238   − cmin 10429   / cdiv 10847  ℕcn 11183  2c2 11233  ℤcz 11540  ℤ≥cuz 11850  ℝ+crp 11996  (,)cioo 12339  (,]cioc 12340  [,)cico 12341  [,]cicc 12342  ...cfz 12490  ..^cfzo 12630  ⌊cfl 12756  ♯chash 13282 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-rep 4911  ax-sep 4921  ax-nul 4929  ax-pow 4980  ax-pr 5043  ax-un 7102  ax-inf2 8699  ax-cnex 10155  ax-resscn 10156  ax-1cn 10157  ax-icn 10158  ax-addcl 10159  ax-addrcl 10160  ax-mulcl 10161  ax-mulrcl 10162  ax-mulcom 10163  ax-addass 10164  ax-mulass 10165  ax-distr 10166  ax-i2m1 10167  ax-1ne0 10168  ax-1rid 10169  ax-rnegex 10170  ax-rrecex 10171  ax-cnre 10172  ax-pre-lttri 10173  ax-pre-lttrn 10174  ax-pre-ltadd 10175  ax-pre-mulgt0 10176  ax-pre-sup 10177 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-nel 3024  df-ral 3043  df-rex 3044  df-reu 3045  df-rmo 3046  df-rab 3047  df-v 3330  df-sbc 3565  df-csb 3663  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-pss 3719  df-nul 4047  df-if 4219  df-pw 4292  df-sn 4310  df-pr 4312  df-tp 4314  df-op 4316  df-uni 4577  df-int 4616  df-iun 4662  df-iin 4663  df-br 4793  df-opab 4853  df-mpt 4870  df-tr 4893  df-id 5162  df-eprel 5167  df-po 5175  df-so 5176  df-fr 5213  df-se 5214  df-we 5215  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-rn 5265  df-res 5266  df-ima 5267  df-pred 5829  df-ord 5875  df-on 5876  df-lim 5877  df-suc 5878  df-iota 6000  df-fun 6039  df-fn 6040  df-f 6041  df-f1 6042  df-fo 6043  df-f1o 6044  df-fv 6045  df-isom 6046  df-riota 6762  df-ov 6804  df-oprab 6805  df-mpt2 6806  df-om 7219  df-1st 7321  df-2nd 7322  df-wrecs 7564  df-recs 7625  df-rdg 7663  df-1o 7717  df-oadd 7721  df-er 7899  df-map 8013  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-fi 8470  df-sup 8501  df-inf 8502  df-oi 8568  df-card 8926  df-cda 9153  df-pnf 10239  df-mnf 10240  df-xr 10241  df-ltxr 10242  df-le 10243  df-sub 10431  df-neg 10432  df-div 10848  df-nn 11184  df-2 11242  df-3 11243  df-n0 11456  df-xnn0 11527  df-z 11541  df-uz 11851  df-q 11953  df-rp 11997  df-xneg 12110  df-xadd 12111  df-xmul 12112  df-ioo 12343  df-ioc 12344  df-ico 12345  df-icc 12346  df-fz 12491  df-fzo 12631  df-fl 12758  df-seq 12967  df-exp 13026  df-hash 13283  df-cj 14009  df-re 14010  df-im 14011  df-sqrt 14145  df-abs 14146  df-rest 16256  df-topgen 16277  df-psmet 19911  df-xmet 19912  df-met 19913  df-bl 19914  df-mopn 19915  df-top 20872  df-topon 20889  df-bases 20923  df-cld 20996  df-ntr 20997  df-cls 20998  df-nei 21075  df-lp 21113  df-cmp 21363 This theorem is referenced by:  fourierdlem89  40884  fourierdlem90  40885  fourierdlem91  40886
 Copyright terms: Public domain W3C validator