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

Theorem fourierdlem50 44807
Description: Continuity of 𝑂 and its limits with respect to the 𝑆 partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem50.xre (𝜑𝑋 ∈ ℝ)
fourierdlem50.p 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem50.m (𝜑𝑀 ∈ ℕ)
fourierdlem50.v (𝜑𝑉 ∈ (𝑃𝑀))
fourierdlem50.a (𝜑𝐴 ∈ ℝ)
fourierdlem50.b (𝜑𝐵 ∈ ℝ)
fourierdlem50.altb (𝜑𝐴 < 𝐵)
fourierdlem50.ab (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
fourierdlem50.q 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋))
fourierdlem50.t 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))
fourierdlem50.n 𝑁 = ((♯‘𝑇) − 1)
fourierdlem50.s 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇))
fourierdlem50.j (𝜑𝐽 ∈ (0..^𝑁))
fourierdlem50.u 𝑈 = (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
fourierdlem50.ch (𝜒 ↔ ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))))
Assertion
Ref Expression
fourierdlem50 (𝜑 → (𝑈 ∈ (0..^𝑀) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1)))))
Distinct variable groups:   𝑖,𝐽,𝑘   𝑖,𝑀,𝑘   𝑚,𝑀,𝑝,𝑖   𝑓,𝑁   𝑄,𝑖,𝑘   𝑆,𝑓   𝑆,𝑖,𝑘   𝑇,𝑓   𝑈,𝑖   𝑖,𝑉,𝑘   𝑉,𝑝   𝑖,𝑋,𝑘   𝑚,𝑋,𝑝   𝜑,𝑓   𝜑,𝑖,𝑘
Allowed substitution hints:   𝜑(𝑚,𝑝)   𝜒(𝑓,𝑖,𝑘,𝑚,𝑝)   𝐴(𝑓,𝑖,𝑘,𝑚,𝑝)   𝐵(𝑓,𝑖,𝑘,𝑚,𝑝)   𝑃(𝑓,𝑖,𝑘,𝑚,𝑝)   𝑄(𝑓,𝑚,𝑝)   𝑆(𝑚,𝑝)   𝑇(𝑖,𝑘,𝑚,𝑝)   𝑈(𝑓,𝑘,𝑚,𝑝)   𝐽(𝑓,𝑚,𝑝)   𝑀(𝑓)   𝑁(𝑖,𝑘,𝑚,𝑝)   𝑉(𝑓,𝑚)   𝑋(𝑓)

