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 42318
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 10776 . . . . . . . 8 (𝜑𝐴𝐵)
7 fourierdlem50.p . . . . . . . . . . . . 13 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
8 fourierdlem50.v . . . . . . . . . . . . 13 (𝜑𝑉 ∈ (𝑃𝑀))
97, 2, 8fourierdlem15 42284 . . . . . . . . . . . 12 (𝜑𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
10 pire 24971 . . . . . . . . . . . . . . . 16 π ∈ ℝ
1110renegcli 10935 . . . . . . . . . . . . . . 15 -π ∈ ℝ
1211a1i 11 . . . . . . . . . . . . . 14 (𝜑 → -π ∈ ℝ)
13 fourierdlem50.xre . . . . . . . . . . . . . 14 (𝜑𝑋 ∈ ℝ)
1412, 13readdcld 10658 . . . . . . . . . . . . 13 (𝜑 → (-π + 𝑋) ∈ ℝ)
1510a1i 11 . . . . . . . . . . . . . 14 (𝜑 → π ∈ ℝ)
1615, 13readdcld 10658 . . . . . . . . . . . . 13 (𝜑 → (π + 𝑋) ∈ ℝ)
1714, 16iccssred 41656 . . . . . . . . . . . 12 (𝜑 → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
189, 17fssd 6521 . . . . . . . . . . 11 (𝜑𝑉:(0...𝑀)⟶ℝ)
1918ffvelrnda 6843 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑉𝑖) ∈ ℝ)
2013adantr 481 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℝ)
2119, 20resubcld 11056 . . . . . . . . 9 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) − 𝑋) ∈ ℝ)
22 fourierdlem50.q . . . . . . . . 9 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋))
2321, 22fmptd 6870 . . . . . . . 8 (𝜑𝑄:(0...𝑀)⟶ℝ)
2422a1i 11 . . . . . . . . . . 11 (𝜑𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋)))
25 fveq2 6663 . . . . . . . . . . . . 13 (𝑖 = 0 → (𝑉𝑖) = (𝑉‘0))
2625oveq1d 7160 . . . . . . . . . . . 12 (𝑖 = 0 → ((𝑉𝑖) − 𝑋) = ((𝑉‘0) − 𝑋))
2726adantl 482 . . . . . . . . . . 11 ((𝜑𝑖 = 0) → ((𝑉𝑖) − 𝑋) = ((𝑉‘0) − 𝑋))
28 nnssnn0 11888 . . . . . . . . . . . . . . 15 ℕ ⊆ ℕ0
2928a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ℕ ⊆ ℕ0)
30 nn0uz 12268 . . . . . . . . . . . . . 14 0 = (ℤ‘0)
3129, 30sseqtrdi 4014 . . . . . . . . . . . . 13 (𝜑 → ℕ ⊆ (ℤ‘0))
3231, 2sseldd 3965 . . . . . . . . . . . 12 (𝜑𝑀 ∈ (ℤ‘0))
33 eluzfz1 12902 . . . . . . . . . . . 12 (𝑀 ∈ (ℤ‘0) → 0 ∈ (0...𝑀))
3432, 33syl 17 . . . . . . . . . . 11 (𝜑 → 0 ∈ (0...𝑀))
3518, 34ffvelrnd 6844 . . . . . . . . . . . 12 (𝜑 → (𝑉‘0) ∈ ℝ)
3635, 13resubcld 11056 . . . . . . . . . . 11 (𝜑 → ((𝑉‘0) − 𝑋) ∈ ℝ)
3724, 27, 34, 36fvmptd 6767 . . . . . . . . . 10 (𝜑 → (𝑄‘0) = ((𝑉‘0) − 𝑋))
387fourierdlem2 42271 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ → (𝑉 ∈ (𝑃𝑀) ↔ (𝑉 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))))
392, 38syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑉 ∈ (𝑃𝑀) ↔ (𝑉 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))))
408, 39mpbid 233 . . . . . . . . . . . . . 14 (𝜑 → (𝑉 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1)))))
4140simprd 496 . . . . . . . . . . . . 13 (𝜑 → (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))
4241simpld 495 . . . . . . . . . . . 12 (𝜑 → ((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)))
4342simpld 495 . . . . . . . . . . 11 (𝜑 → (𝑉‘0) = (-π + 𝑋))
4443oveq1d 7160 . . . . . . . . . 10 (𝜑 → ((𝑉‘0) − 𝑋) = ((-π + 𝑋) − 𝑋))
4512recnd 10657 . . . . . . . . . . 11 (𝜑 → -π ∈ ℂ)
4613recnd 10657 . . . . . . . . . . 11 (𝜑𝑋 ∈ ℂ)
4745, 46pncand 10986 . . . . . . . . . 10 (𝜑 → ((-π + 𝑋) − 𝑋) = -π)
4837, 44, 473eqtrd 2857 . . . . . . . . 9 (𝜑 → (𝑄‘0) = -π)
4912rexrd 10679 . . . . . . . . . 10 (𝜑 → -π ∈ ℝ*)
5015rexrd 10679 . . . . . . . . . 10 (𝜑 → π ∈ ℝ*)
51 fourierdlem50.ab . . . . . . . . . . 11 (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
523leidd 11194 . . . . . . . . . . . 12 (𝜑𝐴𝐴)
533, 4, 3, 52, 6eliccd 41655 . . . . . . . . . . 11 (𝜑𝐴 ∈ (𝐴[,]𝐵))
5451, 53sseldd 3965 . . . . . . . . . 10 (𝜑𝐴 ∈ (-π[,]π))
55 iccgelb 12781 . . . . . . . . . 10 ((-π ∈ ℝ* ∧ π ∈ ℝ*𝐴 ∈ (-π[,]π)) → -π ≤ 𝐴)
5649, 50, 54, 55syl3anc 1363 . . . . . . . . 9 (𝜑 → -π ≤ 𝐴)
5748, 56eqbrtrd 5079 . . . . . . . 8 (𝜑 → (𝑄‘0) ≤ 𝐴)
584leidd 11194 . . . . . . . . . . . 12 (𝜑𝐵𝐵)
593, 4, 4, 6, 58eliccd 41655 . . . . . . . . . . 11 (𝜑𝐵 ∈ (𝐴[,]𝐵))
6051, 59sseldd 3965 . . . . . . . . . 10 (𝜑𝐵 ∈ (-π[,]π))
61 iccleub 12780 . . . . . . . . . 10 ((-π ∈ ℝ* ∧ π ∈ ℝ*𝐵 ∈ (-π[,]π)) → 𝐵 ≤ π)
6249, 50, 60, 61syl3anc 1363 . . . . . . . . 9 (𝜑𝐵 ≤ π)
63 fveq2 6663 . . . . . . . . . . . . 13 (𝑖 = 𝑀 → (𝑉𝑖) = (𝑉𝑀))
6463oveq1d 7160 . . . . . . . . . . . 12 (𝑖 = 𝑀 → ((𝑉𝑖) − 𝑋) = ((𝑉𝑀) − 𝑋))
6564adantl 482 . . . . . . . . . . 11 ((𝜑𝑖 = 𝑀) → ((𝑉𝑖) − 𝑋) = ((𝑉𝑀) − 𝑋))
66 eluzfz2 12903 . . . . . . . . . . . 12 (𝑀 ∈ (ℤ‘0) → 𝑀 ∈ (0...𝑀))
6732, 66syl 17 . . . . . . . . . . 11 (𝜑𝑀 ∈ (0...𝑀))
6818, 67ffvelrnd 6844 . . . . . . . . . . . 12 (𝜑 → (𝑉𝑀) ∈ ℝ)
6968, 13resubcld 11056 . . . . . . . . . . 11 (𝜑 → ((𝑉𝑀) − 𝑋) ∈ ℝ)
7024, 65, 67, 69fvmptd 6767 . . . . . . . . . 10 (𝜑 → (𝑄𝑀) = ((𝑉𝑀) − 𝑋))
7142simprd 496 . . . . . . . . . . 11 (𝜑 → (𝑉𝑀) = (π + 𝑋))
7271oveq1d 7160 . . . . . . . . . 10 (𝜑 → ((𝑉𝑀) − 𝑋) = ((π + 𝑋) − 𝑋))
7315recnd 10657 . . . . . . . . . . 11 (𝜑 → π ∈ ℂ)
7473, 46pncand 10986 . . . . . . . . . 10 (𝜑 → ((π + 𝑋) − 𝑋) = π)
7570, 72, 743eqtrrd 2858 . . . . . . . . 9 (𝜑 → π = (𝑄𝑀))
7662, 75breqtrd 5083 . . . . . . . 8 (𝜑𝐵 ≤ (𝑄𝑀))
77 fourierdlem50.j . . . . . . . 8 (𝜑𝐽 ∈ (0..^𝑁))
78 fourierdlem50.t . . . . . . . 8 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))
79 prfi 8781 . . . . . . . . . . . 12 {𝐴, 𝐵} ∈ Fin
8079a1i 11 . . . . . . . . . . 11 (𝜑 → {𝐴, 𝐵} ∈ Fin)
81 fzfid 13329 . . . . . . . . . . . . 13 (𝜑 → (0...𝑀) ∈ Fin)
8222rnmptfi 41303 . . . . . . . . . . . . 13 ((0...𝑀) ∈ Fin → ran 𝑄 ∈ Fin)
8381, 82syl 17 . . . . . . . . . . . 12 (𝜑 → ran 𝑄 ∈ Fin)
84 infi 8730 . . . . . . . . . . . 12 (ran 𝑄 ∈ Fin → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
8583, 84syl 17 . . . . . . . . . . 11 (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
86 unfi 8773 . . . . . . . . . . 11 (({𝐴, 𝐵} ∈ Fin ∧ (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin) → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
8780, 85, 86syl2anc 584 . . . . . . . . . 10 (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
8878, 87eqeltrid 2914 . . . . . . . . 9 (𝜑𝑇 ∈ Fin)
893, 4jca 512 . . . . . . . . . . . 12 (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
90 prssg 4744 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
913, 4, 90syl2anc 584 . . . . . . . . . . . 12 (𝜑 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
9289, 91mpbid 233 . . . . . . . . . . 11 (𝜑 → {𝐴, 𝐵} ⊆ ℝ)
93 inss2 4203 . . . . . . . . . . . . 13 (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴(,)𝐵)
94 ioossre 12786 . . . . . . . . . . . . 13 (𝐴(,)𝐵) ⊆ ℝ
9593, 94sstri 3973 . . . . . . . . . . . 12 (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ
9695a1i 11 . . . . . . . . . . 11 (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ)
9792, 96unssd 4159 . . . . . . . . . 10 (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ ℝ)
9878, 97eqsstrid 4012 . . . . . . . . 9 (𝜑𝑇 ⊆ ℝ)
99 fourierdlem50.s . . . . . . . . 9 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇))
100 fourierdlem50.n . . . . . . . . 9 𝑁 = ((♯‘𝑇) − 1)
10188, 98, 99, 100fourierdlem36 42305 . . . . . . . 8 (𝜑𝑆 Isom < , < ((0...𝑁), 𝑇))
102 eqid 2818 . . . . . . . 8 sup({𝑥 ∈ (0..^𝑀) ∣ (𝑄𝑥) ≤ (𝑆𝐽)}, ℝ, < ) = sup({𝑥 ∈ (0..^𝑀) ∣ (𝑄𝑥) ≤ (𝑆𝐽)}, ℝ, < )
1032, 3, 4, 6, 23, 57, 76, 77, 78, 101, 102fourierdlem20 42289 . . . . . . 7 (𝜑 → ∃𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
104 fourierdlem50.ch . . . . . . . . . . . . 13 (𝜒 ↔ ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))))
105104biimpi 217 . . . . . . . . . . . . . . . . . 18 (𝜒 → ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))))
106 simp-4l 779 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝜑)
107105, 106syl 17 . . . . . . . . . . . . . . . . 17 (𝜒𝜑)
108 simplr 765 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑘 ∈ (0..^𝑀))
109105, 108syl 17 . . . . . . . . . . . . . . . . 17 (𝜒𝑘 ∈ (0..^𝑀))
110107, 109jca 512 . . . . . . . . . . . . . . . 16 (𝜒 → (𝜑𝑘 ∈ (0..^𝑀)))
111 simp-4r 780 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑖 ∈ (0..^𝑀))
112105, 111syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝑖 ∈ (0..^𝑀))
113 elfzofz 13041 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ (0..^𝑀) → 𝑘 ∈ (0...𝑀))
114113ad2antlr 723 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑘 ∈ (0...𝑀))
115105, 114syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜒𝑘 ∈ (0...𝑀))
116107, 18syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒𝑉:(0...𝑀)⟶ℝ)
117116, 115ffvelrnd 6844 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (𝑉𝑘) ∈ ℝ)
118107, 13syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜒𝑋 ∈ ℝ)
119117, 118resubcld 11056 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ((𝑉𝑘) − 𝑋) ∈ ℝ)
120 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 𝑘 → (𝑉𝑖) = (𝑉𝑘))
121120oveq1d 7160 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑘 → ((𝑉𝑖) − 𝑋) = ((𝑉𝑘) − 𝑋))
122121, 22fvmptg 6759 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ (0...𝑀) ∧ ((𝑉𝑘) − 𝑋) ∈ ℝ) → (𝑄𝑘) = ((𝑉𝑘) − 𝑋))
123115, 119, 122syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑄𝑘) = ((𝑉𝑘) − 𝑋))
124123, 119eqeltrd 2910 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄𝑘) ∈ ℝ)
12523adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
126 fzofzp1 13122 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
127126adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
128125, 127ffvelrnd 6844 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
129107, 112, 128syl2anc 584 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℝ)
130 isof1o 7065 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑆 Isom < , < ((0...𝑁), 𝑇) → 𝑆:(0...𝑁)–1-1-onto𝑇)
131101, 130syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑆:(0...𝑁)–1-1-onto𝑇)
132 f1of 6608 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑆:(0...𝑁)–1-1-onto𝑇𝑆:(0...𝑁)⟶𝑇)
133131, 132syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑆:(0...𝑁)⟶𝑇)
134 fzofzp1 13122 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
13577, 134syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
136133, 135ffvelrnd 6844 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ 𝑇)
13798, 136sseldd 3965 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
138107, 137syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
139 elfzofz 13041 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
14077, 139syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐽 ∈ (0...𝑁))
141133, 140ffvelrnd 6844 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑆𝐽) ∈ 𝑇)
14298, 141sseldd 3965 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑆𝐽) ∈ ℝ)
143107, 142syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑆𝐽) ∈ ℝ)
144105simprd 496 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
145124rexrd 10679 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → (𝑄𝑘) ∈ ℝ*)
14623adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
147 fzofzp1 13122 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 ∈ (0..^𝑀) → (𝑘 + 1) ∈ (0...𝑀))
148147adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0..^𝑀)) → (𝑘 + 1) ∈ (0...𝑀))
149146, 148ffvelrnd 6844 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ (0..^𝑀)) → (𝑄‘(𝑘 + 1)) ∈ ℝ)
150149rexrd 10679 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (0..^𝑀)) → (𝑄‘(𝑘 + 1)) ∈ ℝ*)
151110, 150syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → (𝑄‘(𝑘 + 1)) ∈ ℝ*)
152143rexrd 10679 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → (𝑆𝐽) ∈ ℝ*)
153138rexrd 10679 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → (𝑆‘(𝐽 + 1)) ∈ ℝ*)
154 elfzoelz 13026 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
155154zred 12075 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℝ)
156155ltp1d 11558 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐽 ∈ (0..^𝑁) → 𝐽 < (𝐽 + 1))
15777, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐽 < (𝐽 + 1))
158 isoeq5 7063 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) → (𝑆 Isom < , < ((0...𝑁), 𝑇) ↔ 𝑆 Isom < , < ((0...𝑁), ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))))))
15978, 158ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑆 Isom < , < ((0...𝑁), 𝑇) ↔ 𝑆 Isom < , < ((0...𝑁), ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))))
160101, 159sylib 219 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑆 Isom < , < ((0...𝑁), ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))))
161 isorel 7068 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑆 Isom < , < ((0...𝑁), ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))) ∧ (𝐽 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝐽 < (𝐽 + 1) ↔ (𝑆𝐽) < (𝑆‘(𝐽 + 1))))
162160, 140, 135, 161syl12anc 832 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐽 < (𝐽 + 1) ↔ (𝑆𝐽) < (𝑆‘(𝐽 + 1))))
163157, 162mpbid 233 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑆𝐽) < (𝑆‘(𝐽 + 1)))
164107, 163syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → (𝑆𝐽) < (𝑆‘(𝐽 + 1)))
165145, 151, 152, 153, 164ioossioobi 41669 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ ((𝑄𝑘) ≤ (𝑆𝐽) ∧ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑘 + 1)))))
166144, 165mpbid 233 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → ((𝑄𝑘) ≤ (𝑆𝐽) ∧ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑘 + 1))))
167166simpld 495 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑄𝑘) ≤ (𝑆𝐽))
168124, 143, 138, 167, 164lelttrd 10786 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑄𝑘) < (𝑆‘(𝐽 + 1)))
169 elfzofz 13041 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
170169ad2antlr 723 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑖 ∈ (0...𝑀))
171170ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑖 ∈ (0...𝑀))
172105, 171syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒𝑖 ∈ (0...𝑀))
173107, 172, 21syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → ((𝑉𝑖) − 𝑋) ∈ ℝ)
17422fvmpt2 6771 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ (0...𝑀) ∧ ((𝑉𝑖) − 𝑋) ∈ ℝ) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
175172, 173, 174syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
176175, 173eqeltrd 2910 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (𝑄𝑖) ∈ ℝ)
177 simpllr 772 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
178105, 177syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
179176, 129, 143, 138, 164, 178fourierdlem10 42279 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ((𝑄𝑖) ≤ (𝑆𝐽) ∧ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑖 + 1))))
180179simprd 496 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑖 + 1)))
181124, 138, 129, 168, 180ltletrd 10788 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄𝑘) < (𝑄‘(𝑖 + 1)))
182124, 129, 118, 181ltadd2dd 10787 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + (𝑄𝑘)) < (𝑋 + (𝑄‘(𝑖 + 1))))
183123oveq2d 7161 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + (𝑄𝑘)) = (𝑋 + ((𝑉𝑘) − 𝑋)))
184107, 46syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒𝑋 ∈ ℂ)
185117recnd 10657 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑉𝑘) ∈ ℂ)
186184, 185pncan3d 10988 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + ((𝑉𝑘) − 𝑋)) = (𝑉𝑘))
187183, 186eqtr2d 2854 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑉𝑘) = (𝑋 + (𝑄𝑘)))
188112, 126syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑖 + 1) ∈ (0...𝑀))
18918adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
190189, 127ffvelrnd 6844 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
191107, 112, 190syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℝ)
192191, 118resubcld 11056 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
193188, 192jca 512 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ((𝑖 + 1) ∈ (0...𝑀) ∧ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ))
194 eleq1 2897 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑖 + 1) → (𝑘 ∈ (0...𝑀) ↔ (𝑖 + 1) ∈ (0...𝑀)))
195 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = (𝑖 + 1) → (𝑉𝑘) = (𝑉‘(𝑖 + 1)))
196195oveq1d 7160 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = (𝑖 + 1) → ((𝑉𝑘) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
197196eleq1d 2894 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑖 + 1) → (((𝑉𝑘) − 𝑋) ∈ ℝ ↔ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ))
198194, 197anbi12d 630 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = (𝑖 + 1) → ((𝑘 ∈ (0...𝑀) ∧ ((𝑉𝑘) − 𝑋) ∈ ℝ) ↔ ((𝑖 + 1) ∈ (0...𝑀) ∧ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)))
199 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑖 + 1) → (𝑄𝑘) = (𝑄‘(𝑖 + 1)))
200199, 196eqeq12d 2834 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = (𝑖 + 1) → ((𝑄𝑘) = ((𝑉𝑘) − 𝑋) ↔ (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋)))
201198, 200imbi12d 346 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = (𝑖 + 1) → (((𝑘 ∈ (0...𝑀) ∧ ((𝑉𝑘) − 𝑋) ∈ ℝ) → (𝑄𝑘) = ((𝑉𝑘) − 𝑋)) ↔ (((𝑖 + 1) ∈ (0...𝑀) ∧ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))))
202201, 122vtoclg 3565 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 + 1) ∈ (0...𝑀) → (((𝑖 + 1) ∈ (0...𝑀) ∧ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋)))
203188, 193, 202sylc 65 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
204203oveq2d 7161 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)))
205191recnd 10657 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℂ)
206184, 205pncan3d 10988 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)) = (𝑉‘(𝑖 + 1)))
207204, 206eqtr2d 2854 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑉‘(𝑖 + 1)) = (𝑋 + (𝑄‘(𝑖 + 1))))
208182, 187, 2073brtr4d 5089 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑉𝑘) < (𝑉‘(𝑖 + 1)))
209 eleq1w 2892 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑖 → (𝑙 ∈ (0..^𝑀) ↔ 𝑖 ∈ (0..^𝑀)))
210209anbi2d 628 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑖 → (((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ↔ ((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (0..^𝑀))))
211 oveq1 7152 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑖 → (𝑙 + 1) = (𝑖 + 1))
212211fveq2d 6667 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑖 → (𝑉‘(𝑙 + 1)) = (𝑉‘(𝑖 + 1)))
213212breq2d 5069 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑖 → ((𝑉𝑘) < (𝑉‘(𝑙 + 1)) ↔ (𝑉𝑘) < (𝑉‘(𝑖 + 1))))
214210, 213anbi12d 630 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑖 → ((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑙 + 1))) ↔ (((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑖 + 1)))))
215 fveq2 6663 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑖 → (𝑉𝑙) = (𝑉𝑖))
216215breq2d 5069 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑖 → ((𝑉𝑘) ≤ (𝑉𝑙) ↔ (𝑉𝑘) ≤ (𝑉𝑖)))
217214, 216imbi12d 346 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑖 → (((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑙 + 1))) → (𝑉𝑘) ≤ (𝑉𝑙)) ↔ ((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑖 + 1))) → (𝑉𝑘) ≤ (𝑉𝑖))))
218 eleq1w 2892 . . . . . . . . . . . . . . . . . . . . . 22 ( = 𝑘 → ( ∈ (0..^𝑀) ↔ 𝑘 ∈ (0..^𝑀)))
219218anbi2d 628 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝑘 → ((𝜑 ∈ (0..^𝑀)) ↔ (𝜑𝑘 ∈ (0..^𝑀))))
220219anbi1d 629 . . . . . . . . . . . . . . . . . . . 20 ( = 𝑘 → (((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ↔ ((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀))))
221 fveq2 6663 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝑘 → (𝑉) = (𝑉𝑘))
222221breq1d 5067 . . . . . . . . . . . . . . . . . . . 20 ( = 𝑘 → ((𝑉) < (𝑉‘(𝑙 + 1)) ↔ (𝑉𝑘) < (𝑉‘(𝑙 + 1))))
223220, 222anbi12d 630 . . . . . . . . . . . . . . . . . . 19 ( = 𝑘 → ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ↔ (((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑙 + 1)))))
224221breq1d 5067 . . . . . . . . . . . . . . . . . . 19 ( = 𝑘 → ((𝑉) ≤ (𝑉𝑙) ↔ (𝑉𝑘) ≤ (𝑉𝑙)))
225223, 224imbi12d 346 . . . . . . . . . . . . . . . . . 18 ( = 𝑘 → (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → (𝑉) ≤ (𝑉𝑙)) ↔ ((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑙 + 1))) → (𝑉𝑘) ≤ (𝑉𝑙))))
226 elfzoelz 13026 . . . . . . . . . . . . . . . . . . . . 21 ( ∈ (0..^𝑀) → ∈ ℤ)
227226ad3antlr 727 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → ∈ ℤ)
228 elfzoelz 13026 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 ∈ (0..^𝑀) → 𝑙 ∈ ℤ)
229228ad2antlr 723 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → 𝑙 ∈ ℤ)
230 simplr 765 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ ¬ < (𝑙 + 1)) → (𝑉) < (𝑉‘(𝑙 + 1)))
23118adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑙 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
232 fzofzp1 13122 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (0..^𝑀) → (𝑙 + 1) ∈ (0...𝑀))
233232adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑙 ∈ (0..^𝑀)) → (𝑙 + 1) ∈ (0...𝑀))
234231, 233ffvelrnd 6844 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑙 ∈ (0..^𝑀)) → (𝑉‘(𝑙 + 1)) ∈ ℝ)
235234adantlr 711 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) → (𝑉‘(𝑙 + 1)) ∈ ℝ)
236235adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → (𝑉‘(𝑙 + 1)) ∈ ℝ)
23718adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
238 elfzofz 13041 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ( ∈ (0..^𝑀) → ∈ (0...𝑀))
239238adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∈ (0..^𝑀)) → ∈ (0...𝑀))
240237, 239ffvelrnd 6844 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∈ (0..^𝑀)) → (𝑉) ∈ ℝ)
241240ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → (𝑉) ∈ ℝ)
242228zred 12075 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (0..^𝑀) → 𝑙 ∈ ℝ)
243 peano2re 10801 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ ℝ → (𝑙 + 1) ∈ ℝ)
244242, 243syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑙 ∈ (0..^𝑀) → (𝑙 + 1) ∈ ℝ)
245244ad2antlr 723 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → (𝑙 + 1) ∈ ℝ)
246226zred 12075 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ( ∈ (0..^𝑀) → ∈ ℝ)
247246ad3antlr 727 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → ∈ ℝ)
248 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → ¬ < (𝑙 + 1))
249245, 247, 248nltled 10778 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → (𝑙 + 1) ≤ )
250228peano2zd 12078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (0..^𝑀) → (𝑙 + 1) ∈ ℤ)
251250ad2antlr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → (𝑙 + 1) ∈ ℤ)
252226ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → ∈ ℤ)
253 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → (𝑙 + 1) ≤ )
254 eluz2 12237 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ( ∈ (ℤ‘(𝑙 + 1)) ↔ ((𝑙 + 1) ∈ ℤ ∧ ∈ ℤ ∧ (𝑙 + 1) ≤ ))
255251, 252, 253, 254syl3anbrc 1335 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → ∈ (ℤ‘(𝑙 + 1)))
256255adantlll 714 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → ∈ (ℤ‘(𝑙 + 1)))
257 simplll 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝜑)
258 0zd 11981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 ∈ ℤ)
259 elfzoel2 13025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ( ∈ (0..^𝑀) → 𝑀 ∈ ℤ)
260259ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑀 ∈ ℤ)
261 elfzelz 12896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ ((𝑙 + 1)...) → 𝑖 ∈ ℤ)
262261adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 ∈ ℤ)
263258, 260, 2623jca 1120 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ))
264 0red 10632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 ∈ ℝ)
265261zred 12075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑖 ∈ ((𝑙 + 1)...) → 𝑖 ∈ ℝ)
266265adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 ∈ ℝ)
267242adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑙 ∈ ℝ)
268 elfzole1 13034 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑙 ∈ (0..^𝑀) → 0 ≤ 𝑙)
269268adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 ≤ 𝑙)
270267, 243syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → (𝑙 + 1) ∈ ℝ)
271267ltp1d 11558 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑙 < (𝑙 + 1))
272 elfzle1 12898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑖 ∈ ((𝑙 + 1)...) → (𝑙 + 1) ≤ 𝑖)
273272adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → (𝑙 + 1) ≤ 𝑖)
274267, 270, 266, 271, 273ltletrd 10788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑙 < 𝑖)
275264, 267, 266, 269, 274lelttrd 10786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 < 𝑖)
276264, 266, 275ltled 10776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 ≤ 𝑖)
277276adantll 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 ≤ 𝑖)
278265adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 ∈ ℝ)
279259zred 12075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( ∈ (0..^𝑀) → 𝑀 ∈ ℝ)
280279adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑀 ∈ ℝ)
281246adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → ∈ ℝ)
282 elfzle2 12899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑖 ∈ ((𝑙 + 1)...) → 𝑖)
283282adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖)
284 elfzolt2 13035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ( ∈ (0..^𝑀) → < 𝑀)
285284adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → < 𝑀)
286278, 281, 280, 283, 285lelttrd 10786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 < 𝑀)
287278, 280, 286ltled 10776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖𝑀)
288287adantlr 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖𝑀)
289263, 277, 288jca32 516 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (0 ≤ 𝑖𝑖𝑀)))
290 elfz2 12887 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (0 ≤ 𝑖𝑖𝑀)))
291289, 290sylibr 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 ∈ (0...𝑀))
292291adantlll 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 ∈ (0...𝑀))
293257, 292, 19syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → (𝑉𝑖) ∈ ℝ)
294293adantlr 711 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → (𝑉𝑖) ∈ ℝ)
295 simplll 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝜑)
296 0zd 11981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 0 ∈ ℤ)
297 elfzelz 12896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 ∈ ((𝑙 + 1)...( − 1)) → 𝑖 ∈ ℤ)
298297adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ ℤ)
299 0red 10632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 0 ∈ ℝ)
300298zred 12075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ ℝ)
301242adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑙 ∈ ℝ)
302268adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 0 ≤ 𝑙)
303301, 243syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → (𝑙 + 1) ∈ ℝ)
304301ltp1d 11558 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑙 < (𝑙 + 1))
305 elfzle1 12898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑖 ∈ ((𝑙 + 1)...( − 1)) → (𝑙 + 1) ≤ 𝑖)
306305adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → (𝑙 + 1) ≤ 𝑖)
307301, 303, 300, 304, 306ltletrd 10788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑙 < 𝑖)
308299, 301, 300, 302, 307lelttrd 10786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 0 < 𝑖)
309299, 300, 308ltled 10776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 0 ≤ 𝑖)
310 eluz2 12237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (ℤ‘0) ↔ (0 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 0 ≤ 𝑖))
311296, 298, 309, 310syl3anbrc 1335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ (ℤ‘0))
312311adantll 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ (ℤ‘0))
313 elfzoel2 13025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (0..^𝑀) → 𝑀 ∈ ℤ)
314313ad2antlr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑀 ∈ ℤ)
315297zred 12075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ ((𝑙 + 1)...( − 1)) → 𝑖 ∈ ℝ)
316315adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ ℝ)
317 peano2rem 10941 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( ∈ ℝ → ( − 1) ∈ ℝ)
318246, 317syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ( ∈ (0..^𝑀) → ( − 1) ∈ ℝ)
319318adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → ( − 1) ∈ ℝ)
320279adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑀 ∈ ℝ)
321 elfzle2 12899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ ((𝑙 + 1)...( − 1)) → 𝑖 ≤ ( − 1))
322321adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ≤ ( − 1))
323246ltm1d 11560 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( ∈ (0..^𝑀) → ( − 1) < )
324318, 246, 279, 323, 284lttrd 10789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ( ∈ (0..^𝑀) → ( − 1) < 𝑀)
325324adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → ( − 1) < 𝑀)
326316, 319, 320, 322, 325lelttrd 10786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 < 𝑀)
327326adantll 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 < 𝑀)
328327adantlr 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 < 𝑀)
329 elfzo2 13029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ (0..^𝑀) ↔ (𝑖 ∈ (ℤ‘0) ∧ 𝑀 ∈ ℤ ∧ 𝑖 < 𝑀))
330312, 314, 328, 329syl3anbrc 1335 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ (0..^𝑀))
331169, 19sylan2 592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ∈ ℝ)
33241simprd 496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1)))
333332r19.21bi 3205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) < (𝑉‘(𝑖 + 1)))
334331, 190, 333ltled 10776 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ≤ (𝑉‘(𝑖 + 1)))
335295, 330, 334syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → (𝑉𝑖) ≤ (𝑉‘(𝑖 + 1)))
336335adantlr 711 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → (𝑉𝑖) ≤ (𝑉‘(𝑖 + 1)))
337256, 294, 336monoord 13388 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → (𝑉‘(𝑙 + 1)) ≤ (𝑉))
338249, 337syldan 591 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → (𝑉‘(𝑙 + 1)) ≤ (𝑉))
339236, 241, 338lensymd 10779 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → ¬ (𝑉) < (𝑉‘(𝑙 + 1)))
340339adantlr 711 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ ¬ < (𝑙 + 1)) → ¬ (𝑉) < (𝑉‘(𝑙 + 1)))
341230, 340condan 814 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → < (𝑙 + 1))
342 zleltp1 12021 . . . . . . . . . . . . . . . . . . . . . 22 (( ∈ ℤ ∧ 𝑙 ∈ ℤ) → (𝑙 < (𝑙 + 1)))
343227, 229, 342syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → (𝑙 < (𝑙 + 1)))
344341, 343mpbird 258 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → 𝑙)
345 eluz2 12237 . . . . . . . . . . . . . . . . . . . 20 (𝑙 ∈ (ℤ) ↔ ( ∈ ℤ ∧ 𝑙 ∈ ℤ ∧ 𝑙))
346227, 229, 344, 345syl3anbrc 1335 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → 𝑙 ∈ (ℤ))
34718ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑉:(0...𝑀)⟶ℝ)
348 0zd 11981 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 0 ∈ ℤ)
349259ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑀 ∈ ℤ)
350 elfzelz 12896 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (...𝑙) → 𝑖 ∈ ℤ)
351350adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 ∈ ℤ)
352348, 349, 3513jca 1120 . . . . . . . . . . . . . . . . . . . . . . . 24 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ))
353 0red 10632 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 0 ∈ ℝ)
354246adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → ∈ ℝ)
355350zred 12075 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (...𝑙) → 𝑖 ∈ ℝ)
356355adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 ∈ ℝ)
357 elfzole1 13034 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ( ∈ (0..^𝑀) → 0 ≤ )
358357adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 0 ≤ )
359 elfzle1 12898 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (...𝑙) → 𝑖)
360359adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖)
361353, 354, 356, 358, 360letrd 10785 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 0 ≤ 𝑖)
362361adantlr 711 . . . . . . . . . . . . . . . . . . . . . . . 24 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 0 ≤ 𝑖)
363355adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 ∈ ℝ)
364313zred 12075 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑙 ∈ (0..^𝑀) → 𝑀 ∈ ℝ)
365364adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑀 ∈ ℝ)
366242adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑙 ∈ ℝ)
367 elfzle2 12899 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ (...𝑙) → 𝑖𝑙)
368367adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖𝑙)
369 elfzolt2 13035 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (0..^𝑀) → 𝑙 < 𝑀)
370369adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑙 < 𝑀)
371363, 366, 365, 368, 370lelttrd 10786 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 < 𝑀)
372363, 365, 371ltled 10776 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖𝑀)
373372adantll 710 . . . . . . . . . . . . . . . . . . . . . . . 24 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑖𝑀)
374352, 362, 373jca32 516 . . . . . . . . . . . . . . . . . . . . . . 23 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (0 ≤ 𝑖𝑖𝑀)))
375374, 290sylibr 235 . . . . . . . . . . . . . . . . . . . . . 22 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 ∈ (0...𝑀))
376375adantlll 714 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 ∈ (0...𝑀))
377347, 376ffvelrnd 6844 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → (𝑉𝑖) ∈ ℝ)
378377adantlr 711 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...𝑙)) → (𝑉𝑖) ∈ ℝ)
379 simp-4l 779 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝜑)
380 0zd 11981 . . . . . . . . . . . . . . . . . . . . . . . 24 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 0 ∈ ℤ)
381 elfzelz 12896 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ (...(𝑙 − 1)) → 𝑖 ∈ ℤ)
382381adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ ℤ)
383 0red 10632 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 0 ∈ ℝ)
384246adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → ∈ ℝ)
385382zred 12075 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ ℝ)
386357adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 0 ≤ )
387 elfzle1 12898 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (...(𝑙 − 1)) → 𝑖)
388387adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖)
389383, 384, 385, 386, 388letrd 10785 . . . . . . . . . . . . . . . . . . . . . . . 24 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 0 ≤ 𝑖)
390380, 382, 389, 310syl3anbrc 1335 . . . . . . . . . . . . . . . . . . . . . . 23 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ (ℤ‘0))
391390adantll 710 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ (ℤ‘0))
392391ad4ant14 748 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ (ℤ‘0))
393313ad3antlr 727 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑀 ∈ ℤ)
394381zred 12075 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ (...(𝑙 − 1)) → 𝑖 ∈ ℝ)
395394adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ ℝ)
396242adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑙 ∈ ℝ)
397364adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑀 ∈ ℝ)
398 elfzle2 12899 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (...(𝑙 − 1)) → 𝑖 ≤ (𝑙 − 1))
399398adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ≤ (𝑙 − 1))
400 zltlem1 12023 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑖 ∈ ℤ ∧ 𝑙 ∈ ℤ) → (𝑖 < 𝑙𝑖 ≤ (𝑙 − 1)))
401381, 228, 400syl2anr 596 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → (𝑖 < 𝑙𝑖 ≤ (𝑙 − 1)))
402399, 401mpbird 258 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 < 𝑙)
403369adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑙 < 𝑀)
404395, 396, 397, 402, 403lttrd 10789 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 < 𝑀)
405404adantll 710 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 < 𝑀)
406405adantlr 711 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 < 𝑀)
407392, 393, 406, 329syl3anbrc 1335 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ (0..^𝑀))
408379, 407, 334syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → (𝑉𝑖) ≤ (𝑉‘(𝑖 + 1)))
409346, 378, 408monoord 13388 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → (𝑉) ≤ (𝑉𝑙))
410225, 409chvarvv 1996 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑙 + 1))) → (𝑉𝑘) ≤ (𝑉𝑙))
411217, 410chvarvv 1996 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑖 + 1))) → (𝑉𝑘) ≤ (𝑉𝑖))
412110, 112, 208, 411syl21anc 833 . . . . . . . . . . . . . . 15 (𝜒 → (𝑉𝑘) ≤ (𝑉𝑖))
413107, 112jca 512 . . . . . . . . . . . . . . . 16 (𝜒 → (𝜑𝑖 ∈ (0..^𝑀)))
414110, 149syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄‘(𝑘 + 1)) ∈ ℝ)
415179simpld 495 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑄𝑖) ≤ (𝑆𝐽))
416176, 143, 138, 415, 164lelttrd 10786 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑄𝑖) < (𝑆‘(𝐽 + 1)))
417166simprd 496 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑘 + 1)))
418176, 138, 414, 416, 417ltletrd 10788 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄𝑖) < (𝑄‘(𝑘 + 1)))
419176, 414, 118, 418ltadd2dd 10787 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + (𝑄𝑖)) < (𝑋 + (𝑄‘(𝑘 + 1))))
420175oveq2d 7161 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + (𝑄𝑖)) = (𝑋 + ((𝑉𝑖) − 𝑋)))
421107, 172, 19syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑉𝑖) ∈ ℝ)
422421recnd 10657 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑉𝑖) ∈ ℂ)
423184, 422pncan3d 10988 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + ((𝑉𝑖) − 𝑋)) = (𝑉𝑖))
424420, 423eqtr2d 2854 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑉𝑖) = (𝑋 + (𝑄𝑖)))
42522a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0..^𝑀)) → 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋)))
426 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = (𝑘 + 1) → (𝑉𝑖) = (𝑉‘(𝑘 + 1)))
427426oveq1d 7160 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = (𝑘 + 1) → ((𝑉𝑖) − 𝑋) = ((𝑉‘(𝑘 + 1)) − 𝑋))
428427adantl 482 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑖 = (𝑘 + 1)) → ((𝑉𝑖) − 𝑋) = ((𝑉‘(𝑘 + 1)) − 𝑋))
42918adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
430429, 148ffvelrnd 6844 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (0..^𝑀)) → (𝑉‘(𝑘 + 1)) ∈ ℝ)
43113adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
432430, 431resubcld 11056 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0..^𝑀)) → ((𝑉‘(𝑘 + 1)) − 𝑋) ∈ ℝ)
433425, 428, 148, 432fvmptd 6767 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0..^𝑀)) → (𝑄‘(𝑘 + 1)) = ((𝑉‘(𝑘 + 1)) − 𝑋))
434107, 109, 433syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑄‘(𝑘 + 1)) = ((𝑉‘(𝑘 + 1)) − 𝑋))
435434oveq2d 7161 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + (𝑄‘(𝑘 + 1))) = (𝑋 + ((𝑉‘(𝑘 + 1)) − 𝑋)))
436110, 430syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑉‘(𝑘 + 1)) ∈ ℝ)
437436recnd 10657 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑉‘(𝑘 + 1)) ∈ ℂ)
438184, 437pncan3d 10988 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + ((𝑉‘(𝑘 + 1)) − 𝑋)) = (𝑉‘(𝑘 + 1)))
439435, 438eqtr2d 2854 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑉‘(𝑘 + 1)) = (𝑋 + (𝑄‘(𝑘 + 1))))
440419, 424, 4393brtr4d 5089 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑉𝑖) < (𝑉‘(𝑘 + 1)))
441 eleq1w 2892 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑘 → (𝑙 ∈ (0..^𝑀) ↔ 𝑘 ∈ (0..^𝑀)))
442441anbi2d 628 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑘 → (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ↔ ((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑘 ∈ (0..^𝑀))))
443 oveq1 7152 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑘 → (𝑙 + 1) = (𝑘 + 1))
444443fveq2d 6667 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑘 → (𝑉‘(𝑙 + 1)) = (𝑉‘(𝑘 + 1)))
445444breq2d 5069 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑘 → ((𝑉𝑖) < (𝑉‘(𝑙 + 1)) ↔ (𝑉𝑖) < (𝑉‘(𝑘 + 1))))
446442, 445anbi12d 630 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑘 → ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑙 + 1))) ↔ (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑘 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑘 + 1)))))
447 fveq2 6663 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑘 → (𝑉𝑙) = (𝑉𝑘))
448447breq2d 5069 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑘 → ((𝑉𝑖) ≤ (𝑉𝑙) ↔ (𝑉𝑖) ≤ (𝑉𝑘)))
449446, 448imbi12d 346 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑘 → (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑙 + 1))) → (𝑉𝑖) ≤ (𝑉𝑙)) ↔ ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑘 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑘 + 1))) → (𝑉𝑖) ≤ (𝑉𝑘))))
450 eleq1w 2892 . . . . . . . . . . . . . . . . . . . . . 22 ( = 𝑖 → ( ∈ (0..^𝑀) ↔ 𝑖 ∈ (0..^𝑀)))
451450anbi2d 628 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝑖 → ((𝜑 ∈ (0..^𝑀)) ↔ (𝜑𝑖 ∈ (0..^𝑀))))
452451anbi1d 629 . . . . . . . . . . . . . . . . . . . 20 ( = 𝑖 → (((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ↔ ((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀))))
453 fveq2 6663 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝑖 → (𝑉) = (𝑉𝑖))
454453breq1d 5067 . . . . . . . . . . . . . . . . . . . 20 ( = 𝑖 → ((𝑉) < (𝑉‘(𝑙 + 1)) ↔ (𝑉𝑖) < (𝑉‘(𝑙 + 1))))
455452, 454anbi12d 630 . . . . . . . . . . . . . . . . . . 19 ( = 𝑖 → ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ↔ (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑙 + 1)))))
456453breq1d 5067 . . . . . . . . . . . . . . . . . . 19 ( = 𝑖 → ((𝑉) ≤ (𝑉𝑙) ↔ (𝑉𝑖) ≤ (𝑉𝑙)))
457455, 456imbi12d 346 . . . . . . . . . . . . . . . . . 18 ( = 𝑖 → (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → (𝑉) ≤ (𝑉𝑙)) ↔ ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑙 + 1))) → (𝑉𝑖) ≤ (𝑉𝑙))))
458457, 409chvarvv 1996 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑙 + 1))) → (𝑉𝑖) ≤ (𝑉𝑙))
459449, 458chvarvv 1996 . . . . . . . . . . . . . . . 16 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑘 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑘 + 1))) → (𝑉𝑖) ≤ (𝑉𝑘))
460413, 109, 440, 459syl21anc 833 . . . . . . . . . . . . . . 15 (𝜒 → (𝑉𝑖) ≤ (𝑉𝑘))
461117, 421letri3d 10770 . . . . . . . . . . . . . . 15 (𝜒 → ((𝑉𝑘) = (𝑉𝑖) ↔ ((𝑉𝑘) ≤ (𝑉𝑖) ∧ (𝑉𝑖) ≤ (𝑉𝑘))))
462412, 460, 461mpbir2and 709 . . . . . . . . . . . . . 14 (𝜒 → (𝑉𝑘) = (𝑉𝑖))
4637, 2, 8fourierdlem34 42303 . . . . . . . . . . . . . . . 16 (𝜑𝑉:(0...𝑀)–1-1→ℝ)
464107, 463syl 17 . . . . . . . . . . . . . . 15 (𝜒𝑉:(0...𝑀)–1-1→ℝ)
465 f1fveq 7011 . . . . . . . . . . . . . . 15 ((𝑉:(0...𝑀)–1-1→ℝ ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑀))) → ((𝑉𝑘) = (𝑉𝑖) ↔ 𝑘 = 𝑖))
466464, 115, 172, 465syl12anc 832 . . . . . . . . . . . . . 14 (𝜒 → ((𝑉𝑘) = (𝑉𝑖) ↔ 𝑘 = 𝑖))
467462, 466mpbid 233 . . . . . . . . . . . . 13 (𝜒𝑘 = 𝑖)
468104, 467sylbir 236 . . . . . . . . . . . 12 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑘 = 𝑖)
469468ex 413 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) → 𝑘 = 𝑖))
470 simpl 483 . . . . . . . . . . . . . 14 ((((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑘 = 𝑖) → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
471 fveq2 6663 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑖 → (𝑄𝑘) = (𝑄𝑖))
472 oveq1 7152 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑖 → (𝑘 + 1) = (𝑖 + 1))
473472fveq2d 6667 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑖 → (𝑄‘(𝑘 + 1)) = (𝑄‘(𝑖 + 1)))
474471, 473oveq12d 7163 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑖 → ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
475474eqcomd 2824 . . . . . . . . . . . . . . 15 (𝑘 = 𝑖 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
476475adantl 482 . . . . . . . . . . . . . 14 ((((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑘 = 𝑖) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
477470, 476sseqtrd 4004 . . . . . . . . . . . . 13 ((((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑘 = 𝑖) → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
478477ex 413 . . . . . . . . . . . 12 (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝑘 = 𝑖 → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))))
479478ad2antlr 723 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) → (𝑘 = 𝑖 → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))))
480469, 479impbid 213 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖))
481480ralrimiva 3179 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ∀𝑘 ∈ (0..^𝑀)(((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖))
482481ex 413 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ∀𝑘 ∈ (0..^𝑀)(((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖)))
483482reximdva 3271 . . . . . . 7 (𝜑 → (∃𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)∀𝑘 ∈ (0..^𝑀)(((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖)))
484103, 483mpd 15 . . . . . 6 (𝜑 → ∃𝑖 ∈ (0..^𝑀)∀𝑘 ∈ (0..^𝑀)(((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖))
485 reu6 3714 . . . . . 6 (∃!𝑘 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ ∃𝑖 ∈ (0..^𝑀)∀𝑘 ∈ (0..^𝑀)(((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖))
486484, 485sylibr 235 . . . . 5 (𝜑 → ∃!𝑘 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
487 fveq2 6663 . . . . . . . 8 (𝑖 = 𝑘 → (𝑄𝑖) = (𝑄𝑘))
488 oveq1 7152 . . . . . . . . 9 (𝑖 = 𝑘 → (𝑖 + 1) = (𝑘 + 1))
489488fveq2d 6667 . . . . . . . 8 (𝑖 = 𝑘 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑘 + 1)))
490487, 489oveq12d 7163 . . . . . . 7 (𝑖 = 𝑘 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
491490sseq2d 3996 . . . . . 6 (𝑖 = 𝑘 → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))))
492491cbvreuvw 3449 . . . . 5 (∃!𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ ∃!𝑘 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
493486, 492sylibr 235 . . . 4 (𝜑 → ∃!𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
494 riotacl 7120 . . . 4 (∃!𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (0..^𝑀))
495493, 494syl 17 . . 3 (𝜑 → (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (0..^𝑀))
4961, 495eqeltrid 2914 . 2 (𝜑𝑈 ∈ (0..^𝑀))
4971eqcomi 2827 . . . 4 (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = 𝑈
498497a1i 11 . . 3 (𝜑 → (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = 𝑈)
499 fveq2 6663 . . . . . . 7 (𝑖 = 𝑈 → (𝑄𝑖) = (𝑄𝑈))
500 oveq1 7152 . . . . . . . 8 (𝑖 = 𝑈 → (𝑖 + 1) = (𝑈 + 1))
501500fveq2d 6667 . . . . . . 7 (𝑖 = 𝑈 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑈 + 1)))
502499, 501oveq12d 7163 . . . . . 6 (𝑖 = 𝑈 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1))))
503502sseq2d 3996 . . . . 5 (𝑖 = 𝑈 → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1)))))
504503riota2 7128 . . . 4 ((𝑈 ∈ (0..^𝑀) ∧ ∃!𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1))) ↔ (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = 𝑈))
505496, 493, 504syl2anc 584 . . 3 (𝜑 → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1))) ↔ (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = 𝑈))
506498, 505mpbird 258 . 2 (𝜑 → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1))))
507496, 506jca 512 1 (𝜑 → (𝑈 ∈ (0..^𝑀) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1079   = wceq 1528  wcel 2105  wral 3135  wrex 3136  ∃!wreu 3137  {crab 3139  cun 3931  cin 3932  wss 3933  {cpr 4559   class class class wbr 5057  cmpt 5137  ran crn 5549  cio 6305  wf 6344  1-1wf1 6345  1-1-ontowf1o 6347  cfv 6348   Isom wiso 6349  crio 7102  (class class class)co 7145  m cmap 8395  Fincfn 8497  supcsup 8892  cc 10523  cr 10524  0cc0 10525  1c1 10526   + caddc 10528  *cxr 10662   < clt 10663  cle 10664  cmin 10858  -cneg 10859  cn 11626  0cn0 11885  cz 11969  cuz 12231  (,)cioo 12726  [,]cicc 12729  ...cfz 12880  ..^cfzo 13021  chash 13678  πcpi 15408
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-inf2 9092  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602  ax-pre-sup 10603  ax-addf 10604  ax-mulf 10605
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-iin 4913  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7398  df-om 7570  df-1st 7678  df-2nd 7679  df-supp 7820  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-2o 8092  df-oadd 8095  df-er 8278  df-map 8397  df-pm 8398  df-ixp 8450  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-fsupp 8822  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-card 9356  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286  df-nn 11627  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-z 11970  df-dec 12087  df-uz 12232  df-q 12337  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-ioo 12730  df-ioc 12731  df-ico 12732  df-icc 12733  df-fz 12881  df-fzo 13022  df-fl 13150  df-seq 13358  df-exp 13418  df-fac 13622  df-bc 13651  df-hash 13679  df-shft 14414  df-cj 14446  df-re 14447  df-im 14448  df-sqrt 14582  df-abs 14583  df-limsup 14816  df-clim 14833  df-rlim 14834  df-sum 15031  df-ef 15409  df-sin 15411  df-cos 15412  df-pi 15414  df-struct 16473  df-ndx 16474  df-slot 16475  df-base 16477  df-sets 16478  df-ress 16479  df-plusg 16566  df-mulr 16567  df-starv 16568  df-sca 16569  df-vsca 16570  df-ip 16571  df-tset 16572  df-ple 16573  df-ds 16575  df-unif 16576  df-hom 16577  df-cco 16578  df-rest 16684  df-topn 16685  df-0g 16703  df-gsum 16704  df-topgen 16705  df-pt 16706  df-prds 16709  df-xrs 16763  df-qtop 16768  df-imas 16769  df-xps 16771  df-mre 16845  df-mrc 16846  df-acs 16848  df-mgm 17840  df-sgrp 17889  df-mnd 17900  df-submnd 17945  df-mulg 18163  df-cntz 18385  df-cmn 18837  df-psmet 20465  df-xmet 20466  df-met 20467  df-bl 20468  df-mopn 20469  df-fbas 20470  df-fg 20471  df-cnfld 20474  df-top 21430  df-topon 21447  df-topsp 21469  df-bases 21482  df-cld 21555  df-ntr 21556  df-cls 21557  df-nei 21634  df-lp 21672  df-perf 21673  df-cn 21763  df-cnp 21764  df-haus 21851  df-tx 22098  df-hmeo 22291  df-fil 22382  df-fm 22474  df-flim 22475  df-flf 22476  df-xms 22857  df-ms 22858  df-tms 22859  df-cncf 23413  df-limc 24391  df-dv 24392
This theorem is referenced by:  fourierdlem86  42354  fourierdlem103  42371  fourierdlem104  42372
  Copyright terms: Public domain W3C validator