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 39680
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 10129 . . . . . . . 8 (𝜑𝐴𝐵)
7 fourierdlem50.p . . . . . . . . . . . . 13 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
8 fourierdlem50.v . . . . . . . . . . . . 13 (𝜑𝑉 ∈ (𝑃𝑀))
97, 2, 8fourierdlem15 39646 . . . . . . . . . . . 12 (𝜑𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
10 pire 24114 . . . . . . . . . . . . . . . 16 π ∈ ℝ
1110renegcli 10286 . . . . . . . . . . . . . . 15 -π ∈ ℝ
1211a1i 11 . . . . . . . . . . . . . 14 (𝜑 → -π ∈ ℝ)
13 fourierdlem50.xre . . . . . . . . . . . . . 14 (𝜑𝑋 ∈ ℝ)
1412, 13readdcld 10013 . . . . . . . . . . . . 13 (𝜑 → (-π + 𝑋) ∈ ℝ)
1510a1i 11 . . . . . . . . . . . . . 14 (𝜑 → π ∈ ℝ)
1615, 13readdcld 10013 . . . . . . . . . . . . 13 (𝜑 → (π + 𝑋) ∈ ℝ)
1714, 16iccssred 39138 . . . . . . . . . . . 12 (𝜑 → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
189, 17fssd 6014 . . . . . . . . . . 11 (𝜑𝑉:(0...𝑀)⟶ℝ)
1918ffvelrnda 6315 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑉𝑖) ∈ ℝ)
2013adantr 481 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℝ)
2119, 20resubcld 10402 . . . . . . . . 9 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) − 𝑋) ∈ ℝ)
22 fourierdlem50.q . . . . . . . . 9 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋))
2321, 22fmptd 6340 . . . . . . . 8 (𝜑𝑄:(0...𝑀)⟶ℝ)
2422a1i 11 . . . . . . . . . . 11 (𝜑𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋)))
25 fveq2 6148 . . . . . . . . . . . . 13 (𝑖 = 0 → (𝑉𝑖) = (𝑉‘0))
2625oveq1d 6619 . . . . . . . . . . . 12 (𝑖 = 0 → ((𝑉𝑖) − 𝑋) = ((𝑉‘0) − 𝑋))
2726adantl 482 . . . . . . . . . . 11 ((𝜑𝑖 = 0) → ((𝑉𝑖) − 𝑋) = ((𝑉‘0) − 𝑋))
28 nnssnn0 11239 . . . . . . . . . . . . . . 15 ℕ ⊆ ℕ0
2928a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ℕ ⊆ ℕ0)
30 nn0uz 11666 . . . . . . . . . . . . . 14 0 = (ℤ‘0)
3129, 30syl6sseq 3630 . . . . . . . . . . . . 13 (𝜑 → ℕ ⊆ (ℤ‘0))
3231, 2sseldd 3584 . . . . . . . . . . . 12 (𝜑𝑀 ∈ (ℤ‘0))
33 eluzfz1 12290 . . . . . . . . . . . 12 (𝑀 ∈ (ℤ‘0) → 0 ∈ (0...𝑀))
3432, 33syl 17 . . . . . . . . . . 11 (𝜑 → 0 ∈ (0...𝑀))
3518, 34ffvelrnd 6316 . . . . . . . . . . . 12 (𝜑 → (𝑉‘0) ∈ ℝ)
3635, 13resubcld 10402 . . . . . . . . . . 11 (𝜑 → ((𝑉‘0) − 𝑋) ∈ ℝ)
3724, 27, 34, 36fvmptd 6245 . . . . . . . . . 10 (𝜑 → (𝑄‘0) = ((𝑉‘0) − 𝑋))
387fourierdlem2 39633 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ → (𝑉 ∈ (𝑃𝑀) ↔ (𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))))
392, 38syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑉 ∈ (𝑃𝑀) ↔ (𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))))
408, 39mpbid 222 . . . . . . . . . . . . . 14 (𝜑 → (𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1)))))
4140simprd 479 . . . . . . . . . . . . 13 (𝜑 → (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))
4241simpld 475 . . . . . . . . . . . 12 (𝜑 → ((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)))
4342simpld 475 . . . . . . . . . . 11 (𝜑 → (𝑉‘0) = (-π + 𝑋))
4443oveq1d 6619 . . . . . . . . . 10 (𝜑 → ((𝑉‘0) − 𝑋) = ((-π + 𝑋) − 𝑋))
4512recnd 10012 . . . . . . . . . . 11 (𝜑 → -π ∈ ℂ)
4613recnd 10012 . . . . . . . . . . 11 (𝜑𝑋 ∈ ℂ)
4745, 46pncand 10337 . . . . . . . . . 10 (𝜑 → ((-π + 𝑋) − 𝑋) = -π)
4837, 44, 473eqtrd 2659 . . . . . . . . 9 (𝜑 → (𝑄‘0) = -π)
4912rexrd 10033 . . . . . . . . . 10 (𝜑 → -π ∈ ℝ*)
5015rexrd 10033 . . . . . . . . . 10 (𝜑 → π ∈ ℝ*)
51 fourierdlem50.ab . . . . . . . . . . 11 (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
523leidd 10538 . . . . . . . . . . . 12 (𝜑𝐴𝐴)
533, 4, 3, 52, 6eliccd 39137 . . . . . . . . . . 11 (𝜑𝐴 ∈ (𝐴[,]𝐵))
5451, 53sseldd 3584 . . . . . . . . . 10 (𝜑𝐴 ∈ (-π[,]π))
55 iccgelb 12172 . . . . . . . . . 10 ((-π ∈ ℝ* ∧ π ∈ ℝ*𝐴 ∈ (-π[,]π)) → -π ≤ 𝐴)
5649, 50, 54, 55syl3anc 1323 . . . . . . . . 9 (𝜑 → -π ≤ 𝐴)
5748, 56eqbrtrd 4635 . . . . . . . 8 (𝜑 → (𝑄‘0) ≤ 𝐴)
584leidd 10538 . . . . . . . . . . . 12 (𝜑𝐵𝐵)
593, 4, 4, 6, 58eliccd 39137 . . . . . . . . . . 11 (𝜑𝐵 ∈ (𝐴[,]𝐵))
6051, 59sseldd 3584 . . . . . . . . . 10 (𝜑𝐵 ∈ (-π[,]π))
61 iccleub 12171 . . . . . . . . . 10 ((-π ∈ ℝ* ∧ π ∈ ℝ*𝐵 ∈ (-π[,]π)) → 𝐵 ≤ π)
6249, 50, 60, 61syl3anc 1323 . . . . . . . . 9 (𝜑𝐵 ≤ π)
63 fveq2 6148 . . . . . . . . . . . . 13 (𝑖 = 𝑀 → (𝑉𝑖) = (𝑉𝑀))
6463oveq1d 6619 . . . . . . . . . . . 12 (𝑖 = 𝑀 → ((𝑉𝑖) − 𝑋) = ((𝑉𝑀) − 𝑋))
6564adantl 482 . . . . . . . . . . 11 ((𝜑𝑖 = 𝑀) → ((𝑉𝑖) − 𝑋) = ((𝑉𝑀) − 𝑋))
66 eluzfz2 12291 . . . . . . . . . . . 12 (𝑀 ∈ (ℤ‘0) → 𝑀 ∈ (0...𝑀))
6732, 66syl 17 . . . . . . . . . . 11 (𝜑𝑀 ∈ (0...𝑀))
6818, 67ffvelrnd 6316 . . . . . . . . . . . 12 (𝜑 → (𝑉𝑀) ∈ ℝ)
6968, 13resubcld 10402 . . . . . . . . . . 11 (𝜑 → ((𝑉𝑀) − 𝑋) ∈ ℝ)
7024, 65, 67, 69fvmptd 6245 . . . . . . . . . 10 (𝜑 → (𝑄𝑀) = ((𝑉𝑀) − 𝑋))
7142simprd 479 . . . . . . . . . . 11 (𝜑 → (𝑉𝑀) = (π + 𝑋))
7271oveq1d 6619 . . . . . . . . . 10 (𝜑 → ((𝑉𝑀) − 𝑋) = ((π + 𝑋) − 𝑋))
7315recnd 10012 . . . . . . . . . . 11 (𝜑 → π ∈ ℂ)
7473, 46pncand 10337 . . . . . . . . . 10 (𝜑 → ((π + 𝑋) − 𝑋) = π)
7570, 72, 743eqtrrd 2660 . . . . . . . . 9 (𝜑 → π = (𝑄𝑀))
7662, 75breqtrd 4639 . . . . . . . 8 (𝜑𝐵 ≤ (𝑄𝑀))
77 fourierdlem50.j . . . . . . . 8 (𝜑𝐽 ∈ (0..^𝑁))
78 fourierdlem50.t . . . . . . . 8 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))
79 prfi 8179 . . . . . . . . . . . 12 {𝐴, 𝐵} ∈ Fin
8079a1i 11 . . . . . . . . . . 11 (𝜑 → {𝐴, 𝐵} ∈ Fin)
81 fzfid 12712 . . . . . . . . . . . . 13 (𝜑 → (0...𝑀) ∈ Fin)
8222rnmptfi 38825 . . . . . . . . . . . . 13 ((0...𝑀) ∈ Fin → ran 𝑄 ∈ Fin)
8381, 82syl 17 . . . . . . . . . . . 12 (𝜑 → ran 𝑄 ∈ Fin)
84 infi 8128 . . . . . . . . . . . 12 (ran 𝑄 ∈ Fin → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
8583, 84syl 17 . . . . . . . . . . 11 (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin)
86 unfi 8171 . . . . . . . . . . 11 (({𝐴, 𝐵} ∈ Fin ∧ (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin) → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
8780, 85, 86syl2anc 692 . . . . . . . . . 10 (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin)
8878, 87syl5eqel 2702 . . . . . . . . 9 (𝜑𝑇 ∈ Fin)
893, 4jca 554 . . . . . . . . . . . 12 (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
90 prssg 4318 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
913, 4, 90syl2anc 692 . . . . . . . . . . . 12 (𝜑 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ))
9289, 91mpbid 222 . . . . . . . . . . 11 (𝜑 → {𝐴, 𝐵} ⊆ ℝ)
93 inss2 3812 . . . . . . . . . . . . 13 (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴(,)𝐵)
94 ioossre 12177 . . . . . . . . . . . . 13 (𝐴(,)𝐵) ⊆ ℝ
9593, 94sstri 3592 . . . . . . . . . . . 12 (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ
9695a1i 11 . . . . . . . . . . 11 (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ)
9792, 96unssd 3767 . . . . . . . . . 10 (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ ℝ)
9878, 97syl5eqss 3628 . . . . . . . . 9 (𝜑𝑇 ⊆ ℝ)
99 fourierdlem50.s . . . . . . . . 9 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇))
100 fourierdlem50.n . . . . . . . . 9 𝑁 = ((#‘𝑇) − 1)
10188, 98, 99, 100fourierdlem36 39667 . . . . . . . 8 (𝜑𝑆 Isom < , < ((0...𝑁), 𝑇))
102 eqid 2621 . . . . . . . 8 sup({𝑥 ∈ (0..^𝑀) ∣ (𝑄𝑥) ≤ (𝑆𝐽)}, ℝ, < ) = sup({𝑥 ∈ (0..^𝑀) ∣ (𝑄𝑥) ≤ (𝑆𝐽)}, ℝ, < )
1032, 3, 4, 6, 23, 57, 76, 77, 78, 101, 102fourierdlem20 39651 . . . . . . 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 805 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝜑)
107105, 106syl 17 . . . . . . . . . . . . . . . . 17 (𝜒𝜑)
108 simplr 791 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑘 ∈ (0..^𝑀))
109105, 108syl 17 . . . . . . . . . . . . . . . . 17 (𝜒𝑘 ∈ (0..^𝑀))
110107, 109jca 554 . . . . . . . . . . . . . . . 16 (𝜒 → (𝜑𝑘 ∈ (0..^𝑀)))
111 simp-4r 806 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑖 ∈ (0..^𝑀))
112105, 111syl 17 . . . . . . . . . . . . . . . 16 (𝜒𝑖 ∈ (0..^𝑀))
113 elfzofz 12426 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ (0..^𝑀) → 𝑘 ∈ (0...𝑀))
114113ad2antlr 762 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑘 ∈ (0...𝑀))
115105, 114syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜒𝑘 ∈ (0...𝑀))
116107, 18syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒𝑉:(0...𝑀)⟶ℝ)
117116, 115ffvelrnd 6316 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (𝑉𝑘) ∈ ℝ)
118107, 13syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜒𝑋 ∈ ℝ)
119117, 118resubcld 10402 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ((𝑉𝑘) − 𝑋) ∈ ℝ)
120 fveq2 6148 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 𝑘 → (𝑉𝑖) = (𝑉𝑘))
121120oveq1d 6619 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑘 → ((𝑉𝑖) − 𝑋) = ((𝑉𝑘) − 𝑋))
122121, 22fvmptg 6237 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ (0...𝑀) ∧ ((𝑉𝑘) − 𝑋) ∈ ℝ) → (𝑄𝑘) = ((𝑉𝑘) − 𝑋))
123115, 119, 122syl2anc 692 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑄𝑘) = ((𝑉𝑘) − 𝑋))
124123, 119eqeltrd 2698 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄𝑘) ∈ ℝ)
12523adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
126 fzofzp1 12506 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
127126adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
128125, 127ffvelrnd 6316 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
129107, 112, 128syl2anc 692 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℝ)
130 isof1o 6527 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑆 Isom < , < ((0...𝑁), 𝑇) → 𝑆:(0...𝑁)–1-1-onto𝑇)
131101, 130syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑆:(0...𝑁)–1-1-onto𝑇)
132 f1of 6094 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑆:(0...𝑁)–1-1-onto𝑇𝑆:(0...𝑁)⟶𝑇)
133131, 132syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑆:(0...𝑁)⟶𝑇)
134 fzofzp1 12506 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
13577, 134syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
136133, 135ffvelrnd 6316 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ 𝑇)
13798, 136sseldd 3584 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
138107, 137syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
139 elfzofz 12426 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
14077, 139syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐽 ∈ (0...𝑁))
141133, 140ffvelrnd 6316 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑆𝐽) ∈ 𝑇)
14298, 141sseldd 3584 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑆𝐽) ∈ ℝ)
143107, 142syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑆𝐽) ∈ ℝ)
144105simprd 479 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
145124rexrd 10033 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → (𝑄𝑘) ∈ ℝ*)
14623adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
147 fzofzp1 12506 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 ∈ (0..^𝑀) → (𝑘 + 1) ∈ (0...𝑀))
148147adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0..^𝑀)) → (𝑘 + 1) ∈ (0...𝑀))
149146, 148ffvelrnd 6316 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ (0..^𝑀)) → (𝑄‘(𝑘 + 1)) ∈ ℝ)
150149rexrd 10033 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (0..^𝑀)) → (𝑄‘(𝑘 + 1)) ∈ ℝ*)
151110, 150syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → (𝑄‘(𝑘 + 1)) ∈ ℝ*)
152143rexrd 10033 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → (𝑆𝐽) ∈ ℝ*)
153138rexrd 10033 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → (𝑆‘(𝐽 + 1)) ∈ ℝ*)
154 elfzoelz 12411 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
155154zred 11426 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℝ)
156155ltp1d 10898 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐽 ∈ (0..^𝑁) → 𝐽 < (𝐽 + 1))
15777, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐽 < (𝐽 + 1))
158 isoeq5 6525 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6530 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑆 Isom < , < ((0...𝑁), ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))) ∧ (𝐽 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝐽 < (𝐽 + 1) ↔ (𝑆𝐽) < (𝑆‘(𝐽 + 1))))
162160, 140, 135, 161syl12anc 1321 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐽 < (𝐽 + 1) ↔ (𝑆𝐽) < (𝑆‘(𝐽 + 1))))
163157, 162mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑆𝐽) < (𝑆‘(𝐽 + 1)))
164107, 163syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → (𝑆𝐽) < (𝑆‘(𝐽 + 1)))
165145, 151, 152, 153, 164ioossioobi 39154 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ ((𝑄𝑘) ≤ (𝑆𝐽) ∧ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑘 + 1)))))
166144, 165mpbid 222 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → ((𝑄𝑘) ≤ (𝑆𝐽) ∧ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑘 + 1))))
167166simpld 475 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑄𝑘) ≤ (𝑆𝐽))
168124, 143, 138, 167, 164lelttrd 10139 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑄𝑘) < (𝑆‘(𝐽 + 1)))
169 elfzofz 12426 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
170169ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑖 ∈ (0...𝑀))
171170ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑖 ∈ (0...𝑀))
172105, 171syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒𝑖 ∈ (0...𝑀))
173107, 172, 21syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜒 → ((𝑉𝑖) − 𝑋) ∈ ℝ)
17422fvmpt2 6248 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ (0...𝑀) ∧ ((𝑉𝑖) − 𝑋) ∈ ℝ) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
175172, 173, 174syl2anc 692 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
176175, 173eqeltrd 2698 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → (𝑄𝑖) ∈ ℝ)
177 simpllr 798 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
178105, 177syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
179176, 129, 143, 138, 164, 178fourierdlem10 39641 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ((𝑄𝑖) ≤ (𝑆𝐽) ∧ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑖 + 1))))
180179simprd 479 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑖 + 1)))
181124, 138, 129, 168, 180ltletrd 10141 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄𝑘) < (𝑄‘(𝑖 + 1)))
182124, 129, 118, 181ltadd2dd 10140 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + (𝑄𝑘)) < (𝑋 + (𝑄‘(𝑖 + 1))))
183123oveq2d 6620 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + (𝑄𝑘)) = (𝑋 + ((𝑉𝑘) − 𝑋)))
184107, 46syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜒𝑋 ∈ ℂ)
185117recnd 10012 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑉𝑘) ∈ ℂ)
186184, 185pncan3d 10339 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + ((𝑉𝑘) − 𝑋)) = (𝑉𝑘))
187183, 186eqtr2d 2656 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑉𝑘) = (𝑋 + (𝑄𝑘)))
188112, 126syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑖 + 1) ∈ (0...𝑀))
18918adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
190189, 127ffvelrnd 6316 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
191107, 112, 190syl2anc 692 . . . . . . . . . . . . . . . . . . . . . 22 (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℝ)
192191, 118resubcld 10402 . . . . . . . . . . . . . . . . . . . . 21 (𝜒 → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
193188, 192jca 554 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → ((𝑖 + 1) ∈ (0...𝑀) ∧ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ))
194 eleq1 2686 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑖 + 1) → (𝑘 ∈ (0...𝑀) ↔ (𝑖 + 1) ∈ (0...𝑀)))
195 fveq2 6148 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = (𝑖 + 1) → (𝑉𝑘) = (𝑉‘(𝑖 + 1)))
196195oveq1d 6619 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = (𝑖 + 1) → ((𝑉𝑘) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
197196eleq1d 2683 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑖 + 1) → (((𝑉𝑘) − 𝑋) ∈ ℝ ↔ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ))
198194, 197anbi12d 746 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = (𝑖 + 1) → ((𝑘 ∈ (0...𝑀) ∧ ((𝑉𝑘) − 𝑋) ∈ ℝ) ↔ ((𝑖 + 1) ∈ (0...𝑀) ∧ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)))
199 fveq2 6148 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑖 + 1) → (𝑄𝑘) = (𝑄‘(𝑖 + 1)))
200199, 196eqeq12d 2636 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = (𝑖 + 1) → ((𝑄𝑘) = ((𝑉𝑘) − 𝑋) ↔ (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋)))
201198, 200imbi12d 334 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = (𝑖 + 1) → (((𝑘 ∈ (0...𝑀) ∧ ((𝑉𝑘) − 𝑋) ∈ ℝ) → (𝑄𝑘) = ((𝑉𝑘) − 𝑋)) ↔ (((𝑖 + 1) ∈ (0...𝑀) ∧ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))))
202201, 122vtoclg 3252 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 + 1) ∈ (0...𝑀) → (((𝑖 + 1) ∈ (0...𝑀) ∧ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋)))
203188, 193, 202sylc 65 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
204203oveq2d 6620 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)))
205191recnd 10012 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℂ)
206184, 205pncan3d 10339 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)) = (𝑉‘(𝑖 + 1)))
207204, 206eqtr2d 2656 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑉‘(𝑖 + 1)) = (𝑋 + (𝑄‘(𝑖 + 1))))
208182, 187, 2073brtr4d 4645 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑉𝑘) < (𝑉‘(𝑖 + 1)))
209 eleq1 2686 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑖 → (𝑙 ∈ (0..^𝑀) ↔ 𝑖 ∈ (0..^𝑀)))
210209anbi2d 739 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑖 → (((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ↔ ((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (0..^𝑀))))
211 oveq1 6611 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑖 → (𝑙 + 1) = (𝑖 + 1))
212211fveq2d 6152 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑖 → (𝑉‘(𝑙 + 1)) = (𝑉‘(𝑖 + 1)))
213212breq2d 4625 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑖 → ((𝑉𝑘) < (𝑉‘(𝑙 + 1)) ↔ (𝑉𝑘) < (𝑉‘(𝑖 + 1))))
214210, 213anbi12d 746 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑖 → ((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑙 + 1))) ↔ (((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑖 + 1)))))
215 fveq2 6148 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑖 → (𝑉𝑙) = (𝑉𝑖))
216215breq2d 4625 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑖 → ((𝑉𝑘) ≤ (𝑉𝑙) ↔ (𝑉𝑘) ≤ (𝑉𝑖)))
217214, 216imbi12d 334 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑖 → (((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑙 + 1))) → (𝑉𝑘) ≤ (𝑉𝑙)) ↔ ((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑖 + 1))) → (𝑉𝑘) ≤ (𝑉𝑖))))
218 eleq1 2686 . . . . . . . . . . . . . . . . . . . . . 22 ( = 𝑘 → ( ∈ (0..^𝑀) ↔ 𝑘 ∈ (0..^𝑀)))
219218anbi2d 739 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝑘 → ((𝜑 ∈ (0..^𝑀)) ↔ (𝜑𝑘 ∈ (0..^𝑀))))
220219anbi1d 740 . . . . . . . . . . . . . . . . . . . 20 ( = 𝑘 → (((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ↔ ((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀))))
221 fveq2 6148 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝑘 → (𝑉) = (𝑉𝑘))
222221breq1d 4623 . . . . . . . . . . . . . . . . . . . 20 ( = 𝑘 → ((𝑉) < (𝑉‘(𝑙 + 1)) ↔ (𝑉𝑘) < (𝑉‘(𝑙 + 1))))
223220, 222anbi12d 746 . . . . . . . . . . . . . . . . . . 19 ( = 𝑘 → ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ↔ (((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑙 + 1)))))
224221breq1d 4623 . . . . . . . . . . . . . . . . . . 19 ( = 𝑘 → ((𝑉) ≤ (𝑉𝑙) ↔ (𝑉𝑘) ≤ (𝑉𝑙)))
225223, 224imbi12d 334 . . . . . . . . . . . . . . . . . 18 ( = 𝑘 → (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → (𝑉) ≤ (𝑉𝑙)) ↔ ((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑙 + 1))) → (𝑉𝑘) ≤ (𝑉𝑙))))
226 elfzoelz 12411 . . . . . . . . . . . . . . . . . . . . 21 ( ∈ (0..^𝑀) → ∈ ℤ)
227226ad3antlr 766 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → ∈ ℤ)
228 elfzoelz 12411 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 ∈ (0..^𝑀) → 𝑙 ∈ ℤ)
229228ad2antlr 762 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → 𝑙 ∈ ℤ)
230 simplr 791 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ ¬ < (𝑙 + 1)) → (𝑉) < (𝑉‘(𝑙 + 1)))
23118adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑙 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
232 fzofzp1 12506 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (0..^𝑀) → (𝑙 + 1) ∈ (0...𝑀))
233232adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑙 ∈ (0..^𝑀)) → (𝑙 + 1) ∈ (0...𝑀))
234231, 233ffvelrnd 6316 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑙 ∈ (0..^𝑀)) → (𝑉‘(𝑙 + 1)) ∈ ℝ)
235234adantlr 750 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) → (𝑉‘(𝑙 + 1)) ∈ ℝ)
236235adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → (𝑉‘(𝑙 + 1)) ∈ ℝ)
23718adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
238 elfzofz 12426 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ( ∈ (0..^𝑀) → ∈ (0...𝑀))
239238adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∈ (0..^𝑀)) → ∈ (0...𝑀))
240237, 239ffvelrnd 6316 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∈ (0..^𝑀)) → (𝑉) ∈ ℝ)
241240ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → (𝑉) ∈ ℝ)
242228zred 11426 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (0..^𝑀) → 𝑙 ∈ ℝ)
243 peano2re 10153 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ ℝ → (𝑙 + 1) ∈ ℝ)
244242, 243syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑙 ∈ (0..^𝑀) → (𝑙 + 1) ∈ ℝ)
245244ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → (𝑙 + 1) ∈ ℝ)
246226zred 11426 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ( ∈ (0..^𝑀) → ∈ ℝ)
247246ad3antlr 766 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → ∈ ℝ)
248 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → ¬ < (𝑙 + 1))
249245, 247, 248nltled 10131 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → (𝑙 + 1) ≤ )
250228peano2zd 11429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (0..^𝑀) → (𝑙 + 1) ∈ ℤ)
251250ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → (𝑙 + 1) ∈ ℤ)
252226ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → ∈ ℤ)
253 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → (𝑙 + 1) ≤ )
254 eluz2 11637 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ( ∈ (ℤ‘(𝑙 + 1)) ↔ ((𝑙 + 1) ∈ ℤ ∧ ∈ ℤ ∧ (𝑙 + 1) ≤ ))
255251, 252, 253, 254syl3anbrc 1244 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → ∈ (ℤ‘(𝑙 + 1)))
256255adantlll 753 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → ∈ (ℤ‘(𝑙 + 1)))
257 simplll 797 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝜑)
258 0zd 11333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 ∈ ℤ)
259 elfzoel2 12410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ( ∈ (0..^𝑀) → 𝑀 ∈ ℤ)
260259ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑀 ∈ ℤ)
261 elfzelz 12284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ ((𝑙 + 1)...) → 𝑖 ∈ ℤ)
262261adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 ∈ ℤ)
263258, 260, 2623jca 1240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ))
264 0red 9985 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 ∈ ℝ)
265261zred 11426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑖 ∈ ((𝑙 + 1)...) → 𝑖 ∈ ℝ)
266265adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 ∈ ℝ)
267242adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑙 ∈ ℝ)
268 elfzole1 12419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑙 ∈ (0..^𝑀) → 0 ≤ 𝑙)
269268adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 ≤ 𝑙)
270267, 243syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → (𝑙 + 1) ∈ ℝ)
271267ltp1d 10898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑙 < (𝑙 + 1))
272 elfzle1 12286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑖 ∈ ((𝑙 + 1)...) → (𝑙 + 1) ≤ 𝑖)
273272adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → (𝑙 + 1) ≤ 𝑖)
274267, 270, 266, 271, 273ltletrd 10141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑙 < 𝑖)
275264, 267, 266, 269, 274lelttrd 10139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 < 𝑖)
276264, 266, 275ltled 10129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 ≤ 𝑖)
277276adantll 749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 0 ≤ 𝑖)
278265adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 ∈ ℝ)
279259zred 11426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( ∈ (0..^𝑀) → 𝑀 ∈ ℝ)
280279adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑀 ∈ ℝ)
281246adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → ∈ ℝ)
282 elfzle2 12287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑖 ∈ ((𝑙 + 1)...) → 𝑖)
283282adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖)
284 elfzolt2 12420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ( ∈ (0..^𝑀) → < 𝑀)
285284adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → < 𝑀)
286278, 281, 280, 283, 285lelttrd 10139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 < 𝑀)
287278, 280, 286ltled 10129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖𝑀)
288287adantlr 750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖𝑀)
289263, 277, 288jca32 557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (0 ≤ 𝑖𝑖𝑀)))
290 elfz2 12275 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑖 ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (0 ≤ 𝑖𝑖𝑀)))
291289, 290sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 ∈ (0...𝑀))
292291adantlll 753 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → 𝑖 ∈ (0...𝑀))
293257, 292, 19syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → (𝑉𝑖) ∈ ℝ)
294293adantlr 750 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) ∧ 𝑖 ∈ ((𝑙 + 1)...)) → (𝑉𝑖) ∈ ℝ)
295 simplll 797 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝜑)
296 0zd 11333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 0 ∈ ℤ)
297 elfzelz 12284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 ∈ ((𝑙 + 1)...( − 1)) → 𝑖 ∈ ℤ)
298297adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ ℤ)
299 0red 9985 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 0 ∈ ℝ)
300298zred 11426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ ℝ)
301242adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑙 ∈ ℝ)
302268adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 0 ≤ 𝑙)
303301, 243syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → (𝑙 + 1) ∈ ℝ)
304301ltp1d 10898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑙 < (𝑙 + 1))
305 elfzle1 12286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑖 ∈ ((𝑙 + 1)...( − 1)) → (𝑙 + 1) ≤ 𝑖)
306305adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → (𝑙 + 1) ≤ 𝑖)
307301, 303, 300, 304, 306ltletrd 10141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑙 < 𝑖)
308299, 301, 300, 302, 307lelttrd 10139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 0 < 𝑖)
309299, 300, 308ltled 10129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 0 ≤ 𝑖)
310 eluz2 11637 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (ℤ‘0) ↔ (0 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 0 ≤ 𝑖))
311296, 298, 309, 310syl3anbrc 1244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ (ℤ‘0))
312311adantll 749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ (ℤ‘0))
313 elfzoel2 12410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑙 ∈ (0..^𝑀) → 𝑀 ∈ ℤ)
314313ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑀 ∈ ℤ)
315297zred 11426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ ((𝑙 + 1)...( − 1)) → 𝑖 ∈ ℝ)
316315adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ ℝ)
317 peano2rem 10292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( ∈ ℝ → ( − 1) ∈ ℝ)
318246, 317syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ( ∈ (0..^𝑀) → ( − 1) ∈ ℝ)
319318adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → ( − 1) ∈ ℝ)
320279adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑀 ∈ ℝ)
321 elfzle2 12287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ ((𝑙 + 1)...( − 1)) → 𝑖 ≤ ( − 1))
322321adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ≤ ( − 1))
323246ltm1d 10900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ( ∈ (0..^𝑀) → ( − 1) < )
324318, 246, 279, 323, 284lttrd 10142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ( ∈ (0..^𝑀) → ( − 1) < 𝑀)
325324adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → ( − 1) < 𝑀)
326316, 319, 320, 322, 325lelttrd 10139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 < 𝑀)
327326adantll 749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 < 𝑀)
328327adantlr 750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 < 𝑀)
329 elfzo2 12414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑖 ∈ (0..^𝑀) ↔ (𝑖 ∈ (ℤ‘0) ∧ 𝑀 ∈ ℤ ∧ 𝑖 < 𝑀))
330312, 314, 328, 329syl3anbrc 1244 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → 𝑖 ∈ (0..^𝑀))
331169, 19sylan2 491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ∈ ℝ)
33241simprd 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1)))
333332r19.21bi 2927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) < (𝑉‘(𝑖 + 1)))
334331, 190, 333ltled 10129 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ≤ (𝑉‘(𝑖 + 1)))
335295, 330, 334syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → (𝑉𝑖) ≤ (𝑉‘(𝑖 + 1)))
336335adantlr 750 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) ∧ 𝑖 ∈ ((𝑙 + 1)...( − 1))) → (𝑉𝑖) ≤ (𝑉‘(𝑖 + 1)))
337256, 294, 336monoord 12771 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ) → (𝑉‘(𝑙 + 1)) ≤ (𝑉))
338249, 337syldan 487 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → (𝑉‘(𝑙 + 1)) ≤ (𝑉))
339236, 241, 338lensymd 10132 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ < (𝑙 + 1)) → ¬ (𝑉) < (𝑉‘(𝑙 + 1)))
340339adantlr 750 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ ¬ < (𝑙 + 1)) → ¬ (𝑉) < (𝑉‘(𝑙 + 1)))
341230, 340condan 834 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → < (𝑙 + 1))
342 zleltp1 11372 . . . . . . . . . . . . . . . . . . . . . 22 (( ∈ ℤ ∧ 𝑙 ∈ ℤ) → (𝑙 < (𝑙 + 1)))
343227, 229, 342syl2anc 692 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → (𝑙 < (𝑙 + 1)))
344341, 343mpbird 247 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → 𝑙)
345 eluz2 11637 . . . . . . . . . . . . . . . . . . . 20 (𝑙 ∈ (ℤ) ↔ ( ∈ ℤ ∧ 𝑙 ∈ ℤ ∧ 𝑙))
346227, 229, 344, 345syl3anbrc 1244 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → 𝑙 ∈ (ℤ))
34718ad3antrrr 765 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑉:(0...𝑀)⟶ℝ)
348 0zd 11333 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 0 ∈ ℤ)
349259ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑀 ∈ ℤ)
350 elfzelz 12284 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (...𝑙) → 𝑖 ∈ ℤ)
351350adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 ∈ ℤ)
352348, 349, 3513jca 1240 . . . . . . . . . . . . . . . . . . . . . . . 24 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ))
353 0red 9985 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 0 ∈ ℝ)
354246adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → ∈ ℝ)
355350zred 11426 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (...𝑙) → 𝑖 ∈ ℝ)
356355adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 ∈ ℝ)
357 elfzole1 12419 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ( ∈ (0..^𝑀) → 0 ≤ )
358357adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 0 ≤ )
359 elfzle1 12286 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (...𝑙) → 𝑖)
360359adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖)
361353, 354, 356, 358, 360letrd 10138 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 0 ≤ 𝑖)
362361adantlr 750 . . . . . . . . . . . . . . . . . . . . . . . 24 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 0 ≤ 𝑖)
363355adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 ∈ ℝ)
364313zred 11426 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑙 ∈ (0..^𝑀) → 𝑀 ∈ ℝ)
365364adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑀 ∈ ℝ)
366242adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑙 ∈ ℝ)
367 elfzle2 12287 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ (...𝑙) → 𝑖𝑙)
368367adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖𝑙)
369 elfzolt2 12420 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑙 ∈ (0..^𝑀) → 𝑙 < 𝑀)
370369adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑙 < 𝑀)
371363, 366, 365, 368, 370lelttrd 10139 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 < 𝑀)
372363, 365, 371ltled 10129 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...𝑙)) → 𝑖𝑀)
373372adantll 749 . . . . . . . . . . . . . . . . . . . . . . . 24 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑖𝑀)
374352, 362, 373jca32 557 . . . . . . . . . . . . . . . . . . . . . . 23 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (0 ≤ 𝑖𝑖𝑀)))
375374, 290sylibr 224 . . . . . . . . . . . . . . . . . . . . . 22 ((( ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 ∈ (0...𝑀))
376375adantlll 753 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → 𝑖 ∈ (0...𝑀))
377347, 376ffvelrnd 6316 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...𝑙)) → (𝑉𝑖) ∈ ℝ)
378377adantlr 750 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...𝑙)) → (𝑉𝑖) ∈ ℝ)
379 simp-4l 805 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝜑)
380 0zd 11333 . . . . . . . . . . . . . . . . . . . . . . . 24 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 0 ∈ ℤ)
381 elfzelz 12284 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ (...(𝑙 − 1)) → 𝑖 ∈ ℤ)
382381adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ ℤ)
383 0red 9985 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 0 ∈ ℝ)
384246adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → ∈ ℝ)
385382zred 11426 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ ℝ)
386357adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 0 ≤ )
387 elfzle1 12286 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (...(𝑙 − 1)) → 𝑖)
388387adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖)
389383, 384, 385, 386, 388letrd 10138 . . . . . . . . . . . . . . . . . . . . . . . 24 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 0 ≤ 𝑖)
390380, 382, 389, 310syl3anbrc 1244 . . . . . . . . . . . . . . . . . . . . . . 23 (( ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ (ℤ‘0))
391390adantll 749 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ (ℤ‘0))
392391ad4ant14 1290 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ (ℤ‘0))
393313ad3antlr 766 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑀 ∈ ℤ)
394381zred 11426 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ (...(𝑙 − 1)) → 𝑖 ∈ ℝ)
395394adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ ℝ)
396242adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑙 ∈ ℝ)
397364adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑀 ∈ ℝ)
398 elfzle2 12287 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (...(𝑙 − 1)) → 𝑖 ≤ (𝑙 − 1))
399398adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ≤ (𝑙 − 1))
400 zltlem1 11374 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑖 ∈ ℤ ∧ 𝑙 ∈ ℤ) → (𝑖 < 𝑙𝑖 ≤ (𝑙 − 1)))
401381, 228, 400syl2anr 495 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → (𝑖 < 𝑙𝑖 ≤ (𝑙 − 1)))
402399, 401mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 < 𝑙)
403369adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑙 < 𝑀)
404395, 396, 397, 402, 403lttrd 10142 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 < 𝑀)
405404adantll 749 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 < 𝑀)
406405adantlr 750 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 < 𝑀)
407392, 393, 406, 329syl3anbrc 1244 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → 𝑖 ∈ (0..^𝑀))
408379, 407, 334syl2anc 692 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (...(𝑙 − 1))) → (𝑉𝑖) ≤ (𝑉‘(𝑖 + 1)))
409346, 378, 408monoord 12771 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → (𝑉) ≤ (𝑉𝑙))
410225, 409chvarv 2262 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑙 + 1))) → (𝑉𝑘) ≤ (𝑉𝑙))
411217, 410chvarv 2262 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉𝑘) < (𝑉‘(𝑖 + 1))) → (𝑉𝑘) ≤ (𝑉𝑖))
412110, 112, 208, 411syl21anc 1322 . . . . . . . . . . . . . . 15 (𝜒 → (𝑉𝑘) ≤ (𝑉𝑖))
413107, 112jca 554 . . . . . . . . . . . . . . . 16 (𝜒 → (𝜑𝑖 ∈ (0..^𝑀)))
414110, 149syl 17 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄‘(𝑘 + 1)) ∈ ℝ)
415179simpld 475 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑄𝑖) ≤ (𝑆𝐽))
416176, 143, 138, 415, 164lelttrd 10139 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑄𝑖) < (𝑆‘(𝐽 + 1)))
417166simprd 479 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑘 + 1)))
418176, 138, 414, 416, 417ltletrd 10141 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑄𝑖) < (𝑄‘(𝑘 + 1)))
419176, 414, 118, 418ltadd2dd 10140 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑋 + (𝑄𝑖)) < (𝑋 + (𝑄‘(𝑘 + 1))))
420175oveq2d 6620 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + (𝑄𝑖)) = (𝑋 + ((𝑉𝑖) − 𝑋)))
421107, 172, 19syl2anc 692 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑉𝑖) ∈ ℝ)
422421recnd 10012 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑉𝑖) ∈ ℂ)
423184, 422pncan3d 10339 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + ((𝑉𝑖) − 𝑋)) = (𝑉𝑖))
424420, 423eqtr2d 2656 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑉𝑖) = (𝑋 + (𝑄𝑖)))
42522a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0..^𝑀)) → 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋)))
426 fveq2 6148 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = (𝑘 + 1) → (𝑉𝑖) = (𝑉‘(𝑘 + 1)))
427426oveq1d 6619 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = (𝑘 + 1) → ((𝑉𝑖) − 𝑋) = ((𝑉‘(𝑘 + 1)) − 𝑋))
428427adantl 482 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0..^𝑀)) ∧ 𝑖 = (𝑘 + 1)) → ((𝑉𝑖) − 𝑋) = ((𝑉‘(𝑘 + 1)) − 𝑋))
42918adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
430429, 148ffvelrnd 6316 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (0..^𝑀)) → (𝑉‘(𝑘 + 1)) ∈ ℝ)
43113adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
432430, 431resubcld 10402 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0..^𝑀)) → ((𝑉‘(𝑘 + 1)) − 𝑋) ∈ ℝ)
433425, 428, 148, 432fvmptd 6245 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0..^𝑀)) → (𝑄‘(𝑘 + 1)) = ((𝑉‘(𝑘 + 1)) − 𝑋))
434107, 109, 433syl2anc 692 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑄‘(𝑘 + 1)) = ((𝑉‘(𝑘 + 1)) − 𝑋))
435434oveq2d 6620 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + (𝑄‘(𝑘 + 1))) = (𝑋 + ((𝑉‘(𝑘 + 1)) − 𝑋)))
436110, 430syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜒 → (𝑉‘(𝑘 + 1)) ∈ ℝ)
437436recnd 10012 . . . . . . . . . . . . . . . . . . 19 (𝜒 → (𝑉‘(𝑘 + 1)) ∈ ℂ)
438184, 437pncan3d 10339 . . . . . . . . . . . . . . . . . 18 (𝜒 → (𝑋 + ((𝑉‘(𝑘 + 1)) − 𝑋)) = (𝑉‘(𝑘 + 1)))
439435, 438eqtr2d 2656 . . . . . . . . . . . . . . . . 17 (𝜒 → (𝑉‘(𝑘 + 1)) = (𝑋 + (𝑄‘(𝑘 + 1))))
440419, 424, 4393brtr4d 4645 . . . . . . . . . . . . . . . 16 (𝜒 → (𝑉𝑖) < (𝑉‘(𝑘 + 1)))
441 eleq1 2686 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑘 → (𝑙 ∈ (0..^𝑀) ↔ 𝑘 ∈ (0..^𝑀)))
442441anbi2d 739 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑘 → (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ↔ ((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑘 ∈ (0..^𝑀))))
443 oveq1 6611 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑘 → (𝑙 + 1) = (𝑘 + 1))
444443fveq2d 6152 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑘 → (𝑉‘(𝑙 + 1)) = (𝑉‘(𝑘 + 1)))
445444breq2d 4625 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑘 → ((𝑉𝑖) < (𝑉‘(𝑙 + 1)) ↔ (𝑉𝑖) < (𝑉‘(𝑘 + 1))))
446442, 445anbi12d 746 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑘 → ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑙 + 1))) ↔ (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑘 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑘 + 1)))))
447 fveq2 6148 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑘 → (𝑉𝑙) = (𝑉𝑘))
448447breq2d 4625 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑘 → ((𝑉𝑖) ≤ (𝑉𝑙) ↔ (𝑉𝑖) ≤ (𝑉𝑘)))
449446, 448imbi12d 334 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑘 → (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑙 + 1))) → (𝑉𝑖) ≤ (𝑉𝑙)) ↔ ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑘 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑘 + 1))) → (𝑉𝑖) ≤ (𝑉𝑘))))
450 eleq1 2686 . . . . . . . . . . . . . . . . . . . . . 22 ( = 𝑖 → ( ∈ (0..^𝑀) ↔ 𝑖 ∈ (0..^𝑀)))
451450anbi2d 739 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝑖 → ((𝜑 ∈ (0..^𝑀)) ↔ (𝜑𝑖 ∈ (0..^𝑀))))
452451anbi1d 740 . . . . . . . . . . . . . . . . . . . 20 ( = 𝑖 → (((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ↔ ((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀))))
453 fveq2 6148 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝑖 → (𝑉) = (𝑉𝑖))
454453breq1d 4623 . . . . . . . . . . . . . . . . . . . 20 ( = 𝑖 → ((𝑉) < (𝑉‘(𝑙 + 1)) ↔ (𝑉𝑖) < (𝑉‘(𝑙 + 1))))
455452, 454anbi12d 746 . . . . . . . . . . . . . . . . . . 19 ( = 𝑖 → ((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) ↔ (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑙 + 1)))))
456453breq1d 4623 . . . . . . . . . . . . . . . . . . 19 ( = 𝑖 → ((𝑉) ≤ (𝑉𝑙) ↔ (𝑉𝑖) ≤ (𝑉𝑙)))
457455, 456imbi12d 334 . . . . . . . . . . . . . . . . . 18 ( = 𝑖 → (((((𝜑 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉) < (𝑉‘(𝑙 + 1))) → (𝑉) ≤ (𝑉𝑙)) ↔ ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑙 + 1))) → (𝑉𝑖) ≤ (𝑉𝑙))))
458457, 409chvarv 2262 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑙 + 1))) → (𝑉𝑖) ≤ (𝑉𝑙))
459449, 458chvarv 2262 . . . . . . . . . . . . . . . 16 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑘 ∈ (0..^𝑀)) ∧ (𝑉𝑖) < (𝑉‘(𝑘 + 1))) → (𝑉𝑖) ≤ (𝑉𝑘))
460413, 109, 440, 459syl21anc 1322 . . . . . . . . . . . . . . 15 (𝜒 → (𝑉𝑖) ≤ (𝑉𝑘))
461117, 421letri3d 10123 . . . . . . . . . . . . . . 15 (𝜒 → ((𝑉𝑘) = (𝑉𝑖) ↔ ((𝑉𝑘) ≤ (𝑉𝑖) ∧ (𝑉𝑖) ≤ (𝑉𝑘))))
462412, 460, 461mpbir2and 956 . . . . . . . . . . . . . 14 (𝜒 → (𝑉𝑘) = (𝑉𝑖))
4637, 2, 8fourierdlem34 39665 . . . . . . . . . . . . . . . 16 (𝜑𝑉:(0...𝑀)–1-1→ℝ)
464107, 463syl 17 . . . . . . . . . . . . . . 15 (𝜒𝑉:(0...𝑀)–1-1→ℝ)
465 f1fveq 6473 . . . . . . . . . . . . . . 15 ((𝑉:(0...𝑀)–1-1→ℝ ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑀))) → ((𝑉𝑘) = (𝑉𝑖) ↔ 𝑘 = 𝑖))
466464, 115, 172, 465syl12anc 1321 . . . . . . . . . . . . . 14 (𝜒 → ((𝑉𝑘) = (𝑉𝑖) ↔ 𝑘 = 𝑖))
467462, 466mpbid 222 . . . . . . . . . . . . 13 (𝜒𝑘 = 𝑖)
468104, 467sylbir 225 . . . . . . . . . . . 12 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑘 = 𝑖)
469468ex 450 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) → 𝑘 = 𝑖))
470 simpl 473 . . . . . . . . . . . . . 14 ((((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑘 = 𝑖) → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
471 fveq2 6148 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑖 → (𝑄𝑘) = (𝑄𝑖))
472 oveq1 6611 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑖 → (𝑘 + 1) = (𝑖 + 1))
473472fveq2d 6152 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑖 → (𝑄‘(𝑘 + 1)) = (𝑄‘(𝑖 + 1)))
474471, 473oveq12d 6622 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑖 → ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
475474eqcomd 2627 . . . . . . . . . . . . . . 15 (𝑘 = 𝑖 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
476475adantl 482 . . . . . . . . . . . . . 14 ((((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑘 = 𝑖) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
477470, 476sseqtrd 3620 . . . . . . . . . . . . 13 ((((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑘 = 𝑖) → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
478477ex 450 . . . . . . . . . . . 12 (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝑘 = 𝑖 → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))))
479478ad2antlr 762 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) → (𝑘 = 𝑖 → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))))
480469, 479impbid 202 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖))
481480ralrimiva 2960 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ∀𝑘 ∈ (0..^𝑀)(((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖))
482481ex 450 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ∀𝑘 ∈ (0..^𝑀)(((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖)))
483482reximdva 3011 . . . . . . 7 (𝜑 → (∃𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)∀𝑘 ∈ (0..^𝑀)(((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖)))
484103, 483mpd 15 . . . . . 6 (𝜑 → ∃𝑖 ∈ (0..^𝑀)∀𝑘 ∈ (0..^𝑀)(((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖))
485 reu6 3377 . . . . . 6 (∃!𝑘 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ ∃𝑖 ∈ (0..^𝑀)∀𝑘 ∈ (0..^𝑀)(((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖))
486484, 485sylibr 224 . . . . 5 (𝜑 → ∃!𝑘 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
487 fveq2 6148 . . . . . . . 8 (𝑖 = 𝑘 → (𝑄𝑖) = (𝑄𝑘))
488 oveq1 6611 . . . . . . . . 9 (𝑖 = 𝑘 → (𝑖 + 1) = (𝑘 + 1))
489488fveq2d 6152 . . . . . . . 8 (𝑖 = 𝑘 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑘 + 1)))
490487, 489oveq12d 6622 . . . . . . 7 (𝑖 = 𝑘 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
491490sseq2d 3612 . . . . . 6 (𝑖 = 𝑘 → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1)))))
492491cbvreuv 3161 . . . . 5 (∃!𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ ∃!𝑘 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑘)(,)(𝑄‘(𝑘 + 1))))
493486, 492sylibr 224 . . . 4 (𝜑 → ∃!𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
494 riotacl 6579 . . . 4 (∃!𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (0..^𝑀))
495493, 494syl 17 . . 3 (𝜑 → (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (0..^𝑀))
4961, 495syl5eqel 2702 . 2 (𝜑𝑈 ∈ (0..^𝑀))
4971eqcomi 2630 . . . 4 (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = 𝑈
498497a1i 11 . . 3 (𝜑 → (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = 𝑈)
499 fveq2 6148 . . . . . . 7 (𝑖 = 𝑈 → (𝑄𝑖) = (𝑄𝑈))
500 oveq1 6611 . . . . . . . 8 (𝑖 = 𝑈 → (𝑖 + 1) = (𝑈 + 1))
501500fveq2d 6152 . . . . . . 7 (𝑖 = 𝑈 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑈 + 1)))
502499, 501oveq12d 6622 . . . . . 6 (𝑖 = 𝑈 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1))))
503502sseq2d 3612 . . . . 5 (𝑖 = 𝑈 → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1)))))
504503riota2 6587 . . . 4 ((𝑈 ∈ (0..^𝑀) ∧ ∃!𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1))) ↔ (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = 𝑈))
505496, 493, 504syl2anc 692 . . 3 (𝜑 → (((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1))) ↔ (𝑖 ∈ (0..^𝑀)((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = 𝑈))
506498, 505mpbird 247 . 2 (𝜑 → ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1))))
507496, 506jca 554 1 (𝜑 → (𝑈 ∈ (0..^𝑀) ∧ ((𝑆𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄𝑈)(,)(𝑄‘(𝑈 + 1)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wral 2907  wrex 2908  ∃!wreu 2909  {crab 2911  cun 3553  cin 3554  wss 3555  {cpr 4150   class class class wbr 4613  cmpt 4673  ran crn 5075  cio 5808  wf 5843  1-1wf1 5844  1-1-ontowf1o 5846  cfv 5847   Isom wiso 5848  crio 6564  (class class class)co 6604  𝑚 cmap 7802  Fincfn 7899  supcsup 8290  cc 9878  cr 9879  0cc0 9880  1c1 9881   + caddc 9883  *cxr 10017   < clt 10018  cle 10019  cmin 10210  -cneg 10211  cn 10964  0cn0 11236  cz 11321  cuz 11631  (,)cioo 12117  [,]cicc 12120  ...cfz 12268  ..^cfzo 12406  #chash 13057  πcpi 14722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-inf2 8482  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957  ax-pre-sup 9958  ax-addf 9959  ax-mulf 9960
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-iin 4488  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-of 6850  df-om 7013  df-1st 7113  df-2nd 7114  df-supp 7241  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-2o 7506  df-oadd 7509  df-er 7687  df-map 7804  df-pm 7805  df-ixp 7853  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-fsupp 8220  df-fi 8261  df-sup 8292  df-inf 8293  df-oi 8359  df-card 8709  df-cda 8934  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-div 10629  df-nn 10965  df-2 11023  df-3 11024  df-4 11025  df-5 11026  df-6 11027  df-7 11028  df-8 11029  df-9 11030  df-n0 11237  df-z 11322  df-dec 11438  df-uz 11632  df-q 11733  df-rp 11777  df-xneg 11890  df-xadd 11891  df-xmul 11892  df-ioo 12121  df-ioc 12122  df-ico 12123  df-icc 12124  df-fz 12269  df-fzo 12407  df-fl 12533  df-seq 12742  df-exp 12801  df-fac 13001  df-bc 13030  df-hash 13058  df-shft 13741  df-cj 13773  df-re 13774  df-im 13775  df-sqrt 13909  df-abs 13910  df-limsup 14136  df-clim 14153  df-rlim 14154  df-sum 14351  df-ef 14723  df-sin 14725  df-cos 14726  df-pi 14728  df-struct 15783  df-ndx 15784  df-slot 15785  df-base 15786  df-sets 15787  df-ress 15788  df-plusg 15875  df-mulr 15876  df-starv 15877  df-sca 15878  df-vsca 15879  df-ip 15880  df-tset 15881  df-ple 15882  df-ds 15885  df-unif 15886  df-hom 15887  df-cco 15888  df-rest 16004  df-topn 16005  df-0g 16023  df-gsum 16024  df-topgen 16025  df-pt 16026  df-prds 16029  df-xrs 16083  df-qtop 16088  df-imas 16089  df-xps 16091  df-mre 16167  df-mrc 16168  df-acs 16170  df-mgm 17163  df-sgrp 17205  df-mnd 17216  df-submnd 17257  df-mulg 17462  df-cntz 17671  df-cmn 18116  df-psmet 19657  df-xmet 19658  df-met 19659  df-bl 19660  df-mopn 19661  df-fbas 19662  df-fg 19663  df-cnfld 19666  df-top 20621  df-bases 20622  df-topon 20623  df-topsp 20624  df-cld 20733  df-ntr 20734  df-cls 20735  df-nei 20812  df-lp 20850  df-perf 20851  df-cn 20941  df-cnp 20942  df-haus 21029  df-tx 21275  df-hmeo 21468  df-fil 21560  df-fm 21652  df-flim 21653  df-flf 21654  df-xms 22035  df-ms 22036  df-tms 22037  df-cncf 22589  df-limc 23536  df-dv 23537
This theorem is referenced by:  fourierdlem86  39716  fourierdlem103  39733  fourierdlem104  39734
  Copyright terms: Public domain W3C validator