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 43527
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 . . . 4 (𝜑 → 𝑀 ∈ ℤ)
21peano2zd 12438 . . 3 (𝜑 → (𝑀 + 1) ∈ ℤ)
3 itgspltprt.2 . . . 4 (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))
4 eluzelz 12601 . . . 4 (𝑁 ∈ (ℤ≥‘(𝑀 + 1)) → 𝑁 ∈ ℤ)
53, 4syl 17 . . 3 (𝜑 → 𝑁 ∈ ℤ)
6 eluzle 12604 . . . 4 (𝑁 ∈ (ℤ≥‘(𝑀 + 1)) → (𝑀 + 1) ≤ 𝑁)
73, 6syl 17 . . 3 (𝜑 → (𝑀 + 1) ≤ 𝑁)
8 eluzelre 12602 . . . . 5 (𝑁 ∈ (ℤ≥‘(𝑀 + 1)) → 𝑁 ∈ ℝ)
93, 8syl 17 . . . 4 (𝜑 → 𝑁 ∈ ℝ)
109leidd 11550 . . 3 (𝜑 → 𝑁 ≤ 𝑁)
112, 5, 5, 7, 10elfzd 13256 . 2 (𝜑 → 𝑁 ∈ ((𝑀 + 1)...𝑁))
12 fveq2 6783 . . . . . . 7 (𝑗 = (𝑀 + 1) → (𝑃‘𝑗) = (𝑃‘(𝑀 + 1)))
1312oveq2d 7300 . . . . . 6 (𝑗 = (𝑀 + 1) → ((𝑃‘𝑀)[,](𝑃‘𝑗)) = ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))))
1413itgeq1d 43505 . . . . 5 (𝑗 = (𝑀 + 1) → ∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡)
15 oveq2 7292 . . . . . 6 (𝑗 = (𝑀 + 1) → (𝑀..^𝑗) = (𝑀..^(𝑀 + 1)))
1615sumeq1d 15422 . . . . 5 (𝑗 = (𝑀 + 1) → Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
1714, 16eqeq12d 2755 . . . 4 (𝑗 = (𝑀 + 1) → (∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ↔ ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
1817imbi2d 341 . . 3 (𝑗 = (𝑀 + 1) → ((𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ↔ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)))
19 fveq2 6783 . . . . . . 7 (𝑗 = 𝑘 → (𝑃‘𝑗) = (𝑃‘𝑘))
2019oveq2d 7300 . . . . . 6 (𝑗 = 𝑘 → ((𝑃‘𝑀)[,](𝑃‘𝑗)) = ((𝑃‘𝑀)[,](𝑃‘𝑘)))
2120itgeq1d 43505 . . . . 5 (𝑗 = 𝑘 → ∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡)
22 oveq2 7292 . . . . . 6 (𝑗 = 𝑘 → (𝑀..^𝑗) = (𝑀..^𝑘))
2322sumeq1d 15422 . . . . 5 (𝑗 = 𝑘 → Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
2421, 23eqeq12d 2755 . . . 4 (𝑗 = 𝑘 → (∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ↔ ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
2524imbi2d 341 . . 3 (𝑗 = 𝑘 → ((𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ↔ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)))
26 fveq2 6783 . . . . . . 7 (𝑗 = (𝑘 + 1) → (𝑃‘𝑗) = (𝑃‘(𝑘 + 1)))
2726oveq2d 7300 . . . . . 6 (𝑗 = (𝑘 + 1) → ((𝑃‘𝑀)[,](𝑃‘𝑗)) = ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))))
2827itgeq1d 43505 . . . . 5 (𝑗 = (𝑘 + 1) → ∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = ∫((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡)
29 oveq2 7292 . . . . . 6 (𝑗 = (𝑘 + 1) → (𝑀..^𝑗) = (𝑀..^(𝑘 + 1)))
3029sumeq1d 15422 . . . . 5 (𝑗 = (𝑘 + 1) → Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
3128, 30eqeq12d 2755 . . . 4 (𝑗 = (𝑘 + 1) → (∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ↔ ∫((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
3231imbi2d 341 . . 3 (𝑗 = (𝑘 + 1) → ((𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ↔ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)))
33 fveq2 6783 . . . . . . 7 (𝑗 = 𝑁 → (𝑃‘𝑗) = (𝑃‘𝑁))
3433oveq2d 7300 . . . . . 6 (𝑗 = 𝑁 → ((𝑃‘𝑀)[,](𝑃‘𝑗)) = ((𝑃‘𝑀)[,](𝑃‘𝑁)))
3534itgeq1d 43505 . . . . 5 (𝑗 = 𝑁 → ∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = ∫((𝑃‘𝑀)[,](𝑃‘𝑁))𝐴 d𝑡)
36 oveq2 7292 . . . . . 6 (𝑗 = 𝑁 → (𝑀..^𝑗) = (𝑀..^𝑁))
3736sumeq1d 15422 . . . . 5 (𝑗 = 𝑁 → Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
3835, 37eqeq12d 2755 . . . 4 (𝑗 = 𝑁 → (∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ↔ ∫((𝑃‘𝑀)[,](𝑃‘𝑁))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
3938imbi2d 341 . . 3 (𝑗 = 𝑁 → ((𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ↔ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑁))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)))
401adantl 482 . . . . . . . 8 ((𝑁 ∈ (ℤ≥‘(𝑀 + 1)) ∧ 𝜑) → 𝑀 ∈ ℤ)
41 fzval3 13465 . . . . . . . 8 (𝑀 ∈ ℤ → (𝑀...𝑀) = (𝑀..^(𝑀 + 1)))
4240, 41syl 17 . . . . . . 7 ((𝑁 ∈ (ℤ≥‘(𝑀 + 1)) ∧ 𝜑) → (𝑀...𝑀) = (𝑀..^(𝑀 + 1)))
4342eqcomd 2745 . . . . . 6 ((𝑁 ∈ (ℤ≥‘(𝑀 + 1)) ∧ 𝜑) → (𝑀..^(𝑀 + 1)) = (𝑀...𝑀))
4443sumeq1d 15422 . . . . 5 ((𝑁 ∈ (ℤ≥‘(𝑀 + 1)) ∧ 𝜑) → Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀...𝑀)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
45 itgspltprt.3 . . . . . . . . . . . 12 (𝜑 → 𝑃:(𝑀...𝑁)⟶ℝ)
4645adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑃:(𝑀...𝑁)⟶ℝ)
471zred 12435 . . . . . . . . . . . . . . 15 (𝜑 → 𝑀 ∈ ℝ)
48 1red 10985 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ∈ ℝ)
4947, 48readdcld 11013 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑀 + 1) ∈ ℝ)
5047ltp1d 11914 . . . . . . . . . . . . . . . 16 (𝜑 → 𝑀 < (𝑀 + 1))
5147, 49, 9, 50, 7ltletrd 11144 . . . . . . . . . . . . . . 15 (𝜑 → 𝑀 < 𝑁)
5247, 9, 51ltled 11132 . . . . . . . . . . . . . 14 (𝜑 → 𝑀 ≤ 𝑁)
53 eluz 12605 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁))
541, 5, 53syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁))
5552, 54mpbird 256 . . . . . . . . . . . . 13 (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))
56 eluzfz1 13272 . . . . . . . . . . . . 13 (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁))
5755, 56syl 17 . . . . . . . . . . . 12 (𝜑 → 𝑀 ∈ (𝑀...𝑁))
5857adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑀 ∈ (𝑀...𝑁))
5946, 58ffvelrnd 6971 . . . . . . . . . 10 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘𝑀) ∈ ℝ)
601, 5, 5, 52, 10elfzd 13256 . . . . . . . . . . . 12 (𝜑 → 𝑁 ∈ (𝑀...𝑁))
6145, 60ffvelrnd 6971 . . . . . . . . . . 11 (𝜑 → (𝑃‘𝑁) ∈ ℝ)
6261adantr 481 . . . . . . . . . 10 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘𝑁) ∈ ℝ)
6347lep1d 11915 . . . . . . . . . . . . . 14 (𝜑 → 𝑀 ≤ (𝑀 + 1))
641, 5, 2, 63, 7elfzd 13256 . . . . . . . . . . . . 13 (𝜑 → (𝑀 + 1) ∈ (𝑀...𝑁))
6545, 64ffvelrnd 6971 . . . . . . . . . . . 12 (𝜑 → (𝑃‘(𝑀 + 1)) ∈ ℝ)
6665adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘(𝑀 + 1)) ∈ ℝ)
67 simpr 485 . . . . . . . . . . 11 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))))
68 eliccre 43050 . . . . . . . . . . 11 (((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘(𝑀 + 1)) ∈ ℝ ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ∈ ℝ)
6959, 66, 67, 68syl3anc 1370 . . . . . . . . . 10 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ∈ ℝ)
7045, 57ffvelrnd 6971 . . . . . . . . . . . . 13 (𝜑 → (𝑃‘𝑀) ∈ ℝ)
7170rexrd 11034 . . . . . . . . . . . 12 (𝜑 → (𝑃‘𝑀) ∈ ℝ*)
7271adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘𝑀) ∈ ℝ*)
7366rexrd 11034 . . . . . . . . . . 11 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘(𝑀 + 1)) ∈ ℝ*)
74 iccgelb 13144 . . . . . . . . . . 11 (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘(𝑀 + 1)) ∈ ℝ* ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘𝑀) ≤ 𝑡)
7572, 73, 67, 74syl3anc 1370 . . . . . . . . . 10 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘𝑀) ≤ 𝑡)
76 iccleub 13143 . . . . . . . . . . . 12 (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘(𝑀 + 1)) ∈ ℝ* ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ≤ (𝑃‘(𝑀 + 1)))
7772, 73, 67, 76syl3anc 1370 . . . . . . . . . . 11 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ≤ (𝑃‘(𝑀 + 1)))
7845adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ)
79 elfzelz 13265 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ((𝑀 + 1)...𝑁) → 𝑖 ∈ ℤ)
8079adantl 482 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑖 ∈ ℤ)
8147adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑀 ∈ ℝ)
8280zred 12435 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑖 ∈ ℝ)
8349adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑀 + 1) ∈ ℝ)
8450adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑀 < (𝑀 + 1))
85 elfzle1 13268 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ((𝑀 + 1)...𝑁) → (𝑀 + 1) ≤ 𝑖)
8685adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑀 + 1) ≤ 𝑖)
8781, 83, 82, 84, 86ltletrd 11144 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑀 < 𝑖)
8881, 82, 87ltled 11132 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑀 ≤ 𝑖)
89 elfzle2 13269 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ((𝑀 + 1)...𝑁) → 𝑖 ≤ 𝑁)
9089adantl 482 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑖 ≤ 𝑁)
911, 5jca 512 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
9291adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
93 elfz1 13253 . . . . . . . . . . . . . . . 16 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)))
9492, 93syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)))
9580, 88, 90, 94mpbir3and 1341 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑖 ∈ (𝑀...𝑁))
9678, 95ffvelrnd 6971 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑃‘𝑖) ∈ ℝ)
9745adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
98 elfzelz 13265 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1)) → 𝑖 ∈ ℤ)
9998adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℤ)
10047adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℝ)
10199zred 12435 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
10249adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑀 + 1) ∈ ℝ)
10350adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 < (𝑀 + 1))
104 elfzle1 13268 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1)) → (𝑀 + 1) ≤ 𝑖)
105104adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑀 + 1) ≤ 𝑖)
106100, 102, 101, 103, 105ltletrd 11144 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 < 𝑖)
107100, 101, 106ltled 11132 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 ≤ 𝑖)
1089adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℝ)
109 1red 10985 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
110108, 109resubcld 11412 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
111 elfzle2 13269 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1)) → 𝑖 ≤ (𝑁 − 1))
112111adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ≤ (𝑁 − 1))
113108ltm1d 11916 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
114101, 110, 108, 112, 113lelttrd 11142 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 < 𝑁)
115101, 108, 114ltled 11132 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ≤ 𝑁)
11691adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
117116, 93syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)))
11899, 107, 115, 117mpbir3and 1341 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑁))
11997, 118ffvelrnd 6971 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑃‘𝑖) ∈ ℝ)
12099peano2zd 12438 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℤ)
121101, 109readdcld 11013 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ)
122100, 101, 109, 106ltadd1dd 11595 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑀 + 1) < (𝑖 + 1))
123100, 102, 121, 103, 122lttrd 11145 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 < (𝑖 + 1))
124100, 121, 123ltled 11132 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 ≤ (𝑖 + 1))
125 zltp1le 12379 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
12698, 5, 125syl2anr 597 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
127114, 126mpbid 231 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁)
128 elfz1 13253 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
129116, 128syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
130120, 124, 127, 129mpbir3and 1341 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁))
13197, 130ffvelrnd 6971 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
132 eluz 12605 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑖 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑖))
1331, 98, 132syl2an 596 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑖))
134107, 133mpbird 256 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ (ℤ≥‘𝑀))
1355adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℤ)
136 elfzo2 13399 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀..^𝑁) ↔ (𝑖 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑖 < 𝑁))
137134, 135, 114, 136syl3anbrc 1342 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀..^𝑁))
138 itgspltprt.4 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1)))
139137, 138syldan 591 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1)))
140119, 131, 139ltled 11132 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑃‘𝑖) ≤ (𝑃‘(𝑖 + 1)))
1413, 96, 140monoord 13762 . . . . . . . . . . . 12 (𝜑 → (𝑃‘(𝑀 + 1)) ≤ (𝑃‘𝑁))
142141adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘(𝑀 + 1)) ≤ (𝑃‘𝑁))
14369, 66, 62, 77, 142letrd 11141 . . . . . . . . . 10 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ≤ (𝑃‘𝑁))
14459, 62, 69, 75, 143eliccd 43049 . . . . . . . . 9 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)))
145 itgspltprt.5 . . . . . . . . 9 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁))) → 𝐴 ∈ ℂ)
146144, 145syldan 591 . . . . . . . 8 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝐴 ∈ ℂ)
147 id 22 . . . . . . . . . 10 (𝜑 → 𝜑)
148 fzolb 13402 . . . . . . . . . . 11 (𝑀 ∈ (𝑀..^𝑁) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁))
1491, 5, 51, 148syl3anbrc 1342 . . . . . . . . . 10 (𝜑 → 𝑀 ∈ (𝑀..^𝑁))
150147, 149jca 512 . . . . . . . . 9 (𝜑 → (𝜑 ∧ 𝑀 ∈ (𝑀..^𝑁)))
151 eleq1 2827 . . . . . . . . . . . 12 (𝑖 = 𝑀 → (𝑖 ∈ (𝑀..^𝑁) ↔ 𝑀 ∈ (𝑀..^𝑁)))
152151anbi2d 629 . . . . . . . . . . 11 (𝑖 = 𝑀 → ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ↔ (𝜑 ∧ 𝑀 ∈ (𝑀..^𝑁))))
153 fveq2 6783 . . . . . . . . . . . . . 14 (𝑖 = 𝑀 → (𝑃‘𝑖) = (𝑃‘𝑀))
154 fvoveq1 7307 . . . . . . . . . . . . . 14 (𝑖 = 𝑀 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑀 + 1)))
155153, 154oveq12d 7302 . . . . . . . . . . . . 13 (𝑖 = 𝑀 → ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) = ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))))
156155mpteq1d 5170 . . . . . . . . . . . 12 (𝑖 = 𝑀 → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) = (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴))
157156eleq1d 2824 . . . . . . . . . . 11 (𝑖 = 𝑀 → ((𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿1))
158152, 157imbi12d 345 . . . . . . . . . 10 (𝑖 = 𝑀 → (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1) ↔ ((𝜑 ∧ 𝑀 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿1)))
159 itgspltprt.6 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1)
160158, 159vtoclg 3506 . . . . . . . . 9 (𝑀 ∈ ℤ → ((𝜑 ∧ 𝑀 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿1))
1611, 150, 160sylc 65 . . . . . . . 8 (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿1)
162146, 161itgcl 24957 . . . . . . 7 (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 ∈ ℂ)
163155itgeq1d 43505 . . . . . . . 8 (𝑖 = 𝑀 → ∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡)
164163fsum1 15468 . . . . . . 7 ((𝑀 ∈ ℤ ∧ ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 ∈ ℂ) → Σ𝑖 ∈ (𝑀...𝑀)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡)
1651, 162, 164syl2anc 584 . . . . . 6 (𝜑 → Σ𝑖 ∈ (𝑀...𝑀)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡)
166165adantl 482 . . . . 5 ((𝑁 ∈ (ℤ≥‘(𝑀 + 1)) ∧ 𝜑) → Σ𝑖 ∈ (𝑀...𝑀)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡)
16744, 166eqtr2d 2780 . . . 4 ((𝑁 ∈ (ℤ≥‘(𝑀 + 1)) ∧ 𝜑) → ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
168167ex 413 . . 3 (𝑁 ∈ (ℤ≥‘(𝑀 + 1)) → (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
169 simp3 1137 . . . . 5 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → 𝜑)
170 simp1 1135 . . . . 5 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → 𝑘 ∈ ((𝑀 + 1)..^𝑁))
171 simp2 1136 . . . . . 6 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
172169, 171mpd 15 . . . . 5 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
17347adantr 481 . . . . . . . . . 10 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ∈ ℝ)
174 elfzoelz 13396 . . . . . . . . . . . 12 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 ∈ ℤ)
175174zred 12435 . . . . . . . . . . 11 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 ∈ ℝ)
176175adantl 482 . . . . . . . . . 10 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ ℝ)
17749adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 + 1) ∈ ℝ)
17850adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < (𝑀 + 1))
179 elfzole1 13404 . . . . . . . . . . . 12 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑀 + 1) ≤ 𝑘)
180179adantl 482 . . . . . . . . . . 11 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 + 1) ≤ 𝑘)
181173, 177, 176, 178, 180ltletrd 11144 . . . . . . . . . 10 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < 𝑘)
182173, 176, 181ltled 11132 . . . . . . . . 9 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ≤ 𝑘)
183 eluz 12605 . . . . . . . . . 10 ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑘))
1841, 174, 183syl2an 596 . . . . . . . . 9 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑘))
185182, 184mpbird 256 . . . . . . . 8 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (ℤ≥‘𝑀))
186 simplll 772 . . . . . . . . . 10 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝜑)
187 eliccxr 13176 . . . . . . . . . . . 12 (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) → 𝑡 ∈ ℝ*)
188187adantl 482 . . . . . . . . . . 11 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ℝ*)
189186, 70syl 17 . . . . . . . . . . . 12 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘𝑀) ∈ ℝ)
190186, 45syl 17 . . . . . . . . . . . . 13 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑃:(𝑀...𝑁)⟶ℝ)
191 elfzelz 13265 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀...𝑘) → 𝑖 ∈ ℤ)
192191adantl 482 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ ℤ)
193 elfzle1 13268 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀...𝑘) → 𝑀 ≤ 𝑖)
194193adantl 482 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 ≤ 𝑖)
195192zred 12435 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ ℝ)
1969ad2antrr 723 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑁 ∈ ℝ)
197176adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑘 ∈ ℝ)
198 elfzle2 13269 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (𝑀...𝑘) → 𝑖 ≤ 𝑘)
199198adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ≤ 𝑘)
200 elfzolt2 13405 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 < 𝑁)
201200ad2antlr 724 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑘 < 𝑁)
202195, 197, 196, 199, 201lelttrd 11142 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 < 𝑁)
203195, 196, 202ltled 11132 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ≤ 𝑁)
20491ad2antrr 723 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
205204, 93syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)))
206192, 194, 203, 205mpbir3and 1341 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ (𝑀...𝑁))
207206adantr 481 . . . . . . . . . . . . 13 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑖 ∈ (𝑀...𝑁))
208190, 207ffvelrnd 6971 . . . . . . . . . . . 12 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘𝑖) ∈ ℝ)
209192peano2zd 12438 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ∈ ℤ)
21047ad2antrr 723 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 ∈ ℝ)
211209zred 12435 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ∈ ℝ)
21247adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 ∈ ℝ)
213191zred 12435 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (𝑀...𝑘) → 𝑖 ∈ ℝ)
214213adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ ℝ)
215 1red 10985 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘)) → 1 ∈ ℝ)
216214, 215readdcld 11013 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ∈ ℝ)
217193adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 ≤ 𝑖)
218214ltp1d 11914 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 < (𝑖 + 1))
219212, 214, 216, 217, 218lelttrd 11142 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 < (𝑖 + 1))
220219adantlr 712 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 < (𝑖 + 1))
221210, 211, 220ltled 11132 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 ≤ (𝑖 + 1))
2225, 191anim12ci 614 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ))
223222adantlr 712 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ))
224223, 125syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
225202, 224mpbid 231 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ≤ 𝑁)
226204, 128syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
227209, 221, 225, 226mpbir3and 1341 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ∈ (𝑀...𝑁))
228227adantr 481 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑖 + 1) ∈ (𝑀...𝑁))
229190, 228ffvelrnd 6971 . . . . . . . . . . . . 13 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
230 simpr 485 . . . . . . . . . . . . 13 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))))
231 eliccre 43050 . . . . . . . . . . . . 13 (((𝑃‘𝑖) ∈ ℝ ∧ (𝑃‘(𝑖 + 1)) ∈ ℝ ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ℝ)
232208, 229, 230, 231syl3anc 1370 . . . . . . . . . . . 12 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ℝ)
233 elfzuz 13261 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...𝑘) → 𝑖 ∈ (ℤ≥‘𝑀))
234233adantl 482 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ (ℤ≥‘𝑀))
23545ad3antrrr 727 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑃:(𝑀...𝑁)⟶ℝ)
236 elfzelz 13265 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑀...𝑖) → 𝑗 ∈ ℤ)
237236adantl 482 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ∈ ℤ)
238 elfzle1 13268 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑀...𝑖) → 𝑀 ≤ 𝑗)
239238adantl 482 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑀 ≤ 𝑗)
240237zred 12435 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ∈ ℝ)
241196adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑁 ∈ ℝ)
242195adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑖 ∈ ℝ)
243 elfzle2 13269 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (𝑀...𝑖) → 𝑗 ≤ 𝑖)
244243adantl 482 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ≤ 𝑖)
245202adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑖 < 𝑁)
246240, 242, 241, 244, 245lelttrd 11142 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 < 𝑁)
247240, 241, 246ltled 11132 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ≤ 𝑁)
248204adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
249 elfz1 13253 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁)))
250248, 249syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁)))
251237, 239, 247, 250mpbir3and 1341 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ∈ (𝑀...𝑁))
252235, 251ffvelrnd 6971 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝑃‘𝑗) ∈ ℝ)
25345ad3antrrr 727 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
254 elfzelz 13265 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑗 ∈ ℤ)
255254adantl 482 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ ℤ)
256 elfzle1 13268 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑀 ≤ 𝑗)
257256adantl 482 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 ≤ 𝑗)
258255zred 12435 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ ℝ)
259196adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑁 ∈ ℝ)
260195adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑖 ∈ ℝ)
261 1red 10985 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 1 ∈ ℝ)
262260, 261resubcld 11412 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑖 − 1) ∈ ℝ)
263 elfzle2 13269 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑗 ≤ (𝑖 − 1))
264263adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ≤ (𝑖 − 1))
265260ltm1d 11916 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑖 − 1) < 𝑖)
266258, 262, 260, 264, 265lelttrd 11142 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 < 𝑖)
267202adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑖 < 𝑁)
268258, 260, 259, 266, 267lttrd 11145 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 < 𝑁)
269258, 259, 268ltled 11132 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ≤ 𝑁)
270204adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
271270, 249syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁)))
272255, 257, 269, 271mpbir3and 1341 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ (𝑀...𝑁))
273253, 272ffvelrnd 6971 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑃‘𝑗) ∈ ℝ)
274255peano2zd 12438 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ∈ ℤ)
275173ad2antrr 723 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 ∈ ℝ)
276258, 261readdcld 11013 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ∈ ℝ)
27747adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 ∈ ℝ)
278254zred 12435 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑗 ∈ ℝ)
279278adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ ℝ)
280 1red 10985 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 1 ∈ ℝ)
281279, 280readdcld 11013 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ∈ ℝ)
282256adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 ≤ 𝑗)
283279ltp1d 11914 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 < (𝑗 + 1))
284277, 279, 281, 282, 283lelttrd 11142 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 < (𝑗 + 1))
285284ad4ant14 749 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 < (𝑗 + 1))
286275, 276, 285ltled 11132 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 ≤ (𝑗 + 1))
287 zltp1le 12379 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑗 < 𝑖 ↔ (𝑗 + 1) ≤ 𝑖))
288254, 192, 287syl2anr 597 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 < 𝑖 ↔ (𝑗 + 1) ≤ 𝑖))
289266, 288mpbid 231 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ≤ 𝑖)
290276, 260, 259, 289, 267lelttrd 11142 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) < 𝑁)
291276, 259, 290ltled 11132 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ≤ 𝑁)
292 elfz1 13253 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑗 + 1) ∈ (𝑀...𝑁) ↔ ((𝑗 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑗 + 1) ∧ (𝑗 + 1) ≤ 𝑁)))
293270, 292syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → ((𝑗 + 1) ∈ (𝑀...𝑁) ↔ ((𝑗 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑗 + 1) ∧ (𝑗 + 1) ≤ 𝑁)))
294274, 286, 291, 293mpbir3and 1341 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ∈ (𝑀...𝑁))
295253, 294ffvelrnd 6971 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑃‘(𝑗 + 1)) ∈ ℝ)
296 simplll 772 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝜑)
297 elfzuz 13261 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑗 ∈ (ℤ≥‘𝑀))
298297adantl 482 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ (ℤ≥‘𝑀))
299296, 5syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑁 ∈ ℤ)
300 elfzo2 13399 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑀..^𝑁) ↔ (𝑗 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑗 < 𝑁))
301298, 299, 268, 300syl3anbrc 1342 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ (𝑀..^𝑁))
302 eleq1 2827 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → (𝑖 ∈ (𝑀..^𝑁) ↔ 𝑗 ∈ (𝑀..^𝑁)))
303302anbi2d 629 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ↔ (𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁))))
304 fveq2 6783 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → (𝑃‘𝑖) = (𝑃‘𝑗))
305 fvoveq1 7307 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑗 + 1)))
306304, 305breq12d 5088 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → ((𝑃‘𝑖) < (𝑃‘(𝑖 + 1)) ↔ (𝑃‘𝑗) < (𝑃‘(𝑗 + 1))))
307303, 306imbi12d 345 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑗 → (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑃‘𝑗) < (𝑃‘(𝑗 + 1)))))
308307, 138chvarvv 2003 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑃‘𝑗) < (𝑃‘(𝑗 + 1)))
309296, 301, 308syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑃‘𝑗) < (𝑃‘(𝑗 + 1)))
310273, 295, 309ltled 11132 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑃‘𝑗) ≤ (𝑃‘(𝑗 + 1)))
311234, 252, 310monoord 13762 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑃‘𝑀) ≤ (𝑃‘𝑖))
312311adantr 481 . . . . . . . . . . . 12 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘𝑀) ≤ (𝑃‘𝑖))
313208rexrd 11034 . . . . . . . . . . . . 13 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘𝑖) ∈ ℝ*)
314229rexrd 11034 . . . . . . . . . . . . 13 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘(𝑖 + 1)) ∈ ℝ*)
315 iccgelb 13144 . . . . . . . . . . . . 13 (((𝑃‘𝑖) ∈ ℝ* ∧ (𝑃‘(𝑖 + 1)) ∈ ℝ* ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘𝑖) ≤ 𝑡)
316313, 314, 230, 315syl3anc 1370 . . . . . . . . . . . 12 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘𝑖) ≤ 𝑡)
317189, 208, 232, 312, 316letrd 11141 . . . . . . . . . . 11 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘𝑀) ≤ 𝑡)
318186, 61syl 17 . . . . . . . . . . . 12 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘𝑁) ∈ ℝ)
319 iccleub 13143 . . . . . . . . . . . . 13 (((𝑃‘𝑖) ∈ ℝ* ∧ (𝑃‘(𝑖 + 1)) ∈ ℝ* ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ≤ (𝑃‘(𝑖 + 1)))
320313, 314, 230, 319syl3anc 1370 . . . . . . . . . . . 12 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ≤ (𝑃‘(𝑖 + 1)))
3215ad2antrr 723 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑁 ∈ ℤ)
322 eluz 12605 . . . . . . . . . . . . . . . 16 (((𝑖 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘(𝑖 + 1)) ↔ (𝑖 + 1) ≤ 𝑁))
323209, 321, 322syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑁 ∈ (ℤ≥‘(𝑖 + 1)) ↔ (𝑖 + 1) ≤ 𝑁))
324225, 323mpbird 256 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑁 ∈ (ℤ≥‘(𝑖 + 1)))
325324adantr 481 . . . . . . . . . . . . 13 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑁 ∈ (ℤ≥‘(𝑖 + 1)))
32645ad3antrrr 727 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ)
327 elfzelz 13265 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ((𝑖 + 1)...𝑁) → 𝑗 ∈ ℤ)
328327adantl 482 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑗 ∈ ℤ)
329 elfzel1 13264 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (𝑀...𝑘) → 𝑀 ∈ ℤ)
330329zred 12435 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (𝑀...𝑘) → 𝑀 ∈ ℝ)
331330adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀 ∈ ℝ)
332327zred 12435 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ((𝑖 + 1)...𝑁) → 𝑗 ∈ ℝ)
333332adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑗 ∈ ℝ)
334213adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑖 ∈ ℝ)
335 1red 10985 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 1 ∈ ℝ)
336334, 335readdcld 11013 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑖 + 1) ∈ ℝ)
337193adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀 ≤ 𝑖)
338334ltp1d 11914 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑖 < (𝑖 + 1))
339331, 334, 336, 337, 338lelttrd 11142 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀 < (𝑖 + 1))
340 elfzle1 13268 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ((𝑖 + 1)...𝑁) → (𝑖 + 1) ≤ 𝑗)
341340adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑖 + 1) ≤ 𝑗)
342331, 336, 333, 339, 341ltletrd 11144 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀 < 𝑗)
343331, 333, 342ltled 11132 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀 ≤ 𝑗)
344343adantll 711 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀 ≤ 𝑗)
345 elfzle2 13269 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ((𝑖 + 1)...𝑁) → 𝑗 ≤ 𝑁)
346345adantl 482 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑗 ≤ 𝑁)
347204adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
348347, 249syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁)))
349328, 344, 346, 348mpbir3and 1341 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑗 ∈ (𝑀...𝑁))
350326, 349ffvelrnd 6971 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑃‘𝑗) ∈ ℝ)
351350adantlr 712 . . . . . . . . . . . . 13 (((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑃‘𝑗) ∈ ℝ)
352 simplll 772 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝜑)
353 simplr 766 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑘))
354 simpr 485 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1)))
355453ad2ant1 1132 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
356 elfzelz 13265 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1)) → 𝑗 ∈ ℤ)
3573563ad2ant3 1134 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ℤ)
358473ad2ant1 1132 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℝ)
359357zred 12435 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ℝ)
3602163adant3 1131 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ)
3612193adant3 1131 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 < (𝑖 + 1))
362 elfzle1 13268 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1)) → (𝑖 + 1) ≤ 𝑗)
3633623ad2ant3 1134 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑗)
364358, 360, 359, 361, 363ltletrd 11144 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 < 𝑗)
365358, 359, 364ltled 11132 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 ≤ 𝑗)
366356adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ℤ)
367366zred 12435 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ℝ)
3689adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℝ)
369 1red 10985 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
370368, 369resubcld 11412 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
371 elfzle2 13269 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1)) → 𝑗 ≤ (𝑁 − 1))
372371adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ≤ (𝑁 − 1))
373368ltm1d 11916 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
374367, 370, 368, 372, 373lelttrd 11142 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 < 𝑁)
375367, 368, 374ltled 11132 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ≤ 𝑁)
3763753adant2 1130 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ≤ 𝑁)
377913ad2ant1 1132 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
378377, 249syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁)))
379357, 365, 376, 378mpbir3and 1341 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ (𝑀...𝑁))
380355, 379ffvelrnd 6971 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃‘𝑗) ∈ ℝ)
381357peano2zd 12438 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ∈ ℤ)
382381zred 12435 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ∈ ℝ)
3832133ad2ant2 1133 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
384 1red 10985 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
3852183adant3 1131 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖 < (𝑖 + 1))
386383, 360, 359, 385, 363ltletrd 11144 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖 < 𝑗)
387383, 359, 386ltled 11132 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖 ≤ 𝑗)
388383, 359, 384, 387leadd1dd 11598 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ (𝑗 + 1))
389358, 360, 382, 361, 388ltletrd 11144 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 < (𝑗 + 1))
390358, 382, 389ltled 11132 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 ≤ (𝑗 + 1))
391 zltp1le 12379 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 < 𝑁 ↔ (𝑗 + 1) ≤ 𝑁))
392356, 5, 391syl2anr 597 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 < 𝑁 ↔ (𝑗 + 1) ≤ 𝑁))
393374, 392mpbid 231 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ≤ 𝑁)
3943933adant2 1130 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ≤ 𝑁)
395377, 292syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → ((𝑗 + 1) ∈ (𝑀...𝑁) ↔ ((𝑗 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑗 + 1) ∧ (𝑗 + 1) ≤ 𝑁)))
396381, 390, 394, 395mpbir3and 1341 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ∈ (𝑀...𝑁))
397355, 396ffvelrnd 6971 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃‘(𝑗 + 1)) ∈ ℝ)
398 simp1 1135 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝜑)
39913ad2ant1 1132 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℤ)
400 eluz 12605 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑗 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑗))
401399, 357, 400syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑗))
402365, 401mpbird 256 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ (ℤ≥‘𝑀))
40353ad2ant1 1132 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℤ)
4043743adant2 1130 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 < 𝑁)
405402, 403, 404, 300syl3anbrc 1342 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ (𝑀..^𝑁))
406398, 405, 308syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃‘𝑗) < (𝑃‘(𝑗 + 1)))
407380, 397, 406ltled 11132 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃‘𝑗) ≤ (𝑃‘(𝑗 + 1)))
408352, 353, 354, 407syl3anc 1370 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃‘𝑗) ≤ (𝑃‘(𝑗 + 1)))
409408adantlr 712 . . . . . . . . . . . . 13 (((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃‘𝑗) ≤ (𝑃‘(𝑗 + 1)))
410325, 351, 409monoord 13762 . . . . . . . . . . . 12 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘(𝑖 + 1)) ≤ (𝑃‘𝑁))
411232, 229, 318, 320, 410letrd 11141 . . . . . . . . . . 11 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ≤ (𝑃‘𝑁))
41261rexrd 11034 . . . . . . . . . . . . . 14 (𝜑 → (𝑃‘𝑁) ∈ ℝ*)
41371, 412jca 512 . . . . . . . . . . . . 13 (𝜑 → ((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘𝑁) ∈ ℝ*))
414186, 413syl 17 . . . . . . . . . . . 12 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → ((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘𝑁) ∈ ℝ*))
415 elicc1 13132 . . . . . . . . . . . 12 (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘𝑁) ∈ ℝ*) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↔ (𝑡 ∈ ℝ* ∧ (𝑃‘𝑀) ≤ 𝑡 ∧ 𝑡 ≤ (𝑃‘𝑁))))
416414, 415syl 17 . . . . . . . . . . 11 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↔ (𝑡 ∈ ℝ* ∧ (𝑃‘𝑀) ≤ 𝑡 ∧ 𝑡 ≤ (𝑃‘𝑁))))
417188, 317, 411, 416mpbir3and 1341 . . . . . . . . . 10 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)))
418186, 417, 145syl2anc 584 . . . . . . . . 9 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝐴 ∈ ℂ)
419 simpll 764 . . . . . . . . . 10 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝜑)
420234, 321, 202, 136syl3anbrc 1342 . . . . . . . . . 10 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ (𝑀..^𝑁))
421419, 420, 159syl2anc 584 . . . . . . . . 9 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1)
422418, 421itgcl 24957 . . . . . . . 8 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → ∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ∈ ℂ)
423 fveq2 6783 . . . . . . . . . 10 (𝑖 = 𝑘 → (𝑃‘𝑖) = (𝑃‘𝑘))
424 fvoveq1 7307 . . . . . . . . . 10 (𝑖 = 𝑘 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑘 + 1)))
425423, 424oveq12d 7302 . . . . . . . . 9 (𝑖 = 𝑘 → ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) = ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))))
426425itgeq1d 43505 . . . . . . . 8 (𝑖 = 𝑘 → ∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡)
427185, 422, 426fzosump1 15473 . . . . . . 7 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
4284273adant3 1131 . . . . . 6 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
429 oveq1 7291 . . . . . . . 8 (∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 → (∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
430429eqcomd 2745 . . . . . . 7 (∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 → (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = (∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
4314303ad2ant3 1134 . . . . . 6 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = (∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
43270adantr 481 . . . . . . . . 9 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑀) ∈ ℝ)
43345adantr 481 . . . . . . . . . 10 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ)
434174adantl 482 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ ℤ)
435434peano2zd 12438 . . . . . . . . . . 11 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ ℤ)
436435zred 12435 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ ℝ)
437176ltp1d 11914 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 < (𝑘 + 1))
438173, 176, 436, 181, 437lttrd 11145 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < (𝑘 + 1))
439173, 436, 438ltled 11132 . . . . . . . . . . 11 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ≤ (𝑘 + 1))
440200adantl 482 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 < 𝑁)
441 zltp1le 12379 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 < 𝑁 ↔ (𝑘 + 1) ≤ 𝑁))
442174, 5, 441syl2anr 597 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 < 𝑁 ↔ (𝑘 + 1) ≤ 𝑁))
443440, 442mpbid 231 . . . . . . . . . . 11 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ≤ 𝑁)
44491adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
445 elfz1 13253 . . . . . . . . . . . 12 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑘 + 1) ∈ (𝑀...𝑁) ↔ ((𝑘 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁)))
446444, 445syl 17 . . . . . . . . . . 11 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ((𝑘 + 1) ∈ (𝑀...𝑁) ↔ ((𝑘 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁)))
447435, 439, 443, 446mpbir3and 1341 . . . . . . . . . 10 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ (𝑀...𝑁))
448433, 447ffvelrnd 6971 . . . . . . . . 9 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ∈ ℝ)
4499adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ ℝ)
450176, 449, 440ltled 11132 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ≤ 𝑁)
451 elfz1 13253 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)))
452444, 451syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)))
453434, 182, 450, 452mpbir3and 1341 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (𝑀...𝑁))
454433, 453ffvelrnd 6971 . . . . . . . . . . 11 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) ∈ ℝ)
455454rexrd 11034 . . . . . . . . . 10 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) ∈ ℝ*)
45645ad2antrr 723 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑃:(𝑀...𝑁)⟶ℝ)
457456, 206ffvelrnd 6971 . . . . . . . . . . 11 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑃‘𝑖) ∈ ℝ)
45845ad2antrr 723 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
459 elfzelz 13265 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ∈ ℤ)
460459adantl 482 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ ℤ)
461 elfzle1 13268 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑀 ≤ 𝑖)
462461adantl 482 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 ≤ 𝑖)
463460zred 12435 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ ℝ)
4649ad2antrr 723 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑁 ∈ ℝ)
465176adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑘 ∈ ℝ)
466 1red 10985 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 1 ∈ ℝ)
467465, 466resubcld 11412 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑘 − 1) ∈ ℝ)
468 elfzle2 13269 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ≤ (𝑘 − 1))
469468adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ≤ (𝑘 − 1))
470465ltm1d 11916 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑘 − 1) < 𝑘)
471463, 467, 465, 469, 470lelttrd 11142 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 < 𝑘)
472440adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑘 < 𝑁)
473463, 465, 464, 471, 472lttrd 11145 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 < 𝑁)
474463, 464, 473ltled 11132 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ≤ 𝑁)
47591ad2antrr 723 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
476475, 93syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)))
477460, 462, 474, 476mpbir3and 1341 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (𝑀...𝑁))
478458, 477ffvelrnd 6971 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘𝑖) ∈ ℝ)
479460peano2zd 12438 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ∈ ℤ)
48047ad2antrr 723 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 ∈ ℝ)
481463, 466readdcld 11013 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ∈ ℝ)
482463ltp1d 11914 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 < (𝑖 + 1))
483480, 463, 481, 462, 482lelttrd 11142 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 < (𝑖 + 1))
484480, 481, 483ltled 11132 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 ≤ (𝑖 + 1))
485 zltp1le 12379 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑖 < 𝑘 ↔ (𝑖 + 1) ≤ 𝑘))
486459, 434, 485syl2anr 597 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 < 𝑘 ↔ (𝑖 + 1) ≤ 𝑘))
487471, 486mpbid 231 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ≤ 𝑘)
488481, 465, 464, 487, 472lelttrd 11142 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) < 𝑁)
489481, 464, 488ltled 11132 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ≤ 𝑁)
490475, 128syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
491479, 484, 489, 490mpbir3and 1341 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁))
492458, 491ffvelrnd 6971 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
493 simpll 764 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝜑)
494 elfzuz 13261 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ∈ (ℤ≥‘𝑀))
495494adantl 482 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (ℤ≥‘𝑀))
4965ad2antrr 723 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑁 ∈ ℤ)
497495, 496, 473, 136syl3anbrc 1342 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (𝑀..^𝑁))
498493, 497, 138syl2anc 584 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1)))
499478, 492, 498ltled 11132 . . . . . . . . . . 11 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘𝑖) ≤ (𝑃‘(𝑖 + 1)))
500185, 457, 499monoord 13762 . . . . . . . . . 10 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑀) ≤ (𝑃‘𝑘))
5015adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ ℤ)
502 elfzo2 13399 . . . . . . . . . . . . 13 (𝑘 ∈ (𝑀..^𝑁) ↔ (𝑘 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑘 < 𝑁))
503185, 501, 440, 502syl3anbrc 1342 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (𝑀..^𝑁))
504 eleq1 2827 . . . . . . . . . . . . . . 15 (𝑖 = 𝑘 → (𝑖 ∈ (𝑀..^𝑁) ↔ 𝑘 ∈ (𝑀..^𝑁)))
505504anbi2d 629 . . . . . . . . . . . . . 14 (𝑖 = 𝑘 → ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ↔ (𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁))))
506423, 424breq12d 5088 . . . . . . . . . . . . . 14 (𝑖 = 𝑘 → ((𝑃‘𝑖) < (𝑃‘(𝑖 + 1)) ↔ (𝑃‘𝑘) < (𝑃‘(𝑘 + 1))))
507505, 506imbi12d 345 . . . . . . . . . . . . 13 (𝑖 = 𝑘 → (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑃‘𝑘) < (𝑃‘(𝑘 + 1)))))
508507, 138chvarvv 2003 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑃‘𝑘) < (𝑃‘(𝑘 + 1)))
509503, 508syldan 591 . . . . . . . . . . 11 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) < (𝑃‘(𝑘 + 1)))
510454, 448, 509ltled 11132 . . . . . . . . . 10 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) ≤ (𝑃‘(𝑘 + 1)))
51171adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑀) ∈ ℝ*)
512448rexrd 11034 . . . . . . . . . . 11 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ∈ ℝ*)
513 elicc1 13132 . . . . . . . . . . 11 (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ*) → ((𝑃‘𝑘) ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ↔ ((𝑃‘𝑘) ∈ ℝ* ∧ (𝑃‘𝑀) ≤ (𝑃‘𝑘) ∧ (𝑃‘𝑘) ≤ (𝑃‘(𝑘 + 1)))))
514511, 512, 513syl2anc 584 . . . . . . . . . 10 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ((𝑃‘𝑘) ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ↔ ((𝑃‘𝑘) ∈ ℝ* ∧ (𝑃‘𝑀) ≤ (𝑃‘𝑘) ∧ (𝑃‘𝑘) ≤ (𝑃‘(𝑘 + 1)))))
515455, 500, 510, 514mpbir3and 1341 . . . . . . . . 9 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))))
516 simpll 764 . . . . . . . . . 10 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝜑)
517 eliccxr 13176 . . . . . . . . . . . 12 (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) → 𝑡 ∈ ℝ*)
518517adantl 482 . . . . . . . . . . 11 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ℝ*)
51971ad2antrr 723 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑀) ∈ ℝ*)
520512adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ∈ ℝ*)
521 simpr 485 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))))
522 iccgelb 13144 . . . . . . . . . . . 12 (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ* ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑀) ≤ 𝑡)
523519, 520, 521, 522syl3anc 1370 . . . . . . . . . . 11 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑀) ≤ 𝑡)
52470ad2antrr 723 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑀) ∈ ℝ)
525448adantr 481 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ∈ ℝ)
526 eliccre 43050 . . . . . . . . . . . . 13 (((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ℝ)
527524, 525, 521, 526syl3anc 1370 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ℝ)
52861ad2antrr 723 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑁) ∈ ℝ)
529 iccleub 13143 . . . . . . . . . . . . 13 (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ* ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ≤ (𝑃‘(𝑘 + 1)))
530519, 520, 521, 529syl3anc 1370 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ≤ (𝑃‘(𝑘 + 1)))
531 eluz2 12597 . . . . . . . . . . . . . . 15 (𝑁 ∈ (ℤ≥‘(𝑘 + 1)) ↔ ((𝑘 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑘 + 1) ≤ 𝑁))
532435, 501, 443, 531syl3anbrc 1342 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ (ℤ≥‘(𝑘 + 1)))
53345ad2antrr 723 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ)
5341ad2antrr 723 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 ∈ ℤ)
5355ad2antrr 723 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑁 ∈ ℤ)
536 elfzelz 13265 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖 ∈ ℤ)
537536adantl 482 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℤ)
53847ad2antrr 723 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 ∈ ℝ)
539537zred 12435 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℝ)
540176adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 ∈ ℝ)
541181adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 < 𝑘)
542175adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 ∈ ℝ)
543 1red 10985 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 1 ∈ ℝ)
544542, 543readdcld 11013 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑘 + 1) ∈ ℝ)
545536zred 12435 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖 ∈ ℝ)
546545adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℝ)
547542ltp1d 11914 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < (𝑘 + 1))
548 elfzle1 13268 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ ((𝑘 + 1)...𝑁) → (𝑘 + 1) ≤ 𝑖)
549548adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑘 + 1) ≤ 𝑖)
550542, 544, 546, 547, 549ltletrd 11144 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < 𝑖)
551550adantll 711 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < 𝑖)
552538, 540, 539, 541, 551lttrd 11145 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 < 𝑖)
553538, 539, 552ltled 11132 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 ≤ 𝑖)
554 elfzle2 13269 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖 ≤ 𝑁)
555554adantl 482 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ≤ 𝑁)
556534, 535, 537, 553, 555elfzd 13256 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ (𝑀...𝑁))
557533, 556ffvelrnd 6971 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑃‘𝑖) ∈ ℝ)
55845ad2antrr 723 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
5591ad2antrr 723 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℤ)
5605ad2antrr 723 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℤ)
561 elfzelz 13265 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ∈ ℤ)
562561adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℤ)
56347ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℝ)
564562zred 12435 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
565176adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 ∈ ℝ)
566181adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < 𝑘)
567175adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 ∈ ℝ)
568 1red 10985 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
569567, 568readdcld 11013 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑘 + 1) ∈ ℝ)
570561zred 12435 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ∈ ℝ)
571570adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
572567ltp1d 11914 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < (𝑘 + 1))
573 elfzle1 13268 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → (𝑘 + 1) ≤ 𝑖)
574573adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑘 + 1) ≤ 𝑖)
575567, 569, 571, 572, 574ltletrd 11144 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < 𝑖)
576575adantll 711 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < 𝑖)
577563, 565, 564, 566, 576lttrd 11145 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < 𝑖)
578563, 564, 577ltled 11132 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ≤ 𝑖)
579570adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
5809adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℝ)
581 1red 10985 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
582580, 581resubcld 11412 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
583 elfzle2 13269 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ≤ (𝑁 − 1))
584583adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ≤ (𝑁 − 1))
585580ltm1d 11916 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
586579, 582, 580, 584, 585lelttrd 11142 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 < 𝑁)
587579, 580, 586ltled 11132 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ≤ 𝑁)
588587adantlr 712 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ≤ 𝑁)
589559, 560, 562, 578, 588elfzd 13256 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑁))
590558, 589ffvelrnd 6971 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃‘𝑖) ∈ ℝ)
591562peano2zd 12438 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℤ)
592591zred 12435 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ)
593564ltp1d 11914 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 < (𝑖 + 1))
594565, 564, 592, 576, 593lttrd 11145 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < (𝑖 + 1))
595563, 565, 592, 566, 594lttrd 11145 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < (𝑖 + 1))
596563, 592, 595ltled 11132 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ≤ (𝑖 + 1))
597586adantlr 712 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 < 𝑁)
598561, 501, 125syl2anr 597 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
599597, 598mpbid 231 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁)
600559, 560, 591, 596, 599elfzd 13256 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁))
601558, 600ffvelrnd 6971 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
602 simpll 764 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝜑)
603 eluz2 12597 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖))
604559, 562, 578, 603syl3anbrc 1342 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (ℤ≥‘𝑀))
605604, 560, 597, 136syl3anbrc 1342 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀..^𝑁))
606602, 605, 138syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1)))
607590, 601, 606ltled 11132 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃‘𝑖) ≤ (𝑃‘(𝑖 + 1)))
608532, 557, 607monoord 13762 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ≤ (𝑃‘𝑁))
609608adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ≤ (𝑃‘𝑁))
610527, 525, 528, 530, 609letrd 11141 . . . . . . . . . . 11 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ≤ (𝑃‘𝑁))
611413ad2antrr 723 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → ((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘𝑁) ∈ ℝ*))
612611, 415syl 17 . . . . . . . . . . 11 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↔ (𝑡 ∈ ℝ* ∧ (𝑃‘𝑀) ≤ 𝑡 ∧ 𝑡 ≤ (𝑃‘𝑁))))
613518, 523, 610, 612mpbir3and 1341 . . . . . . . . . 10 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)))
614516, 613, 145syl2anc 584 . . . . . . . . 9 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝐴 ∈ ℂ)
615 nfv 1918 . . . . . . . . . 10 Ⅎ𝑡(𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁))
6161adantr 481 . . . . . . . . . 10 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ∈ ℤ)
617 elfzouz 13400 . . . . . . . . . . 11 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 ∈ (ℤ≥‘(𝑀 + 1)))
618617adantl 482 . . . . . . . . . 10 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (ℤ≥‘(𝑀 + 1)))
619 simpll 764 . . . . . . . . . . 11 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝜑)
620 elfzouz 13400 . . . . . . . . . . . . 13 (𝑖 ∈ (𝑀..^𝑘) → 𝑖 ∈ (ℤ≥‘𝑀))
621620adantl 482 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 ∈ (ℤ≥‘𝑀))
6225ad2antrr 723 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑁 ∈ ℤ)
623 elfzoelz 13396 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀..^𝑘) → 𝑖 ∈ ℤ)
624623zred 12435 . . . . . . . . . . . . . 14 (𝑖 ∈ (𝑀..^𝑘) → 𝑖 ∈ ℝ)
625624adantl 482 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 ∈ ℝ)
626176adantr 481 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑘 ∈ ℝ)
6279ad2antrr 723 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑁 ∈ ℝ)
628 elfzolt2 13405 . . . . . . . . . . . . . 14 (𝑖 ∈ (𝑀..^𝑘) → 𝑖 < 𝑘)
629628adantl 482 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 < 𝑘)
630440adantr 481 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑘 < 𝑁)
631625, 626, 627, 629, 630lttrd 11145 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 < 𝑁)
632621, 622, 631, 136syl3anbrc 1342 . . . . . . . . . . 11 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 ∈ (𝑀..^𝑁))
633619, 632, 138syl2anc 584 . . . . . . . . . 10 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1)))
634 simpll 764 . . . . . . . . . . 11 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → 𝜑)
63570ad2antrr 723 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → (𝑃‘𝑀) ∈ ℝ)
63661ad2antrr 723 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → (𝑃‘𝑁) ∈ ℝ)
637454adantr 481 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → (𝑃‘𝑘) ∈ ℝ)
638 simpr 485 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)))
639 eliccre 43050 . . . . . . . . . . . . 13 (((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘𝑘) ∈ ℝ ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → 𝑡 ∈ ℝ)
640635, 637, 638, 639syl3anc 1370 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → 𝑡 ∈ ℝ)
64171ad2antrr 723 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → (𝑃‘𝑀) ∈ ℝ*)
642455adantr 481 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → (𝑃‘𝑘) ∈ ℝ*)
643 iccgelb 13144 . . . . . . . . . . . . 13 (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘𝑘) ∈ ℝ* ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → (𝑃‘𝑀) ≤ 𝑡)
644641, 642, 638, 643syl3anc 1370 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → (𝑃‘𝑀) ≤ 𝑡)
645 iccleub 13143 . . . . . . . . . . . . . 14 (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘𝑘) ∈ ℝ* ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → 𝑡 ≤ (𝑃‘𝑘))
646641, 642, 638, 645syl3anc 1370 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → 𝑡 ≤ (𝑃‘𝑘))
647 elfzouz2 13411 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑁 ∈ (ℤ≥‘𝑘))
648647adantl 482 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ (ℤ≥‘𝑘))
64945ad2antrr 723 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ)
6501ad2antrr 723 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀 ∈ ℤ)
6515ad2antrr 723 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑁 ∈ ℤ)
652 elfzelz 13265 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (𝑘...𝑁) → 𝑖 ∈ ℤ)
653652adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑖 ∈ ℤ)
65447ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀 ∈ ℝ)
655653zred 12435 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑖 ∈ ℝ)
656176adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑘 ∈ ℝ)
657181adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀 < 𝑘)
658 elfzle1 13268 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (𝑘...𝑁) → 𝑘 ≤ 𝑖)
659658adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑘 ≤ 𝑖)
660654, 656, 655, 657, 659ltletrd 11144 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀 < 𝑖)
661654, 655, 660ltled 11132 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀 ≤ 𝑖)
662 elfzle2 13269 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (𝑘...𝑁) → 𝑖 ≤ 𝑁)
663662adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑖 ≤ 𝑁)
664650, 651, 653, 661, 663elfzd 13256 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑖 ∈ (𝑀...𝑁))
665649, 664ffvelrnd 6971 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → (𝑃‘𝑖) ∈ ℝ)
66645ad2antrr 723 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
6671ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 ∈ ℤ)
6685ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑁 ∈ ℤ)
669 elfzelz 13265 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (𝑘...(𝑁 − 1)) → 𝑖 ∈ ℤ)
670669adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ ℤ)
67147ad2antrr 723 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 ∈ ℝ)
672670zred 12435 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ ℝ)
673176adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑘 ∈ ℝ)
674181adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 < 𝑘)
675 elfzle1 13268 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (𝑘...(𝑁 − 1)) → 𝑘 ≤ 𝑖)
676675adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑘 ≤ 𝑖)
677671, 673, 672, 674, 676ltletrd 11144 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 < 𝑖)
678671, 672, 677ltled 11132 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 ≤ 𝑖)
679669zred 12435 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (𝑘...(𝑁 − 1)) → 𝑖 ∈ ℝ)
680679adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ ℝ)
6819adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑁 ∈ ℝ)
682 1red 10985 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 1 ∈ ℝ)
683681, 682resubcld 11412 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
684 elfzle2 13269 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (𝑘...(𝑁 − 1)) → 𝑖 ≤ (𝑁 − 1))
685684adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ≤ (𝑁 − 1))
686681ltm1d 11916 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
687680, 683, 681, 685, 686lelttrd 11142 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 < 𝑁)
688680, 681, 687ltled 11132 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ≤ 𝑁)
689688adantlr 712 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ≤ 𝑁)
690667, 668, 670, 678, 689elfzd 13256 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑁))
691666, 690ffvelrnd 6971 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑃‘𝑖) ∈ ℝ)
692670peano2zd 12438 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ∈ ℤ)
693692zred 12435 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ)
694672ltp1d 11914 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 < (𝑖 + 1))
695671, 672, 693, 678, 694lelttrd 11142 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 < (𝑖 + 1))
696671, 693, 695ltled 11132 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 ≤ (𝑖 + 1))
697669, 5, 125syl2anr 597 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
698687, 697mpbid 231 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁)
699698adantlr 712 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁)
700667, 668, 692, 696, 699elfzd 13256 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁))
701666, 700ffvelrnd 6971 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
702 simpll 764 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝜑)
703667, 670, 678, 603syl3anbrc 1342 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ (ℤ≥‘𝑀))
704687adantlr 712 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 < 𝑁)
705703, 668, 704, 136syl3anbrc 1342 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ (𝑀..^𝑁))
706702, 705, 138syl2anc 584 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1)))
707691, 701, 706ltled 11132 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑃‘𝑖) ≤ (𝑃‘(𝑖 + 1)))
708648, 665, 707monoord 13762 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) ≤ (𝑃‘𝑁))
709708adantr 481 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → (𝑃‘𝑘) ≤ (𝑃‘𝑁))
710640, 637, 636, 646, 709letrd 11141 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → 𝑡 ≤ (𝑃‘𝑁))
711635, 636, 640, 644, 710eliccd 43049 . . . . . . . . . . 11 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)))
712634, 711, 145syl2anc 584 . . . . . . . . . 10 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → 𝐴 ∈ ℂ)
713619, 632, 159syl2anc 584 . . . . . . . . . 10 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1)
714615, 616, 618, 457, 633, 712, 713iblspltprt 43521 . . . . . . . . 9 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1)
715425mpteq1d 5170 . . . . . . . . . . . . 13 (𝑖 = 𝑘 → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) = (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴))
716715eleq1d 2824 . . . . . . . . . . . 12 (𝑖 = 𝑘 → ((𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1))
717505, 716imbi12d 345 . . . . . . . . . . 11 (𝑖 = 𝑘 → (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1) ↔ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1)))
718717, 159chvarvv 2003 . . . . . . . . . 10 ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1)
719503, 718syldan 591 . . . . . . . . 9 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1)
720432, 448, 515, 614, 714, 719itgspliticc 25010 . . . . . . . 8 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ∫((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = (∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
721720eqcomd 2745 . . . . . . 7 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = ∫((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡)
7227213adant3 1131 . . . . . 6 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → (∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = ∫((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡)
723428, 431, 7223eqtrrd 2784 . . . . 5 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → ∫((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
724169, 170, 172, 723syl3anc 1370 . . . 4 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → ∫((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
7257243exp 1118 . . 3 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → ((𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)))
72618, 25, 32, 39, 168, 725fzind2 13514 . 2 (𝑁 ∈ ((𝑀 + 1)...𝑁) → (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑁))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
72711, 726mpcom 38 1 (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑁))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
Colors of variables: wff setvar class
Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107   class class class wbr 5075   ↦ cmpt 5158  ⟶wf 6433  ‘cfv 6437  (class class class)co 7284  ℂcc 10878  ℝcr 10879  1c1 10881   + caddc 10883  ℝ*cxr 11017   < clt 11018   ≤ cle 11019   − cmin 11214  ℤcz 12328  ℤ≥cuz 12591  [,]cicc 13091  ...cfz 13248  ..^cfzo 13391  Σcsu 15406  𝐿1cibl 24790  ∫citg 24791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-inf2 9408  ax-cnex 10936  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957  ax-pre-sup 10958  ax-addf 10959
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rmo 3072  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-int 4881  df-iun 4927  df-disj 5041  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-se 5546  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-isom 6446  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-of 7542  df-ofr 7543  df-om 7722  df-1st 7840  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-1o 8306  df-2o 8307  df-er 8507  df-map 8626  df-pm 8627  df-en 8743  df-dom 8744  df-sdom 8745  df-fin 8746  df-fi 9179  df-sup 9210  df-inf 9211  df-oi 9278  df-dju 9668  df-card 9706  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-div 11642  df-nn 11983  df-2 12045  df-3 12046  df-4 12047  df-n0 12243  df-z 12329  df-uz 12592  df-q 12698  df-rp 12740  df-xneg 12857  df-xadd 12858  df-xmul 12859  df-ioo 13092  df-ico 13094  df-icc 13095  df-fz 13249  df-fzo 13392  df-fl 13521  df-mod 13599  df-seq 13731  df-exp 13792  df-hash 14054  df-cj 14819  df-re 14820  df-im 14821  df-sqrt 14955  df-abs 14956  df-clim 15206  df-sum 15407  df-rest 17142  df-topgen 17163  df-psmet 20598  df-xmet 20599  df-met 20600  df-bl 20601  df-mopn 20602  df-top 22052  df-topon 22069  df-bases 22105  df-cmp 22547  df-ovol 24637  df-vol 24638  df-mbf 24792  df-itg1 24793  df-itg2 24794  df-ibl 24795  df-itg 24796
This theorem is referenced by:  fourierdlem73  43727  fourierdlem81  43735  fourierdlem93  43747
  Copyright terms: Public domain W3C validator