Proof of Theorem fourierdlem50
Dummy variables 𝑥 𝑙 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem50.u . . 3 𝑈 = (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
2 fourierdlem50.m . . . . . . . 8 (𝜑𝑀 ∈ ℕ)
3 fourierdlem50.a . . . . . . . 8 (𝜑𝐴 ∈ ℝ)
4 fourierdlem50.b . . . . . . . 8 (𝜑𝐵 ∈ ℝ)
5 fourierdlem50.altb . . . . . . . . 9 (𝜑𝐴 < 𝐵)
63, 4, 5ltled 11358 . . . . . . . 8 (𝜑𝐴𝐵)
7 fourierdlem50.p . . . . . . . . . . . . 13 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
8 fourierdlem50.v . . . . . . . . . . . . 13 (𝜑𝑉 ∈ (𝑃𝑀))
97, 2, 8fourierdlem15 44773 . . . . . . . . . . . 12 (𝜑𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
10 pire 25950 . . . . . . . . . . . . . . . 16 π ∈ ℝ
1110renegcli 11517 . . . . . . . . . . . . . . 15 -π ∈ ℝ
1211a1i 11 . . . . . . . . . . . . . 14 (𝜑 → -π ∈ ℝ)
13 fourierdlem50.xre . . . . . . . . . . . . . 14 (𝜑𝑋 ∈ ℝ)
1412, 13readdcld 11239 . . . . . . . . . . . . 13 (𝜑 → (-π + 𝑋) ∈ ℝ)
1510a1i 11 . . . . . . . . . . . . . 14 (𝜑 → π ∈ ℝ)
1615, 13readdcld 11239 . . . . . . . . . . . . 13 (𝜑 → (π + 𝑋) ∈ ℝ)
1714, 16iccssred 13407 . . . . . . . . . . . 12 (𝜑 → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
189, 17fssd 6732 . . . . . . . . . . 11 (𝜑𝑉:(0...𝑀)⟶ℝ)
1918ffvelcdmda 7082 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑉𝑖) ∈ ℝ)
2013adantr 482 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℝ)
2119, 20resubcld 11638 . . . . . . . . 9 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) − 𝑋) ∈ ℝ)
22 fourierdlem50.q . . . . . . . . 9 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋))
2321, 22fmptd 7109 . . . . . . . 8 (𝜑𝑄:(0...𝑀)⟶ℝ)
2422a1i 11 . . . . . . . . . . 11 (𝜑𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋)))
25 fveq2 6888 . . . . . . . . . . . . 13 (𝑖 = 0 → (𝑉𝑖) = (𝑉‘0))
2625oveq1d 7419 . . . . . . . . . . . 12 (𝑖 = 0 → ((𝑉𝑖) − 𝑋) = ((𝑉‘0) − 𝑋))
2726adantl 483 . . . . . . . . . . 11 ((𝜑𝑖 = 0) → ((𝑉𝑖) − 𝑋) = ((𝑉‘0) − 𝑋))
28 nnssnn0 12471 . . . . . . . . . . . . . . 15 ℕ ⊆ ℕ0
2928a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ℕ ⊆ ℕ0)
30 nn0uz 12860 . . . . . . . . . . . . . 14 0 = (ℤ‘0)
3129, 30sseqtrdi 4031 . . . . . . . . . . . . 13 (𝜑 → ℕ ⊆ (ℤ‘0))
3231, 2sseldd 3982 . . . . . . . . . . . 12 (𝜑𝑀 ∈ (ℤ‘0))
33 eluzfz1 13504 . . . . . . . . . . . 12 (𝑀 ∈ (ℤ‘0) → 0 ∈ (0...𝑀))
3432, 33syl 17 . . . . . . . . . . 11 (𝜑 → 0 ∈ (0...𝑀))
3518, 34ffvelcdmd 7083 . . . . . . . . . . . 12 (𝜑 → (𝑉‘0) ∈ ℝ)
3635, 13resubcld 11638 . . . . . . . . . . 11 (𝜑 → ((𝑉‘0) − 𝑋) ∈ ℝ)
3724, 27, 34, 36fvmptd 7001 . . . . . . . . . 10 (𝜑 → (𝑄‘0) = ((𝑉‘0) − 𝑋))
387fourierdlem2 44760 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ → (𝑉 ∈ (𝑃𝑀) ↔ (𝑉 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))))
392, 38syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑉 ∈ (𝑃𝑀) ↔ (𝑉 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))))
408, 39mpbid 231 . . . . . . . . . . . . . 14 (𝜑 → (𝑉 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1)))))
4140simprd 497 . . . . . . . . . . . . 13 (𝜑 → (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))
4241simpld 496 . . . . . . . . . . . 12 (𝜑 → ((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)))
4342simpld 496 . . . . . . . . . . 11 (𝜑 → (𝑉‘0) = (-π + 𝑋))
4443oveq1d 7419 . . . . . . . . . 10 (𝜑 → ((𝑉‘0) − 𝑋) = ((-π + 𝑋) − 𝑋))
4512recnd 11238 . . . . . . . . . . 11 (𝜑 → -π ∈ ℂ)
4613recnd 11238 . . . . . . . . . . 11 (𝜑𝑋 ∈ ℂ)
4745, 46pncand 11568 . . . . . . . . . 10 (𝜑 → ((-π + 𝑋) − 𝑋) = -π)
4837, 44, 473eqtrd 2777 . . . . . . . . 9 (𝜑 → (𝑄‘0) = -π)
4912rexrd 11260 . . . . . . . . . 10 (𝜑 → -π ∈ ℝ*)
5015rexrd 11260 . . . . . . . . . 10 (𝜑 → π ∈ ℝ*)
51 fourierdlem50.ab . . . . . . . . . . 11 (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
523leidd 11776 . . . . . . . . . . . 12 (𝜑𝐴𝐴)
533, 4, 3, 52, 6eliccd 44152 . . . . . . . . . . 11 (𝜑𝐴 ∈ (𝐴[,]𝐵))
5451, 53sseldd 3982 . . . . . . . . . 10 (𝜑𝐴 ∈ (-π[,]π))
55 iccgelb 13376 . . . . . . . . . 10 ((-π ∈ ℝ* ∧ π ∈ ℝ*𝐴 ∈ (-π[,]π)) → -π ≤ 𝐴)
5649, 50, 54, 55syl3anc 1372 . . . . . . . . 9 (𝜑 → -π ≤ 𝐴)
5748, 56eqbrtrd 5169 . . . . . . . 8 (𝜑 → (𝑄‘0) ≤ 𝐴)
584leidd 11776 . . . . . . . . . . . 12 (𝜑𝐵𝐵)
593, 4, 4, 6, 58eliccd 44152 . . . . . . . . . . 11 (𝜑𝐵 ∈ (𝐴[,]𝐵))
6051, 59sseldd 3982 . . . . . . . . . 10 (𝜑𝐵 ∈ (-π[,]π))
61 iccleub 13375 . . . . . . . . . 10 ((-π ∈ ℝ* ∧ π ∈ ℝ*𝐵 ∈ (-π[,]π)) → 𝐵 ≤ π)
6249, 50, 60, 61syl3anc 1372 . . . . . . . . 9 (𝜑𝐵 ≤ π)
63 fveq2 6888 . . . . . . . . . . . . 13 (𝑖 = 𝑀 → (𝑉𝑖) = (𝑉𝑀))
6463oveq1d 7419 . . . . . . . . . . . 12 (𝑖 = 𝑀 → ((𝑉𝑖) − 𝑋) = ((𝑉𝑀) − 𝑋))
6564adantl 483 . . . . . . . . . . 11 ((𝜑𝑖 = 𝑀) → ((𝑉𝑖) − 𝑋) = ((𝑉𝑀) − 𝑋))
66 eluzfz2 13505 . . . . . . . . . . . 12 (𝑀 ∈ (ℤ‘0) → 𝑀 ∈ (0...𝑀))
6732, 66syl 17 . . . . . . . . . . 11 (𝜑𝑀 ∈ (0...𝑀))
6818, 67ffvelcdmd 7083 . . . . . . . . . . . 12 (𝜑 → (𝑉𝑀) ∈ ℝ)
6968, 13resubcld 11638 . . . . . . . . . . 11 (𝜑 → ((𝑉𝑀) − 𝑋) ∈ ℝ)
7024, 65, 67, 69fvmptd 7001 . . . . . . . . . 10 (𝜑 → (𝑄𝑀) = ((𝑉𝑀) − 𝑋))
7142simprd 497 . . . . . . . . . . 11 (𝜑 → (𝑉𝑀) = (π + 𝑋))
7271oveq1d 7419 . . . . . . . . . 10 (𝜑 → ((𝑉𝑀) − 𝑋) = ((π + 𝑋) − 𝑋))
7315recnd 11238 . . . . . . . . . . 11 (𝜑 → π ∈ ℂ)
7473, 46pncand 11568 . . . . . . . . . 10 (𝜑 → ((π + 𝑋) − 𝑋) = π)
7570, 72, 743eqtrrd 2778 . . . . . . . . 9 (𝜑 → π = (𝑄𝑀))
7662, 75breqtrd 5173 . . . . . . . 8 (𝜑𝐵 ≤ (𝑄𝑀))
77 fourierdlem50.j . . . . . . . 8 (𝜑𝐽 ∈ (0..^𝑁))
78 fourierdlem50.t . . . . . . . 8 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))
79 prfi 9318 . . . . . . . . . . . 12 {𝐴, 𝐵} ∈ Fin
8079a1i 11 . . . . . . . . . . 11 (𝜑 → {𝐴, 𝐵} ∈ Fin)
81 fzfid 13934 . . . . . . . . . . . . 13 (𝜑 → (0...𝑀) ∈ Fin)
8222rnmptfi 43800 . . . . . . . . . . . . 13 ((0...𝑀) ∈ Fin → ran 𝑄 ∈ Fin)
8381, 82syl 17 . . . . . . . . . . . 12 (𝜑 → ran 𝑄 ∈ Fin)
84 infi 9264 . . . . . . . . . . . 12 (ran 𝑄 ∈ Fin → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
8583, 84syl 17 . . . . . . . . . . 11 (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
86 unfi 9168 . . . . . . . . . . 11 (({𝐴, 𝐵} ∈ Fin ∧ (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin) → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
8780, 85, 86syl2anc 585 . . . . . . . . . 10 (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
8878, 87eqeltrid 2838 . . . . . . . . 9 (𝜑𝑇 ∈ Fin)
893, 4jca 513 . . . . . . . . . . . 12 (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
90 prssg 4821 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
913, 4, 90syl2anc 585 . . . . . . . . . . . 12 (𝜑 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
9289, 91mpbid 231 . . . . . . . . . . 11 (𝜑 → {𝐴, 𝐵} ⊆ ℝ)
93 inss2 4228 . . . . . . . . . . . . 13 (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴(,)𝐵)
94 ioossre 13381 . . . . . . . . . . . . 13 (𝐴(,)𝐵) ⊆ ℝ
9593, 94sstri 3990 . . . . . . . . . . . 12 (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ
9695a1i 11 . . . . . . . . . . 11 (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ)
9792, 96unssd 4185 . . . . . . . . . 10 (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ ℝ)
9878, 97eqsstrid 4029 . . . . . . . . 9 (𝜑𝑇 ⊆ ℝ)
99 fourierdlem50.s . . . . . . . . 9 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇))
100 fourierdlem50.n . . . . . . . . 9 𝑁 = ((♯‘𝑇) − 1)
10188, 98, 99, 100fourierdlem36 44794 . . . . . . . 8 (𝜑𝑆 Isom < , < ((0...𝑁), 𝑇))
102 eqid 2733 . . . . . . . 8 sup({𝑥 ∈ (0..^𝑀) ∣ (𝑄𝑥) ≤ (𝑆𝐽)}, ℝ, < ) = sup({𝑥 ∈ (0..^𝑀) ∣ (𝑄𝑥) ≤ (𝑆𝐽)}, ℝ, < )
1032, 3, 4, 6, 23, 57, 76, 77, 78, 101, 102fourierdlem20 44778 . . . . . . 7 (𝜑 → ∃𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
104 fourierdlem50.ch . . . . . . . . . . . . 13 (𝜒 ↔ ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))))
105104biimpi 215 . . . . . . . . . . . . . . . . . 18 (𝜒 → ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))))
106 simp-4l 782 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝜑)
107105, 106syl 17 . . . . . . . . . . . . . . . . 17 (𝜒𝜑)
108 simplr 768 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑘 ∈ (0..^𝑀))
109105, 108syl 17 . . . . . . . . . . . . . . . . 17 (𝜒𝑘 ∈ (0..^𝑀))
110107, 109jca 513 . . . . . . . . . . . . . . . 16 (𝜒 → (𝜑𝑘 ∈ (0..^𝑀)))
111 simp-4r 783 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑖 ∈ (0..^𝑀))
112105, 111syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝑖 ∈ (0..^𝑀))
113 elfzofz 13644 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ (0..^𝑀) → 𝑘 ∈ (0...𝑀))
114113ad2antlr 726 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑘 ∈ (0...𝑀))
115105, 114syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜒𝑘 ∈ (0...𝑀))
116107, 18syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒𝑉:(0...𝑀)⟶ℝ)
117116, 115ffvelcdmd 7083 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (𝑉𝑘) ∈ ℝ)
118107, 13syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜒𝑋 ∈ ℝ)
119117, 118resubcld 11638 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ((𝑉𝑘) − 𝑋) ∈ ℝ)
120 fveq2 6888 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 𝑘 → (𝑉𝑖) = (𝑉𝑘))
121120oveq1d 7419 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑘 → ((𝑉𝑖) − 𝑋) = ((𝑉𝑘) − 𝑋))
122121, 22fvmptg 6992 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ (0...𝑀) ∧ ((𝑉𝑘) − 𝑋) ∈ ℝ) → (𝑄𝑘) = ((𝑉𝑘) − 𝑋))
123115, 119, 122syl2anc 585 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑄𝑘) = ((𝑉𝑘) − 𝑋))
124123, 119eqeltrd 2834 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄𝑘) ∈ ℝ)
12523adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
126 fzofzp1 13725 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
127126adantl 483 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
128125, 127ffvelcdmd 7083 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
129107, 112, 128syl2anc 585 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℝ)
130 isof1o 7315 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑆 Isom < , < ((0...𝑁), 𝑇) → 𝑆:(0...𝑁)–1-1-onto𝑇)
131101, 130syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑆:(0...𝑁)–1-1-onto𝑇)
132 f1of 6830 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑆:(0...𝑁)–1-1-onto𝑇𝑆:(0...𝑁)⟶𝑇)
133131, 132syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑆:(0...𝑁)⟶𝑇)
134 fzofzp1 13725 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
13577, 134syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
136133, 135ffvelcdmd 7083 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ 𝑇)
13798, 136sseldd 3982 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
138107, 137syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
139 elfzofz 13644 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
14077, 139syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐽 ∈ (0...𝑁))
141133, 140ffvelcdmd 7083 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑆𝐽) ∈ 𝑇)
14298, 141sseldd 3982 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑆𝐽) ∈ ℝ)
143107, 142syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑆𝐽) ∈ ℝ)
144105simprd 497 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
145124rexrd 11260 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → (𝑄𝑘) ∈ ℝ*)
14623adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
147 fzofzp1 13725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 ∈ (0..^𝑀) → (𝑘 + 1) ∈ (0...𝑀))
148147adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0..^𝑀)) → (𝑘 + 1) ∈ (0...𝑀))
149146, 148ffvelcdmd 7083 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ (0..^𝑀)) → (𝑄‘(𝑘 + 1)) ∈ ℝ)
150149rexrd 11260 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (0..^𝑀)) → (𝑄‘(𝑘 + 1)) ∈ ℝ*)
151110, 150syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → (𝑄‘(𝑘 + 1)) ∈ ℝ*)
152143rexrd 11260 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → (𝑆𝐽) ∈ ℝ*)
153138rexrd 11260 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → (𝑆‘(𝐽 + 1)) ∈ ℝ*)
154 elfzoelz 13628 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
155154zred 12662 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℝ)
156155ltp1d 12140 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐽 ∈ (0..^𝑁) → 𝐽 < (𝐽 + 1))
15777, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐽 < (𝐽 + 1))
158 isoeq5 7313 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) → (𝑆 Isom < , < ((0...𝑁), 𝑇) ↔ 𝑆 Isom < , < ((0...𝑁), ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))))))
15978, 158ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑆 Isom < , < ((0...𝑁), 𝑇) ↔ 𝑆 Isom < , < ((0...𝑁), ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))))
160101, 159sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑆 Isom < , < ((0...𝑁), ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))))
161 isorel 7318 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑆 Isom < , < ((0...𝑁), ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))) ∧ (𝐽 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝐽 < (𝐽 + 1) ↔ (𝑆𝐽) < (𝑆‘(𝐽 + 1))))
162160, 140, 135, 161syl12anc 836 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐽 < (𝐽 + 1) ↔ (𝑆𝐽) < (𝑆‘(𝐽 + 1))))
163157, 162mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑆𝐽) < (𝑆‘(𝐽 + 1)))
164107, 163syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → (𝑆𝐽) < (𝑆‘(𝐽 + 1)))
165145, 151, 152, 153, 164ioossioobi 44165 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ ((𝑄𝑘) ≤ (𝑆𝐽) ∧ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑘 + 1)))))
166144, 165mpbid 231 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → ((𝑄𝑘) ≤ (𝑆𝐽) ∧ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑘 + 1))))
167166simpld 496 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑄𝑘) ≤ (𝑆𝐽))
168124, 143, 138, 167, 164lelttrd 11368 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑄𝑘) < (𝑆‘(𝐽 + 1)))
169 elfzofz 13644 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
170169ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑖 ∈ (0...𝑀))
171170ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑖 ∈ (0...𝑀))
172105, 171syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒𝑖 ∈ (0...𝑀))
173107, 172, 21syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → ((𝑉𝑖) − 𝑋) ∈ ℝ)
17422fvmpt2 7005 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ (0...𝑀) ∧ ((𝑉𝑖) − 𝑋) ∈ ℝ) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
175172, 173, 174syl2anc 585 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
176175, 173eqeltrd 2834 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (𝑄𝑖) ∈ ℝ)
177 simpllr 775 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
178105, 177syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
179176, 129, 143, 138, 164, 178fourierdlem10 44768 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ((𝑄𝑖) ≤ (𝑆𝐽) ∧ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑖 + 1))))
180179simprd 497 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑖 + 1)))
181124, 138, 129, 168, 180ltletrd 11370 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄𝑘) < (𝑄‘(𝑖 + 1)))
182124, 129, 118, 181ltadd2dd 11369 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + (𝑄𝑘)) < (𝑋 + (𝑄‘(𝑖 + 1))))
183123oveq2d 7420 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + (𝑄𝑘)) = (𝑋 + ((𝑉𝑘) − 𝑋)))
184107, 46syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒𝑋 ∈ ℂ)
185117recnd 11238 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑉𝑘) ∈ ℂ)
186184, 185pncan3d 11570 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + ((𝑉𝑘) − 𝑋)) = (𝑉𝑘))
187183, 186eqtr2d 2774 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑉𝑘) = (𝑋 + (𝑄𝑘)))
188112, 126syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑖 + 1) ∈ (0...𝑀))
18918adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
190189, 127ffvelcdmd 7083 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
191107, 112, 190syl2anc 585 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℝ)
192191, 118resubcld 11638 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
193188, 192jca 513 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ((𝑖 + 1) ∈ (0...𝑀) ∧ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ))
194 eleq1 2822 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑖 + 1) → (𝑘 ∈ (0...𝑀) ↔ (𝑖 + 1) ∈ (0...𝑀)))
195 fveq2 6888 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = (𝑖 + 1) → (𝑉𝑘) = (𝑉‘(𝑖 + 1)))
196195oveq1d 7419 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = (𝑖 + 1) → ((𝑉𝑘) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
197196eleq1d 2819 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑖 + 1) → (((𝑉𝑘) − 𝑋) ∈ ℝ ↔ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ))
198194, 197anbi12d 632 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = (𝑖 + 1) → ((𝑘 ∈ (0...𝑀) ∧ ((𝑉𝑘) − 𝑋) ∈ ℝ) ↔ ((𝑖 + 1) ∈ (0...𝑀) ∧ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)))
199 fveq2 6888 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑖 + 1) → (𝑄𝑘) = (𝑄‘(𝑖 + 1)))
200199, 196eqeq12d 2749 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = (𝑖 + 1) → ((𝑄𝑘) = ((𝑉𝑘) − 𝑋) ↔ (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋)))
201198, 200imbi12d 345 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = (𝑖 + 1) → (((𝑘 ∈ (0...𝑀) ∧ ((𝑉𝑘) − 𝑋) ∈ ℝ) → (𝑄𝑘) = ((𝑉𝑘) − 𝑋)) ↔ (((𝑖 + 1) ∈ (0...𝑀) ∧ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))))
202201, 122vtoclg 3556 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 + 1) ∈ (0...𝑀) → (((𝑖 + 1) ∈ (0...𝑀) ∧ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋)))
203188, 193, 202sylc 65 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
204203oveq2d 7420 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)))
205191recnd 11238 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℂ)
206184, 205pncan3d 11570 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)) = (𝑉‘(𝑖 + 1)))
207204, 206eqtr2d 2774 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑉‘(𝑖 + 1)) = (𝑋 + (𝑄‘(𝑖 + 1))))
208182, 187, 2073brtr4d 5179 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑉𝑘) < (𝑉‘(𝑖 + 1)))
209 eleq1w 2817 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑖 → (𝑙 ∈ (0..^𝑀) ↔ 𝑖 ∈ (0..^𝑀)))
210209anbi2d 630 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑖 → (((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ↔ ((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (0..^𝑀))))
211 oveq1 7411 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑖 → (𝑙 + 1) = (𝑖 + 1))
212211fveq2d 6892 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑖 → (𝑉‘(𝑙 + 1)) = (𝑉‘(𝑖 + 1)))
213212breq2d 5159 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑖 → ((𝑉𝑘) < (𝑉‘(𝑙 + 1)) ↔ (𝑉𝑘) < (𝑉‘(𝑖 + 1))))
214210, 213anbi12d 632 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑖 → ((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑙 + 1))) ↔ (((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑖 + 1)))))
215 fveq2 6888 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑖 → (𝑉𝑙) = (𝑉𝑖))
216215breq2d 5159 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑖 → ((𝑉𝑘) ≤ (𝑉𝑙) ↔ (𝑉𝑘) ≤ (𝑉𝑖)))
217214, 216imbi12d 345 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑖 → (((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑙 + 1))) → (𝑉𝑘) ≤ (𝑉𝑙)) ↔ ((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑖 + 1))) → (𝑉𝑘) ≤ (𝑉𝑖))))
218 eleq1w 2817 . . . . . . . . . . . . . . . . . . . . . 22 ( = 𝑘 → ( ∈ (0..^𝑀) ↔ 𝑘 ∈ (0..^𝑀)))
219218anbi2d 630 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝑘 → ((𝜑 ∈ (0..^𝑀)) ↔ (𝜑𝑘 ∈ (0..^𝑀))))
220219anbi1d 631 . . . . . . . . . . . . . . . . . . . 20 ( = 𝑘 → (((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ↔ ((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀))))
221 fveq2 6888 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝑘 → (𝑉) = (𝑉𝑘))
222221breq1d 5157 . . . . . . . . . . . . . . . . . . . 20 ( = 𝑘 → ((𝑉) < (𝑉‘(𝑙 + 1)) ↔ (𝑉𝑘) < (𝑉‘(𝑙 + 1))))
223220, 222anbi12d 632 . . . . . . . . . . . . . . . . . . 19 ( = 𝑘 → ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ↔ (((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑙 + 1)))))
224221breq1d 5157 . . . . . . . . . . . . . . . . . . 19 ( = 𝑘 → ((𝑉) ≤ (𝑉𝑙) ↔ (𝑉𝑘) ≤ (𝑉𝑙)))
225223, 224imbi12d 345 . . . . . . . . . . . . . . . . . 18 ( = 𝑘 → (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → (𝑉) ≤ (𝑉𝑙)) ↔ ((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑙 + 1))) → (𝑉𝑘) ≤ (𝑉𝑙))))
226 elfzoelz 13628 . . . . . . . . . . . . . . . . . . . . 21 ( ∈ (0..^𝑀) → ∈ ℤ)
227226ad3antlr 730 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → ∈ ℤ)
228 elfzoelz 13628 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 ∈ (0..^𝑀) → 𝑙 ∈ ℤ)
229228ad2antlr 726 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → 𝑙 ∈ ℤ)
230 simplr 768 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ ¬ < (𝑙 + 1)) → (𝑉) < (𝑉‘(𝑙 + 1)))
23118adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑙 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
232 fzofzp1 13725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (0..^𝑀) → (𝑙 + 1) ∈ (0...𝑀))
233232adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑙 ∈ (0..^𝑀)) → (𝑙 + 1) ∈ (0...𝑀))
234231, 233ffvelcdmd 7083 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑙 ∈ (0..^𝑀)) → (𝑉‘(𝑙 + 1)) ∈ ℝ)
235234adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) → (𝑉‘(𝑙 + 1)) ∈ ℝ)
236235adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → (𝑉‘(𝑙 + 1)) ∈ ℝ)
23718adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
238 elfzofz 13644 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ( ∈ (0..^𝑀) → ∈ (0...𝑀))
239238adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∈ (0..^𝑀)) → ∈ (0...𝑀))
240237, 239ffvelcdmd 7083 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∈ (0..^𝑀)) → (𝑉) ∈ ℝ)
241240ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → (𝑉) ∈ ℝ)
242228zred 12662 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (0..^𝑀) → 𝑙 ∈ ℝ)
243 peano2re 11383 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ ℝ → (𝑙 + 1) ∈ ℝ)
244242, 243syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑙 ∈ (0..^𝑀) → (𝑙 + 1) ∈ ℝ)
245244ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → (𝑙 + 1) ∈ ℝ)
246226zred 12662 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ( ∈ (0..^𝑀) → ∈ ℝ)
247246ad3antlr 730 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → ∈ ℝ)
248 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → ¬ < (𝑙 + 1))
249245, 247, 248nltled 11360 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → (𝑙 + 1) ≤ )
250228peano2zd 12665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (0..^𝑀) → (𝑙 + 1) ∈ ℤ)
251250ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → (𝑙 + 1) ∈ ℤ)
252226ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → ∈ ℤ)
253 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → (𝑙 + 1) ≤ )
254 eluz2 12824 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ( ∈ (ℤ‘(𝑙 + 1)) ↔ ((𝑙 + 1) ∈ ℤ ∧ ∈ ℤ ∧ (𝑙 + 1) ≤ ))
255251, 252, 253, 254syl3anbrc 1344 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → ∈ (ℤ‘(𝑙 + 1)))
256255adantlll 717 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → ∈ (ℤ‘(𝑙 + 1)))
257 simplll 774 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝜑)
258 0zd 12566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 ∈ ℤ)
259 elfzoel2 13627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ( ∈ (0..^𝑀) → 𝑀 ∈ ℤ)
260259ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑀 ∈ ℤ)
261 elfzelz 13497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ ((𝑙 + 1)...) → 𝑖 ∈ ℤ)
262261adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 ∈ ℤ)
263 0red 11213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 ∈ ℝ)
264261zred 12662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ ((𝑙 + 1)...) → 𝑖 ∈ ℝ)
265264adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 ∈ ℝ)
266242adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑙 ∈ ℝ)
267 elfzole1 13636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑙 ∈ (0..^𝑀) → 0 ≤ 𝑙)
268267adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 ≤ 𝑙)
269266, 243syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → (𝑙 + 1) ∈ ℝ)
270266ltp1d 12140 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑙 < (𝑙 + 1))
271 elfzle1 13500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑖 ∈ ((𝑙 + 1)...) → (𝑙 + 1) ≤ 𝑖)
272271adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → (𝑙 + 1) ≤ 𝑖)
273266, 269, 265, 270, 272ltletrd 11370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑙 < 𝑖)
274263, 266, 265, 268, 273lelttrd 11368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 < 𝑖)
275263, 265, 274ltled 11358 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 ≤ 𝑖)
276275adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 ≤ 𝑖)
277264adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 ∈ ℝ)
278259zred 12662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ( ∈ (0..^𝑀) → 𝑀 ∈ ℝ)
279278adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑀 ∈ ℝ)
280246adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → ∈ ℝ)
281 elfzle2 13501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑖 ∈ ((𝑙 + 1)...) → 𝑖)
282281adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖)
283 elfzolt2 13637 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( ∈ (0..^𝑀) → < 𝑀)
284283adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → < 𝑀)
285277, 280, 279, 282, 284lelttrd 11368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 < 𝑀)
286277, 279, 285ltled 11358 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖𝑀)
287286adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖𝑀)
288258, 260, 262, 276, 287elfzd 13488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 ∈ (0...𝑀))
289288adantlll 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 ∈ (0...𝑀))
290257, 289, 19syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → (𝑉𝑖) ∈ ℝ)
291290adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → (𝑉𝑖) ∈ ℝ)
292 simplll 774 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝜑)
293 0zd 12566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 0 ∈ ℤ)
294 elfzelz 13497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 ∈ ((𝑙 + 1)...( − 1)) → 𝑖 ∈ ℤ)
295294adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ ℤ)
296 0red 11213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 0 ∈ ℝ)
297295zred 12662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ ℝ)
298242adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑙 ∈ ℝ)
299267adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 0 ≤ 𝑙)
300298, 243syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → (𝑙 + 1) ∈ ℝ)
301298ltp1d 12140 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑙 < (𝑙 + 1))
302 elfzle1 13500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑖 ∈ ((𝑙 + 1)...( − 1)) → (𝑙 + 1) ≤ 𝑖)
303302adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → (𝑙 + 1) ≤ 𝑖)
304298, 300, 297, 301, 303ltletrd 11370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑙 < 𝑖)
305296, 298, 297, 299, 304lelttrd 11368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 0 < 𝑖)
306296, 297, 305ltled 11358 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 0 ≤ 𝑖)
307 eluz2 12824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (ℤ‘0) ↔ (0 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 0 ≤ 𝑖))
308293, 295, 306, 307syl3anbrc 1344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ (ℤ‘0))
309308adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ (ℤ‘0))
310 elfzoel2 13627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (0..^𝑀) → 𝑀 ∈ ℤ)
311310ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑀 ∈ ℤ)
312294zred 12662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ ((𝑙 + 1)...( − 1)) → 𝑖 ∈ ℝ)
313312adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ ℝ)
314 peano2rem 11523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( ∈ ℝ → ( − 1) ∈ ℝ)
315246, 314syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ( ∈ (0..^𝑀) → ( − 1) ∈ ℝ)
316315adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → ( − 1) ∈ ℝ)
317278adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑀 ∈ ℝ)
318 elfzle2 13501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ ((𝑙 + 1)...( − 1)) → 𝑖 ≤ ( − 1))
319318adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ≤ ( − 1))
320246ltm1d 12142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( ∈ (0..^𝑀) → ( − 1) < )
321315, 246, 278, 320, 283lttrd 11371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ( ∈ (0..^𝑀) → ( − 1) < 𝑀)
322321adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → ( − 1) < 𝑀)
323313, 316, 317, 319, 322lelttrd 11368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 < 𝑀)
324323adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 < 𝑀)
325324adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 < 𝑀)
326 elfzo2 13631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ (0..^𝑀) ↔ (𝑖 ∈ (ℤ‘0) ∧ 𝑀 ∈ ℤ ∧ 𝑖 < 𝑀))
327309, 311, 325, 326syl3anbrc 1344 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ (0..^𝑀))
328169, 19sylan2 594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ∈ ℝ)
32941simprd 497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1)))
330329r19.21bi 3249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) < (𝑉‘(𝑖 + 1)))
331328, 190, 330ltled 11358 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ≤ (𝑉‘(𝑖 + 1)))
332292, 327, 331syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → (𝑉𝑖) ≤ (𝑉‘(𝑖 + 1)))
333332adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → (𝑉𝑖) ≤ (𝑉‘(𝑖 + 1)))
334256, 291, 333monoord 13994 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → (𝑉‘(𝑙 + 1)) ≤ (𝑉))
335249, 334syldan 592 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → (𝑉‘(𝑙 + 1)) ≤ (𝑉))
336236, 241, 335lensymd 11361 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → ¬ (𝑉) < (𝑉‘(𝑙 + 1)))
337336adantlr 714 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ ¬ < (𝑙 + 1)) → ¬ (𝑉) < (𝑉‘(𝑙 + 1)))
338230, 337condan 817 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → < (𝑙 + 1))
339 zleltp1 12609 . . . . . . . . . . . . . . . . . . . . . 22 (( ∈ ℤ ∧ 𝑙 ∈ ℤ) → (𝑙 < (𝑙 + 1)))
340227, 229, 339syl2anc 585 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → (𝑙 < (𝑙 + 1)))
341338, 340mpbird 257 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → 𝑙)
342 eluz2 12824 . . . . . . . . . . . . . . . . . . . 20 (𝑙 ∈ (ℤ) ↔ ( ∈ ℤ ∧ 𝑙 ∈ ℤ ∧ 𝑙))
343227, 229, 341, 342syl3anbrc 1344 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → 𝑙 ∈ (ℤ))
34418ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑉:(0...𝑀)⟶ℝ)
345 0zd 12566 . . . . . . . . . . . . . . . . . . . . . . 23 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 0 ∈ ℤ)
346259ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑀 ∈ ℤ)
347 elfzelz 13497 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 ∈ (...𝑙) → 𝑖 ∈ ℤ)
348347adantl 483 . . . . . . . . . . . . . . . . . . . . . . 23 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 ∈ ℤ)
349 0red 11213 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 0 ∈ ℝ)
350246adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → ∈ ℝ)
351347zred 12662 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (...𝑙) → 𝑖 ∈ ℝ)
352351adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 ∈ ℝ)
353 elfzole1 13636 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ( ∈ (0..^𝑀) → 0 ≤ )
354353adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 0 ≤ )
355 elfzle1 13500 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (...𝑙) → 𝑖)
356355adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖)
357349, 350, 352, 354, 356letrd 11367 . . . . . . . . . . . . . . . . . . . . . . . 24 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 0 ≤ 𝑖)
358357adantlr 714 . . . . . . . . . . . . . . . . . . . . . . 23 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 0 ≤ 𝑖)
359351adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 ∈ ℝ)
360310zred 12662 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑙 ∈ (0..^𝑀) → 𝑀 ∈ ℝ)
361360adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑀 ∈ ℝ)
362242adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑙 ∈ ℝ)
363 elfzle2 13501 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (...𝑙) → 𝑖𝑙)
364363adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖𝑙)
365 elfzolt2 13637 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑙 ∈ (0..^𝑀) → 𝑙 < 𝑀)
366365adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑙 < 𝑀)
367359, 362, 361, 364, 366lelttrd 11368 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 < 𝑀)
368359, 361, 367ltled 11358 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖𝑀)
369368adantll 713 . . . . . . . . . . . . . . . . . . . . . . 23 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑖𝑀)
370345, 346, 348, 358, 369elfzd 13488 . . . . . . . . . . . . . . . . . . . . . 22 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 ∈ (0...𝑀))
371370adantlll 717 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 ∈ (0...𝑀))
372344, 371ffvelcdmd 7083 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → (𝑉𝑖) ∈ ℝ)
373372adantlr 714 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...𝑙)) → (𝑉𝑖) ∈ ℝ)
374 simp-4l 782 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝜑)
375 0zd 12566 . . . . . . . . . . . . . . . . . . . . . . . 24 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 0 ∈ ℤ)
376 elfzelz 13497 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ (...(𝑙 − 1)) → 𝑖 ∈ ℤ)
377376adantl 483 . . . . . . . . . . . . . . . . . . . . . . . 24 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ ℤ)
378 0red 11213 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 0 ∈ ℝ)
379246adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → ∈ ℝ)
380377zred 12662 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ ℝ)
381353adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 0 ≤ )
382 elfzle1 13500 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (...(𝑙 − 1)) → 𝑖)
383382adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖)
384378, 379, 380, 381, 383letrd 11367 . . . . . . . . . . . . . . . . . . . . . . . 24 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 0 ≤ 𝑖)
385375, 377, 384, 307syl3anbrc 1344 . . . . . . . . . . . . . . . . . . . . . . 23 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ (ℤ‘0))
386385adantll 713 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ (ℤ‘0))
387386ad4ant14 751 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ (ℤ‘0))
388310ad3antlr 730 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑀 ∈ ℤ)
389376zred 12662 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ (...(𝑙 − 1)) → 𝑖 ∈ ℝ)
390389adantl 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ ℝ)
391242adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑙 ∈ ℝ)
392360adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑀 ∈ ℝ)
393 elfzle2 13501 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (...(𝑙 − 1)) → 𝑖 ≤ (𝑙 − 1))
394393adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ≤ (𝑙 − 1))
395 zltlem1 12611 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑖 ∈ ℤ ∧ 𝑙 ∈ ℤ) → (𝑖 < 𝑙𝑖 ≤ (𝑙 − 1)))
396376, 228, 395syl2anr 598 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → (𝑖 < 𝑙𝑖 ≤ (𝑙 − 1)))
397394, 396mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 < 𝑙)
398365adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑙 < 𝑀)
399390, 391, 392, 397, 398lttrd 11371 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 < 𝑀)
400399adantll 713 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 < 𝑀)
401400adantlr 714 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 < 𝑀)
402387, 388, 401, 326syl3anbrc 1344 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ (0..^𝑀))
403374, 402, 331syl2anc 585 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → (𝑉𝑖) ≤ (𝑉‘(𝑖 + 1)))
404343, 373, 403monoord 13994 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → (𝑉) ≤ (𝑉𝑙))
405225, 404chvarvv 2003 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑙 + 1))) → (𝑉𝑘) ≤ (𝑉𝑙))
406217, 405chvarvv 2003 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑖 + 1))) → (𝑉𝑘) ≤ (𝑉𝑖))
407110, 112, 208, 406syl21anc 837 . . . . . . . . . . . . . . 15 (𝜒 → (𝑉𝑘) ≤ (𝑉𝑖))
408107, 112jca 513 . . . . . . . . . . . . . . . 16 (𝜒 → (𝜑𝑖 ∈ (0..^𝑀)))
409110, 149syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄‘(𝑘 + 1)) ∈ ℝ)
410179simpld 496 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑄𝑖) ≤ (𝑆𝐽))
411176, 143, 138, 410, 164lelttrd 11368 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑄𝑖) < (𝑆‘(𝐽 + 1)))
412166simprd 497 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑘 + 1)))
413176, 138, 409, 411, 412ltletrd 11370 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄𝑖) < (𝑄‘(𝑘 + 1)))
414176, 409, 118, 413ltadd2dd 11369 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + (𝑄𝑖)) < (𝑋 + (𝑄‘(𝑘 + 1))))
415175oveq2d 7420 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + (𝑄𝑖)) = (𝑋 + ((𝑉𝑖) − 𝑋)))
416107, 172, 19syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑉𝑖) ∈ ℝ)
417416recnd 11238 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑉𝑖) ∈ ℂ)
418184, 417pncan3d 11570 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + ((𝑉𝑖) − 𝑋)) = (𝑉𝑖))
419415, 418eqtr2d 2774 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑉𝑖) = (𝑋 + (𝑄𝑖)))
42022a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0..^𝑀)) → 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋)))
421 fveq2 6888 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = (𝑘 + 1) → (𝑉𝑖) = (𝑉‘(𝑘 + 1)))
422421oveq1d 7419 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = (𝑘 + 1) → ((𝑉𝑖) − 𝑋) = ((𝑉‘(𝑘 + 1)) − 𝑋))
423422adantl 483 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑖 = (𝑘 + 1)) → ((𝑉𝑖) − 𝑋) = ((𝑉‘(𝑘 + 1)) − 𝑋))
42418adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
425424, 148ffvelcdmd 7083 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (0..^𝑀)) → (𝑉‘(𝑘 + 1)) ∈ ℝ)
42613adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
427425, 426resubcld 11638 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0..^𝑀)) → ((𝑉‘(𝑘 + 1)) − 𝑋) ∈ ℝ)
428420, 423, 148, 427fvmptd 7001 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0..^𝑀)) → (𝑄‘(𝑘 + 1)) = ((𝑉‘(𝑘 + 1)) − 𝑋))
429107, 109, 428syl2anc 585 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑄‘(𝑘 + 1)) = ((𝑉‘(𝑘 + 1)) − 𝑋))
430429oveq2d 7420 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + (𝑄‘(𝑘 + 1))) = (𝑋 + ((𝑉‘(𝑘 + 1)) − 𝑋)))
431110, 425syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑉‘(𝑘 + 1)) ∈ ℝ)
432431recnd 11238 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑉‘(𝑘 + 1)) ∈ ℂ)
433184, 432pncan3d 11570 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + ((𝑉‘(𝑘 + 1)) − 𝑋)) = (𝑉‘(𝑘 + 1)))
434430, 433eqtr2d 2774 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑉‘(𝑘 + 1)) = (𝑋 + (𝑄‘(𝑘 + 1))))
435414, 419, 4343brtr4d 5179 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑉𝑖) < (𝑉‘(𝑘 + 1)))
436 eleq1w 2817 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑘 → (𝑙 ∈ (0..^𝑀) ↔ 𝑘 ∈ (0..^𝑀)))
437436anbi2d 630 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑘 → (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ↔ ((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑘 ∈ (0..^𝑀))))
438 oveq1 7411 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑘 → (𝑙 + 1) = (𝑘 + 1))
439438fveq2d 6892 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑘 → (𝑉‘(𝑙 + 1)) = (𝑉‘(𝑘 + 1)))
440439breq2d 5159 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑘 → ((𝑉𝑖) < (𝑉‘(𝑙 + 1)) ↔ (𝑉𝑖) < (𝑉‘(𝑘 + 1))))
441437, 440anbi12d 632 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑘 → ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑙 + 1))) ↔ (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑘 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑘 + 1)))))
442 fveq2 6888 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑘 → (𝑉𝑙) = (𝑉𝑘))
443442breq2d 5159 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑘 → ((𝑉𝑖) ≤ (𝑉𝑙) ↔ (𝑉𝑖) ≤ (𝑉𝑘)))
444441, 443imbi12d 345 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑘 → (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑙 + 1))) → (𝑉𝑖) ≤ (𝑉𝑙)) ↔ ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑘 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑘 + 1))) → (𝑉𝑖) ≤ (𝑉𝑘))))
445 eleq1w 2817 . . . . . . . . . . . . . . . . . . . . . 22 ( = 𝑖 → ( ∈ (0..^𝑀) ↔ 𝑖 ∈ (0..^𝑀)))
446445anbi2d 630 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝑖 → ((𝜑 ∈ (0..^𝑀)) ↔ (𝜑𝑖 ∈ (0..^𝑀))))
447446anbi1d 631 . . . . . . . . . . . . . . . . . . . 20 ( = 𝑖 → (((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ↔ ((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀))))
448 fveq2 6888 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝑖 → (𝑉) = (𝑉𝑖))
449448breq1d 5157 . . . . . . . . . . . . . . . . . . . 20 ( = 𝑖 → ((𝑉) < (𝑉‘(𝑙 + 1)) ↔ (𝑉𝑖) < (𝑉‘(𝑙 + 1))))
450447, 449anbi12d 632 . . . . . . . . . . . . . . . . . . 19 ( = 𝑖 → ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ↔ (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑙 + 1)))))
451448breq1d 5157 . . . . . . . . . . . . . . . . . . 19 ( = 𝑖 → ((𝑉) ≤ (𝑉𝑙) ↔ (𝑉𝑖) ≤ (𝑉𝑙)))
452450, 451imbi12d 345 . . . . . . . . . . . . . . . . . 18 ( = 𝑖 → (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → (𝑉) ≤ (𝑉𝑙)) ↔ ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑙 + 1))) → (𝑉𝑖) ≤ (𝑉𝑙))))
453452, 404chvarvv 2003 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑙 + 1))) → (𝑉𝑖) ≤ (𝑉𝑙))
454444, 453chvarvv 2003 . . . . . . . . . . . . . . . 16 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑘 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑘 + 1))) → (𝑉𝑖) ≤ (𝑉𝑘))
455408, 109, 435, 454syl21anc 837 . . . . . . . . . . . . . . 15 (𝜒 → (𝑉𝑖) ≤ (𝑉𝑘))
456117, 416letri3d 11352 . . . . . . . . . . . . . . 15 (𝜒 → ((𝑉𝑘) = (𝑉𝑖) ↔ ((𝑉𝑘) ≤ (𝑉𝑖) ∧ (𝑉𝑖) ≤ (𝑉𝑘))))
457407, 455, 456mpbir2and 712 . . . . . . . . . . . . . 14 (𝜒 → (𝑉𝑘) = (𝑉𝑖))
4587, 2, 8fourierdlem34 44792 . . . . . . . . . . . . . . . 16 (𝜑𝑉:(0...𝑀)–1-1→ℝ)
459107, 458syl 17 . . . . . . . . . . . . . . 15 (𝜒𝑉:(0...𝑀)–1-1→ℝ)
460 f1fveq 7256 . . . . . . . . . . . . . . 15 ((𝑉:(0...𝑀)–1-1→ℝ ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑀))) → ((𝑉𝑘) = (𝑉𝑖) ↔ 𝑘 = 𝑖))
461459, 115, 172, 460syl12anc 836 . . . . . . . . . . . . . 14 (𝜒 → ((𝑉𝑘) = (𝑉𝑖) ↔ 𝑘 = 𝑖))
462457, 461mpbid 231 . . . . . . . . . . . . 13 (𝜒𝑘 = 𝑖)
463104, 462sylbir 234 . . . . . . . . . . . 12 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑘 = 𝑖)
464463ex 414 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) → 𝑘 = 𝑖))
465 simpl 484 . . . . . . . . . . . . . 14 ((((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑘 = 𝑖) → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
466 fveq2 6888 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑖 → (𝑄𝑘) = (𝑄𝑖))
467 oveq1 7411 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑖 → (𝑘 + 1) = (𝑖 + 1))
468467fveq2d 6892 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑖 → (𝑄‘(𝑘 + 1)) = (𝑄‘(𝑖 + 1)))
469466, 468oveq12d 7422 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑖 → ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
470469eqcomd 2739 . . . . . . . . . . . . . . 15 (𝑘 = 𝑖 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
471470adantl 483 . . . . . . . . . . . . . 14 ((((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑘 = 𝑖) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
472465, 471sseqtrd 4021 . . . . . . . . . . . . 13 ((((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑘 = 𝑖) → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
473472ex 414 . . . . . . . . . . . 12 (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝑘 = 𝑖 → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))))
474473ad2antlr 726 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) → (𝑘 = 𝑖 → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))))
475464, 474impbid 211 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖))
476475ralrimiva 3147 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ∀𝑘 ∈ (0..^𝑀)(((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖))
477476ex 414 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ∀𝑘 ∈ (0..^𝑀)(((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖)))
478477reximdva 3169 . . . . . . 7 (𝜑 → (∃𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)∀𝑘 ∈ (0..^𝑀)(((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖)))
479103, 478mpd 15 . . . . . 6 (𝜑 → ∃𝑖 ∈ (0..^𝑀)∀𝑘 ∈ (0..^𝑀)(((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖))
480 reu6 3721 . . . . . 6 (∃!𝑘 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ ∃𝑖 ∈ (0..^𝑀)∀𝑘 ∈ (0..^𝑀)(((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖))
481479, 480sylibr 233 . . . . 5 (𝜑 → ∃!𝑘 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
482 fveq2 6888 . . . . . . . 8 (𝑖 = 𝑘 → (𝑄𝑖) = (𝑄𝑘))
483 oveq1 7411 . . . . . . . . 9 (𝑖 = 𝑘 → (𝑖 + 1) = (𝑘 + 1))
484483fveq2d 6892 . . . . . . . 8 (𝑖 = 𝑘 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑘 + 1)))
485482, 484oveq12d 7422 . . . . . . 7 (𝑖 = 𝑘 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
486485sseq2d 4013 . . . . . 6 (𝑖 = 𝑘 → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))))
487486cbvreuvw 3401 . . . . 5 (∃!𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ ∃!𝑘 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
488481, 487sylibr 233 . . . 4 (𝜑 → ∃!𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
489 riotacl 7378 . . . 4 (∃!𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (0..^𝑀))
490488, 489syl 17 . . 3 (𝜑 → (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (0..^𝑀))
4911, 490eqeltrid 2838 . 2 (𝜑𝑈 ∈ (0..^𝑀))
4921eqcomi 2742 . . . 4 (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = 𝑈
493492a1i 11 . . 3 (𝜑 → (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = 𝑈)
494 fveq2 6888 . . . . . . 7 (𝑖 = 𝑈 → (𝑄𝑖) = (𝑄𝑈))
495 oveq1 7411 . . . . . . . 8 (𝑖 = 𝑈 → (𝑖 + 1) = (𝑈 + 1))
496495fveq2d 6892 . . . . . . 7 (𝑖 = 𝑈 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑈 + 1)))
497494, 496oveq12d 7422 . . . . . 6 (𝑖 = 𝑈 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1))))
498497sseq2d 4013 . . . . 5 (𝑖 = 𝑈 → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1)))))
499498riota2 7386 . . . 4 ((𝑈 ∈ (0..^𝑀) ∧ ∃!𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1))) ↔ (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = 𝑈))
500491, 488, 499syl2anc 585 . . 3 (𝜑 → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1))) ↔ (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = 𝑈))
501493, 500mpbird 257 . 2 (𝜑 → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1))))
502491, 501jca 513 1 (𝜑 → (𝑈 ∈ (0..^𝑀) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  wral 3062  wrex 3071  ∃!wreu 3375  {crab 3433  cun 3945  cin 3946  wss 3947  {cpr 4629   class class class wbr 5147  cmpt 5230  ran crn 5676  cio 6490  wf 6536  1-1wf1 6537  1-1-ontowf1o 6539  cfv 6540   Isom wiso 6541  crio 7359  (class class class)co 7404  m cmap 8816  Fincfn 8935  supcsup 9431  cc 11104  cr 11105  0cc0 11106  1c1 11107   + caddc 11109  *cxr 11243   < clt 11244  cle 11245  cmin 11440  -cneg 11441  cn 12208  0cn0 12468  cz 12554  cuz 12818  (,)cioo 13320  [,]cicc 13323  ...cfz 13480  ..^cfzo 13623  chash 14286  πcpi 16006
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185  ax-mulf 11186
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-of 7665  df-om 7851  df-1st 7970  df-2nd 7971  df-supp 8142  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-er 8699  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-fi 9402  df-sup 9433  df-inf 9434  df-oi 9501  df-card 9930  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-z 12555  df-dec 12674  df-uz 12819  df-q 12929  df-rp 12971  df-xneg 13088  df-xadd 13089  df-xmul 13090  df-ioo 13324  df-ioc 13325  df-ico 13326  df-icc 13327  df-fz 13481  df-fzo 13624  df-fl 13753  df-seq 13963  df-exp 14024  df-fac 14230  df-bc 14259  df-hash 14287  df-shft 15010  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-limsup 15411  df-clim 15428  df-rlim 15429  df-sum 15629  df-ef 16007  df-sin 16009  df-cos 16010  df-pi 16012  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-plusg 17206  df-mulr 17207  df-starv 17208  df-sca 17209  df-vsca 17210  df-ip 17211  df-tset 17212  df-ple 17213  df-ds 17215  df-unif 17216  df-hom 17217  df-cco 17218  df-rest 17364  df-topn 17365  df-0g 17383  df-gsum 17384  df-topgen 17385  df-pt 17386  df-prds 17389  df-xrs 17444  df-qtop 17449  df-imas 17450  df-xps 17452  df-mre 17526  df-mrc 17527  df-acs 17529  df-mgm 18557  df-sgrp 18606  df-mnd 18622  df-submnd 18668  df-mulg 18945  df-cntz 19175  df-cmn 19643  df-psmet 20921  df-xmet 20922  df-met 20923  df-bl 20924  df-mopn 20925  df-fbas 20926  df-fg 20927  df-cnfld 20930  df-top 22378  df-topon 22395  df-topsp 22417  df-bases 22431  df-cld 22505  df-ntr 22506  df-cls 22507  df-nei 22584  df-lp 22622  df-perf 22623  df-cn 22713  df-cnp 22714  df-haus 22801  df-tx 23048  df-hmeo 23241  df-fil 23332  df-fm 23424  df-flim 23425  df-flf 23426  df-xms 23808  df-ms 23809  df-tms 23810  df-cncf 24376  df-limc 25365  df-dv 25366
This theorem is referenced by:  fourierdlem86  44843  fourierdlem103  44860  fourierdlem104  44861
  Copyright terms: Public domain W3C validator