Theorem ser3mono 10845

Description: The partial sums in an infinite series of positive terms form a monotonic sequence. (Contributed by NM, 17-Mar-2005.) (Revised by Jim Kingdon, 22-Apr-2023.)

Hypotheses

Ref	Expression
sermono.1	⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀))
sermono.2	⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝐾))
ser3mono.3	⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ ℝ)
sermono.4	⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ (𝐹‘𝑥))

Assertion

Ref	Expression
ser3mono	⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) ≤ (seq𝑀( + , 𝐹)‘𝑁))

Distinct variable groups:   𝑥,𝐹   𝑥,𝐾   𝑥,𝑀   𝑥,𝑁   𝜑,𝑥

Proof of Theorem ser3mono

Dummy variables 𝑘 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sermono.2	. 2 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝐾))
2		eqid 2232	. . . 4 ⊢ (ℤ≥‘𝑀) = (ℤ≥‘𝑀)
3		sermono.1	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀))
4		eluzel2 9854	. . . . . 6 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
5	3, 4	syl 14	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ ℤ)
6	5	adantr 276	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...𝑁)) → 𝑀 ∈ ℤ)
7		ser3mono.3	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ ℝ)
8	7	adantlr 477	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝐾...𝑁)) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ ℝ)
9	2, 6, 8	serfre 10842	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...𝑁)) → seq𝑀( + , 𝐹):(ℤ≥‘𝑀)⟶ℝ)
10		elfzuz 10351	. . . 4 ⊢ (𝑘 ∈ (𝐾...𝑁) → 𝑘 ∈ (ℤ≥‘𝐾))
11		uztrn 9867	. . . 4 ⊢ ((𝑘 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑀)) → 𝑘 ∈ (ℤ≥‘𝑀))
12	10, 3, 11	syl2anr 290	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...𝑁)) → 𝑘 ∈ (ℤ≥‘𝑀))
13	9, 12	ffvelcdmd 5812	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...𝑁)) → (seq𝑀( + , 𝐹)‘𝑘) ∈ ℝ)
14		fveq2 5669	. . . . . 6 ⊢ (𝑥 = (𝑘 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑘 + 1)))
15	14	breq2d 4120	. . . . 5 ⊢ (𝑥 = (𝑘 + 1) → (0 ≤ (𝐹‘𝑥) ↔ 0 ≤ (𝐹‘(𝑘 + 1))))
16		sermono.4	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ (𝐹‘𝑥))
17	16	ralrimiva 2615	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ ((𝐾 + 1)...𝑁)0 ≤ (𝐹‘𝑥))
18	17	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → ∀𝑥 ∈ ((𝐾 + 1)...𝑁)0 ≤ (𝐹‘𝑥))
19		simpr 110	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 𝑘 ∈ (𝐾...(𝑁 − 1)))
20	3	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 𝐾 ∈ (ℤ≥‘𝑀))
21		eluzelz 9859	. . . . . . . . 9 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → 𝐾 ∈ ℤ)
22	20, 21	syl 14	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 𝐾 ∈ ℤ)
23	1	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 𝑁 ∈ (ℤ≥‘𝐾))
24		eluzelz 9859	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → 𝑁 ∈ ℤ)
25	23, 24	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 𝑁 ∈ ℤ)
26		peano2zm 9611	. . . . . . . . 9 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
27	25, 26	syl 14	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝑁 − 1) ∈ ℤ)
28		elfzelz 10355	. . . . . . . . 9 ⊢ (𝑘 ∈ (𝐾...(𝑁 − 1)) → 𝑘 ∈ ℤ)
29	28	adantl 277	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 𝑘 ∈ ℤ)
30		1zzd 9600	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 1 ∈ ℤ)
31		fzaddel 10389	. . . . . . . 8 ⊢ (((𝐾 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) ∧ (𝑘 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑘 ∈ (𝐾...(𝑁 − 1)) ↔ (𝑘 + 1) ∈ ((𝐾 + 1)...((𝑁 − 1) + 1))))
32	22, 27, 29, 30, 31	syl22anc 1275	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝑘 ∈ (𝐾...(𝑁 − 1)) ↔ (𝑘 + 1) ∈ ((𝐾 + 1)...((𝑁 − 1) + 1))))
33	19, 32	mpbid 147	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝑘 + 1) ∈ ((𝐾 + 1)...((𝑁 − 1) + 1)))
34		zcn 9578	. . . . . . . . 9 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
35		ax-1cn 8216	. . . . . . . . 9 ⊢ 1 ∈ ℂ
36		npcan 8478	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 − 1) + 1) = 𝑁)
37	34, 35, 36	sylancl 413	. . . . . . . 8 ⊢ (𝑁 ∈ ℤ → ((𝑁 − 1) + 1) = 𝑁)
38	25, 37	syl 14	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁)
39	38	oveq2d 6065	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → ((𝐾 + 1)...((𝑁 − 1) + 1)) = ((𝐾 + 1)...𝑁))
40	33, 39	eleqtrd 2311	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝑘 + 1) ∈ ((𝐾 + 1)...𝑁))
41	15, 18, 40	rspcdva 2925	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 0 ≤ (𝐹‘(𝑘 + 1)))
42		fzelp1 10404	. . . . . . . 8 ⊢ (𝑘 ∈ (𝐾...(𝑁 − 1)) → 𝑘 ∈ (𝐾...((𝑁 − 1) + 1)))
43	42	adantl 277	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 𝑘 ∈ (𝐾...((𝑁 − 1) + 1)))
44	38	oveq2d 6065	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝐾...((𝑁 − 1) + 1)) = (𝐾...𝑁))
45	43, 44	eleqtrd 2311	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 𝑘 ∈ (𝐾...𝑁))
46	45, 13	syldan 282	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (seq𝑀( + , 𝐹)‘𝑘) ∈ ℝ)
47	14	eleq1d 2301	. . . . . 6 ⊢ (𝑥 = (𝑘 + 1) → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘(𝑘 + 1)) ∈ ℝ))
48	7	ralrimiva 2615	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ (ℤ≥‘𝑀)(𝐹‘𝑥) ∈ ℝ)
49	48	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → ∀𝑥 ∈ (ℤ≥‘𝑀)(𝐹‘𝑥) ∈ ℝ)
50		fzss1 10393	. . . . . . . . 9 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → (𝐾...𝑁) ⊆ (𝑀...𝑁))
51	20, 50	syl 14	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝐾...𝑁) ⊆ (𝑀...𝑁))
52		fzp1elp1 10405	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝐾...(𝑁 − 1)) → (𝑘 + 1) ∈ (𝐾...((𝑁 − 1) + 1)))
53	52	adantl 277	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝑘 + 1) ∈ (𝐾...((𝑁 − 1) + 1)))
54	53, 44	eleqtrd 2311	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝑘 + 1) ∈ (𝐾...𝑁))
55	51, 54	sseldd 3238	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝑘 + 1) ∈ (𝑀...𝑁))
56		elfzuz 10351	. . . . . . 7 ⊢ ((𝑘 + 1) ∈ (𝑀...𝑁) → (𝑘 + 1) ∈ (ℤ≥‘𝑀))
57	55, 56	syl 14	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝑘 + 1) ∈ (ℤ≥‘𝑀))
58	47, 49, 57	rspcdva 2925	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝐹‘(𝑘 + 1)) ∈ ℝ)
59	46, 58	addge01d 8803	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (0 ≤ (𝐹‘(𝑘 + 1)) ↔ (seq𝑀( + , 𝐹)‘𝑘) ≤ ((seq𝑀( + , 𝐹)‘𝑘) + (𝐹‘(𝑘 + 1)))))
60	41, 59	mpbid 147	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (seq𝑀( + , 𝐹)‘𝑘) ≤ ((seq𝑀( + , 𝐹)‘𝑘) + (𝐹‘(𝑘 + 1))))
61	45, 12	syldan 282	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 𝑘 ∈ (ℤ≥‘𝑀))
62	7	adantlr 477	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ ℝ)
63		readdcl 8249	. . . . 5 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ)
64	63	adantl 277	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 + 𝑦) ∈ ℝ)
65	61, 62, 64	seq3p1 10823	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (seq𝑀( + , 𝐹)‘(𝑘 + 1)) = ((seq𝑀( + , 𝐹)‘𝑘) + (𝐹‘(𝑘 + 1))))
66	60, 65	breqtrrd 4136	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (seq𝑀( + , 𝐹)‘𝑘) ≤ (seq𝑀( + , 𝐹)‘(𝑘 + 1)))
67	1, 13, 66	monoord 10843	1 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) ≤ (seq𝑀( + , 𝐹)‘𝑁))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1398   ∈ wcel 2203  ∀wral 2520   ⊆ wss 3210   class class class wbr 4108  ‘cfv 5351  (class class class)co 6049  ℂcc 8121  ℝcr 8122  0cc0 8123  1c1 8124   + caddc 8126   ≤ cle 8305   − cmin 8440  ℤcz 9573  ℤ_≥cuz 9849  ...cfz 10338  seqcseq 10805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-coll 4224  ax-sep 4227  ax-nul 4235  ax-pow 4286  ax-pr 4321  ax-un 4553  ax-setind 4658  ax-iinf 4709  ax-cnex 8214  ax-resscn 8215  ax-1cn 8216  ax-1re 8217  ax-icn 8218  ax-addcl 8219  ax-addrcl 8220  ax-mulcl 8221  ax-addcom 8223  ax-addass 8225  ax-distr 8227  ax-i2m1 8228  ax-0lt1 8229  ax-0id 8231  ax-rnegex 8232  ax-cnre 8234  ax-pre-ltirr 8235  ax-pre-ltwlin 8236  ax-pre-lttrn 8237  ax-pre-ltadd 8239

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-nel 2508  df-ral 2525  df-rex 2526  df-reu 2527  df-rab 2529  df-v 2814  df-sbc 3042  df-csb 3138  df-dif 3212  df-un 3214  df-in 3216  df-ss 3223  df-nul 3508  df-pw 3670  df-sn 3694  df-pr 3695  df-op 3697  df-uni 3914  df-int 3949  df-iun 3992  df-br 4109  df-opab 4171  df-mpt 4172  df-tr 4208  df-id 4413  df-iord 4486  df-on 4488  df-ilim 4489  df-suc 4491  df-iom 4712  df-xp 4754  df-rel 4755  df-cnv 4756  df-co 4757  df-dm 4758  df-rn 4759  df-res 4760  df-ima 4761  df-iota 5311  df-fun 5353  df-fn 5354  df-f 5355  df-f1 5356  df-fo 5357  df-f1o 5358  df-fv 5359  df-riota 6002  df-ov 6052  df-oprab 6053  df-mpo 6054  df-1st 6333  df-2nd 6334  df-recs 6535  df-frec 6621  df-pnf 8306  df-mnf 8307  df-xr 8308  df-ltxr 8309  df-le 8310  df-sub 8442  df-neg 8443  df-inn 9234  df-n0 9493  df-z 9574  df-uz 9850  df-fz 10339  df-seqfrec 10806

This theorem is referenced by: (None)