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

Theorem iblspltprt 40507
Description: If a function is integrable on any interval of a partition, then it is integrable on the whole interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
iblspltprt.1 𝑡𝜑
iblspltprt.2 (𝜑𝑀 ∈ ℤ)
iblspltprt.3 (𝜑𝑁 ∈ (ℤ‘(𝑀 + 1)))
iblspltprt.4 ((𝜑𝑖 ∈ (𝑀...𝑁)) → (𝑃𝑖) ∈ ℝ)
iblspltprt.5 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑃𝑖) < (𝑃‘(𝑖 + 1)))
iblspltprt.6 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁))) → 𝐴 ∈ ℂ)
iblspltprt.7 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1)
Assertion
Ref Expression
iblspltprt (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)) ↦ 𝐴) ∈ 𝐿1)
Distinct variable groups:   𝐴,𝑖   𝑖,𝑀,𝑡   𝑖,𝑁,𝑡   𝑃,𝑖,𝑡   𝜑,𝑖
Allowed substitution hints:   𝜑(𝑡)   𝐴(𝑡)

Proof of Theorem iblspltprt
Dummy variables 𝑘 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 iblspltprt.3 . . . 4 (𝜑𝑁 ∈ (ℤ‘(𝑀 + 1)))
2 eluzelz 11735 . . . 4 (𝑁 ∈ (ℤ‘(𝑀 + 1)) → 𝑁 ∈ ℤ)
31, 2syl 17 . . 3 (𝜑𝑁 ∈ ℤ)
4 eluzle 11738 . . . 4 (𝑁 ∈ (ℤ‘(𝑀 + 1)) → (𝑀 + 1) ≤ 𝑁)
51, 4syl 17 . . 3 (𝜑 → (𝑀 + 1) ≤ 𝑁)
63zred 11520 . . . 4 (𝜑𝑁 ∈ ℝ)
76leidd 10632 . . 3 (𝜑𝑁𝑁)
8 iblspltprt.2 . . . . 5 (𝜑𝑀 ∈ ℤ)
98peano2zd 11523 . . . 4 (𝜑 → (𝑀 + 1) ∈ ℤ)
10 elfz1 12369 . . . 4 (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ ((𝑀 + 1)...𝑁) ↔ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁𝑁𝑁)))
119, 3, 10syl2anc 694 . . 3 (𝜑 → (𝑁 ∈ ((𝑀 + 1)...𝑁) ↔ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁𝑁𝑁)))
123, 5, 7, 11mpbir3and 1264 . 2 (𝜑𝑁 ∈ ((𝑀 + 1)...𝑁))
13 fveq2 6229 . . . . . . 7 (𝑗 = (𝑀 + 1) → (𝑃𝑗) = (𝑃‘(𝑀 + 1)))
1413oveq2d 6706 . . . . . 6 (𝑗 = (𝑀 + 1) → ((𝑃𝑀)[,](𝑃𝑗)) = ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))))
1514mpteq1d 4771 . . . . 5 (𝑗 = (𝑀 + 1) → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑗)) ↦ 𝐴) = (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴))
1615eleq1d 2715 . . . 4 (𝑗 = (𝑀 + 1) → ((𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑗)) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿1))
1716imbi2d 329 . . 3 (𝑗 = (𝑀 + 1) → ((𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑗)) ↦ 𝐴) ∈ 𝐿1) ↔ (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿1)))
18 fveq2 6229 . . . . . . 7 (𝑗 = 𝑘 → (𝑃𝑗) = (𝑃𝑘))
1918oveq2d 6706 . . . . . 6 (𝑗 = 𝑘 → ((𝑃𝑀)[,](𝑃𝑗)) = ((𝑃𝑀)[,](𝑃𝑘)))
2019mpteq1d 4771 . . . . 5 (𝑗 = 𝑘 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑗)) ↦ 𝐴) = (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)) ↦ 𝐴))
2120eleq1d 2715 . . . 4 (𝑗 = 𝑘 → ((𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑗)) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)) ↦ 𝐴) ∈ 𝐿1))
2221imbi2d 329 . . 3 (𝑗 = 𝑘 → ((𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑗)) ↦ 𝐴) ∈ 𝐿1) ↔ (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)) ↦ 𝐴) ∈ 𝐿1)))
23 fveq2 6229 . . . . . . 7 (𝑗 = (𝑘 + 1) → (𝑃𝑗) = (𝑃‘(𝑘 + 1)))
2423oveq2d 6706 . . . . . 6 (𝑗 = (𝑘 + 1) → ((𝑃𝑀)[,](𝑃𝑗)) = ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))))
2524mpteq1d 4771 . . . . 5 (𝑗 = (𝑘 + 1) → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑗)) ↦ 𝐴) = (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴))
2625eleq1d 2715 . . . 4 (𝑗 = (𝑘 + 1) → ((𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑗)) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1))
2726imbi2d 329 . . 3 (𝑗 = (𝑘 + 1) → ((𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑗)) ↦ 𝐴) ∈ 𝐿1) ↔ (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1)))
28 fveq2 6229 . . . . . . 7 (𝑗 = 𝑁 → (𝑃𝑗) = (𝑃𝑁))
2928oveq2d 6706 . . . . . 6 (𝑗 = 𝑁 → ((𝑃𝑀)[,](𝑃𝑗)) = ((𝑃𝑀)[,](𝑃𝑁)))
3029mpteq1d 4771 . . . . 5 (𝑗 = 𝑁 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑗)) ↦ 𝐴) = (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)) ↦ 𝐴))
3130eleq1d 2715 . . . 4 (𝑗 = 𝑁 → ((𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑗)) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)) ↦ 𝐴) ∈ 𝐿1))
3231imbi2d 329 . . 3 (𝑗 = 𝑁 → ((𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑗)) ↦ 𝐴) ∈ 𝐿1) ↔ (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)) ↦ 𝐴) ∈ 𝐿1)))
33 uzid 11740 . . . . . . 7 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
348, 33syl 17 . . . . . 6 (𝜑𝑀 ∈ (ℤ𝑀))
358zred 11520 . . . . . . 7 (𝜑𝑀 ∈ ℝ)
36 1red 10093 . . . . . . . 8 (𝜑 → 1 ∈ ℝ)
3735, 36readdcld 10107 . . . . . . 7 (𝜑 → (𝑀 + 1) ∈ ℝ)
3835ltp1d 10992 . . . . . . 7 (𝜑𝑀 < (𝑀 + 1))
3935, 37, 6, 38, 5ltletrd 10235 . . . . . 6 (𝜑𝑀 < 𝑁)
40 elfzo2 12512 . . . . . 6 (𝑀 ∈ (𝑀..^𝑁) ↔ (𝑀 ∈ (ℤ𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁))
4134, 3, 39, 40syl3anbrc 1265 . . . . 5 (𝜑𝑀 ∈ (𝑀..^𝑁))
42 fveq2 6229 . . . . . . . . . 10 (𝑖 = 𝑀 → (𝑃𝑖) = (𝑃𝑀))
43 oveq1 6697 . . . . . . . . . . 11 (𝑖 = 𝑀 → (𝑖 + 1) = (𝑀 + 1))
4443fveq2d 6233 . . . . . . . . . 10 (𝑖 = 𝑀 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑀 + 1)))
4542, 44oveq12d 6708 . . . . . . . . 9 (𝑖 = 𝑀 → ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) = ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))))
4645mpteq1d 4771 . . . . . . . 8 (𝑖 = 𝑀 → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) = (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴))
4746eleq1d 2715 . . . . . . 7 (𝑖 = 𝑀 → ((𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿1))
4847imbi2d 329 . . . . . 6 (𝑖 = 𝑀 → ((𝜑 → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1) ↔ (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿1)))
49 iblspltprt.7 . . . . . . 7 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1)
5049expcom 450 . . . . . 6 (𝑖 ∈ (𝑀..^𝑁) → (𝜑 → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1))
5148, 50vtoclga 3303 . . . . 5 (𝑀 ∈ (𝑀..^𝑁) → (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿1))
5241, 51mpcom 38 . . . 4 (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿1)
5352a1i 11 . . 3 (𝑁 ∈ (ℤ‘(𝑀 + 1)) → (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈ 𝐿1))
54 nfv 1883 . . . . . 6 𝑡 𝑘 ∈ ((𝑀 + 1)..^𝑁)
55 iblspltprt.1 . . . . . . 7 𝑡𝜑
56 nfmpt1 4780 . . . . . . . 8 𝑡(𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)) ↦ 𝐴)
5756nfel1 2808 . . . . . . 7 𝑡(𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)) ↦ 𝐴) ∈ 𝐿1
5855, 57nfim 1865 . . . . . 6 𝑡(𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)) ↦ 𝐴) ∈ 𝐿1)
5954, 58, 55nf3an 1871 . . . . 5 𝑡(𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑)
60 simp3 1083 . . . . . 6 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → 𝜑)
61 simp1 1081 . . . . . 6 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → 𝑘 ∈ ((𝑀 + 1)..^𝑁))
6235leidd 10632 . . . . . . . . . . . . 13 (𝜑𝑀𝑀)
6335, 6, 39ltled 10223 . . . . . . . . . . . . 13 (𝜑𝑀𝑁)
64 elfz1 12369 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∈ (𝑀...𝑁) ↔ (𝑀 ∈ ℤ ∧ 𝑀𝑀𝑀𝑁)))
658, 3, 64syl2anc 694 . . . . . . . . . . . . 13 (𝜑 → (𝑀 ∈ (𝑀...𝑁) ↔ (𝑀 ∈ ℤ ∧ 𝑀𝑀𝑀𝑁)))
668, 62, 63, 65mpbir3and 1264 . . . . . . . . . . . 12 (𝜑𝑀 ∈ (𝑀...𝑁))
6766ancli 573 . . . . . . . . . . . 12 (𝜑 → (𝜑𝑀 ∈ (𝑀...𝑁)))
68 eleq1 2718 . . . . . . . . . . . . . . 15 (𝑖 = 𝑀 → (𝑖 ∈ (𝑀...𝑁) ↔ 𝑀 ∈ (𝑀...𝑁)))
6968anbi2d 740 . . . . . . . . . . . . . 14 (𝑖 = 𝑀 → ((𝜑𝑖 ∈ (𝑀...𝑁)) ↔ (𝜑𝑀 ∈ (𝑀...𝑁))))
7042eleq1d 2715 . . . . . . . . . . . . . 14 (𝑖 = 𝑀 → ((𝑃𝑖) ∈ ℝ ↔ (𝑃𝑀) ∈ ℝ))
7169, 70imbi12d 333 . . . . . . . . . . . . 13 (𝑖 = 𝑀 → (((𝜑𝑖 ∈ (𝑀...𝑁)) → (𝑃𝑖) ∈ ℝ) ↔ ((𝜑𝑀 ∈ (𝑀...𝑁)) → (𝑃𝑀) ∈ ℝ)))
72 iblspltprt.4 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (𝑀...𝑁)) → (𝑃𝑖) ∈ ℝ)
7371, 72vtoclg 3297 . . . . . . . . . . . 12 (𝑀 ∈ (𝑀...𝑁) → ((𝜑𝑀 ∈ (𝑀...𝑁)) → (𝑃𝑀) ∈ ℝ))
7466, 67, 73sylc 65 . . . . . . . . . . 11 (𝜑 → (𝑃𝑀) ∈ ℝ)
7574adantr 480 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑀) ∈ ℝ)
7675rexrd 10127 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑀) ∈ ℝ*)
77 simpl 472 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝜑)
78 elfzoelz 12509 . . . . . . . . . . . . 13 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 ∈ ℤ)
7978adantl 481 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ ℤ)
8035adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ∈ ℝ)
8179zred 11520 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ ℝ)
8237adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 + 1) ∈ ℝ)
8338adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < (𝑀 + 1))
84 elfzole1 12517 . . . . . . . . . . . . . . 15 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑀 + 1) ≤ 𝑘)
8584adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 + 1) ≤ 𝑘)
8680, 82, 81, 83, 85ltletrd 10235 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < 𝑘)
8780, 81, 86ltled 10223 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀𝑘)
886adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ ℝ)
89 elfzolt2 12518 . . . . . . . . . . . . . 14 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 < 𝑁)
9089adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 < 𝑁)
9181, 88, 90ltled 10223 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘𝑁)
928, 3jca 553 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
9392adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
94 elfz1 12369 . . . . . . . . . . . . 13 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘𝑁)))
9593, 94syl 17 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ ℤ ∧ 𝑀𝑘𝑘𝑁)))
9679, 87, 91, 95mpbir3and 1264 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (𝑀...𝑁))
97 eleq1 2718 . . . . . . . . . . . . . 14 (𝑖 = 𝑘 → (𝑖 ∈ (𝑀...𝑁) ↔ 𝑘 ∈ (𝑀...𝑁)))
9897anbi2d 740 . . . . . . . . . . . . 13 (𝑖 = 𝑘 → ((𝜑𝑖 ∈ (𝑀...𝑁)) ↔ (𝜑𝑘 ∈ (𝑀...𝑁))))
99 fveq2 6229 . . . . . . . . . . . . . 14 (𝑖 = 𝑘 → (𝑃𝑖) = (𝑃𝑘))
10099eleq1d 2715 . . . . . . . . . . . . 13 (𝑖 = 𝑘 → ((𝑃𝑖) ∈ ℝ ↔ (𝑃𝑘) ∈ ℝ))
10198, 100imbi12d 333 . . . . . . . . . . . 12 (𝑖 = 𝑘 → (((𝜑𝑖 ∈ (𝑀...𝑁)) → (𝑃𝑖) ∈ ℝ) ↔ ((𝜑𝑘 ∈ (𝑀...𝑁)) → (𝑃𝑘) ∈ ℝ)))
102101, 72chvarv 2299 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (𝑀...𝑁)) → (𝑃𝑘) ∈ ℝ)
10377, 96, 102syl2anc 694 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑘) ∈ ℝ)
104103rexrd 10127 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑘) ∈ ℝ*)
10579peano2zd 11523 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ ℤ)
106105zred 11520 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ ℝ)
107 1red 10093 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 1 ∈ ℝ)
10880, 81, 107, 86ltadd1dd 10676 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 + 1) < (𝑘 + 1))
10980, 82, 106, 83, 108lttrd 10236 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < (𝑘 + 1))
11080, 106, 109ltled 10223 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ≤ (𝑘 + 1))
111 zltp1le 11465 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 < 𝑁 ↔ (𝑘 + 1) ≤ 𝑁))
11278, 3, 111syl2anr 494 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 < 𝑁 ↔ (𝑘 + 1) ≤ 𝑁))
11390, 112mpbid 222 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ≤ 𝑁)
114 elfz1 12369 . . . . . . . . . . . . 13 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑘 + 1) ∈ (𝑀...𝑁) ↔ ((𝑘 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁)))
11593, 114syl 17 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ((𝑘 + 1) ∈ (𝑀...𝑁) ↔ ((𝑘 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁)))
116105, 110, 113, 115mpbir3and 1264 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ (𝑀...𝑁))
11777, 116jca 553 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁)))
118 eleq1 2718 . . . . . . . . . . . . . 14 (𝑖 = (𝑘 + 1) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑘 + 1) ∈ (𝑀...𝑁)))
119118anbi2d 740 . . . . . . . . . . . . 13 (𝑖 = (𝑘 + 1) → ((𝜑𝑖 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁))))
120 fveq2 6229 . . . . . . . . . . . . . 14 (𝑖 = (𝑘 + 1) → (𝑃𝑖) = (𝑃‘(𝑘 + 1)))
121120eleq1d 2715 . . . . . . . . . . . . 13 (𝑖 = (𝑘 + 1) → ((𝑃𝑖) ∈ ℝ ↔ (𝑃‘(𝑘 + 1)) ∈ ℝ))
122119, 121imbi12d 333 . . . . . . . . . . . 12 (𝑖 = (𝑘 + 1) → (((𝜑𝑖 ∈ (𝑀...𝑁)) → (𝑃𝑖) ∈ ℝ) ↔ ((𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁)) → (𝑃‘(𝑘 + 1)) ∈ ℝ)))
123122, 72vtoclg 3297 . . . . . . . . . . 11 ((𝑘 + 1) ∈ (𝑀...𝑁) → ((𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁)) → (𝑃‘(𝑘 + 1)) ∈ ℝ))
124116, 117, 123sylc 65 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ∈ ℝ)
125124rexrd 10127 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ∈ ℝ*)
126 eluz 11739 . . . . . . . . . . . 12 ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 ∈ (ℤ𝑀) ↔ 𝑀𝑘))
1278, 78, 126syl2an 493 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 ∈ (ℤ𝑀) ↔ 𝑀𝑘))
12887, 127mpbird 247 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (ℤ𝑀))
129 simpll 805 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝜑)
130 elfzelz 12380 . . . . . . . . . . . . 13 (𝑖 ∈ (𝑀...𝑘) → 𝑖 ∈ ℤ)
131130adantl 481 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ ℤ)
132 elfzle1 12382 . . . . . . . . . . . . 13 (𝑖 ∈ (𝑀...𝑘) → 𝑀𝑖)
133132adantl 481 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀𝑖)
134131zred 11520 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ ℝ)
135129, 6syl 17 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑁 ∈ ℝ)
13681adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑘 ∈ ℝ)
137 elfzle2 12383 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...𝑘) → 𝑖𝑘)
138137adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖𝑘)
13990adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑘 < 𝑁)
140134, 136, 135, 138, 139lelttrd 10233 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 < 𝑁)
141134, 135, 140ltled 10223 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖𝑁)
142 elfz1 12369 . . . . . . . . . . . . 13 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀𝑖𝑖𝑁)))
143129, 92, 1423syl 18 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀𝑖𝑖𝑁)))
144131, 133, 141, 143mpbir3and 1264 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ (𝑀...𝑁))
145129, 144, 72syl2anc 694 . . . . . . . . . 10 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑃𝑖) ∈ ℝ)
146 simpll 805 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝜑)
147 elfzelz 12380 . . . . . . . . . . . . . 14 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ∈ ℤ)
148147adantl 481 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ ℤ)
149 elfzle1 12382 . . . . . . . . . . . . . 14 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑀𝑖)
150149adantl 481 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀𝑖)
151148zred 11520 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ ℝ)
152146, 6syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑁 ∈ ℝ)
15381adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑘 ∈ ℝ)
154 1red 10093 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 1 ∈ ℝ)
155153, 154resubcld 10496 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑘 − 1) ∈ ℝ)
156 elfzle2 12383 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ≤ (𝑘 − 1))
157156adantl 481 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ≤ (𝑘 − 1))
15878zred 11520 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 ∈ ℝ)
159 1red 10093 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 1 ∈ ℝ)
160158, 159resubcld 10496 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑘 − 1) ∈ ℝ)
161 elfzoel2 12508 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑁 ∈ ℤ)
162161zred 11520 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑁 ∈ ℝ)
163158ltm1d 10994 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑘 − 1) < 𝑘)
164160, 158, 162, 163, 89lttrd 10236 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑘 − 1) < 𝑁)
165164ad2antlr 763 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑘 − 1) < 𝑁)
166151, 155, 152, 157, 165lelttrd 10233 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 < 𝑁)
167151, 152, 166ltled 10223 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖𝑁)
168146, 92, 1423syl 18 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀𝑖𝑖𝑁)))
169148, 150, 167, 168mpbir3and 1264 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (𝑀...𝑁))
170146, 169, 72syl2anc 694 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃𝑖) ∈ ℝ)
171148peano2zd 11523 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ∈ ℤ)
172 elfzel1 12379 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑀 ∈ ℤ)
173172zred 11520 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑀 ∈ ℝ)
174147zred 11520 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ∈ ℝ)
175 1red 10093 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 1 ∈ ℝ)
176174, 175readdcld 10107 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...(𝑘 − 1)) → (𝑖 + 1) ∈ ℝ)
177174ltp1d 10992 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 < (𝑖 + 1))
178173, 174, 176, 149, 177lelttrd 10233 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑀 < (𝑖 + 1))
179173, 176, 178ltled 10223 . . . . . . . . . . . . . 14 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑀 ≤ (𝑖 + 1))
180179adantl 481 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 ≤ (𝑖 + 1))
181146, 1, 23syl 18 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑁 ∈ ℤ)
182 zltp1le 11465 . . . . . . . . . . . . . . 15 ((𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
183148, 181, 182syl2anc 694 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
184166, 183mpbid 222 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ≤ 𝑁)
185 elfz1 12369 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
186146, 92, 1853syl 18 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
187171, 180, 184, 186mpbir3and 1264 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁))
188146, 187jca 553 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝜑 ∧ (𝑖 + 1) ∈ (𝑀...𝑁)))
189 eleq1 2718 . . . . . . . . . . . . . . 15 (𝑘 = (𝑖 + 1) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑖 + 1) ∈ (𝑀...𝑁)))
190189anbi2d 740 . . . . . . . . . . . . . 14 (𝑘 = (𝑖 + 1) → ((𝜑𝑘 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ (𝑖 + 1) ∈ (𝑀...𝑁))))
191 fveq2 6229 . . . . . . . . . . . . . . 15 (𝑘 = (𝑖 + 1) → (𝑃𝑘) = (𝑃‘(𝑖 + 1)))
192191eleq1d 2715 . . . . . . . . . . . . . 14 (𝑘 = (𝑖 + 1) → ((𝑃𝑘) ∈ ℝ ↔ (𝑃‘(𝑖 + 1)) ∈ ℝ))
193190, 192imbi12d 333 . . . . . . . . . . . . 13 (𝑘 = (𝑖 + 1) → (((𝜑𝑘 ∈ (𝑀...𝑁)) → (𝑃𝑘) ∈ ℝ) ↔ ((𝜑 ∧ (𝑖 + 1) ∈ (𝑀...𝑁)) → (𝑃‘(𝑖 + 1)) ∈ ℝ)))
194193, 102vtoclg 3297 . . . . . . . . . . . 12 ((𝑖 + 1) ∈ (𝑀...𝑁) → ((𝜑 ∧ (𝑖 + 1) ∈ (𝑀...𝑁)) → (𝑃‘(𝑖 + 1)) ∈ ℝ))
195187, 188, 194sylc 65 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
196 elfzuz 12376 . . . . . . . . . . . . . 14 (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ∈ (ℤ𝑀))
197196adantl 481 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (ℤ𝑀))
198 elfzo2 12512 . . . . . . . . . . . . 13 (𝑖 ∈ (𝑀..^𝑁) ↔ (𝑖 ∈ (ℤ𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑖 < 𝑁))
199197, 181, 166, 198syl3anbrc 1265 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (𝑀..^𝑁))
200 iblspltprt.5 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑃𝑖) < (𝑃‘(𝑖 + 1)))
201146, 199, 200syl2anc 694 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃𝑖) < (𝑃‘(𝑖 + 1)))
202170, 195, 201ltled 10223 . . . . . . . . . 10 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃𝑖) ≤ (𝑃‘(𝑖 + 1)))
203128, 145, 202monoord 12871 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑀) ≤ (𝑃𝑘))
204161adantl 481 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ ℤ)
205 elfzo2 12512 . . . . . . . . . . . 12 (𝑘 ∈ (𝑀..^𝑁) ↔ (𝑘 ∈ (ℤ𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑘 < 𝑁))
206128, 204, 90, 205syl3anbrc 1265 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (𝑀..^𝑁))
207 eleq1 2718 . . . . . . . . . . . . . 14 (𝑖 = 𝑘 → (𝑖 ∈ (𝑀..^𝑁) ↔ 𝑘 ∈ (𝑀..^𝑁)))
208207anbi2d 740 . . . . . . . . . . . . 13 (𝑖 = 𝑘 → ((𝜑𝑖 ∈ (𝑀..^𝑁)) ↔ (𝜑𝑘 ∈ (𝑀..^𝑁))))
209 oveq1 6697 . . . . . . . . . . . . . . 15 (𝑖 = 𝑘 → (𝑖 + 1) = (𝑘 + 1))
210209fveq2d 6233 . . . . . . . . . . . . . 14 (𝑖 = 𝑘 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑘 + 1)))
21199, 210breq12d 4698 . . . . . . . . . . . . 13 (𝑖 = 𝑘 → ((𝑃𝑖) < (𝑃‘(𝑖 + 1)) ↔ (𝑃𝑘) < (𝑃‘(𝑘 + 1))))
212208, 211imbi12d 333 . . . . . . . . . . . 12 (𝑖 = 𝑘 → (((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑃𝑖) < (𝑃‘(𝑖 + 1))) ↔ ((𝜑𝑘 ∈ (𝑀..^𝑁)) → (𝑃𝑘) < (𝑃‘(𝑘 + 1)))))
213212, 200chvarv 2299 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (𝑀..^𝑁)) → (𝑃𝑘) < (𝑃‘(𝑘 + 1)))
21477, 206, 213syl2anc 694 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑘) < (𝑃‘(𝑘 + 1)))
215103, 124, 214ltled 10223 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑘) ≤ (𝑃‘(𝑘 + 1)))
216 iccintsng 40067 . . . . . . . . 9 ((((𝑃𝑀) ∈ ℝ* ∧ (𝑃𝑘) ∈ ℝ* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ*) ∧ ((𝑃𝑀) ≤ (𝑃𝑘) ∧ (𝑃𝑘) ≤ (𝑃‘(𝑘 + 1)))) → (((𝑃𝑀)[,](𝑃𝑘)) ∩ ((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))) = {(𝑃𝑘)})
21776, 104, 125, 203, 215, 216syl32anc 1374 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (((𝑃𝑀)[,](𝑃𝑘)) ∩ ((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))) = {(𝑃𝑘)})
218217fveq2d 6233 . . . . . . 7 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (vol*‘(((𝑃𝑀)[,](𝑃𝑘)) ∩ ((𝑃𝑘)[,](𝑃‘(𝑘 + 1))))) = (vol*‘{(𝑃𝑘)}))
219 ovolsn 23309 . . . . . . . 8 ((𝑃𝑘) ∈ ℝ → (vol*‘{(𝑃𝑘)}) = 0)
220103, 219syl 17 . . . . . . 7 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (vol*‘{(𝑃𝑘)}) = 0)
221218, 220eqtrd 2685 . . . . . 6 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (vol*‘(((𝑃𝑀)[,](𝑃𝑘)) ∩ ((𝑃𝑘)[,](𝑃‘(𝑘 + 1))))) = 0)
22260, 61, 221syl2anc 694 . . . . 5 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → (vol*‘(((𝑃𝑀)[,](𝑃𝑘)) ∩ ((𝑃𝑘)[,](𝑃‘(𝑘 + 1))))) = 0)
22375, 124, 103, 203, 215eliccd 40044 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃𝑘) ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))))
22475, 124, 2233jca 1261 . . . . . . 7 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ((𝑃𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ ∧ (𝑃𝑘) ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))))
22560, 61, 224syl2anc 694 . . . . . 6 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → ((𝑃𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ ∧ (𝑃𝑘) ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))))
226 iccsplit 12343 . . . . . 6 (((𝑃𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ ∧ (𝑃𝑘) ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))) = (((𝑃𝑀)[,](𝑃𝑘)) ∪ ((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))))
227225, 226syl 17 . . . . 5 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))) = (((𝑃𝑀)[,](𝑃𝑘)) ∪ ((𝑃𝑘)[,](𝑃‘(𝑘 + 1)))))
228 simpl3 1086 . . . . . 6 (((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝜑)
229 simpl1 1084 . . . . . 6 (((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑘 ∈ ((𝑀 + 1)..^𝑁))
230 simpr 476 . . . . . 6 (((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))))
231 simp1 1081 . . . . . . 7 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝜑)
232 eliccxr 40055 . . . . . . . . 9 (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))) → 𝑡 ∈ ℝ*)
2332323ad2ant3 1104 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ℝ*)
23474rexrd 10127 . . . . . . . . . 10 (𝜑 → (𝑃𝑀) ∈ ℝ*)
2352343ad2ant1 1102 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃𝑀) ∈ ℝ*)
2361253adant3 1101 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ∈ ℝ*)
237 simp3 1083 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))))
238 iccgelb 12268 . . . . . . . . 9 (((𝑃𝑀) ∈ ℝ* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ*𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃𝑀) ≤ 𝑡)
239235, 236, 237, 238syl3anc 1366 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃𝑀) ≤ 𝑡)
24075, 124jca 553 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ((𝑃𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ))
2412403adant3 1101 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → ((𝑃𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ))
242 iccssre 12293 . . . . . . . . . . 11 (((𝑃𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ) → ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))) ⊆ ℝ)
243242sseld 3635 . . . . . . . . . 10 (((𝑃𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ) → (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))) → 𝑡 ∈ ℝ))
244241, 237, 243sylc 65 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ℝ)
2451243adant3 1101 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ∈ ℝ)
246 elfz1 12369 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (𝑀...𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑀𝑁𝑁𝑁)))
2478, 3, 246syl2anc 694 . . . . . . . . . . . . 13 (𝜑 → (𝑁 ∈ (𝑀...𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑀𝑁𝑁𝑁)))
2483, 63, 7, 247mpbir3and 1264 . . . . . . . . . . . 12 (𝜑𝑁 ∈ (𝑀...𝑁))
249248ancli 573 . . . . . . . . . . 11 (𝜑 → (𝜑𝑁 ∈ (𝑀...𝑁)))
250 eleq1 2718 . . . . . . . . . . . . . 14 (𝑖 = 𝑁 → (𝑖 ∈ (𝑀...𝑁) ↔ 𝑁 ∈ (𝑀...𝑁)))
251250anbi2d 740 . . . . . . . . . . . . 13 (𝑖 = 𝑁 → ((𝜑𝑖 ∈ (𝑀...𝑁)) ↔ (𝜑𝑁 ∈ (𝑀...𝑁))))
252 fveq2 6229 . . . . . . . . . . . . . 14 (𝑖 = 𝑁 → (𝑃𝑖) = (𝑃𝑁))
253252eleq1d 2715 . . . . . . . . . . . . 13 (𝑖 = 𝑁 → ((𝑃𝑖) ∈ ℝ ↔ (𝑃𝑁) ∈ ℝ))
254251, 253imbi12d 333 . . . . . . . . . . . 12 (𝑖 = 𝑁 → (((𝜑𝑖 ∈ (𝑀...𝑁)) → (𝑃𝑖) ∈ ℝ) ↔ ((𝜑𝑁 ∈ (𝑀...𝑁)) → (𝑃𝑁) ∈ ℝ)))
255254, 72vtoclg 3297 . . . . . . . . . . 11 (𝑁 ∈ ℤ → ((𝜑𝑁 ∈ (𝑀...𝑁)) → (𝑃𝑁) ∈ ℝ))
2563, 249, 255sylc 65 . . . . . . . . . 10 (𝜑 → (𝑃𝑁) ∈ ℝ)
2572563ad2ant1 1102 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃𝑁) ∈ ℝ)
258 elicc1 12257 . . . . . . . . . . . 12 (((𝑃𝑀) ∈ ℝ* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ*) → (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))) ↔ (𝑡 ∈ ℝ* ∧ (𝑃𝑀) ≤ 𝑡𝑡 ≤ (𝑃‘(𝑘 + 1)))))
259235, 236, 258syl2anc 694 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))) ↔ (𝑡 ∈ ℝ* ∧ (𝑃𝑀) ≤ 𝑡𝑡 ≤ (𝑃‘(𝑘 + 1)))))
260237, 259mpbid 222 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑡 ∈ ℝ* ∧ (𝑃𝑀) ≤ 𝑡𝑡 ≤ (𝑃‘(𝑘 + 1))))
261260simp3d 1095 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ≤ (𝑃‘(𝑘 + 1)))
262 elfzop1le2 39816 . . . . . . . . . . . . 13 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑘 + 1) ≤ 𝑁)
26378peano2zd 11523 . . . . . . . . . . . . . 14 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑘 + 1) ∈ ℤ)
264 eluz 11739 . . . . . . . . . . . . . 14 (((𝑘 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ‘(𝑘 + 1)) ↔ (𝑘 + 1) ≤ 𝑁))
265263, 161, 264syl2anc 694 . . . . . . . . . . . . 13 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑁 ∈ (ℤ‘(𝑘 + 1)) ↔ (𝑘 + 1) ≤ 𝑁))
266262, 265mpbird 247 . . . . . . . . . . . 12 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑁 ∈ (ℤ‘(𝑘 + 1)))
267266adantl 481 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ (ℤ‘(𝑘 + 1)))
268 simpll 805 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝜑)
269 elfzelz 12380 . . . . . . . . . . . . . 14 (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖 ∈ ℤ)
270269adantl 481 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℤ)
271268, 35syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 ∈ ℝ)
272270zred 11520 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℝ)
27381adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 ∈ ℝ)
27486adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 < 𝑘)
275158adantr 480 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 ∈ ℝ)
276 1red 10093 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 1 ∈ ℝ)
277275, 276readdcld 10107 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑘 + 1) ∈ ℝ)
278269zred 11520 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖 ∈ ℝ)
279278adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℝ)
280275ltp1d 10992 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < (𝑘 + 1))
281 elfzle1 12382 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ((𝑘 + 1)...𝑁) → (𝑘 + 1) ≤ 𝑖)
282281adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑘 + 1) ≤ 𝑖)
283275, 277, 279, 280, 282ltletrd 10235 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < 𝑖)
284283adantll 750 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < 𝑖)
285271, 273, 272, 274, 284lttrd 10236 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 < 𝑖)
286271, 272, 285ltled 10223 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀𝑖)
287 elfzle2 12383 . . . . . . . . . . . . . 14 (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖𝑁)
288287adantl 481 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖𝑁)
289268, 92, 1423syl 18 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀𝑖𝑖𝑁)))
290270, 286, 288, 289mpbir3and 1264 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ (𝑀...𝑁))
291268, 290, 72syl2anc 694 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑃𝑖) ∈ ℝ)
292 simpll 805 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝜑)
293 elfzelz 12380 . . . . . . . . . . . . . . 15 (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ∈ ℤ)
294293adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℤ)
295292, 35syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℝ)
296294zred 11520 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
29781adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 ∈ ℝ)
29886adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < 𝑘)
299158adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 ∈ ℝ)
300 1red 10093 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
301299, 300readdcld 10107 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑘 + 1) ∈ ℝ)
302293zred 11520 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ∈ ℝ)
303302adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
304299ltp1d 10992 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < (𝑘 + 1))
305 elfzle1 12382 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → (𝑘 + 1) ≤ 𝑖)
306305adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑘 + 1) ≤ 𝑖)
307299, 301, 303, 304, 306ltletrd 10235 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < 𝑖)
308307adantll 750 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < 𝑖)
309295, 297, 296, 298, 308lttrd 10236 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < 𝑖)
310295, 296, 309ltled 10223 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀𝑖)
311302adantl 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ)
3126adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℝ)
313 1red 10093 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 1 ∈ ℝ)
314312, 313resubcld 10496 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
315 elfzle2 12383 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ≤ (𝑁 − 1))
316315adantl 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ≤ (𝑁 − 1))
317312ltm1d 10994 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
318311, 314, 312, 316, 317lelttrd 10233 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 < 𝑁)
319311, 312, 318ltled 10223 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖𝑁)
320319adantlr 751 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖𝑁)
321292, 92, 1423syl 18 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀𝑖𝑖𝑁)))
322294, 310, 320, 321mpbir3and 1264 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑁))
323292, 322, 72syl2anc 694 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃𝑖) ∈ ℝ)
324294peano2zd 11523 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℤ)
325324zred 11520 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ)
326303, 300readdcld 10107 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ)
327299, 303, 307ltled 10223 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘𝑖)
328299, 303, 300, 327leadd1dd 10679 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑘 + 1) ≤ (𝑖 + 1))
329299, 301, 326, 304, 328ltletrd 10235 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < (𝑖 + 1))
330329adantll 750 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < (𝑖 + 1))
331295, 297, 325, 298, 330lttrd 10236 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < (𝑖 + 1))
332295, 325, 331ltled 10223 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ≤ (𝑖 + 1))
333293, 3, 182syl2anr 494 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁))
334318, 333mpbid 222 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁)
335334adantlr 751 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁)
336292, 92, 1853syl 18 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁)))
337324, 332, 335, 336mpbir3and 1264 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁))
338292, 337jca 553 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝜑 ∧ (𝑖 + 1) ∈ (𝑀...𝑁)))
339337, 338, 194sylc 65 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ)
340292, 8syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℤ)
341 eluz 11739 . . . . . . . . . . . . . . . 16 ((𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑖 ∈ (ℤ𝑀) ↔ 𝑀𝑖))
342340, 294, 341syl2anc 694 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 ∈ (ℤ𝑀) ↔ 𝑀𝑖))
343310, 342mpbird 247 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (ℤ𝑀))
344292, 1, 23syl 18 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℤ)
345318adantlr 751 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 < 𝑁)
346343, 344, 345, 198syl3anbrc 1265 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀..^𝑁))
347292, 346, 200syl2anc 694 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃𝑖) < (𝑃‘(𝑖 + 1)))
348323, 339, 347ltled 10223 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃𝑖) ≤ (𝑃‘(𝑖 + 1)))
349267, 291, 348monoord 12871 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ≤ (𝑃𝑁))
3503493adant3 1101 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ≤ (𝑃𝑁))
351244, 245, 257, 261, 350letrd 10232 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ≤ (𝑃𝑁))
352257rexrd 10127 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃𝑁) ∈ ℝ*)
353 elicc1 12257 . . . . . . . . 9 (((𝑃𝑀) ∈ ℝ* ∧ (𝑃𝑁) ∈ ℝ*) → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)) ↔ (𝑡 ∈ ℝ* ∧ (𝑃𝑀) ≤ 𝑡𝑡 ≤ (𝑃𝑁))))
354235, 352, 353syl2anc 694 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)) ↔ (𝑡 ∈ ℝ* ∧ (𝑃𝑀) ≤ 𝑡𝑡 ≤ (𝑃𝑁))))
355233, 239, 351, 354mpbir3and 1264 . . . . . . 7 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)))
356 iblspltprt.6 . . . . . . 7 ((𝜑𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁))) → 𝐴 ∈ ℂ)
357231, 355, 356syl2anc 694 . . . . . 6 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝐴 ∈ ℂ)
358228, 229, 230, 357syl3anc 1366 . . . . 5 (((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) ∧ 𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝐴 ∈ ℂ)
359 simp2 1082 . . . . . 6 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)) ↦ 𝐴) ∈ 𝐿1))
36060, 359mpd 15 . . . . 5 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)) ↦ 𝐴) ∈ 𝐿1)
36160, 61jca 553 . . . . . 6 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → (𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)))
36277, 206jca 553 . . . . . 6 ((𝜑𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝜑𝑘 ∈ (𝑀..^𝑁)))
36399, 210oveq12d 6708 . . . . . . . . . 10 (𝑖 = 𝑘 → ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) = ((𝑃𝑘)[,](𝑃‘(𝑘 + 1))))
364363mpteq1d 4771 . . . . . . . . 9 (𝑖 = 𝑘 → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) = (𝑡 ∈ ((𝑃𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴))
365364eleq1d 2715 . . . . . . . 8 (𝑖 = 𝑘 → ((𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1))
366208, 365imbi12d 333 . . . . . . 7 (𝑖 = 𝑘 → (((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1) ↔ ((𝜑𝑘 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1)))
367366, 49chvarv 2299 . . . . . 6 ((𝜑𝑘 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1)
368361, 362, 3673syl 18 . . . . 5 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → (𝑡 ∈ ((𝑃𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1)
36959, 222, 227, 358, 360, 368iblsplitf 40504 . . . 4 ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1)
3703693exp 1283 . . 3 (𝑘 ∈ ((𝑀 + 1)..^𝑁) → ((𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑘)) ↦ 𝐴) ∈ 𝐿1) → (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈ 𝐿1)))
37117, 22, 27, 32, 53, 370fzind2 12626 . 2 (𝑁 ∈ ((𝑀 + 1)...𝑁) → (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)) ↦ 𝐴) ∈ 𝐿1))
37212, 371mpcom 38 1 (𝜑 → (𝑡 ∈ ((𝑃𝑀)[,](𝑃𝑁)) ↦ 𝐴) ∈ 𝐿1)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wnf 1748  wcel 2030  cun 3605  cin 3606  {csn 4210   class class class wbr 4685  cmpt 4762  cfv 5926  (class class class)co 6690  cc 9972  cr 9973  0cc0 9974  1c1 9975   + caddc 9977  *cxr 10111   < clt 10112  cle 10113  cmin 10304  cz 11415  cuz 11725  [,]cicc 12216  ...cfz 12364  ..^cfzo 12504  vol*covol 23277  𝐿1cibl 23431
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-disj 4653  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-ofr 6940  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-sum 14461  df-rest 16130  df-topgen 16151  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-top 20747  df-topon 20764  df-bases 20798  df-cmp 21238  df-ovol 23279  df-vol 23280  df-mbf 23433  df-itg1 23434  df-itg2 23435  df-ibl 23436
This theorem is referenced by:  itgspltprt  40513  fourierdlem69  40710
  Copyright terms: Public domain W3C validator