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 41010
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 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (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 10439 . . . . . . . 8 (𝜑𝐴𝐵)
7 fourierdlem50.p . . . . . . . . . . . . 13 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
8 fourierdlem50.v . . . . . . . . . . . . 13 (𝜑𝑉 ∈ (𝑃𝑀))
97, 2, 8fourierdlem15 40976 . . . . . . . . . . . 12 (𝜑𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
10 pire 24502 . . . . . . . . . . . . . . . 16 π ∈ ℝ
1110renegcli 10596 . . . . . . . . . . . . . . 15 -π ∈ ℝ
1211a1i 11 . . . . . . . . . . . . . 14 (𝜑 → -π ∈ ℝ)
13 fourierdlem50.xre . . . . . . . . . . . . . 14 (𝜑𝑋 ∈ ℝ)
1412, 13readdcld 10323 . . . . . . . . . . . . 13 (𝜑 → (-π + 𝑋) ∈ ℝ)
1510a1i 11 . . . . . . . . . . . . . 14 (𝜑 → π ∈ ℝ)
1615, 13readdcld 10323 . . . . . . . . . . . . 13 (𝜑 → (π + 𝑋) ∈ ℝ)
1714, 16iccssred 40369 . . . . . . . . . . . 12 (𝜑 → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
189, 17fssd 6237 . . . . . . . . . . 11 (𝜑𝑉:(0...𝑀)⟶ℝ)
1918ffvelrnda 6549 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑉𝑖) ∈ ℝ)
2013adantr 472 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℝ)
2119, 20resubcld 10712 . . . . . . . . 9 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) − 𝑋) ∈ ℝ)
22 fourierdlem50.q . . . . . . . . 9 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋))
2321, 22fmptd 6574 . . . . . . . 8 (𝜑𝑄:(0...𝑀)⟶ℝ)
2422a1i 11 . . . . . . . . . . 11 (𝜑𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋)))
25 fveq2 6375 . . . . . . . . . . . . 13 (𝑖 = 0 → (𝑉𝑖) = (𝑉‘0))
2625oveq1d 6857 . . . . . . . . . . . 12 (𝑖 = 0 → ((𝑉𝑖) − 𝑋) = ((𝑉‘0) − 𝑋))
2726adantl 473 . . . . . . . . . . 11 ((𝜑𝑖 = 0) → ((𝑉𝑖) − 𝑋) = ((𝑉‘0) − 𝑋))
28 nnssnn0 11541 . . . . . . . . . . . . . . 15 ℕ ⊆ ℕ0
2928a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ℕ ⊆ ℕ0)
30 nn0uz 11922 . . . . . . . . . . . . . 14 0 = (ℤ‘0)
3129, 30syl6sseq 3811 . . . . . . . . . . . . 13 (𝜑 → ℕ ⊆ (ℤ‘0))
3231, 2sseldd 3762 . . . . . . . . . . . 12 (𝜑𝑀 ∈ (ℤ‘0))
33 eluzfz1 12555 . . . . . . . . . . . 12 (𝑀 ∈ (ℤ‘0) → 0 ∈ (0...𝑀))
3432, 33syl 17 . . . . . . . . . . 11 (𝜑 → 0 ∈ (0...𝑀))
3518, 34ffvelrnd 6550 . . . . . . . . . . . 12 (𝜑 → (𝑉‘0) ∈ ℝ)
3635, 13resubcld 10712 . . . . . . . . . . 11 (𝜑 → ((𝑉‘0) − 𝑋) ∈ ℝ)
3724, 27, 34, 36fvmptd 6477 . . . . . . . . . 10 (𝜑 → (𝑄‘0) = ((𝑉‘0) − 𝑋))
387fourierdlem2 40963 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ → (𝑉 ∈ (𝑃𝑀) ↔ (𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))))
392, 38syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑉 ∈ (𝑃𝑀) ↔ (𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))))
408, 39mpbid 223 . . . . . . . . . . . . . 14 (𝜑 → (𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1)))))
4140simprd 489 . . . . . . . . . . . . 13 (𝜑 → (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))
4241simpld 488 . . . . . . . . . . . 12 (𝜑 → ((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)))
4342simpld 488 . . . . . . . . . . 11 (𝜑 → (𝑉‘0) = (-π + 𝑋))
4443oveq1d 6857 . . . . . . . . . 10 (𝜑 → ((𝑉‘0) − 𝑋) = ((-π + 𝑋) − 𝑋))
4512recnd 10322 . . . . . . . . . . 11 (𝜑 → -π ∈ ℂ)
4613recnd 10322 . . . . . . . . . . 11 (𝜑𝑋 ∈ ℂ)
4745, 46pncand 10647 . . . . . . . . . 10 (𝜑 → ((-π + 𝑋) − 𝑋) = -π)
4837, 44, 473eqtrd 2803 . . . . . . . . 9 (𝜑 → (𝑄‘0) = -π)
4912rexrd 10343 . . . . . . . . . 10 (𝜑 → -π ∈ ℝ*)
5015rexrd 10343 . . . . . . . . . 10 (𝜑 → π ∈ ℝ*)
51 fourierdlem50.ab . . . . . . . . . . 11 (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
523leidd 10848 . . . . . . . . . . . 12 (𝜑𝐴𝐴)
533, 4, 3, 52, 6eliccd 40368 . . . . . . . . . . 11 (𝜑𝐴 ∈ (𝐴[,]𝐵))
5451, 53sseldd 3762 . . . . . . . . . 10 (𝜑𝐴 ∈ (-π[,]π))
55 iccgelb 12432 . . . . . . . . . 10 ((-π ∈ ℝ* ∧ π ∈ ℝ*𝐴 ∈ (-π[,]π)) → -π ≤ 𝐴)
5649, 50, 54, 55syl3anc 1490 . . . . . . . . 9 (𝜑 → -π ≤ 𝐴)
5748, 56eqbrtrd 4831 . . . . . . . 8 (𝜑 → (𝑄‘0) ≤ 𝐴)
584leidd 10848 . . . . . . . . . . . 12 (𝜑𝐵𝐵)
593, 4, 4, 6, 58eliccd 40368 . . . . . . . . . . 11 (𝜑𝐵 ∈ (𝐴[,]𝐵))
6051, 59sseldd 3762 . . . . . . . . . 10 (𝜑𝐵 ∈ (-π[,]π))
61 iccleub 12431 . . . . . . . . . 10 ((-π ∈ ℝ* ∧ π ∈ ℝ*𝐵 ∈ (-π[,]π)) → 𝐵 ≤ π)
6249, 50, 60, 61syl3anc 1490 . . . . . . . . 9 (𝜑𝐵 ≤ π)
63 fveq2 6375 . . . . . . . . . . . . 13 (𝑖 = 𝑀 → (𝑉𝑖) = (𝑉𝑀))
6463oveq1d 6857 . . . . . . . . . . . 12 (𝑖 = 𝑀 → ((𝑉𝑖) − 𝑋) = ((𝑉𝑀) − 𝑋))
6564adantl 473 . . . . . . . . . . 11 ((𝜑𝑖 = 𝑀) → ((𝑉𝑖) − 𝑋) = ((𝑉𝑀) − 𝑋))
66 eluzfz2 12556 . . . . . . . . . . . 12 (𝑀 ∈ (ℤ‘0) → 𝑀 ∈ (0...𝑀))
6732, 66syl 17 . . . . . . . . . . 11 (𝜑𝑀 ∈ (0...𝑀))
6818, 67ffvelrnd 6550 . . . . . . . . . . . 12 (𝜑 → (𝑉𝑀) ∈ ℝ)
6968, 13resubcld 10712 . . . . . . . . . . 11 (𝜑 → ((𝑉𝑀) − 𝑋) ∈ ℝ)
7024, 65, 67, 69fvmptd 6477 . . . . . . . . . 10 (𝜑 → (𝑄𝑀) = ((𝑉𝑀) − 𝑋))
7142simprd 489 . . . . . . . . . . 11 (𝜑 → (𝑉𝑀) = (π + 𝑋))
7271oveq1d 6857 . . . . . . . . . 10 (𝜑 → ((𝑉𝑀) − 𝑋) = ((π + 𝑋) − 𝑋))
7315recnd 10322 . . . . . . . . . . 11 (𝜑 → π ∈ ℂ)
7473, 46pncand 10647 . . . . . . . . . 10 (𝜑 → ((π + 𝑋) − 𝑋) = π)
7570, 72, 743eqtrrd 2804 . . . . . . . . 9 (𝜑 → π = (𝑄𝑀))
7662, 75breqtrd 4835 . . . . . . . 8 (𝜑𝐵 ≤ (𝑄𝑀))
77 fourierdlem50.j . . . . . . . 8 (𝜑𝐽 ∈ (0..^𝑁))
78 fourierdlem50.t . . . . . . . 8 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))
79 prfi 8442 . . . . . . . . . . . 12 {𝐴, 𝐵} ∈ Fin
8079a1i 11 . . . . . . . . . . 11 (𝜑 → {𝐴, 𝐵} ∈ Fin)
81 fzfid 12980 . . . . . . . . . . . . 13 (𝜑 → (0...𝑀) ∈ Fin)
8222rnmptfi 39998 . . . . . . . . . . . . 13 ((0...𝑀) ∈ Fin → ran 𝑄 ∈ Fin)
8381, 82syl 17 . . . . . . . . . . . 12 (𝜑 → ran 𝑄 ∈ Fin)
84 infi 8391 . . . . . . . . . . . 12 (ran 𝑄 ∈ Fin → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
8583, 84syl 17 . . . . . . . . . . 11 (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
86 unfi 8434 . . . . . . . . . . 11 (({𝐴, 𝐵} ∈ Fin ∧ (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin) → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
8780, 85, 86syl2anc 579 . . . . . . . . . 10 (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
8878, 87syl5eqel 2848 . . . . . . . . 9 (𝜑𝑇 ∈ Fin)
893, 4jca 507 . . . . . . . . . . . 12 (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
90 prssg 4504 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
913, 4, 90syl2anc 579 . . . . . . . . . . . 12 (𝜑 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
9289, 91mpbid 223 . . . . . . . . . . 11 (𝜑 → {𝐴, 𝐵} ⊆ ℝ)
93 inss2 3993 . . . . . . . . . . . . 13 (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴(,)𝐵)
94 ioossre 12437 . . . . . . . . . . . . 13 (𝐴(,)𝐵) ⊆ ℝ
9593, 94sstri 3770 . . . . . . . . . . . 12 (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ
9695a1i 11 . . . . . . . . . . 11 (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ)
9792, 96unssd 3951 . . . . . . . . . 10 (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ ℝ)
9878, 97syl5eqss 3809 . . . . . . . . 9 (𝜑𝑇 ⊆ ℝ)
99 fourierdlem50.s . . . . . . . . 9 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇))
100 fourierdlem50.n . . . . . . . . 9 𝑁 = ((♯‘𝑇) − 1)
10188, 98, 99, 100fourierdlem36 40997 . . . . . . . 8 (𝜑𝑆 Isom < , < ((0...𝑁), 𝑇))
102 eqid 2765 . . . . . . . 8 sup({𝑥 ∈ (0..^𝑀) ∣ (𝑄𝑥) ≤ (𝑆𝐽)}, ℝ, < ) = sup({𝑥 ∈ (0..^𝑀) ∣ (𝑄𝑥) ≤ (𝑆𝐽)}, ℝ, < )
1032, 3, 4, 6, 23, 57, 76, 77, 78, 101, 102fourierdlem20 40981 . . . . . . 7 (𝜑 → ∃𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
104 fourierdlem50.ch . . . . . . . . . . . . 13 (𝜒 ↔ ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))))
105104biimpi 207 . . . . . . . . . . . . . . . . . 18 (𝜒 → ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))))
106 simp-4l 801 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝜑)
107105, 106syl 17 . . . . . . . . . . . . . . . . 17 (𝜒𝜑)
108 simplr 785 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑘 ∈ (0..^𝑀))
109105, 108syl 17 . . . . . . . . . . . . . . . . 17 (𝜒𝑘 ∈ (0..^𝑀))
110107, 109jca 507 . . . . . . . . . . . . . . . 16 (𝜒 → (𝜑𝑘 ∈ (0..^𝑀)))
111 simp-4r 803 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑖 ∈ (0..^𝑀))
112105, 111syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝑖 ∈ (0..^𝑀))
113 elfzofz 12693 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ (0..^𝑀) → 𝑘 ∈ (0...𝑀))
114113ad2antlr 718 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑘 ∈ (0...𝑀))
115105, 114syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜒𝑘 ∈ (0...𝑀))
116107, 18syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒𝑉:(0...𝑀)⟶ℝ)
117116, 115ffvelrnd 6550 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (𝑉𝑘) ∈ ℝ)
118107, 13syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜒𝑋 ∈ ℝ)
119117, 118resubcld 10712 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ((𝑉𝑘) − 𝑋) ∈ ℝ)
120 fveq2 6375 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 𝑘 → (𝑉𝑖) = (𝑉𝑘))
121120oveq1d 6857 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑘 → ((𝑉𝑖) − 𝑋) = ((𝑉𝑘) − 𝑋))
122121, 22fvmptg 6469 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ (0...𝑀) ∧ ((𝑉𝑘) − 𝑋) ∈ ℝ) → (𝑄𝑘) = ((𝑉𝑘) − 𝑋))
123115, 119, 122syl2anc 579 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑄𝑘) = ((𝑉𝑘) − 𝑋))
124123, 119eqeltrd 2844 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄𝑘) ∈ ℝ)
12523adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
126 fzofzp1 12773 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
127126adantl 473 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
128125, 127ffvelrnd 6550 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
129107, 112, 128syl2anc 579 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℝ)
130 isof1o 6765 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑆 Isom < , < ((0...𝑁), 𝑇) → 𝑆:(0...𝑁)–1-1-onto𝑇)
131101, 130syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑆:(0...𝑁)–1-1-onto𝑇)
132 f1of 6320 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑆:(0...𝑁)–1-1-onto𝑇𝑆:(0...𝑁)⟶𝑇)
133131, 132syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑆:(0...𝑁)⟶𝑇)
134 fzofzp1 12773 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
13577, 134syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
136133, 135ffvelrnd 6550 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ 𝑇)
13798, 136sseldd 3762 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
138107, 137syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
139 elfzofz 12693 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
14077, 139syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐽 ∈ (0...𝑁))
141133, 140ffvelrnd 6550 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑆𝐽) ∈ 𝑇)
14298, 141sseldd 3762 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑆𝐽) ∈ ℝ)
143107, 142syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑆𝐽) ∈ ℝ)
144105simprd 489 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
145124rexrd 10343 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → (𝑄𝑘) ∈ ℝ*)
14623adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
147 fzofzp1 12773 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 ∈ (0..^𝑀) → (𝑘 + 1) ∈ (0...𝑀))
148147adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0..^𝑀)) → (𝑘 + 1) ∈ (0...𝑀))
149146, 148ffvelrnd 6550 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ (0..^𝑀)) → (𝑄‘(𝑘 + 1)) ∈ ℝ)
150149rexrd 10343 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (0..^𝑀)) → (𝑄‘(𝑘 + 1)) ∈ ℝ*)
151110, 150syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → (𝑄‘(𝑘 + 1)) ∈ ℝ*)
152143rexrd 10343 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → (𝑆𝐽) ∈ ℝ*)
153138rexrd 10343 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → (𝑆‘(𝐽 + 1)) ∈ ℝ*)
154 elfzoelz 12678 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
155154zred 11729 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℝ)
156155ltp1d 11208 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐽 ∈ (0..^𝑁) → 𝐽 < (𝐽 + 1))
15777, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐽 < (𝐽 + 1))
158 isoeq5 6763 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) → (𝑆 Isom < , < ((0...𝑁), 𝑇) ↔ 𝑆 Isom < , < ((0...𝑁), ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))))))
15978, 158ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑆 Isom < , < ((0...𝑁), 𝑇) ↔ 𝑆 Isom < , < ((0...𝑁), ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))))
160101, 159sylib 209 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑆 Isom < , < ((0...𝑁), ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))))
161 isorel 6768 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑆 Isom < , < ((0...𝑁), ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))) ∧ (𝐽 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝐽 < (𝐽 + 1) ↔ (𝑆𝐽) < (𝑆‘(𝐽 + 1))))
162160, 140, 135, 161syl12anc 865 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐽 < (𝐽 + 1) ↔ (𝑆𝐽) < (𝑆‘(𝐽 + 1))))
163157, 162mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑆𝐽) < (𝑆‘(𝐽 + 1)))
164107, 163syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → (𝑆𝐽) < (𝑆‘(𝐽 + 1)))
165145, 151, 152, 153, 164ioossioobi 40382 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ ((𝑄𝑘) ≤ (𝑆𝐽) ∧ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑘 + 1)))))
166144, 165mpbid 223 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → ((𝑄𝑘) ≤ (𝑆𝐽) ∧ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑘 + 1))))
167166simpld 488 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑄𝑘) ≤ (𝑆𝐽))
168124, 143, 138, 167, 164lelttrd 10449 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑄𝑘) < (𝑆‘(𝐽 + 1)))
169 elfzofz 12693 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
170169ad2antlr 718 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑖 ∈ (0...𝑀))
171170ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑖 ∈ (0...𝑀))
172105, 171syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒𝑖 ∈ (0...𝑀))
173107, 172, 21syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → ((𝑉𝑖) − 𝑋) ∈ ℝ)
17422fvmpt2 6480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ (0...𝑀) ∧ ((𝑉𝑖) − 𝑋) ∈ ℝ) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
175172, 173, 174syl2anc 579 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
176175, 173eqeltrd 2844 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (𝑄𝑖) ∈ ℝ)
177 simpllr 793 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
178105, 177syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
179176, 129, 143, 138, 164, 178fourierdlem10 40971 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ((𝑄𝑖) ≤ (𝑆𝐽) ∧ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑖 + 1))))
180179simprd 489 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑖 + 1)))
181124, 138, 129, 168, 180ltletrd 10451 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄𝑘) < (𝑄‘(𝑖 + 1)))
182124, 129, 118, 181ltadd2dd 10450 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + (𝑄𝑘)) < (𝑋 + (𝑄‘(𝑖 + 1))))
183123oveq2d 6858 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + (𝑄𝑘)) = (𝑋 + ((𝑉𝑘) − 𝑋)))
184107, 46syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒𝑋 ∈ ℂ)
185117recnd 10322 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑉𝑘) ∈ ℂ)
186184, 185pncan3d 10649 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + ((𝑉𝑘) − 𝑋)) = (𝑉𝑘))
187183, 186eqtr2d 2800 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑉𝑘) = (𝑋 + (𝑄𝑘)))
188112, 126syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑖 + 1) ∈ (0...𝑀))
18918adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
190189, 127ffvelrnd 6550 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
191107, 112, 190syl2anc 579 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℝ)
192191, 118resubcld 10712 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
193188, 192jca 507 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ((𝑖 + 1) ∈ (0...𝑀) ∧ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ))
194 eleq1 2832 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑖 + 1) → (𝑘 ∈ (0...𝑀) ↔ (𝑖 + 1) ∈ (0...𝑀)))
195 fveq2 6375 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = (𝑖 + 1) → (𝑉𝑘) = (𝑉‘(𝑖 + 1)))
196195oveq1d 6857 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = (𝑖 + 1) → ((𝑉𝑘) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
197196eleq1d 2829 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑖 + 1) → (((𝑉𝑘) − 𝑋) ∈ ℝ ↔ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ))
198194, 197anbi12d 624 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = (𝑖 + 1) → ((𝑘 ∈ (0...𝑀) ∧ ((𝑉𝑘) − 𝑋) ∈ ℝ) ↔ ((𝑖 + 1) ∈ (0...𝑀) ∧ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)))
199 fveq2 6375 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑖 + 1) → (𝑄𝑘) = (𝑄‘(𝑖 + 1)))
200199, 196eqeq12d 2780 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = (𝑖 + 1) → ((𝑄𝑘) = ((𝑉𝑘) − 𝑋) ↔ (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋)))
201198, 200imbi12d 335 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = (𝑖 + 1) → (((𝑘 ∈ (0...𝑀) ∧ ((𝑉𝑘) − 𝑋) ∈ ℝ) → (𝑄𝑘) = ((𝑉𝑘) − 𝑋)) ↔ (((𝑖 + 1) ∈ (0...𝑀) ∧ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))))
202201, 122vtoclg 3418 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 + 1) ∈ (0...𝑀) → (((𝑖 + 1) ∈ (0...𝑀) ∧ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋)))
203188, 193, 202sylc 65 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
204203oveq2d 6858 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)))
205191recnd 10322 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℂ)
206184, 205pncan3d 10649 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)) = (𝑉‘(𝑖 + 1)))
207204, 206eqtr2d 2800 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑉‘(𝑖 + 1)) = (𝑋 + (𝑄‘(𝑖 + 1))))
208182, 187, 2073brtr4d 4841 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑉𝑘) < (𝑉‘(𝑖 + 1)))
209 eleq1w 2827 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑖 → (𝑙 ∈ (0..^𝑀) ↔ 𝑖 ∈ (0..^𝑀)))
210209anbi2d 622 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑖 → (((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ↔ ((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (0..^𝑀))))
211 oveq1 6849 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑖 → (𝑙 + 1) = (𝑖 + 1))
212211fveq2d 6379 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑖 → (𝑉‘(𝑙 + 1)) = (𝑉‘(𝑖 + 1)))
213212breq2d 4821 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑖 → ((𝑉𝑘) < (𝑉‘(𝑙 + 1)) ↔ (𝑉𝑘) < (𝑉‘(𝑖 + 1))))
214210, 213anbi12d 624 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑖 → ((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑙 + 1))) ↔ (((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑖 + 1)))))
215 fveq2 6375 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑖 → (𝑉𝑙) = (𝑉𝑖))
216215breq2d 4821 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑖 → ((𝑉𝑘) ≤ (𝑉𝑙) ↔ (𝑉𝑘) ≤ (𝑉𝑖)))
217214, 216imbi12d 335 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑖 → (((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑙 + 1))) → (𝑉𝑘) ≤ (𝑉𝑙)) ↔ ((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑖 + 1))) → (𝑉𝑘) ≤ (𝑉𝑖))))
218 eleq1w 2827 . . . . . . . . . . . . . . . . . . . . . 22 ( = 𝑘 → ( ∈ (0..^𝑀) ↔ 𝑘 ∈ (0..^𝑀)))
219218anbi2d 622 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝑘 → ((𝜑 ∈ (0..^𝑀)) ↔ (𝜑𝑘 ∈ (0..^𝑀))))
220219anbi1d 623 . . . . . . . . . . . . . . . . . . . 20 ( = 𝑘 → (((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ↔ ((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀))))
221 fveq2 6375 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝑘 → (𝑉) = (𝑉𝑘))
222221breq1d 4819 . . . . . . . . . . . . . . . . . . . 20 ( = 𝑘 → ((𝑉) < (𝑉‘(𝑙 + 1)) ↔ (𝑉𝑘) < (𝑉‘(𝑙 + 1))))
223220, 222anbi12d 624 . . . . . . . . . . . . . . . . . . 19 ( = 𝑘 → ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ↔ (((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑙 + 1)))))
224221breq1d 4819 . . . . . . . . . . . . . . . . . . 19 ( = 𝑘 → ((𝑉) ≤ (𝑉𝑙) ↔ (𝑉𝑘) ≤ (𝑉𝑙)))
225223, 224imbi12d 335 . . . . . . . . . . . . . . . . . 18 ( = 𝑘 → (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → (𝑉) ≤ (𝑉𝑙)) ↔ ((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑙 + 1))) → (𝑉𝑘) ≤ (𝑉𝑙))))
226 elfzoelz 12678 . . . . . . . . . . . . . . . . . . . . 21 ( ∈ (0..^𝑀) → ∈ ℤ)
227226ad3antlr 722 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → ∈ ℤ)
228 elfzoelz 12678 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 ∈ (0..^𝑀) → 𝑙 ∈ ℤ)
229228ad2antlr 718 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → 𝑙 ∈ ℤ)
230 simplr 785 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ ¬ < (𝑙 + 1)) → (𝑉) < (𝑉‘(𝑙 + 1)))
23118adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑙 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
232 fzofzp1 12773 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (0..^𝑀) → (𝑙 + 1) ∈ (0...𝑀))
233232adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑙 ∈ (0..^𝑀)) → (𝑙 + 1) ∈ (0...𝑀))
234231, 233ffvelrnd 6550 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑙 ∈ (0..^𝑀)) → (𝑉‘(𝑙 + 1)) ∈ ℝ)
235234adantlr 706 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) → (𝑉‘(𝑙 + 1)) ∈ ℝ)
236235adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → (𝑉‘(𝑙 + 1)) ∈ ℝ)
23718adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
238 elfzofz 12693 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ( ∈ (0..^𝑀) → ∈ (0...𝑀))
239238adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∈ (0..^𝑀)) → ∈ (0...𝑀))
240237, 239ffvelrnd 6550 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∈ (0..^𝑀)) → (𝑉) ∈ ℝ)
241240ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → (𝑉) ∈ ℝ)
242228zred 11729 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (0..^𝑀) → 𝑙 ∈ ℝ)
243 peano2re 10463 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ ℝ → (𝑙 + 1) ∈ ℝ)
244242, 243syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑙 ∈ (0..^𝑀) → (𝑙 + 1) ∈ ℝ)
245244ad2antlr 718 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → (𝑙 + 1) ∈ ℝ)
246226zred 11729 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ( ∈ (0..^𝑀) → ∈ ℝ)
247246ad3antlr 722 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → ∈ ℝ)
248 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → ¬ < (𝑙 + 1))
249245, 247, 248nltled 10441 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → (𝑙 + 1) ≤ )
250228peano2zd 11732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (0..^𝑀) → (𝑙 + 1) ∈ ℤ)
251250ad2antlr 718 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → (𝑙 + 1) ∈ ℤ)
252226ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → ∈ ℤ)
253 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → (𝑙 + 1) ≤ )
254 eluz2 11892 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ( ∈ (ℤ‘(𝑙 + 1)) ↔ ((𝑙 + 1) ∈ ℤ ∧ ∈ ℤ ∧ (𝑙 + 1) ≤ ))
255251, 252, 253, 254syl3anbrc 1443 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → ∈ (ℤ‘(𝑙 + 1)))
256255adantlll 709 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → ∈ (ℤ‘(𝑙 + 1)))
257 simplll 791 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝜑)
258 0zd 11636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 ∈ ℤ)
259 elfzoel2 12677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ( ∈ (0..^𝑀) → 𝑀 ∈ ℤ)
260259ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑀 ∈ ℤ)
261 elfzelz 12549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ ((𝑙 + 1)...) → 𝑖 ∈ ℤ)
262261adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 ∈ ℤ)
263258, 260, 2623jca 1158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ))
264 0red 10297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 ∈ ℝ)
265261zred 11729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑖 ∈ ((𝑙 + 1)...) → 𝑖 ∈ ℝ)
266265adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 ∈ ℝ)
267242adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑙 ∈ ℝ)
268 elfzole1 12686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑙 ∈ (0..^𝑀) → 0 ≤ 𝑙)
269268adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 ≤ 𝑙)
270267, 243syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → (𝑙 + 1) ∈ ℝ)
271267ltp1d 11208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑙 < (𝑙 + 1))
272 elfzle1 12551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑖 ∈ ((𝑙 + 1)...) → (𝑙 + 1) ≤ 𝑖)
273272adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → (𝑙 + 1) ≤ 𝑖)
274267, 270, 266, 271, 273ltletrd 10451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑙 < 𝑖)
275264, 267, 266, 269, 274lelttrd 10449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 < 𝑖)
276264, 266, 275ltled 10439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 ≤ 𝑖)
277276adantll 705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 ≤ 𝑖)
278265adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 ∈ ℝ)
279259zred 11729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( ∈ (0..^𝑀) → 𝑀 ∈ ℝ)
280279adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑀 ∈ ℝ)
281246adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → ∈ ℝ)
282 elfzle2 12552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑖 ∈ ((𝑙 + 1)...) → 𝑖)
283282adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖)
284 elfzolt2 12687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ( ∈ (0..^𝑀) → < 𝑀)
285284adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → < 𝑀)
286278, 281, 280, 283, 285lelttrd 10449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 < 𝑀)
287278, 280, 286ltled 10439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖𝑀)
288287adantlr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖𝑀)
289263, 277, 288jca32 511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (0 ≤ 𝑖𝑖𝑀)))
290 elfz2 12540 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (0 ≤ 𝑖𝑖𝑀)))
291289, 290sylibr 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 ∈ (0...𝑀))
292291adantlll 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 ∈ (0...𝑀))
293257, 292, 19syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → (𝑉𝑖) ∈ ℝ)
294293adantlr 706 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → (𝑉𝑖) ∈ ℝ)
295 simplll 791 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝜑)
296 0zd 11636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 0 ∈ ℤ)
297 elfzelz 12549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 ∈ ((𝑙 + 1)...( − 1)) → 𝑖 ∈ ℤ)
298297adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ ℤ)
299 0red 10297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 0 ∈ ℝ)
300298zred 11729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ ℝ)
301242adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑙 ∈ ℝ)
302268adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 0 ≤ 𝑙)
303301, 243syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → (𝑙 + 1) ∈ ℝ)
304301ltp1d 11208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑙 < (𝑙 + 1))
305 elfzle1 12551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑖 ∈ ((𝑙 + 1)...( − 1)) → (𝑙 + 1) ≤ 𝑖)
306305adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → (𝑙 + 1) ≤ 𝑖)
307301, 303, 300, 304, 306ltletrd 10451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑙 < 𝑖)
308299, 301, 300, 302, 307lelttrd 10449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 0 < 𝑖)
309299, 300, 308ltled 10439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 0 ≤ 𝑖)
310 eluz2 11892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (ℤ‘0) ↔ (0 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 0 ≤ 𝑖))
311296, 298, 309, 310syl3anbrc 1443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ (ℤ‘0))
312311adantll 705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ (ℤ‘0))
313 elfzoel2 12677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (0..^𝑀) → 𝑀 ∈ ℤ)
314313ad2antlr 718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑀 ∈ ℤ)
315297zred 11729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ ((𝑙 + 1)...( − 1)) → 𝑖 ∈ ℝ)
316315adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ ℝ)
317 peano2rem 10602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( ∈ ℝ → ( − 1) ∈ ℝ)
318246, 317syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ( ∈ (0..^𝑀) → ( − 1) ∈ ℝ)
319318adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → ( − 1) ∈ ℝ)
320279adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑀 ∈ ℝ)
321 elfzle2 12552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ ((𝑙 + 1)...( − 1)) → 𝑖 ≤ ( − 1))
322321adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ≤ ( − 1))
323246ltm1d 11210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( ∈ (0..^𝑀) → ( − 1) < )
324318, 246, 279, 323, 284lttrd 10452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ( ∈ (0..^𝑀) → ( − 1) < 𝑀)
325324adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → ( − 1) < 𝑀)
326316, 319, 320, 322, 325lelttrd 10449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 < 𝑀)
327326adantll 705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 < 𝑀)
328327adantlr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 < 𝑀)
329 elfzo2 12681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ (0..^𝑀) ↔ (𝑖 ∈ (ℤ‘0) ∧ 𝑀 ∈ ℤ ∧ 𝑖 < 𝑀))
330312, 314, 328, 329syl3anbrc 1443 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ (0..^𝑀))
331169, 19sylan2 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ∈ ℝ)
33241simprd 489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1)))
333332r19.21bi 3079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) < (𝑉‘(𝑖 + 1)))
334331, 190, 333ltled 10439 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ≤ (𝑉‘(𝑖 + 1)))
335295, 330, 334syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → (𝑉𝑖) ≤ (𝑉‘(𝑖 + 1)))
336335adantlr 706 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → (𝑉𝑖) ≤ (𝑉‘(𝑖 + 1)))
337256, 294, 336monoord 13038 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → (𝑉‘(𝑙 + 1)) ≤ (𝑉))
338249, 337syldan 585 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → (𝑉‘(𝑙 + 1)) ≤ (𝑉))
339236, 241, 338lensymd 10442 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → ¬ (𝑉) < (𝑉‘(𝑙 + 1)))
340339adantlr 706 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ ¬ < (𝑙 + 1)) → ¬ (𝑉) < (𝑉‘(𝑙 + 1)))
341230, 340condan 852 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → < (𝑙 + 1))
342 zleltp1 11675 . . . . . . . . . . . . . . . . . . . . . 22 (( ∈ ℤ ∧ 𝑙 ∈ ℤ) → (𝑙 < (𝑙 + 1)))
343227, 229, 342syl2anc 579 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → (𝑙 < (𝑙 + 1)))
344341, 343mpbird 248 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → 𝑙)
345 eluz2 11892 . . . . . . . . . . . . . . . . . . . 20 (𝑙 ∈ (ℤ) ↔ ( ∈ ℤ ∧ 𝑙 ∈ ℤ ∧ 𝑙))
346227, 229, 344, 345syl3anbrc 1443 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → 𝑙 ∈ (ℤ))
34718ad3antrrr 721 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑉:(0...𝑀)⟶ℝ)
348 0zd 11636 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 0 ∈ ℤ)
349259ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑀 ∈ ℤ)
350 elfzelz 12549 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (...𝑙) → 𝑖 ∈ ℤ)
351350adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 ∈ ℤ)
352348, 349, 3513jca 1158 . . . . . . . . . . . . . . . . . . . . . . . 24 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ))
353 0red 10297 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 0 ∈ ℝ)
354246adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → ∈ ℝ)
355350zred 11729 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (...𝑙) → 𝑖 ∈ ℝ)
356355adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 ∈ ℝ)
357 elfzole1 12686 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ( ∈ (0..^𝑀) → 0 ≤ )
358357adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 0 ≤ )
359 elfzle1 12551 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (...𝑙) → 𝑖)
360359adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖)
361353, 354, 356, 358, 360letrd 10448 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 0 ≤ 𝑖)
362361adantlr 706 . . . . . . . . . . . . . . . . . . . . . . . 24 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 0 ≤ 𝑖)
363355adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 ∈ ℝ)
364313zred 11729 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑙 ∈ (0..^𝑀) → 𝑀 ∈ ℝ)
365364adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑀 ∈ ℝ)
366242adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑙 ∈ ℝ)
367 elfzle2 12552 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ (...𝑙) → 𝑖𝑙)
368367adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖𝑙)
369 elfzolt2 12687 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (0..^𝑀) → 𝑙 < 𝑀)
370369adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑙 < 𝑀)
371363, 366, 365, 368, 370lelttrd 10449 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 < 𝑀)
372363, 365, 371ltled 10439 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖𝑀)
373372adantll 705 . . . . . . . . . . . . . . . . . . . . . . . 24 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑖𝑀)
374352, 362, 373jca32 511 . . . . . . . . . . . . . . . . . . . . . . 23 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (0 ≤ 𝑖𝑖𝑀)))
375374, 290sylibr 225 . . . . . . . . . . . . . . . . . . . . . 22 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 ∈ (0...𝑀))
376375adantlll 709 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 ∈ (0...𝑀))
377347, 376ffvelrnd 6550 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → (𝑉𝑖) ∈ ℝ)
378377adantlr 706 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...𝑙)) → (𝑉𝑖) ∈ ℝ)
379 simp-4l 801 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝜑)
380 0zd 11636 . . . . . . . . . . . . . . . . . . . . . . . 24 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 0 ∈ ℤ)
381 elfzelz 12549 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ (...(𝑙 − 1)) → 𝑖 ∈ ℤ)
382381adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ ℤ)
383 0red 10297 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 0 ∈ ℝ)
384246adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → ∈ ℝ)
385382zred 11729 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ ℝ)
386357adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 0 ≤ )
387 elfzle1 12551 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (...(𝑙 − 1)) → 𝑖)
388387adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖)
389383, 384, 385, 386, 388letrd 10448 . . . . . . . . . . . . . . . . . . . . . . . 24 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 0 ≤ 𝑖)
390380, 382, 389, 310syl3anbrc 1443 . . . . . . . . . . . . . . . . . . . . . . 23 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ (ℤ‘0))
391390adantll 705 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ (ℤ‘0))
392391ad4ant14 759 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ (ℤ‘0))
393313ad3antlr 722 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑀 ∈ ℤ)
394381zred 11729 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ (...(𝑙 − 1)) → 𝑖 ∈ ℝ)
395394adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ ℝ)
396242adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑙 ∈ ℝ)
397364adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑀 ∈ ℝ)
398 elfzle2 12552 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (...(𝑙 − 1)) → 𝑖 ≤ (𝑙 − 1))
399398adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ≤ (𝑙 − 1))
400 zltlem1 11677 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑖 ∈ ℤ ∧ 𝑙 ∈ ℤ) → (𝑖 < 𝑙𝑖 ≤ (𝑙 − 1)))
401381, 228, 400syl2anr 590 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → (𝑖 < 𝑙𝑖 ≤ (𝑙 − 1)))
402399, 401mpbird 248 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 < 𝑙)
403369adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑙 < 𝑀)
404395, 396, 397, 402, 403lttrd 10452 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 < 𝑀)
405404adantll 705 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 < 𝑀)
406405adantlr 706 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 < 𝑀)
407392, 393, 406, 329syl3anbrc 1443 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ (0..^𝑀))
408379, 407, 334syl2anc 579 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → (𝑉𝑖) ≤ (𝑉‘(𝑖 + 1)))
409346, 378, 408monoord 13038 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → (𝑉) ≤ (𝑉𝑙))
410225, 409chvarv 2369 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑙 + 1))) → (𝑉𝑘) ≤ (𝑉𝑙))
411217, 410chvarv 2369 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑖 + 1))) → (𝑉𝑘) ≤ (𝑉𝑖))
412110, 112, 208, 411syl21anc 866 . . . . . . . . . . . . . . 15 (𝜒 → (𝑉𝑘) ≤ (𝑉𝑖))
413107, 112jca 507 . . . . . . . . . . . . . . . 16 (𝜒 → (𝜑𝑖 ∈ (0..^𝑀)))
414110, 149syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄‘(𝑘 + 1)) ∈ ℝ)
415179simpld 488 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑄𝑖) ≤ (𝑆𝐽))
416176, 143, 138, 415, 164lelttrd 10449 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑄𝑖) < (𝑆‘(𝐽 + 1)))
417166simprd 489 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑘 + 1)))
418176, 138, 414, 416, 417ltletrd 10451 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄𝑖) < (𝑄‘(𝑘 + 1)))
419176, 414, 118, 418ltadd2dd 10450 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + (𝑄𝑖)) < (𝑋 + (𝑄‘(𝑘 + 1))))
420175oveq2d 6858 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + (𝑄𝑖)) = (𝑋 + ((𝑉𝑖) − 𝑋)))
421107, 172, 19syl2anc 579 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑉𝑖) ∈ ℝ)
422421recnd 10322 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑉𝑖) ∈ ℂ)
423184, 422pncan3d 10649 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + ((𝑉𝑖) − 𝑋)) = (𝑉𝑖))
424420, 423eqtr2d 2800 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑉𝑖) = (𝑋 + (𝑄𝑖)))
42522a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0..^𝑀)) → 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋)))
426 fveq2 6375 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = (𝑘 + 1) → (𝑉𝑖) = (𝑉‘(𝑘 + 1)))
427426oveq1d 6857 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = (𝑘 + 1) → ((𝑉𝑖) − 𝑋) = ((𝑉‘(𝑘 + 1)) − 𝑋))
428427adantl 473 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑖 = (𝑘 + 1)) → ((𝑉𝑖) − 𝑋) = ((𝑉‘(𝑘 + 1)) − 𝑋))
42918adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
430429, 148ffvelrnd 6550 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (0..^𝑀)) → (𝑉‘(𝑘 + 1)) ∈ ℝ)
43113adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
432430, 431resubcld 10712 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0..^𝑀)) → ((𝑉‘(𝑘 + 1)) − 𝑋) ∈ ℝ)
433425, 428, 148, 432fvmptd 6477 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0..^𝑀)) → (𝑄‘(𝑘 + 1)) = ((𝑉‘(𝑘 + 1)) − 𝑋))
434107, 109, 433syl2anc 579 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑄‘(𝑘 + 1)) = ((𝑉‘(𝑘 + 1)) − 𝑋))
435434oveq2d 6858 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + (𝑄‘(𝑘 + 1))) = (𝑋 + ((𝑉‘(𝑘 + 1)) − 𝑋)))
436110, 430syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑉‘(𝑘 + 1)) ∈ ℝ)
437436recnd 10322 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑉‘(𝑘 + 1)) ∈ ℂ)
438184, 437pncan3d 10649 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + ((𝑉‘(𝑘 + 1)) − 𝑋)) = (𝑉‘(𝑘 + 1)))
439435, 438eqtr2d 2800 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑉‘(𝑘 + 1)) = (𝑋 + (𝑄‘(𝑘 + 1))))
440419, 424, 4393brtr4d 4841 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑉𝑖) < (𝑉‘(𝑘 + 1)))
441 eleq1w 2827 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑘 → (𝑙 ∈ (0..^𝑀) ↔ 𝑘 ∈ (0..^𝑀)))
442441anbi2d 622 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑘 → (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ↔ ((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑘 ∈ (0..^𝑀))))
443 oveq1 6849 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑘 → (𝑙 + 1) = (𝑘 + 1))
444443fveq2d 6379 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑘 → (𝑉‘(𝑙 + 1)) = (𝑉‘(𝑘 + 1)))
445444breq2d 4821 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑘 → ((𝑉𝑖) < (𝑉‘(𝑙 + 1)) ↔ (𝑉𝑖) < (𝑉‘(𝑘 + 1))))
446442, 445anbi12d 624 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑘 → ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑙 + 1))) ↔ (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑘 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑘 + 1)))))
447 fveq2 6375 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑘 → (𝑉𝑙) = (𝑉𝑘))
448447breq2d 4821 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑘 → ((𝑉𝑖) ≤ (𝑉𝑙) ↔ (𝑉𝑖) ≤ (𝑉𝑘)))
449446, 448imbi12d 335 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑘 → (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑙 + 1))) → (𝑉𝑖) ≤ (𝑉𝑙)) ↔ ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑘 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑘 + 1))) → (𝑉𝑖) ≤ (𝑉𝑘))))
450 eleq1w 2827 . . . . . . . . . . . . . . . . . . . . . 22 ( = 𝑖 → ( ∈ (0..^𝑀) ↔ 𝑖 ∈ (0..^𝑀)))
451450anbi2d 622 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝑖 → ((𝜑 ∈ (0..^𝑀)) ↔ (𝜑𝑖 ∈ (0..^𝑀))))
452451anbi1d 623 . . . . . . . . . . . . . . . . . . . 20 ( = 𝑖 → (((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ↔ ((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀))))
453 fveq2 6375 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝑖 → (𝑉) = (𝑉𝑖))
454453breq1d 4819 . . . . . . . . . . . . . . . . . . . 20 ( = 𝑖 → ((𝑉) < (𝑉‘(𝑙 + 1)) ↔ (𝑉𝑖) < (𝑉‘(𝑙 + 1))))
455452, 454anbi12d 624 . . . . . . . . . . . . . . . . . . 19 ( = 𝑖 → ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ↔ (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑙 + 1)))))
456453breq1d 4819 . . . . . . . . . . . . . . . . . . 19 ( = 𝑖 → ((𝑉) ≤ (𝑉𝑙) ↔ (𝑉𝑖) ≤ (𝑉𝑙)))
457455, 456imbi12d 335 . . . . . . . . . . . . . . . . . 18 ( = 𝑖 → (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → (𝑉) ≤ (𝑉𝑙)) ↔ ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑙 + 1))) → (𝑉𝑖) ≤ (𝑉𝑙))))
458457, 409chvarv 2369 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑙 + 1))) → (𝑉𝑖) ≤ (𝑉𝑙))
459449, 458chvarv 2369 . . . . . . . . . . . . . . . 16 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑘 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑘 + 1))) → (𝑉𝑖) ≤ (𝑉𝑘))
460413, 109, 440, 459syl21anc 866 . . . . . . . . . . . . . . 15 (𝜒 → (𝑉𝑖) ≤ (𝑉𝑘))
461117, 421letri3d 10433 . . . . . . . . . . . . . . 15 (𝜒 → ((𝑉𝑘) = (𝑉𝑖) ↔ ((𝑉𝑘) ≤ (𝑉𝑖) ∧ (𝑉𝑖) ≤ (𝑉𝑘))))
462412, 460, 461mpbir2and 704 . . . . . . . . . . . . . 14 (𝜒 → (𝑉𝑘) = (𝑉𝑖))
4637, 2, 8fourierdlem34 40995 . . . . . . . . . . . . . . . 16 (𝜑𝑉:(0...𝑀)–1-1→ℝ)
464107, 463syl 17 . . . . . . . . . . . . . . 15 (𝜒𝑉:(0...𝑀)–1-1→ℝ)
465 f1fveq 6711 . . . . . . . . . . . . . . 15 ((𝑉:(0...𝑀)–1-1→ℝ ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑀))) → ((𝑉𝑘) = (𝑉𝑖) ↔ 𝑘 = 𝑖))
466464, 115, 172, 465syl12anc 865 . . . . . . . . . . . . . 14 (𝜒 → ((𝑉𝑘) = (𝑉𝑖) ↔ 𝑘 = 𝑖))
467462, 466mpbid 223 . . . . . . . . . . . . 13 (𝜒𝑘 = 𝑖)
468104, 467sylbir 226 . . . . . . . . . . . 12 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑘 = 𝑖)
469468ex 401 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) → 𝑘 = 𝑖))
470 simpl 474 . . . . . . . . . . . . . 14 ((((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑘 = 𝑖) → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
471 fveq2 6375 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑖 → (𝑄𝑘) = (𝑄𝑖))
472 oveq1 6849 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑖 → (𝑘 + 1) = (𝑖 + 1))
473472fveq2d 6379 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑖 → (𝑄‘(𝑘 + 1)) = (𝑄‘(𝑖 + 1)))
474471, 473oveq12d 6860 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑖 → ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
475474eqcomd 2771 . . . . . . . . . . . . . . 15 (𝑘 = 𝑖 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
476475adantl 473 . . . . . . . . . . . . . 14 ((((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑘 = 𝑖) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
477470, 476sseqtrd 3801 . . . . . . . . . . . . 13 ((((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑘 = 𝑖) → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
478477ex 401 . . . . . . . . . . . 12 (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝑘 = 𝑖 → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))))
479478ad2antlr 718 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) → (𝑘 = 𝑖 → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))))
480469, 479impbid 203 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖))
481480ralrimiva 3113 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ∀𝑘 ∈ (0..^𝑀)(((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖))
482481ex 401 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ∀𝑘 ∈ (0..^𝑀)(((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖)))
483482reximdva 3163 . . . . . . 7 (𝜑 → (∃𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)∀𝑘 ∈ (0..^𝑀)(((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖)))
484103, 483mpd 15 . . . . . 6 (𝜑 → ∃𝑖 ∈ (0..^𝑀)∀𝑘 ∈ (0..^𝑀)(((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖))
485 reu6 3554 . . . . . 6 (∃!𝑘 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ ∃𝑖 ∈ (0..^𝑀)∀𝑘 ∈ (0..^𝑀)(((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖))
486484, 485sylibr 225 . . . . 5 (𝜑 → ∃!𝑘 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
487 fveq2 6375 . . . . . . . 8 (𝑖 = 𝑘 → (𝑄𝑖) = (𝑄𝑘))
488 oveq1 6849 . . . . . . . . 9 (𝑖 = 𝑘 → (𝑖 + 1) = (𝑘 + 1))
489488fveq2d 6379 . . . . . . . 8 (𝑖 = 𝑘 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑘 + 1)))
490487, 489oveq12d 6860 . . . . . . 7 (𝑖 = 𝑘 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
491490sseq2d 3793 . . . . . 6 (𝑖 = 𝑘 → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))))
492491cbvreuv 3321 . . . . 5 (∃!𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ ∃!𝑘 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
493486, 492sylibr 225 . . . 4 (𝜑 → ∃!𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
494 riotacl 6817 . . . 4 (∃!𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (0..^𝑀))
495493, 494syl 17 . . 3 (𝜑 → (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (0..^𝑀))
4961, 495syl5eqel 2848 . 2 (𝜑𝑈 ∈ (0..^𝑀))
4971eqcomi 2774 . . . 4 (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = 𝑈
498497a1i 11 . . 3 (𝜑 → (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = 𝑈)
499 fveq2 6375 . . . . . . 7 (𝑖 = 𝑈 → (𝑄𝑖) = (𝑄𝑈))
500 oveq1 6849 . . . . . . . 8 (𝑖 = 𝑈 → (𝑖 + 1) = (𝑈 + 1))
501500fveq2d 6379 . . . . . . 7 (𝑖 = 𝑈 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑈 + 1)))
502499, 501oveq12d 6860 . . . . . 6 (𝑖 = 𝑈 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1))))
503502sseq2d 3793 . . . . 5 (𝑖 = 𝑈 → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1)))))
504503riota2 6825 . . . 4 ((𝑈 ∈ (0..^𝑀) ∧ ∃!𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1))) ↔ (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = 𝑈))
505496, 493, 504syl2anc 579 . . 3 (𝜑 → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1))) ↔ (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = 𝑈))
506498, 505mpbird 248 . 2 (𝜑 → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1))))
507496, 506jca 507 1 (𝜑 → (𝑈 ∈ (0..^𝑀) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wral 3055  wrex 3056  ∃!wreu 3057  {crab 3059  cun 3730  cin 3731  wss 3732  {cpr 4336   class class class wbr 4809  cmpt 4888  ran crn 5278  cio 6029  wf 6064  1-1wf1 6065  1-1-ontowf1o 6067  cfv 6068   Isom wiso 6069  crio 6802  (class class class)co 6842  𝑚 cmap 8060  Fincfn 8160  supcsup 8553  cc 10187  cr 10188  0cc0 10189  1c1 10190   + caddc 10192  *cxr 10327   < clt 10328  cle 10329  cmin 10520  -cneg 10521  cn 11274  0cn0 11538  cz 11624  cuz 11886  (,)cioo 12377  [,]cicc 12380  ...cfz 12533  ..^cfzo 12673  chash 13321  πcpi 15079
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-inf2 8753  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267  ax-addf 10268  ax-mulf 10269
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-iin 4679  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-isom 6077  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-of 7095  df-om 7264  df-1st 7366  df-2nd 7367  df-supp 7498  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-oadd 7768  df-er 7947  df-map 8062  df-pm 8063  df-ixp 8114  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-fsupp 8483  df-fi 8524  df-sup 8555  df-inf 8556  df-oi 8622  df-card 9016  df-cda 9243  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-7 11340  df-8 11341  df-9 11342  df-n0 11539  df-z 11625  df-dec 11741  df-uz 11887  df-q 11990  df-rp 12029  df-xneg 12146  df-xadd 12147  df-xmul 12148  df-ioo 12381  df-ioc 12382  df-ico 12383  df-icc 12384  df-fz 12534  df-fzo 12674  df-fl 12801  df-seq 13009  df-exp 13068  df-fac 13265  df-bc 13294  df-hash 13322  df-shft 14092  df-cj 14124  df-re 14125  df-im 14126  df-sqrt 14260  df-abs 14261  df-limsup 14487  df-clim 14504  df-rlim 14505  df-sum 14702  df-ef 15080  df-sin 15082  df-cos 15083  df-pi 15085  df-struct 16132  df-ndx 16133  df-slot 16134  df-base 16136  df-sets 16137  df-ress 16138  df-plusg 16227  df-mulr 16228  df-starv 16229  df-sca 16230  df-vsca 16231  df-ip 16232  df-tset 16233  df-ple 16234  df-ds 16236  df-unif 16237  df-hom 16238  df-cco 16239  df-rest 16349  df-topn 16350  df-0g 16368  df-gsum 16369  df-topgen 16370  df-pt 16371  df-prds 16374  df-xrs 16428  df-qtop 16433  df-imas 16434  df-xps 16436  df-mre 16512  df-mrc 16513  df-acs 16515  df-mgm 17508  df-sgrp 17550  df-mnd 17561  df-submnd 17602  df-mulg 17808  df-cntz 18013  df-cmn 18461  df-psmet 20011  df-xmet 20012  df-met 20013  df-bl 20014  df-mopn 20015  df-fbas 20016  df-fg 20017  df-cnfld 20020  df-top 20978  df-topon 20995  df-topsp 21017  df-bases 21030  df-cld 21103  df-ntr 21104  df-cls 21105  df-nei 21182  df-lp 21220  df-perf 21221  df-cn 21311  df-cnp 21312  df-haus 21399  df-tx 21645  df-hmeo 21838  df-fil 21929  df-fm 22021  df-flim 22022  df-flf 22023  df-xms 22404  df-ms 22405  df-tms 22406  df-cncf 22960  df-limc 23921  df-dv 23922
This theorem is referenced by:  fourierdlem86  41046  fourierdlem103  41063  fourierdlem104  41064
  Copyright terms: Public domain W3C validator