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 40691
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 10223 . . . . . . . 8 (𝜑𝐴𝐵)
7 fourierdlem50.p . . . . . . . . . . . . 13 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
8 fourierdlem50.v . . . . . . . . . . . . 13 (𝜑𝑉 ∈ (𝑃𝑀))
97, 2, 8fourierdlem15 40657 . . . . . . . . . . . 12 (𝜑𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
10 pire 24255 . . . . . . . . . . . . . . . 16 π ∈ ℝ
1110renegcli 10380 . . . . . . . . . . . . . . 15 -π ∈ ℝ
1211a1i 11 . . . . . . . . . . . . . 14 (𝜑 → -π ∈ ℝ)
13 fourierdlem50.xre . . . . . . . . . . . . . 14 (𝜑𝑋 ∈ ℝ)
1412, 13readdcld 10107 . . . . . . . . . . . . 13 (𝜑 → (-π + 𝑋) ∈ ℝ)
1510a1i 11 . . . . . . . . . . . . . 14 (𝜑 → π ∈ ℝ)
1615, 13readdcld 10107 . . . . . . . . . . . . 13 (𝜑 → (π + 𝑋) ∈ ℝ)
1714, 16iccssred 40045 . . . . . . . . . . . 12 (𝜑 → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
189, 17fssd 6095 . . . . . . . . . . 11 (𝜑𝑉:(0...𝑀)⟶ℝ)
1918ffvelrnda 6399 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑉𝑖) ∈ ℝ)
2013adantr 480 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℝ)
2119, 20resubcld 10496 . . . . . . . . 9 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) − 𝑋) ∈ ℝ)
22 fourierdlem50.q . . . . . . . . 9 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋))
2321, 22fmptd 6425 . . . . . . . 8 (𝜑𝑄:(0...𝑀)⟶ℝ)
2422a1i 11 . . . . . . . . . . 11 (𝜑𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋)))
25 fveq2 6229 . . . . . . . . . . . . 13 (𝑖 = 0 → (𝑉𝑖) = (𝑉‘0))
2625oveq1d 6705 . . . . . . . . . . . 12 (𝑖 = 0 → ((𝑉𝑖) − 𝑋) = ((𝑉‘0) − 𝑋))
2726adantl 481 . . . . . . . . . . 11 ((𝜑𝑖 = 0) → ((𝑉𝑖) − 𝑋) = ((𝑉‘0) − 𝑋))
28 nnssnn0 11333 . . . . . . . . . . . . . . 15 ℕ ⊆ ℕ0
2928a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ℕ ⊆ ℕ0)
30 nn0uz 11760 . . . . . . . . . . . . . 14 0 = (ℤ‘0)
3129, 30syl6sseq 3684 . . . . . . . . . . . . 13 (𝜑 → ℕ ⊆ (ℤ‘0))
3231, 2sseldd 3637 . . . . . . . . . . . 12 (𝜑𝑀 ∈ (ℤ‘0))
33 eluzfz1 12386 . . . . . . . . . . . 12 (𝑀 ∈ (ℤ‘0) → 0 ∈ (0...𝑀))
3432, 33syl 17 . . . . . . . . . . 11 (𝜑 → 0 ∈ (0...𝑀))
3518, 34ffvelrnd 6400 . . . . . . . . . . . 12 (𝜑 → (𝑉‘0) ∈ ℝ)
3635, 13resubcld 10496 . . . . . . . . . . 11 (𝜑 → ((𝑉‘0) − 𝑋) ∈ ℝ)
3724, 27, 34, 36fvmptd 6327 . . . . . . . . . 10 (𝜑 → (𝑄‘0) = ((𝑉‘0) − 𝑋))
387fourierdlem2 40644 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ → (𝑉 ∈ (𝑃𝑀) ↔ (𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))))
392, 38syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑉 ∈ (𝑃𝑀) ↔ (𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))))
408, 39mpbid 222 . . . . . . . . . . . . . 14 (𝜑 → (𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1)))))
4140simprd 478 . . . . . . . . . . . . 13 (𝜑 → (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))
4241simpld 474 . . . . . . . . . . . 12 (𝜑 → ((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)))
4342simpld 474 . . . . . . . . . . 11 (𝜑 → (𝑉‘0) = (-π + 𝑋))
4443oveq1d 6705 . . . . . . . . . 10 (𝜑 → ((𝑉‘0) − 𝑋) = ((-π + 𝑋) − 𝑋))
4512recnd 10106 . . . . . . . . . . 11 (𝜑 → -π ∈ ℂ)
4613recnd 10106 . . . . . . . . . . 11 (𝜑𝑋 ∈ ℂ)
4745, 46pncand 10431 . . . . . . . . . 10 (𝜑 → ((-π + 𝑋) − 𝑋) = -π)
4837, 44, 473eqtrd 2689 . . . . . . . . 9 (𝜑 → (𝑄‘0) = -π)
4912rexrd 10127 . . . . . . . . . 10 (𝜑 → -π ∈ ℝ*)
5015rexrd 10127 . . . . . . . . . 10 (𝜑 → π ∈ ℝ*)
51 fourierdlem50.ab . . . . . . . . . . 11 (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
523leidd 10632 . . . . . . . . . . . 12 (𝜑𝐴𝐴)
533, 4, 3, 52, 6eliccd 40044 . . . . . . . . . . 11 (𝜑𝐴 ∈ (𝐴[,]𝐵))
5451, 53sseldd 3637 . . . . . . . . . 10 (𝜑𝐴 ∈ (-π[,]π))
55 iccgelb 12268 . . . . . . . . . 10 ((-π ∈ ℝ* ∧ π ∈ ℝ*𝐴 ∈ (-π[,]π)) → -π ≤ 𝐴)
5649, 50, 54, 55syl3anc 1366 . . . . . . . . 9 (𝜑 → -π ≤ 𝐴)
5748, 56eqbrtrd 4707 . . . . . . . 8 (𝜑 → (𝑄‘0) ≤ 𝐴)
584leidd 10632 . . . . . . . . . . . 12 (𝜑𝐵𝐵)
593, 4, 4, 6, 58eliccd 40044 . . . . . . . . . . 11 (𝜑𝐵 ∈ (𝐴[,]𝐵))
6051, 59sseldd 3637 . . . . . . . . . 10 (𝜑𝐵 ∈ (-π[,]π))
61 iccleub 12267 . . . . . . . . . 10 ((-π ∈ ℝ* ∧ π ∈ ℝ*𝐵 ∈ (-π[,]π)) → 𝐵 ≤ π)
6249, 50, 60, 61syl3anc 1366 . . . . . . . . 9 (𝜑𝐵 ≤ π)
63 fveq2 6229 . . . . . . . . . . . . 13 (𝑖 = 𝑀 → (𝑉𝑖) = (𝑉𝑀))
6463oveq1d 6705 . . . . . . . . . . . 12 (𝑖 = 𝑀 → ((𝑉𝑖) − 𝑋) = ((𝑉𝑀) − 𝑋))
6564adantl 481 . . . . . . . . . . 11 ((𝜑𝑖 = 𝑀) → ((𝑉𝑖) − 𝑋) = ((𝑉𝑀) − 𝑋))
66 eluzfz2 12387 . . . . . . . . . . . 12 (𝑀 ∈ (ℤ‘0) → 𝑀 ∈ (0...𝑀))
6732, 66syl 17 . . . . . . . . . . 11 (𝜑𝑀 ∈ (0...𝑀))
6818, 67ffvelrnd 6400 . . . . . . . . . . . 12 (𝜑 → (𝑉𝑀) ∈ ℝ)
6968, 13resubcld 10496 . . . . . . . . . . 11 (𝜑 → ((𝑉𝑀) − 𝑋) ∈ ℝ)
7024, 65, 67, 69fvmptd 6327 . . . . . . . . . 10 (𝜑 → (𝑄𝑀) = ((𝑉𝑀) − 𝑋))
7142simprd 478 . . . . . . . . . . 11 (𝜑 → (𝑉𝑀) = (π + 𝑋))
7271oveq1d 6705 . . . . . . . . . 10 (𝜑 → ((𝑉𝑀) − 𝑋) = ((π + 𝑋) − 𝑋))
7315recnd 10106 . . . . . . . . . . 11 (𝜑 → π ∈ ℂ)
7473, 46pncand 10431 . . . . . . . . . 10 (𝜑 → ((π + 𝑋) − 𝑋) = π)
7570, 72, 743eqtrrd 2690 . . . . . . . . 9 (𝜑 → π = (𝑄𝑀))
7662, 75breqtrd 4711 . . . . . . . 8 (𝜑𝐵 ≤ (𝑄𝑀))
77 fourierdlem50.j . . . . . . . 8 (𝜑𝐽 ∈ (0..^𝑁))
78 fourierdlem50.t . . . . . . . 8 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))
79 prfi 8276 . . . . . . . . . . . 12 {𝐴, 𝐵} ∈ Fin
8079a1i 11 . . . . . . . . . . 11 (𝜑 → {𝐴, 𝐵} ∈ Fin)
81 fzfid 12812 . . . . . . . . . . . . 13 (𝜑 → (0...𝑀) ∈ Fin)
8222rnmptfi 39665 . . . . . . . . . . . . 13 ((0...𝑀) ∈ Fin → ran 𝑄 ∈ Fin)
8381, 82syl 17 . . . . . . . . . . . 12 (𝜑 → ran 𝑄 ∈ Fin)
84 infi 8225 . . . . . . . . . . . 12 (ran 𝑄 ∈ Fin → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
8583, 84syl 17 . . . . . . . . . . 11 (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
86 unfi 8268 . . . . . . . . . . 11 (({𝐴, 𝐵} ∈ Fin ∧ (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin) → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
8780, 85, 86syl2anc 694 . . . . . . . . . 10 (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
8878, 87syl5eqel 2734 . . . . . . . . 9 (𝜑𝑇 ∈ Fin)
893, 4jca 553 . . . . . . . . . . . 12 (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
90 prssg 4382 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
913, 4, 90syl2anc 694 . . . . . . . . . . . 12 (𝜑 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
9289, 91mpbid 222 . . . . . . . . . . 11 (𝜑 → {𝐴, 𝐵} ⊆ ℝ)
93 inss2 3867 . . . . . . . . . . . . 13 (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴(,)𝐵)
94 ioossre 12273 . . . . . . . . . . . . 13 (𝐴(,)𝐵) ⊆ ℝ
9593, 94sstri 3645 . . . . . . . . . . . 12 (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ
9695a1i 11 . . . . . . . . . . 11 (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ)
9792, 96unssd 3822 . . . . . . . . . 10 (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ ℝ)
9878, 97syl5eqss 3682 . . . . . . . . 9 (𝜑𝑇 ⊆ ℝ)
99 fourierdlem50.s . . . . . . . . 9 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇))
100 fourierdlem50.n . . . . . . . . 9 𝑁 = ((#‘𝑇) − 1)
10188, 98, 99, 100fourierdlem36 40678 . . . . . . . 8 (𝜑𝑆 Isom < , < ((0...𝑁), 𝑇))
102 eqid 2651 . . . . . . . 8 sup({𝑥 ∈ (0..^𝑀) ∣ (𝑄𝑥) ≤ (𝑆𝐽)}, ℝ, < ) = sup({𝑥 ∈ (0..^𝑀) ∣ (𝑄𝑥) ≤ (𝑆𝐽)}, ℝ, < )
1032, 3, 4, 6, 23, 57, 76, 77, 78, 101, 102fourierdlem20 40662 . . . . . . 7 (𝜑 → ∃𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
104 fourierdlem50.ch . . . . . . . . . . . . 13 (𝜒 ↔ ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))))
105104biimpi 206 . . . . . . . . . . . . . . . . . 18 (𝜒 → ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))))
106 simp-4l 823 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝜑)
107105, 106syl 17 . . . . . . . . . . . . . . . . 17 (𝜒𝜑)
108 simplr 807 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑘 ∈ (0..^𝑀))
109105, 108syl 17 . . . . . . . . . . . . . . . . 17 (𝜒𝑘 ∈ (0..^𝑀))
110107, 109jca 553 . . . . . . . . . . . . . . . 16 (𝜒 → (𝜑𝑘 ∈ (0..^𝑀)))
111 simp-4r 824 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑖 ∈ (0..^𝑀))
112105, 111syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝑖 ∈ (0..^𝑀))
113 elfzofz 12524 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ (0..^𝑀) → 𝑘 ∈ (0...𝑀))
114113ad2antlr 763 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑘 ∈ (0...𝑀))
115105, 114syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜒𝑘 ∈ (0...𝑀))
116107, 18syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒𝑉:(0...𝑀)⟶ℝ)
117116, 115ffvelrnd 6400 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (𝑉𝑘) ∈ ℝ)
118107, 13syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜒𝑋 ∈ ℝ)
119117, 118resubcld 10496 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ((𝑉𝑘) − 𝑋) ∈ ℝ)
120 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 𝑘 → (𝑉𝑖) = (𝑉𝑘))
121120oveq1d 6705 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑘 → ((𝑉𝑖) − 𝑋) = ((𝑉𝑘) − 𝑋))
122121, 22fvmptg 6319 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ (0...𝑀) ∧ ((𝑉𝑘) − 𝑋) ∈ ℝ) → (𝑄𝑘) = ((𝑉𝑘) − 𝑋))
123115, 119, 122syl2anc 694 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑄𝑘) = ((𝑉𝑘) − 𝑋))
124123, 119eqeltrd 2730 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄𝑘) ∈ ℝ)
12523adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
126 fzofzp1 12605 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
127126adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
128125, 127ffvelrnd 6400 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
129107, 112, 128syl2anc 694 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℝ)
130 isof1o 6613 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑆 Isom < , < ((0...𝑁), 𝑇) → 𝑆:(0...𝑁)–1-1-onto𝑇)
131101, 130syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑆:(0...𝑁)–1-1-onto𝑇)
132 f1of 6175 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑆:(0...𝑁)–1-1-onto𝑇𝑆:(0...𝑁)⟶𝑇)
133131, 132syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑆:(0...𝑁)⟶𝑇)
134 fzofzp1 12605 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
13577, 134syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
136133, 135ffvelrnd 6400 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ 𝑇)
13798, 136sseldd 3637 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
138107, 137syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
139 elfzofz 12524 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
14077, 139syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐽 ∈ (0...𝑁))
141133, 140ffvelrnd 6400 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑆𝐽) ∈ 𝑇)
14298, 141sseldd 3637 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑆𝐽) ∈ ℝ)
143107, 142syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑆𝐽) ∈ ℝ)
144105simprd 478 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
145124rexrd 10127 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → (𝑄𝑘) ∈ ℝ*)
14623adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
147 fzofzp1 12605 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 ∈ (0..^𝑀) → (𝑘 + 1) ∈ (0...𝑀))
148147adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0..^𝑀)) → (𝑘 + 1) ∈ (0...𝑀))
149146, 148ffvelrnd 6400 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ (0..^𝑀)) → (𝑄‘(𝑘 + 1)) ∈ ℝ)
150149rexrd 10127 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (0..^𝑀)) → (𝑄‘(𝑘 + 1)) ∈ ℝ*)
151110, 150syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → (𝑄‘(𝑘 + 1)) ∈ ℝ*)
152143rexrd 10127 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → (𝑆𝐽) ∈ ℝ*)
153138rexrd 10127 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → (𝑆‘(𝐽 + 1)) ∈ ℝ*)
154 elfzoelz 12509 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
155154zred 11520 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℝ)
156155ltp1d 10992 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐽 ∈ (0..^𝑁) → 𝐽 < (𝐽 + 1))
15777, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐽 < (𝐽 + 1))
158 isoeq5 6611 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) → (𝑆 Isom < , < ((0...𝑁), 𝑇) ↔ 𝑆 Isom < , < ((0...𝑁), ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))))))
15978, 158ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑆 Isom < , < ((0...𝑁), 𝑇) ↔ 𝑆 Isom < , < ((0...𝑁), ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))))
160101, 159sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑆 Isom < , < ((0...𝑁), ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))))
161 isorel 6616 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑆 Isom < , < ((0...𝑁), ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))) ∧ (𝐽 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝐽 < (𝐽 + 1) ↔ (𝑆𝐽) < (𝑆‘(𝐽 + 1))))
162160, 140, 135, 161syl12anc 1364 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐽 < (𝐽 + 1) ↔ (𝑆𝐽) < (𝑆‘(𝐽 + 1))))
163157, 162mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑆𝐽) < (𝑆‘(𝐽 + 1)))
164107, 163syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → (𝑆𝐽) < (𝑆‘(𝐽 + 1)))
165145, 151, 152, 153, 164ioossioobi 40061 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ ((𝑄𝑘) ≤ (𝑆𝐽) ∧ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑘 + 1)))))
166144, 165mpbid 222 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → ((𝑄𝑘) ≤ (𝑆𝐽) ∧ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑘 + 1))))
167166simpld 474 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑄𝑘) ≤ (𝑆𝐽))
168124, 143, 138, 167, 164lelttrd 10233 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑄𝑘) < (𝑆‘(𝐽 + 1)))
169 elfzofz 12524 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
170169ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑖 ∈ (0...𝑀))
171170ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑖 ∈ (0...𝑀))
172105, 171syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒𝑖 ∈ (0...𝑀))
173107, 172, 21syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → ((𝑉𝑖) − 𝑋) ∈ ℝ)
17422fvmpt2 6330 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ (0...𝑀) ∧ ((𝑉𝑖) − 𝑋) ∈ ℝ) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
175172, 173, 174syl2anc 694 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
176175, 173eqeltrd 2730 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (𝑄𝑖) ∈ ℝ)
177 simpllr 815 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
178105, 177syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
179176, 129, 143, 138, 164, 178fourierdlem10 40652 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ((𝑄𝑖) ≤ (𝑆𝐽) ∧ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑖 + 1))))
180179simprd 478 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑖 + 1)))
181124, 138, 129, 168, 180ltletrd 10235 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄𝑘) < (𝑄‘(𝑖 + 1)))
182124, 129, 118, 181ltadd2dd 10234 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + (𝑄𝑘)) < (𝑋 + (𝑄‘(𝑖 + 1))))
183123oveq2d 6706 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + (𝑄𝑘)) = (𝑋 + ((𝑉𝑘) − 𝑋)))
184107, 46syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒𝑋 ∈ ℂ)
185117recnd 10106 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑉𝑘) ∈ ℂ)
186184, 185pncan3d 10433 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + ((𝑉𝑘) − 𝑋)) = (𝑉𝑘))
187183, 186eqtr2d 2686 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑉𝑘) = (𝑋 + (𝑄𝑘)))
188112, 126syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑖 + 1) ∈ (0...𝑀))
18918adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
190189, 127ffvelrnd 6400 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
191107, 112, 190syl2anc 694 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℝ)
192191, 118resubcld 10496 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
193188, 192jca 553 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ((𝑖 + 1) ∈ (0...𝑀) ∧ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ))
194 eleq1 2718 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑖 + 1) → (𝑘 ∈ (0...𝑀) ↔ (𝑖 + 1) ∈ (0...𝑀)))
195 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = (𝑖 + 1) → (𝑉𝑘) = (𝑉‘(𝑖 + 1)))
196195oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = (𝑖 + 1) → ((𝑉𝑘) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
197196eleq1d 2715 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑖 + 1) → (((𝑉𝑘) − 𝑋) ∈ ℝ ↔ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ))
198194, 197anbi12d 747 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = (𝑖 + 1) → ((𝑘 ∈ (0...𝑀) ∧ ((𝑉𝑘) − 𝑋) ∈ ℝ) ↔ ((𝑖 + 1) ∈ (0...𝑀) ∧ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)))
199 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑖 + 1) → (𝑄𝑘) = (𝑄‘(𝑖 + 1)))
200199, 196eqeq12d 2666 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = (𝑖 + 1) → ((𝑄𝑘) = ((𝑉𝑘) − 𝑋) ↔ (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋)))
201198, 200imbi12d 333 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = (𝑖 + 1) → (((𝑘 ∈ (0...𝑀) ∧ ((𝑉𝑘) − 𝑋) ∈ ℝ) → (𝑄𝑘) = ((𝑉𝑘) − 𝑋)) ↔ (((𝑖 + 1) ∈ (0...𝑀) ∧ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))))
202201, 122vtoclg 3297 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 + 1) ∈ (0...𝑀) → (((𝑖 + 1) ∈ (0...𝑀) ∧ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋)))
203188, 193, 202sylc 65 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
204203oveq2d 6706 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)))
205191recnd 10106 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℂ)
206184, 205pncan3d 10433 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)) = (𝑉‘(𝑖 + 1)))
207204, 206eqtr2d 2686 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑉‘(𝑖 + 1)) = (𝑋 + (𝑄‘(𝑖 + 1))))
208182, 187, 2073brtr4d 4717 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑉𝑘) < (𝑉‘(𝑖 + 1)))
209 eleq1 2718 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑖 → (𝑙 ∈ (0..^𝑀) ↔ 𝑖 ∈ (0..^𝑀)))
210209anbi2d 740 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑖 → (((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ↔ ((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (0..^𝑀))))
211 oveq1 6697 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑖 → (𝑙 + 1) = (𝑖 + 1))
212211fveq2d 6233 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑖 → (𝑉‘(𝑙 + 1)) = (𝑉‘(𝑖 + 1)))
213212breq2d 4697 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑖 → ((𝑉𝑘) < (𝑉‘(𝑙 + 1)) ↔ (𝑉𝑘) < (𝑉‘(𝑖 + 1))))
214210, 213anbi12d 747 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑖 → ((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑙 + 1))) ↔ (((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑖 + 1)))))
215 fveq2 6229 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑖 → (𝑉𝑙) = (𝑉𝑖))
216215breq2d 4697 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑖 → ((𝑉𝑘) ≤ (𝑉𝑙) ↔ (𝑉𝑘) ≤ (𝑉𝑖)))
217214, 216imbi12d 333 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑖 → (((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑙 + 1))) → (𝑉𝑘) ≤ (𝑉𝑙)) ↔ ((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑖 + 1))) → (𝑉𝑘) ≤ (𝑉𝑖))))
218 eleq1 2718 . . . . . . . . . . . . . . . . . . . . . 22 ( = 𝑘 → ( ∈ (0..^𝑀) ↔ 𝑘 ∈ (0..^𝑀)))
219218anbi2d 740 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝑘 → ((𝜑 ∈ (0..^𝑀)) ↔ (𝜑𝑘 ∈ (0..^𝑀))))
220219anbi1d 741 . . . . . . . . . . . . . . . . . . . 20 ( = 𝑘 → (((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ↔ ((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀))))
221 fveq2 6229 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝑘 → (𝑉) = (𝑉𝑘))
222221breq1d 4695 . . . . . . . . . . . . . . . . . . . 20 ( = 𝑘 → ((𝑉) < (𝑉‘(𝑙 + 1)) ↔ (𝑉𝑘) < (𝑉‘(𝑙 + 1))))
223220, 222anbi12d 747 . . . . . . . . . . . . . . . . . . 19 ( = 𝑘 → ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ↔ (((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑙 + 1)))))
224221breq1d 4695 . . . . . . . . . . . . . . . . . . 19 ( = 𝑘 → ((𝑉) ≤ (𝑉𝑙) ↔ (𝑉𝑘) ≤ (𝑉𝑙)))
225223, 224imbi12d 333 . . . . . . . . . . . . . . . . . 18 ( = 𝑘 → (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → (𝑉) ≤ (𝑉𝑙)) ↔ ((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑙 + 1))) → (𝑉𝑘) ≤ (𝑉𝑙))))
226 elfzoelz 12509 . . . . . . . . . . . . . . . . . . . . 21 ( ∈ (0..^𝑀) → ∈ ℤ)
227226ad3antlr 767 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → ∈ ℤ)
228 elfzoelz 12509 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 ∈ (0..^𝑀) → 𝑙 ∈ ℤ)
229228ad2antlr 763 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → 𝑙 ∈ ℤ)
230 simplr 807 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ ¬ < (𝑙 + 1)) → (𝑉) < (𝑉‘(𝑙 + 1)))
23118adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑙 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
232 fzofzp1 12605 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (0..^𝑀) → (𝑙 + 1) ∈ (0...𝑀))
233232adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑙 ∈ (0..^𝑀)) → (𝑙 + 1) ∈ (0...𝑀))
234231, 233ffvelrnd 6400 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑙 ∈ (0..^𝑀)) → (𝑉‘(𝑙 + 1)) ∈ ℝ)
235234adantlr 751 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) → (𝑉‘(𝑙 + 1)) ∈ ℝ)
236235adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → (𝑉‘(𝑙 + 1)) ∈ ℝ)
23718adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
238 elfzofz 12524 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ( ∈ (0..^𝑀) → ∈ (0...𝑀))
239238adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∈ (0..^𝑀)) → ∈ (0...𝑀))
240237, 239ffvelrnd 6400 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∈ (0..^𝑀)) → (𝑉) ∈ ℝ)
241240ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → (𝑉) ∈ ℝ)
242228zred 11520 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (0..^𝑀) → 𝑙 ∈ ℝ)
243 peano2re 10247 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ ℝ → (𝑙 + 1) ∈ ℝ)
244242, 243syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑙 ∈ (0..^𝑀) → (𝑙 + 1) ∈ ℝ)
245244ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → (𝑙 + 1) ∈ ℝ)
246226zred 11520 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ( ∈ (0..^𝑀) → ∈ ℝ)
247246ad3antlr 767 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → ∈ ℝ)
248 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → ¬ < (𝑙 + 1))
249245, 247, 248nltled 10225 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → (𝑙 + 1) ≤ )
250228peano2zd 11523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (0..^𝑀) → (𝑙 + 1) ∈ ℤ)
251250ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → (𝑙 + 1) ∈ ℤ)
252226ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → ∈ ℤ)
253 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → (𝑙 + 1) ≤ )
254 eluz2 11731 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ( ∈ (ℤ‘(𝑙 + 1)) ↔ ((𝑙 + 1) ∈ ℤ ∧ ∈ ℤ ∧ (𝑙 + 1) ≤ ))
255251, 252, 253, 254syl3anbrc 1265 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → ∈ (ℤ‘(𝑙 + 1)))
256255adantlll 754 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → ∈ (ℤ‘(𝑙 + 1)))
257 simplll 813 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝜑)
258 0zd 11427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 ∈ ℤ)
259 elfzoel2 12508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ( ∈ (0..^𝑀) → 𝑀 ∈ ℤ)
260259ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑀 ∈ ℤ)
261 elfzelz 12380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ ((𝑙 + 1)...) → 𝑖 ∈ ℤ)
262261adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 ∈ ℤ)
263258, 260, 2623jca 1261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ))
264 0red 10079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 ∈ ℝ)
265261zred 11520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑖 ∈ ((𝑙 + 1)...) → 𝑖 ∈ ℝ)
266265adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 ∈ ℝ)
267242adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑙 ∈ ℝ)
268 elfzole1 12517 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑙 ∈ (0..^𝑀) → 0 ≤ 𝑙)
269268adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 ≤ 𝑙)
270267, 243syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → (𝑙 + 1) ∈ ℝ)
271267ltp1d 10992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑙 < (𝑙 + 1))
272 elfzle1 12382 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑖 ∈ ((𝑙 + 1)...) → (𝑙 + 1) ≤ 𝑖)
273272adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → (𝑙 + 1) ≤ 𝑖)
274267, 270, 266, 271, 273ltletrd 10235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑙 < 𝑖)
275264, 267, 266, 269, 274lelttrd 10233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 < 𝑖)
276264, 266, 275ltled 10223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 ≤ 𝑖)
277276adantll 750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 ≤ 𝑖)
278265adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 ∈ ℝ)
279259zred 11520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( ∈ (0..^𝑀) → 𝑀 ∈ ℝ)
280279adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑀 ∈ ℝ)
281246adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → ∈ ℝ)
282 elfzle2 12383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑖 ∈ ((𝑙 + 1)...) → 𝑖)
283282adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖)
284 elfzolt2 12518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ( ∈ (0..^𝑀) → < 𝑀)
285284adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → < 𝑀)
286278, 281, 280, 283, 285lelttrd 10233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 < 𝑀)
287278, 280, 286ltled 10223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖𝑀)
288287adantlr 751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖𝑀)
289263, 277, 288jca32 557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (0 ≤ 𝑖𝑖𝑀)))
290 elfz2 12371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (0 ≤ 𝑖𝑖𝑀)))
291289, 290sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 ∈ (0...𝑀))
292291adantlll 754 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 ∈ (0...𝑀))
293257, 292, 19syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → (𝑉𝑖) ∈ ℝ)
294293adantlr 751 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → (𝑉𝑖) ∈ ℝ)
295 simplll 813 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝜑)
296 0zd 11427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 0 ∈ ℤ)
297 elfzelz 12380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 ∈ ((𝑙 + 1)...( − 1)) → 𝑖 ∈ ℤ)
298297adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ ℤ)
299 0red 10079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 0 ∈ ℝ)
300298zred 11520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ ℝ)
301242adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑙 ∈ ℝ)
302268adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 0 ≤ 𝑙)
303301, 243syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → (𝑙 + 1) ∈ ℝ)
304301ltp1d 10992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑙 < (𝑙 + 1))
305 elfzle1 12382 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑖 ∈ ((𝑙 + 1)...( − 1)) → (𝑙 + 1) ≤ 𝑖)
306305adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → (𝑙 + 1) ≤ 𝑖)
307301, 303, 300, 304, 306ltletrd 10235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑙 < 𝑖)
308299, 301, 300, 302, 307lelttrd 10233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 0 < 𝑖)
309299, 300, 308ltled 10223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 0 ≤ 𝑖)
310 eluz2 11731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (ℤ‘0) ↔ (0 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 0 ≤ 𝑖))
311296, 298, 309, 310syl3anbrc 1265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ (ℤ‘0))
312311adantll 750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ (ℤ‘0))
313 elfzoel2 12508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (0..^𝑀) → 𝑀 ∈ ℤ)
314313ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑀 ∈ ℤ)
315297zred 11520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ ((𝑙 + 1)...( − 1)) → 𝑖 ∈ ℝ)
316315adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ ℝ)
317 peano2rem 10386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( ∈ ℝ → ( − 1) ∈ ℝ)
318246, 317syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ( ∈ (0..^𝑀) → ( − 1) ∈ ℝ)
319318adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → ( − 1) ∈ ℝ)
320279adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑀 ∈ ℝ)
321 elfzle2 12383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ ((𝑙 + 1)...( − 1)) → 𝑖 ≤ ( − 1))
322321adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ≤ ( − 1))
323246ltm1d 10994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( ∈ (0..^𝑀) → ( − 1) < )
324318, 246, 279, 323, 284lttrd 10236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ( ∈ (0..^𝑀) → ( − 1) < 𝑀)
325324adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → ( − 1) < 𝑀)
326316, 319, 320, 322, 325lelttrd 10233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 < 𝑀)
327326adantll 750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 < 𝑀)
328327adantlr 751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 < 𝑀)
329 elfzo2 12512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ (0..^𝑀) ↔ (𝑖 ∈ (ℤ‘0) ∧ 𝑀 ∈ ℤ ∧ 𝑖 < 𝑀))
330312, 314, 328, 329syl3anbrc 1265 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ (0..^𝑀))
331169, 19sylan2 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ∈ ℝ)
33241simprd 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1)))
333332r19.21bi 2961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) < (𝑉‘(𝑖 + 1)))
334331, 190, 333ltled 10223 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ≤ (𝑉‘(𝑖 + 1)))
335295, 330, 334syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → (𝑉𝑖) ≤ (𝑉‘(𝑖 + 1)))
336335adantlr 751 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → (𝑉𝑖) ≤ (𝑉‘(𝑖 + 1)))
337256, 294, 336monoord 12871 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → (𝑉‘(𝑙 + 1)) ≤ (𝑉))
338249, 337syldan 486 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → (𝑉‘(𝑙 + 1)) ≤ (𝑉))
339236, 241, 338lensymd 10226 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → ¬ (𝑉) < (𝑉‘(𝑙 + 1)))
340339adantlr 751 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ ¬ < (𝑙 + 1)) → ¬ (𝑉) < (𝑉‘(𝑙 + 1)))
341230, 340condan 852 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → < (𝑙 + 1))
342 zleltp1 11466 . . . . . . . . . . . . . . . . . . . . . 22 (( ∈ ℤ ∧ 𝑙 ∈ ℤ) → (𝑙 < (𝑙 + 1)))
343227, 229, 342syl2anc 694 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → (𝑙 < (𝑙 + 1)))
344341, 343mpbird 247 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → 𝑙)
345 eluz2 11731 . . . . . . . . . . . . . . . . . . . 20 (𝑙 ∈ (ℤ) ↔ ( ∈ ℤ ∧ 𝑙 ∈ ℤ ∧ 𝑙))
346227, 229, 344, 345syl3anbrc 1265 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → 𝑙 ∈ (ℤ))
34718ad3antrrr 766 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑉:(0...𝑀)⟶ℝ)
348 0zd 11427 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 0 ∈ ℤ)
349259ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑀 ∈ ℤ)
350 elfzelz 12380 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (...𝑙) → 𝑖 ∈ ℤ)
351350adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 ∈ ℤ)
352348, 349, 3513jca 1261 . . . . . . . . . . . . . . . . . . . . . . . 24 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ))
353 0red 10079 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 0 ∈ ℝ)
354246adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → ∈ ℝ)
355350zred 11520 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (...𝑙) → 𝑖 ∈ ℝ)
356355adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 ∈ ℝ)
357 elfzole1 12517 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ( ∈ (0..^𝑀) → 0 ≤ )
358357adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 0 ≤ )
359 elfzle1 12382 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (...𝑙) → 𝑖)
360359adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖)
361353, 354, 356, 358, 360letrd 10232 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 0 ≤ 𝑖)
362361adantlr 751 . . . . . . . . . . . . . . . . . . . . . . . 24 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 0 ≤ 𝑖)
363355adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 ∈ ℝ)
364313zred 11520 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑙 ∈ (0..^𝑀) → 𝑀 ∈ ℝ)
365364adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑀 ∈ ℝ)
366242adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑙 ∈ ℝ)
367 elfzle2 12383 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ (...𝑙) → 𝑖𝑙)
368367adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖𝑙)
369 elfzolt2 12518 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (0..^𝑀) → 𝑙 < 𝑀)
370369adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑙 < 𝑀)
371363, 366, 365, 368, 370lelttrd 10233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 < 𝑀)
372363, 365, 371ltled 10223 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖𝑀)
373372adantll 750 . . . . . . . . . . . . . . . . . . . . . . . 24 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑖𝑀)
374352, 362, 373jca32 557 . . . . . . . . . . . . . . . . . . . . . . 23 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (0 ≤ 𝑖𝑖𝑀)))
375374, 290sylibr 224 . . . . . . . . . . . . . . . . . . . . . 22 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 ∈ (0...𝑀))
376375adantlll 754 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 ∈ (0...𝑀))
377347, 376ffvelrnd 6400 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → (𝑉𝑖) ∈ ℝ)
378377adantlr 751 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...𝑙)) → (𝑉𝑖) ∈ ℝ)
379 simp-4l 823 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝜑)
380 0zd 11427 . . . . . . . . . . . . . . . . . . . . . . . 24 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 0 ∈ ℤ)
381 elfzelz 12380 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ (...(𝑙 − 1)) → 𝑖 ∈ ℤ)
382381adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ ℤ)
383 0red 10079 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 0 ∈ ℝ)
384246adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → ∈ ℝ)
385382zred 11520 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ ℝ)
386357adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 0 ≤ )
387 elfzle1 12382 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (...(𝑙 − 1)) → 𝑖)
388387adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖)
389383, 384, 385, 386, 388letrd 10232 . . . . . . . . . . . . . . . . . . . . . . . 24 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 0 ≤ 𝑖)
390380, 382, 389, 310syl3anbrc 1265 . . . . . . . . . . . . . . . . . . . . . . 23 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ (ℤ‘0))
391390adantll 750 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ (ℤ‘0))
392391ad4ant14 1317 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ (ℤ‘0))
393313ad3antlr 767 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑀 ∈ ℤ)
394381zred 11520 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ (...(𝑙 − 1)) → 𝑖 ∈ ℝ)
395394adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ ℝ)
396242adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑙 ∈ ℝ)
397364adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑀 ∈ ℝ)
398 elfzle2 12383 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (...(𝑙 − 1)) → 𝑖 ≤ (𝑙 − 1))
399398adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ≤ (𝑙 − 1))
400 zltlem1 11468 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑖 ∈ ℤ ∧ 𝑙 ∈ ℤ) → (𝑖 < 𝑙𝑖 ≤ (𝑙 − 1)))
401381, 228, 400syl2anr 494 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → (𝑖 < 𝑙𝑖 ≤ (𝑙 − 1)))
402399, 401mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 < 𝑙)
403369adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑙 < 𝑀)
404395, 396, 397, 402, 403lttrd 10236 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 < 𝑀)
405404adantll 750 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 < 𝑀)
406405adantlr 751 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 < 𝑀)
407392, 393, 406, 329syl3anbrc 1265 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ (0..^𝑀))
408379, 407, 334syl2anc 694 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → (𝑉𝑖) ≤ (𝑉‘(𝑖 + 1)))
409346, 378, 408monoord 12871 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → (𝑉) ≤ (𝑉𝑙))
410225, 409chvarv 2299 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑙 + 1))) → (𝑉𝑘) ≤ (𝑉𝑙))
411217, 410chvarv 2299 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑖 + 1))) → (𝑉𝑘) ≤ (𝑉𝑖))
412110, 112, 208, 411syl21anc 1365 . . . . . . . . . . . . . . 15 (𝜒 → (𝑉𝑘) ≤ (𝑉𝑖))
413107, 112jca 553 . . . . . . . . . . . . . . . 16 (𝜒 → (𝜑𝑖 ∈ (0..^𝑀)))
414110, 149syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄‘(𝑘 + 1)) ∈ ℝ)
415179simpld 474 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑄𝑖) ≤ (𝑆𝐽))
416176, 143, 138, 415, 164lelttrd 10233 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑄𝑖) < (𝑆‘(𝐽 + 1)))
417166simprd 478 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑘 + 1)))
418176, 138, 414, 416, 417ltletrd 10235 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄𝑖) < (𝑄‘(𝑘 + 1)))
419176, 414, 118, 418ltadd2dd 10234 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + (𝑄𝑖)) < (𝑋 + (𝑄‘(𝑘 + 1))))
420175oveq2d 6706 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + (𝑄𝑖)) = (𝑋 + ((𝑉𝑖) − 𝑋)))
421107, 172, 19syl2anc 694 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑉𝑖) ∈ ℝ)
422421recnd 10106 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑉𝑖) ∈ ℂ)
423184, 422pncan3d 10433 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + ((𝑉𝑖) − 𝑋)) = (𝑉𝑖))
424420, 423eqtr2d 2686 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑉𝑖) = (𝑋 + (𝑄𝑖)))
42522a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0..^𝑀)) → 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋)))
426 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = (𝑘 + 1) → (𝑉𝑖) = (𝑉‘(𝑘 + 1)))
427426oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = (𝑘 + 1) → ((𝑉𝑖) − 𝑋) = ((𝑉‘(𝑘 + 1)) − 𝑋))
428427adantl 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑖 = (𝑘 + 1)) → ((𝑉𝑖) − 𝑋) = ((𝑉‘(𝑘 + 1)) − 𝑋))
42918adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
430429, 148ffvelrnd 6400 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (0..^𝑀)) → (𝑉‘(𝑘 + 1)) ∈ ℝ)
43113adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
432430, 431resubcld 10496 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0..^𝑀)) → ((𝑉‘(𝑘 + 1)) − 𝑋) ∈ ℝ)
433425, 428, 148, 432fvmptd 6327 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0..^𝑀)) → (𝑄‘(𝑘 + 1)) = ((𝑉‘(𝑘 + 1)) − 𝑋))
434107, 109, 433syl2anc 694 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑄‘(𝑘 + 1)) = ((𝑉‘(𝑘 + 1)) − 𝑋))
435434oveq2d 6706 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + (𝑄‘(𝑘 + 1))) = (𝑋 + ((𝑉‘(𝑘 + 1)) − 𝑋)))
436110, 430syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑉‘(𝑘 + 1)) ∈ ℝ)
437436recnd 10106 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑉‘(𝑘 + 1)) ∈ ℂ)
438184, 437pncan3d 10433 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + ((𝑉‘(𝑘 + 1)) − 𝑋)) = (𝑉‘(𝑘 + 1)))
439435, 438eqtr2d 2686 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑉‘(𝑘 + 1)) = (𝑋 + (𝑄‘(𝑘 + 1))))
440419, 424, 4393brtr4d 4717 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑉𝑖) < (𝑉‘(𝑘 + 1)))
441 eleq1 2718 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑘 → (𝑙 ∈ (0..^𝑀) ↔ 𝑘 ∈ (0..^𝑀)))
442441anbi2d 740 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑘 → (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ↔ ((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑘 ∈ (0..^𝑀))))
443 oveq1 6697 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑘 → (𝑙 + 1) = (𝑘 + 1))
444443fveq2d 6233 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑘 → (𝑉‘(𝑙 + 1)) = (𝑉‘(𝑘 + 1)))
445444breq2d 4697 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑘 → ((𝑉𝑖) < (𝑉‘(𝑙 + 1)) ↔ (𝑉𝑖) < (𝑉‘(𝑘 + 1))))
446442, 445anbi12d 747 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑘 → ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑙 + 1))) ↔ (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑘 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑘 + 1)))))
447 fveq2 6229 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑘 → (𝑉𝑙) = (𝑉𝑘))
448447breq2d 4697 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑘 → ((𝑉𝑖) ≤ (𝑉𝑙) ↔ (𝑉𝑖) ≤ (𝑉𝑘)))
449446, 448imbi12d 333 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑘 → (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑙 + 1))) → (𝑉𝑖) ≤ (𝑉𝑙)) ↔ ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑘 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑘 + 1))) → (𝑉𝑖) ≤ (𝑉𝑘))))
450 eleq1 2718 . . . . . . . . . . . . . . . . . . . . . 22 ( = 𝑖 → ( ∈ (0..^𝑀) ↔ 𝑖 ∈ (0..^𝑀)))
451450anbi2d 740 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝑖 → ((𝜑 ∈ (0..^𝑀)) ↔ (𝜑𝑖 ∈ (0..^𝑀))))
452451anbi1d 741 . . . . . . . . . . . . . . . . . . . 20 ( = 𝑖 → (((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ↔ ((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀))))
453 fveq2 6229 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝑖 → (𝑉) = (𝑉𝑖))
454453breq1d 4695 . . . . . . . . . . . . . . . . . . . 20 ( = 𝑖 → ((𝑉) < (𝑉‘(𝑙 + 1)) ↔ (𝑉𝑖) < (𝑉‘(𝑙 + 1))))
455452, 454anbi12d 747 . . . . . . . . . . . . . . . . . . 19 ( = 𝑖 → ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ↔ (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑙 + 1)))))
456453breq1d 4695 . . . . . . . . . . . . . . . . . . 19 ( = 𝑖 → ((𝑉) ≤ (𝑉𝑙) ↔ (𝑉𝑖) ≤ (𝑉𝑙)))
457455, 456imbi12d 333 . . . . . . . . . . . . . . . . . 18 ( = 𝑖 → (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → (𝑉) ≤ (𝑉𝑙)) ↔ ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑙 + 1))) → (𝑉𝑖) ≤ (𝑉𝑙))))
458457, 409chvarv 2299 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑙 + 1))) → (𝑉𝑖) ≤ (𝑉𝑙))
459449, 458chvarv 2299 . . . . . . . . . . . . . . . 16 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑘 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑘 + 1))) → (𝑉𝑖) ≤ (𝑉𝑘))
460413, 109, 440, 459syl21anc 1365 . . . . . . . . . . . . . . 15 (𝜒 → (𝑉𝑖) ≤ (𝑉𝑘))
461117, 421letri3d 10217 . . . . . . . . . . . . . . 15 (𝜒 → ((𝑉𝑘) = (𝑉𝑖) ↔ ((𝑉𝑘) ≤ (𝑉𝑖) ∧ (𝑉𝑖) ≤ (𝑉𝑘))))
462412, 460, 461mpbir2and 977 . . . . . . . . . . . . . 14 (𝜒 → (𝑉𝑘) = (𝑉𝑖))
4637, 2, 8fourierdlem34 40676 . . . . . . . . . . . . . . . 16 (𝜑𝑉:(0...𝑀)–1-1→ℝ)
464107, 463syl 17 . . . . . . . . . . . . . . 15 (𝜒𝑉:(0...𝑀)–1-1→ℝ)
465 f1fveq 6559 . . . . . . . . . . . . . . 15 ((𝑉:(0...𝑀)–1-1→ℝ ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑀))) → ((𝑉𝑘) = (𝑉𝑖) ↔ 𝑘 = 𝑖))
466464, 115, 172, 465syl12anc 1364 . . . . . . . . . . . . . 14 (𝜒 → ((𝑉𝑘) = (𝑉𝑖) ↔ 𝑘 = 𝑖))
467462, 466mpbid 222 . . . . . . . . . . . . 13 (𝜒𝑘 = 𝑖)
468104, 467sylbir 225 . . . . . . . . . . . 12 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑘 = 𝑖)
469468ex 449 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) → 𝑘 = 𝑖))
470 simpl 472 . . . . . . . . . . . . . 14 ((((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑘 = 𝑖) → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
471 fveq2 6229 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑖 → (𝑄𝑘) = (𝑄𝑖))
472 oveq1 6697 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑖 → (𝑘 + 1) = (𝑖 + 1))
473472fveq2d 6233 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑖 → (𝑄‘(𝑘 + 1)) = (𝑄‘(𝑖 + 1)))
474471, 473oveq12d 6708 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑖 → ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
475474eqcomd 2657 . . . . . . . . . . . . . . 15 (𝑘 = 𝑖 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
476475adantl 481 . . . . . . . . . . . . . 14 ((((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑘 = 𝑖) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
477470, 476sseqtrd 3674 . . . . . . . . . . . . 13 ((((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑘 = 𝑖) → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
478477ex 449 . . . . . . . . . . . 12 (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝑘 = 𝑖 → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))))
479478ad2antlr 763 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) → (𝑘 = 𝑖 → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))))
480469, 479impbid 202 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖))
481480ralrimiva 2995 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ∀𝑘 ∈ (0..^𝑀)(((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖))
482481ex 449 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ∀𝑘 ∈ (0..^𝑀)(((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖)))
483482reximdva 3046 . . . . . . 7 (𝜑 → (∃𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)∀𝑘 ∈ (0..^𝑀)(((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖)))
484103, 483mpd 15 . . . . . 6 (𝜑 → ∃𝑖 ∈ (0..^𝑀)∀𝑘 ∈ (0..^𝑀)(((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖))
485 reu6 3428 . . . . . 6 (∃!𝑘 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ ∃𝑖 ∈ (0..^𝑀)∀𝑘 ∈ (0..^𝑀)(((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖))
486484, 485sylibr 224 . . . . 5 (𝜑 → ∃!𝑘 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
487 fveq2 6229 . . . . . . . 8 (𝑖 = 𝑘 → (𝑄𝑖) = (𝑄𝑘))
488 oveq1 6697 . . . . . . . . 9 (𝑖 = 𝑘 → (𝑖 + 1) = (𝑘 + 1))
489488fveq2d 6233 . . . . . . . 8 (𝑖 = 𝑘 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑘 + 1)))
490487, 489oveq12d 6708 . . . . . . 7 (𝑖 = 𝑘 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
491490sseq2d 3666 . . . . . 6 (𝑖 = 𝑘 → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))))
492491cbvreuv 3203 . . . . 5 (∃!𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ ∃!𝑘 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
493486, 492sylibr 224 . . . 4 (𝜑 → ∃!𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
494 riotacl 6665 . . . 4 (∃!𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (0..^𝑀))
495493, 494syl 17 . . 3 (𝜑 → (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (0..^𝑀))
4961, 495syl5eqel 2734 . 2 (𝜑𝑈 ∈ (0..^𝑀))
4971eqcomi 2660 . . . 4 (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = 𝑈
498497a1i 11 . . 3 (𝜑 → (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = 𝑈)
499 fveq2 6229 . . . . . . 7 (𝑖 = 𝑈 → (𝑄𝑖) = (𝑄𝑈))
500 oveq1 6697 . . . . . . . 8 (𝑖 = 𝑈 → (𝑖 + 1) = (𝑈 + 1))
501500fveq2d 6233 . . . . . . 7 (𝑖 = 𝑈 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑈 + 1)))
502499, 501oveq12d 6708 . . . . . 6 (𝑖 = 𝑈 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1))))
503502sseq2d 3666 . . . . 5 (𝑖 = 𝑈 → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1)))))
504503riota2 6673 . . . 4 ((𝑈 ∈ (0..^𝑀) ∧ ∃!𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1))) ↔ (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = 𝑈))
505496, 493, 504syl2anc 694 . . 3 (𝜑 → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1))) ↔ (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = 𝑈))
506498, 505mpbird 247 . 2 (𝜑 → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1))))
507496, 506jca 553 1 (𝜑 → (𝑈 ∈ (0..^𝑀) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wral 2941  wrex 2942  ∃!wreu 2943  {crab 2945  cun 3605  cin 3606  wss 3607  {cpr 4212   class class class wbr 4685  cmpt 4762  ran crn 5144  cio 5887  wf 5922  1-1wf1 5923  1-1-ontowf1o 5925  cfv 5926   Isom wiso 5927  crio 6650  (class class class)co 6690  𝑚 cmap 7899  Fincfn 7997  supcsup 8387  cc 9972  cr 9973  0cc0 9974  1c1 9975   + caddc 9977  *cxr 10111   < clt 10112  cle 10113  cmin 10304  -cneg 10305  cn 11058  0cn0 11330  cz 11415  cuz 11725  (,)cioo 12213  [,]cicc 12216  ...cfz 12364  ..^cfzo 12504  #chash 13157  πcpi 14841
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053  ax-mulf 10054
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ioc 12218  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-seq 12842  df-exp 12901  df-fac 13101  df-bc 13130  df-hash 13158  df-shft 13851  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-limsup 14246  df-clim 14263  df-rlim 14264  df-sum 14461  df-ef 14842  df-sin 14844  df-cos 14845  df-pi 14847  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-mulr 16002  df-starv 16003  df-sca 16004  df-vsca 16005  df-ip 16006  df-tset 16007  df-ple 16008  df-ds 16011  df-unif 16012  df-hom 16013  df-cco 16014  df-rest 16130  df-topn 16131  df-0g 16149  df-gsum 16150  df-topgen 16151  df-pt 16152  df-prds 16155  df-xrs 16209  df-qtop 16214  df-imas 16215  df-xps 16217  df-mre 16293  df-mrc 16294  df-acs 16296  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-submnd 17383  df-mulg 17588  df-cntz 17796  df-cmn 18241  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-fbas 19791  df-fg 19792  df-cnfld 19795  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-cld 20871  df-ntr 20872  df-cls 20873  df-nei 20950  df-lp 20988  df-perf 20989  df-cn 21079  df-cnp 21080  df-haus 21167  df-tx 21413  df-hmeo 21606  df-fil 21697  df-fm 21789  df-flim 21790  df-flf 21791  df-xms 22172  df-ms 22173  df-tms 22174  df-cncf 22728  df-limc 23675  df-dv 23676
This theorem is referenced by:  fourierdlem86  40727  fourierdlem103  40744  fourierdlem104  40745
  Copyright terms: Public domain W3C validator