Theorem fsumcmp 6986

Description: If all of the terms of finite sums compare, so do the sums.

Assertion

Ref	Expression
fsumcmp	⊢ ((N ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...N)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) → Σk ∈ (M...N)A ≤ Σk ∈ (M...N)B)

Distinct variable groups:   k,M   k,N

Proof of Theorem fsumcmp

Step	Hyp	Ref	Expression
1		ra4sbca 1994	. . . . . . 7 ⊢ ((M ∈ (M...M) ⋀ ∀k ∈ (M...M)A ≤ B) → [M / k]A ≤ B)
2		elfz3t 6431	. . . . . . 7 ⊢ (M ∈ ℤ → M ∈ (M...M))
3		3simp3 789	. . . . . . . 8 ⊢ ((A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → A ≤ B)
4	3	r19.20si 1703	. . . . . . 7 ⊢ (∀k ∈ (M...M)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → ∀k ∈ (M...M)A ≤ B)
5	1, 2, 4	syl2an 454	. . . . . 6 ⊢ ((M ∈ ℤ ⋀ ∀k ∈ (M...M)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) → [M / k]A ≤ B)
6		sbcbr12g 2658	. . . . . . 7 ⊢ (M ∈ ℤ → ([M / k]A ≤ B ↔ [M / k]A ≤ [M / k]B))
7	6	adantr 389	. . . . . 6 ⊢ ((M ∈ ℤ ⋀ ∀k ∈ (M...M)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) → ([M / k]A ≤ B ↔ [M / k]A ≤ [M / k]B))
8	5, 7	mpbid 195	. . . . 5 ⊢ ((M ∈ ℤ ⋀ ∀k ∈ (M...M)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) → [M / k]A ≤ [M / k]B)
9		fsum1s 6955	. . . . . 6 ⊢ ((M ∈ ℤ ⋀ ∀k ∈ (M...M)A ∈ ℝ) → Σk ∈ (M...M)A = [M / k]A)
10		3simp1 787	. . . . . . 7 ⊢ ((A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → A ∈ ℝ)
11	10	r19.20si 1703	. . . . . 6 ⊢ (∀k ∈ (M...M)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → ∀k ∈ (M...M)A ∈ ℝ)
12	9, 11	sylan2 451	. . . . 5 ⊢ ((M ∈ ℤ ⋀ ∀k ∈ (M...M)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) → Σk ∈ (M...M)A = [M / k]A)
13		fsum1s 6955	. . . . . 6 ⊢ ((M ∈ ℤ ⋀ ∀k ∈ (M...M)B ∈ ℝ) → Σk ∈ (M...M)B = [M / k]B)
14		3simp2 788	. . . . . . 7 ⊢ ((A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → B ∈ ℝ)
15	14	r19.20si 1703	. . . . . 6 ⊢ (∀k ∈ (M...M)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → ∀k ∈ (M...M)B ∈ ℝ)
16	13, 15	sylan2 451	. . . . 5 ⊢ ((M ∈ ℤ ⋀ ∀k ∈ (M...M)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) → Σk ∈ (M...M)B = [M / k]B)
17	8, 12, 16	3brtr4d 2640	. . . 4 ⊢ ((M ∈ ℤ ⋀ ∀k ∈ (M...M)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) → Σk ∈ (M...M)A ≤ Σk ∈ (M...M)B)
18	17	ex 373	. . 3 ⊢ (M ∈ ℤ → (∀k ∈ (M...M)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → Σk ∈ (M...M)A ≤ Σk ∈ (M...M)B))
19		fzssp1t 6446	. . . . . . . . 9 ⊢ ((M ∈ ℤ ⋀ m ∈ ℤ) → (M...m) ⊆ (M...(m + 1)))
20		eluzel2 6364	. . . . . . . . 9 ⊢ (m ∈ (ℤ≥ ‘M) → M ∈ ℤ)
21		eluzelz 6363	. . . . . . . . 9 ⊢ (m ∈ (ℤ≥ ‘M) → m ∈ ℤ)
22	19, 20, 21	sylanc 471	. . . . . . . 8 ⊢ (m ∈ (ℤ≥ ‘M) → (M...m) ⊆ (M...(m + 1)))
23	22	sseld 2063	. . . . . . 7 ⊢ (m ∈ (ℤ≥ ‘M) → (k ∈ (M...m) → k ∈ (M...(m + 1))))
24	23	imim1d 28	. . . . . 6 ⊢ (m ∈ (ℤ≥ ‘M) → ((k ∈ (M...(m + 1)) → (A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) → (k ∈ (M...m) → (A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B))))
25	24	r19.20dv2 1708	. . . . 5 ⊢ (m ∈ (ℤ≥ ‘M) → (∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → ∀k ∈ (M...m)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)))
26	25	imim1d 28	. . . 4 ⊢ (m ∈ (ℤ≥ ‘M) → ((∀k ∈ (M...m)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → Σk ∈ (M...m)A ≤ Σk ∈ (M...m)B) → (∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → Σk ∈ (M...m)A ≤ Σk ∈ (M...m)B)))
27		fsump1s 6959	. . . . . . . . . 10 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))A ∈ ℝ) → Σk ∈ (M...(m + 1))A = (Σk ∈ (M...m)A + [(m + 1) / k]A))
28	10	r19.20si 1703	. . . . . . . . . 10 ⊢ (∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → ∀k ∈ (M...(m + 1))A ∈ ℝ)
29	27, 28	sylan2 451	. . . . . . . . 9 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) → Σk ∈ (M...(m + 1))A = (Σk ∈ (M...m)A + [(m + 1) / k]A))
30	29	adantr 389	. . . . . . . 8 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) ⋀ Σk ∈ (M...m)A ≤ Σk ∈ (M...m)B) → Σk ∈ (M...(m + 1))A = (Σk ∈ (M...m)A + [(m + 1) / k]A))
31		pm3.27 323	. . . . . . . . 9 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) ⋀ Σk ∈ (M...m)A ≤ Σk ∈ (M...m)B) → Σk ∈ (M...m)A ≤ Σk ∈ (M...m)B)
32		leadd1t 5607	. . . . . . . . . 10 ⊢ ((Σk ∈ (M...m)A ∈ ℝ ⋀ Σk ∈ (M...m)B ∈ ℝ ⋀ [(m + 1) / k]A ∈ ℝ) → (Σk ∈ (M...m)A ≤ Σk ∈ (M...m)B ↔ (Σk ∈ (M...m)A + [(m + 1) / k]A) ≤ (Σk ∈ (M...m)B + [(m + 1) / k]A)))
33	10	a1i 8	. . . . . . . . . . . . . . 15 ⊢ (m ∈ (ℤ≥ ‘M) → ((A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → A ∈ ℝ))
34	23, 33	imim12d 29	. . . . . . . . . . . . . 14 ⊢ (m ∈ (ℤ≥ ‘M) → ((k ∈ (M...(m + 1)) → (A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) → (k ∈ (M...m) → A ∈ ℝ)))
35	34	r19.20dv2 1708	. . . . . . . . . . . . 13 ⊢ (m ∈ (ℤ≥ ‘M) → (∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → ∀k ∈ (M...m)A ∈ ℝ))
36	35	imp 350	. . . . . . . . . . . 12 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) → ∀k ∈ (M...m)A ∈ ℝ)
37		fsumreclt 6963	. . . . . . . . . . . 12 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...m)A ∈ ℝ) → Σk ∈ (M...m)A ∈ ℝ)
38	36, 37	syldan 467	. . . . . . . . . . 11 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) → Σk ∈ (M...m)A ∈ ℝ)
39	38	adantr 389	. . . . . . . . . 10 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) ⋀ Σk ∈ (M...m)A ≤ Σk ∈ (M...m)B) → Σk ∈ (M...m)A ∈ ℝ)
40	14	a1i 8	. . . . . . . . . . . . . . 15 ⊢ (m ∈ (ℤ≥ ‘M) → ((A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → B ∈ ℝ))
41	23, 40	imim12d 29	. . . . . . . . . . . . . 14 ⊢ (m ∈ (ℤ≥ ‘M) → ((k ∈ (M...(m + 1)) → (A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) → (k ∈ (M...m) → B ∈ ℝ)))
42	41	r19.20dv2 1708	. . . . . . . . . . . . 13 ⊢ (m ∈ (ℤ≥ ‘M) → (∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → ∀k ∈ (M...m)B ∈ ℝ))
43	42	imp 350	. . . . . . . . . . . 12 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) → ∀k ∈ (M...m)B ∈ ℝ)
44		fsumreclt 6963	. . . . . . . . . . . 12 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...m)B ∈ ℝ) → Σk ∈ (M...m)B ∈ ℝ)
45	43, 44	syldan 467	. . . . . . . . . . 11 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) → Σk ∈ (M...m)B ∈ ℝ)
46	45	adantr 389	. . . . . . . . . 10 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) ⋀ Σk ∈ (M...m)A ≤ Σk ∈ (M...m)B) → Σk ∈ (M...m)B ∈ ℝ)
47		ra4csbela 2038	. . . . . . . . . . . 12 ⊢ (((m + 1) ∈ (M...(m + 1)) ⋀ ∀k ∈ (M...(m + 1))A ∈ ℝ) → [(m + 1) / k]A ∈ ℝ)
48		peano2uz 6387	. . . . . . . . . . . . 13 ⊢ (m ∈ (ℤ≥ ‘M) → (m + 1) ∈ (ℤ≥ ‘M))
49		eluzfz2t 6429	. . . . . . . . . . . . 13 ⊢ ((m + 1) ∈ (ℤ≥ ‘M) → (m + 1) ∈ (M...(m + 1)))
50	48, 49	syl 10	. . . . . . . . . . . 12 ⊢ (m ∈ (ℤ≥ ‘M) → (m + 1) ∈ (M...(m + 1)))
51	47, 50, 28	syl2an 454	. . . . . . . . . . 11 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) → [(m + 1) / k]A ∈ ℝ)
52	51	adantr 389	. . . . . . . . . 10 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) ⋀ Σk ∈ (M...m)A ≤ Σk ∈ (M...m)B) → [(m + 1) / k]A ∈ ℝ)
53	32, 39, 46, 52	syl3anc 857	. . . . . . . . 9 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) ⋀ Σk ∈ (M...m)A ≤ Σk ∈ (M...m)B) → (Σk ∈ (M...m)A ≤ Σk ∈ (M...m)B ↔ (Σk ∈ (M...m)A + [(m + 1) / k]A) ≤ (Σk ∈ (M...m)B + [(m + 1) / k]A)))
54	31, 53	mpbid 195	. . . . . . . 8 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) ⋀ Σk ∈ (M...m)A ≤ Σk ∈ (M...m)B) → (Σk ∈ (M...m)A + [(m + 1) / k]A) ≤ (Σk ∈ (M...m)B + [(m + 1) / k]A))
55	30, 54	eqbrtrd 2630	. . . . . . 7 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) ⋀ Σk ∈ (M...m)A ≤ Σk ∈ (M...m)B) → Σk ∈ (M...(m + 1))A ≤ (Σk ∈ (M...m)B + [(m + 1) / k]A))
56		ra4sbca 1994	. . . . . . . . . . . 12 ⊢ (((m + 1) ∈ (M...(m + 1)) ⋀ ∀k ∈ (M...(m + 1))A ≤ B) → [(m + 1) / k]A ≤ B)
57		oprex 3974	. . . . . . . . . . . . 13 ⊢ (m + 1) ∈ V
58		sbcbr12g 2658	. . . . . . . . . . . . 13 ⊢ ((m + 1) ∈ V → ([(m + 1) / k]A ≤ B ↔ [(m + 1) / k]A ≤ [(m + 1) / k]B))
59	57, 58	ax-mp 7	. . . . . . . . . . . 12 ⊢ ([(m + 1) / k]A ≤ B ↔ [(m + 1) / k]A ≤ [(m + 1) / k]B)
60	56, 59	sylib 198	. . . . . . . . . . 11 ⊢ (((m + 1) ∈ (M...(m + 1)) ⋀ ∀k ∈ (M...(m + 1))A ≤ B) → [(m + 1) / k]A ≤ [(m + 1) / k]B)
61	3	r19.20si 1703	. . . . . . . . . . 11 ⊢ (∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → ∀k ∈ (M...(m + 1))A ≤ B)
62	60, 50, 61	syl2an 454	. . . . . . . . . 10 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) → [(m + 1) / k]A ≤ [(m + 1) / k]B)
63		leadd2t 5608	. . . . . . . . . . 11 ⊢ (([(m + 1) / k]A ∈ ℝ ⋀ [(m + 1) / k]B ∈ ℝ ⋀ Σk ∈ (M...m)B ∈ ℝ) → ([(m + 1) / k]A ≤ [(m + 1) / k]B ↔ (Σk ∈ (M...m)B + [(m + 1) / k]A) ≤ (Σk ∈ (M...m)B + [(m + 1) / k]B)))
64		ra4csbela 2038	. . . . . . . . . . . 12 ⊢ (((m + 1) ∈ (M...(m + 1)) ⋀ ∀k ∈ (M...(m + 1))B ∈ ℝ) → [(m + 1) / k]B ∈ ℝ)
65	14	r19.20si 1703	. . . . . . . . . . . 12 ⊢ (∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → ∀k ∈ (M...(m + 1))B ∈ ℝ)
66	64, 50, 65	syl2an 454	. . . . . . . . . . 11 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) → [(m + 1) / k]B ∈ ℝ)
67	63, 51, 66, 45	syl3anc 857	. . . . . . . . . 10 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) → ([(m + 1) / k]A ≤ [(m + 1) / k]B ↔ (Σk ∈ (M...m)B + [(m + 1) / k]A) ≤ (Σk ∈ (M...m)B + [(m + 1) / k]B)))
68	62, 67	mpbid 195	. . . . . . . . 9 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) → (Σk ∈ (M...m)B + [(m + 1) / k]A) ≤ (Σk ∈ (M...m)B + [(m + 1) / k]B))
69		fsump1s 6959	. . . . . . . . . 10 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))B ∈ ℝ) → Σk ∈ (M...(m + 1))B = (Σk ∈ (M...m)B + [(m + 1) / k]B))
70	69, 65	sylan2 451	. . . . . . . . 9 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) → Σk ∈ (M...(m + 1))B = (Σk ∈ (M...m)B + [(m + 1) / k]B))
71	68, 70	breqtrrd 2636	. . . . . . . 8 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) → (Σk ∈ (M...m)B + [(m + 1) / k]A) ≤ Σk ∈ (M...(m + 1))B)
72	71	adantr 389	. . . . . . 7 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) ⋀ Σk ∈ (M...m)A ≤ Σk ∈ (M...m)B) → (Σk ∈ (M...m)B + [(m + 1) / k]A) ≤ Σk ∈ (M...(m + 1))B)
73		letrt 5506	. . . . . . . . 9 ⊢ ((Σk ∈ (M...(m + 1))A ∈ ℝ ⋀ (Σk ∈ (M...m)B + [(m + 1) / k]A) ∈ ℝ ⋀ Σk ∈ (M...(m + 1))B ∈ ℝ) → ((Σk ∈ (M...(m + 1))A ≤ (Σk ∈ (M...m)B + [(m + 1) / k]A) ⋀ (Σk ∈ (M...m)B + [(m + 1) / k]A) ≤ Σk ∈ (M...(m + 1))B) → Σk ∈ (M...(m + 1))A ≤ Σk ∈ (M...(m + 1))B))
74		fsumreclt 6963	. . . . . . . . . 10 ⊢ (((m + 1) ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))A ∈ ℝ) → Σk ∈ (M...(m + 1))A ∈ ℝ)
75	74, 48, 28	syl2an 454	. . . . . . . . 9 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) → Σk ∈ (M...(m + 1))A ∈ ℝ)
76		axaddrcl 5252	. . . . . . . . . 10 ⊢ ((Σk ∈ (M...m)B ∈ ℝ ⋀ [(m + 1) / k]A ∈ ℝ) → (Σk ∈ (M...m)B + [(m + 1) / k]A) ∈ ℝ)
77	76, 45, 51	sylanc 471	. . . . . . . . 9 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) → (Σk ∈ (M...m)B + [(m + 1) / k]A) ∈ ℝ)
78		fsumreclt 6963	. . . . . . . . . 10 ⊢ (((m + 1) ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))B ∈ ℝ) → Σk ∈ (M...(m + 1))B ∈ ℝ)
79	78, 48, 65	syl2an 454	. . . . . . . . 9 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) → Σk ∈ (M...(m + 1))B ∈ ℝ)
80	73, 75, 77, 79	syl3anc 857	. . . . . . . 8 ⊢ ((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) → ((Σk ∈ (M...(m + 1))A ≤ (Σk ∈ (M...m)B + [(m + 1) / k]A) ⋀ (Σk ∈ (M...m)B + [(m + 1) / k]A) ≤ Σk ∈ (M...(m + 1))B) → Σk ∈ (M...(m + 1))A ≤ Σk ∈ (M...(m + 1))B))
81	80	adantr 389	. . . . . . 7 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) ⋀ Σk ∈ (M...m)A ≤ Σk ∈ (M...m)B) → ((Σk ∈ (M...(m + 1))A ≤ (Σk ∈ (M...m)B + [(m + 1) / k]A) ⋀ (Σk ∈ (M...m)B + [(m + 1) / k]A) ≤ Σk ∈ (M...(m + 1))B) → Σk ∈ (M...(m + 1))A ≤ Σk ∈ (M...(m + 1))B))
82	55, 72, 81	mp2and 702	. . . . . 6 ⊢ (((m ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) ⋀ Σk ∈ (M...m)A ≤ Σk ∈ (M...m)B) → Σk ∈ (M...(m + 1))A ≤ Σk ∈ (M...(m + 1))B)
83	82	exp31 376	. . . . 5 ⊢ (m ∈ (ℤ≥ ‘M) → (∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → (Σk ∈ (M...m)A ≤ Σk ∈ (M...m)B → Σk ∈ (M...(m + 1))A ≤ Σk ∈ (M...(m + 1))B)))
84	83	a2d 13	. . . 4 ⊢ (m ∈ (ℤ≥ ‘M) → ((∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → Σk ∈ (M...m)A ≤ Σk ∈ (M...m)B) → (∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → Σk ∈ (M...(m + 1))A ≤ Σk ∈ (M...(m + 1))B)))
85	26, 84	syld 27	. . 3 ⊢ (m ∈ (ℤ≥ ‘M) → ((∀k ∈ (M...m)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → Σk ∈ (M...m)A ≤ Σk ∈ (M...m)B) → (∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → Σk ∈ (M...(m + 1))A ≤ Σk ∈ (M...(m + 1))B)))
86		opreq2 3960	. . . . 5 ⊢ (j = M → (M...j) = (M...M))
87	86	raleq1d 1786	. . . 4 ⊢ (j = M → (∀k ∈ (M...j)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) ↔ ∀k ∈ (M...M)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)))
88	86	sumeq1d 6936	. . . . 5 ⊢ (j = M → Σk ∈ (M...j)A = Σk ∈ (M...M)A)
89	86	sumeq1d 6936	. . . . 5 ⊢ (j = M → Σk ∈ (M...j)B = Σk ∈ (M...M)B)
90	88, 89	breq12d 2626	. . . 4 ⊢ (j = M → (Σk ∈ (M...j)A ≤ Σk ∈ (M...j)B ↔ Σk ∈ (M...M)A ≤ Σk ∈ (M...M)B))
91	87, 90	imbi12d 625	. . 3 ⊢ (j = M → ((∀k ∈ (M...j)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → Σk ∈ (M...j)A ≤ Σk ∈ (M...j)B) ↔ (∀k ∈ (M...M)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → Σk ∈ (M...M)A ≤ Σk ∈ (M...M)B)))
92		opreq2 3960	. . . . 5 ⊢ (j = m → (M...j) = (M...m))
93	92	raleq1d 1786	. . . 4 ⊢ (j = m → (∀k ∈ (M...j)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) ↔ ∀k ∈ (M...m)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)))
94	92	sumeq1d 6936	. . . . 5 ⊢ (j = m → Σk ∈ (M...j)A = Σk ∈ (M...m)A)
95	92	sumeq1d 6936	. . . . 5 ⊢ (j = m → Σk ∈ (M...j)B = Σk ∈ (M...m)B)
96	94, 95	breq12d 2626	. . . 4 ⊢ (j = m → (Σk ∈ (M...j)A ≤ Σk ∈ (M...j)B ↔ Σk ∈ (M...m)A ≤ Σk ∈ (M...m)B))
97	93, 96	imbi12d 625	. . 3 ⊢ (j = m → ((∀k ∈ (M...j)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → Σk ∈ (M...j)A ≤ Σk ∈ (M...j)B) ↔ (∀k ∈ (M...m)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → Σk ∈ (M...m)A ≤ Σk ∈ (M...m)B)))
98		opreq2 3960	. . . . 5 ⊢ (j = (m + 1) → (M...j) = (M...(m + 1)))
99	98	raleq1d 1786	. . . 4 ⊢ (j = (m + 1) → (∀k ∈ (M...j)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) ↔ ∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)))
100	98	sumeq1d 6936	. . . . 5 ⊢ (j = (m + 1) → Σk ∈ (M...j)A = Σk ∈ (M...(m + 1))A)
101	98	sumeq1d 6936	. . . . 5 ⊢ (j = (m + 1) → Σk ∈ (M...j)B = Σk ∈ (M...(m + 1))B)
102	100, 101	breq12d 2626	. . . 4 ⊢ (j = (m + 1) → (Σk ∈ (M...j)A ≤ Σk ∈ (M...j)B ↔ Σk ∈ (M...(m + 1))A ≤ Σk ∈ (M...(m + 1))B))
103	99, 102	imbi12d 625	. . 3 ⊢ (j = (m + 1) → ((∀k ∈ (M...j)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → Σk ∈ (M...j)A ≤ Σk ∈ (M...j)B) ↔ (∀k ∈ (M...(m + 1))(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → Σk ∈ (M...(m + 1))A ≤ Σk ∈ (M...(m + 1))B)))
104		opreq2 3960	. . . . 5 ⊢ (j = N → (M...j) = (M...N))
105	104	raleq1d 1786	. . . 4 ⊢ (j = N → (∀k ∈ (M...j)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) ↔ ∀k ∈ (M...N)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)))
106	104	sumeq1d 6936	. . . . 5 ⊢ (j = N → Σk ∈ (M...j)A = Σk ∈ (M...N)A)
107	104	sumeq1d 6936	. . . . 5 ⊢ (j = N → Σk ∈ (M...j)B = Σk ∈ (M...N)B)
108	106, 107	breq12d 2626	. . . 4 ⊢ (j = N → (Σk ∈ (M...j)A ≤ Σk ∈ (M...j)B ↔ Σk ∈ (M...N)A ≤ Σk ∈ (M...N)B))
109	105, 108	imbi12d 625	. . 3 ⊢ (j = N → ((∀k ∈ (M...j)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → Σk ∈ (M...j)A ≤ Σk ∈ (M...j)B) ↔ (∀k ∈ (M...N)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → Σk ∈ (M...N)A ≤ Σk ∈ (M...N)B)))
110	18, 85, 91, 97, 103, 109	uzind4ALT 6391	. 2 ⊢ (N ∈ (ℤ≥ ‘M) → (∀k ∈ (M...N)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B) → Σk ∈ (M...N)A ≤ Σk ∈ (M...N)B))
111	110	imp 350	1 ⊢ ((N ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...N)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B)) → Σk ∈ (M...N)A ≤ Σk ∈ (M...N)B)

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223   ⋀ w3a 774   = wceq 954   ∈ wcel 956  [wsbc 1168  ∀wral 1642  Vcvv 1807  [csb 1997   ⊆ wss 2043   class class class wbr 2614   ‘cfv 3177  (class class class)co 3954  ℝcr 5213  1c1 5215   + caddc 5217   ≤ cle 5275  ℤcz 5278  ℤ_≥cuz 6357  ...cfz 6407  Σcsu 6925

This theorem is referenced by:  fsumcmp0 6987  serzcmp 7000  efaddlem16 7303  efaddlem19 7306

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-rep 2688  ax-sep 2698  ax-nul 2705  ax-pow 2737  ax-pr 2774  ax-un 2861  ax-inf2 4605

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-nel 1585  df-ral 1646  df-rex 1647  df-reu 1648  df-rab 1649  df-v 1808  df-sbc 1938  df-csb 1998  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-pss 2051  df-nul 2277  df-if 2358  df-pw 2398  df-sn 2408  df-pr 2409  df-tp 2411  df-op 2412  df-uni 2499  df-int 2529  df-iun 2563  df-br 2615  df-opab 2662  df-tr 2676  df-eprel 2827  df-id 2830  df-po 2835  df-so 2845  df-fr 2912  df-we 2929  df-ord 2946  df-on 2947  df-lim 2948  df-suc 2949  df-om 3127  df-xp 3179  df-rel 3180  df-cnv 3181  df-co 3182  df-dm 3183  df-rn 3184  df-res 3185  df-ima 3186  df-fun 3187  df-fn 3188  df-f 3189  df-f1 3190  df-fo 3191  df-f1o 3192  df-fv 3193  df-rdg 3923  df-opr 3956  df-oprab 3957  df-1st 4069  df-2nd