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 39730
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 39654 . . . . . . . . 9 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
52, 4syl 17 . . . . . . . 8 (𝜑 → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
61, 5mpbid 222 . . . . . . 7 (𝜑 → (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
76simpld 475 . . . . . 6 (𝜑𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)))
8 elmapi 7830 . . . . . 6 (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
97, 8syl 17 . . . . 5 (𝜑𝑄:(0...𝑀)⟶ℝ)
109adantr 481 . . . 4 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑄:(0...𝑀)⟶ℝ)
11 fourierdlem79.t . . . . . . . . 9 𝑇 = (𝐵𝐴)
12 fourierdlem79.e . . . . . . . . 9 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
13 fourierdlem79.l . . . . . . . . 9 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))
14 fourierdlem79.i . . . . . . . . 9 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ))
153, 2, 1, 11, 12, 13, 14fourierdlem37 39689 . . . . . . . 8 (𝜑 → (𝐼:ℝ⟶(0..^𝑀) ∧ (𝑥 ∈ ℝ → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))})))
1615simpld 475 . . . . . . 7 (𝜑𝐼:ℝ⟶(0..^𝑀))
17 fzossfz 12436 . . . . . . . 8 (0..^𝑀) ⊆ (0...𝑀)
1817a1i 11 . . . . . . 7 (𝜑 → (0..^𝑀) ⊆ (0...𝑀))
1916, 18fssd 6019 . . . . . 6 (𝜑𝐼:ℝ⟶(0...𝑀))
2019adantr 481 . . . . 5 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐼:ℝ⟶(0...𝑀))
21 fourierdlem79.c . . . . . . . . . . . . 13 (𝜑𝐶 ∈ ℝ)
22 fourierdlem79.d . . . . . . . . . . . . 13 (𝜑𝐷 ∈ ℝ)
23 fourierdlem79.cltd . . . . . . . . . . . . 13 (𝜑𝐶 < 𝐷)
24 fourierdlem79.o . . . . . . . . . . . . 13 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
25 fourierdlem79.h . . . . . . . . . . . . 13 𝐻 = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
26 fourierdlem79.n . . . . . . . . . . . . 13 𝑁 = ((#‘𝐻) − 1)
27 fourierdlem79.s . . . . . . . . . . . . 13 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
2811, 3, 2, 1, 21, 22, 23, 24, 25, 26, 27fourierdlem54 39705 . . . . . . . . . . . 12 (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
2928simpld 475 . . . . . . . . . . 11 (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂𝑁)))
3029simprd 479 . . . . . . . . . 10 (𝜑𝑆 ∈ (𝑂𝑁))
3130adantr 481 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑆 ∈ (𝑂𝑁))
3229simpld 475 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℕ)
3332adantr 481 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑁 ∈ ℕ)
3424fourierdlem2 39654 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂𝑁) ↔ (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆𝑖) < (𝑆‘(𝑖 + 1))))))
3533, 34syl 17 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆 ∈ (𝑂𝑁) ↔ (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆𝑖) < (𝑆‘(𝑖 + 1))))))
3631, 35mpbid 222 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆𝑖) < (𝑆‘(𝑖 + 1)))))
3736simpld 475 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)))
38 elmapi 7830 . . . . . . 7 (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
3937, 38syl 17 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
40 elfzofz 12433 . . . . . . 7 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ (0...𝑁))
4140adantl 482 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0...𝑁))
4239, 41ffvelrnd 6321 . . . . 5 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ∈ ℝ)
4320, 42ffvelrnd 6321 . . . 4 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆𝑗)) ∈ (0...𝑀))
4410, 43ffvelrnd 6321 . . 3 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆𝑗))) ∈ ℝ)
4544rexrd 10040 . 2 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆𝑗))) ∈ ℝ*)
4616adantr 481 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐼:ℝ⟶(0..^𝑀))
4746, 42ffvelrnd 6321 . . . . 5 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆𝑗)) ∈ (0..^𝑀))
48 fzofzp1 12513 . . . . 5 ((𝐼‘(𝑆𝑗)) ∈ (0..^𝑀) → ((𝐼‘(𝑆𝑗)) + 1) ∈ (0...𝑀))
4947, 48syl 17 . . . 4 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆𝑗)) + 1) ∈ (0...𝑀))
5010, 49ffvelrnd 6321 . . 3 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ∈ ℝ)
5150rexrd 10040 . 2 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ∈ ℝ*)
5214a1i 11 . . . . 5 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < )))
53 fveq2 6153 . . . . . . . . . 10 (𝑥 = (𝑆𝑗) → (𝐸𝑥) = (𝐸‘(𝑆𝑗)))
5453fveq2d 6157 . . . . . . . . 9 (𝑥 = (𝑆𝑗) → (𝐿‘(𝐸𝑥)) = (𝐿‘(𝐸‘(𝑆𝑗))))
5554breq2d 4630 . . . . . . . 8 (𝑥 = (𝑆𝑗) → ((𝑄𝑖) ≤ (𝐿‘(𝐸𝑥)) ↔ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))))
5655rabbidv 3180 . . . . . . 7 (𝑥 = (𝑆𝑗) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))} = {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))})
5756supeq1d 8303 . . . . . 6 (𝑥 = (𝑆𝑗) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ))
5857adantl 482 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑥 = (𝑆𝑗)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ))
59 ltso 10069 . . . . . . 7 < Or ℝ
6059supex 8320 . . . . . 6 sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ V
6160a1i 11 . . . . 5 ((𝜑𝑗 ∈ (0..^𝑁)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ V)
6252, 58, 42, 61fvmptd 6250 . . . 4 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆𝑗)) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ))
6362fveq2d 6157 . . 3 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆𝑗))) = (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < )))
64 simpl 473 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝜑)
6564, 42jca 554 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝜑 ∧ (𝑆𝑗) ∈ ℝ))
66 eleq1 2686 . . . . . . . . 9 (𝑥 = (𝑆𝑗) → (𝑥 ∈ ℝ ↔ (𝑆𝑗) ∈ ℝ))
6766anbi2d 739 . . . . . . . 8 (𝑥 = (𝑆𝑗) → ((𝜑𝑥 ∈ ℝ) ↔ (𝜑 ∧ (𝑆𝑗) ∈ ℝ)))
6857, 56eleq12d 2692 . . . . . . . 8 (𝑥 = (𝑆𝑗) → (sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))} ↔ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}))
6967, 68imbi12d 334 . . . . . . 7 (𝑥 = (𝑆𝑗) → (((𝜑𝑥 ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}) ↔ ((𝜑 ∧ (𝑆𝑗) ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))})))
7015simprd 479 . . . . . . . 8 (𝜑 → (𝑥 ∈ ℝ → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}))
7170imp 445 . . . . . . 7 ((𝜑𝑥 ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))})
7269, 71vtoclg 3255 . . . . . 6 ((𝑆𝑗) ∈ ℝ → ((𝜑 ∧ (𝑆𝑗) ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}))
7342, 65, 72sylc 65 . . . . 5 ((𝜑𝑗 ∈ (0..^𝑁)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))})
74 nfrab1 3114 . . . . . . 7 𝑖{𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}
75 nfcv 2761 . . . . . . 7 𝑖
76 nfcv 2761 . . . . . . 7 𝑖 <
7774, 75, 76nfsup 8308 . . . . . 6 𝑖sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < )
78 nfcv 2761 . . . . . 6 𝑖(0..^𝑀)
79 nfcv 2761 . . . . . . . 8 𝑖𝑄
8079, 77nffv 6160 . . . . . . 7 𝑖(𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ))
81 nfcv 2761 . . . . . . 7 𝑖
82 nfcv 2761 . . . . . . 7 𝑖(𝐿‘(𝐸‘(𝑆𝑗)))
8380, 81, 82nfbr 4664 . . . . . 6 𝑖(𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))
84 fveq2 6153 . . . . . . 7 (𝑖 = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) → (𝑄𝑖) = (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < )))
8584breq1d 4628 . . . . . 6 (𝑖 = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) → ((𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗))) ↔ (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))))
8677, 78, 83, 85elrabf 3347 . . . . 5 (sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ↔ (sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ (0..^𝑀) ∧ (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))))
8773, 86sylib 208 . . . 4 ((𝜑𝑗 ∈ (0..^𝑁)) → (sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ (0..^𝑀) ∧ (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))))
8887simprd 479 . . 3 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆𝑗))))
8963, 88eqbrtrd 4640 . 2 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆𝑗))) ≤ (𝐿‘(𝐸‘(𝑆𝑗))))
902ad2antrr 761 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝑀 ∈ ℕ)
911ad2antrr 761 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝑄 ∈ (𝑃𝑀))
9221ad2antrr 761 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐶 ∈ ℝ)
9322ad2antrr 761 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐷 ∈ ℝ)
9423ad2antrr 761 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐶 < 𝐷)
95 0le1 10502 . . . . . . . 8 0 ≤ 1
9695a1i 11 . . . . . . 7 (𝜑 → 0 ≤ 1)
972nnge1d 11014 . . . . . . 7 (𝜑 → 1 ≤ 𝑀)
98 1zzd 11359 . . . . . . . 8 (𝜑 → 1 ∈ ℤ)
99 0zd 11340 . . . . . . . 8 (𝜑 → 0 ∈ ℤ)
1002nnzd 11432 . . . . . . . 8 (𝜑𝑀 ∈ ℤ)
101 elfz 12281 . . . . . . . 8 ((1 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (1 ∈ (0...𝑀) ↔ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
10298, 99, 100, 101syl3anc 1323 . . . . . . 7 (𝜑 → (1 ∈ (0...𝑀) ↔ (0 ≤ 1 ∧ 1 ≤ 𝑀)))
10396, 97, 102mpbir2and 956 . . . . . 6 (𝜑 → 1 ∈ (0...𝑀))
104103ad2antrr 761 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 1 ∈ (0...𝑀))
105 simplr 791 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝑗 ∈ (0..^𝑁))
106 fourierdlem79.z . . . . . . . 8 𝑍 = ((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)))
107 fzofzp1 12513 . . . . . . . . . . . . . 14 (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ (0...𝑁))
108107adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈ (0...𝑁))
10939, 108ffvelrnd 6321 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℝ)
110109, 42resubcld 10409 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) ∈ ℝ)
111110rehalfcld 11230 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2) ∈ ℝ)
1129, 103ffvelrnd 6321 . . . . . . . . . . . . 13 (𝜑 → (𝑄‘1) ∈ ℝ)
1133, 2, 1fourierdlem11 39663 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
114113simp1d 1071 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℝ)
115112, 114resubcld 10409 . . . . . . . . . . . 12 (𝜑 → ((𝑄‘1) − 𝐴) ∈ ℝ)
116115rehalfcld 11230 . . . . . . . . . . 11 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ)
117116adantr 481 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ)
118111, 117ifcld 4108 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ∈ ℝ)
11942, 118readdcld 10020 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) ∈ ℝ)
120106, 119syl5eqel 2702 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑍 ∈ ℝ)
121 2re 11041 . . . . . . . . . . . . . 14 2 ∈ ℝ
122121a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → 2 ∈ ℝ)
123 elfzoelz 12418 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℤ)
124123zred 11433 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℝ)
125124ltp1d 10905 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0..^𝑁) → 𝑗 < (𝑗 + 1))
126125adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑗 < (𝑗 + 1))
12728simprd 479 . . . . . . . . . . . . . . . . 17 (𝜑𝑆 Isom < , < ((0...𝑁), 𝐻))
128127adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑆 Isom < , < ((0...𝑁), 𝐻))
129 isorel 6536 . . . . . . . . . . . . . . . 16 ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝑗 + 1) ∈ (0...𝑁))) → (𝑗 < (𝑗 + 1) ↔ (𝑆𝑗) < (𝑆‘(𝑗 + 1))))
130128, 41, 108, 129syl12anc 1321 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑗 < (𝑗 + 1) ↔ (𝑆𝑗) < (𝑆‘(𝑗 + 1))))
131126, 130mpbid 222 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) < (𝑆‘(𝑗 + 1)))
13242, 109posdifd 10565 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) < (𝑆‘(𝑗 + 1)) ↔ 0 < ((𝑆‘(𝑗 + 1)) − (𝑆𝑗))))
133131, 132mpbid 222 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → 0 < ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)))
134 2pos 11063 . . . . . . . . . . . . . 14 0 < 2
135134a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → 0 < 2)
136110, 122, 133, 135divgt0d 10910 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → 0 < (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
137111, 136elrpd 11820 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2) ∈ ℝ+)
138121a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 2 ∈ ℝ)
1392nngt0d 11015 . . . . . . . . . . . . . . . . . 18 (𝜑 → 0 < 𝑀)
140 fzolb 12424 . . . . . . . . . . . . . . . . . 18 (0 ∈ (0..^𝑀) ↔ (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
14199, 100, 139, 140syl3anbrc 1244 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ∈ (0..^𝑀))
142 0re 9991 . . . . . . . . . . . . . . . . . 18 0 ∈ ℝ
143 eleq1 2686 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 0 → (𝑖 ∈ (0..^𝑀) ↔ 0 ∈ (0..^𝑀)))
144143anbi2d 739 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 0 → ((𝜑𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 0 ∈ (0..^𝑀))))
145 fveq2 6153 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 0 → (𝑄𝑖) = (𝑄‘0))
146 oveq1 6617 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 0 → (𝑖 + 1) = (0 + 1))
147146fveq2d 6157 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 0 → (𝑄‘(𝑖 + 1)) = (𝑄‘(0 + 1)))
148145, 147breq12d 4631 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 0 → ((𝑄𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘0) < (𝑄‘(0 + 1))))
149144, 148imbi12d 334 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 0 → (((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))))
1506simprd 479 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))
151150simprd 479 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))
152151r19.21bi 2927 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
153149, 152vtoclg 3255 . . . . . . . . . . . . . . . . . 18 (0 ∈ ℝ → ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1))))
154142, 153ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1)))
155141, 154mpdan 701 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘0) < (𝑄‘(0 + 1)))
156150simpld 475 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵))
157156simpld 475 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘0) = 𝐴)
158 0p1e1 11083 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
159158fveq2i 6156 . . . . . . . . . . . . . . . . 17 (𝑄‘(0 + 1)) = (𝑄‘1)
160159a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘(0 + 1)) = (𝑄‘1))
161155, 157, 1603brtr3d 4649 . . . . . . . . . . . . . . 15 (𝜑𝐴 < (𝑄‘1))
162114, 112posdifd 10565 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 < (𝑄‘1) ↔ 0 < ((𝑄‘1) − 𝐴)))
163161, 162mpbid 222 . . . . . . . . . . . . . 14 (𝜑 → 0 < ((𝑄‘1) − 𝐴))
164134a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 0 < 2)
165115, 138, 163, 164divgt0d 10910 . . . . . . . . . . . . 13 (𝜑 → 0 < (((𝑄‘1) − 𝐴) / 2))
166116, 165elrpd 11820 . . . . . . . . . . . 12 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ+)
167166adantr 481 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ+)
168137, 167ifcld 4108 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ∈ ℝ+)
16942, 168ltaddrpd 11856 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) < ((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
17042, 119, 169ltled 10136 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ≤ ((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
171170, 106syl6breqr 4660 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ≤ 𝑍)
17242, 111readdcld 10020 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) ∈ ℝ)
173 iftrue 4069 . . . . . . . . . . . . 13 (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
174173adantl 482 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
175111leidd 10545 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
176175adantr 481 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
177174, 176eqbrtrd 4640 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
178 iffalse 4072 . . . . . . . . . . . . 13 (¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) − 𝐴) / 2))
179178adantl 482 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) − 𝐴) / 2))
180115ad2antrr 761 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑄‘1) − 𝐴) ∈ ℝ)
181110adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) ∈ ℝ)
182 2rp 11788 . . . . . . . . . . . . . 14 2 ∈ ℝ+
183182a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → 2 ∈ ℝ+)
184 simpr 477 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴))
185180, 181, 184nltled 10138 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑄‘1) − 𝐴) ≤ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)))
186180, 181, 183, 185lediv1dd 11881 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑄‘1) − 𝐴) / 2) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
187179, 186eqbrtrd 4640 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
188177, 187pm2.61dan 831 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
189118, 111, 42, 188leadd2dd 10593 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) ≤ ((𝑆𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)))
19042recnd 10019 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ∈ ℂ)
191109recnd 10019 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℂ)
192190, 191addcomd 10189 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + (𝑆‘(𝑗 + 1))) = ((𝑆‘(𝑗 + 1)) + (𝑆𝑗)))
193192oveq1d 6625 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) = (((𝑆‘(𝑗 + 1)) + (𝑆𝑗)) / 2))
194193oveq1d 6625 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → ((((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = ((((𝑆‘(𝑗 + 1)) + (𝑆𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)))
195 halfaddsub 11216 . . . . . . . . . . . . . . 15 (((𝑆‘(𝑗 + 1)) ∈ ℂ ∧ (𝑆𝑗) ∈ ℂ) → (((((𝑆‘(𝑗 + 1)) + (𝑆𝑗)) / 2) + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = (𝑆‘(𝑗 + 1)) ∧ ((((𝑆‘(𝑗 + 1)) + (𝑆𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = (𝑆𝑗)))
196191, 190, 195syl2anc 692 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → (((((𝑆‘(𝑗 + 1)) + (𝑆𝑗)) / 2) + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = (𝑆‘(𝑗 + 1)) ∧ ((((𝑆‘(𝑗 + 1)) + (𝑆𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = (𝑆𝑗)))
197196simprd 479 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → ((((𝑆‘(𝑗 + 1)) + (𝑆𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = (𝑆𝑗))
198194, 197eqtrd 2655 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → ((((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = (𝑆𝑗))
199190, 191addcld 10010 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + (𝑆‘(𝑗 + 1))) ∈ ℂ)
200199halfcld 11228 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) ∈ ℂ)
201111recnd 10019 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2) ∈ ℂ)
202200, 201, 190subsub23d 38986 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → (((((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = (𝑆𝑗) ↔ ((((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (𝑆𝑗)) = (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)))
203198, 202mpbid 222 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → ((((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (𝑆𝑗)) = (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2))
204200, 190, 201subaddd 10361 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → (((((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (𝑆𝑗)) = (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2) ↔ ((𝑆𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = (((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2)))
205203, 204mpbid 222 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) = (((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2))
206 avglt2 11222 . . . . . . . . . . . 12 (((𝑆𝑗) ∈ ℝ ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ) → ((𝑆𝑗) < (𝑆‘(𝑗 + 1)) ↔ (((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) < (𝑆‘(𝑗 + 1))))
20742, 109, 206syl2anc 692 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) < (𝑆‘(𝑗 + 1)) ↔ (((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) < (𝑆‘(𝑗 + 1))))
208131, 207mpbid 222 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆𝑗) + (𝑆‘(𝑗 + 1))) / 2) < (𝑆‘(𝑗 + 1)))
209205, 208eqbrtrd 4640 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) < (𝑆‘(𝑗 + 1)))
210119, 172, 109, 189, 209lelttrd 10146 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑆‘(𝑗 + 1)))
211106, 210syl5eqbr 4653 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑍 < (𝑆‘(𝑗 + 1)))
212109rexrd 10040 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℝ*)
213 elico2 12186 . . . . . . . 8 (((𝑆𝑗) ∈ ℝ ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ*) → (𝑍 ∈ ((𝑆𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ (𝑍 ∈ ℝ ∧ (𝑆𝑗) ≤ 𝑍𝑍 < (𝑆‘(𝑗 + 1)))))
21442, 212, 213syl2anc 692 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑍 ∈ ((𝑆𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ (𝑍 ∈ ℝ ∧ (𝑆𝑗) ≤ 𝑍𝑍 < (𝑆‘(𝑗 + 1)))))
215120, 171, 211, 214mpbir3and 1243 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑍 ∈ ((𝑆𝑗)[,)(𝑆‘(𝑗 + 1))))
216215adantr 481 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝑍 ∈ ((𝑆𝑗)[,)(𝑆‘(𝑗 + 1))))
217114ad2antrr 761 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐴 ∈ ℝ)
218113simp2d 1072 . . . . . . . . 9 (𝜑𝐵 ∈ ℝ)
219218ad2antrr 761 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐵 ∈ ℝ)
220113simp3d 1073 . . . . . . . . 9 (𝜑𝐴 < 𝐵)
221220ad2antrr 761 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐴 < 𝐵)
22242adantr 481 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝑆𝑗) ∈ ℝ)
223 simpr 477 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) = 𝐵)
224169, 106syl6breqr 4660 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) < 𝑍)
225218, 114resubcld 10409 . . . . . . . . . . . . . 14 (𝜑 → (𝐵𝐴) ∈ ℝ)
22611, 225syl5eqel 2702 . . . . . . . . . . . . 13 (𝜑𝑇 ∈ ℝ)
227226adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑇 ∈ ℝ)
228111adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2) ∈ ℝ)
229116ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ)
230110adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) ∈ ℝ)
231115ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑄‘1) − 𝐴) ∈ ℝ)
232182a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → 2 ∈ ℝ+)
233 simpr 477 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴))
234230, 231, 232, 233ltdiv1dd 11880 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2) < (((𝑄‘1) − 𝐴) / 2))
235228, 229, 234ltled 10136 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2) ≤ (((𝑄‘1) − 𝐴) / 2))
236174, 235eqbrtrd 4640 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2))
237178adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) − 𝐴) / 2))
238116leidd 10545 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ≤ (((𝑄‘1) − 𝐴) / 2))
239238adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑄‘1) − 𝐴) / 2) ≤ (((𝑄‘1) − 𝐴) / 2))
240237, 239eqbrtrd 4640 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2))
241240adantlr 750 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2))
242236, 241pm2.61dan 831 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2))
243225rehalfcld 11230 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵𝐴) / 2) ∈ ℝ)
244182a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 2 ∈ ℝ+)
245114rexrd 10040 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ ℝ*)
246218rexrd 10040 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ∈ ℝ*)
2473, 2, 1fourierdlem15 39667 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
248247, 103ffvelrnd 6321 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑄‘1) ∈ (𝐴[,]𝐵))
249 iccleub 12178 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝑄‘1) ∈ (𝐴[,]𝐵)) → (𝑄‘1) ≤ 𝐵)
250245, 246, 248, 249syl3anc 1323 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑄‘1) ≤ 𝐵)
251112, 218, 114, 250lesub1dd 10594 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑄‘1) − 𝐴) ≤ (𝐵𝐴))
252115, 225, 244, 251lediv1dd 11881 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ≤ ((𝐵𝐴) / 2))
25311eqcomi 2630 . . . . . . . . . . . . . . . . . 18 (𝐵𝐴) = 𝑇
254253oveq1i 6620 . . . . . . . . . . . . . . . . 17 ((𝐵𝐴) / 2) = (𝑇 / 2)
255114, 218posdifd 10565 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
256220, 255mpbid 222 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 < (𝐵𝐴))
257256, 11syl6breqr 4660 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 < 𝑇)
258226, 257elrpd 11820 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 ∈ ℝ+)
259 rphalflt 11811 . . . . . . . . . . . . . . . . . 18 (𝑇 ∈ ℝ+ → (𝑇 / 2) < 𝑇)
260258, 259syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑇 / 2) < 𝑇)
261254, 260syl5eqbr 4653 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵𝐴) / 2) < 𝑇)
262116, 243, 226, 252, 261lelttrd 10146 . . . . . . . . . . . . . . 15 (𝜑 → (((𝑄‘1) − 𝐴) / 2) < 𝑇)
263116, 226, 262ltled 10136 . . . . . . . . . . . . . 14 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ≤ 𝑇)
264263adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑄‘1) − 𝐴) / 2) ≤ 𝑇)
265118, 117, 227, 242, 264letrd 10145 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ 𝑇)
266118, 227, 42, 265leadd2dd 10593 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) ≤ ((𝑆𝑗) + 𝑇))
267106, 266syl5eqbr 4653 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑍 ≤ ((𝑆𝑗) + 𝑇))
26842rexrd 10040 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ∈ ℝ*)
26942, 227readdcld 10020 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) + 𝑇) ∈ ℝ)
270 elioc2 12185 . . . . . . . . . . 11 (((𝑆𝑗) ∈ ℝ* ∧ ((𝑆𝑗) + 𝑇) ∈ ℝ) → (𝑍 ∈ ((𝑆𝑗)(,]((𝑆𝑗) + 𝑇)) ↔ (𝑍 ∈ ℝ ∧ (𝑆𝑗) < 𝑍𝑍 ≤ ((𝑆𝑗) + 𝑇))))
271268, 269, 270syl2anc 692 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑍 ∈ ((𝑆𝑗)(,]((𝑆𝑗) + 𝑇)) ↔ (𝑍 ∈ ℝ ∧ (𝑆𝑗) < 𝑍𝑍 ≤ ((𝑆𝑗) + 𝑇))))
272120, 224, 267, 271mpbir3and 1243 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑍 ∈ ((𝑆𝑗)(,]((𝑆𝑗) + 𝑇)))
273272adantr 481 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝑍 ∈ ((𝑆𝑗)(,]((𝑆𝑗) + 𝑇)))
274217, 219, 221, 11, 12, 222, 223, 273fourierdlem26 39678 . . . . . . 7 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸𝑍) = (𝐴 + (𝑍 − (𝑆𝑗))))
275106a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑍 = ((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
276275oveq1d 6625 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑍 − (𝑆𝑗)) = (((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆𝑗)))
277276oveq2d 6626 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐴 + (𝑍 − (𝑆𝑗))) = (𝐴 + (((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆𝑗))))
278277adantr 481 . . . . . . 7 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐴 + (𝑍 − (𝑆𝑗))) = (𝐴 + (((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆𝑗))))
279118recnd 10019 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ∈ ℂ)
280190, 279pncan2d 10345 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → (((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆𝑗)) = if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)))
281280oveq2d 6626 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐴 + (((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆𝑗))) = (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
282281adantr 481 . . . . . . 7 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐴 + (((𝑆𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆𝑗))) = (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
283274, 278, 2823eqtrd 2659 . . . . . 6 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸𝑍) = (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))))
284173oveq2d 6626 . . . . . . . . . 10 (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)))
285284adantl 482 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)))
286114adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ℝ)
287286, 111readdcld 10020 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) ∈ ℝ)
288287adantr 481 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) ∈ ℝ)
289286, 117readdcld 10020 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) ∈ ℝ)
290289adantr 481 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) ∈ ℝ)
291112ad2antrr 761 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝑄‘1) ∈ ℝ)
292114ad2antrr 761 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → 𝐴 ∈ ℝ)
293228, 229, 292, 234ltadd2dd 10147 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) < (𝐴 + (((𝑄‘1) − 𝐴) / 2)))
294112recnd 10019 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄‘1) ∈ ℂ)
295114recnd 10019 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ ℂ)
296 halfaddsub 11216 . . . . . . . . . . . . . . . 16 (((𝑄‘1) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (((((𝑄‘1) + 𝐴) / 2) + (((𝑄‘1) − 𝐴) / 2)) = (𝑄‘1) ∧ ((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) = 𝐴))
297294, 295, 296syl2anc 692 . . . . . . . . . . . . . . 15 (𝜑 → (((((𝑄‘1) + 𝐴) / 2) + (((𝑄‘1) − 𝐴) / 2)) = (𝑄‘1) ∧ ((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) = 𝐴))
298297simprd 479 . . . . . . . . . . . . . 14 (𝜑 → ((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) = 𝐴)
299298oveq1d 6625 . . . . . . . . . . . . 13 (𝜑 → (((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) + (((𝑄‘1) − 𝐴) / 2)) = (𝐴 + (((𝑄‘1) − 𝐴) / 2)))
300112, 114readdcld 10020 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑄‘1) + 𝐴) ∈ ℝ)
301300rehalfcld 11230 . . . . . . . . . . . . . . 15 (𝜑 → (((𝑄‘1) + 𝐴) / 2) ∈ ℝ)
302301recnd 10019 . . . . . . . . . . . . . 14 (𝜑 → (((𝑄‘1) + 𝐴) / 2) ∈ ℂ)
303116recnd 10019 . . . . . . . . . . . . . 14 (𝜑 → (((𝑄‘1) − 𝐴) / 2) ∈ ℂ)
304302, 303npcand 10347 . . . . . . . . . . . . 13 (𝜑 → (((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) + (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) + 𝐴) / 2))
305299, 304eqtr3d 2657 . . . . . . . . . . . 12 (𝜑 → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) + 𝐴) / 2))
306112, 112readdcld 10020 . . . . . . . . . . . . . 14 (𝜑 → ((𝑄‘1) + (𝑄‘1)) ∈ ℝ)
307114, 112, 112, 161ltadd2dd 10147 . . . . . . . . . . . . . 14 (𝜑 → ((𝑄‘1) + 𝐴) < ((𝑄‘1) + (𝑄‘1)))
308300, 306, 244, 307ltdiv1dd 11880 . . . . . . . . . . . . 13 (𝜑 → (((𝑄‘1) + 𝐴) / 2) < (((𝑄‘1) + (𝑄‘1)) / 2))
3092942timesd 11226 . . . . . . . . . . . . . . . 16 (𝜑 → (2 · (𝑄‘1)) = ((𝑄‘1) + (𝑄‘1)))
310309eqcomd 2627 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑄‘1) + (𝑄‘1)) = (2 · (𝑄‘1)))
311310oveq1d 6625 . . . . . . . . . . . . . 14 (𝜑 → (((𝑄‘1) + (𝑄‘1)) / 2) = ((2 · (𝑄‘1)) / 2))
312 2cnd 11044 . . . . . . . . . . . . . . 15 (𝜑 → 2 ∈ ℂ)
313 2ne0 11064 . . . . . . . . . . . . . . . 16 2 ≠ 0
314313a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 2 ≠ 0)
315294, 312, 314divcan3d 10757 . . . . . . . . . . . . . 14 (𝜑 → ((2 · (𝑄‘1)) / 2) = (𝑄‘1))
316311, 315eqtrd 2655 . . . . . . . . . . . . 13 (𝜑 → (((𝑄‘1) + (𝑄‘1)) / 2) = (𝑄‘1))
317308, 316breqtrd 4644 . . . . . . . . . . . 12 (𝜑 → (((𝑄‘1) + 𝐴) / 2) < (𝑄‘1))
318305, 317eqbrtrd 4640 . . . . . . . . . . 11 (𝜑 → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) < (𝑄‘1))
319318ad2antrr 761 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) < (𝑄‘1))
320288, 290, 291, 293, 319lttrd 10149 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2)) < (𝑄‘1))
321285, 320eqbrtrd 4640 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1))
322178oveq2d 6626 . . . . . . . . . 10 (¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑄‘1) − 𝐴) / 2)))
323322adantl 482 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑄‘1) − 𝐴) / 2)))
324318ad2antrr 761 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) < (𝑄‘1))
325323, 324eqbrtrd 4640 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1))
326321, 325pm2.61dan 831 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1))
327326adantr 481 . . . . . 6 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1))
328283, 327eqbrtrd 4640 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸𝑍) < (𝑄‘1))
329 eqid 2621 . . . . 5 ((𝑄‘1) − ((𝐸𝑍) − 𝑍)) = ((𝑄‘1) − ((𝐸𝑍) − 𝑍))
33011, 3, 90, 91, 92, 93, 94, 24, 25, 26, 27, 12, 104, 105, 216, 328, 329fourierdlem63 39714 . . . 4 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘1))
33114a1i 11 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < )))
33257adantl 482 . . . . . . . . 9 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ 𝑥 = (𝑆𝑗)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ))
33360a1i 11 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) ∈ V)
334331, 332, 222, 333fvmptd 6250 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐼‘(𝑆𝑗)) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ))
335 fveq2 6153 . . . . . . . . . . . . 13 ((𝐸‘(𝑆𝑗)) = 𝐵 → (𝐿‘(𝐸‘(𝑆𝑗))) = (𝐿𝐵))
33613a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)))
337 iftrue 4069 . . . . . . . . . . . . . . 15 (𝑦 = 𝐵 → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝐴)
338337adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑦 = 𝐵) → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝐴)
339 ubioc1 12176 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵) → 𝐵 ∈ (𝐴(,]𝐵))
340245, 246, 220, 339syl3anc 1323 . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ (𝐴(,]𝐵))
341336, 338, 340, 114fvmptd 6250 . . . . . . . . . . . . 13 (𝜑 → (𝐿𝐵) = 𝐴)
342335, 341sylan9eqr 2677 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐿‘(𝐸‘(𝑆𝑗))) = 𝐴)
343342breq2d 4630 . . . . . . . . . . 11 ((𝜑 ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → ((𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗))) ↔ (𝑄𝑖) ≤ 𝐴))
344343rabbidv 3180 . . . . . . . . . 10 ((𝜑 ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} = {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴})
345344supeq1d 8303 . . . . . . . . 9 ((𝜑 ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}, ℝ, < ))
346345adantlr 750 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}, ℝ, < ))
347 simpl 473 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}) → 𝜑)
348 elrabi 3346 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴} → 𝑗 ∈ (0..^𝑀))
349348adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}) → 𝑗 ∈ (0..^𝑀))
350 fveq2 6153 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑗 → (𝑄𝑖) = (𝑄𝑗))
351350breq1d 4628 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → ((𝑄𝑖) ≤ 𝐴 ↔ (𝑄𝑗) ≤ 𝐴))
352351elrab 3350 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴} ↔ (𝑗 ∈ (0..^𝑀) ∧ (𝑄𝑗) ≤ 𝐴))
353352simprbi 480 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴} → (𝑄𝑗) ≤ 𝐴)
354353adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}) → (𝑄𝑗) ≤ 𝐴)
355 simp3 1061 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑀) ∧ (𝑄𝑗) ≤ 𝐴) → (𝑄𝑗) ≤ 𝐴)
356114ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝐴 ∈ ℝ)
357112ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝑄‘1) ∈ ℝ)
3589adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
35918sselda 3587 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0..^𝑀)) → 𝑗 ∈ (0...𝑀))
360358, 359ffvelrnd 6321 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑄𝑗) ∈ ℝ)
361360adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝑄𝑗) ∈ ℝ)
362161ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝐴 < (𝑄‘1))
363 1zzd 11359 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 1 ∈ ℤ)
364 elfzoelz 12418 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℤ)
365364ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝑗 ∈ ℤ)
366 1e0p1 11503 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 = (0 + 1)
367 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → ¬ 𝑗 ≤ 0)
368 0red 9992 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 0 ∈ ℝ)
369365zred 11433 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝑗 ∈ ℝ)
370368, 369ltnled 10135 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (0 < 𝑗 ↔ ¬ 𝑗 ≤ 0))
371367, 370mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 0 < 𝑗)
372 0zd 11340 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 0 ∈ ℤ)
373 zltp1le 11378 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((0 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (0 < 𝑗 ↔ (0 + 1) ≤ 𝑗))
374372, 365, 373syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (0 < 𝑗 ↔ (0 + 1) ≤ 𝑗))
375371, 374mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (0 + 1) ≤ 𝑗)
376366, 375syl5eqbr 4653 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 1 ≤ 𝑗)
377 eluz2 11644 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 ∈ (ℤ‘1) ↔ (1 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 1 ≤ 𝑗))
378363, 365, 376, 377syl3anbrc 1244 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝑗 ∈ (ℤ‘1))
3799ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑄:(0...𝑀)⟶ℝ)
380 0red 9992 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (1...𝑗) → 0 ∈ ℝ)
381 elfzelz 12291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 𝑙 ∈ ℤ)
382381zred 11433 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (1...𝑗) → 𝑙 ∈ ℝ)
383 1red 10006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 1 ∈ ℝ)
384 0lt1 10501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 0 < 1
385384a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 0 < 1)
386 elfzle1 12293 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 1 ≤ 𝑙)
387380, 383, 382, 385, 386ltletrd 10148 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (1...𝑗) → 0 < 𝑙)
388380, 382, 387ltled 10136 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑙 ∈ (1...𝑗) → 0 ≤ 𝑙)
389388adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 0 ≤ 𝑙)
390382adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ∈ ℝ)
391100zred 11433 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑀 ∈ ℝ)
392391ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑀 ∈ ℝ)
393364zred 11433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℝ)
394393ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑗 ∈ ℝ)
395 elfzle2 12294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...𝑗) → 𝑙𝑗)
396395adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙𝑗)
397 elfzolt2 12427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0..^𝑀) → 𝑗 < 𝑀)
398397ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑗 < 𝑀)
399390, 394, 392, 396, 398lelttrd 10146 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 < 𝑀)
400390, 392, 399ltled 10136 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙𝑀)
401381adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ∈ ℤ)
402 0zd 11340 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 0 ∈ ℤ)
403100ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑀 ∈ ℤ)
404 elfz 12281 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑙 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑙 ∈ (0...𝑀) ↔ (0 ≤ 𝑙𝑙𝑀)))
405401, 402, 403, 404syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → (𝑙 ∈ (0...𝑀) ↔ (0 ≤ 𝑙𝑙𝑀)))
406389, 400, 405mpbir2and 956 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ∈ (0...𝑀))
407379, 406ffvelrnd 6321 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → (𝑄𝑙) ∈ ℝ)
408407adantlr 750 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) ∧ 𝑙 ∈ (1...𝑗)) → (𝑄𝑙) ∈ ℝ)
4099ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑄:(0...𝑀)⟶ℝ)
410 0zd 11340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ∈ ℤ)
411100ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℤ)
412 elfzelz 12291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 𝑙 ∈ ℤ)
413412adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℤ)
414410, 411, 4133jca 1240 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑙 ∈ ℤ))
415 0red 9992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 0 ∈ ℝ)
416412zred 11433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 𝑙 ∈ ℝ)
417 1red 10006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑙 ∈ (1...(𝑗 − 1)) → 1 ∈ ℝ)
418384a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑙 ∈ (1...(𝑗 − 1)) → 0 < 1)
419 elfzle1 12293 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑙 ∈ (1...(𝑗 − 1)) → 1 ≤ 𝑙)
420415, 417, 416, 418, 419ltletrd 10148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 0 < 𝑙)
421415, 416, 420ltled 10136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...(𝑗 − 1)) → 0 ≤ 𝑙)
422421adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ≤ 𝑙)
423413zred 11433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℝ)
424391ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℝ)
425393ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 ∈ ℝ)
426416adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℝ)
427 peano2rem 10299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 ∈ ℝ → (𝑗 − 1) ∈ ℝ)
428393, 427syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑗 ∈ (0..^𝑀) → (𝑗 − 1) ∈ ℝ)
429428adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑗 − 1) ∈ ℝ)
430393adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 ∈ ℝ)
431 elfzle2 12294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑙 ∈ (1...(𝑗 − 1)) → 𝑙 ≤ (𝑗 − 1))
432431adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ≤ (𝑗 − 1))
433430ltm1d 10907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑗 − 1) < 𝑗)
434426, 429, 430, 432, 433lelttrd 10146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑗)
435434adantll 749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑗)
436397ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 < 𝑀)
437423, 425, 424, 435, 436lttrd 10149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑀)
438423, 424, 437ltled 10136 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙𝑀)
439414, 422, 438jca32 557 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑙 ∈ ℤ) ∧ (0 ≤ 𝑙𝑙𝑀)))
440 elfz2 12282 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑙 ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑙 ∈ ℤ) ∧ (0 ≤ 𝑙𝑙𝑀)))
441439, 440sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ (0...𝑀))
442409, 441ffvelrnd 6321 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄𝑙) ∈ ℝ)
443413peano2zd 11436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ∈ ℤ)
444410, 411, 4433jca 1240 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑙 + 1) ∈ ℤ))
445416, 417readdcld 10020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) ∈ ℝ)
446416, 417, 420, 418addgt0d 10553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (1...(𝑗 − 1)) → 0 < (𝑙 + 1))
447415, 445, 446ltled 10136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (1...(𝑗 − 1)) → 0 ≤ (𝑙 + 1))
448447adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ≤ (𝑙 + 1))
449445adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ∈ ℝ)
450445recnd 10019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) ∈ ℂ)
451 1cnd 10007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑙 ∈ (1...(𝑗 − 1)) → 1 ∈ ℂ)
452450, 451npcand 10347 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑙 ∈ (1...(𝑗 − 1)) → (((𝑙 + 1) − 1) + 1) = (𝑙 + 1))
453452eqcomd 2627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) = (((𝑙 + 1) − 1) + 1))
454453adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) = (((𝑙 + 1) − 1) + 1))
455 peano2re 10160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑙 ∈ ℝ → (𝑙 + 1) ∈ ℝ)
456 peano2rem 10299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑙 + 1) ∈ ℝ → ((𝑙 + 1) − 1) ∈ ℝ)
457426, 455, 4563syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((𝑙 + 1) − 1) ∈ ℝ)
458 peano2re 10160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑗 − 1) ∈ ℝ → ((𝑗 − 1) + 1) ∈ ℝ)
459 peano2rem 10299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑗 − 1) + 1) ∈ ℝ → (((𝑗 − 1) + 1) − 1) ∈ ℝ)
460429, 458, 4593syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (((𝑗 − 1) + 1) − 1) ∈ ℝ)
461 1red 10006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 1 ∈ ℝ)
462 elfzel2 12289 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑗 − 1) ∈ ℤ)
463462zred 11433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑗 − 1) ∈ ℝ)
464463, 417readdcld 10020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑙 ∈ (1...(𝑗 − 1)) → ((𝑗 − 1) + 1) ∈ ℝ)
465416, 463, 417, 431leadd1dd 10592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) ≤ ((𝑗 − 1) + 1))
466445, 464, 417, 465lesub1dd 10594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑙 ∈ (1...(𝑗 − 1)) → ((𝑙 + 1) − 1) ≤ (((𝑗 − 1) + 1) − 1))
467466adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((𝑙 + 1) − 1) ≤ (((𝑗 − 1) + 1) − 1))
468457, 460, 461, 467leadd1dd 10592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (((𝑙 + 1) − 1) + 1) ≤ ((((𝑗 − 1) + 1) − 1) + 1))
469 peano2zm 11371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑗 ∈ ℤ → (𝑗 − 1) ∈ ℤ)
470364, 469syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑗 ∈ (0..^𝑀) → (𝑗 − 1) ∈ ℤ)
471470peano2zd 11436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑗 ∈ (0..^𝑀) → ((𝑗 − 1) + 1) ∈ ℤ)
472471zcnd 11434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ (0..^𝑀) → ((𝑗 − 1) + 1) ∈ ℂ)
473 1cnd 10007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ (0..^𝑀) → 1 ∈ ℂ)
474472, 473npcand 10347 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 ∈ (0..^𝑀) → ((((𝑗 − 1) + 1) − 1) + 1) = ((𝑗 − 1) + 1))
475393recnd 10019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℂ)
476475, 473npcand 10347 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 ∈ (0..^𝑀) → ((𝑗 − 1) + 1) = 𝑗)
477474, 476eqtrd 2655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 ∈ (0..^𝑀) → ((((𝑗 − 1) + 1) − 1) + 1) = 𝑗)
478477adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((((𝑗 − 1) + 1) − 1) + 1) = 𝑗)
479468, 478breqtrd 4644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (((𝑙 + 1) − 1) + 1) ≤ 𝑗)
480454, 479eqbrtrd 4640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ≤ 𝑗)
481480adantll 749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ≤ 𝑗)
482449, 425, 424, 481, 436lelttrd 10146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) < 𝑀)
483449, 424, 482ltled 10136 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ≤ 𝑀)
484444, 448, 483jca32 557 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑙 + 1) ∈ ℤ) ∧ (0 ≤ (𝑙 + 1) ∧ (𝑙 + 1) ≤ 𝑀)))
485 elfz2 12282 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑙 + 1) ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑙 + 1) ∈ ℤ) ∧ (0 ≤ (𝑙 + 1) ∧ (𝑙 + 1) ≤ 𝑀)))
486484, 485sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ∈ (0...𝑀))
487409, 486ffvelrnd 6321 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄‘(𝑙 + 1)) ∈ ℝ)
488 simpll 789 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝜑)
489 0zd 11340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ∈ ℤ)
490412adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℤ)
491421adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ≤ 𝑙)
492 eluz2 11644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (ℤ‘0) ↔ (0 ∈ ℤ ∧ 𝑙 ∈ ℤ ∧ 0 ≤ 𝑙))
493489, 490, 491, 492syl3anbrc 1244 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ (ℤ‘0))
494 elfzoel2 12417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0..^𝑀) → 𝑀 ∈ ℤ)
495494adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℤ)
496495zred 11433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℝ)
497397adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 < 𝑀)
498426, 430, 496, 434, 497lttrd 10149 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑀)
499 elfzo2 12421 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (0..^𝑀) ↔ (𝑙 ∈ (ℤ‘0) ∧ 𝑀 ∈ ℤ ∧ 𝑙 < 𝑀))
500493, 495, 498, 499syl3anbrc 1244 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ (0..^𝑀))
501500adantll 749 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ (0..^𝑀))
502 eleq1 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 = 𝑙 → (𝑖 ∈ (0..^𝑀) ↔ 𝑙 ∈ (0..^𝑀)))
503502anbi2d 739 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 = 𝑙 → ((𝜑𝑖 ∈ (0..^𝑀)) ↔ (𝜑𝑙 ∈ (0..^𝑀))))
504 fveq2 6153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 = 𝑙 → (𝑄𝑖) = (𝑄𝑙))
505 oveq1 6617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 = 𝑙 → (𝑖 + 1) = (𝑙 + 1))
506505fveq2d 6157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 = 𝑙 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑙 + 1)))
507504, 506breq12d 4631 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 = 𝑙 → ((𝑄𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄𝑙) < (𝑄‘(𝑙 + 1))))
508503, 507imbi12d 334 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 = 𝑙 → (((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑𝑙 ∈ (0..^𝑀)) → (𝑄𝑙) < (𝑄‘(𝑙 + 1)))))
509508, 152chvarv 2262 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑙 ∈ (0..^𝑀)) → (𝑄𝑙) < (𝑄‘(𝑙 + 1)))
510488, 501, 509syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄𝑙) < (𝑄‘(𝑙 + 1)))
511442, 487, 510ltled 10136 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄𝑙) ≤ (𝑄‘(𝑙 + 1)))
512511adantlr 750 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄𝑙) ≤ (𝑄‘(𝑙 + 1)))
513378, 408, 512monoord 12778 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝑄‘1) ≤ (𝑄𝑗))
514356, 357, 361, 362, 513ltletrd 10148 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝐴 < (𝑄𝑗))
515356, 361ltnled 10135 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝐴 < (𝑄𝑗) ↔ ¬ (𝑄𝑗) ≤ 𝐴))
516514, 515mpbid 222 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → ¬ (𝑄𝑗) ≤ 𝐴)
517516ex 450 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑀)) → (¬ 𝑗 ≤ 0 → ¬ (𝑄𝑗) ≤ 𝐴))
5185173adant3 1079 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑀) ∧ (𝑄𝑗) ≤ 𝐴) → (¬ 𝑗 ≤ 0 → ¬ (𝑄𝑗) ≤ 𝐴))
519355, 518mt4d 152 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑀) ∧ (𝑄𝑗) ≤ 𝐴) → 𝑗 ≤ 0)
520 elfzole1 12426 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0..^𝑀) → 0 ≤ 𝑗)
5215203ad2ant2 1081 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑀) ∧ (𝑄𝑗) ≤ 𝐴) → 0 ≤ 𝑗)
5223933ad2ant2 1081 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑀) ∧ (𝑄𝑗) ≤ 𝐴) → 𝑗 ∈ ℝ)
523 0red 9992 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑀) ∧ (𝑄𝑗) ≤ 𝐴) → 0 ∈ ℝ)
524522, 523letri3d 10130 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑀) ∧ (𝑄𝑗) ≤ 𝐴) → (𝑗 = 0 ↔ (𝑗 ≤ 0 ∧ 0 ≤ 𝑗)))
525519, 521, 524mpbir2and 956 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑀) ∧ (𝑄𝑗) ≤ 𝐴) → 𝑗 = 0)
526347, 349, 354, 525syl3anc 1323 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}) → 𝑗 = 0)
527 velsn 4169 . . . . . . . . . . . . . . 15 (𝑗 ∈ {0} ↔ 𝑗 = 0)
528526, 527sylibr 224 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}) → 𝑗 ∈ {0})
529528ralrimiva 2961 . . . . . . . . . . . . 13 (𝜑 → ∀𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}𝑗 ∈ {0})
530 dfss3 3577 . . . . . . . . . . . . 13 ({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴} ⊆ {0} ↔ ∀𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}𝑗 ∈ {0})
531529, 530sylibr 224 . . . . . . . . . . . 12 (𝜑 → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴} ⊆ {0})
532157, 114eqeltrd 2698 . . . . . . . . . . . . . . 15 (𝜑 → (𝑄‘0) ∈ ℝ)
533532, 157eqled 10091 . . . . . . . . . . . . . 14 (𝜑 → (𝑄‘0) ≤ 𝐴)
534145breq1d 4628 . . . . . . . . . . . . . . 15 (𝑖 = 0 → ((𝑄𝑖) ≤ 𝐴 ↔ (𝑄‘0) ≤ 𝐴))
535534elrab 3350 . . . . . . . . . . . . . 14 (0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴} ↔ (0 ∈ (0..^𝑀) ∧ (𝑄‘0) ≤ 𝐴))
536141, 533, 535sylanbrc 697 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴})
537536snssd 4314 . . . . . . . . . . . 12 (𝜑 → {0} ⊆ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴})
538531, 537eqssd 3604 . . . . . . . . . . 11 (𝜑 → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴} = {0})
539538supeq1d 8303 . . . . . . . . . 10 (𝜑 → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}, ℝ, < ) = sup({0}, ℝ, < ))
540 supsn 8329 . . . . . . . . . . . 12 (( < Or ℝ ∧ 0 ∈ ℝ) → sup({0}, ℝ, < ) = 0)
54159, 142, 540mp2an 707 . . . . . . . . . . 11 sup({0}, ℝ, < ) = 0
542541a1i 11 . . . . . . . . . 10 (𝜑 → sup({0}, ℝ, < ) = 0)
543539, 542eqtrd 2655 . . . . . . . . 9 (𝜑 → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}, ℝ, < ) = 0)
544543ad2antrr 761 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ 𝐴}, ℝ, < ) = 0)
545334, 346, 5443eqtrd 2659 . . . . . . 7 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐼‘(𝑆𝑗)) = 0)
546545oveq1d 6625 . . . . . 6 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → ((𝐼‘(𝑆𝑗)) + 1) = (0 + 1))
547546fveq2d 6157 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) = (𝑄‘(0 + 1)))
548547, 159syl6req 2672 . . . 4 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝑄‘1) = (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
549330, 548breqtrd 4644 . . 3 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
55065adantr 481 . . . 4 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝜑 ∧ (𝑆𝑗) ∈ ℝ))
551 simplr 791 . . . 4 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝑗 ∈ (0..^𝑁))
55213a1i 11 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)))
553 simpr 477 . . . . . . . . . . . . . . . 16 ((¬ (𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → 𝑦 = (𝐸‘(𝑆𝑗)))
554 neqne 2798 . . . . . . . . . . . . . . . . 17 (¬ (𝐸‘(𝑆𝑗)) = 𝐵 → (𝐸‘(𝑆𝑗)) ≠ 𝐵)
555554adantr 481 . . . . . . . . . . . . . . . 16 ((¬ (𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → (𝐸‘(𝑆𝑗)) ≠ 𝐵)
556553, 555eqnetrd 2857 . . . . . . . . . . . . . . 15 ((¬ (𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → 𝑦𝐵)
557556neneqd 2795 . . . . . . . . . . . . . 14 ((¬ (𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → ¬ 𝑦 = 𝐵)
558557iffalsed 4074 . . . . . . . . . . . . 13 ((¬ (𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝑦)
559558, 553eqtrd 2655 . . . . . . . . . . . 12 ((¬ (𝐸‘(𝑆𝑗)) = 𝐵𝑦 = (𝐸‘(𝑆𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = (𝐸‘(𝑆𝑗)))
560559adantll 749 . . . . . . . . . . 11 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ 𝑦 = (𝐸‘(𝑆𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = (𝐸‘(𝑆𝑗)))
561114, 218, 220, 11, 12fourierdlem4 39656 . . . . . . . . . . . . . 14 (𝜑𝐸:ℝ⟶(𝐴(,]𝐵))
562561adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐸:ℝ⟶(𝐴(,]𝐵))
563562, 42ffvelrnd 6321 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆𝑗)) ∈ (𝐴(,]𝐵))
564563adantr 481 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) ∈ (𝐴(,]𝐵))
565552, 560, 564, 564fvmptd 6250 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐿‘(𝐸‘(𝑆𝑗))) = (𝐸‘(𝑆𝑗)))
566565eqcomd 2627 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) = (𝐿‘(𝐸‘(𝑆𝑗))))
567114, 218, 220, 13fourierdlem17 39669 . . . . . . . . . . . . 13 (𝜑𝐿:(𝐴(,]𝐵)⟶(𝐴[,]𝐵))
568567adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐿:(𝐴(,]𝐵)⟶(𝐴[,]𝐵))
569114, 218iccssred 39161 . . . . . . . . . . . . 13 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
570569adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐴[,]𝐵) ⊆ ℝ)
571568, 570fssd 6019 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐿:(𝐴(,]𝐵)⟶ℝ)
572571, 563ffvelrnd 6321 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐿‘(𝐸‘(𝑆𝑗))) ∈ ℝ)
573572adantr 481 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐿‘(𝐸‘(𝑆𝑗))) ∈ ℝ)
574566, 573eqeltrd 2698 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) ∈ ℝ)
575218ad2antrr 761 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐵 ∈ ℝ)
576245adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ℝ*)
577218adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐵 ∈ ℝ)
578 elioc2 12185 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → ((𝐸‘(𝑆𝑗)) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘(𝑆𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆𝑗)) ∧ (𝐸‘(𝑆𝑗)) ≤ 𝐵)))
579576, 577, 578syl2anc 692 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆𝑗)) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘(𝑆𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆𝑗)) ∧ (𝐸‘(𝑆𝑗)) ≤ 𝐵)))
580563, 579mpbid 222 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆𝑗)) ∧ (𝐸‘(𝑆𝑗)) ≤ 𝐵))
581580simp3d 1073 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆𝑗)) ≤ 𝐵)
582581adantr 481 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) ≤ 𝐵)
583554necomd 2845 . . . . . . . . 9 (¬ (𝐸‘(𝑆𝑗)) = 𝐵𝐵 ≠ (𝐸‘(𝑆𝑗)))
584583adantl 482 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → 𝐵 ≠ (𝐸‘(𝑆𝑗)))
585574, 575, 582, 584leneltd 10142 . . . . . . 7 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) < 𝐵)
586585adantr 481 . . . . . 6 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆𝑗)) < 𝐵)
587 oveq1 6617 . . . . . . . . . . 11 ((𝐼‘(𝑆𝑗)) = (𝑀 − 1) → ((𝐼‘(𝑆𝑗)) + 1) = ((𝑀 − 1) + 1))
5882nncnd 10987 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℂ)
589 1cnd 10007 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℂ)
590588, 589npcand 10347 . . . . . . . . . . 11 (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
591587, 590sylan9eqr 2677 . . . . . . . . . 10 ((𝜑 ∧ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆𝑗)) + 1) = 𝑀)
592591fveq2d 6157 . . . . . . . . 9 ((𝜑 ∧ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) = (𝑄𝑀))
593156simprd 479 . . . . . . . . . 10 (𝜑 → (𝑄𝑀) = 𝐵)
594593adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝑄𝑀) = 𝐵)
595592, 594eqtr2d 2656 . . . . . . . 8 ((𝜑 ∧ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → 𝐵 = (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
596595adantlr 750 . . . . . . 7 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → 𝐵 = (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
597596adantlr 750 . . . . . 6 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → 𝐵 = (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
598586, 597breqtrd 4644 . . . . 5 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
599566adantr 481 . . . . . 6 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆𝑗)) = (𝐿‘(𝐸‘(𝑆𝑗))))
600 ssrab2 3671 . . . . . . . . . . . . 13 {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ⊆ (0..^𝑀)
601 fzssz 12292 . . . . . . . . . . . . . . 15 (0...𝑀) ⊆ ℤ
60217, 601sstri 3596 . . . . . . . . . . . . . 14 (0..^𝑀) ⊆ ℤ
603 zssre 11335 . . . . . . . . . . . . . 14 ℤ ⊆ ℝ
604602, 603sstri 3596 . . . . . . . . . . . . 13 (0..^𝑀) ⊆ ℝ
605600, 604sstri 3596 . . . . . . . . . . . 12 {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ⊆ ℝ
606605a1i 11 . . . . . . . . . . 11 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ⊆ ℝ)
60756neeq1d 2849 . . . . . . . . . . . . . . 15 (𝑥 = (𝑆𝑗) → ({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))} ≠ ∅ ↔ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ≠ ∅))
60867, 607imbi12d 334 . . . . . . . . . . . . . 14 (𝑥 = (𝑆𝑗) → (((𝜑𝑥 ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))} ≠ ∅) ↔ ((𝜑 ∧ (𝑆𝑗) ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ≠ ∅)))
609141adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → 0 ∈ (0..^𝑀))
610533ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ) ∧ (𝐸𝑥) = 𝐵) → (𝑄‘0) ≤ 𝐴)
611 iftrue 4069 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸𝑥) = 𝐵 → if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)) = 𝐴)
612611eqcomd 2627 . . . . . . . . . . . . . . . . . . . 20 ((𝐸𝑥) = 𝐵𝐴 = if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
613612adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ) ∧ (𝐸𝑥) = 𝐵) → 𝐴 = if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
614610, 613breqtrd 4644 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ) ∧ (𝐸𝑥) = 𝐵) → (𝑄‘0) ≤ if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
615532adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → (𝑄‘0) ∈ ℝ)
616114adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ ℝ) → 𝐴 ∈ ℝ)
617616rexrd 10040 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ ℝ) → 𝐴 ∈ ℝ*)
618218adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ ℝ) → 𝐵 ∈ ℝ)
619 iocssre 12202 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
620617, 618, 619syl2anc 692 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
621561ffvelrnda 6320 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → (𝐸𝑥) ∈ (𝐴(,]𝐵))
622620, 621sseldd 3588 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → (𝐸𝑥) ∈ ℝ)
623157adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → (𝑄‘0) = 𝐴)
624 elioc2 12185 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → ((𝐸𝑥) ∈ (𝐴(,]𝐵) ↔ ((𝐸𝑥) ∈ ℝ ∧ 𝐴 < (𝐸𝑥) ∧ (𝐸𝑥) ≤ 𝐵)))
625617, 618, 624syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ ℝ) → ((𝐸𝑥) ∈ (𝐴(,]𝐵) ↔ ((𝐸𝑥) ∈ ℝ ∧ 𝐴 < (𝐸𝑥) ∧ (𝐸𝑥) ≤ 𝐵)))
626621, 625mpbid 222 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ ℝ) → ((𝐸𝑥) ∈ ℝ ∧ 𝐴 < (𝐸𝑥) ∧ (𝐸𝑥) ≤ 𝐵))
627626simp2d 1072 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → 𝐴 < (𝐸𝑥))
628623, 627eqbrtrd 4640 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → (𝑄‘0) < (𝐸𝑥))
629615, 622, 628ltled 10136 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → (𝑄‘0) ≤ (𝐸𝑥))
630629adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ) ∧ ¬ (𝐸𝑥) = 𝐵) → (𝑄‘0) ≤ (𝐸𝑥))
631 iffalse 4072 . . . . . . . . . . . . . . . . . . . . 21 (¬ (𝐸𝑥) = 𝐵 → if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)) = (𝐸𝑥))
632631eqcomd 2627 . . . . . . . . . . . . . . . . . . . 20 (¬ (𝐸𝑥) = 𝐵 → (𝐸𝑥) = if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
633632adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ) ∧ ¬ (𝐸𝑥) = 𝐵) → (𝐸𝑥) = if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
634630, 633breqtrd 4644 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ) ∧ ¬ (𝐸𝑥) = 𝐵) → (𝑄‘0) ≤ if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
635614, 634pm2.61dan 831 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → (𝑄‘0) ≤ if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
63613a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)))
637 eqeq1 2625 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐸𝑥) → (𝑦 = 𝐵 ↔ (𝐸𝑥) = 𝐵))
638 id 22 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐸𝑥) → 𝑦 = (𝐸𝑥))
639637, 638ifbieq2d 4088 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝐸𝑥) → if(𝑦 = 𝐵, 𝐴, 𝑦) = if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
640639adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ) ∧ 𝑦 = (𝐸𝑥)) → if(𝑦 = 𝐵, 𝐴, 𝑦) = if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
641616, 622ifcld 4108 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)) ∈ ℝ)
642636, 640, 621, 641fvmptd 6250 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → (𝐿‘(𝐸𝑥)) = if((𝐸𝑥) = 𝐵, 𝐴, (𝐸𝑥)))
643635, 642breqtrrd 4646 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → (𝑄‘0) ≤ (𝐿‘(𝐸𝑥)))
644145breq1d 4628 . . . . . . . . . . . . . . . . 17 (𝑖 = 0 → ((𝑄𝑖) ≤ (𝐿‘(𝐸𝑥)) ↔ (𝑄‘0) ≤ (𝐿‘(𝐸𝑥))))
645644elrab 3350 . . . . . . . . . . . . . . . 16 (0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))} ↔ (0 ∈ (0..^𝑀) ∧ (𝑄‘0) ≤ (𝐿‘(𝐸𝑥))))
646609, 643, 645sylanbrc 697 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ) → 0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))})
647 ne0i 3902 . . . . . . . . . . . . . . 15 (0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))} → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))} ≠ ∅)
648646, 647syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸𝑥))} ≠ ∅)
649608, 648vtoclg 3255 . . . . . . . . . . . . 13 ((𝑆𝑗) ∈ ℝ → ((𝜑 ∧ (𝑆𝑗) ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ≠ ∅))
65042, 65, 649sylc 65 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ≠ ∅)
651650ad2antrr 761 . . . . . . . . . . 11 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ≠ ∅)
652605a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ⊆ ℝ)
653 fzofi 12720 . . . . . . . . . . . . . . 15 (0..^𝑀) ∈ Fin
654 ssfi 8131 . . . . . . . . . . . . . . 15 (((0..^𝑀) ∈ Fin ∧ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ⊆ (0..^𝑀)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ∈ Fin)
655653, 600, 654mp2an 707 . . . . . . . . . . . . . 14 {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ∈ Fin
656655a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0..^𝑁)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ∈ Fin)
657 fimaxre2 10920 . . . . . . . . . . . . 13 (({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ⊆ ℝ ∧ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}𝑙𝑥)
658652, 656, 657syl2anc 692 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0..^𝑁)) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}𝑙𝑥)
659658ad2antrr 761 . . . . . . . . . . 11 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}𝑙𝑥)
660 0red 9992 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → 0 ∈ ℝ)
661604, 47sseldi 3585 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆𝑗)) ∈ ℝ)
662 1red 10006 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑁)) → 1 ∈ ℝ)
663661, 662readdcld 10020 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆𝑗)) + 1) ∈ ℝ)
664 elfzouz 12422 . . . . . . . . . . . . . . . . . 18 ((𝐼‘(𝑆𝑗)) ∈ (0..^𝑀) → (𝐼‘(𝑆𝑗)) ∈ (ℤ‘0))
665 eluzle 11651 . . . . . . . . . . . . . . . . . 18 ((𝐼‘(𝑆𝑗)) ∈ (ℤ‘0) → 0 ≤ (𝐼‘(𝑆𝑗)))
66647, 664, 6653syl 18 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑁)) → 0 ≤ (𝐼‘(𝑆𝑗)))
667384a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0..^𝑁)) → 0 < 1)
668661, 662, 666, 667addgegt0d 10552 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → 0 < ((𝐼‘(𝑆𝑗)) + 1))
669660, 663, 668ltled 10136 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0..^𝑁)) → 0 ≤ ((𝐼‘(𝑆𝑗)) + 1))
670669adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → 0 ≤ ((𝐼‘(𝑆𝑗)) + 1))
671661adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐼‘(𝑆𝑗)) ∈ ℝ)
672 1red 10006 . . . . . . . . . . . . . . . . . 18 (𝜑 → 1 ∈ ℝ)
673391, 672resubcld 10409 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 − 1) ∈ ℝ)
674673ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝑀 − 1) ∈ ℝ)
675 1red 10006 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → 1 ∈ ℝ)
676 elfzolt2 12427 . . . . . . . . . . . . . . . . . . . 20 ((𝐼‘(𝑆𝑗)) ∈ (0..^𝑀) → (𝐼‘(𝑆𝑗)) < 𝑀)
67747, 676syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆𝑗)) < 𝑀)
678601, 43sseldi 3585 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆𝑗)) ∈ ℤ)
679100adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑀 ∈ ℤ)
680 zltlem1 11381 . . . . . . . . . . . . . . . . . . . 20 (((𝐼‘(𝑆𝑗)) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝐼‘(𝑆𝑗)) < 𝑀 ↔ (𝐼‘(𝑆𝑗)) ≤ (𝑀 − 1)))
681678, 679, 680syl2anc 692 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆𝑗)) < 𝑀 ↔ (𝐼‘(𝑆𝑗)) ≤ (𝑀 − 1)))
682677, 681mpbid 222 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆𝑗)) ≤ (𝑀 − 1))
683682adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐼‘(𝑆𝑗)) ≤ (𝑀 − 1))
684 neqne 2798 . . . . . . . . . . . . . . . . . . 19 (¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1) → (𝐼‘(𝑆𝑗)) ≠ (𝑀 − 1))
685684necomd 2845 . . . . . . . . . . . . . . . . . 18 (¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1) → (𝑀 − 1) ≠ (𝐼‘(𝑆𝑗)))
686685adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝑀 − 1) ≠ (𝐼‘(𝑆𝑗)))
687671, 674, 683, 686leneltd 10142 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐼‘(𝑆𝑗)) < (𝑀 − 1))
688671, 674, 675, 687ltadd1dd 10589 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆𝑗)) + 1) < ((𝑀 − 1) + 1))
689590ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → ((𝑀 − 1) + 1) = 𝑀)
690688, 689breqtrd 4644 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆𝑗)) + 1) < 𝑀)
691601, 49sseldi 3585 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆𝑗)) + 1) ∈ ℤ)
692691adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆𝑗)) + 1) ∈ ℤ)
693 0zd 11340 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → 0 ∈ ℤ)
694100ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → 𝑀 ∈ ℤ)
695 elfzo 12420 . . . . . . . . . . . . . . 15 ((((𝐼‘(𝑆𝑗)) + 1) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝐼‘(𝑆𝑗)) + 1) ∈ (0..^𝑀) ↔ (0 ≤ ((𝐼‘(𝑆𝑗)) + 1) ∧ ((𝐼‘(𝑆𝑗)) + 1) < 𝑀)))
696692, 693, 694, 695syl3anc 1323 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (((𝐼‘(𝑆𝑗)) + 1) ∈ (0..^𝑀) ↔ (0 ≤ ((𝐼‘(𝑆𝑗)) + 1) ∧ ((𝐼‘(𝑆𝑗)) + 1) < 𝑀)))
697670, 690, 696mpbir2and 956 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆𝑗)) + 1) ∈ (0..^𝑀))
698697adantr 481 . . . . . . . . . . . 12 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → ((𝐼‘(𝑆𝑗)) + 1) ∈ (0..^𝑀))
699 simpr 477 . . . . . . . . . . . 12 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗))))
700 fveq2 6153 . . . . . . . . . . . . . 14 (𝑖 = ((𝐼‘(𝑆𝑗)) + 1) → (𝑄𝑖) = (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
701700breq1d 4628 . . . . . . . . . . . . 13 (𝑖 = ((𝐼‘(𝑆𝑗)) + 1) → ((𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗))) ↔ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))))
702701elrab 3350 . . . . . . . . . . . 12 (((𝐼‘(𝑆𝑗)) + 1) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ↔ (((𝐼‘(𝑆𝑗)) + 1) ∈ (0..^𝑀) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))))
703698, 699, 702sylanbrc 697 . . . . . . . . . . 11 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → ((𝐼‘(𝑆𝑗)) + 1) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))})
704 suprub 10935 . . . . . . . . . . 11 ((({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ⊆ ℝ ∧ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}𝑙𝑥) ∧ ((𝐼‘(𝑆𝑗)) + 1) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}) → ((𝐼‘(𝑆𝑗)) + 1) ≤ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ))
705606, 651, 659, 703, 704syl31anc 1326 . . . . . . . . . 10 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → ((𝐼‘(𝑆𝑗)) + 1) ≤ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ))
70662eqcomd 2627 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) = (𝐼‘(𝑆𝑗)))
707706ad2antrr 761 . . . . . . . . . 10 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))}, ℝ, < ) = (𝐼‘(𝑆𝑗)))
708705, 707breqtrd 4644 . . . . . . . . 9 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → ((𝐼‘(𝑆𝑗)) + 1) ≤ (𝐼‘(𝑆𝑗)))
709661ltp1d 10905 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆𝑗)) < ((𝐼‘(𝑆𝑗)) + 1))
710661, 663ltnled 10135 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆𝑗)) < ((𝐼‘(𝑆𝑗)) + 1) ↔ ¬ ((𝐼‘(𝑆𝑗)) + 1) ≤ (𝐼‘(𝑆𝑗))))
711709, 710mpbid 222 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑁)) → ¬ ((𝐼‘(𝑆𝑗)) + 1) ≤ (𝐼‘(𝑆𝑗)))
712711ad2antrr 761 . . . . . . . . 9 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))) → ¬ ((𝐼‘(𝑆𝑗)) + 1) ≤ (𝐼‘(𝑆𝑗)))
713708, 712pm2.65da 599 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → ¬ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗))))
714572adantr 481 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐿‘(𝐸‘(𝑆𝑗))) ∈ ℝ)
71550adantr 481 . . . . . . . . 9 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ∈ ℝ)
716714, 715ltnled 10135 . . . . . . . 8 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → ((𝐿‘(𝐸‘(𝑆𝑗))) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ↔ ¬ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆𝑗)))))
717713, 716mpbird 247 . . . . . . 7 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐿‘(𝐸‘(𝑆𝑗))) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
718717adantlr 750 . . . . . 6 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐿‘(𝐸‘(𝑆𝑗))) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
719599, 718eqbrtrd 4640 . . . . 5 ((((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) ∧ ¬ (𝐼‘(𝑆𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
720598, 719pm2.61dan 831 . . . 4 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
72123ad2ant1 1080 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → 𝑀 ∈ ℕ)
72213ad2ant1 1080 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → 𝑄 ∈ (𝑃𝑀))
723213ad2ant1 1080 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → 𝐶 ∈ ℝ)
724223ad2ant1 1080 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → 𝐷 ∈ ℝ)
725233ad2ant1 1080 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → 𝐶 < 𝐷)
726493adant3 1079 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → ((𝐼‘(𝑆𝑗)) + 1) ∈ (0...𝑀))
727 simp2 1060 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → 𝑗 ∈ (0..^𝑁))
72842leidd 10545 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ≤ (𝑆𝑗))
729 elico2 12186 . . . . . . . . 9 (((𝑆𝑗) ∈ ℝ ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ*) → ((𝑆𝑗) ∈ ((𝑆𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ ((𝑆𝑗) ∈ ℝ ∧ (𝑆𝑗) ≤ (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝑗 + 1)))))
73042, 212, 729syl2anc 692 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗) ∈ ((𝑆𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ ((𝑆𝑗) ∈ ℝ ∧ (𝑆𝑗) ≤ (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝑗 + 1)))))
73142, 728, 131, 730mpbir3and 1243 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝑆𝑗) ∈ ((𝑆𝑗)[,)(𝑆‘(𝑗 + 1))))
7327313adant3 1079 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → (𝑆𝑗) ∈ ((𝑆𝑗)[,)(𝑆‘(𝑗 + 1))))
733 simp3 1061 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
734 eqid 2621 . . . . . 6 ((𝑄‘((𝐼‘(𝑆𝑗)) + 1)) − ((𝐸‘(𝑆𝑗)) − (𝑆𝑗))) = ((𝑄‘((𝐼‘(𝑆𝑗)) + 1)) − ((𝐸‘(𝑆𝑗)) − (𝑆𝑗)))
73511, 3, 721, 722, 723, 724, 725, 24, 25, 26, 27, 12, 726, 727, 732, 733, 734fourierdlem63 39714 . . . . 5 ((𝜑𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
7367353adant1r 1316 . . . 4 (((𝜑 ∧ (𝑆𝑗) ∈ ℝ) ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆𝑗)) < (𝑄‘((𝐼‘(𝑆𝑗)) + 1))) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
737550, 551, 720, 736syl3anc 1323 . . 3 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆𝑗)) = 𝐵) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
738549, 737pm2.61dan 831 . 2 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))
739 ioossioo 12214 . 2 ((((𝑄‘(𝐼‘(𝑆𝑗))) ∈ ℝ* ∧ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)) ∈ ℝ*) ∧ ((𝑄‘(𝐼‘(𝑆𝑗))) ≤ (𝐿‘(𝐸‘(𝑆𝑗))) ∧ (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆𝑗)) + 1)))) → ((𝐿‘(𝐸‘(𝑆𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆𝑗)))(,)(𝑄‘((𝐼‘(𝑆𝑗)) + 1))))
74045, 51, 89, 738, 739syl22anc 1324 1 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐿‘(𝐸‘(𝑆𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆𝑗)))(,)(𝑄‘((𝐼‘(𝑆𝑗)) + 1))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wne 2790  wral 2907  wrex 2908  {crab 2911  Vcvv 3189  cun 3557  wss 3559  c0 3896  ifcif 4063  {csn 4153  {cpr 4155   class class class wbr 4618  cmpt 4678   Or wor 4999  ran crn 5080  cio 5813  wf 5848  cfv 5852   Isom wiso 5853  (class class class)co 6610  𝑚 cmap 7809  Fincfn 7906  supcsup 8297  cc 9885  cr 9886  0cc0 9887  1c1 9888   + caddc 9890   · cmul 9892  *cxr 10024   < clt 10025  cle 10026  cmin 10217   / cdiv 10635  cn 10971  2c2 11021  cz 11328  cuz 11638  +crp 11783  (,)cioo 12124  (,]cioc 12125  [,)cico 12126  [,]cicc 12127  ...cfz 12275  ..^cfzo 12413  cfl 12538  #chash 13064
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8489  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964  ax-pre-sup 9965
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-iin 4493  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-oadd 7516  df-er 7694  df-map 7811  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910  df-fi 8268  df-sup 8299  df-inf 8300  df-oi 8366  df-card 8716  df-cda 8941  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-div 10636  df-nn 10972  df-2 11030  df-3 11031  df-n0 11244  df-xnn0 11315  df-z 11329  df-uz 11639  df-q 11740  df-rp 11784  df-xneg 11897  df-xadd 11898  df-xmul 11899  df-ioo 12128  df-ioc 12129  df-ico 12130  df-icc 12131  df-fz 12276  df-fzo 12414  df-fl 12540  df-seq 12749  df-exp 12808  df-hash 13065  df-cj 13780  df-re 13781  df-im 13782  df-sqrt 13916  df-abs 13917  df-rest 16011  df-topgen 16032  df-psmet 19666  df-xmet 19667  df-met 19668  df-bl 19669  df-mopn 19670  df-top 20627  df-topon 20644  df-bases 20670  df-cld 20742  df-ntr 20743  df-cls 20744  df-nei 20821  df-lp 20859  df-cmp 21109
This theorem is referenced by:  fourierdlem89  39740  fourierdlem90  39741  fourierdlem91  39742
  Copyright terms: Public domain W3C validator