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 40716
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 11697 . . . . 5 (𝜑 → (𝑀 + 1) ∈ ℤ)
3 itgspltprt.2 . . . . . 6 (𝜑𝑁 ∈ (ℤ‘(𝑀 + 1)))
4 eluzelz 11909 . . . . . 6 (𝑁 ∈ (ℤ‘(𝑀 + 1)) → 𝑁 ∈ ℤ)
53, 4syl 17 . . . . 5 (𝜑𝑁 ∈ ℤ)
62, 5, 53jca 1123 . . . 4 (𝜑 → ((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ))
7 eluzle 11912 . . . . 5 (𝑁 ∈ (ℤ‘(𝑀 + 1)) → (𝑀 + 1) ≤ 𝑁)
83, 7syl 17 . . . 4 (𝜑 → (𝑀 + 1) ≤ 𝑁)
9 eluzelre 11910 . . . . . 6 (𝑁 ∈ (ℤ‘(𝑀 + 1)) → 𝑁 ∈ ℝ)
103, 9syl 17 . . . . 5 (𝜑𝑁 ∈ ℝ)
1110leidd 10806 . . . 4 (𝜑𝑁𝑁)
126, 8, 11jca32 559 . . 3 (𝜑 → (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑀 + 1) ≤ 𝑁𝑁𝑁)))
13 elfz2 12546 . . 3 (𝑁 ∈ ((𝑀 + 1)...𝑁) ↔ (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑀 + 1) ≤ 𝑁𝑁𝑁)))
1412, 13sylibr 224 . 2 (𝜑𝑁 ∈ ((𝑀 + 1)...𝑁))
15 fveq2 6353 . . . . . . 7 (𝑗 = (𝑀 + 1) → (𝑃𝑗) = (𝑃‘(𝑀 + 1)))
1615oveq2d 6830 . . . . . 6 (𝑗 = (𝑀 + 1) → ((𝑃𝑀)[,](𝑃𝑗)) = ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))))
1716itgeq1d 40693 . . . . 5 (𝑗 = (𝑀 + 1) → ∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡)
18 oveq2 6822 . . . . . 6 (𝑗 = (𝑀 + 1) → (𝑀..^𝑗) = (𝑀..^(𝑀 + 1)))
1918sumeq1d 14650 . . . . 5 (𝑗 = (𝑀 + 1) → Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
2017, 19eqeq12d 2775 . . . 4 (𝑗 = (𝑀 + 1) → (∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ↔ ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
2120imbi2d 329 . . 3 (𝑗 = (𝑀 + 1) → ((𝜑 → ∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ↔ (𝜑 → ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)))
22 fveq2 6353 . . . . . . 7 (𝑗 = 𝑘 → (𝑃𝑗) = (𝑃𝑘))
2322oveq2d 6830 . . . . . 6 (𝑗 = 𝑘 → ((𝑃𝑀)[,](𝑃𝑗)) = ((𝑃𝑀)[,](𝑃𝑘)))
2423itgeq1d 40693 . . . . 5 (𝑗 = 𝑘 → ∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡)
25 oveq2 6822 . . . . . 6 (𝑗 = 𝑘 → (𝑀..^𝑗) = (𝑀..^𝑘))
2625sumeq1d 14650 . . . . 5 (𝑗 = 𝑘 → Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
2724, 26eqeq12d 2775 . . . 4 (𝑗 = 𝑘 → (∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ↔ ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
2827imbi2d 329 . . 3 (𝑗 = 𝑘 → ((𝜑 → ∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ↔ (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)))
29 fveq2 6353 . . . . . . 7 (𝑗 = (𝑘 + 1) → (𝑃𝑗) = (𝑃‘(𝑘 + 1)))
3029oveq2d 6830 . . . . . 6 (𝑗 = (𝑘 + 1) → ((𝑃𝑀)[,](𝑃𝑗)) = ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))))
3130itgeq1d 40693 . . . . 5 (𝑗 = (𝑘 + 1) → ∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = ∫((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡)
32 oveq2 6822 . . . . . 6 (𝑗 = (𝑘 + 1) → (𝑀..^𝑗) = (𝑀..^(𝑘 + 1)))
3332sumeq1d 14650 . . . . 5 (𝑗 = (𝑘 + 1) → Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
3431, 33eqeq12d 2775 . . . 4 (𝑗 = (𝑘 + 1) → (∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ↔ ∫((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
3534imbi2d 329 . . 3 (𝑗 = (𝑘 + 1) → ((𝜑 → ∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ↔ (𝜑 → ∫((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)))
36 fveq2 6353 . . . . . . 7 (𝑗 = 𝑁 → (𝑃𝑗) = (𝑃𝑁))
3736oveq2d 6830 . . . . . 6 (𝑗 = 𝑁 → ((𝑃𝑀)[,](𝑃𝑗)) = ((𝑃𝑀)[,](𝑃𝑁)))
3837itgeq1d 40693 . . . . 5 (𝑗 = 𝑁 → ∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = ∫((𝑃𝑀)[,](𝑃𝑁))𝐴 d𝑡)
39 oveq2 6822 . . . . . 6 (𝑗 = 𝑁 → (𝑀..^𝑗) = (𝑀..^𝑁))
4039sumeq1d 14650 . . . . 5 (𝑗 = 𝑁 → Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
4138, 40eqeq12d 2775 . . . 4 (𝑗 = 𝑁 → (∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ↔ ∫((𝑃𝑀)[,](𝑃𝑁))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
4241imbi2d 329 . . 3 (𝑗 = 𝑁 → ((𝜑 → ∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ↔ (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑁))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)))
431adantl 473 . . . . . . . 8 ((𝑁 ∈ (ℤ‘(𝑀 + 1)) ∧ 𝜑) → 𝑀 ∈ ℤ)
44 fzval3 12751 . . . . . . . 8 (𝑀 ∈ ℤ → (𝑀...𝑀) = (𝑀..^(𝑀 + 1)))
4543, 44syl 17 . . . . . . 7 ((𝑁 ∈ (ℤ‘(𝑀 + 1)) ∧ 𝜑) → (𝑀...𝑀) = (𝑀..^(𝑀 + 1)))
4645eqcomd 2766 . . . . . 6 ((𝑁 ∈ (ℤ‘(𝑀 + 1)) ∧ 𝜑) → (𝑀..^(𝑀 + 1)) = (𝑀...𝑀))
4746sumeq1d 14650 . . . . 5 ((𝑁 ∈ (ℤ‘(𝑀 + 1)) ∧ 𝜑) → Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀...𝑀)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
48 itgspltprt.3 . . . . . . . . . . . 12 (𝜑𝑃:(𝑀...𝑁)⟶ℝ)
4948adantr 472 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑃:(𝑀...𝑁)⟶ℝ)
501zred 11694 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℝ)
51 1red 10267 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ∈ ℝ)
5250, 51readdcld 10281 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑀 + 1) ∈ ℝ)
5350ltp1d 11166 . . . . . . . . . . . . . . . 16 (𝜑𝑀 < (𝑀 + 1))
5450, 52, 10, 53, 8ltletrd 10409 . . . . . . . . . . . . . . 15 (𝜑𝑀 < 𝑁)
5550, 10, 54ltled 10397 . . . . . . . . . . . . . 14 (𝜑𝑀𝑁)
56 eluz 11913 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ𝑀) ↔ 𝑀𝑁))
571, 5, 56syl2anc 696 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 ∈ (ℤ𝑀) ↔ 𝑀𝑁))
5855, 57mpbird 247 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ (ℤ𝑀))
59 eluzfz1 12561 . . . . . . . . . . . . 13 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...𝑁))
6058, 59syl 17 . . . . . . . . . . . 12 (𝜑𝑀 ∈ (𝑀...𝑁))
6160adantr 472 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑀 ∈ (𝑀...𝑁))
6249, 61ffvelrnd 6524 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃𝑀) ∈ ℝ)
63 elfz1 12544 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (𝑀...𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑀𝑁𝑁𝑁)))
641, 5, 63syl2anc 696 . . . . . . . . . . . . 13 (𝜑 → (𝑁 ∈ (𝑀...𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑀𝑁𝑁𝑁)))
655, 55, 11, 64mpbir3and 1428 . . . . . . . . . . . 12 (𝜑𝑁 ∈ (𝑀...𝑁))
6648, 65ffvelrnd 6524 . . . . . . . . . . 11 (𝜑 → (𝑃𝑁) ∈ ℝ)
6766adantr 472 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃𝑁) ∈ ℝ)
6850lep1d 11167 . . . . . . . . . . . . . 14 (𝜑𝑀 ≤ (𝑀 + 1))
69 elfz1 12544 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 + 1) ∈ (𝑀...𝑁) ↔ ((𝑀 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑀 + 1) ∧ (𝑀 + 1) ≤ 𝑁)))
701, 5, 69syl2anc 696 . . . . . . . . . . . . . 14 (𝜑 → ((𝑀 + 1) ∈ (𝑀...𝑁) ↔ ((𝑀 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑀 + 1) ∧ (𝑀 + 1) ≤ 𝑁)))
712, 68, 8, 70mpbir3and 1428 . . . . . . . . . . . . 13 (𝜑 → (𝑀 + 1) ∈ (𝑀...𝑁))
7248, 71ffvelrnd 6524 . . . . . . . . . . . 12 (𝜑 → (𝑃‘(𝑀 + 1)) ∈ ℝ)
7372adantr 472 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘(𝑀 + 1)) ∈ ℝ)
74 simpr 479 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))))
75 eliccre 40249 . . . . . . . . . . 11 (((𝑃𝑀) ∈ ℝ ∧ (𝑃‘(𝑀 + 1)) ∈ ℝ ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ∈ ℝ)
7662, 73, 74, 75syl3anc 1477 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ∈ ℝ)
7748, 60ffvelrnd 6524 . . . . . . . . . . . . 13 (𝜑 → (𝑃𝑀) ∈ ℝ)
7877rexrd 10301 . . . . . . . . . . . 12 (𝜑 → (𝑃𝑀) ∈ ℝ*)
7978adantr 472 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃𝑀) ∈ ℝ*)
8073rexrd 10301 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘(𝑀 + 1)) ∈ ℝ*)
81 iccgelb 12443 . . . . . . . . . . 11 (((𝑃𝑀) ∈ ℝ* ∧ (𝑃‘(𝑀 + 1)) ∈ ℝ*𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃𝑀) ≤ 𝑡)
8279, 80, 74, 81syl3anc 1477 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃𝑀) ≤ 𝑡)
83 iccleub 12442 . . . . . . . . . . . 12 (((𝑃𝑀) ∈ ℝ* ∧ (𝑃‘(𝑀 + 1)) ∈ ℝ*𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ≤ (𝑃‘(𝑀 + 1)))
8479, 80, 74, 83syl3anc 1477 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ≤ (𝑃‘(𝑀 + 1)))
8548adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ)
86 elfzelz 12555 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ((𝑀 + 1)...𝑁) → 𝑖 ∈ ℤ)
8786adantl 473 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑖 ∈ ℤ)
8850adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑀 ∈ ℝ)
8987zred 11694 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑖 ∈ ℝ)
9052adantr 472 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑀 + 1) ∈ ℝ)
9153adantr 472 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑀 < (𝑀 + 1))
92 elfzle1 12557 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ((𝑀 + 1)...𝑁) → (𝑀 + 1) ≤ 𝑖)
9392adantl 473 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑀 + 1) ≤ 𝑖)
9488, 90, 89, 91, 93ltletrd 10409 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑀 < 𝑖)
9588, 89, 94ltled 10397 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑀𝑖)
96 elfzle2 12558 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ((𝑀 + 1)...𝑁) → 𝑖𝑁)
9796adantl 473 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑖𝑁)
981, 5jca 555 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
9998adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
100 elfz1 12544 . . . . . . . . . . . . . . . 16 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀𝑖𝑖𝑁)))
10199, 100syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀𝑖𝑖𝑁)))
10287, 95, 97, 101mpbir3and 1428 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑖 ∈ (𝑀...𝑁))
10385, 102ffvelrnd 6524 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑃𝑖) ∈ ℝ)
10448adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
105 elfzelz 12555 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1)) → 𝑖 ∈ ℤ)
106105adantl 473 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℤ)
10750adantr 472 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℝ)
108106zred 11694 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
10952adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑀 + 1) ∈ ℝ)
11053adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 < (𝑀 + 1))
111 elfzle1 12557 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1)) → (𝑀 + 1) ≤ 𝑖)
112111adantl 473 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑀 + 1) ≤ 𝑖)
113107, 109, 108, 110, 112ltletrd 10409 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 < 𝑖)
114107, 108, 113ltled 10397 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀𝑖)
11510adantr 472 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℝ)
116 1red 10267 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
117115, 116resubcld 10670 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
118 elfzle2 12558 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1)) → 𝑖 ≤ (𝑁 − 1))
119118adantl 473 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ≤ (𝑁 − 1))
120115ltm1d 11168 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
121108, 117, 115, 119, 120lelttrd 10407 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 < 𝑁)
122108, 115, 121ltled 10397 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖𝑁)
12398adantr 472 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
124123, 100syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀𝑖𝑖𝑁)))
125106, 114, 122, 124mpbir3and 1428 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑁))
126104, 125ffvelrnd 6524 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑃𝑖) ∈ ℝ)
127106peano2zd 11697 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℤ)
128108, 116readdcld 10281 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ)
129107, 108, 116, 113ltadd1dd 10850 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑀 + 1) < (𝑖 + 1))
130107, 109, 128, 110, 129lttrd 10410 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 < (𝑖 + 1))
131107, 128, 130ltled 10397 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 ≤ (𝑖 + 1))
132 zltp1le 11639 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
133105, 5, 132syl2anr 496 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
134121, 133mpbid 222 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁)
135 elfz1 12544 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
136123, 135syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
137127, 131, 134, 136mpbir3and 1428 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁))
138104, 137ffvelrnd 6524 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
139 eluz 11913 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑖 ∈ (ℤ𝑀) ↔ 𝑀𝑖))
1401, 105, 139syl2an 495 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 ∈ (ℤ𝑀) ↔ 𝑀𝑖))
141114, 140mpbird 247 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ (ℤ𝑀))
1425adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℤ)
143 elfzo2 12687 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀..^𝑁) ↔ (𝑖 ∈ (ℤ𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑖 < 𝑁))
144141, 142, 121, 143syl3anbrc 1429 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀..^𝑁))
145 itgspltprt.4 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑃𝑖) < (𝑃‘(𝑖 + 1)))
146144, 145syldan 488 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑃𝑖) < (𝑃‘(𝑖 + 1)))
147126, 138, 146ltled 10397 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑃𝑖) ≤ (𝑃‘(𝑖 + 1)))
1483, 103, 147monoord 13045 . . . . . . . . . . . 12 (𝜑 → (𝑃‘(𝑀 + 1)) ≤ (𝑃𝑁))
149148adantr 472 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘(𝑀 + 1)) ≤ (𝑃𝑁))
15076, 73, 67, 84, 149letrd 10406 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ≤ (𝑃𝑁))
15162, 67, 76, 82, 150eliccd 40247 . . . . . . . . 9 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)))
152 itgspltprt.5 . . . . . . . . 9 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁))) → 𝐴 ∈ ℂ)
153151, 152syldan 488 . . . . . . . 8 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝐴 ∈ ℂ)
154 id 22 . . . . . . . . . 10 (𝜑𝜑)
155 fzolb 12690 . . . . . . . . . . 11 (𝑀 ∈ (𝑀..^𝑁) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁))
1561, 5, 54, 155syl3anbrc 1429 . . . . . . . . . 10 (𝜑𝑀 ∈ (𝑀..^𝑁))
157154, 156jca 555 . . . . . . . . 9 (𝜑 → (𝜑𝑀 ∈ (𝑀..^𝑁)))
158 eleq1 2827 . . . . . . . . . . . 12 (𝑖 = 𝑀 → (𝑖 ∈ (𝑀..^𝑁) ↔ 𝑀 ∈ (𝑀..^𝑁)))
159158anbi2d 742 . . . . . . . . . . 11 (𝑖 = 𝑀 → ((𝜑𝑖 ∈ (𝑀..^𝑁)) ↔ (𝜑𝑀 ∈ (𝑀..^𝑁))))
160 fveq2 6353 . . . . . . . . . . . . . 14 (𝑖 = 𝑀 → (𝑃𝑖) = (𝑃𝑀))
161 oveq1 6821 . . . . . . . . . . . . . . 15 (𝑖 = 𝑀 → (𝑖 + 1) = (𝑀 + 1))
162161fveq2d 6357 . . . . . . . . . . . . . 14 (𝑖 = 𝑀 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑀 + 1)))
163160, 162oveq12d 6832 . . . . . . . . . . . . 13 (𝑖 = 𝑀 → ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) = ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))))
164163mpteq1d 4890 . . . . . . . . . . . 12 (𝑖 = 𝑀 → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) = (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴))
165164eleq1d 2824 . . . . . . . . . . 11 (𝑖 = 𝑀 → ((𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿1))
166159, 165imbi12d 333 . . . . . . . . . 10 (𝑖 = 𝑀 → (((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1) ↔ ((𝜑𝑀 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿1)))
167 itgspltprt.6 . . . . . . . . . 10 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1)
168166, 167vtoclg 3406 . . . . . . . . 9 (𝑀 ∈ ℤ → ((𝜑𝑀 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿1))
1691, 157, 168sylc 65 . . . . . . . 8 (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿1)
170153, 169itgcl 23769 . . . . . . 7 (𝜑 → ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 ∈ ℂ)
171163itgeq1d 40693 . . . . . . . 8 (𝑖 = 𝑀 → ∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡)
172171fsum1 14695 . . . . . . 7 ((𝑀 ∈ ℤ ∧ ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 ∈ ℂ) → Σ𝑖 ∈ (𝑀...𝑀)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡)
1731, 170, 172syl2anc 696 . . . . . 6 (𝜑 → Σ𝑖 ∈ (𝑀...𝑀)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡)
174173adantl 473 . . . . 5 ((𝑁 ∈ (ℤ‘(𝑀 + 1)) ∧ 𝜑) → Σ𝑖 ∈ (𝑀...𝑀)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡)
17547, 174eqtr2d 2795 . . . 4 ((𝑁 ∈ (ℤ‘(𝑀 + 1)) ∧ 𝜑) → ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
176175ex 449 . . 3 (𝑁 ∈ (ℤ‘(𝑀 + 1)) → (𝜑 → ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
177 simp3 1133 . . . . 5 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → 𝜑)
178 simp1 1131 . . . . 5 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → 𝑘 ∈ ((𝑀 + 1)..^𝑁))
179 simp2 1132 . . . . . 6 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
180177, 179mpd 15 . . . . 5 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
18150adantr 472 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ∈ ℝ)
182 elfzoelz 12684 . . . . . . . . . . . 12 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 ∈ ℤ)
183182zred 11694 . . . . . . . . . . 11 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 ∈ ℝ)
184183adantl 473 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ ℝ)
18552adantr 472 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 + 1) ∈ ℝ)
18653adantr 472 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < (𝑀 + 1))
187 elfzole1 12692 . . . . . . . . . . . 12 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑀 + 1) ≤ 𝑘)
188187adantl 473 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 + 1) ≤ 𝑘)
189181, 185, 184, 186, 188ltletrd 10409 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < 𝑘)
190181, 184, 189ltled 10397 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀𝑘)
191 eluz 11913 . . . . . . . . . 10 ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 ∈ (ℤ𝑀) ↔ 𝑀𝑘))
1921, 182, 191syl2an 495 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 ∈ (ℤ𝑀) ↔ 𝑀𝑘))
193190, 192mpbird 247 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (ℤ𝑀))
194 simplll 815 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝜑)
195 eliccxr 40258 . . . . . . . . . . . 12 (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) → 𝑡 ∈ ℝ*)
196195adantl 473 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ℝ*)
197194, 77syl 17 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃𝑀) ∈ ℝ)
198194, 48syl 17 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑃:(𝑀...𝑁)⟶ℝ)
199 elfzelz 12555 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀...𝑘) → 𝑖 ∈ ℤ)
200199adantl 473 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ ℤ)
201 elfzle1 12557 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀...𝑘) → 𝑀𝑖)
202201adantl 473 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀𝑖)
203200zred 11694 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ ℝ)
20410ad2antrr 764 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑁 ∈ ℝ)
205184adantr 472 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑘 ∈ ℝ)
206 elfzle2 12558 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (𝑀...𝑘) → 𝑖𝑘)
207206adantl 473 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖𝑘)
208 elfzolt2 12693 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 < 𝑁)
209208ad2antlr 765 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑘 < 𝑁)
210203, 205, 204, 207, 209lelttrd 10407 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 < 𝑁)
211203, 204, 210ltled 10397 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖𝑁)
21298ad2antrr 764 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
213212, 100syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀𝑖𝑖𝑁)))
214200, 202, 211, 213mpbir3and 1428 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ (𝑀...𝑁))
215214adantr 472 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑖 ∈ (𝑀...𝑁))
216198, 215ffvelrnd 6524 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃𝑖) ∈ ℝ)
217200peano2zd 11697 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ∈ ℤ)
21850ad2antrr 764 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 ∈ ℝ)
219217zred 11694 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ∈ ℝ)
22050adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘)) → 𝑀 ∈ ℝ)
221199zred 11694 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (𝑀...𝑘) → 𝑖 ∈ ℝ)
222221adantl 473 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ ℝ)
223 1red 10267 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑀...𝑘)) → 1 ∈ ℝ)
224222, 223readdcld 10281 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ∈ ℝ)
225201adantl 473 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘)) → 𝑀𝑖)
226222ltp1d 11166 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘)) → 𝑖 < (𝑖 + 1))
227220, 222, 224, 225, 226lelttrd 10407 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘)) → 𝑀 < (𝑖 + 1))
228227adantlr 753 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 < (𝑖 + 1))
229218, 219, 228ltled 10397 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 ≤ (𝑖 + 1))
2305, 199anim12ci 592 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘)) → (𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ))
231230adantlr 753 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ))
232231, 132syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
233210, 232mpbid 222 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ≤ 𝑁)
234212, 135syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
235217, 229, 233, 234mpbir3and 1428 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ∈ (𝑀...𝑁))
236235adantr 472 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑖 + 1) ∈ (𝑀...𝑁))
237198, 236ffvelrnd 6524 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
238 simpr 479 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))))
239 eliccre 40249 . . . . . . . . . . . . 13 (((𝑃𝑖) ∈ ℝ ∧ (𝑃‘(𝑖 + 1)) ∈ ℝ ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ℝ)
240216, 237, 238, 239syl3anc 1477 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ℝ)
241 elfzuz 12551 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...𝑘) → 𝑖 ∈ (ℤ𝑀))
242241adantl 473 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ (ℤ𝑀))
24348ad3antrrr 768 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑃:(𝑀...𝑁)⟶ℝ)
244 elfzelz 12555 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑀...𝑖) → 𝑗 ∈ ℤ)
245244adantl 473 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ∈ ℤ)
246 elfzle1 12557 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑀...𝑖) → 𝑀𝑗)
247246adantl 473 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑀𝑗)
248245zred 11694 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ∈ ℝ)
249204adantr 472 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑁 ∈ ℝ)
250203adantr 472 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑖 ∈ ℝ)
251 elfzle2 12558 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (𝑀...𝑖) → 𝑗𝑖)
252251adantl 473 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗𝑖)
253210adantr 472 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑖 < 𝑁)
254248, 250, 249, 252, 253lelttrd 10407 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 < 𝑁)
255248, 249, 254ltled 10397 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗𝑁)
256212adantr 472 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
257 elfz1 12544 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀𝑗𝑗𝑁)))
258256, 257syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀𝑗𝑗𝑁)))
259245, 247, 255, 258mpbir3and 1428 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ∈ (𝑀...𝑁))
260243, 259ffvelrnd 6524 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝑃𝑗) ∈ ℝ)
26148ad3antrrr 768 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
262 elfzelz 12555 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑗 ∈ ℤ)
263262adantl 473 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ ℤ)
264 elfzle1 12557 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑀𝑗)
265264adantl 473 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀𝑗)
266263zred 11694 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ ℝ)
267204adantr 472 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑁 ∈ ℝ)
268203adantr 472 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑖 ∈ ℝ)
269 1red 10267 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 1 ∈ ℝ)
270268, 269resubcld 10670 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑖 − 1) ∈ ℝ)
271 elfzle2 12558 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑗 ≤ (𝑖 − 1))
272271adantl 473 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ≤ (𝑖 − 1))
273268ltm1d 11168 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑖 − 1) < 𝑖)
274266, 270, 268, 272, 273lelttrd 10407 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 < 𝑖)
275210adantr 472 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑖 < 𝑁)
276266, 268, 267, 274, 275lttrd 10410 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 < 𝑁)
277266, 267, 276ltled 10397 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗𝑁)
278212adantr 472 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
279278, 257syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀𝑗𝑗𝑁)))
280263, 265, 277, 279mpbir3and 1428 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ (𝑀...𝑁))
281261, 280ffvelrnd 6524 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑃𝑗) ∈ ℝ)
282263peano2zd 11697 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ∈ ℤ)
283181ad2antrr 764 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 ∈ ℝ)
284266, 269readdcld 10281 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ∈ ℝ)
28550adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 ∈ ℝ)
286262zred 11694 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑗 ∈ ℝ)
287286adantl 473 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ ℝ)
288 1red 10267 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (𝑀...(𝑖 − 1))) → 1 ∈ ℝ)
289287, 288readdcld 10281 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ∈ ℝ)
290264adantl 473 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀𝑗)
291287ltp1d 11166 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 < (𝑗 + 1))
292285, 287, 289, 290, 291lelttrd 10407 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 < (𝑗 + 1))
293292ad4ant14 1209 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 < (𝑗 + 1))
294283, 284, 293ltled 10397 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 ≤ (𝑗 + 1))
295 zltp1le 11639 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑗 < 𝑖 ↔ (𝑗 + 1) ≤ 𝑖))
296262, 200, 295syl2anr 496 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 < 𝑖 ↔ (𝑗 + 1) ≤ 𝑖))
297274, 296mpbid 222 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ≤ 𝑖)
298284, 268, 267, 297, 275lelttrd 10407 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) < 𝑁)
299284, 267, 298ltled 10397 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ≤ 𝑁)
300 elfz1 12544 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑗 + 1) ∈ (𝑀...𝑁) ↔ ((𝑗 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑗 + 1) ∧ (𝑗 + 1) ≤ 𝑁)))
301278, 300syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → ((𝑗 + 1) ∈ (𝑀...𝑁) ↔ ((𝑗 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑗 + 1) ∧ (𝑗 + 1) ≤ 𝑁)))
302282, 294, 299, 301mpbir3and 1428 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ∈ (𝑀...𝑁))
303261, 302ffvelrnd 6524 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑃‘(𝑗 + 1)) ∈ ℝ)
304 simplll 815 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝜑)
305 elfzuz 12551 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑗 ∈ (ℤ𝑀))
306305adantl 473 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ (ℤ𝑀))
307304, 5syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑁 ∈ ℤ)
308 elfzo2 12687 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑀..^𝑁) ↔ (𝑗 ∈ (ℤ𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑗 < 𝑁))
309306, 307, 276, 308syl3anbrc 1429 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ (𝑀..^𝑁))
310 eleq1 2827 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → (𝑖 ∈ (𝑀..^𝑁) ↔ 𝑗 ∈ (𝑀..^𝑁)))
311310anbi2d 742 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → ((𝜑𝑖 ∈ (𝑀..^𝑁)) ↔ (𝜑𝑗 ∈ (𝑀..^𝑁))))
312 fveq2 6353 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → (𝑃𝑖) = (𝑃𝑗))
313 oveq1 6821 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
314313fveq2d 6357 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑗 + 1)))
315312, 314breq12d 4817 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → ((𝑃𝑖) < (𝑃‘(𝑖 + 1)) ↔ (𝑃𝑗) < (𝑃‘(𝑗 + 1))))
316311, 315imbi12d 333 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑗 → (((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑃𝑖) < (𝑃‘(𝑖 + 1))) ↔ ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑃𝑗) < (𝑃‘(𝑗 + 1)))))
317316, 145chvarv 2408 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑃𝑗) < (𝑃‘(𝑗 + 1)))
318304, 309, 317syl2anc 696 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑃𝑗) < (𝑃‘(𝑗 + 1)))
319281, 303, 318ltled 10397 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑃𝑗) ≤ (𝑃‘(𝑗 + 1)))
320242, 260, 319monoord 13045 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑃𝑀) ≤ (𝑃𝑖))
321320adantr 472 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃𝑀) ≤ (𝑃𝑖))
322216rexrd 10301 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃𝑖) ∈ ℝ*)
323237rexrd 10301 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘(𝑖 + 1)) ∈ ℝ*)
324 iccgelb 12443 . . . . . . . . . . . . 13 (((𝑃𝑖) ∈ ℝ* ∧ (𝑃‘(𝑖 + 1)) ∈ ℝ*𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃𝑖) ≤ 𝑡)
325322, 323, 238, 324syl3anc 1477 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃𝑖) ≤ 𝑡)
326197, 216, 240, 321, 325letrd 10406 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃𝑀) ≤ 𝑡)
327194, 66syl 17 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃𝑁) ∈ ℝ)
328 iccleub 12442 . . . . . . . . . . . . 13 (((𝑃𝑖) ∈ ℝ* ∧ (𝑃‘(𝑖 + 1)) ∈ ℝ*𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ≤ (𝑃‘(𝑖 + 1)))
329322, 323, 238, 328syl3anc 1477 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ≤ (𝑃‘(𝑖 + 1)))
3305ad2antrr 764 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑁 ∈ ℤ)
331 eluz 11913 . . . . . . . . . . . . . . . 16 (((𝑖 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ‘(𝑖 + 1)) ↔ (𝑖 + 1) ≤ 𝑁))
332217, 330, 331syl2anc 696 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑁 ∈ (ℤ‘(𝑖 + 1)) ↔ (𝑖 + 1) ≤ 𝑁))
333233, 332mpbird 247 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑁 ∈ (ℤ‘(𝑖 + 1)))
334333adantr 472 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑁 ∈ (ℤ‘(𝑖 + 1)))
33548ad3antrrr 768 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ)
336 elfzelz 12555 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ((𝑖 + 1)...𝑁) → 𝑗 ∈ ℤ)
337336adantl 473 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑗 ∈ ℤ)
338 elfzel1 12554 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (𝑀...𝑘) → 𝑀 ∈ ℤ)
339338zred 11694 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (𝑀...𝑘) → 𝑀 ∈ ℝ)
340339adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀 ∈ ℝ)
341336zred 11694 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ((𝑖 + 1)...𝑁) → 𝑗 ∈ ℝ)
342341adantl 473 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑗 ∈ ℝ)
343221adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑖 ∈ ℝ)
344 1red 10267 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 1 ∈ ℝ)
345343, 344readdcld 10281 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑖 + 1) ∈ ℝ)
346201adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀𝑖)
347343ltp1d 11166 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑖 < (𝑖 + 1))
348340, 343, 345, 346, 347lelttrd 10407 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀 < (𝑖 + 1))
349 elfzle1 12557 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ((𝑖 + 1)...𝑁) → (𝑖 + 1) ≤ 𝑗)
350349adantl 473 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑖 + 1) ≤ 𝑗)
351340, 345, 342, 348, 350ltletrd 10409 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀 < 𝑗)
352340, 342, 351ltled 10397 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀𝑗)
353352adantll 752 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀𝑗)
354 elfzle2 12558 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ((𝑖 + 1)...𝑁) → 𝑗𝑁)
355354adantl 473 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑗𝑁)
356212adantr 472 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
357356, 257syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀𝑗𝑗𝑁)))
358337, 353, 355, 357mpbir3and 1428 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑗 ∈ (𝑀...𝑁))
359335, 358ffvelrnd 6524 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑃𝑗) ∈ ℝ)
360359adantlr 753 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑃𝑗) ∈ ℝ)
361 simplll 815 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝜑)
362 simplr 809 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑘))
363 simpr 479 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1)))
364483ad2ant1 1128 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
365 elfzelz 12555 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1)) → 𝑗 ∈ ℤ)
3663653ad2ant3 1130 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ℤ)
367503ad2ant1 1128 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℝ)
368366zred 11694 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ℝ)
3692243adant3 1127 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ)
3702273adant3 1127 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 < (𝑖 + 1))
371 elfzle1 12557 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1)) → (𝑖 + 1) ≤ 𝑗)
3723713ad2ant3 1130 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑗)
373367, 369, 368, 370, 372ltletrd 10409 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 < 𝑗)
374367, 368, 373ltled 10397 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀𝑗)
375365adantl 473 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ℤ)
376375zred 11694 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ℝ)
37710adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℝ)
378 1red 10267 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
379377, 378resubcld 10670 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
380 elfzle2 12558 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1)) → 𝑗 ≤ (𝑁 − 1))
381380adantl 473 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ≤ (𝑁 − 1))
382377ltm1d 11168 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
383376, 379, 377, 381, 382lelttrd 10407 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 < 𝑁)
384376, 377, 383ltled 10397 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗𝑁)
3853843adant2 1126 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗𝑁)
386983ad2ant1 1128 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
387386, 257syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀𝑗𝑗𝑁)))
388366, 374, 385, 387mpbir3and 1428 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ (𝑀...𝑁))
389364, 388ffvelrnd 6524 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃𝑗) ∈ ℝ)
390366peano2zd 11697 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ∈ ℤ)
391390zred 11694 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ∈ ℝ)
3922213ad2ant2 1129 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
393 1red 10267 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
3942263adant3 1127 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖 < (𝑖 + 1))
395392, 369, 368, 394, 372ltletrd 10409 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖 < 𝑗)
396392, 368, 395ltled 10397 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖𝑗)
397392, 368, 393, 396leadd1dd 10853 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ (𝑗 + 1))
398367, 369, 391, 370, 397ltletrd 10409 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 < (𝑗 + 1))
399367, 391, 398ltled 10397 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 ≤ (𝑗 + 1))
400 zltp1le 11639 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 < 𝑁 ↔ (𝑗 + 1) ≤ 𝑁))
401365, 5, 400syl2anr 496 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 < 𝑁 ↔ (𝑗 + 1) ≤ 𝑁))
402383, 401mpbid 222 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ≤ 𝑁)
4034023adant2 1126 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ≤ 𝑁)
404386, 300syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → ((𝑗 + 1) ∈ (𝑀...𝑁) ↔ ((𝑗 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑗 + 1) ∧ (𝑗 + 1) ≤ 𝑁)))
405390, 399, 403, 404mpbir3and 1428 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ∈ (𝑀...𝑁))
406364, 405ffvelrnd 6524 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃‘(𝑗 + 1)) ∈ ℝ)
407 simp1 1131 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝜑)
40813ad2ant1 1128 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℤ)
409 eluz 11913 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑗 ∈ (ℤ𝑀) ↔ 𝑀𝑗))
410408, 366, 409syl2anc 696 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 ∈ (ℤ𝑀) ↔ 𝑀𝑗))
411374, 410mpbird 247 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ (ℤ𝑀))
41253ad2ant1 1128 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℤ)
4133833adant2 1126 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 < 𝑁)
414411, 412, 413, 308syl3anbrc 1429 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ (𝑀..^𝑁))
415407, 414, 317syl2anc 696 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃𝑗) < (𝑃‘(𝑗 + 1)))
416389, 406, 415ltled 10397 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃𝑗) ≤ (𝑃‘(𝑗 + 1)))
417361, 362, 363, 416syl3anc 1477 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃𝑗) ≤ (𝑃‘(𝑗 + 1)))
418417adantlr 753 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃𝑗) ≤ (𝑃‘(𝑗 + 1)))
419334, 360, 418monoord 13045 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘(𝑖 + 1)) ≤ (𝑃𝑁))
420240, 237, 327, 329, 419letrd 10406 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ≤ (𝑃𝑁))
42166rexrd 10301 . . . . . . . . . . . . . 14 (𝜑 → (𝑃𝑁) ∈ ℝ*)
42278, 421jca 555 . . . . . . . . . . . . 13 (𝜑 → ((𝑃𝑀) ∈ ℝ* ∧ (𝑃𝑁) ∈ ℝ*))
423194, 422syl 17 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → ((𝑃𝑀) ∈ ℝ* ∧ (𝑃𝑁) ∈ ℝ*))
424 elicc1 12432 . . . . . . . . . . . 12 (((𝑃𝑀) ∈ ℝ* ∧ (𝑃𝑁) ∈ ℝ*) → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)) ↔ (𝑡 ∈ ℝ* ∧ (𝑃𝑀) ≤ 𝑡𝑡 ≤ (𝑃𝑁))))
425423, 424syl 17 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)) ↔ (𝑡 ∈ ℝ* ∧ (𝑃𝑀) ≤ 𝑡𝑡 ≤ (𝑃𝑁))))
426196, 326, 420, 425mpbir3and 1428 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)))
427194, 426, 152syl2anc 696 . . . . . . . . 9 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝐴 ∈ ℂ)
428 simpll 807 . . . . . . . . . 10 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝜑)
429242, 330, 210, 143syl3anbrc 1429 . . . . . . . . . 10 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ (𝑀..^𝑁))
430428, 429, 167syl2anc 696 . . . . . . . . 9 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1)
431427, 430itgcl 23769 . . . . . . . 8 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → ∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ∈ ℂ)
432 fveq2 6353 . . . . . . . . . 10 (𝑖 = 𝑘 → (𝑃𝑖) = (𝑃𝑘))
433 oveq1 6821 . . . . . . . . . . 11 (𝑖 = 𝑘 → (𝑖 + 1) = (𝑘 + 1))
434433fveq2d 6357 . . . . . . . . . 10 (𝑖 = 𝑘 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑘 + 1)))
435432, 434oveq12d 6832 . . . . . . . . 9 (𝑖 = 𝑘 → ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) = ((𝑃𝑘)[,](𝑃‘(𝑘 + 1))))
436435itgeq1d 40693 . . . . . . . 8 (𝑖 = 𝑘 → ∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡)
437193, 431, 436fzosump1 14700 . . . . . . 7 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
4384373adant3 1127 . . . . . 6 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
439 oveq1 6821 . . . . . . . 8 (∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 → (∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
440439eqcomd 2766 . . . . . . 7 (∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 → (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = (∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
4414403ad2ant3 1130 . . . . . 6 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = (∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
44277adantr 472 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑀) ∈ ℝ)
44348adantr 472 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ)
444182adantl 473 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ ℤ)
445444peano2zd 11697 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ ℤ)
446445zred 11694 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ ℝ)
447184ltp1d 11166 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 < (𝑘 + 1))
448181, 184, 446, 189, 447lttrd 10410 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < (𝑘 + 1))
449181, 446, 448ltled 10397 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ≤ (𝑘 + 1))
450208adantl 473 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 < 𝑁)
451 zltp1le 11639 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 < 𝑁 ↔ (𝑘 + 1) ≤ 𝑁))
452182, 5, 451syl2anr 496 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 < 𝑁 ↔ (𝑘 + 1) ≤ 𝑁))
453450, 452mpbid 222 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ≤ 𝑁)
45498adantr 472 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
455 elfz1 12544 . . . . . . . . . . . 12 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑘 + 1) ∈ (𝑀...𝑁) ↔ ((𝑘 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁)))
456454, 455syl 17 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ((𝑘 + 1) ∈ (𝑀...𝑁) ↔ ((𝑘 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁)))
457445, 449, 453, 456mpbir3and 1428 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ (𝑀...𝑁))
458443, 457ffvelrnd 6524 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ∈ ℝ)
45910adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ ℝ)
460184, 459, 450ltled 10397 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘𝑁)
461 elfz1 12544 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘𝑁)))
462454, 461syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘𝑁)))
463444, 190, 460, 462mpbir3and 1428 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (𝑀...𝑁))
464443, 463ffvelrnd 6524 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑘) ∈ ℝ)
465464rexrd 10301 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑘) ∈ ℝ*)
46648ad2antrr 764 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑃:(𝑀...𝑁)⟶ℝ)
467466, 214ffvelrnd 6524 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑃𝑖) ∈ ℝ)
46848ad2antrr 764 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
469 elfzelz 12555 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ∈ ℤ)
470469adantl 473 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ ℤ)
471 elfzle1 12557 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑀𝑖)
472471adantl 473 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀𝑖)
473470zred 11694 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ ℝ)
47410ad2antrr 764 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑁 ∈ ℝ)
475184adantr 472 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑘 ∈ ℝ)
476 1red 10267 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 1 ∈ ℝ)
477475, 476resubcld 10670 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑘 − 1) ∈ ℝ)
478 elfzle2 12558 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ≤ (𝑘 − 1))
479478adantl 473 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ≤ (𝑘 − 1))
480475ltm1d 11168 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑘 − 1) < 𝑘)
481473, 477, 475, 479, 480lelttrd 10407 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 < 𝑘)
482450adantr 472 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑘 < 𝑁)
483473, 475, 474, 481, 482lttrd 10410 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 < 𝑁)
484473, 474, 483ltled 10397 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖𝑁)
48598ad2antrr 764 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
486485, 100syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀𝑖𝑖𝑁)))
487470, 472, 484, 486mpbir3and 1428 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (𝑀...𝑁))
488468, 487ffvelrnd 6524 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃𝑖) ∈ ℝ)
489470peano2zd 11697 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ∈ ℤ)
49050ad2antrr 764 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 ∈ ℝ)
491473, 476readdcld 10281 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ∈ ℝ)
492473ltp1d 11166 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 < (𝑖 + 1))
493490, 473, 491, 472, 492lelttrd 10407 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 < (𝑖 + 1))
494490, 491, 493ltled 10397 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 ≤ (𝑖 + 1))
495 zltp1le 11639 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑖 < 𝑘 ↔ (𝑖 + 1) ≤ 𝑘))
496469, 444, 495syl2anr 496 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 < 𝑘 ↔ (𝑖 + 1) ≤ 𝑘))
497481, 496mpbid 222 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ≤ 𝑘)
498491, 475, 474, 497, 482lelttrd 10407 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) < 𝑁)
499491, 474, 498ltled 10397 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ≤ 𝑁)
500485, 135syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
501489, 494, 499, 500mpbir3and 1428 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁))
502468, 501ffvelrnd 6524 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
503 simpll 807 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝜑)
504 elfzuz 12551 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ∈ (ℤ𝑀))
505504adantl 473 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (ℤ𝑀))
5065ad2antrr 764 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑁 ∈ ℤ)
507505, 506, 483, 143syl3anbrc 1429 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (𝑀..^𝑁))
508503, 507, 145syl2anc 696 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃𝑖) < (𝑃‘(𝑖 + 1)))
509488, 502, 508ltled 10397 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃𝑖) ≤ (𝑃‘(𝑖 + 1)))
510193, 467, 509monoord 13045 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑀) ≤ (𝑃𝑘))
5115adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ ℤ)
512 elfzo2 12687 . . . . . . . . . . . . 13 (𝑘 ∈ (𝑀..^𝑁) ↔ (𝑘 ∈ (ℤ𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑘 < 𝑁))
513193, 511, 450, 512syl3anbrc 1429 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (𝑀..^𝑁))
514 eleq1 2827 . . . . . . . . . . . . . . 15 (𝑖 = 𝑘 → (𝑖 ∈ (𝑀..^𝑁) ↔ 𝑘 ∈ (𝑀..^𝑁)))
515514anbi2d 742 . . . . . . . . . . . . . 14 (𝑖 = 𝑘 → ((𝜑𝑖 ∈ (𝑀..^𝑁)) ↔ (𝜑𝑘 ∈ (𝑀..^𝑁))))
516432, 434breq12d 4817 . . . . . . . . . . . . . 14 (𝑖 = 𝑘 → ((𝑃𝑖) < (𝑃‘(𝑖 + 1)) ↔ (𝑃𝑘) < (𝑃‘(𝑘 + 1))))
517515, 516imbi12d 333 . . . . . . . . . . . . 13 (𝑖 = 𝑘 → (((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑃𝑖) < (𝑃‘(𝑖 + 1))) ↔ ((𝜑𝑘 ∈ (𝑀..^𝑁)) → (𝑃𝑘) < (𝑃‘(𝑘 + 1)))))
518517, 145chvarv 2408 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (𝑀..^𝑁)) → (𝑃𝑘) < (𝑃‘(𝑘 + 1)))
519513, 518syldan 488 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑘) < (𝑃‘(𝑘 + 1)))
520464, 458, 519ltled 10397 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑘) ≤ (𝑃‘(𝑘 + 1)))
52178adantr 472 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑀) ∈ ℝ*)
522458rexrd 10301 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ∈ ℝ*)
523 elicc1 12432 . . . . . . . . . . 11 (((𝑃𝑀) ∈ ℝ* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ*) → ((𝑃𝑘) ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))) ↔ ((𝑃𝑘) ∈ ℝ* ∧ (𝑃𝑀) ≤ (𝑃𝑘) ∧ (𝑃𝑘) ≤ (𝑃‘(𝑘 + 1)))))
524521, 522, 523syl2anc 696 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ((𝑃𝑘) ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))) ↔ ((𝑃𝑘) ∈ ℝ* ∧ (𝑃𝑀) ≤ (𝑃𝑘) ∧ (𝑃𝑘) ≤ (𝑃‘(𝑘 + 1)))))
525465, 510, 520, 524mpbir3and 1428 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑘) ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))))
526 simpll 807 . . . . . . . . . 10 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝜑)
527 eliccxr 40258 . . . . . . . . . . . 12 (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))) → 𝑡 ∈ ℝ*)
528527adantl 473 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ℝ*)
52978ad2antrr 764 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃𝑀) ∈ ℝ*)
530522adantr 472 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ∈ ℝ*)
531 simpr 479 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))))
532 iccgelb 12443 . . . . . . . . . . . 12 (((𝑃𝑀) ∈ ℝ* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ*𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃𝑀) ≤ 𝑡)
533529, 530, 531, 532syl3anc 1477 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃𝑀) ≤ 𝑡)
53477ad2antrr 764 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃𝑀) ∈ ℝ)
535458adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ∈ ℝ)
536 eliccre 40249 . . . . . . . . . . . . 13 (((𝑃𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ℝ)
537534, 535, 531, 536syl3anc 1477 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ℝ)
53866ad2antrr 764 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃𝑁) ∈ ℝ)
539 iccleub 12442 . . . . . . . . . . . . 13 (((𝑃𝑀) ∈ ℝ* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ*𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ≤ (𝑃‘(𝑘 + 1)))
540529, 530, 531, 539syl3anc 1477 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ≤ (𝑃‘(𝑘 + 1)))
541 eluz2 11905 . . . . . . . . . . . . . . 15 (𝑁 ∈ (ℤ‘(𝑘 + 1)) ↔ ((𝑘 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑘 + 1) ≤ 𝑁))
542445, 511, 453, 541syl3anbrc 1429 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ (ℤ‘(𝑘 + 1)))
54348ad2antrr 764 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ)
5441ad2antrr 764 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 ∈ ℤ)
5455ad2antrr 764 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑁 ∈ ℤ)
546 elfzelz 12555 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖 ∈ ℤ)
547546adantl 473 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℤ)
548544, 545, 5473jca 1123 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ))
54950ad2antrr 764 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 ∈ ℝ)
550547zred 11694 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℝ)
551184adantr 472 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 ∈ ℝ)
552189adantr 472 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 < 𝑘)
553183adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 ∈ ℝ)
554 1red 10267 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 1 ∈ ℝ)
555553, 554readdcld 10281 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑘 + 1) ∈ ℝ)
556546zred 11694 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖 ∈ ℝ)
557556adantl 473 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℝ)
558553ltp1d 11166 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < (𝑘 + 1))
559 elfzle1 12557 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ ((𝑘 + 1)...𝑁) → (𝑘 + 1) ≤ 𝑖)
560559adantl 473 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑘 + 1) ≤ 𝑖)
561553, 555, 557, 558, 560ltletrd 10409 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < 𝑖)
562561adantll 752 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < 𝑖)
563549, 551, 550, 552, 562lttrd 10410 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 < 𝑖)
564549, 550, 563ltled 10397 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀𝑖)
565 elfzle2 12558 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖𝑁)
566565adantl 473 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖𝑁)
567548, 564, 566jca32 559 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑀𝑖𝑖𝑁)))
568 elfz2 12546 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑀𝑖𝑖𝑁)))
569567, 568sylibr 224 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ (𝑀...𝑁))
570543, 569ffvelrnd 6524 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑃𝑖) ∈ ℝ)
57148ad2antrr 764 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
5721ad2antrr 764 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℤ)
5735ad2antrr 764 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℤ)
574 elfzelz 12555 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ∈ ℤ)
575574adantl 473 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℤ)
576572, 573, 5753jca 1123 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ))
57750ad2antrr 764 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℝ)
578575zred 11694 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
579184adantr 472 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 ∈ ℝ)
580189adantr 472 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < 𝑘)
581183adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 ∈ ℝ)
582 1red 10267 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
583581, 582readdcld 10281 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑘 + 1) ∈ ℝ)
584574zred 11694 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ∈ ℝ)
585584adantl 473 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
586581ltp1d 11166 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < (𝑘 + 1))
587 elfzle1 12557 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → (𝑘 + 1) ≤ 𝑖)
588587adantl 473 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑘 + 1) ≤ 𝑖)
589581, 583, 585, 586, 588ltletrd 10409 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < 𝑖)
590589adantll 752 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < 𝑖)
591577, 579, 578, 580, 590lttrd 10410 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < 𝑖)
592577, 578, 591ltled 10397 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀𝑖)
593584adantl 473 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
59410adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℝ)
595 1red 10267 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
596594, 595resubcld 10670 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
597 elfzle2 12558 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ≤ (𝑁 − 1))
598597adantl 473 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ≤ (𝑁 − 1))
599594ltm1d 11168 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
600593, 596, 594, 598, 599lelttrd 10407 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 < 𝑁)
601593, 594, 600ltled 10397 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖𝑁)
602601adantlr 753 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖𝑁)
603576, 592, 602jca32 559 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑀𝑖𝑖𝑁)))
604603, 568sylibr 224 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑁))
605571, 604ffvelrnd 6524 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃𝑖) ∈ ℝ)
606575peano2zd 11697 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℤ)
607572, 573, 6063jca 1123 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ))
608606zred 11694 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ)
609578ltp1d 11166 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 < (𝑖 + 1))
610579, 578, 608, 590, 609lttrd 10410 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < (𝑖 + 1))
611577, 579, 608, 580, 610lttrd 10410 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < (𝑖 + 1))
612577, 608, 611ltled 10397 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ≤ (𝑖 + 1))
613600adantlr 753 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 < 𝑁)
614574, 511, 132syl2anr 496 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
615613, 614mpbid 222 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁)
616607, 612, 615jca32 559 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ) ∧ (𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
617 elfz2 12546 . . . . . . . . . . . . . . . . 17 ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ) ∧ (𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
618616, 617sylibr 224 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁))
619571, 618ffvelrnd 6524 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
620 simpll 807 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝜑)
621 eluz2 11905 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 𝑀𝑖))
622572, 575, 592, 621syl3anbrc 1429 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (ℤ𝑀))
623622, 573, 613, 143syl3anbrc 1429 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀..^𝑁))
624620, 623, 145syl2anc 696 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃𝑖) < (𝑃‘(𝑖 + 1)))
625605, 619, 624ltled 10397 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃𝑖) ≤ (𝑃‘(𝑖 + 1)))
626542, 570, 625monoord 13045 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ≤ (𝑃𝑁))
627626adantr 472 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ≤ (𝑃𝑁))
628537, 535, 538, 540, 627letrd 10406 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ≤ (𝑃𝑁))
629422ad2antrr 764 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → ((𝑃𝑀) ∈ ℝ* ∧ (𝑃𝑁) ∈ ℝ*))
630629, 424syl 17 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)) ↔ (𝑡 ∈ ℝ* ∧ (𝑃𝑀) ≤ 𝑡𝑡 ≤ (𝑃𝑁))))
631528, 533, 628, 630mpbir3and 1428 . . . . . . . . . 10 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)))
632526, 631, 152syl2anc 696 . . . . . . . . 9 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝐴 ∈ ℂ)
633 nfv 1992 . . . . . . . . . 10 𝑡(𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁))
6341adantr 472 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ∈ ℤ)
635 elfzouz 12688 . . . . . . . . . . 11 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 ∈ (ℤ‘(𝑀 + 1)))
636635adantl 473 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (ℤ‘(𝑀 + 1)))
637 simpll 807 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝜑)
638 elfzouz 12688 . . . . . . . . . . . . 13 (𝑖 ∈ (𝑀..^𝑘) → 𝑖 ∈ (ℤ𝑀))
639638adantl 473 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 ∈ (ℤ𝑀))
6405ad2antrr 764 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑁 ∈ ℤ)
641 elfzoelz 12684 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀..^𝑘) → 𝑖 ∈ ℤ)
642641zred 11694 . . . . . . . . . . . . . 14 (𝑖 ∈ (𝑀..^𝑘) → 𝑖 ∈ ℝ)
643642adantl 473 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 ∈ ℝ)
644184adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑘 ∈ ℝ)
64510ad2antrr 764 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑁 ∈ ℝ)
646 elfzolt2 12693 . . . . . . . . . . . . . 14 (𝑖 ∈ (𝑀..^𝑘) → 𝑖 < 𝑘)
647646adantl 473 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 < 𝑘)
648450adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑘 < 𝑁)
649643, 644, 645, 647, 648lttrd 10410 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 < 𝑁)
650639, 640, 649, 143syl3anbrc 1429 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 ∈ (𝑀..^𝑁))
651637, 650, 145syl2anc 696 . . . . . . . . . 10 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → (𝑃𝑖) < (𝑃‘(𝑖 + 1)))
652 simpll 807 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → 𝜑)
65377ad2antrr 764 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → (𝑃𝑀) ∈ ℝ)
65466ad2antrr 764 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → (𝑃𝑁) ∈ ℝ)
655464adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → (𝑃𝑘) ∈ ℝ)
656 simpr 479 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)))
657 eliccre 40249 . . . . . . . . . . . . 13 (((𝑃𝑀) ∈ ℝ ∧ (𝑃𝑘) ∈ ℝ ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → 𝑡 ∈ ℝ)
658653, 655, 656, 657syl3anc 1477 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → 𝑡 ∈ ℝ)
65978ad2antrr 764 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → (𝑃𝑀) ∈ ℝ*)
660465adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → (𝑃𝑘) ∈ ℝ*)
661 iccgelb 12443 . . . . . . . . . . . . 13 (((𝑃𝑀) ∈ ℝ* ∧ (𝑃𝑘) ∈ ℝ*𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → (𝑃𝑀) ≤ 𝑡)
662659, 660, 656, 661syl3anc 1477 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → (𝑃𝑀) ≤ 𝑡)
663 iccleub 12442 . . . . . . . . . . . . . 14 (((𝑃𝑀) ∈ ℝ* ∧ (𝑃𝑘) ∈ ℝ*𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → 𝑡 ≤ (𝑃𝑘))
664659, 660, 656, 663syl3anc 1477 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → 𝑡 ≤ (𝑃𝑘))
665 elfzouz2 12698 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑁 ∈ (ℤ𝑘))
666665adantl 473 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ (ℤ𝑘))
66748ad2antrr 764 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ)
6681ad2antrr 764 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀 ∈ ℤ)
6695ad2antrr 764 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑁 ∈ ℤ)
670 elfzelz 12555 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (𝑘...𝑁) → 𝑖 ∈ ℤ)
671670adantl 473 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑖 ∈ ℤ)
672668, 669, 6713jca 1123 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ))
67350ad2antrr 764 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀 ∈ ℝ)
674671zred 11694 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑖 ∈ ℝ)
675184adantr 472 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑘 ∈ ℝ)
676189adantr 472 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀 < 𝑘)
677 elfzle1 12557 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (𝑘...𝑁) → 𝑘𝑖)
678677adantl 473 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑘𝑖)
679673, 675, 674, 676, 678ltletrd 10409 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀 < 𝑖)
680673, 674, 679ltled 10397 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀𝑖)
681 elfzle2 12558 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (𝑘...𝑁) → 𝑖𝑁)
682681adantl 473 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑖𝑁)
683672, 680, 682jca32 559 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑀𝑖𝑖𝑁)))
684683, 568sylibr 224 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑖 ∈ (𝑀...𝑁))
685667, 684ffvelrnd 6524 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → (𝑃𝑖) ∈ ℝ)
68648ad2antrr 764 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
6871ad2antrr 764 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 ∈ ℤ)
6885ad2antrr 764 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑁 ∈ ℤ)
689 elfzelz 12555 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (𝑘...(𝑁 − 1)) → 𝑖 ∈ ℤ)
690689adantl 473 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ ℤ)
691687, 688, 6903jca 1123 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ))
69250ad2antrr 764 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 ∈ ℝ)
693690zred 11694 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ ℝ)
694184adantr 472 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑘 ∈ ℝ)
695189adantr 472 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 < 𝑘)
696 elfzle1 12557 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (𝑘...(𝑁 − 1)) → 𝑘𝑖)
697696adantl 473 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑘𝑖)
698692, 694, 693, 695, 697ltletrd 10409 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 < 𝑖)
699692, 693, 698ltled 10397 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀𝑖)
700689zred 11694 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (𝑘...(𝑁 − 1)) → 𝑖 ∈ ℝ)
701700adantl 473 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ ℝ)
70210adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑁 ∈ ℝ)
703 1red 10267 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → 1 ∈ ℝ)
704702, 703resubcld 10670 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
705 elfzle2 12558 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (𝑘...(𝑁 − 1)) → 𝑖 ≤ (𝑁 − 1))
706705adantl 473 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ≤ (𝑁 − 1))
707702ltm1d 11168 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
708701, 704, 702, 706, 707lelttrd 10407 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 < 𝑁)
709701, 702, 708ltled 10397 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖𝑁)
710709adantlr 753 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖𝑁)
711691, 699, 710jca32 559 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑀𝑖𝑖𝑁)))
712711, 568sylibr 224 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑁))
713686, 712ffvelrnd 6524 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑃𝑖) ∈ ℝ)
714690peano2zd 11697 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ∈ ℤ)
715687, 688, 7143jca 1123 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ))
716714zred 11694 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ)
717693ltp1d 11166 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 < (𝑖 + 1))
718692, 693, 716, 699, 717lelttrd 10407 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 < (𝑖 + 1))
719692, 716, 718ltled 10397 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 ≤ (𝑖 + 1))
720689, 5, 132syl2anr 496 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
721708, 720mpbid 222 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁)
722721adantlr 753 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁)
723715, 719, 722jca32 559 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ) ∧ (𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
724723, 617sylibr 224 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁))
725686, 724ffvelrnd 6524 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
726 simpll 807 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝜑)
727687, 690, 699, 621syl3anbrc 1429 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ (ℤ𝑀))
728708adantlr 753 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 < 𝑁)
729727, 688, 728, 143syl3anbrc 1429 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ (𝑀..^𝑁))
730726, 729, 145syl2anc 696 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑃𝑖) < (𝑃‘(𝑖 + 1)))
731713, 725, 730ltled 10397 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑃𝑖) ≤ (𝑃‘(𝑖 + 1)))
732666, 685, 731monoord 13045 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑘) ≤ (𝑃𝑁))
733732adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → (𝑃𝑘) ≤ (𝑃𝑁))
734658, 655, 654, 664, 733letrd 10406 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → 𝑡 ≤ (𝑃𝑁))
735653, 654, 658, 662, 734eliccd 40247 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)))
736652, 735, 152syl2anc 696 . . . . . . . . . 10 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → 𝐴 ∈ ℂ)
737637, 650, 167syl2anc 696 . . . . . . . . . 10 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1)
738633, 634, 636, 467, 651, 736, 737iblspltprt 40710 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)) ↦ 𝐴) ∈ 𝐿1)
739435mpteq1d 4890 . . . . . . . . . . . . 13 (𝑖 = 𝑘 → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) = (𝑡 ∈ ((𝑃𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴))
740739eleq1d 2824 . . . . . . . . . . . 12 (𝑖 = 𝑘 → ((𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1))
741515, 740imbi12d 333 . . . . . . . . . . 11 (𝑖 = 𝑘 → (((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1) ↔ ((𝜑𝑘 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1)))
742741, 167chvarv 2408 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1)
743513, 742syldan 488 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑡 ∈ ((𝑃𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1)
744442, 458, 525, 632, 738, 743itgspliticc 23822 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ∫((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = (∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
745744eqcomd 2766 . . . . . . 7 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = ∫((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡)
7467453adant3 1127 . . . . . 6 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → (∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = ∫((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡)
747438, 441, 7463eqtrrd 2799 . . . . 5 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → ∫((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
748177, 178, 180, 747syl3anc 1477 . . . 4 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → ∫((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
7497483exp 1113 . . 3 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → ((𝜑 → ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → (𝜑 → ∫((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)))
75021, 28, 35, 42, 176, 749fzind2 12800 . 2 (𝑁 ∈ ((𝑀 + 1)...𝑁) → (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑁))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
75114, 750mpcom 38 1 (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑁))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1632  wcel 2139   class class class wbr 4804  cmpt 4881  wf 6045  cfv 6049  (class class class)co 6814  cc 10146  cr 10147  1c1 10149   + caddc 10151  *cxr 10285   < clt 10286  cle 10287  cmin 10478  cz 11589  cuz 11899  [,]cicc 12391  ...cfz 12539  ..^cfzo 12679  Σcsu 14635  𝐿1cibl 23605  citg 23606
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-inf2 8713  ax-cnex 10204  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-mulcom 10212  ax-addass 10213  ax-mulass 10214  ax-distr 10215  ax-i2m1 10216  ax-1ne0 10217  ax-1rid 10218  ax-rnegex 10219  ax-rrecex 10220  ax-cnre 10221  ax-pre-lttri 10222  ax-pre-lttrn 10223  ax-pre-ltadd 10224  ax-pre-mulgt0 10225  ax-pre-sup 10226  ax-addf 10227
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-disj 4773  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6775  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-of 7063  df-ofr 7064  df-om 7232  df-1st 7334  df-2nd 7335  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-1o 7730  df-2o 7731  df-oadd 7734  df-er 7913  df-map 8027  df-pm 8028  df-en 8124  df-dom 8125  df-sdom 8126  df-fin 8127  df-fi 8484  df-sup 8515  df-inf 8516  df-oi 8582  df-card 8975  df-cda 9202  df-pnf 10288  df-mnf 10289  df-xr 10290  df-ltxr 10291  df-le 10292  df-sub 10480  df-neg 10481  df-div 10897  df-nn 11233  df-2 11291  df-3 11292  df-4 11293  df-n0 11505  df-z 11590  df-uz 11900  df-q 12002  df-rp 12046  df-xneg 12159  df-xadd 12160  df-xmul 12161  df-ioo 12392  df-ico 12394  df-icc 12395  df-fz 12540  df-fzo 12680  df-fl 12807  df-mod 12883  df-seq 13016  df-exp 13075  df-hash 13332  df-cj 14058  df-re 14059  df-im 14060  df-sqrt 14194  df-abs 14195  df-clim 14438  df-sum 14636  df-rest 16305  df-topgen 16326  df-psmet 19960  df-xmet 19961  df-met 19962  df-bl 19963  df-mopn 19964  df-top 20921  df-topon 20938  df-bases 20972  df-cmp 21412  df-ovol 23453  df-vol 23454  df-mbf 23607  df-itg1 23608  df-itg2 23609  df-ibl 23610  df-itg 23611
This theorem is referenced by:  fourierdlem73  40917  fourierdlem81  40925  fourierdlem93  40937
  Copyright terms: Public domain W3C validator