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

Theorem itgspltprt 42140
Description: The integral splits on a given partition 𝑃. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
itgspltprt.1 (𝜑𝑀 ∈ ℤ)
itgspltprt.2 (𝜑𝑁 ∈ (ℤ‘(𝑀 + 1)))
itgspltprt.3 (𝜑𝑃:(𝑀...𝑁)⟶ℝ)
itgspltprt.4 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑃𝑖) < (𝑃‘(𝑖 + 1)))
itgspltprt.5 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁))) → 𝐴 ∈ ℂ)
itgspltprt.6 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1)
Assertion
Ref Expression
itgspltprt (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑁))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
Distinct variable groups:   𝐴,𝑖   𝑖,𝑀,𝑡   𝑖,𝑁,𝑡   𝑃,𝑖,𝑡   𝜑,𝑖,𝑡
Allowed substitution hint:   𝐴(𝑡)

Proof of Theorem itgspltprt
Dummy variables 𝑗 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 itgspltprt.1 . . . . . 6 (𝜑𝑀 ∈ ℤ)
21peano2zd 12078 . . . . 5 (𝜑 → (𝑀 + 1) ∈ ℤ)
3 itgspltprt.2 . . . . . 6 (𝜑𝑁 ∈ (ℤ‘(𝑀 + 1)))
4 eluzelz 12241 . . . . . 6 (𝑁 ∈ (ℤ‘(𝑀 + 1)) → 𝑁 ∈ ℤ)
53, 4syl 17 . . . . 5 (𝜑𝑁 ∈ ℤ)
62, 5, 53jca 1120 . . . 4 (𝜑 → ((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ))
7 eluzle 12244 . . . . 5 (𝑁 ∈ (ℤ‘(𝑀 + 1)) → (𝑀 + 1) ≤ 𝑁)
83, 7syl 17 . . . 4 (𝜑 → (𝑀 + 1) ≤ 𝑁)
9 eluzelre 12242 . . . . . 6 (𝑁 ∈ (ℤ‘(𝑀 + 1)) → 𝑁 ∈ ℝ)
103, 9syl 17 . . . . 5 (𝜑𝑁 ∈ ℝ)
1110leidd 11194 . . . 4 (𝜑𝑁𝑁)
126, 8, 11jca32 516 . . 3 (𝜑 → (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑀 + 1) ≤ 𝑁𝑁𝑁)))
13 elfz2 12887 . . 3 (𝑁 ∈ ((𝑀 + 1)...𝑁) ↔ (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑀 + 1) ≤ 𝑁𝑁𝑁)))
1412, 13sylibr 235 . 2 (𝜑𝑁 ∈ ((𝑀 + 1)...𝑁))
15 fveq2 6663 . . . . . . 7 (𝑗 = (𝑀 + 1) → (𝑃𝑗) = (𝑃‘(𝑀 + 1)))
1615oveq2d 7161 . . . . . 6 (𝑗 = (𝑀 + 1) → ((𝑃𝑀)[,](𝑃𝑗)) = ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))))
1716itgeq1d 42118 . . . . 5 (𝑗 = (𝑀 + 1) → ∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡)
18 oveq2 7153 . . . . . 6 (𝑗 = (𝑀 + 1) → (𝑀..^𝑗) = (𝑀..^(𝑀 + 1)))
1918sumeq1d 15046 . . . . 5 (𝑗 = (𝑀 + 1) → Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
2017, 19eqeq12d 2834 . . . 4 (𝑗 = (𝑀 + 1) → (∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ↔ ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
2120imbi2d 342 . . 3 (𝑗 = (𝑀 + 1) → ((𝜑 → ∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ↔ (𝜑 → ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)))
22 fveq2 6663 . . . . . . 7 (𝑗 = 𝑘 → (𝑃𝑗) = (𝑃𝑘))
2322oveq2d 7161 . . . . . 6 (𝑗 = 𝑘 → ((𝑃𝑀)[,](𝑃𝑗)) = ((𝑃𝑀)[,](𝑃𝑘)))
2423itgeq1d 42118 . . . . 5 (𝑗 = 𝑘 → ∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡)
25 oveq2 7153 . . . . . 6 (𝑗 = 𝑘 → (𝑀..^𝑗) = (𝑀..^𝑘))
2625sumeq1d 15046 . . . . 5 (𝑗 = 𝑘 → Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
2724, 26eqeq12d 2834 . . . 4 (𝑗 = 𝑘 → (∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ↔ ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
2827imbi2d 342 . . 3 (𝑗 = 𝑘 → ((𝜑 → ∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ↔ (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)))
29 fveq2 6663 . . . . . . 7 (𝑗 = (𝑘 + 1) → (𝑃𝑗) = (𝑃‘(𝑘 + 1)))
3029oveq2d 7161 . . . . . 6 (𝑗 = (𝑘 + 1) → ((𝑃𝑀)[,](𝑃𝑗)) = ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))))
3130itgeq1d 42118 . . . . 5 (𝑗 = (𝑘 + 1) → ∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = ∫((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡)
32 oveq2 7153 . . . . . 6 (𝑗 = (𝑘 + 1) → (𝑀..^𝑗) = (𝑀..^(𝑘 + 1)))
3332sumeq1d 15046 . . . . 5 (𝑗 = (𝑘 + 1) → Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
3431, 33eqeq12d 2834 . . . 4 (𝑗 = (𝑘 + 1) → (∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ↔ ∫((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
3534imbi2d 342 . . 3 (𝑗 = (𝑘 + 1) → ((𝜑 → ∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ↔ (𝜑 → ∫((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)))
36 fveq2 6663 . . . . . . 7 (𝑗 = 𝑁 → (𝑃𝑗) = (𝑃𝑁))
3736oveq2d 7161 . . . . . 6 (𝑗 = 𝑁 → ((𝑃𝑀)[,](𝑃𝑗)) = ((𝑃𝑀)[,](𝑃𝑁)))
3837itgeq1d 42118 . . . . 5 (𝑗 = 𝑁 → ∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = ∫((𝑃𝑀)[,](𝑃𝑁))𝐴 d𝑡)
39 oveq2 7153 . . . . . 6 (𝑗 = 𝑁 → (𝑀..^𝑗) = (𝑀..^𝑁))
4039sumeq1d 15046 . . . . 5 (𝑗 = 𝑁 → Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
4138, 40eqeq12d 2834 . . . 4 (𝑗 = 𝑁 → (∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ↔ ∫((𝑃𝑀)[,](𝑃𝑁))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
4241imbi2d 342 . . 3 (𝑗 = 𝑁 → ((𝜑 → ∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ↔ (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑁))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)))
431adantl 482 . . . . . . . 8 ((𝑁 ∈ (ℤ‘(𝑀 + 1)) ∧ 𝜑) → 𝑀 ∈ ℤ)
44 fzval3 13094 . . . . . . . 8 (𝑀 ∈ ℤ → (𝑀...𝑀) = (𝑀..^(𝑀 + 1)))
4543, 44syl 17 . . . . . . 7 ((𝑁 ∈ (ℤ‘(𝑀 + 1)) ∧ 𝜑) → (𝑀...𝑀) = (𝑀..^(𝑀 + 1)))
4645eqcomd 2824 . . . . . 6 ((𝑁 ∈ (ℤ‘(𝑀 + 1)) ∧ 𝜑) → (𝑀..^(𝑀 + 1)) = (𝑀...𝑀))
4746sumeq1d 15046 . . . . 5 ((𝑁 ∈ (ℤ‘(𝑀 + 1)) ∧ 𝜑) → Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀...𝑀)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
48 itgspltprt.3 . . . . . . . . . . . 12 (𝜑𝑃:(𝑀...𝑁)⟶ℝ)
4948adantr 481 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑃:(𝑀...𝑁)⟶ℝ)
501zred 12075 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℝ)
51 1red 10630 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ∈ ℝ)
5250, 51readdcld 10658 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑀 + 1) ∈ ℝ)
5350ltp1d 11558 . . . . . . . . . . . . . . . 16 (𝜑𝑀 < (𝑀 + 1))
5450, 52, 10, 53, 8ltletrd 10788 . . . . . . . . . . . . . . 15 (𝜑𝑀 < 𝑁)
5550, 10, 54ltled 10776 . . . . . . . . . . . . . 14 (𝜑𝑀𝑁)
56 eluz 12245 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ𝑀) ↔ 𝑀𝑁))
571, 5, 56syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 ∈ (ℤ𝑀) ↔ 𝑀𝑁))
5855, 57mpbird 258 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ (ℤ𝑀))
59 eluzfz1 12902 . . . . . . . . . . . . 13 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...𝑁))
6058, 59syl 17 . . . . . . . . . . . 12 (𝜑𝑀 ∈ (𝑀...𝑁))
6160adantr 481 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑀 ∈ (𝑀...𝑁))
6249, 61ffvelrnd 6844 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃𝑀) ∈ ℝ)
63 elfz1 12885 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (𝑀...𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑀𝑁𝑁𝑁)))
641, 5, 63syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → (𝑁 ∈ (𝑀...𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑀𝑁𝑁𝑁)))
655, 55, 11, 64mpbir3and 1334 . . . . . . . . . . . 12 (𝜑𝑁 ∈ (𝑀...𝑁))
6648, 65ffvelrnd 6844 . . . . . . . . . . 11 (𝜑 → (𝑃𝑁) ∈ ℝ)
6766adantr 481 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃𝑁) ∈ ℝ)
6850lep1d 11559 . . . . . . . . . . . . . 14 (𝜑𝑀 ≤ (𝑀 + 1))
69 elfz1 12885 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 + 1) ∈ (𝑀...𝑁) ↔ ((𝑀 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑀 + 1) ∧ (𝑀 + 1) ≤ 𝑁)))
701, 5, 69syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → ((𝑀 + 1) ∈ (𝑀...𝑁) ↔ ((𝑀 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑀 + 1) ∧ (𝑀 + 1) ≤ 𝑁)))
712, 68, 8, 70mpbir3and 1334 . . . . . . . . . . . . 13 (𝜑 → (𝑀 + 1) ∈ (𝑀...𝑁))
7248, 71ffvelrnd 6844 . . . . . . . . . . . 12 (𝜑 → (𝑃‘(𝑀 + 1)) ∈ ℝ)
7372adantr 481 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘(𝑀 + 1)) ∈ ℝ)
74 simpr 485 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))))
75 eliccre 41657 . . . . . . . . . . 11 (((𝑃𝑀) ∈ ℝ ∧ (𝑃‘(𝑀 + 1)) ∈ ℝ ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ∈ ℝ)
7662, 73, 74, 75syl3anc 1363 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ∈ ℝ)
7748, 60ffvelrnd 6844 . . . . . . . . . . . . 13 (𝜑 → (𝑃𝑀) ∈ ℝ)
7877rexrd 10679 . . . . . . . . . . . 12 (𝜑 → (𝑃𝑀) ∈ ℝ*)
7978adantr 481 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃𝑀) ∈ ℝ*)
8073rexrd 10679 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘(𝑀 + 1)) ∈ ℝ*)
81 iccgelb 12781 . . . . . . . . . . 11 (((𝑃𝑀) ∈ ℝ* ∧ (𝑃‘(𝑀 + 1)) ∈ ℝ*𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃𝑀) ≤ 𝑡)
8279, 80, 74, 81syl3anc 1363 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃𝑀) ≤ 𝑡)
83 iccleub 12780 . . . . . . . . . . . 12 (((𝑃𝑀) ∈ ℝ* ∧ (𝑃‘(𝑀 + 1)) ∈ ℝ*𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ≤ (𝑃‘(𝑀 + 1)))
8479, 80, 74, 83syl3anc 1363 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ≤ (𝑃‘(𝑀 + 1)))
8548adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ)
86 elfzelz 12896 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ((𝑀 + 1)...𝑁) → 𝑖 ∈ ℤ)
8786adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑖 ∈ ℤ)
8850adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑀 ∈ ℝ)
8987zred 12075 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑖 ∈ ℝ)
9052adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑀 + 1) ∈ ℝ)
9153adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑀 < (𝑀 + 1))
92 elfzle1 12898 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ((𝑀 + 1)...𝑁) → (𝑀 + 1) ≤ 𝑖)
9392adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑀 + 1) ≤ 𝑖)
9488, 90, 89, 91, 93ltletrd 10788 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑀 < 𝑖)
9588, 89, 94ltled 10776 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑀𝑖)
96 elfzle2 12899 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ((𝑀 + 1)...𝑁) → 𝑖𝑁)
9796adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑖𝑁)
981, 5jca 512 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
9998adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
100 elfz1 12885 . . . . . . . . . . . . . . . 16 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀𝑖𝑖𝑁)))
10199, 100syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀𝑖𝑖𝑁)))
10287, 95, 97, 101mpbir3and 1334 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑖 ∈ (𝑀...𝑁))
10385, 102ffvelrnd 6844 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑃𝑖) ∈ ℝ)
10448adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
105 elfzelz 12896 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1)) → 𝑖 ∈ ℤ)
106105adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℤ)
10750adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℝ)
108106zred 12075 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
10952adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑀 + 1) ∈ ℝ)
11053adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 < (𝑀 + 1))
111 elfzle1 12898 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1)) → (𝑀 + 1) ≤ 𝑖)
112111adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑀 + 1) ≤ 𝑖)
113107, 109, 108, 110, 112ltletrd 10788 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 < 𝑖)
114107, 108, 113ltled 10776 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀𝑖)
11510adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℝ)
116 1red 10630 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
117115, 116resubcld 11056 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
118 elfzle2 12899 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1)) → 𝑖 ≤ (𝑁 − 1))
119118adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ≤ (𝑁 − 1))
120115ltm1d 11560 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
121108, 117, 115, 119, 120lelttrd 10786 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 < 𝑁)
122108, 115, 121ltled 10776 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖𝑁)
12398adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
124123, 100syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀𝑖𝑖𝑁)))
125106, 114, 122, 124mpbir3and 1334 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑁))
126104, 125ffvelrnd 6844 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑃𝑖) ∈ ℝ)
127106peano2zd 12078 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℤ)
128108, 116readdcld 10658 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ)
129107, 108, 116, 113ltadd1dd 11239 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑀 + 1) < (𝑖 + 1))
130107, 109, 128, 110, 129lttrd 10789 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 < (𝑖 + 1))
131107, 128, 130ltled 10776 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 ≤ (𝑖 + 1))
132 zltp1le 12020 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
133105, 5, 132syl2anr 596 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
134121, 133mpbid 233 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁)
135 elfz1 12885 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
136123, 135syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
137127, 131, 134, 136mpbir3and 1334 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁))
138104, 137ffvelrnd 6844 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
139 eluz 12245 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑖 ∈ (ℤ𝑀) ↔ 𝑀𝑖))
1401, 105, 139syl2an 595 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 ∈ (ℤ𝑀) ↔ 𝑀𝑖))
141114, 140mpbird 258 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ (ℤ𝑀))
1425adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℤ)
143 elfzo2 13029 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀..^𝑁) ↔ (𝑖 ∈ (ℤ𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑖 < 𝑁))
144141, 142, 121, 143syl3anbrc 1335 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀..^𝑁))
145 itgspltprt.4 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑃𝑖) < (𝑃‘(𝑖 + 1)))
146144, 145syldan 591 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑃𝑖) < (𝑃‘(𝑖 + 1)))
147126, 138, 146ltled 10776 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑃𝑖) ≤ (𝑃‘(𝑖 + 1)))
1483, 103, 147monoord 13388 . . . . . . . . . . . 12 (𝜑 → (𝑃‘(𝑀 + 1)) ≤ (𝑃𝑁))
149148adantr 481 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘(𝑀 + 1)) ≤ (𝑃𝑁))
15076, 73, 67, 84, 149letrd 10785 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ≤ (𝑃𝑁))
15162, 67, 76, 82, 150eliccd 41655 . . . . . . . . 9 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)))
152 itgspltprt.5 . . . . . . . . 9 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁))) → 𝐴 ∈ ℂ)
153151, 152syldan 591 . . . . . . . 8 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝐴 ∈ ℂ)
154 id 22 . . . . . . . . . 10 (𝜑𝜑)
155 fzolb 13032 . . . . . . . . . . 11 (𝑀 ∈ (𝑀..^𝑁) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁))
1561, 5, 54, 155syl3anbrc 1335 . . . . . . . . . 10 (𝜑𝑀 ∈ (𝑀..^𝑁))
157154, 156jca 512 . . . . . . . . 9 (𝜑 → (𝜑𝑀 ∈ (𝑀..^𝑁)))
158 eleq1 2897 . . . . . . . . . . . 12 (𝑖 = 𝑀 → (𝑖 ∈ (𝑀..^𝑁) ↔ 𝑀 ∈ (𝑀..^𝑁)))
159158anbi2d 628 . . . . . . . . . . 11 (𝑖 = 𝑀 → ((𝜑𝑖 ∈ (𝑀..^𝑁)) ↔ (𝜑𝑀 ∈ (𝑀..^𝑁))))
160 fveq2 6663 . . . . . . . . . . . . . 14 (𝑖 = 𝑀 → (𝑃𝑖) = (𝑃𝑀))
161 fvoveq1 7168 . . . . . . . . . . . . . 14 (𝑖 = 𝑀 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑀 + 1)))
162160, 161oveq12d 7163 . . . . . . . . . . . . 13 (𝑖 = 𝑀 → ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) = ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))))
163162mpteq1d 5146 . . . . . . . . . . . 12 (𝑖 = 𝑀 → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) = (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴))
164163eleq1d 2894 . . . . . . . . . . 11 (𝑖 = 𝑀 → ((𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿1))
165159, 164imbi12d 346 . . . . . . . . . 10 (𝑖 = 𝑀 → (((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1) ↔ ((𝜑𝑀 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿1)))
166 itgspltprt.6 . . . . . . . . . 10 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1)
167165, 166vtoclg 3565 . . . . . . . . 9 (𝑀 ∈ ℤ → ((𝜑𝑀 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿1))
1681, 157, 167sylc 65 . . . . . . . 8 (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿1)
169153, 168itgcl 24311 . . . . . . 7 (𝜑 → ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 ∈ ℂ)
170162itgeq1d 42118 . . . . . . . 8 (𝑖 = 𝑀 → ∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡)
171170fsum1 15090 . . . . . . 7 ((𝑀 ∈ ℤ ∧ ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 ∈ ℂ) → Σ𝑖 ∈ (𝑀...𝑀)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡)
1721, 169, 171syl2anc 584 . . . . . 6 (𝜑 → Σ𝑖 ∈ (𝑀...𝑀)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡)
173172adantl 482 . . . . 5 ((𝑁 ∈ (ℤ‘(𝑀 + 1)) ∧ 𝜑) → Σ𝑖 ∈ (𝑀...𝑀)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡)
17447, 173eqtr2d 2854 . . . 4 ((𝑁 ∈ (ℤ‘(𝑀 + 1)) ∧ 𝜑) → ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
175174ex 413 . . 3 (𝑁 ∈ (ℤ‘(𝑀 + 1)) → (𝜑 → ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
176 simp3 1130 . . . . 5 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → 𝜑)
177 simp1 1128 . . . . 5 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → 𝑘 ∈ ((𝑀 + 1)..^𝑁))
178 simp2 1129 . . . . . 6 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
179176, 178mpd 15 . . . . 5 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
18050adantr 481 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ∈ ℝ)
181 elfzoelz 13026 . . . . . . . . . . . 12 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 ∈ ℤ)
182181zred 12075 . . . . . . . . . . 11 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 ∈ ℝ)
183182adantl 482 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ ℝ)
18452adantr 481 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 + 1) ∈ ℝ)
18553adantr 481 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < (𝑀 + 1))
186 elfzole1 13034 . . . . . . . . . . . 12 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑀 + 1) ≤ 𝑘)
187186adantl 482 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 + 1) ≤ 𝑘)
188180, 184, 183, 185, 187ltletrd 10788 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < 𝑘)
189180, 183, 188ltled 10776 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀𝑘)
190 eluz 12245 . . . . . . . . . 10 ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 ∈ (ℤ𝑀) ↔ 𝑀𝑘))
1911, 181, 190syl2an 595 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 ∈ (ℤ𝑀) ↔ 𝑀𝑘))
192189, 191mpbird 258 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (ℤ𝑀))
193 simplll 771 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝜑)
194 eliccxr 12811 . . . . . . . . . . . 12 (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) → 𝑡 ∈ ℝ*)
195194adantl 482 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ℝ*)
196193, 77syl 17 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃𝑀) ∈ ℝ)
197193, 48syl 17 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑃:(𝑀...𝑁)⟶ℝ)
198 elfzelz 12896 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀...𝑘) → 𝑖 ∈ ℤ)
199198adantl 482 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ ℤ)
200 elfzle1 12898 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀...𝑘) → 𝑀𝑖)
201200adantl 482 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀𝑖)
202199zred 12075 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ ℝ)
20310ad2antrr 722 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑁 ∈ ℝ)
204183adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑘 ∈ ℝ)
205 elfzle2 12899 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (𝑀...𝑘) → 𝑖𝑘)
206205adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖𝑘)
207 elfzolt2 13035 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 < 𝑁)
208207ad2antlr 723 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑘 < 𝑁)
209202, 204, 203, 206, 208lelttrd 10786 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 < 𝑁)
210202, 203, 209ltled 10776 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖𝑁)
21198ad2antrr 722 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
212211, 100syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀𝑖𝑖𝑁)))
213199, 201, 210, 212mpbir3and 1334 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ (𝑀...𝑁))
214213adantr 481 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑖 ∈ (𝑀...𝑁))
215197, 214ffvelrnd 6844 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃𝑖) ∈ ℝ)
216199peano2zd 12078 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ∈ ℤ)
21750ad2antrr 722 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 ∈ ℝ)
218216zred 12075 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ∈ ℝ)
21950adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘)) → 𝑀 ∈ ℝ)
220198zred 12075 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (𝑀...𝑘) → 𝑖 ∈ ℝ)
221220adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ ℝ)
222 1red 10630 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑀...𝑘)) → 1 ∈ ℝ)
223221, 222readdcld 10658 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ∈ ℝ)
224200adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘)) → 𝑀𝑖)
225221ltp1d 11558 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘)) → 𝑖 < (𝑖 + 1))
226219, 221, 223, 224, 225lelttrd 10786 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘)) → 𝑀 < (𝑖 + 1))
227226adantlr 711 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 < (𝑖 + 1))
228217, 218, 227ltled 10776 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 ≤ (𝑖 + 1))
2295, 198anim12ci 613 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘)) → (𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ))
230229adantlr 711 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ))
231230, 132syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
232209, 231mpbid 233 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ≤ 𝑁)
233211, 135syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
234216, 228, 232, 233mpbir3and 1334 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ∈ (𝑀...𝑁))
235234adantr 481 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑖 + 1) ∈ (𝑀...𝑁))
236197, 235ffvelrnd 6844 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
237 simpr 485 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))))
238 eliccre 41657 . . . . . . . . . . . . 13 (((𝑃𝑖) ∈ ℝ ∧ (𝑃‘(𝑖 + 1)) ∈ ℝ ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ℝ)
239215, 236, 237, 238syl3anc 1363 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ℝ)
240 elfzuz 12892 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...𝑘) → 𝑖 ∈ (ℤ𝑀))
241240adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ (ℤ𝑀))
24248ad3antrrr 726 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑃:(𝑀...𝑁)⟶ℝ)
243 elfzelz 12896 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑀...𝑖) → 𝑗 ∈ ℤ)
244243adantl 482 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ∈ ℤ)
245 elfzle1 12898 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑀...𝑖) → 𝑀𝑗)
246245adantl 482 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑀𝑗)
247244zred 12075 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ∈ ℝ)
248203adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑁 ∈ ℝ)
249202adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑖 ∈ ℝ)
250 elfzle2 12899 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (𝑀...𝑖) → 𝑗𝑖)
251250adantl 482 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗𝑖)
252209adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑖 < 𝑁)
253247, 249, 248, 251, 252lelttrd 10786 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 < 𝑁)
254247, 248, 253ltled 10776 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗𝑁)
255211adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
256 elfz1 12885 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀𝑗𝑗𝑁)))
257255, 256syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀𝑗𝑗𝑁)))
258244, 246, 254, 257mpbir3and 1334 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ∈ (𝑀...𝑁))
259242, 258ffvelrnd 6844 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝑃𝑗) ∈ ℝ)
26048ad3antrrr 726 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
261 elfzelz 12896 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑗 ∈ ℤ)
262261adantl 482 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ ℤ)
263 elfzle1 12898 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑀𝑗)
264263adantl 482 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀𝑗)
265262zred 12075 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ ℝ)
266203adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑁 ∈ ℝ)
267202adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑖 ∈ ℝ)
268 1red 10630 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 1 ∈ ℝ)
269267, 268resubcld 11056 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑖 − 1) ∈ ℝ)
270 elfzle2 12899 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑗 ≤ (𝑖 − 1))
271270adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ≤ (𝑖 − 1))
272267ltm1d 11560 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑖 − 1) < 𝑖)
273265, 269, 267, 271, 272lelttrd 10786 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 < 𝑖)
274209adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑖 < 𝑁)
275265, 267, 266, 273, 274lttrd 10789 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 < 𝑁)
276265, 266, 275ltled 10776 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗𝑁)
277211adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
278277, 256syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀𝑗𝑗𝑁)))
279262, 264, 276, 278mpbir3and 1334 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ (𝑀...𝑁))
280260, 279ffvelrnd 6844 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑃𝑗) ∈ ℝ)
281262peano2zd 12078 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ∈ ℤ)
282180ad2antrr 722 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 ∈ ℝ)
283265, 268readdcld 10658 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ∈ ℝ)
28450adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 ∈ ℝ)
285261zred 12075 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑗 ∈ ℝ)
286285adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ ℝ)
287 1red 10630 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (𝑀...(𝑖 − 1))) → 1 ∈ ℝ)
288286, 287readdcld 10658 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ∈ ℝ)
289263adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀𝑗)
290286ltp1d 11558 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 < (𝑗 + 1))
291284, 286, 288, 289, 290lelttrd 10786 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 < (𝑗 + 1))
292291ad4ant14 748 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 < (𝑗 + 1))
293282, 283, 292ltled 10776 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 ≤ (𝑗 + 1))
294 zltp1le 12020 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑗 < 𝑖 ↔ (𝑗 + 1) ≤ 𝑖))
295261, 199, 294syl2anr 596 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 < 𝑖 ↔ (𝑗 + 1) ≤ 𝑖))
296273, 295mpbid 233 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ≤ 𝑖)
297283, 267, 266, 296, 274lelttrd 10786 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) < 𝑁)
298283, 266, 297ltled 10776 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ≤ 𝑁)
299 elfz1 12885 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑗 + 1) ∈ (𝑀...𝑁) ↔ ((𝑗 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑗 + 1) ∧ (𝑗 + 1) ≤ 𝑁)))
300277, 299syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → ((𝑗 + 1) ∈ (𝑀...𝑁) ↔ ((𝑗 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑗 + 1) ∧ (𝑗 + 1) ≤ 𝑁)))
301281, 293, 298, 300mpbir3and 1334 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ∈ (𝑀...𝑁))
302260, 301ffvelrnd 6844 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑃‘(𝑗 + 1)) ∈ ℝ)
303 simplll 771 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝜑)
304 elfzuz 12892 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑗 ∈ (ℤ𝑀))
305304adantl 482 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ (ℤ𝑀))
306303, 5syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑁 ∈ ℤ)
307 elfzo2 13029 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑀..^𝑁) ↔ (𝑗 ∈ (ℤ𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑗 < 𝑁))
308305, 306, 275, 307syl3anbrc 1335 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ (𝑀..^𝑁))
309 eleq1 2897 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → (𝑖 ∈ (𝑀..^𝑁) ↔ 𝑗 ∈ (𝑀..^𝑁)))
310309anbi2d 628 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → ((𝜑𝑖 ∈ (𝑀..^𝑁)) ↔ (𝜑𝑗 ∈ (𝑀..^𝑁))))
311 fveq2 6663 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → (𝑃𝑖) = (𝑃𝑗))
312 fvoveq1 7168 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑗 + 1)))
313311, 312breq12d 5070 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → ((𝑃𝑖) < (𝑃‘(𝑖 + 1)) ↔ (𝑃𝑗) < (𝑃‘(𝑗 + 1))))
314310, 313imbi12d 346 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑗 → (((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑃𝑖) < (𝑃‘(𝑖 + 1))) ↔ ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑃𝑗) < (𝑃‘(𝑗 + 1)))))
315314, 145chvarvv 1996 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑃𝑗) < (𝑃‘(𝑗 + 1)))
316303, 308, 315syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑃𝑗) < (𝑃‘(𝑗 + 1)))
317280, 302, 316ltled 10776 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑃𝑗) ≤ (𝑃‘(𝑗 + 1)))
318241, 259, 317monoord 13388 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑃𝑀) ≤ (𝑃𝑖))
319318adantr 481 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃𝑀) ≤ (𝑃𝑖))
320215rexrd 10679 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃𝑖) ∈ ℝ*)
321236rexrd 10679 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘(𝑖 + 1)) ∈ ℝ*)
322 iccgelb 12781 . . . . . . . . . . . . 13 (((𝑃𝑖) ∈ ℝ* ∧ (𝑃‘(𝑖 + 1)) ∈ ℝ*𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃𝑖) ≤ 𝑡)
323320, 321, 237, 322syl3anc 1363 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃𝑖) ≤ 𝑡)
324196, 215, 239, 319, 323letrd 10785 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃𝑀) ≤ 𝑡)
325193, 66syl 17 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃𝑁) ∈ ℝ)
326 iccleub 12780 . . . . . . . . . . . . 13 (((𝑃𝑖) ∈ ℝ* ∧ (𝑃‘(𝑖 + 1)) ∈ ℝ*𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ≤ (𝑃‘(𝑖 + 1)))
327320, 321, 237, 326syl3anc 1363 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ≤ (𝑃‘(𝑖 + 1)))
3285ad2antrr 722 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑁 ∈ ℤ)
329 eluz 12245 . . . . . . . . . . . . . . . 16 (((𝑖 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ‘(𝑖 + 1)) ↔ (𝑖 + 1) ≤ 𝑁))
330216, 328, 329syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑁 ∈ (ℤ‘(𝑖 + 1)) ↔ (𝑖 + 1) ≤ 𝑁))
331232, 330mpbird 258 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑁 ∈ (ℤ‘(𝑖 + 1)))
332331adantr 481 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑁 ∈ (ℤ‘(𝑖 + 1)))
33348ad3antrrr 726 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ)
334 elfzelz 12896 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ((𝑖 + 1)...𝑁) → 𝑗 ∈ ℤ)
335334adantl 482 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑗 ∈ ℤ)
336 elfzel1 12895 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (𝑀...𝑘) → 𝑀 ∈ ℤ)
337336zred 12075 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (𝑀...𝑘) → 𝑀 ∈ ℝ)
338337adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀 ∈ ℝ)
339334zred 12075 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ((𝑖 + 1)...𝑁) → 𝑗 ∈ ℝ)
340339adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑗 ∈ ℝ)
341220adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑖 ∈ ℝ)
342 1red 10630 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 1 ∈ ℝ)
343341, 342readdcld 10658 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑖 + 1) ∈ ℝ)
344200adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀𝑖)
345341ltp1d 11558 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑖 < (𝑖 + 1))
346338, 341, 343, 344, 345lelttrd 10786 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀 < (𝑖 + 1))
347 elfzle1 12898 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ((𝑖 + 1)...𝑁) → (𝑖 + 1) ≤ 𝑗)
348347adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑖 + 1) ≤ 𝑗)
349338, 343, 340, 346, 348ltletrd 10788 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀 < 𝑗)
350338, 340, 349ltled 10776 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀𝑗)
351350adantll 710 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀𝑗)
352 elfzle2 12899 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ((𝑖 + 1)...𝑁) → 𝑗𝑁)
353352adantl 482 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑗𝑁)
354211adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
355354, 256syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀𝑗𝑗𝑁)))
356335, 351, 353, 355mpbir3and 1334 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑗 ∈ (𝑀...𝑁))
357333, 356ffvelrnd 6844 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑃𝑗) ∈ ℝ)
358357adantlr 711 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑃𝑗) ∈ ℝ)
359 simplll 771 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝜑)
360 simplr 765 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑘))
361 simpr 485 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1)))
362483ad2ant1 1125 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
363 elfzelz 12896 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1)) → 𝑗 ∈ ℤ)
3643633ad2ant3 1127 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ℤ)
365503ad2ant1 1125 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℝ)
366364zred 12075 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ℝ)
3672233adant3 1124 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ)
3682263adant3 1124 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 < (𝑖 + 1))
369 elfzle1 12898 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1)) → (𝑖 + 1) ≤ 𝑗)
3703693ad2ant3 1127 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑗)
371365, 367, 366, 368, 370ltletrd 10788 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 < 𝑗)
372365, 366, 371ltled 10776 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀𝑗)
373363adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ℤ)
374373zred 12075 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ℝ)
37510adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℝ)
376 1red 10630 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
377375, 376resubcld 11056 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
378 elfzle2 12899 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1)) → 𝑗 ≤ (𝑁 − 1))
379378adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ≤ (𝑁 − 1))
380375ltm1d 11560 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
381374, 377, 375, 379, 380lelttrd 10786 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 < 𝑁)
382374, 375, 381ltled 10776 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗𝑁)
3833823adant2 1123 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗𝑁)
384983ad2ant1 1125 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
385384, 256syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀𝑗𝑗𝑁)))
386364, 372, 383, 385mpbir3and 1334 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ (𝑀...𝑁))
387362, 386ffvelrnd 6844 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃𝑗) ∈ ℝ)
388364peano2zd 12078 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ∈ ℤ)
389388zred 12075 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ∈ ℝ)
3902203ad2ant2 1126 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
391 1red 10630 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
3922253adant3 1124 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖 < (𝑖 + 1))
393390, 367, 366, 392, 370ltletrd 10788 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖 < 𝑗)
394390, 366, 393ltled 10776 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖𝑗)
395390, 366, 391, 394leadd1dd 11242 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ (𝑗 + 1))
396365, 367, 389, 368, 395ltletrd 10788 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 < (𝑗 + 1))
397365, 389, 396ltled 10776 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 ≤ (𝑗 + 1))
398 zltp1le 12020 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 < 𝑁 ↔ (𝑗 + 1) ≤ 𝑁))
399363, 5, 398syl2anr 596 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 < 𝑁 ↔ (𝑗 + 1) ≤ 𝑁))
400381, 399mpbid 233 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ≤ 𝑁)
4014003adant2 1123 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ≤ 𝑁)
402384, 299syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → ((𝑗 + 1) ∈ (𝑀...𝑁) ↔ ((𝑗 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑗 + 1) ∧ (𝑗 + 1) ≤ 𝑁)))
403388, 397, 401, 402mpbir3and 1334 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ∈ (𝑀...𝑁))
404362, 403ffvelrnd 6844 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃‘(𝑗 + 1)) ∈ ℝ)
405 simp1 1128 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝜑)
40613ad2ant1 1125 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℤ)
407 eluz 12245 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑗 ∈ (ℤ𝑀) ↔ 𝑀𝑗))
408406, 364, 407syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 ∈ (ℤ𝑀) ↔ 𝑀𝑗))
409372, 408mpbird 258 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ (ℤ𝑀))
41053ad2ant1 1125 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℤ)
4113813adant2 1123 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 < 𝑁)
412409, 410, 411, 307syl3anbrc 1335 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ (𝑀..^𝑁))
413405, 412, 315syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃𝑗) < (𝑃‘(𝑗 + 1)))
414387, 404, 413ltled 10776 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃𝑗) ≤ (𝑃‘(𝑗 + 1)))
415359, 360, 361, 414syl3anc 1363 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃𝑗) ≤ (𝑃‘(𝑗 + 1)))
416415adantlr 711 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃𝑗) ≤ (𝑃‘(𝑗 + 1)))
417332, 358, 416monoord 13388 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘(𝑖 + 1)) ≤ (𝑃𝑁))
418239, 236, 325, 327, 417letrd 10785 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ≤ (𝑃𝑁))
41966rexrd 10679 . . . . . . . . . . . . . 14 (𝜑 → (𝑃𝑁) ∈ ℝ*)
42078, 419jca 512 . . . . . . . . . . . . 13 (𝜑 → ((𝑃𝑀) ∈ ℝ* ∧ (𝑃𝑁) ∈ ℝ*))
421193, 420syl 17 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → ((𝑃𝑀) ∈ ℝ* ∧ (𝑃𝑁) ∈ ℝ*))
422 elicc1 12770 . . . . . . . . . . . 12 (((𝑃𝑀) ∈ ℝ* ∧ (𝑃𝑁) ∈ ℝ*) → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)) ↔ (𝑡 ∈ ℝ* ∧ (𝑃𝑀) ≤ 𝑡𝑡 ≤ (𝑃𝑁))))
423421, 422syl 17 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)) ↔ (𝑡 ∈ ℝ* ∧ (𝑃𝑀) ≤ 𝑡𝑡 ≤ (𝑃𝑁))))
424195, 324, 418, 423mpbir3and 1334 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)))
425193, 424, 152syl2anc 584 . . . . . . . . 9 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝐴 ∈ ℂ)
426 simpll 763 . . . . . . . . . 10 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝜑)
427241, 328, 209, 143syl3anbrc 1335 . . . . . . . . . 10 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ (𝑀..^𝑁))
428426, 427, 166syl2anc 584 . . . . . . . . 9 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1)
429425, 428itgcl 24311 . . . . . . . 8 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → ∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ∈ ℂ)
430 fveq2 6663 . . . . . . . . . 10 (𝑖 = 𝑘 → (𝑃𝑖) = (𝑃𝑘))
431 fvoveq1 7168 . . . . . . . . . 10 (𝑖 = 𝑘 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑘 + 1)))
432430, 431oveq12d 7163 . . . . . . . . 9 (𝑖 = 𝑘 → ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) = ((𝑃𝑘)[,](𝑃‘(𝑘 + 1))))
433432itgeq1d 42118 . . . . . . . 8 (𝑖 = 𝑘 → ∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡)
434192, 429, 433fzosump1 15095 . . . . . . 7 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
4354343adant3 1124 . . . . . 6 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
436 oveq1 7152 . . . . . . . 8 (∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 → (∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
437436eqcomd 2824 . . . . . . 7 (∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 → (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = (∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
4384373ad2ant3 1127 . . . . . 6 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = (∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
43977adantr 481 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑀) ∈ ℝ)
44048adantr 481 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ)
441181adantl 482 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ ℤ)
442441peano2zd 12078 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ ℤ)
443442zred 12075 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ ℝ)
444183ltp1d 11558 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 < (𝑘 + 1))
445180, 183, 443, 188, 444lttrd 10789 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < (𝑘 + 1))
446180, 443, 445ltled 10776 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ≤ (𝑘 + 1))
447207adantl 482 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 < 𝑁)
448 zltp1le 12020 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 < 𝑁 ↔ (𝑘 + 1) ≤ 𝑁))
449181, 5, 448syl2anr 596 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 < 𝑁 ↔ (𝑘 + 1) ≤ 𝑁))
450447, 449mpbid 233 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ≤ 𝑁)
45198adantr 481 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
452 elfz1 12885 . . . . . . . . . . . 12 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑘 + 1) ∈ (𝑀...𝑁) ↔ ((𝑘 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁)))
453451, 452syl 17 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ((𝑘 + 1) ∈ (𝑀...𝑁) ↔ ((𝑘 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁)))
454442, 446, 450, 453mpbir3and 1334 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ (𝑀...𝑁))
455440, 454ffvelrnd 6844 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ∈ ℝ)
45610adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ ℝ)
457183, 456, 447ltled 10776 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘𝑁)
458 elfz1 12885 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘𝑁)))
459451, 458syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘𝑁)))
460441, 189, 457, 459mpbir3and 1334 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (𝑀...𝑁))
461440, 460ffvelrnd 6844 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑘) ∈ ℝ)
462461rexrd 10679 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑘) ∈ ℝ*)
46348ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑃:(𝑀...𝑁)⟶ℝ)
464463, 213ffvelrnd 6844 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑃𝑖) ∈ ℝ)
46548ad2antrr 722 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
466 elfzelz 12896 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ∈ ℤ)
467466adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ ℤ)
468 elfzle1 12898 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑀𝑖)
469468adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀𝑖)
470467zred 12075 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ ℝ)
47110ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑁 ∈ ℝ)
472183adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑘 ∈ ℝ)
473 1red 10630 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 1 ∈ ℝ)
474472, 473resubcld 11056 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑘 − 1) ∈ ℝ)
475 elfzle2 12899 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ≤ (𝑘 − 1))
476475adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ≤ (𝑘 − 1))
477472ltm1d 11560 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑘 − 1) < 𝑘)
478470, 474, 472, 476, 477lelttrd 10786 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 < 𝑘)
479447adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑘 < 𝑁)
480470, 472, 471, 478, 479lttrd 10789 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 < 𝑁)
481470, 471, 480ltled 10776 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖𝑁)
48298ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
483482, 100syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀𝑖𝑖𝑁)))
484467, 469, 481, 483mpbir3and 1334 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (𝑀...𝑁))
485465, 484ffvelrnd 6844 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃𝑖) ∈ ℝ)
486467peano2zd 12078 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ∈ ℤ)
48750ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 ∈ ℝ)
488470, 473readdcld 10658 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ∈ ℝ)
489470ltp1d 11558 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 < (𝑖 + 1))
490487, 470, 488, 469, 489lelttrd 10786 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 < (𝑖 + 1))
491487, 488, 490ltled 10776 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 ≤ (𝑖 + 1))
492 zltp1le 12020 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑖 < 𝑘 ↔ (𝑖 + 1) ≤ 𝑘))
493466, 441, 492syl2anr 596 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 < 𝑘 ↔ (𝑖 + 1) ≤ 𝑘))
494478, 493mpbid 233 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ≤ 𝑘)
495488, 472, 471, 494, 479lelttrd 10786 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) < 𝑁)
496488, 471, 495ltled 10776 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ≤ 𝑁)
497482, 135syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
498486, 491, 496, 497mpbir3and 1334 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁))
499465, 498ffvelrnd 6844 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
500 simpll 763 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝜑)
501 elfzuz 12892 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ∈ (ℤ𝑀))
502501adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (ℤ𝑀))
5035ad2antrr 722 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑁 ∈ ℤ)
504502, 503, 480, 143syl3anbrc 1335 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (𝑀..^𝑁))
505500, 504, 145syl2anc 584 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃𝑖) < (𝑃‘(𝑖 + 1)))
506485, 499, 505ltled 10776 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃𝑖) ≤ (𝑃‘(𝑖 + 1)))
507192, 464, 506monoord 13388 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑀) ≤ (𝑃𝑘))
5085adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ ℤ)
509 elfzo2 13029 . . . . . . . . . . . . 13 (𝑘 ∈ (𝑀..^𝑁) ↔ (𝑘 ∈ (ℤ𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑘 < 𝑁))
510192, 508, 447, 509syl3anbrc 1335 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (𝑀..^𝑁))
511 eleq1 2897 . . . . . . . . . . . . . . 15 (𝑖 = 𝑘 → (𝑖 ∈ (𝑀..^𝑁) ↔ 𝑘 ∈ (𝑀..^𝑁)))
512511anbi2d 628 . . . . . . . . . . . . . 14 (𝑖 = 𝑘 → ((𝜑𝑖 ∈ (𝑀..^𝑁)) ↔ (𝜑𝑘 ∈ (𝑀..^𝑁))))
513430, 431breq12d 5070 . . . . . . . . . . . . . 14 (𝑖 = 𝑘 → ((𝑃𝑖) < (𝑃‘(𝑖 + 1)) ↔ (𝑃𝑘) < (𝑃‘(𝑘 + 1))))
514512, 513imbi12d 346 . . . . . . . . . . . . 13 (𝑖 = 𝑘 → (((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑃𝑖) < (𝑃‘(𝑖 + 1))) ↔ ((𝜑𝑘 ∈ (𝑀..^𝑁)) → (𝑃𝑘) < (𝑃‘(𝑘 + 1)))))
515514, 145chvarvv 1996 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (𝑀..^𝑁)) → (𝑃𝑘) < (𝑃‘(𝑘 + 1)))
516510, 515syldan 591 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑘) < (𝑃‘(𝑘 + 1)))
517461, 455, 516ltled 10776 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑘) ≤ (𝑃‘(𝑘 + 1)))
51878adantr 481 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑀) ∈ ℝ*)
519455rexrd 10679 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ∈ ℝ*)
520 elicc1 12770 . . . . . . . . . . 11 (((𝑃𝑀) ∈ ℝ* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ*) → ((𝑃𝑘) ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))) ↔ ((𝑃𝑘) ∈ ℝ* ∧ (𝑃𝑀) ≤ (𝑃𝑘) ∧ (𝑃𝑘) ≤ (𝑃‘(𝑘 + 1)))))
521518, 519, 520syl2anc 584 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ((𝑃𝑘) ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))) ↔ ((𝑃𝑘) ∈ ℝ* ∧ (𝑃𝑀) ≤ (𝑃𝑘) ∧ (𝑃𝑘) ≤ (𝑃‘(𝑘 + 1)))))
522462, 507, 517, 521mpbir3and 1334 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑘) ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))))
523 simpll 763 . . . . . . . . . 10 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝜑)
524 eliccxr 12811 . . . . . . . . . . . 12 (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))) → 𝑡 ∈ ℝ*)
525524adantl 482 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ℝ*)
52678ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃𝑀) ∈ ℝ*)
527519adantr 481 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ∈ ℝ*)
528 simpr 485 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))))
529 iccgelb 12781 . . . . . . . . . . . 12 (((𝑃𝑀) ∈ ℝ* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ*𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃𝑀) ≤ 𝑡)
530526, 527, 528, 529syl3anc 1363 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃𝑀) ≤ 𝑡)
53177ad2antrr 722 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃𝑀) ∈ ℝ)
532455adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ∈ ℝ)
533 eliccre 41657 . . . . . . . . . . . . 13 (((𝑃𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ℝ)
534531, 532, 528, 533syl3anc 1363 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ℝ)
53566ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃𝑁) ∈ ℝ)
536 iccleub 12780 . . . . . . . . . . . . 13 (((𝑃𝑀) ∈ ℝ* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ*𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ≤ (𝑃‘(𝑘 + 1)))
537526, 527, 528, 536syl3anc 1363 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ≤ (𝑃‘(𝑘 + 1)))
538 eluz2 12237 . . . . . . . . . . . . . . 15 (𝑁 ∈ (ℤ‘(𝑘 + 1)) ↔ ((𝑘 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑘 + 1) ≤ 𝑁))
539442, 508, 450, 538syl3anbrc 1335 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ (ℤ‘(𝑘 + 1)))
54048ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ)
5411ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 ∈ ℤ)
5425ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑁 ∈ ℤ)
543 elfzelz 12896 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖 ∈ ℤ)
544543adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℤ)
545541, 542, 5443jca 1120 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ))
54650ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 ∈ ℝ)
547544zred 12075 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℝ)
548183adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 ∈ ℝ)
549188adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 < 𝑘)
550182adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 ∈ ℝ)
551 1red 10630 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 1 ∈ ℝ)
552550, 551readdcld 10658 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑘 + 1) ∈ ℝ)
553543zred 12075 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖 ∈ ℝ)
554553adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℝ)
555550ltp1d 11558 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < (𝑘 + 1))
556 elfzle1 12898 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ ((𝑘 + 1)...𝑁) → (𝑘 + 1) ≤ 𝑖)
557556adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑘 + 1) ≤ 𝑖)
558550, 552, 554, 555, 557ltletrd 10788 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < 𝑖)
559558adantll 710 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < 𝑖)
560546, 548, 547, 549, 559lttrd 10789 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 < 𝑖)
561546, 547, 560ltled 10776 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀𝑖)
562 elfzle2 12899 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖𝑁)
563562adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖𝑁)
564545, 561, 563jca32 516 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑀𝑖𝑖𝑁)))
565 elfz2 12887 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑀𝑖𝑖𝑁)))
566564, 565sylibr 235 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ (𝑀...𝑁))
567540, 566ffvelrnd 6844 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑃𝑖) ∈ ℝ)
56848ad2antrr 722 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
5691ad2antrr 722 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℤ)
5705ad2antrr 722 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℤ)
571 elfzelz 12896 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ∈ ℤ)
572571adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℤ)
573569, 570, 5723jca 1120 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ))
57450ad2antrr 722 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℝ)
575572zred 12075 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
576183adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 ∈ ℝ)
577188adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < 𝑘)
578182adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 ∈ ℝ)
579 1red 10630 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
580578, 579readdcld 10658 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑘 + 1) ∈ ℝ)
581571zred 12075 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ∈ ℝ)
582581adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
583578ltp1d 11558 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < (𝑘 + 1))
584 elfzle1 12898 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → (𝑘 + 1) ≤ 𝑖)
585584adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑘 + 1) ≤ 𝑖)
586578, 580, 582, 583, 585ltletrd 10788 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < 𝑖)
587586adantll 710 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < 𝑖)
588574, 576, 575, 577, 587lttrd 10789 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < 𝑖)
589574, 575, 588ltled 10776 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀𝑖)
590581adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
59110adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℝ)
592 1red 10630 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
593591, 592resubcld 11056 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
594 elfzle2 12899 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ≤ (𝑁 − 1))
595594adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ≤ (𝑁 − 1))
596591ltm1d 11560 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
597590, 593, 591, 595, 596lelttrd 10786 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 < 𝑁)
598590, 591, 597ltled 10776 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖𝑁)
599598adantlr 711 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖𝑁)
600573, 589, 599jca32 516 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑀𝑖𝑖𝑁)))
601600, 565sylibr 235 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑁))
602568, 601ffvelrnd 6844 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃𝑖) ∈ ℝ)
603572peano2zd 12078 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℤ)
604569, 570, 6033jca 1120 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ))
605603zred 12075 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ)
606575ltp1d 11558 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 < (𝑖 + 1))
607576, 575, 605, 587, 606lttrd 10789 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < (𝑖 + 1))
608574, 576, 605, 577, 607lttrd 10789 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < (𝑖 + 1))
609574, 605, 608ltled 10776 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ≤ (𝑖 + 1))
610597adantlr 711 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 < 𝑁)
611571, 508, 132syl2anr 596 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
612610, 611mpbid 233 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁)
613604, 609, 612jca32 516 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ) ∧ (𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
614 elfz2 12887 . . . . . . . . . . . . . . . . 17 ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ) ∧ (𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
615613, 614sylibr 235 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁))
616568, 615ffvelrnd 6844 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
617 simpll 763 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝜑)
618 eluz2 12237 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 𝑀𝑖))
619569, 572, 589, 618syl3anbrc 1335 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (ℤ𝑀))
620619, 570, 610, 143syl3anbrc 1335 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀..^𝑁))
621617, 620, 145syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃𝑖) < (𝑃‘(𝑖 + 1)))
622602, 616, 621ltled 10776 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃𝑖) ≤ (𝑃‘(𝑖 + 1)))
623539, 567, 622monoord 13388 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ≤ (𝑃𝑁))
624623adantr 481 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ≤ (𝑃𝑁))
625534, 532, 535, 537, 624letrd 10785 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ≤ (𝑃𝑁))
626420ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → ((𝑃𝑀) ∈ ℝ* ∧ (𝑃𝑁) ∈ ℝ*))
627626, 422syl 17 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)) ↔ (𝑡 ∈ ℝ* ∧ (𝑃𝑀) ≤ 𝑡𝑡 ≤ (𝑃𝑁))))
628525, 530, 625, 627mpbir3and 1334 . . . . . . . . . 10 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)))
629523, 628, 152syl2anc 584 . . . . . . . . 9 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝐴 ∈ ℂ)
630 nfv 1906 . . . . . . . . . 10 𝑡(𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁))
6311adantr 481 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ∈ ℤ)
632 elfzouz 13030 . . . . . . . . . . 11 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 ∈ (ℤ‘(𝑀 + 1)))
633632adantl 482 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (ℤ‘(𝑀 + 1)))
634 simpll 763 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝜑)
635 elfzouz 13030 . . . . . . . . . . . . 13 (𝑖 ∈ (𝑀..^𝑘) → 𝑖 ∈ (ℤ𝑀))
636635adantl 482 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 ∈ (ℤ𝑀))
6375ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑁 ∈ ℤ)
638 elfzoelz 13026 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀..^𝑘) → 𝑖 ∈ ℤ)
639638zred 12075 . . . . . . . . . . . . . 14 (𝑖 ∈ (𝑀..^𝑘) → 𝑖 ∈ ℝ)
640639adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 ∈ ℝ)
641183adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑘 ∈ ℝ)
64210ad2antrr 722 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑁 ∈ ℝ)
643 elfzolt2 13035 . . . . . . . . . . . . . 14 (𝑖 ∈ (𝑀..^𝑘) → 𝑖 < 𝑘)
644643adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 < 𝑘)
645447adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑘 < 𝑁)
646640, 641, 642, 644, 645lttrd 10789 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 < 𝑁)
647636, 637, 646, 143syl3anbrc 1335 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 ∈ (𝑀..^𝑁))
648634, 647, 145syl2anc 584 . . . . . . . . . 10 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → (𝑃𝑖) < (𝑃‘(𝑖 + 1)))
649 simpll 763 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → 𝜑)
65077ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → (𝑃𝑀) ∈ ℝ)
65166ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → (𝑃𝑁) ∈ ℝ)
652461adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → (𝑃𝑘) ∈ ℝ)
653 simpr 485 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)))
654 eliccre 41657 . . . . . . . . . . . . 13 (((𝑃𝑀) ∈ ℝ ∧ (𝑃𝑘) ∈ ℝ ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → 𝑡 ∈ ℝ)
655650, 652, 653, 654syl3anc 1363 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → 𝑡 ∈ ℝ)
65678ad2antrr 722 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → (𝑃𝑀) ∈ ℝ*)
657462adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → (𝑃𝑘) ∈ ℝ*)
658 iccgelb 12781 . . . . . . . . . . . . 13 (((𝑃𝑀) ∈ ℝ* ∧ (𝑃𝑘) ∈ ℝ*𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → (𝑃𝑀) ≤ 𝑡)
659656, 657, 653, 658syl3anc 1363 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → (𝑃𝑀) ≤ 𝑡)
660 iccleub 12780 . . . . . . . . . . . . . 14 (((𝑃𝑀) ∈ ℝ* ∧ (𝑃𝑘) ∈ ℝ*𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → 𝑡 ≤ (𝑃𝑘))
661656, 657, 653, 660syl3anc 1363 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → 𝑡 ≤ (𝑃𝑘))
662 elfzouz2 13040 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑁 ∈ (ℤ𝑘))
663662adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ (ℤ𝑘))
66448ad2antrr 722 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ)
6651ad2antrr 722 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀 ∈ ℤ)
6665ad2antrr 722 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑁 ∈ ℤ)
667 elfzelz 12896 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (𝑘...𝑁) → 𝑖 ∈ ℤ)
668667adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑖 ∈ ℤ)
669665, 666, 6683jca 1120 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ))
67050ad2antrr 722 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀 ∈ ℝ)
671668zred 12075 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑖 ∈ ℝ)
672183adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑘 ∈ ℝ)
673188adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀 < 𝑘)
674 elfzle1 12898 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (𝑘...𝑁) → 𝑘𝑖)
675674adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑘𝑖)
676670, 672, 671, 673, 675ltletrd 10788 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀 < 𝑖)
677670, 671, 676ltled 10776 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀𝑖)
678 elfzle2 12899 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (𝑘...𝑁) → 𝑖𝑁)
679678adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑖𝑁)
680669, 677, 679jca32 516 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑀𝑖𝑖𝑁)))
681680, 565sylibr 235 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑖 ∈ (𝑀...𝑁))
682664, 681ffvelrnd 6844 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → (𝑃𝑖) ∈ ℝ)
68348ad2antrr 722 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
6841ad2antrr 722 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 ∈ ℤ)
6855ad2antrr 722 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑁 ∈ ℤ)
686 elfzelz 12896 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (𝑘...(𝑁 − 1)) → 𝑖 ∈ ℤ)
687686adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ ℤ)
688684, 685, 6873jca 1120 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ))
68950ad2antrr 722 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 ∈ ℝ)
690687zred 12075 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ ℝ)
691183adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑘 ∈ ℝ)
692188adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 < 𝑘)
693 elfzle1 12898 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (𝑘...(𝑁 − 1)) → 𝑘𝑖)
694693adantl 482 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑘𝑖)
695689, 691, 690, 692, 694ltletrd 10788 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 < 𝑖)
696689, 690, 695ltled 10776 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀𝑖)
697686zred 12075 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (𝑘...(𝑁 − 1)) → 𝑖 ∈ ℝ)
698697adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ ℝ)
69910adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑁 ∈ ℝ)
700 1red 10630 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → 1 ∈ ℝ)
701699, 700resubcld 11056 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
702 elfzle2 12899 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (𝑘...(𝑁 − 1)) → 𝑖 ≤ (𝑁 − 1))
703702adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ≤ (𝑁 − 1))
704699ltm1d 11560 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
705698, 701, 699, 703, 704lelttrd 10786 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 < 𝑁)
706698, 699, 705ltled 10776 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖𝑁)
707706adantlr 711 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖𝑁)
708688, 696, 707jca32 516 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑀𝑖𝑖𝑁)))
709708, 565sylibr 235 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑁))
710683, 709ffvelrnd 6844 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑃𝑖) ∈ ℝ)
711687peano2zd 12078 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ∈ ℤ)
712684, 685, 7113jca 1120 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ))
713711zred 12075 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ)
714690ltp1d 11558 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 < (𝑖 + 1))
715689, 690, 713, 696, 714lelttrd 10786 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 < (𝑖 + 1))
716689, 713, 715ltled 10776 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 ≤ (𝑖 + 1))
717686, 5, 132syl2anr 596 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
718705, 717mpbid 233 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁)
719718adantlr 711 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁)
720712, 716, 719jca32 516 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ) ∧ (𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
721720, 614sylibr 235 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁))
722683, 721ffvelrnd 6844 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
723 simpll 763 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝜑)
724684, 687, 696, 618syl3anbrc 1335 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ (ℤ𝑀))
725705adantlr 711 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 < 𝑁)
726724, 685, 725, 143syl3anbrc 1335 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ (𝑀..^𝑁))
727723, 726, 145syl2anc 584 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑃𝑖) < (𝑃‘(𝑖 + 1)))
728710, 722, 727ltled 10776 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑃𝑖) ≤ (𝑃‘(𝑖 + 1)))
729663, 682, 728monoord 13388 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑘) ≤ (𝑃𝑁))
730729adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → (𝑃𝑘) ≤ (𝑃𝑁))
731655, 652, 651, 661, 730letrd 10785 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → 𝑡 ≤ (𝑃𝑁))
732650, 651, 655, 659, 731eliccd 41655 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)))
733649, 732, 152syl2anc 584 . . . . . . . . . 10 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → 𝐴 ∈ ℂ)
734634, 647, 166syl2anc 584 . . . . . . . . . 10 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1)
735630, 631, 633, 464, 648, 733, 734iblspltprt 42134 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)) ↦ 𝐴) ∈ 𝐿1)
736432mpteq1d 5146 . . . . . . . . . . . . 13 (𝑖 = 𝑘 → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) = (𝑡 ∈ ((𝑃𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴))
737736eleq1d 2894 . . . . . . . . . . . 12 (𝑖 = 𝑘 → ((𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1))
738512, 737imbi12d 346 . . . . . . . . . . 11 (𝑖 = 𝑘 → (((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1) ↔ ((𝜑𝑘 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1)))
739738, 166chvarvv 1996 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1)
740510, 739syldan 591 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑡 ∈ ((𝑃𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1)
741439, 455, 522, 629, 735, 740itgspliticc 24364 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ∫((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = (∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
742741eqcomd 2824 . . . . . . 7 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = ∫((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡)
7437423adant3 1124 . . . . . 6 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → (∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = ∫((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡)
744435, 438, 7433eqtrrd 2858 . . . . 5 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → ∫((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
745176, 177, 179, 744syl3anc 1363 . . . 4 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → ∫((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
7467453exp 1111 . . 3 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → ((𝜑 → ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → (𝜑 → ∫((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)))
74721, 28, 35, 42, 175, 746fzind2 13143 . 2 (𝑁 ∈ ((𝑀 + 1)...𝑁) → (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑁))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
74814, 747mpcom 38 1 (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑁))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1079   = wceq 1528  wcel 2105   class class class wbr 5057  cmpt 5137  wf 6344  cfv 6348  (class class class)co 7145  cc 10523  cr 10524  1c1 10526   + caddc 10528  *cxr 10662   < clt 10663  cle 10664  cmin 10858  cz 11969  cuz 12231  [,]cicc 12729  ...cfz 12880  ..^cfzo 13021  Σcsu 15030  𝐿1cibl 24145  citg 24146
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-inf2 9092  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602  ax-pre-sup 10603  ax-addf 10604
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-disj 5023  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7398  df-ofr 7399  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-2o 8092  df-oadd 8095  df-er 8278  df-map 8397  df-pm 8398  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-dju 9318  df-card 9356  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286  df-nn 11627  df-2 11688  df-3 11689  df-4 11690  df-n0 11886  df-z 11970  df-uz 12232  df-q 12337  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-ioo 12730  df-ico 12732  df-icc 12733  df-fz 12881  df-fzo 13022  df-fl 13150  df-mod 13226  df-seq 13358  df-exp 13418  df-hash 13679  df-cj 14446  df-re 14447  df-im 14448  df-sqrt 14582  df-abs 14583  df-clim 14833  df-sum 15031  df-rest 16684  df-topgen 16705  df-psmet 20465  df-xmet 20466  df-met 20467  df-bl 20468  df-mopn 20469  df-top 21430  df-topon 21447  df-bases 21482  df-cmp 21923  df-ovol 23992  df-vol 23993  df-mbf 24147  df-itg1 24148  df-itg2 24149  df-ibl 24150  df-itg 24151
This theorem is referenced by:  fourierdlem73  42341  fourierdlem81  42349  fourierdlem93  42361
  Copyright terms: Public domain W3C validator