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 46008
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 12700 . . 3 (𝜑 → (𝑀 + 1) ∈ ℤ)
3 itgspltprt.2 . . . 4 (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))
4 eluzelz 12862 . . . 4 (𝑁 ∈ (ℤ≥‘(𝑀 + 1)) → 𝑁 ∈ ℤ)
53, 4syl 17 . . 3 (𝜑 → 𝑁 ∈ ℤ)
6 eluzle 12865 . . . 4 (𝑁 ∈ (ℤ≥‘(𝑀 + 1)) → (𝑀 + 1) ≤ 𝑁)
73, 6syl 17 . . 3 (𝜑 → (𝑀 + 1) ≤ 𝑁)
8 eluzelre 12863 . . . . 5 (𝑁 ∈ (ℤ≥‘(𝑀 + 1)) → 𝑁 ∈ ℝ)
93, 8syl 17 . . . 4 (𝜑 → 𝑁 ∈ ℝ)
109leidd 11803 . . 3 (𝜑 → 𝑁 ≤ 𝑁)
112, 5, 5, 7, 10elfzd 13532 . 2 (𝜑 → 𝑁 ∈ ((𝑀 + 1)...𝑁))
12 fveq2 6876 . . . . . . 7 (𝑗 = (𝑀 + 1) → (𝑃‘𝑗) = (𝑃‘(𝑀 + 1)))
1312oveq2d 7421 . . . . . 6 (𝑗 = (𝑀 + 1) → ((𝑃‘𝑀)[,](𝑃‘𝑗)) = ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))))
1413itgeq1d 45986 . . . . 5 (𝑗 = (𝑀 + 1) → ∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡)
15 oveq2 7413 . . . . . 6 (𝑗 = (𝑀 + 1) → (𝑀..^𝑗) = (𝑀..^(𝑀 + 1)))
1615sumeq1d 15716 . . . . 5 (𝑗 = (𝑀 + 1) → Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
1714, 16eqeq12d 2751 . . . 4 (𝑗 = (𝑀 + 1) → (∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ↔ ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
1817imbi2d 340 . . 3 (𝑗 = (𝑀 + 1) → ((𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ↔ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)))
19 fveq2 6876 . . . . . . 7 (𝑗 = 𝑘 → (𝑃‘𝑗) = (𝑃‘𝑘))
2019oveq2d 7421 . . . . . 6 (𝑗 = 𝑘 → ((𝑃‘𝑀)[,](𝑃‘𝑗)) = ((𝑃‘𝑀)[,](𝑃‘𝑘)))
2120itgeq1d 45986 . . . . 5 (𝑗 = 𝑘 → ∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡)
22 oveq2 7413 . . . . . 6 (𝑗 = 𝑘 → (𝑀..^𝑗) = (𝑀..^𝑘))
2322sumeq1d 15716 . . . . 5 (𝑗 = 𝑘 → Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
2421, 23eqeq12d 2751 . . . 4 (𝑗 = 𝑘 → (∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ↔ ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
2524imbi2d 340 . . 3 (𝑗 = 𝑘 → ((𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ↔ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)))
26 fveq2 6876 . . . . . . 7 (𝑗 = (𝑘 + 1) → (𝑃‘𝑗) = (𝑃‘(𝑘 + 1)))
2726oveq2d 7421 . . . . . 6 (𝑗 = (𝑘 + 1) → ((𝑃‘𝑀)[,](𝑃‘𝑗)) = ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))))
2827itgeq1d 45986 . . . . 5 (𝑗 = (𝑘 + 1) → ∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = ∫((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡)
29 oveq2 7413 . . . . . 6 (𝑗 = (𝑘 + 1) → (𝑀..^𝑗) = (𝑀..^(𝑘 + 1)))
3029sumeq1d 15716 . . . . 5 (𝑗 = (𝑘 + 1) → Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
3128, 30eqeq12d 2751 . . . 4 (𝑗 = (𝑘 + 1) → (∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ↔ ∫((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
3231imbi2d 340 . . 3 (𝑗 = (𝑘 + 1) → ((𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ↔ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)))
33 fveq2 6876 . . . . . . 7 (𝑗 = 𝑁 → (𝑃‘𝑗) = (𝑃‘𝑁))
3433oveq2d 7421 . . . . . 6 (𝑗 = 𝑁 → ((𝑃‘𝑀)[,](𝑃‘𝑗)) = ((𝑃‘𝑀)[,](𝑃‘𝑁)))
3534itgeq1d 45986 . . . . 5 (𝑗 = 𝑁 → ∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = ∫((𝑃‘𝑀)[,](𝑃‘𝑁))𝐴 d𝑡)
36 oveq2 7413 . . . . . 6 (𝑗 = 𝑁 → (𝑀..^𝑗) = (𝑀..^𝑁))
3736sumeq1d 15716 . . . . 5 (𝑗 = 𝑁 → Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
3835, 37eqeq12d 2751 . . . 4 (𝑗 = 𝑁 → (∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ↔ ∫((𝑃‘𝑀)[,](𝑃‘𝑁))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
3938imbi2d 340 . . 3 (𝑗 = 𝑁 → ((𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ↔ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑁))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)))
401adantl 481 . . . . . . . 8 ((𝑁 ∈ (ℤ≥‘(𝑀 + 1)) ∧ 𝜑) → 𝑀 ∈ ℤ)
41 fzval3 13750 . . . . . . . 8 (𝑀 ∈ ℤ → (𝑀...𝑀) = (𝑀..^(𝑀 + 1)))
4240, 41syl 17 . . . . . . 7 ((𝑁 ∈ (ℤ≥‘(𝑀 + 1)) ∧ 𝜑) → (𝑀...𝑀) = (𝑀..^(𝑀 + 1)))
4342eqcomd 2741 . . . . . 6 ((𝑁 ∈ (ℤ≥‘(𝑀 + 1)) ∧ 𝜑) → (𝑀..^(𝑀 + 1)) = (𝑀...𝑀))
4443sumeq1d 15716 . . . . 5 ((𝑁 ∈ (ℤ≥‘(𝑀 + 1)) ∧ 𝜑) → Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀...𝑀)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
45 itgspltprt.3 . . . . . . . . . . . 12 (𝜑 → 𝑃:(𝑀...𝑁)⟶ℝ)
4645adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑃:(𝑀...𝑁)⟶ℝ)
471zred 12697 . . . . . . . . . . . . . . 15 (𝜑 → 𝑀 ∈ ℝ)
48 1red 11236 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ∈ ℝ)
4947, 48readdcld 11264 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑀 + 1) ∈ ℝ)
5047ltp1d 12172 . . . . . . . . . . . . . . . 16 (𝜑 → 𝑀 < (𝑀 + 1))
5147, 49, 9, 50, 7ltletrd 11395 . . . . . . . . . . . . . . 15 (𝜑 → 𝑀 < 𝑁)
5247, 9, 51ltled 11383 . . . . . . . . . . . . . 14 (𝜑 → 𝑀 ≤ 𝑁)
53 eluz 12866 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁))
541, 5, 53syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁))
5552, 54mpbird 257 . . . . . . . . . . . . 13 (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))
56 eluzfz1 13548 . . . . . . . . . . . . 13 (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁))
5755, 56syl 17 . . . . . . . . . . . 12 (𝜑 → 𝑀 ∈ (𝑀...𝑁))
5857adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑀 ∈ (𝑀...𝑁))
5946, 58ffvelcdmd 7075 . . . . . . . . . 10 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘𝑀) ∈ ℝ)
601, 5, 5, 52, 10elfzd 13532 . . . . . . . . . . . 12 (𝜑 → 𝑁 ∈ (𝑀...𝑁))
6145, 60ffvelcdmd 7075 . . . . . . . . . . 11 (𝜑 → (𝑃‘𝑁) ∈ ℝ)
6261adantr 480 . . . . . . . . . 10 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘𝑁) ∈ ℝ)
6347lep1d 12173 . . . . . . . . . . . . . 14 (𝜑 → 𝑀 ≤ (𝑀 + 1))
641, 5, 2, 63, 7elfzd 13532 . . . . . . . . . . . . 13 (𝜑 → (𝑀 + 1) ∈ (𝑀...𝑁))
6545, 64ffvelcdmd 7075 . . . . . . . . . . . 12 (𝜑 → (𝑃‘(𝑀 + 1)) ∈ ℝ)
6665adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘(𝑀 + 1)) ∈ ℝ)
67 simpr 484 . . . . . . . . . . 11 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))))
68 eliccre 45534 . . . . . . . . . . 11 (((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘(𝑀 + 1)) ∈ ℝ ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ∈ ℝ)
6959, 66, 67, 68syl3anc 1373 . . . . . . . . . 10 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ∈ ℝ)
7045, 57ffvelcdmd 7075 . . . . . . . . . . . . 13 (𝜑 → (𝑃‘𝑀) ∈ ℝ)
7170rexrd 11285 . . . . . . . . . . . 12 (𝜑 → (𝑃‘𝑀) ∈ ℝ*)
7271adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘𝑀) ∈ ℝ*)
7366rexrd 11285 . . . . . . . . . . 11 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘(𝑀 + 1)) ∈ ℝ*)
74 iccgelb 13419 . . . . . . . . . . 11 (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘(𝑀 + 1)) ∈ ℝ* ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘𝑀) ≤ 𝑡)
7572, 73, 67, 74syl3anc 1373 . . . . . . . . . 10 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘𝑀) ≤ 𝑡)
76 iccleub 13418 . . . . . . . . . . . 12 (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘(𝑀 + 1)) ∈ ℝ* ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ≤ (𝑃‘(𝑀 + 1)))
7772, 73, 67, 76syl3anc 1373 . . . . . . . . . . 11 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ≤ (𝑃‘(𝑀 + 1)))
7845adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ)
79 elfzelz 13541 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ((𝑀 + 1)...𝑁) → 𝑖 ∈ ℤ)
8079adantl 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑖 ∈ ℤ)
8147adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑀 ∈ ℝ)
8280zred 12697 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑖 ∈ ℝ)
8349adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑀 + 1) ∈ ℝ)
8450adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑀 < (𝑀 + 1))
85 elfzle1 13544 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ((𝑀 + 1)...𝑁) → (𝑀 + 1) ≤ 𝑖)
8685adantl 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑀 + 1) ≤ 𝑖)
8781, 83, 82, 84, 86ltletrd 11395 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑀 < 𝑖)
8881, 82, 87ltled 11383 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑀 ≤ 𝑖)
89 elfzle2 13545 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ((𝑀 + 1)...𝑁) → 𝑖 ≤ 𝑁)
9089adantl 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑖 ≤ 𝑁)
911, 5jca 511 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
9291adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
93 elfz1 13529 . . . . . . . . . . . . . . . 16 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)))
9492, 93syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)))
9580, 88, 90, 94mpbir3and 1343 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑖 ∈ (𝑀...𝑁))
9678, 95ffvelcdmd 7075 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑃‘𝑖) ∈ ℝ)
9745adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
98 elfzelz 13541 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1)) → 𝑖 ∈ ℤ)
9998adantl 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℤ)
10047adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℝ)
10199zred 12697 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
10249adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑀 + 1) ∈ ℝ)
10350adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 < (𝑀 + 1))
104 elfzle1 13544 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1)) → (𝑀 + 1) ≤ 𝑖)
105104adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑀 + 1) ≤ 𝑖)
106100, 102, 101, 103, 105ltletrd 11395 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 < 𝑖)
107100, 101, 106ltled 11383 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 ≤ 𝑖)
1089adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℝ)
109 1red 11236 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
110108, 109resubcld 11665 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
111 elfzle2 13545 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1)) → 𝑖 ≤ (𝑁 − 1))
112111adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ≤ (𝑁 − 1))
113108ltm1d 12174 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
114101, 110, 108, 112, 113lelttrd 11393 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 < 𝑁)
115101, 108, 114ltled 11383 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ≤ 𝑁)
11691adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
117116, 93syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)))
11899, 107, 115, 117mpbir3and 1343 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑁))
11997, 118ffvelcdmd 7075 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑃‘𝑖) ∈ ℝ)
12099peano2zd 12700 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℤ)
121101, 109readdcld 11264 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ)
122100, 101, 109, 106ltadd1dd 11848 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑀 + 1) < (𝑖 + 1))
123100, 102, 121, 103, 122lttrd 11396 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 < (𝑖 + 1))
124100, 121, 123ltled 11383 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 ≤ (𝑖 + 1))
125 zltp1le 12642 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
12698, 5, 125syl2anr 597 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
127114, 126mpbid 232 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁)
128 elfz1 13529 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
129116, 128syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
130120, 124, 127, 129mpbir3and 1343 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁))
13197, 130ffvelcdmd 7075 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
132 eluz 12866 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑖 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑖))
1331, 98, 132syl2an 596 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑖))
134107, 133mpbird 257 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ (ℤ≥‘𝑀))
1355adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℤ)
136 elfzo2 13679 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀..^𝑁) ↔ (𝑖 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑖 < 𝑁))
137134, 135, 114, 136syl3anbrc 1344 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀..^𝑁))
138 itgspltprt.4 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1)))
139137, 138syldan 591 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1)))
140119, 131, 139ltled 11383 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑃‘𝑖) ≤ (𝑃‘(𝑖 + 1)))
1413, 96, 140monoord 14050 . . . . . . . . . . . 12 (𝜑 → (𝑃‘(𝑀 + 1)) ≤ (𝑃‘𝑁))
142141adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘(𝑀 + 1)) ≤ (𝑃‘𝑁))
14369, 66, 62, 77, 142letrd 11392 . . . . . . . . . 10 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ≤ (𝑃‘𝑁))
14459, 62, 69, 75, 143eliccd 45533 . . . . . . . . 9 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)))
145 itgspltprt.5 . . . . . . . . 9 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁))) → 𝐴 ∈ ℂ)
146144, 145syldan 591 . . . . . . . 8 ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝐴 ∈ ℂ)
147 id 22 . . . . . . . . . 10 (𝜑 → 𝜑)
148 fzolb 13682 . . . . . . . . . . 11 (𝑀 ∈ (𝑀..^𝑁) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁))
1491, 5, 51, 148syl3anbrc 1344 . . . . . . . . . 10 (𝜑 → 𝑀 ∈ (𝑀..^𝑁))
150147, 149jca 511 . . . . . . . . 9 (𝜑 → (𝜑 ∧ 𝑀 ∈ (𝑀..^𝑁)))
151 eleq1 2822 . . . . . . . . . . . 12 (𝑖 = 𝑀 → (𝑖 ∈ (𝑀..^𝑁) ↔ 𝑀 ∈ (𝑀..^𝑁)))
152151anbi2d 630 . . . . . . . . . . 11 (𝑖 = 𝑀 → ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ↔ (𝜑 ∧ 𝑀 ∈ (𝑀..^𝑁))))
153 fveq2 6876 . . . . . . . . . . . . . 14 (𝑖 = 𝑀 → (𝑃‘𝑖) = (𝑃‘𝑀))
154 fvoveq1 7428 . . . . . . . . . . . . . 14 (𝑖 = 𝑀 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑀 + 1)))
155153, 154oveq12d 7423 . . . . . . . . . . . . 13 (𝑖 = 𝑀 → ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) = ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))))
156155mpteq1d 5210 . . . . . . . . . . . 12 (𝑖 = 𝑀 → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) = (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴))
157156eleq1d 2819 . . . . . . . . . . 11 (𝑖 = 𝑀 → ((𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿1))
158152, 157imbi12d 344 . . . . . . . . . 10 (𝑖 = 𝑀 → (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1) ↔ ((𝜑 ∧ 𝑀 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿1)))
159 itgspltprt.6 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1)
160158, 159vtoclg 3533 . . . . . . . . 9 (𝑀 ∈ ℤ → ((𝜑 ∧ 𝑀 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿1))
1611, 150, 160sylc 65 . . . . . . . 8 (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿1)
162146, 161itgcl 25737 . . . . . . 7 (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 ∈ ℂ)
163155itgeq1d 45986 . . . . . . . 8 (𝑖 = 𝑀 → ∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡)
164163fsum1 15763 . . . . . . 7 ((𝑀 ∈ ℤ ∧ ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 ∈ ℂ) → Σ𝑖 ∈ (𝑀...𝑀)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡)
1651, 162, 164syl2anc 584 . . . . . 6 (𝜑 → Σ𝑖 ∈ (𝑀...𝑀)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡)
166165adantl 481 . . . . 5 ((𝑁 ∈ (ℤ≥‘(𝑀 + 1)) ∧ 𝜑) → Σ𝑖 ∈ (𝑀...𝑀)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡)
16744, 166eqtr2d 2771 . . . 4 ((𝑁 ∈ (ℤ≥‘(𝑀 + 1)) ∧ 𝜑) → ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
168167ex 412 . . 3 (𝑁 ∈ (ℤ≥‘(𝑀 + 1)) → (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
169 simp3 1138 . . . . 5 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → 𝜑)
170 simp1 1136 . . . . 5 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → 𝑘 ∈ ((𝑀 + 1)..^𝑁))
171 simp2 1137 . . . . . 6 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
172169, 171mpd 15 . . . . 5 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
17347adantr 480 . . . . . . . . . 10 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ∈ ℝ)
174 elfzoelz 13676 . . . . . . . . . . . 12 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 ∈ ℤ)
175174zred 12697 . . . . . . . . . . 11 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 ∈ ℝ)
176175adantl 481 . . . . . . . . . 10 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ ℝ)
17749adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 + 1) ∈ ℝ)
17850adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < (𝑀 + 1))
179 elfzole1 13684 . . . . . . . . . . . 12 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑀 + 1) ≤ 𝑘)
180179adantl 481 . . . . . . . . . . 11 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 + 1) ≤ 𝑘)
181173, 177, 176, 178, 180ltletrd 11395 . . . . . . . . . 10 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < 𝑘)
182173, 176, 181ltled 11383 . . . . . . . . 9 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ≤ 𝑘)
183 eluz 12866 . . . . . . . . . 10 ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑘))
1841, 174, 183syl2an 596 . . . . . . . . 9 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑘))
185182, 184mpbird 257 . . . . . . . 8 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (ℤ≥‘𝑀))
186 simplll 774 . . . . . . . . . 10 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝜑)
187 eliccxr 13452 . . . . . . . . . . . 12 (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) → 𝑡 ∈ ℝ*)
188187adantl 481 . . . . . . . . . . 11 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ℝ*)
189186, 70syl 17 . . . . . . . . . . . 12 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘𝑀) ∈ ℝ)
190186, 45syl 17 . . . . . . . . . . . . 13 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑃:(𝑀...𝑁)⟶ℝ)
191 elfzelz 13541 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀...𝑘) → 𝑖 ∈ ℤ)
192191adantl 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ ℤ)
193 elfzle1 13544 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀...𝑘) → 𝑀 ≤ 𝑖)
194193adantl 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 ≤ 𝑖)
195192zred 12697 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ ℝ)
1969ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑁 ∈ ℝ)
197176adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑘 ∈ ℝ)
198 elfzle2 13545 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (𝑀...𝑘) → 𝑖 ≤ 𝑘)
199198adantl 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ≤ 𝑘)
200 elfzolt2 13685 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 < 𝑁)
201200ad2antlr 727 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑘 < 𝑁)
202195, 197, 196, 199, 201lelttrd 11393 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 < 𝑁)
203195, 196, 202ltled 11383 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ≤ 𝑁)
20491ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
205204, 93syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)))
206192, 194, 203, 205mpbir3and 1343 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ (𝑀...𝑁))
207206adantr 480 . . . . . . . . . . . . 13 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑖 ∈ (𝑀...𝑁))
208190, 207ffvelcdmd 7075 . . . . . . . . . . . 12 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘𝑖) ∈ ℝ)
209192peano2zd 12700 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ∈ ℤ)
21047ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 ∈ ℝ)
211209zred 12697 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ∈ ℝ)
21247adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 ∈ ℝ)
213191zred 12697 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (𝑀...𝑘) → 𝑖 ∈ ℝ)
214213adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ ℝ)
215 1red 11236 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘)) → 1 ∈ ℝ)
216214, 215readdcld 11264 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ∈ ℝ)
217193adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 ≤ 𝑖)
218214ltp1d 12172 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 < (𝑖 + 1))
219212, 214, 216, 217, 218lelttrd 11393 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 < (𝑖 + 1))
220219adantlr 715 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 < (𝑖 + 1))
221210, 211, 220ltled 11383 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 ≤ (𝑖 + 1))
2225, 191anim12ci 614 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ))
223222adantlr 715 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ))
224223, 125syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
225202, 224mpbid 232 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ≤ 𝑁)
226204, 128syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
227209, 221, 225, 226mpbir3and 1343 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ∈ (𝑀...𝑁))
228227adantr 480 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑖 + 1) ∈ (𝑀...𝑁))
229190, 228ffvelcdmd 7075 . . . . . . . . . . . . 13 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
230 simpr 484 . . . . . . . . . . . . 13 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))))
231 eliccre 45534 . . . . . . . . . . . . 13 (((𝑃‘𝑖) ∈ ℝ ∧ (𝑃‘(𝑖 + 1)) ∈ ℝ ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ℝ)
232208, 229, 230, 231syl3anc 1373 . . . . . . . . . . . 12 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ℝ)
233 elfzuz 13537 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...𝑘) → 𝑖 ∈ (ℤ≥‘𝑀))
234233adantl 481 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ (ℤ≥‘𝑀))
23545ad3antrrr 730 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑃:(𝑀...𝑁)⟶ℝ)
236 elfzelz 13541 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑀...𝑖) → 𝑗 ∈ ℤ)
237236adantl 481 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ∈ ℤ)
238 elfzle1 13544 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑀...𝑖) → 𝑀 ≤ 𝑗)
239238adantl 481 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑀 ≤ 𝑗)
240237zred 12697 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ∈ ℝ)
241196adantr 480 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑁 ∈ ℝ)
242195adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑖 ∈ ℝ)
243 elfzle2 13545 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (𝑀...𝑖) → 𝑗 ≤ 𝑖)
244243adantl 481 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ≤ 𝑖)
245202adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑖 < 𝑁)
246240, 242, 241, 244, 245lelttrd 11393 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 < 𝑁)
247240, 241, 246ltled 11383 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ≤ 𝑁)
248204adantr 480 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
249 elfz1 13529 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁)))
250248, 249syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁)))
251237, 239, 247, 250mpbir3and 1343 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ∈ (𝑀...𝑁))
252235, 251ffvelcdmd 7075 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝑃‘𝑗) ∈ ℝ)
25345ad3antrrr 730 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
254 elfzelz 13541 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑗 ∈ ℤ)
255254adantl 481 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ ℤ)
256 elfzle1 13544 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑀 ≤ 𝑗)
257256adantl 481 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 ≤ 𝑗)
258255zred 12697 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ ℝ)
259196adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑁 ∈ ℝ)
260195adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑖 ∈ ℝ)
261 1red 11236 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 1 ∈ ℝ)
262260, 261resubcld 11665 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑖 − 1) ∈ ℝ)
263 elfzle2 13545 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑗 ≤ (𝑖 − 1))
264263adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ≤ (𝑖 − 1))
265260ltm1d 12174 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑖 − 1) < 𝑖)
266258, 262, 260, 264, 265lelttrd 11393 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 < 𝑖)
267202adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑖 < 𝑁)
268258, 260, 259, 266, 267lttrd 11396 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 < 𝑁)
269258, 259, 268ltled 11383 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ≤ 𝑁)
270204adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
271270, 249syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁)))
272255, 257, 269, 271mpbir3and 1343 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ (𝑀...𝑁))
273253, 272ffvelcdmd 7075 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑃‘𝑗) ∈ ℝ)
274255peano2zd 12700 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ∈ ℤ)
275173ad2antrr 726 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 ∈ ℝ)
276258, 261readdcld 11264 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ∈ ℝ)
27747adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 ∈ ℝ)
278254zred 12697 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑗 ∈ ℝ)
279278adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ ℝ)
280 1red 11236 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 1 ∈ ℝ)
281279, 280readdcld 11264 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ∈ ℝ)
282256adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 ≤ 𝑗)
283279ltp1d 12172 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 < (𝑗 + 1))
284277, 279, 281, 282, 283lelttrd 11393 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 < (𝑗 + 1))
285284ad4ant14 752 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 < (𝑗 + 1))
286275, 276, 285ltled 11383 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 ≤ (𝑗 + 1))
287 zltp1le 12642 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑗 < 𝑖 ↔ (𝑗 + 1) ≤ 𝑖))
288254, 192, 287syl2anr 597 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 < 𝑖 ↔ (𝑗 + 1) ≤ 𝑖))
289266, 288mpbid 232 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ≤ 𝑖)
290276, 260, 259, 289, 267lelttrd 11393 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) < 𝑁)
291276, 259, 290ltled 11383 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ≤ 𝑁)
292 elfz1 13529 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑗 + 1) ∈ (𝑀...𝑁) ↔ ((𝑗 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑗 + 1) ∧ (𝑗 + 1) ≤ 𝑁)))
293270, 292syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → ((𝑗 + 1) ∈ (𝑀...𝑁) ↔ ((𝑗 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑗 + 1) ∧ (𝑗 + 1) ≤ 𝑁)))
294274, 286, 291, 293mpbir3and 1343 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ∈ (𝑀...𝑁))
295253, 294ffvelcdmd 7075 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑃‘(𝑗 + 1)) ∈ ℝ)
296 simplll 774 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝜑)
297 elfzuz 13537 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑗 ∈ (ℤ≥‘𝑀))
298297adantl 481 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ (ℤ≥‘𝑀))
299296, 5syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑁 ∈ ℤ)
300 elfzo2 13679 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑀..^𝑁) ↔ (𝑗 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑗 < 𝑁))
301298, 299, 268, 300syl3anbrc 1344 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ (𝑀..^𝑁))
302 eleq1 2822 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → (𝑖 ∈ (𝑀..^𝑁) ↔ 𝑗 ∈ (𝑀..^𝑁)))
303302anbi2d 630 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ↔ (𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁))))
304 fveq2 6876 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → (𝑃‘𝑖) = (𝑃‘𝑗))
305 fvoveq1 7428 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑗 + 1)))
306304, 305breq12d 5132 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → ((𝑃‘𝑖) < (𝑃‘(𝑖 + 1)) ↔ (𝑃‘𝑗) < (𝑃‘(𝑗 + 1))))
307303, 306imbi12d 344 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑗 → (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑃‘𝑗) < (𝑃‘(𝑗 + 1)))))
308307, 138chvarvv 1998 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑃‘𝑗) < (𝑃‘(𝑗 + 1)))
309296, 301, 308syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑃‘𝑗) < (𝑃‘(𝑗 + 1)))
310273, 295, 309ltled 11383 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑃‘𝑗) ≤ (𝑃‘(𝑗 + 1)))
311234, 252, 310monoord 14050 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑃‘𝑀) ≤ (𝑃‘𝑖))
312311adantr 480 . . . . . . . . . . . 12 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘𝑀) ≤ (𝑃‘𝑖))
313208rexrd 11285 . . . . . . . . . . . . 13 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘𝑖) ∈ ℝ*)
314229rexrd 11285 . . . . . . . . . . . . 13 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘(𝑖 + 1)) ∈ ℝ*)
315 iccgelb 13419 . . . . . . . . . . . . 13 (((𝑃‘𝑖) ∈ ℝ* ∧ (𝑃‘(𝑖 + 1)) ∈ ℝ* ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘𝑖) ≤ 𝑡)
316313, 314, 230, 315syl3anc 1373 . . . . . . . . . . . 12 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘𝑖) ≤ 𝑡)
317189, 208, 232, 312, 316letrd 11392 . . . . . . . . . . 11 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘𝑀) ≤ 𝑡)
318186, 61syl 17 . . . . . . . . . . . 12 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘𝑁) ∈ ℝ)
319 iccleub 13418 . . . . . . . . . . . . 13 (((𝑃‘𝑖) ∈ ℝ* ∧ (𝑃‘(𝑖 + 1)) ∈ ℝ* ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ≤ (𝑃‘(𝑖 + 1)))
320313, 314, 230, 319syl3anc 1373 . . . . . . . . . . . 12 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ≤ (𝑃‘(𝑖 + 1)))
3215ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑁 ∈ ℤ)
322 eluz 12866 . . . . . . . . . . . . . . . 16 (((𝑖 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘(𝑖 + 1)) ↔ (𝑖 + 1) ≤ 𝑁))
323209, 321, 322syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑁 ∈ (ℤ≥‘(𝑖 + 1)) ↔ (𝑖 + 1) ≤ 𝑁))
324225, 323mpbird 257 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑁 ∈ (ℤ≥‘(𝑖 + 1)))
325324adantr 480 . . . . . . . . . . . . 13 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑁 ∈ (ℤ≥‘(𝑖 + 1)))
32645ad3antrrr 730 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ)
327 elfzelz 13541 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ((𝑖 + 1)...𝑁) → 𝑗 ∈ ℤ)
328327adantl 481 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑗 ∈ ℤ)
329 elfzel1 13540 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (𝑀...𝑘) → 𝑀 ∈ ℤ)
330329zred 12697 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (𝑀...𝑘) → 𝑀 ∈ ℝ)
331330adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀 ∈ ℝ)
332327zred 12697 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ((𝑖 + 1)...𝑁) → 𝑗 ∈ ℝ)
333332adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑗 ∈ ℝ)
334213adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑖 ∈ ℝ)
335 1red 11236 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 1 ∈ ℝ)
336334, 335readdcld 11264 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑖 + 1) ∈ ℝ)
337193adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀 ≤ 𝑖)
338334ltp1d 12172 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑖 < (𝑖 + 1))
339331, 334, 336, 337, 338lelttrd 11393 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀 < (𝑖 + 1))
340 elfzle1 13544 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ((𝑖 + 1)...𝑁) → (𝑖 + 1) ≤ 𝑗)
341340adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑖 + 1) ≤ 𝑗)
342331, 336, 333, 339, 341ltletrd 11395 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀 < 𝑗)
343331, 333, 342ltled 11383 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀 ≤ 𝑗)
344343adantll 714 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀 ≤ 𝑗)
345 elfzle2 13545 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ ((𝑖 + 1)...𝑁) → 𝑗 ≤ 𝑁)
346345adantl 481 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑗 ≤ 𝑁)
347204adantr 480 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
348347, 249syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁)))
349328, 344, 346, 348mpbir3and 1343 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑗 ∈ (𝑀...𝑁))
350326, 349ffvelcdmd 7075 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑃‘𝑗) ∈ ℝ)
351350adantlr 715 . . . . . . . . . . . . 13 (((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑃‘𝑗) ∈ ℝ)
352 simplll 774 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝜑)
353 simplr 768 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑘))
354 simpr 484 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1)))
355453ad2ant1 1133 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
356 elfzelz 13541 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1)) → 𝑗 ∈ ℤ)
3573563ad2ant3 1135 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ℤ)
358473ad2ant1 1133 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℝ)
359357zred 12697 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ℝ)
3602163adant3 1132 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ)
3612193adant3 1132 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 < (𝑖 + 1))
362 elfzle1 13544 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1)) → (𝑖 + 1) ≤ 𝑗)
3633623ad2ant3 1135 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑗)
364358, 360, 359, 361, 363ltletrd 11395 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 < 𝑗)
365358, 359, 364ltled 11383 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 ≤ 𝑗)
366356adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ℤ)
367366zred 12697 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ℝ)
3689adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℝ)
369 1red 11236 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
370368, 369resubcld 11665 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
371 elfzle2 13545 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1)) → 𝑗 ≤ (𝑁 − 1))
372371adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ≤ (𝑁 − 1))
373368ltm1d 12174 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
374367, 370, 368, 372, 373lelttrd 11393 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 < 𝑁)
375367, 368, 374ltled 11383 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ≤ 𝑁)
3763753adant2 1131 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ≤ 𝑁)
377913ad2ant1 1133 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
378377, 249syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁)))
379357, 365, 376, 378mpbir3and 1343 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ (𝑀...𝑁))
380355, 379ffvelcdmd 7075 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃‘𝑗) ∈ ℝ)
381357peano2zd 12700 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ∈ ℤ)
382381zred 12697 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ∈ ℝ)
3832133ad2ant2 1134 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
384 1red 11236 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
3852183adant3 1132 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖 < (𝑖 + 1))
386383, 360, 359, 385, 363ltletrd 11395 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖 < 𝑗)
387383, 359, 386ltled 11383 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖 ≤ 𝑗)
388383, 359, 384, 387leadd1dd 11851 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ (𝑗 + 1))
389358, 360, 382, 361, 388ltletrd 11395 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 < (𝑗 + 1))
390358, 382, 389ltled 11383 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 ≤ (𝑗 + 1))
391 zltp1le 12642 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 < 𝑁 ↔ (𝑗 + 1) ≤ 𝑁))
392356, 5, 391syl2anr 597 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 < 𝑁 ↔ (𝑗 + 1) ≤ 𝑁))
393374, 392mpbid 232 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ≤ 𝑁)
3943933adant2 1131 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ≤ 𝑁)
395377, 292syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → ((𝑗 + 1) ∈ (𝑀...𝑁) ↔ ((𝑗 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑗 + 1) ∧ (𝑗 + 1) ≤ 𝑁)))
396381, 390, 394, 395mpbir3and 1343 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ∈ (𝑀...𝑁))
397355, 396ffvelcdmd 7075 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃‘(𝑗 + 1)) ∈ ℝ)
398 simp1 1136 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝜑)
39913ad2ant1 1133 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℤ)
400 eluz 12866 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑗 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑗))
401399, 357, 400syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑗))
402365, 401mpbird 257 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ (ℤ≥‘𝑀))
40353ad2ant1 1133 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℤ)
4043743adant2 1131 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 < 𝑁)
405402, 403, 404, 300syl3anbrc 1344 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ (𝑀..^𝑁))
406398, 405, 308syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃‘𝑗) < (𝑃‘(𝑗 + 1)))
407380, 397, 406ltled 11383 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃‘𝑗) ≤ (𝑃‘(𝑗 + 1)))
408352, 353, 354, 407syl3anc 1373 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃‘𝑗) ≤ (𝑃‘(𝑗 + 1)))
409408adantlr 715 . . . . . . . . . . . . 13 (((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃‘𝑗) ≤ (𝑃‘(𝑗 + 1)))
410325, 351, 409monoord 14050 . . . . . . . . . . . 12 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘(𝑖 + 1)) ≤ (𝑃‘𝑁))
411232, 229, 318, 320, 410letrd 11392 . . . . . . . . . . 11 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ≤ (𝑃‘𝑁))
41261rexrd 11285 . . . . . . . . . . . . . 14 (𝜑 → (𝑃‘𝑁) ∈ ℝ*)
41371, 412jca 511 . . . . . . . . . . . . 13 (𝜑 → ((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘𝑁) ∈ ℝ*))
414186, 413syl 17 . . . . . . . . . . . 12 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → ((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘𝑁) ∈ ℝ*))
415 elicc1 13406 . . . . . . . . . . . 12 (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘𝑁) ∈ ℝ*) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↔ (𝑡 ∈ ℝ* ∧ (𝑃‘𝑀) ≤ 𝑡 ∧ 𝑡 ≤ (𝑃‘𝑁))))
416414, 415syl 17 . . . . . . . . . . 11 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↔ (𝑡 ∈ ℝ* ∧ (𝑃‘𝑀) ≤ 𝑡 ∧ 𝑡 ≤ (𝑃‘𝑁))))
417188, 317, 411, 416mpbir3and 1343 . . . . . . . . . 10 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)))
418186, 417, 145syl2anc 584 . . . . . . . . 9 ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝐴 ∈ ℂ)
419 simpll 766 . . . . . . . . . 10 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝜑)
420234, 321, 202, 136syl3anbrc 1344 . . . . . . . . . 10 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ (𝑀..^𝑁))
421419, 420, 159syl2anc 584 . . . . . . . . 9 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1)
422418, 421itgcl 25737 . . . . . . . 8 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → ∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ∈ ℂ)
423 fveq2 6876 . . . . . . . . . 10 (𝑖 = 𝑘 → (𝑃‘𝑖) = (𝑃‘𝑘))
424 fvoveq1 7428 . . . . . . . . . 10 (𝑖 = 𝑘 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑘 + 1)))
425423, 424oveq12d 7423 . . . . . . . . 9 (𝑖 = 𝑘 → ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) = ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))))
426425itgeq1d 45986 . . . . . . . 8 (𝑖 = 𝑘 → ∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡)
427185, 422, 426fzosump1 15768 . . . . . . 7 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
4284273adant3 1132 . . . . . 6 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
429 oveq1 7412 . . . . . . . 8 (∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 → (∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
430429eqcomd 2741 . . . . . . 7 (∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 → (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = (∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
4314303ad2ant3 1135 . . . . . 6 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = (∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
43270adantr 480 . . . . . . . . 9 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑀) ∈ ℝ)
43345adantr 480 . . . . . . . . . 10 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ)
434174adantl 481 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ ℤ)
435434peano2zd 12700 . . . . . . . . . . 11 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ ℤ)
436435zred 12697 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ ℝ)
437176ltp1d 12172 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 < (𝑘 + 1))
438173, 176, 436, 181, 437lttrd 11396 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < (𝑘 + 1))
439173, 436, 438ltled 11383 . . . . . . . . . . 11 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ≤ (𝑘 + 1))
440200adantl 481 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 < 𝑁)
441 zltp1le 12642 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 < 𝑁 ↔ (𝑘 + 1) ≤ 𝑁))
442174, 5, 441syl2anr 597 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 < 𝑁 ↔ (𝑘 + 1) ≤ 𝑁))
443440, 442mpbid 232 . . . . . . . . . . 11 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ≤ 𝑁)
44491adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
445 elfz1 13529 . . . . . . . . . . . 12 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑘 + 1) ∈ (𝑀...𝑁) ↔ ((𝑘 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁)))
446444, 445syl 17 . . . . . . . . . . 11 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ((𝑘 + 1) ∈ (𝑀...𝑁) ↔ ((𝑘 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁)))
447435, 439, 443, 446mpbir3and 1343 . . . . . . . . . 10 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ (𝑀...𝑁))
448433, 447ffvelcdmd 7075 . . . . . . . . 9 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ∈ ℝ)
4499adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ ℝ)
450176, 449, 440ltled 11383 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ≤ 𝑁)
451 elfz1 13529 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)))
452444, 451syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)))
453434, 182, 450, 452mpbir3and 1343 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (𝑀...𝑁))
454433, 453ffvelcdmd 7075 . . . . . . . . . . 11 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) ∈ ℝ)
455454rexrd 11285 . . . . . . . . . 10 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) ∈ ℝ*)
45645ad2antrr 726 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑃:(𝑀...𝑁)⟶ℝ)
457456, 206ffvelcdmd 7075 . . . . . . . . . . 11 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑃‘𝑖) ∈ ℝ)
45845ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
459 elfzelz 13541 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ∈ ℤ)
460459adantl 481 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ ℤ)
461 elfzle1 13544 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑀 ≤ 𝑖)
462461adantl 481 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 ≤ 𝑖)
463460zred 12697 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ ℝ)
4649ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑁 ∈ ℝ)
465176adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑘 ∈ ℝ)
466 1red 11236 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 1 ∈ ℝ)
467465, 466resubcld 11665 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑘 − 1) ∈ ℝ)
468 elfzle2 13545 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ≤ (𝑘 − 1))
469468adantl 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ≤ (𝑘 − 1))
470465ltm1d 12174 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑘 − 1) < 𝑘)
471463, 467, 465, 469, 470lelttrd 11393 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 < 𝑘)
472440adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑘 < 𝑁)
473463, 465, 464, 471, 472lttrd 11396 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 < 𝑁)
474463, 464, 473ltled 11383 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ≤ 𝑁)
47591ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
476475, 93syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)))
477460, 462, 474, 476mpbir3and 1343 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (𝑀...𝑁))
478458, 477ffvelcdmd 7075 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘𝑖) ∈ ℝ)
479460peano2zd 12700 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ∈ ℤ)
48047ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 ∈ ℝ)
481463, 466readdcld 11264 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ∈ ℝ)
482463ltp1d 12172 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 < (𝑖 + 1))
483480, 463, 481, 462, 482lelttrd 11393 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 < (𝑖 + 1))
484480, 481, 483ltled 11383 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 ≤ (𝑖 + 1))
485 zltp1le 12642 . . . . . . . . . . . . . . . . . 18 ((𝑖 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑖 < 𝑘 ↔ (𝑖 + 1) ≤ 𝑘))
486459, 434, 485syl2anr 597 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 < 𝑘 ↔ (𝑖 + 1) ≤ 𝑘))
487471, 486mpbid 232 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ≤ 𝑘)
488481, 465, 464, 487, 472lelttrd 11393 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) < 𝑁)
489481, 464, 488ltled 11383 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ≤ 𝑁)
490475, 128syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
491479, 484, 489, 490mpbir3and 1343 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁))
492458, 491ffvelcdmd 7075 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
493 simpll 766 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝜑)
494 elfzuz 13537 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ∈ (ℤ≥‘𝑀))
495494adantl 481 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (ℤ≥‘𝑀))
4965ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑁 ∈ ℤ)
497495, 496, 473, 136syl3anbrc 1344 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (𝑀..^𝑁))
498493, 497, 138syl2anc 584 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1)))
499478, 492, 498ltled 11383 . . . . . . . . . . 11 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘𝑖) ≤ (𝑃‘(𝑖 + 1)))
500185, 457, 499monoord 14050 . . . . . . . . . 10 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑀) ≤ (𝑃‘𝑘))
5015adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ ℤ)
502 elfzo2 13679 . . . . . . . . . . . . 13 (𝑘 ∈ (𝑀..^𝑁) ↔ (𝑘 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑘 < 𝑁))
503185, 501, 440, 502syl3anbrc 1344 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (𝑀..^𝑁))
504 eleq1 2822 . . . . . . . . . . . . . . 15 (𝑖 = 𝑘 → (𝑖 ∈ (𝑀..^𝑁) ↔ 𝑘 ∈ (𝑀..^𝑁)))
505504anbi2d 630 . . . . . . . . . . . . . 14 (𝑖 = 𝑘 → ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ↔ (𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁))))
506423, 424breq12d 5132 . . . . . . . . . . . . . 14 (𝑖 = 𝑘 → ((𝑃‘𝑖) < (𝑃‘(𝑖 + 1)) ↔ (𝑃‘𝑘) < (𝑃‘(𝑘 + 1))))
507505, 506imbi12d 344 . . . . . . . . . . . . 13 (𝑖 = 𝑘 → (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑃‘𝑘) < (𝑃‘(𝑘 + 1)))))
508507, 138chvarvv 1998 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑃‘𝑘) < (𝑃‘(𝑘 + 1)))
509503, 508syldan 591 . . . . . . . . . . 11 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) < (𝑃‘(𝑘 + 1)))
510454, 448, 509ltled 11383 . . . . . . . . . 10 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) ≤ (𝑃‘(𝑘 + 1)))
51171adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑀) ∈ ℝ*)
512448rexrd 11285 . . . . . . . . . . 11 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ∈ ℝ*)
513 elicc1 13406 . . . . . . . . . . 11 (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ*) → ((𝑃‘𝑘) ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ↔ ((𝑃‘𝑘) ∈ ℝ* ∧ (𝑃‘𝑀) ≤ (𝑃‘𝑘) ∧ (𝑃‘𝑘) ≤ (𝑃‘(𝑘 + 1)))))
514511, 512, 513syl2anc 584 . . . . . . . . . 10 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ((𝑃‘𝑘) ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ↔ ((𝑃‘𝑘) ∈ ℝ* ∧ (𝑃‘𝑀) ≤ (𝑃‘𝑘) ∧ (𝑃‘𝑘) ≤ (𝑃‘(𝑘 + 1)))))
515455, 500, 510, 514mpbir3and 1343 . . . . . . . . 9 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))))
516 simpll 766 . . . . . . . . . 10 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝜑)
517 eliccxr 13452 . . . . . . . . . . . 12 (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) → 𝑡 ∈ ℝ*)
518517adantl 481 . . . . . . . . . . 11 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ℝ*)
51971ad2antrr 726 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑀) ∈ ℝ*)
520512adantr 480 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ∈ ℝ*)
521 simpr 484 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))))
522 iccgelb 13419 . . . . . . . . . . . 12 (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ* ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑀) ≤ 𝑡)
523519, 520, 521, 522syl3anc 1373 . . . . . . . . . . 11 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑀) ≤ 𝑡)
52470ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑀) ∈ ℝ)
525448adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ∈ ℝ)
526 eliccre 45534 . . . . . . . . . . . . 13 (((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ℝ)
527524, 525, 521, 526syl3anc 1373 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ℝ)
52861ad2antrr 726 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑁) ∈ ℝ)
529 iccleub 13418 . . . . . . . . . . . . 13 (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ* ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ≤ (𝑃‘(𝑘 + 1)))
530519, 520, 521, 529syl3anc 1373 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ≤ (𝑃‘(𝑘 + 1)))
531 eluz2 12858 . . . . . . . . . . . . . . 15 (𝑁 ∈ (ℤ≥‘(𝑘 + 1)) ↔ ((𝑘 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑘 + 1) ≤ 𝑁))
532435, 501, 443, 531syl3anbrc 1344 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ (ℤ≥‘(𝑘 + 1)))
53345ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ)
5341ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 ∈ ℤ)
5355ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑁 ∈ ℤ)
536 elfzelz 13541 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖 ∈ ℤ)
537536adantl 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℤ)
53847ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 ∈ ℝ)
539537zred 12697 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℝ)
540176adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 ∈ ℝ)
541181adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 < 𝑘)
542175adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 ∈ ℝ)
543 1red 11236 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 1 ∈ ℝ)
544542, 543readdcld 11264 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑘 + 1) ∈ ℝ)
545536zred 12697 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖 ∈ ℝ)
546545adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℝ)
547542ltp1d 12172 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < (𝑘 + 1))
548 elfzle1 13544 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ ((𝑘 + 1)...𝑁) → (𝑘 + 1) ≤ 𝑖)
549548adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑘 + 1) ≤ 𝑖)
550542, 544, 546, 547, 549ltletrd 11395 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < 𝑖)
551550adantll 714 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < 𝑖)
552538, 540, 539, 541, 551lttrd 11396 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 < 𝑖)
553538, 539, 552ltled 11383 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 ≤ 𝑖)
554 elfzle2 13545 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖 ≤ 𝑁)
555554adantl 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ≤ 𝑁)
556534, 535, 537, 553, 555elfzd 13532 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ (𝑀...𝑁))
557533, 556ffvelcdmd 7075 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑃‘𝑖) ∈ ℝ)
55845ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
5591ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℤ)
5605ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℤ)
561 elfzelz 13541 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ∈ ℤ)
562561adantl 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℤ)
56347ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℝ)
564562zred 12697 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
565176adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 ∈ ℝ)
566181adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < 𝑘)
567175adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 ∈ ℝ)
568 1red 11236 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
569567, 568readdcld 11264 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑘 + 1) ∈ ℝ)
570561zred 12697 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ∈ ℝ)
571570adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
572567ltp1d 12172 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < (𝑘 + 1))
573 elfzle1 13544 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → (𝑘 + 1) ≤ 𝑖)
574573adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑘 + 1) ≤ 𝑖)
575567, 569, 571, 572, 574ltletrd 11395 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < 𝑖)
576575adantll 714 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < 𝑖)
577563, 565, 564, 566, 576lttrd 11396 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < 𝑖)
578563, 564, 577ltled 11383 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ≤ 𝑖)
579570adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
5809adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℝ)
581 1red 11236 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
582580, 581resubcld 11665 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
583 elfzle2 13545 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ≤ (𝑁 − 1))
584583adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ≤ (𝑁 − 1))
585580ltm1d 12174 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
586579, 582, 580, 584, 585lelttrd 11393 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 < 𝑁)
587579, 580, 586ltled 11383 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ≤ 𝑁)
588587adantlr 715 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ≤ 𝑁)
589559, 560, 562, 578, 588elfzd 13532 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑁))
590558, 589ffvelcdmd 7075 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃‘𝑖) ∈ ℝ)
591562peano2zd 12700 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℤ)
592591zred 12697 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ)
593564ltp1d 12172 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 < (𝑖 + 1))
594565, 564, 592, 576, 593lttrd 11396 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < (𝑖 + 1))
595563, 565, 592, 566, 594lttrd 11396 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < (𝑖 + 1))
596563, 592, 595ltled 11383 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ≤ (𝑖 + 1))
597586adantlr 715 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 < 𝑁)
598561, 501, 125syl2anr 597 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
599597, 598mpbid 232 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁)
600559, 560, 591, 596, 599elfzd 13532 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁))
601558, 600ffvelcdmd 7075 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
602 simpll 766 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝜑)
603 eluz2 12858 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖))
604559, 562, 578, 603syl3anbrc 1344 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (ℤ≥‘𝑀))
605604, 560, 597, 136syl3anbrc 1344 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀..^𝑁))
606602, 605, 138syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1)))
607590, 601, 606ltled 11383 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃‘𝑖) ≤ (𝑃‘(𝑖 + 1)))
608532, 557, 607monoord 14050 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ≤ (𝑃‘𝑁))
609608adantr 480 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ≤ (𝑃‘𝑁))
610527, 525, 528, 530, 609letrd 11392 . . . . . . . . . . 11 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ≤ (𝑃‘𝑁))
611413ad2antrr 726 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → ((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘𝑁) ∈ ℝ*))
612611, 415syl 17 . . . . . . . . . . 11 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↔ (𝑡 ∈ ℝ* ∧ (𝑃‘𝑀) ≤ 𝑡 ∧ 𝑡 ≤ (𝑃‘𝑁))))
613518, 523, 610, 612mpbir3and 1343 . . . . . . . . . 10 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)))
614516, 613, 145syl2anc 584 . . . . . . . . 9 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝐴 ∈ ℂ)
615 nfv 1914 . . . . . . . . . 10 Ⅎ𝑡(𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁))
6161adantr 480 . . . . . . . . . 10 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ∈ ℤ)
617 elfzouz 13680 . . . . . . . . . . 11 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 ∈ (ℤ≥‘(𝑀 + 1)))
618617adantl 481 . . . . . . . . . 10 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (ℤ≥‘(𝑀 + 1)))
619 simpll 766 . . . . . . . . . . 11 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝜑)
620 elfzouz 13680 . . . . . . . . . . . . 13 (𝑖 ∈ (𝑀..^𝑘) → 𝑖 ∈ (ℤ≥‘𝑀))
621620adantl 481 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 ∈ (ℤ≥‘𝑀))
6225ad2antrr 726 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑁 ∈ ℤ)
623 elfzoelz 13676 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀..^𝑘) → 𝑖 ∈ ℤ)
624623zred 12697 . . . . . . . . . . . . . 14 (𝑖 ∈ (𝑀..^𝑘) → 𝑖 ∈ ℝ)
625624adantl 481 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 ∈ ℝ)
626176adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑘 ∈ ℝ)
6279ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑁 ∈ ℝ)
628 elfzolt2 13685 . . . . . . . . . . . . . 14 (𝑖 ∈ (𝑀..^𝑘) → 𝑖 < 𝑘)
629628adantl 481 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 < 𝑘)
630440adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑘 < 𝑁)
631625, 626, 627, 629, 630lttrd 11396 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 < 𝑁)
632621, 622, 631, 136syl3anbrc 1344 . . . . . . . . . . 11 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 ∈ (𝑀..^𝑁))
633619, 632, 138syl2anc 584 . . . . . . . . . 10 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1)))
634 simpll 766 . . . . . . . . . . 11 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → 𝜑)
63570ad2antrr 726 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → (𝑃‘𝑀) ∈ ℝ)
63661ad2antrr 726 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → (𝑃‘𝑁) ∈ ℝ)
637454adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → (𝑃‘𝑘) ∈ ℝ)
638 simpr 484 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)))
639 eliccre 45534 . . . . . . . . . . . . 13 (((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘𝑘) ∈ ℝ ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → 𝑡 ∈ ℝ)
640635, 637, 638, 639syl3anc 1373 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → 𝑡 ∈ ℝ)
64171ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → (𝑃‘𝑀) ∈ ℝ*)
642455adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → (𝑃‘𝑘) ∈ ℝ*)
643 iccgelb 13419 . . . . . . . . . . . . 13 (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘𝑘) ∈ ℝ* ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → (𝑃‘𝑀) ≤ 𝑡)
644641, 642, 638, 643syl3anc 1373 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → (𝑃‘𝑀) ≤ 𝑡)
645 iccleub 13418 . . . . . . . . . . . . . 14 (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘𝑘) ∈ ℝ* ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → 𝑡 ≤ (𝑃‘𝑘))
646641, 642, 638, 645syl3anc 1373 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → 𝑡 ≤ (𝑃‘𝑘))
647 elfzouz2 13691 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑁 ∈ (ℤ≥‘𝑘))
648647adantl 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ (ℤ≥‘𝑘))
64945ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ)
6501ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀 ∈ ℤ)
6515ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑁 ∈ ℤ)
652 elfzelz 13541 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (𝑘...𝑁) → 𝑖 ∈ ℤ)
653652adantl 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑖 ∈ ℤ)
65447ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀 ∈ ℝ)
655653zred 12697 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑖 ∈ ℝ)
656176adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑘 ∈ ℝ)
657181adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀 < 𝑘)
658 elfzle1 13544 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (𝑘...𝑁) → 𝑘 ≤ 𝑖)
659658adantl 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑘 ≤ 𝑖)
660654, 656, 655, 657, 659ltletrd 11395 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀 < 𝑖)
661654, 655, 660ltled 11383 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀 ≤ 𝑖)
662 elfzle2 13545 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (𝑘...𝑁) → 𝑖 ≤ 𝑁)
663662adantl 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑖 ≤ 𝑁)
664650, 651, 653, 661, 663elfzd 13532 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑖 ∈ (𝑀...𝑁))
665649, 664ffvelcdmd 7075 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → (𝑃‘𝑖) ∈ ℝ)
66645ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ)
6671ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 ∈ ℤ)
6685ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑁 ∈ ℤ)
669 elfzelz 13541 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (𝑘...(𝑁 − 1)) → 𝑖 ∈ ℤ)
670669adantl 481 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ ℤ)
67147ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 ∈ ℝ)
672670zred 12697 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ ℝ)
673176adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑘 ∈ ℝ)
674181adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 < 𝑘)
675 elfzle1 13544 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (𝑘...(𝑁 − 1)) → 𝑘 ≤ 𝑖)
676675adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑘 ≤ 𝑖)
677671, 673, 672, 674, 676ltletrd 11395 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 < 𝑖)
678671, 672, 677ltled 11383 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 ≤ 𝑖)
679669zred 12697 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (𝑘...(𝑁 − 1)) → 𝑖 ∈ ℝ)
680679adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ ℝ)
6819adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑁 ∈ ℝ)
682 1red 11236 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 1 ∈ ℝ)
683681, 682resubcld 11665 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
684 elfzle2 13545 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (𝑘...(𝑁 − 1)) → 𝑖 ≤ (𝑁 − 1))
685684adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ≤ (𝑁 − 1))
686681ltm1d 12174 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
687680, 683, 681, 685, 686lelttrd 11393 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 < 𝑁)
688680, 681, 687ltled 11383 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ≤ 𝑁)
689688adantlr 715 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ≤ 𝑁)
690667, 668, 670, 678, 689elfzd 13532 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑁))
691666, 690ffvelcdmd 7075 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑃‘𝑖) ∈ ℝ)
692670peano2zd 12700 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ∈ ℤ)
693692zred 12697 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ)
694672ltp1d 12172 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 < (𝑖 + 1))
695671, 672, 693, 678, 694lelttrd 11393 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 < (𝑖 + 1))
696671, 693, 695ltled 11383 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 ≤ (𝑖 + 1))
697669, 5, 125syl2anr 597 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
698687, 697mpbid 232 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁)
699698adantlr 715 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁)
700667, 668, 692, 696, 699elfzd 13532 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁))
701666, 700ffvelcdmd 7075 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
702 simpll 766 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝜑)
703667, 670, 678, 603syl3anbrc 1344 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ (ℤ≥‘𝑀))
704687adantlr 715 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 < 𝑁)
705703, 668, 704, 136syl3anbrc 1344 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ (𝑀..^𝑁))
706702, 705, 138syl2anc 584 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1)))
707691, 701, 706ltled 11383 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑃‘𝑖) ≤ (𝑃‘(𝑖 + 1)))
708648, 665, 707monoord 14050 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) ≤ (𝑃‘𝑁))
709708adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → (𝑃‘𝑘) ≤ (𝑃‘𝑁))
710640, 637, 636, 646, 709letrd 11392 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → 𝑡 ≤ (𝑃‘𝑁))
711635, 636, 640, 644, 710eliccd 45533 . . . . . . . . . . 11 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)))
712634, 711, 145syl2anc 584 . . . . . . . . . 10 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → 𝐴 ∈ ℂ)
713619, 632, 159syl2anc 584 . . . . . . . . . 10 (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1)
714615, 616, 618, 457, 633, 712, 713iblspltprt 46002 . . . . . . . . 9 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1)
715425mpteq1d 5210 . . . . . . . . . . . . 13 (𝑖 = 𝑘 → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) = (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴))
716715eleq1d 2819 . . . . . . . . . . . 12 (𝑖 = 𝑘 → ((𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1))
717505, 716imbi12d 344 . . . . . . . . . . 11 (𝑖 = 𝑘 → (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1) ↔ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1)))
718717, 159chvarvv 1998 . . . . . . . . . 10 ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1)
719503, 718syldan 591 . . . . . . . . 9 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1)
720432, 448, 515, 614, 714, 719itgspliticc 25790 . . . . . . . 8 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ∫((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = (∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡))
721720eqcomd 2741 . . . . . . 7 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = ∫((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡)
7227213adant3 1132 . . . . . 6 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → (∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = ∫((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡)
723428, 431, 7223eqtrrd 2775 . . . . 5 ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → ∫((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
724169, 170, 172, 723syl3anc 1373 . . . 4 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → ∫((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
7257243exp 1119 . . 3 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → ((𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)))
72618, 25, 32, 39, 168, 725fzind2 13801 . 2 (𝑁 ∈ ((𝑀 + 1)...𝑁) → (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑁))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))
72711, 726mpcom 38 1 (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑁))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)
Colors of variables: wff setvar class
Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2108   class class class wbr 5119   ↦ cmpt 5201  ⟶wf 6527  ‘cfv 6531  (class class class)co 7405  ℂcc 11127  ℝcr 11128  1c1 11130   + caddc 11132  ℝ*cxr 11268   < clt 11269   ≤ cle 11270   − cmin 11466  ℤcz 12588  ℤ≥cuz 12852  [,]cicc 13365  ...cfz 13524  ..^cfzo 13671  Σcsu 15702  𝐿1cibl 25570  ∫citg 25571
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5249  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729  ax-inf2 9655  ax-cnex 11185  ax-resscn 11186  ax-1cn 11187  ax-icn 11188  ax-addcl 11189  ax-addrcl 11190  ax-mulcl 11191  ax-mulrcl 11192  ax-mulcom 11193  ax-addass 11194  ax-mulass 11195  ax-distr 11196  ax-i2m1 11197  ax-1ne0 11198  ax-1rid 11199  ax-rnegex 11200  ax-rrecex 11201  ax-cnre 11202  ax-pre-lttri 11203  ax-pre-lttrn 11204  ax-pre-ltadd 11205  ax-pre-mulgt0 11206  ax-pre-sup 11207  ax-addf 11208
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-int 4923  df-iun 4969  df-disj 5087  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-se 5607  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-isom 6540  df-riota 7362  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7671  df-ofr 7672  df-om 7862  df-1st 7988  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-2o 8481  df-er 8719  df-map 8842  df-pm 8843  df-en 8960  df-dom 8961  df-sdom 8962  df-fin 8963  df-fi 9423  df-sup 9454  df-inf 9455  df-oi 9524  df-dju 9915  df-card 9953  df-pnf 11271  df-mnf 11272  df-xr 11273  df-ltxr 11274  df-le 11275  df-sub 11468  df-neg 11469  df-div 11895  df-nn 12241  df-2 12303  df-3 12304  df-4 12305  df-n0 12502  df-z 12589  df-uz 12853  df-q 12965  df-rp 13009  df-xneg 13128  df-xadd 13129  df-xmul 13130  df-ioo 13366  df-ico 13368  df-icc 13369  df-fz 13525  df-fzo 13672  df-fl 13809  df-mod 13887  df-seq 14020  df-exp 14080  df-hash 14349  df-cj 15118  df-re 15119  df-im 15120  df-sqrt 15254  df-abs 15255  df-clim 15504  df-sum 15703  df-rest 17436  df-topgen 17457  df-psmet 21307  df-xmet 21308  df-met 21309  df-bl 21310  df-mopn 21311  df-top 22832  df-topon 22849  df-bases 22884  df-cmp 23325  df-ovol 25417  df-vol 25418  df-mbf 25572  df-itg1 25573  df-itg2 25574  df-ibl 25575  df-itg 25576
This theorem is referenced by:  fourierdlem73  46208  fourierdlem81  46216  fourierdlem93  46228
  Copyright terms: Public domain W3C validator