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 39502
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 11429 . . . . 5 (𝜑 → (𝑀 + 1) ∈ ℤ)
3 itgspltprt.2 . . . . . 6 (𝜑𝑁 ∈ (ℤ‘(𝑀 + 1)))
4 eluzelz 11641 . . . . . 6 (𝑁 ∈ (ℤ‘(𝑀 + 1)) → 𝑁 ∈ ℤ)
53, 4syl 17 . . . . 5 (𝜑𝑁 ∈ ℤ)
62, 5, 53jca 1240 . . . 4 (𝜑 → ((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ))
7 eluzle 11644 . . . . 5 (𝑁 ∈ (ℤ‘(𝑀 + 1)) → (𝑀 + 1) ≤ 𝑁)
83, 7syl 17 . . . 4 (𝜑 → (𝑀 + 1) ≤ 𝑁)
9 eluzelre 11642 . . . . . 6 (𝑁 ∈ (ℤ‘(𝑀 + 1)) → 𝑁 ∈ ℝ)
103, 9syl 17 . . . . 5 (𝜑𝑁 ∈ ℝ)
1110leidd 10538 . . . 4 (𝜑𝑁𝑁)
126, 8, 11jca32 557 . . 3 (𝜑 → (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑀 + 1) ≤ 𝑁𝑁𝑁)))
13 elfz2 12275 . . 3 (𝑁 ∈ ((𝑀 + 1)...𝑁) ↔ (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑀 + 1) ≤ 𝑁𝑁𝑁)))
1412, 13sylibr 224 . 2 (𝜑𝑁 ∈ ((𝑀 + 1)...𝑁))
15 fveq2 6148 . . . . . . 7 (𝑗 = (𝑀 + 1) → (𝑃𝑗) = (𝑃‘(𝑀 + 1)))
1615oveq2d 6620 . . . . . 6 (𝑗 = (𝑀 + 1) → ((𝑃𝑀)[,](𝑃𝑗)) = ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))))
1716itgeq1d 39479 . . . . 5 (𝑗 = (𝑀 + 1) → ∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡)
18 oveq2 6612 . . . . . 6 (𝑗 = (𝑀 + 1) → (𝑀..^𝑗) = (𝑀..^(𝑀 + 1)))
1918sumeq1d 14365 . . . . 5 (𝑗 = (𝑀 + 1) → Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
2017, 19eqeq12d 2636 . . . 4 (𝑗 = (𝑀 + 1) → (∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ↔ ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
2120imbi2d 330 . . 3 (𝑗 = (𝑀 + 1) → ((𝜑 → ∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ↔ (𝜑 → ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)))
22 fveq2 6148 . . . . . . 7 (𝑗 = 𝑘 → (𝑃𝑗) = (𝑃𝑘))
2322oveq2d 6620 . . . . . 6 (𝑗 = 𝑘 → ((𝑃𝑀)[,](𝑃𝑗)) = ((𝑃𝑀)[,](𝑃𝑘)))
2423itgeq1d 39479 . . . . 5 (𝑗 = 𝑘 → ∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡)
25 oveq2 6612 . . . . . 6 (𝑗 = 𝑘 → (𝑀..^𝑗) = (𝑀..^𝑘))
2625sumeq1d 14365 . . . . 5 (𝑗 = 𝑘 → Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
2724, 26eqeq12d 2636 . . . 4 (𝑗 = 𝑘 → (∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ↔ ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
2827imbi2d 330 . . 3 (𝑗 = 𝑘 → ((𝜑 → ∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ↔ (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)))
29 fveq2 6148 . . . . . . 7 (𝑗 = (𝑘 + 1) → (𝑃𝑗) = (𝑃‘(𝑘 + 1)))
3029oveq2d 6620 . . . . . 6 (𝑗 = (𝑘 + 1) → ((𝑃𝑀)[,](𝑃𝑗)) = ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))))
3130itgeq1d 39479 . . . . 5 (𝑗 = (𝑘 + 1) → ∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = ∫((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡)
32 oveq2 6612 . . . . . 6 (𝑗 = (𝑘 + 1) → (𝑀..^𝑗) = (𝑀..^(𝑘 + 1)))
3332sumeq1d 14365 . . . . 5 (𝑗 = (𝑘 + 1) → Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
3431, 33eqeq12d 2636 . . . 4 (𝑗 = (𝑘 + 1) → (∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ↔ ∫((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
3534imbi2d 330 . . 3 (𝑗 = (𝑘 + 1) → ((𝜑 → ∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ↔ (𝜑 → ∫((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)))
36 fveq2 6148 . . . . . . 7 (𝑗 = 𝑁 → (𝑃𝑗) = (𝑃𝑁))
3736oveq2d 6620 . . . . . 6 (𝑗 = 𝑁 → ((𝑃𝑀)[,](𝑃𝑗)) = ((𝑃𝑀)[,](𝑃𝑁)))
3837itgeq1d 39479 . . . . 5 (𝑗 = 𝑁 → ∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = ∫((𝑃𝑀)[,](𝑃𝑁))𝐴 d𝑡)
39 oveq2 6612 . . . . . 6 (𝑗 = 𝑁 → (𝑀..^𝑗) = (𝑀..^𝑁))
4039sumeq1d 14365 . . . . 5 (𝑗 = 𝑁 → Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
4138, 40eqeq12d 2636 . . . 4 (𝑗 = 𝑁 → (∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ↔ ∫((𝑃𝑀)[,](𝑃𝑁))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
4241imbi2d 330 . . 3 (𝑗 = 𝑁 → ((𝜑 → ∫((𝑃𝑀)[,](𝑃𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ↔ (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑁))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)))
431adantl 482 . . . . . . . 8 ((𝑁 ∈ (ℤ‘(𝑀 + 1)) ∧ 𝜑) → 𝑀 ∈ ℤ)
44 fzval3 12477 . . . . . . . 8 (𝑀 ∈ ℤ → (𝑀...𝑀) = (𝑀..^(𝑀 + 1)))
4543, 44syl 17 . . . . . . 7 ((𝑁 ∈ (ℤ‘(𝑀 + 1)) ∧ 𝜑) → (𝑀...𝑀) = (𝑀..^(𝑀 + 1)))
4645eqcomd 2627 . . . . . 6 ((𝑁 ∈ (ℤ‘(𝑀 + 1)) ∧ 𝜑) → (𝑀..^(𝑀 + 1)) = (𝑀...𝑀))
4746sumeq1d 14365 . . . . 5 ((𝑁 ∈ (ℤ‘(𝑀 + 1)) ∧ 𝜑) → Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀...𝑀)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
48 itgspltprt.3 . . . . . . . . . . . 12 (𝜑𝑃:(𝑀...𝑁)⟶ℝ)
4948adantr 481 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑃:(𝑀...𝑁)⟶ℝ)
501zred 11426 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℝ)
51 1red 9999 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ∈ ℝ)
5250, 51readdcld 10013 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑀 + 1) ∈ ℝ)
5350ltp1d 10898 . . . . . . . . . . . . . . . 16 (𝜑𝑀 < (𝑀 + 1))
5450, 52, 10, 53, 8ltletrd 10141 . . . . . . . . . . . . . . 15 (𝜑𝑀 < 𝑁)
5550, 10, 54ltled 10129 . . . . . . . . . . . . . 14 (𝜑𝑀𝑁)
56 eluz 11645 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ𝑀) ↔ 𝑀𝑁))
571, 5, 56syl2anc 692 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 ∈ (ℤ𝑀) ↔ 𝑀𝑁))
5855, 57mpbird 247 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ (ℤ𝑀))
59 eluzfz1 12290 . . . . . . . . . . . . 13 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...𝑁))
6058, 59syl 17 . . . . . . . . . . . 12 (𝜑𝑀 ∈ (𝑀...𝑁))
6160adantr 481 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑀 ∈ (𝑀...𝑁))
6249, 61ffvelrnd 6316 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃𝑀) ∈ ℝ)
63 elfz1 12273 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (𝑀...𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑀𝑁𝑁𝑁)))
641, 5, 63syl2anc 692 . . . . . . . . . . . . 13 (𝜑 → (𝑁 ∈ (𝑀...𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑀𝑁𝑁𝑁)))
655, 55, 11, 64mpbir3and 1243 . . . . . . . . . . . 12 (𝜑𝑁 ∈ (𝑀...𝑁))
6648, 65ffvelrnd 6316 . . . . . . . . . . 11 (𝜑 → (𝑃𝑁) ∈ ℝ)
6766adantr 481 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃𝑁) ∈ ℝ)
6850lep1d 10899 . . . . . . . . . . . . . 14 (𝜑𝑀 ≤ (𝑀 + 1))
69 elfz1 12273 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 + 1) ∈ (𝑀...𝑁) ↔ ((𝑀 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑀 + 1) ∧ (𝑀 + 1) ≤ 𝑁)))
701, 5, 69syl2anc 692 . . . . . . . . . . . . . 14 (𝜑 → ((𝑀 + 1) ∈ (𝑀...𝑁) ↔ ((𝑀 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑀 + 1) ∧ (𝑀 + 1) ≤ 𝑁)))
712, 68, 8, 70mpbir3and 1243 . . . . . . . . . . . . 13 (𝜑 → (𝑀 + 1) ∈ (𝑀...𝑁))
7248, 71ffvelrnd 6316 . . . . . . . . . . . 12 (𝜑 → (𝑃‘(𝑀 + 1)) ∈ ℝ)
7372adantr 481 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘(𝑀 + 1)) ∈ ℝ)
74 simpr 477 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))))
75 eliccre 39139 . . . . . . . . . . 11 (((𝑃𝑀) ∈ ℝ ∧ (𝑃‘(𝑀 + 1)) ∈ ℝ ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ∈ ℝ)
7662, 73, 74, 75syl3anc 1323 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ∈ ℝ)
7748, 60ffvelrnd 6316 . . . . . . . . . . . . 13 (𝜑 → (𝑃𝑀) ∈ ℝ)
7877rexrd 10033 . . . . . . . . . . . 12 (𝜑 → (𝑃𝑀) ∈ ℝ*)
7978adantr 481 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃𝑀) ∈ ℝ*)
8073rexrd 10033 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘(𝑀 + 1)) ∈ ℝ*)
81 iccgelb 12172 . . . . . . . . . . 11 (((𝑃𝑀) ∈ ℝ* ∧ (𝑃‘(𝑀 + 1)) ∈ ℝ*𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃𝑀) ≤ 𝑡)
8279, 80, 74, 81syl3anc 1323 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃𝑀) ≤ 𝑡)
83 iccleub 12171 . . . . . . . . . . . 12 (((𝑃𝑀) ∈ ℝ* ∧ (𝑃‘(𝑀 + 1)) ∈ ℝ*𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ≤ (𝑃‘(𝑀 + 1)))
8479, 80, 74, 83syl3anc 1323 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ≤ (𝑃‘(𝑀 + 1)))
8548adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ)
86 elfzelz 12284 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ((𝑀 + 1)...𝑁) → 𝑖 ∈ ℤ)
8786adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑖 ∈ ℤ)
8850adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑀 ∈ ℝ)
8987zred 11426 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑖 ∈ ℝ)
9052adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑀 + 1) ∈ ℝ)
9153adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑀 < (𝑀 + 1))
92 elfzle1 12286 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ((𝑀 + 1)...𝑁) → (𝑀 + 1) ≤ 𝑖)
9392adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑀 + 1) ≤ 𝑖)
9488, 90, 89, 91, 93ltletrd 10141 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑀 < 𝑖)
9588, 89, 94ltled 10129 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑀𝑖)
96 elfzle2 12287 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ((𝑀 + 1)...𝑁) → 𝑖𝑁)
9796adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑖𝑁)
981, 5jca 554 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
9998adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
100 elfz1 12273 . . . . . . . . . . . . . . . 16 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀𝑖𝑖𝑁)))
10199, 100syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀𝑖𝑖𝑁)))
10287, 95, 97, 101mpbir3and 1243 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑖 ∈ (𝑀...𝑁))
10385, 102ffvelrnd 6316 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑃𝑖) ∈ ℝ)
10448adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
105 elfzelz 12284 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1)) → 𝑖 ∈ ℤ)
106105adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℤ)
10750adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℝ)
108106zred 11426 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
10952adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑀 + 1) ∈ ℝ)
11053adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 < (𝑀 + 1))
111 elfzle1 12286 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1)) → (𝑀 + 1) ≤ 𝑖)
112111adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑀 + 1) ≤ 𝑖)
113107, 109, 108, 110, 112ltletrd 10141 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 < 𝑖)
114107, 108, 113ltled 10129 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀𝑖)
11510adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℝ)
116 1red 9999 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
117115, 116resubcld 10402 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
118 elfzle2 12287 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1)) → 𝑖 ≤ (𝑁 − 1))
119118adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ≤ (𝑁 − 1))
120115ltm1d 10900 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
121108, 117, 115, 119, 120lelttrd 10139 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 < 𝑁)
122108, 115, 121ltled 10129 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖𝑁)
12398adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
124123, 100syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀𝑖𝑖𝑁)))
125106, 114, 122, 124mpbir3and 1243 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑁))
126104, 125ffvelrnd 6316 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑃𝑖) ∈ ℝ)
127106peano2zd 11429 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℤ)
128108, 116readdcld 10013 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ)
129107, 108, 116, 113ltadd1dd 10582 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑀 + 1) < (𝑖 + 1))
130107, 109, 128, 110, 129lttrd 10142 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 < (𝑖 + 1))
131107, 128, 130ltled 10129 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 ≤ (𝑖 + 1))
132 zltp1le 11371 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
133105, 5, 132syl2anr 495 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
134121, 133mpbid 222 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁)
135 elfz1 12273 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
136123, 135syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
137127, 131, 134, 136mpbir3and 1243 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁))
138104, 137ffvelrnd 6316 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
139 eluz 11645 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑖 ∈ (ℤ𝑀) ↔ 𝑀𝑖))
1401, 105, 139syl2an 494 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 ∈ (ℤ𝑀) ↔ 𝑀𝑖))
141114, 140mpbird 247 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ (ℤ𝑀))
1425adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℤ)
143 elfzo2 12414 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀..^𝑁) ↔ (𝑖 ∈ (ℤ𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑖 < 𝑁))
144141, 142, 121, 143syl3anbrc 1244 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀..^𝑁))
145 itgspltprt.4 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑃𝑖) < (𝑃‘(𝑖 + 1)))
146144, 145syldan 487 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑃𝑖) < (𝑃‘(𝑖 + 1)))
147126, 138, 146ltled 10129 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑃𝑖) ≤ (𝑃‘(𝑖 + 1)))
1483, 103, 147monoord 12771 . . . . . . . . . . . 12 (𝜑 → (𝑃‘(𝑀 + 1)) ≤ (𝑃𝑁))
149148adantr 481 . . . . . . . . . . 11 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘(𝑀 + 1)) ≤ (𝑃𝑁))
15076, 73, 67, 84, 149letrd 10138 . . . . . . . . . 10 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ≤ (𝑃𝑁))
15162, 67, 76, 82, 150eliccd 39137 . . . . . . . . 9 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)))
152 itgspltprt.5 . . . . . . . . 9 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁))) → 𝐴 ∈ ℂ)
153151, 152syldan 487 . . . . . . . 8 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝐴 ∈ ℂ)
154 id 22 . . . . . . . . . 10 (𝜑𝜑)
155 fzolb 12417 . . . . . . . . . . 11 (𝑀 ∈ (𝑀..^𝑁) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁))
1561, 5, 54, 155syl3anbrc 1244 . . . . . . . . . 10 (𝜑𝑀 ∈ (𝑀..^𝑁))
157154, 156jca 554 . . . . . . . . 9 (𝜑 → (𝜑𝑀 ∈ (𝑀..^𝑁)))
158 eleq1 2686 . . . . . . . . . . . 12 (𝑖 = 𝑀 → (𝑖 ∈ (𝑀..^𝑁) ↔ 𝑀 ∈ (𝑀..^𝑁)))
159158anbi2d 739 . . . . . . . . . . 11 (𝑖 = 𝑀 → ((𝜑𝑖 ∈ (𝑀..^𝑁)) ↔ (𝜑𝑀 ∈ (𝑀..^𝑁))))
160 fveq2 6148 . . . . . . . . . . . . . 14 (𝑖 = 𝑀 → (𝑃𝑖) = (𝑃𝑀))
161 oveq1 6611 . . . . . . . . . . . . . . 15 (𝑖 = 𝑀 → (𝑖 + 1) = (𝑀 + 1))
162161fveq2d 6152 . . . . . . . . . . . . . 14 (𝑖 = 𝑀 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑀 + 1)))
163160, 162oveq12d 6622 . . . . . . . . . . . . 13 (𝑖 = 𝑀 → ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) = ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))))
164163mpteq1d 4698 . . . . . . . . . . . 12 (𝑖 = 𝑀 → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) = (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴))
165164eleq1d 2683 . . . . . . . . . . 11 (𝑖 = 𝑀 → ((𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿1))
166159, 165imbi12d 334 . . . . . . . . . 10 (𝑖 = 𝑀 → (((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1) ↔ ((𝜑𝑀 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿1)))
167 itgspltprt.6 . . . . . . . . . 10 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1)
168166, 167vtoclg 3252 . . . . . . . . 9 (𝑀 ∈ ℤ → ((𝜑𝑀 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿1))
1691, 157, 168sylc 65 . . . . . . . 8 (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿1)
170153, 169itgcl 23456 . . . . . . 7 (𝜑 → ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 ∈ ℂ)
171163itgeq1d 39479 . . . . . . . 8 (𝑖 = 𝑀 → ∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡)
172171fsum1 14406 . . . . . . 7 ((𝑀 ∈ ℤ ∧ ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 ∈ ℂ) → Σ𝑖 ∈ (𝑀...𝑀)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡)
1731, 170, 172syl2anc 692 . . . . . 6 (𝜑 → Σ𝑖 ∈ (𝑀...𝑀)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡)
174173adantl 482 . . . . 5 ((𝑁 ∈ (ℤ‘(𝑀 + 1)) ∧ 𝜑) → Σ𝑖 ∈ (𝑀...𝑀)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡)
17547, 174eqtr2d 2656 . . . 4 ((𝑁 ∈ (ℤ‘(𝑀 + 1)) ∧ 𝜑) → ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
176175ex 450 . . 3 (𝑁 ∈ (ℤ‘(𝑀 + 1)) → (𝜑 → ∫((𝑃𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
177 simp3 1061 . . . . 5 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → 𝜑)
178 simp1 1059 . . . . 5 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → 𝑘 ∈ ((𝑀 + 1)..^𝑁))
179 simp2 1060 . . . . . 6 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
180177, 179mpd 15 . . . . 5 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
18150adantr 481 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ∈ ℝ)
182 elfzoelz 12411 . . . . . . . . . . . 12 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 ∈ ℤ)
183182zred 11426 . . . . . . . . . . 11 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 ∈ ℝ)
184183adantl 482 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ ℝ)
18552adantr 481 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 + 1) ∈ ℝ)
18653adantr 481 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < (𝑀 + 1))
187 elfzole1 12419 . . . . . . . . . . . 12 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑀 + 1) ≤ 𝑘)
188187adantl 482 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 + 1) ≤ 𝑘)
189181, 185, 184, 186, 188ltletrd 10141 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < 𝑘)
190181, 184, 189ltled 10129 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀𝑘)
191 eluz 11645 . . . . . . . . . 10 ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 ∈ (ℤ𝑀) ↔ 𝑀𝑘))
1921, 182, 191syl2an 494 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 ∈ (ℤ𝑀) ↔ 𝑀𝑘))
193190, 192mpbird 247 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (ℤ𝑀))
194 simplll 797 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝜑)
195 eliccxr 39148 . . . . . . . . . . . 12 (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) → 𝑡 ∈ ℝ*)
196195adantl 482 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ℝ*)
197194, 77syl 17 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃𝑀) ∈ ℝ)
198194, 48syl 17 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑃:(𝑀...𝑁)⟶ℝ)
199 elfzelz 12284 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀...𝑘) → 𝑖 ∈ ℤ)
200199adantl 482 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ ℤ)
201 elfzle1 12286 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀...𝑘) → 𝑀𝑖)
202201adantl 482 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀𝑖)
203200zred 11426 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ ℝ)
20410ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑁 ∈ ℝ)
205184adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑘 ∈ ℝ)
206 elfzle2 12287 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (𝑀...𝑘) → 𝑖𝑘)
207206adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖𝑘)
208 elfzolt2 12420 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 < 𝑁)
209208ad2antlr 762 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑘 < 𝑁)
210203, 205, 204, 207, 209lelttrd 10139 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 < 𝑁)
211203, 204, 210ltled 10129 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖𝑁)
21298ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
213212, 100syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀𝑖𝑖𝑁)))
214200, 202, 211, 213mpbir3and 1243 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ (𝑀...𝑁))
215214adantr 481 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑖 ∈ (𝑀...𝑁))
216198, 215ffvelrnd 6316 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃𝑖) ∈ ℝ)
217200peano2zd 11429 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ∈ ℤ)
21850ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 ∈ ℝ)
219217zred 11426 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ∈ ℝ)
22050adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘)) → 𝑀 ∈ ℝ)
221199zred 11426 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (𝑀...𝑘) → 𝑖 ∈ ℝ)
222221adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ ℝ)
223 1red 9999 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑀...𝑘)) → 1 ∈ ℝ)
224222, 223readdcld 10013 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ∈ ℝ)
225201adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘)) → 𝑀𝑖)
226222ltp1d 10898 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘)) → 𝑖 < (𝑖 + 1))
227220, 222, 224, 225, 226lelttrd 10139 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘)) → 𝑀 < (𝑖 + 1))
228227adantlr 750 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 < (𝑖 + 1))
229218, 219, 228ltled 10129 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 ≤ (𝑖 + 1))
2305, 199anim12ci 590 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘)) → (𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ))
231230adantlr 750 . . . . . . . . . . . . . . . . . 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 1243 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ∈ (𝑀...𝑁))
236235adantr 481 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑖 + 1) ∈ (𝑀...𝑁))
237198, 236ffvelrnd 6316 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
238 simpr 477 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))))
239 eliccre 39139 . . . . . . . . . . . . 13 (((𝑃𝑖) ∈ ℝ ∧ (𝑃‘(𝑖 + 1)) ∈ ℝ ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ℝ)
240216, 237, 238, 239syl3anc 1323 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ℝ)
241 elfzuz 12280 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...𝑘) → 𝑖 ∈ (ℤ𝑀))
242241adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ (ℤ𝑀))
24348ad3antrrr 765 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑃:(𝑀...𝑁)⟶ℝ)
244 elfzelz 12284 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑀...𝑖) → 𝑗 ∈ ℤ)
245244adantl 482 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ∈ ℤ)
246 elfzle1 12286 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑀...𝑖) → 𝑀𝑗)
247246adantl 482 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑀𝑗)
248245zred 11426 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ∈ ℝ)
249204adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑁 ∈ ℝ)
250203adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑖 ∈ ℝ)
251 elfzle2 12287 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (𝑀...𝑖) → 𝑗𝑖)
252251adantl 482 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗𝑖)
253210adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑖 < 𝑁)
254248, 250, 249, 252, 253lelttrd 10139 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 < 𝑁)
255248, 249, 254ltled 10129 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗𝑁)
256212adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
257 elfz1 12273 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀𝑗𝑗𝑁)))
258256, 257syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀𝑗𝑗𝑁)))
259245, 247, 255, 258mpbir3and 1243 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ∈ (𝑀...𝑁))
260243, 259ffvelrnd 6316 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝑃𝑗) ∈ ℝ)
26148ad3antrrr 765 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
262 elfzelz 12284 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑗 ∈ ℤ)
263262adantl 482 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ ℤ)
264 elfzle1 12286 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑀𝑗)
265264adantl 482 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀𝑗)
266263zred 11426 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ ℝ)
267204adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑁 ∈ ℝ)
268203adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑖 ∈ ℝ)
269 1red 9999 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 1 ∈ ℝ)
270268, 269resubcld 10402 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑖 − 1) ∈ ℝ)
271 elfzle2 12287 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑗 ≤ (𝑖 − 1))
272271adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ≤ (𝑖 − 1))
273268ltm1d 10900 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑖 − 1) < 𝑖)
274266, 270, 268, 272, 273lelttrd 10139 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 < 𝑖)
275210adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑖 < 𝑁)
276266, 268, 267, 274, 275lttrd 10142 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 < 𝑁)
277266, 267, 276ltled 10129 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗𝑁)
278212adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
279278, 257syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀𝑗𝑗𝑁)))
280263, 265, 277, 279mpbir3and 1243 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ (𝑀...𝑁))
281261, 280ffvelrnd 6316 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑃𝑗) ∈ ℝ)
282263peano2zd 11429 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ∈ ℤ)
283181ad2antrr 761 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 ∈ ℝ)
284266, 269readdcld 10013 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ∈ ℝ)
28550adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 ∈ ℝ)
286262zred 11426 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑗 ∈ ℝ)
287286adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ ℝ)
288 1red 9999 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (𝑀...(𝑖 − 1))) → 1 ∈ ℝ)
289287, 288readdcld 10013 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ∈ ℝ)
290264adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀𝑗)
291287ltp1d 10898 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 < (𝑗 + 1))
292285, 287, 289, 290, 291lelttrd 10139 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 < (𝑗 + 1))
293292ad4ant14 1290 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 < (𝑗 + 1))
294283, 284, 293ltled 10129 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 ≤ (𝑗 + 1))
295 zltp1le 11371 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑗 < 𝑖 ↔ (𝑗 + 1) ≤ 𝑖))
296262, 200, 295syl2anr 495 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 < 𝑖 ↔ (𝑗 + 1) ≤ 𝑖))
297274, 296mpbid 222 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ≤ 𝑖)
298284, 268, 267, 297, 275lelttrd 10139 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) < 𝑁)
299284, 267, 298ltled 10129 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ≤ 𝑁)
300 elfz1 12273 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑗 + 1) ∈ (𝑀...𝑁) ↔ ((𝑗 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑗 + 1) ∧ (𝑗 + 1) ≤ 𝑁)))
301278, 300syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → ((𝑗 + 1) ∈ (𝑀...𝑁) ↔ ((𝑗 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑗 + 1) ∧ (𝑗 + 1) ≤ 𝑁)))
302282, 294, 299, 301mpbir3and 1243 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ∈ (𝑀...𝑁))
303261, 302ffvelrnd 6316 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑃‘(𝑗 + 1)) ∈ ℝ)
304 simplll 797 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝜑)
305 elfzuz 12280 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑗 ∈ (ℤ𝑀))
306305adantl 482 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ (ℤ𝑀))
307304, 5syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑁 ∈ ℤ)
308 elfzo2 12414 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑀..^𝑁) ↔ (𝑗 ∈ (ℤ𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑗 < 𝑁))
309306, 307, 276, 308syl3anbrc 1244 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ (𝑀..^𝑁))
310 eleq1 2686 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → (𝑖 ∈ (𝑀..^𝑁) ↔ 𝑗 ∈ (𝑀..^𝑁)))
311310anbi2d 739 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → ((𝜑𝑖 ∈ (𝑀..^𝑁)) ↔ (𝜑𝑗 ∈ (𝑀..^𝑁))))
312 fveq2 6148 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → (𝑃𝑖) = (𝑃𝑗))
313 oveq1 6611 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
314313fveq2d 6152 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑗 + 1)))
315312, 314breq12d 4626 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → ((𝑃𝑖) < (𝑃‘(𝑖 + 1)) ↔ (𝑃𝑗) < (𝑃‘(𝑗 + 1))))
316311, 315imbi12d 334 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑗 → (((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑃𝑖) < (𝑃‘(𝑖 + 1))) ↔ ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑃𝑗) < (𝑃‘(𝑗 + 1)))))
317316, 145chvarv 2262 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑀..^𝑁)) → (𝑃𝑗) < (𝑃‘(𝑗 + 1)))
318304, 309, 317syl2anc 692 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑃𝑗) < (𝑃‘(𝑗 + 1)))
319281, 303, 318ltled 10129 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑃𝑗) ≤ (𝑃‘(𝑗 + 1)))
320242, 260, 319monoord 12771 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑃𝑀) ≤ (𝑃𝑖))
321320adantr 481 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃𝑀) ≤ (𝑃𝑖))
322216rexrd 10033 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃𝑖) ∈ ℝ*)
323237rexrd 10033 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘(𝑖 + 1)) ∈ ℝ*)
324 iccgelb 12172 . . . . . . . . . . . . 13 (((𝑃𝑖) ∈ ℝ* ∧ (𝑃‘(𝑖 + 1)) ∈ ℝ*𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃𝑖) ≤ 𝑡)
325322, 323, 238, 324syl3anc 1323 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃𝑖) ≤ 𝑡)
326197, 216, 240, 321, 325letrd 10138 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃𝑀) ≤ 𝑡)
327194, 66syl 17 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃𝑁) ∈ ℝ)
328 iccleub 12171 . . . . . . . . . . . . 13 (((𝑃𝑖) ∈ ℝ* ∧ (𝑃‘(𝑖 + 1)) ∈ ℝ*𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ≤ (𝑃‘(𝑖 + 1)))
329322, 323, 238, 328syl3anc 1323 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ≤ (𝑃‘(𝑖 + 1)))
3305ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑁 ∈ ℤ)
331 eluz 11645 . . . . . . . . . . . . . . . 16 (((𝑖 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ‘(𝑖 + 1)) ↔ (𝑖 + 1) ≤ 𝑁))
332217, 330, 331syl2anc 692 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑁 ∈ (ℤ‘(𝑖 + 1)) ↔ (𝑖 + 1) ≤ 𝑁))
333233, 332mpbird 247 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑁 ∈ (ℤ‘(𝑖 + 1)))
334333adantr 481 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑁 ∈ (ℤ‘(𝑖 + 1)))
33548ad3antrrr 765 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ)
336 elfzelz 12284 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ((𝑖 + 1)...𝑁) → 𝑗 ∈ ℤ)
337336adantl 482 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑗 ∈ ℤ)
338 elfzel1 12283 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (𝑀...𝑘) → 𝑀 ∈ ℤ)
339338zred 11426 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (𝑀...𝑘) → 𝑀 ∈ ℝ)
340339adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀 ∈ ℝ)
341336zred 11426 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ((𝑖 + 1)...𝑁) → 𝑗 ∈ ℝ)
342341adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑗 ∈ ℝ)
343221adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑖 ∈ ℝ)
344 1red 9999 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 1 ∈ ℝ)
345343, 344readdcld 10013 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑖 + 1) ∈ ℝ)
346201adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀𝑖)
347343ltp1d 10898 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑖 < (𝑖 + 1))
348340, 343, 345, 346, 347lelttrd 10139 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀 < (𝑖 + 1))
349 elfzle1 12286 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ((𝑖 + 1)...𝑁) → (𝑖 + 1) ≤ 𝑗)
350349adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑖 + 1) ≤ 𝑗)
351340, 345, 342, 348, 350ltletrd 10141 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀 < 𝑗)
352340, 342, 351ltled 10129 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀𝑗)
353352adantll 749 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀𝑗)
354 elfzle2 12287 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ((𝑖 + 1)...𝑁) → 𝑗𝑁)
355354adantl 482 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑗𝑁)
356212adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
357356, 257syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀𝑗𝑗𝑁)))
358337, 353, 355, 357mpbir3and 1243 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑗 ∈ (𝑀...𝑁))
359335, 358ffvelrnd 6316 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑃𝑗) ∈ ℝ)
360359adantlr 750 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑃𝑗) ∈ ℝ)
361 simplll 797 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝜑)
362 simplr 791 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑘))
363 simpr 477 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1)))
364483ad2ant1 1080 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
365 elfzelz 12284 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1)) → 𝑗 ∈ ℤ)
3663653ad2ant3 1082 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ℤ)
367503ad2ant1 1080 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℝ)
368366zred 11426 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ℝ)
3692243adant3 1079 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ)
3702273adant3 1079 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 < (𝑖 + 1))
371 elfzle1 12286 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1)) → (𝑖 + 1) ≤ 𝑗)
3723713ad2ant3 1082 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑗)
373367, 369, 368, 370, 372ltletrd 10141 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 < 𝑗)
374367, 368, 373ltled 10129 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀𝑗)
375365adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ℤ)
376375zred 11426 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ℝ)
37710adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℝ)
378 1red 9999 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
379377, 378resubcld 10402 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
380 elfzle2 12287 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1)) → 𝑗 ≤ (𝑁 − 1))
381380adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ≤ (𝑁 − 1))
382377ltm1d 10900 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
383376, 379, 377, 381, 382lelttrd 10139 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 < 𝑁)
384376, 377, 383ltled 10129 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗𝑁)
3853843adant2 1078 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗𝑁)
386983ad2ant1 1080 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
387386, 257syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀𝑗𝑗𝑁)))
388366, 374, 385, 387mpbir3and 1243 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ (𝑀...𝑁))
389364, 388ffvelrnd 6316 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃𝑗) ∈ ℝ)
390366peano2zd 11429 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ∈ ℤ)
391390zred 11426 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ∈ ℝ)
3922213ad2ant2 1081 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
393 1red 9999 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
3942263adant3 1079 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖 < (𝑖 + 1))
395392, 369, 368, 394, 372ltletrd 10141 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖 < 𝑗)
396392, 368, 395ltled 10129 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖𝑗)
397392, 368, 393, 396leadd1dd 10585 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ (𝑗 + 1))
398367, 369, 391, 370, 397ltletrd 10141 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 < (𝑗 + 1))
399367, 391, 398ltled 10129 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 ≤ (𝑗 + 1))
400 zltp1le 11371 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 < 𝑁 ↔ (𝑗 + 1) ≤ 𝑁))
401365, 5, 400syl2anr 495 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 < 𝑁 ↔ (𝑗 + 1) ≤ 𝑁))
402383, 401mpbid 222 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ≤ 𝑁)
4034023adant2 1078 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ≤ 𝑁)
404386, 300syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → ((𝑗 + 1) ∈ (𝑀...𝑁) ↔ ((𝑗 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑗 + 1) ∧ (𝑗 + 1) ≤ 𝑁)))
405390, 399, 403, 404mpbir3and 1243 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ∈ (𝑀...𝑁))
406364, 405ffvelrnd 6316 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃‘(𝑗 + 1)) ∈ ℝ)
407 simp1 1059 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝜑)
40813ad2ant1 1080 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℤ)
409 eluz 11645 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑗 ∈ (ℤ𝑀) ↔ 𝑀𝑗))
410408, 366, 409syl2anc 692 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 ∈ (ℤ𝑀) ↔ 𝑀𝑗))
411374, 410mpbird 247 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ (ℤ𝑀))
41253ad2ant1 1080 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℤ)
4133833adant2 1078 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 < 𝑁)
414411, 412, 413, 308syl3anbrc 1244 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ (𝑀..^𝑁))
415407, 414, 317syl2anc 692 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃𝑗) < (𝑃‘(𝑗 + 1)))
416389, 406, 415ltled 10129 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃𝑗) ≤ (𝑃‘(𝑗 + 1)))
417361, 362, 363, 416syl3anc 1323 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃𝑗) ≤ (𝑃‘(𝑗 + 1)))
418417adantlr 750 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃𝑗) ≤ (𝑃‘(𝑗 + 1)))
419334, 360, 418monoord 12771 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘(𝑖 + 1)) ≤ (𝑃𝑁))
420240, 237, 327, 329, 419letrd 10138 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ≤ (𝑃𝑁))
42166rexrd 10033 . . . . . . . . . . . . . 14 (𝜑 → (𝑃𝑁) ∈ ℝ*)
42278, 421jca 554 . . . . . . . . . . . . 13 (𝜑 → ((𝑃𝑀) ∈ ℝ* ∧ (𝑃𝑁) ∈ ℝ*))
423194, 422syl 17 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → ((𝑃𝑀) ∈ ℝ* ∧ (𝑃𝑁) ∈ ℝ*))
424 elicc1 12161 . . . . . . . . . . . 12 (((𝑃𝑀) ∈ ℝ* ∧ (𝑃𝑁) ∈ ℝ*) → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)) ↔ (𝑡 ∈ ℝ* ∧ (𝑃𝑀) ≤ 𝑡𝑡 ≤ (𝑃𝑁))))
425423, 424syl 17 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)) ↔ (𝑡 ∈ ℝ* ∧ (𝑃𝑀) ≤ 𝑡𝑡 ≤ (𝑃𝑁))))
426196, 326, 420, 425mpbir3and 1243 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)))
427194, 426, 152syl2anc 692 . . . . . . . . 9 ((((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝐴 ∈ ℂ)
428 simpll 789 . . . . . . . . . 10 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝜑)
429242, 330, 210, 143syl3anbrc 1244 . . . . . . . . . 10 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ (𝑀..^𝑁))
430428, 429, 167syl2anc 692 . . . . . . . . 9 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1)
431427, 430itgcl 23456 . . . . . . . 8 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → ∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ∈ ℂ)
432 fveq2 6148 . . . . . . . . . 10 (𝑖 = 𝑘 → (𝑃𝑖) = (𝑃𝑘))
433 oveq1 6611 . . . . . . . . . . 11 (𝑖 = 𝑘 → (𝑖 + 1) = (𝑘 + 1))
434433fveq2d 6152 . . . . . . . . . 10 (𝑖 = 𝑘 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑘 + 1)))
435432, 434oveq12d 6622 . . . . . . . . 9 (𝑖 = 𝑘 → ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) = ((𝑃𝑘)[,](𝑃‘(𝑘 + 1))))
436435itgeq1d 39479 . . . . . . . 8 (𝑖 = 𝑘 → ∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡)
437193, 431, 436fzosump1 14411 . . . . . . 7 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
4384373adant3 1079 . . . . . 6 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
439 oveq1 6611 . . . . . . . 8 (∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 → (∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
440439eqcomd 2627 . . . . . . 7 (∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 → (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = (∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
4414403ad2ant3 1082 . . . . . 6 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = (∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
44277adantr 481 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑀) ∈ ℝ)
44348adantr 481 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ)
444182adantl 482 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ ℤ)
445444peano2zd 11429 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ ℤ)
446445zred 11426 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ ℝ)
447184ltp1d 10898 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 < (𝑘 + 1))
448181, 184, 446, 189, 447lttrd 10142 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < (𝑘 + 1))
449181, 446, 448ltled 10129 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ≤ (𝑘 + 1))
450208adantl 482 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 < 𝑁)
451 zltp1le 11371 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 < 𝑁 ↔ (𝑘 + 1) ≤ 𝑁))
452182, 5, 451syl2anr 495 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 < 𝑁 ↔ (𝑘 + 1) ≤ 𝑁))
453450, 452mpbid 222 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ≤ 𝑁)
45498adantr 481 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
455 elfz1 12273 . . . . . . . . . . . 12 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑘 + 1) ∈ (𝑀...𝑁) ↔ ((𝑘 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁)))
456454, 455syl 17 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ((𝑘 + 1) ∈ (𝑀...𝑁) ↔ ((𝑘 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁)))
457445, 449, 453, 456mpbir3and 1243 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ (𝑀...𝑁))
458443, 457ffvelrnd 6316 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ∈ ℝ)
45910adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ ℝ)
460184, 459, 450ltled 10129 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘𝑁)
461 elfz1 12273 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘𝑁)))
462454, 461syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘𝑁)))
463444, 190, 460, 462mpbir3and 1243 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (𝑀...𝑁))
464443, 463ffvelrnd 6316 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑘) ∈ ℝ)
465464rexrd 10033 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑘) ∈ ℝ*)
46648ad2antrr 761 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑃:(𝑀...𝑁)⟶ℝ)
467466, 214ffvelrnd 6316 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑃𝑖) ∈ ℝ)
46848ad2antrr 761 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
469 elfzelz 12284 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ∈ ℤ)
470469adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ ℤ)
471 elfzle1 12286 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑀𝑖)
472471adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀𝑖)
473470zred 11426 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ ℝ)
47410ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑁 ∈ ℝ)
475184adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑘 ∈ ℝ)
476 1red 9999 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 1 ∈ ℝ)
477475, 476resubcld 10402 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑘 − 1) ∈ ℝ)
478 elfzle2 12287 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ≤ (𝑘 − 1))
479478adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ≤ (𝑘 − 1))
480475ltm1d 10900 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑘 − 1) < 𝑘)
481473, 477, 475, 479, 480lelttrd 10139 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 < 𝑘)
482450adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑘 < 𝑁)
483473, 475, 474, 481, 482lttrd 10142 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 < 𝑁)
484473, 474, 483ltled 10129 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖𝑁)
48598ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
486485, 100syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀𝑖𝑖𝑁)))
487470, 472, 484, 486mpbir3and 1243 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (𝑀...𝑁))
488468, 487ffvelrnd 6316 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃𝑖) ∈ ℝ)
489470peano2zd 11429 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ∈ ℤ)
49050ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 ∈ ℝ)
491473, 476readdcld 10013 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ∈ ℝ)
492473ltp1d 10898 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 < (𝑖 + 1))
493490, 473, 491, 472, 492lelttrd 10139 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 < (𝑖 + 1))
494490, 491, 493ltled 10129 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 ≤ (𝑖 + 1))
495 zltp1le 11371 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑖 < 𝑘 ↔ (𝑖 + 1) ≤ 𝑘))
496469, 444, 495syl2anr 495 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 < 𝑘 ↔ (𝑖 + 1) ≤ 𝑘))
497481, 496mpbid 222 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ≤ 𝑘)
498491, 475, 474, 497, 482lelttrd 10139 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) < 𝑁)
499491, 474, 498ltled 10129 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ≤ 𝑁)
500485, 135syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
501489, 494, 499, 500mpbir3and 1243 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁))
502468, 501ffvelrnd 6316 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
503 simpll 789 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝜑)
504 elfzuz 12280 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ∈ (ℤ𝑀))
505504adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (ℤ𝑀))
5065ad2antrr 761 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑁 ∈ ℤ)
507505, 506, 483, 143syl3anbrc 1244 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (𝑀..^𝑁))
508503, 507, 145syl2anc 692 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃𝑖) < (𝑃‘(𝑖 + 1)))
509488, 502, 508ltled 10129 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃𝑖) ≤ (𝑃‘(𝑖 + 1)))
510193, 467, 509monoord 12771 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑀) ≤ (𝑃𝑘))
5115adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ ℤ)
512 elfzo2 12414 . . . . . . . . . . . . 13 (𝑘 ∈ (𝑀..^𝑁) ↔ (𝑘 ∈ (ℤ𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑘 < 𝑁))
513193, 511, 450, 512syl3anbrc 1244 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (𝑀..^𝑁))
514 eleq1 2686 . . . . . . . . . . . . . . 15 (𝑖 = 𝑘 → (𝑖 ∈ (𝑀..^𝑁) ↔ 𝑘 ∈ (𝑀..^𝑁)))
515514anbi2d 739 . . . . . . . . . . . . . 14 (𝑖 = 𝑘 → ((𝜑𝑖 ∈ (𝑀..^𝑁)) ↔ (𝜑𝑘 ∈ (𝑀..^𝑁))))
516432, 434breq12d 4626 . . . . . . . . . . . . . 14 (𝑖 = 𝑘 → ((𝑃𝑖) < (𝑃‘(𝑖 + 1)) ↔ (𝑃𝑘) < (𝑃‘(𝑘 + 1))))
517515, 516imbi12d 334 . . . . . . . . . . . . 13 (𝑖 = 𝑘 → (((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑃𝑖) < (𝑃‘(𝑖 + 1))) ↔ ((𝜑𝑘 ∈ (𝑀..^𝑁)) → (𝑃𝑘) < (𝑃‘(𝑘 + 1)))))
518517, 145chvarv 2262 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (𝑀..^𝑁)) → (𝑃𝑘) < (𝑃‘(𝑘 + 1)))
519513, 518syldan 487 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑘) < (𝑃‘(𝑘 + 1)))
520464, 458, 519ltled 10129 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑘) ≤ (𝑃‘(𝑘 + 1)))
52178adantr 481 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑀) ∈ ℝ*)
522458rexrd 10033 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ∈ ℝ*)
523 elicc1 12161 . . . . . . . . . . 11 (((𝑃𝑀) ∈ ℝ* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ*) → ((𝑃𝑘) ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))) ↔ ((𝑃𝑘) ∈ ℝ* ∧ (𝑃𝑀) ≤ (𝑃𝑘) ∧ (𝑃𝑘) ≤ (𝑃‘(𝑘 + 1)))))
524521, 522, 523syl2anc 692 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ((𝑃𝑘) ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))) ↔ ((𝑃𝑘) ∈ ℝ* ∧ (𝑃𝑀) ≤ (𝑃𝑘) ∧ (𝑃𝑘) ≤ (𝑃‘(𝑘 + 1)))))
525465, 510, 520, 524mpbir3and 1243 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑘) ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))))
526 simpll 789 . . . . . . . . . 10 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝜑)
527 eliccxr 39148 . . . . . . . . . . . 12 (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))) → 𝑡 ∈ ℝ*)
528527adantl 482 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ℝ*)
52978ad2antrr 761 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃𝑀) ∈ ℝ*)
530522adantr 481 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ∈ ℝ*)
531 simpr 477 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))))
532 iccgelb 12172 . . . . . . . . . . . 12 (((𝑃𝑀) ∈ ℝ* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ*𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃𝑀) ≤ 𝑡)
533529, 530, 531, 532syl3anc 1323 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃𝑀) ≤ 𝑡)
53477ad2antrr 761 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃𝑀) ∈ ℝ)
535458adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ∈ ℝ)
536 eliccre 39139 . . . . . . . . . . . . 13 (((𝑃𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ℝ)
537534, 535, 531, 536syl3anc 1323 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ℝ)
53866ad2antrr 761 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃𝑁) ∈ ℝ)
539 iccleub 12171 . . . . . . . . . . . . 13 (((𝑃𝑀) ∈ ℝ* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ*𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ≤ (𝑃‘(𝑘 + 1)))
540529, 530, 531, 539syl3anc 1323 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ≤ (𝑃‘(𝑘 + 1)))
541 eluz2 11637 . . . . . . . . . . . . . . 15 (𝑁 ∈ (ℤ‘(𝑘 + 1)) ↔ ((𝑘 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑘 + 1) ≤ 𝑁))
542445, 511, 453, 541syl3anbrc 1244 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ (ℤ‘(𝑘 + 1)))
54348ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ)
5441ad2antrr 761 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 ∈ ℤ)
5455ad2antrr 761 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑁 ∈ ℤ)
546 elfzelz 12284 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖 ∈ ℤ)
547546adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℤ)
548544, 545, 5473jca 1240 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ))
54950ad2antrr 761 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 ∈ ℝ)
550547zred 11426 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℝ)
551184adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 ∈ ℝ)
552189adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 < 𝑘)
553183adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 ∈ ℝ)
554 1red 9999 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 1 ∈ ℝ)
555553, 554readdcld 10013 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑘 + 1) ∈ ℝ)
556546zred 11426 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖 ∈ ℝ)
557556adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℝ)
558553ltp1d 10898 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < (𝑘 + 1))
559 elfzle1 12286 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ ((𝑘 + 1)...𝑁) → (𝑘 + 1) ≤ 𝑖)
560559adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑘 + 1) ≤ 𝑖)
561553, 555, 557, 558, 560ltletrd 10141 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < 𝑖)
562561adantll 749 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < 𝑖)
563549, 551, 550, 552, 562lttrd 10142 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 < 𝑖)
564549, 550, 563ltled 10129 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀𝑖)
565 elfzle2 12287 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖𝑁)
566565adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖𝑁)
567548, 564, 566jca32 557 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑀𝑖𝑖𝑁)))
568 elfz2 12275 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑀𝑖𝑖𝑁)))
569567, 568sylibr 224 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ (𝑀...𝑁))
570543, 569ffvelrnd 6316 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑃𝑖) ∈ ℝ)
57148ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
5721ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℤ)
5735ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℤ)
574 elfzelz 12284 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ∈ ℤ)
575574adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℤ)
576572, 573, 5753jca 1240 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ))
57750ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℝ)
578575zred 11426 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
579184adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 ∈ ℝ)
580189adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < 𝑘)
581183adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 ∈ ℝ)
582 1red 9999 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
583581, 582readdcld 10013 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑘 + 1) ∈ ℝ)
584574zred 11426 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ∈ ℝ)
585584adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
586581ltp1d 10898 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < (𝑘 + 1))
587 elfzle1 12286 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → (𝑘 + 1) ≤ 𝑖)
588587adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑘 + 1) ≤ 𝑖)
589581, 583, 585, 586, 588ltletrd 10141 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < 𝑖)
590589adantll 749 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < 𝑖)
591577, 579, 578, 580, 590lttrd 10142 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < 𝑖)
592577, 578, 591ltled 10129 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀𝑖)
593584adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
59410adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℝ)
595 1red 9999 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
596594, 595resubcld 10402 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
597 elfzle2 12287 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ≤ (𝑁 − 1))
598597adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ≤ (𝑁 − 1))
599594ltm1d 10900 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
600593, 596, 594, 598, 599lelttrd 10139 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 < 𝑁)
601593, 594, 600ltled 10129 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖𝑁)
602601adantlr 750 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖𝑁)
603576, 592, 602jca32 557 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑀𝑖𝑖𝑁)))
604603, 568sylibr 224 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑁))
605571, 604ffvelrnd 6316 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃𝑖) ∈ ℝ)
606575peano2zd 11429 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℤ)
607572, 573, 6063jca 1240 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ))
608606zred 11426 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ)
609578ltp1d 10898 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 < (𝑖 + 1))
610579, 578, 608, 590, 609lttrd 10142 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < (𝑖 + 1))
611577, 579, 608, 580, 610lttrd 10142 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < (𝑖 + 1))
612577, 608, 611ltled 10129 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ≤ (𝑖 + 1))
613600adantlr 750 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 < 𝑁)
614574, 511, 132syl2anr 495 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
615613, 614mpbid 222 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁)
616607, 612, 615jca32 557 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ) ∧ (𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
617 elfz2 12275 . . . . . . . . . . . . . . . . 17 ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ) ∧ (𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
618616, 617sylibr 224 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁))
619571, 618ffvelrnd 6316 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
620 simpll 789 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝜑)
621 eluz2 11637 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 𝑀𝑖))
622572, 575, 592, 621syl3anbrc 1244 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (ℤ𝑀))
623622, 573, 613, 143syl3anbrc 1244 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀..^𝑁))
624620, 623, 145syl2anc 692 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃𝑖) < (𝑃‘(𝑖 + 1)))
625605, 619, 624ltled 10129 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃𝑖) ≤ (𝑃‘(𝑖 + 1)))
626542, 570, 625monoord 12771 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ≤ (𝑃𝑁))
627626adantr 481 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ≤ (𝑃𝑁))
628537, 535, 538, 540, 627letrd 10138 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ≤ (𝑃𝑁))
629422ad2antrr 761 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → ((𝑃𝑀) ∈ ℝ* ∧ (𝑃𝑁) ∈ ℝ*))
630629, 424syl 17 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)) ↔ (𝑡 ∈ ℝ* ∧ (𝑃𝑀) ≤ 𝑡𝑡 ≤ (𝑃𝑁))))
631528, 533, 628, 630mpbir3and 1243 . . . . . . . . . 10 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)))
632526, 631, 152syl2anc 692 . . . . . . . . 9 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝐴 ∈ ℂ)
633 nfv 1840 . . . . . . . . . 10 𝑡(𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁))
6341adantr 481 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ∈ ℤ)
635 elfzouz 12415 . . . . . . . . . . 11 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 ∈ (ℤ‘(𝑀 + 1)))
636635adantl 482 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (ℤ‘(𝑀 + 1)))
637 simpll 789 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝜑)
638 elfzouz 12415 . . . . . . . . . . . . 13 (𝑖 ∈ (𝑀..^𝑘) → 𝑖 ∈ (ℤ𝑀))
639638adantl 482 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 ∈ (ℤ𝑀))
6405ad2antrr 761 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑁 ∈ ℤ)
641 elfzoelz 12411 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀..^𝑘) → 𝑖 ∈ ℤ)
642641zred 11426 . . . . . . . . . . . . . 14 (𝑖 ∈ (𝑀..^𝑘) → 𝑖 ∈ ℝ)
643642adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 ∈ ℝ)
644184adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑘 ∈ ℝ)
64510ad2antrr 761 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑁 ∈ ℝ)
646 elfzolt2 12420 . . . . . . . . . . . . . 14 (𝑖 ∈ (𝑀..^𝑘) → 𝑖 < 𝑘)
647646adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 < 𝑘)
648450adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑘 < 𝑁)
649643, 644, 645, 647, 648lttrd 10142 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 < 𝑁)
650639, 640, 649, 143syl3anbrc 1244 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 ∈ (𝑀..^𝑁))
651637, 650, 145syl2anc 692 . . . . . . . . . 10 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → (𝑃𝑖) < (𝑃‘(𝑖 + 1)))
652 simpll 789 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → 𝜑)
65377ad2antrr 761 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → (𝑃𝑀) ∈ ℝ)
65466ad2antrr 761 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → (𝑃𝑁) ∈ ℝ)
655464adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → (𝑃𝑘) ∈ ℝ)
656 simpr 477 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)))
657 eliccre 39139 . . . . . . . . . . . . 13 (((𝑃𝑀) ∈ ℝ ∧ (𝑃𝑘) ∈ ℝ ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → 𝑡 ∈ ℝ)
658653, 655, 656, 657syl3anc 1323 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → 𝑡 ∈ ℝ)
65978ad2antrr 761 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → (𝑃𝑀) ∈ ℝ*)
660465adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → (𝑃𝑘) ∈ ℝ*)
661 iccgelb 12172 . . . . . . . . . . . . 13 (((𝑃𝑀) ∈ ℝ* ∧ (𝑃𝑘) ∈ ℝ*𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → (𝑃𝑀) ≤ 𝑡)
662659, 660, 656, 661syl3anc 1323 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → (𝑃𝑀) ≤ 𝑡)
663 iccleub 12171 . . . . . . . . . . . . . 14 (((𝑃𝑀) ∈ ℝ* ∧ (𝑃𝑘) ∈ ℝ*𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → 𝑡 ≤ (𝑃𝑘))
664659, 660, 656, 663syl3anc 1323 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → 𝑡 ≤ (𝑃𝑘))
665 elfzouz2 12425 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑁 ∈ (ℤ𝑘))
666665adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ (ℤ𝑘))
66748ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ)
6681ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀 ∈ ℤ)
6695ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑁 ∈ ℤ)
670 elfzelz 12284 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (𝑘...𝑁) → 𝑖 ∈ ℤ)
671670adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑖 ∈ ℤ)
672668, 669, 6713jca 1240 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ))
67350ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀 ∈ ℝ)
674671zred 11426 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑖 ∈ ℝ)
675184adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑘 ∈ ℝ)
676189adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀 < 𝑘)
677 elfzle1 12286 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (𝑘...𝑁) → 𝑘𝑖)
678677adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑘𝑖)
679673, 675, 674, 676, 678ltletrd 10141 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀 < 𝑖)
680673, 674, 679ltled 10129 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀𝑖)
681 elfzle2 12287 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (𝑘...𝑁) → 𝑖𝑁)
682681adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑖𝑁)
683672, 680, 682jca32 557 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑀𝑖𝑖𝑁)))
684683, 568sylibr 224 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑖 ∈ (𝑀...𝑁))
685667, 684ffvelrnd 6316 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → (𝑃𝑖) ∈ ℝ)
68648ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
6871ad2antrr 761 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 ∈ ℤ)
6885ad2antrr 761 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑁 ∈ ℤ)
689 elfzelz 12284 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (𝑘...(𝑁 − 1)) → 𝑖 ∈ ℤ)
690689adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ ℤ)
691687, 688, 6903jca 1240 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ))
69250ad2antrr 761 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 ∈ ℝ)
693690zred 11426 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ ℝ)
694184adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑘 ∈ ℝ)
695189adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 < 𝑘)
696 elfzle1 12286 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (𝑘...(𝑁 − 1)) → 𝑘𝑖)
697696adantl 482 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑘𝑖)
698692, 694, 693, 695, 697ltletrd 10141 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 < 𝑖)
699692, 693, 698ltled 10129 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀𝑖)
700689zred 11426 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (𝑘...(𝑁 − 1)) → 𝑖 ∈ ℝ)
701700adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ ℝ)
70210adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑁 ∈ ℝ)
703 1red 9999 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → 1 ∈ ℝ)
704702, 703resubcld 10402 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
705 elfzle2 12287 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (𝑘...(𝑁 − 1)) → 𝑖 ≤ (𝑁 − 1))
706705adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ≤ (𝑁 − 1))
707702ltm1d 10900 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
708701, 704, 702, 706, 707lelttrd 10139 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 < 𝑁)
709701, 702, 708ltled 10129 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖𝑁)
710709adantlr 750 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖𝑁)
711691, 699, 710jca32 557 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑀𝑖𝑖𝑁)))
712711, 568sylibr 224 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑁))
713686, 712ffvelrnd 6316 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑃𝑖) ∈ ℝ)
714690peano2zd 11429 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ∈ ℤ)
715687, 688, 7143jca 1240 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ))
716714zred 11426 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ)
717693ltp1d 10898 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 < (𝑖 + 1))
718692, 693, 716, 699, 717lelttrd 10139 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 < (𝑖 + 1))
719692, 716, 718ltled 10129 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 ≤ (𝑖 + 1))
720689, 5, 132syl2anr 495 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
721708, 720mpbid 222 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁)
722721adantlr 750 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁)
723715, 719, 722jca32 557 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ) ∧ (𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
724723, 617sylibr 224 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁))
725686, 724ffvelrnd 6316 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
726 simpll 789 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝜑)
727687, 690, 699, 621syl3anbrc 1244 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ (ℤ𝑀))
728708adantlr 750 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 < 𝑁)
729727, 688, 728, 143syl3anbrc 1244 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ (𝑀..^𝑁))
730726, 729, 145syl2anc 692 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑃𝑖) < (𝑃‘(𝑖 + 1)))
731713, 725, 730ltled 10129 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑃𝑖) ≤ (𝑃‘(𝑖 + 1)))
732666, 685, 731monoord 12771 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑘) ≤ (𝑃𝑁))
733732adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → (𝑃𝑘) ≤ (𝑃𝑁))
734658, 655, 654, 664, 733letrd 10138 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → 𝑡 ≤ (𝑃𝑁))
735653, 654, 658, 662, 734eliccd 39137 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)))
736652, 735, 152syl2anc 692 . . . . . . . . . 10 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘))) → 𝐴 ∈ ℂ)
737637, 650, 167syl2anc 692 . . . . . . . . . 10 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1)
738633, 634, 636, 467, 651, 736, 737iblspltprt 39496 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)) ↦ 𝐴) ∈ 𝐿1)
739435mpteq1d 4698 . . . . . . . . . . . . 13 (𝑖 = 𝑘 → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) = (𝑡 ∈ ((𝑃𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴))
740739eleq1d 2683 . . . . . . . . . . . 12 (𝑖 = 𝑘 → ((𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1))
741515, 740imbi12d 334 . . . . . . . . . . 11 (𝑖 = 𝑘 → (((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1) ↔ ((𝜑𝑘 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1)))
742741, 167chvarv 2262 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1)
743513, 742syldan 487 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑡 ∈ ((𝑃𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1)
744442, 458, 525, 632, 738, 743itgspliticc 23509 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ∫((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = (∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
745744eqcomd 2627 . . . . . . 7 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = ∫((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡)
7467453adant3 1079 . . . . . 6 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → (∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 + ∫((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = ∫((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡)
747438, 441, 7463eqtrrd 2660 . . . . 5 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → ∫((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
748177, 178, 180, 747syl3anc 1323 . . . 4 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → ∫((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
7497483exp 1261 . . 3 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → ((𝜑 → ∫((𝑃𝑀)[,](𝑃𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → (𝜑 → ∫((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)))
75021, 28, 35, 42, 176, 749fzind2 12526 . 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 384  w3a 1036   = wceq 1480  wcel 1987   class class class wbr 4613  cmpt 4673  wf 5843  cfv 5847  (class class class)co 6604  cc 9878  cr 9879  1c1 9881   + caddc 9883  *cxr 10017   < clt 10018  cle 10019  cmin 10210  cz 11321  cuz 11631  [,]cicc 12120  ...cfz 12268  ..^cfzo 12406  Σcsu 14350  𝐿1cibl 23292  citg 23293
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-inf2 8482  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957  ax-pre-sup 9958  ax-addf 9959
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-disj 4584  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-of 6850  df-ofr 6851  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-2o 7506  df-oadd 7509  df-er 7687  df-map 7804  df-pm 7805  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-fi 8261  df-sup 8292  df-inf 8293  df-oi 8359  df-card 8709  df-cda 8934  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-div 10629  df-nn 10965  df-2 11023  df-3 11024  df-4 11025  df-n0 11237  df-z 11322  df-uz 11632  df-q 11733  df-rp 11777  df-xneg 11890  df-xadd 11891  df-xmul 11892  df-ioo 12121  df-ico 12123  df-icc 12124  df-fz 12269  df-fzo 12407  df-fl 12533  df-mod 12609  df-seq 12742  df-exp 12801  df-hash 13058  df-cj 13773  df-re 13774  df-im 13775  df-sqrt 13909  df-abs 13910  df-clim 14153  df-sum 14351  df-rest 16004  df-topgen 16025  df-psmet 19657  df-xmet 19658  df-met 19659  df-bl 19660  df-mopn 19661  df-top 20621  df-bases 20622  df-topon 20623  df-cmp 21100  df-ovol 23140  df-vol 23141  df-mbf 23294  df-itg1 23295  df-itg2 23296  df-ibl 23297  df-itg 23298
This theorem is referenced by:  fourierdlem73  39703  fourierdlem81  39711  fourierdlem93  39723
  Copyright terms: Public domain W3C validator