HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem fsumcmp 7163
Description: If all of the terms of finite sums compare, so do the sums.
Assertion
Ref Expression
fsumcmp |- ((N e. (ZZ>` M) /\ A.k e. (M...N)(A e. RR /\ B e. RR /\ A <_ B)) -> sum_k e. (M...N)A <_ sum_k e. (M...N)B)
Distinct variable groups:   k,M   k,N

Proof of Theorem fsumcmp
StepHypRef Expression
1 ra4sbca 2040 . . . . . . 7 |- ((M e. (M...M) /\ A.k e. (M...M)A <_ B) -> [M / k]A <_ B)
2 elfz3 6551 . . . . . . 7 |- (M e. ZZ -> M e. (M...M))
3 3simp3 793 . . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A <_ B) -> A <_ B)
43r19.20si 1744 . . . . . . 7 |- (A.k e. (M...M)(A e. RR /\ B e. RR /\ A <_ B) -> A.k e. (M...M)A <_ B)
51, 2, 4syl2an 456 . . . . . 6 |- ((M e. ZZ /\ A.k e. (M...M)(A e. RR /\ B e. RR /\ A <_ B)) -> [M / k]A <_ B)
6 sbcbr12g 2714 . . . . . . 7 |- (M e. ZZ -> ([M / k]A <_ B <-> [_M / k]_A <_ [_M / k]_B))
76adantr 389 . . . . . 6 |- ((M e. ZZ /\ A.k e. (M...M)(A e. RR /\ B e. RR /\ A <_ B)) -> ([M / k]A <_ B <-> [_M / k]_A <_ [_M / k]_B))
85, 7mpbid 193 . . . . 5 |- ((M e. ZZ /\ A.k e. (M...M)(A e. RR /\ B e. RR /\ A <_ B)) -> [_M / k]_A <_ [_M / k]_B)
9 fsum1s 7132 . . . . . 6 |- ((M e. ZZ /\ A.k e. (M...M)A e. RR) -> sum_k e. (M...M)A = [_M / k]_A)
10 3simp1 791 . . . . . . 7 |- ((A e. RR /\ B e. RR /\ A <_ B) -> A e. RR)
1110r19.20si 1744 . . . . . 6 |- (A.k e. (M...M)(A e. RR /\ B e. RR /\ A <_ B) -> A.k e. (M...M)A e. RR)
129, 11sylan2 453 . . . . 5 |- ((M e. ZZ /\ A.k e. (M...M)(A e. RR /\ B e. RR /\ A <_ B)) -> sum_k e. (M...M)A = [_M / k]_A)
13 fsum1s 7132 . . . . . 6 |- ((M e. ZZ /\ A.k e. (M...M)B e. RR) -> sum_k e. (M...M)B = [_M / k]_B)
14 3simp2 792 . . . . . . 7 |- ((A e. RR /\ B e. RR /\ A <_ B) -> B e. RR)
1514r19.20si 1744 . . . . . 6 |- (A.k e. (M...M)(A e. RR /\ B e. RR /\ A <_ B) -> A.k e. (M...M)B e. RR)
1613, 15sylan2 453 . . . . 5 |- ((M e. ZZ /\ A.k e. (M...M)(A e. RR /\ B e. RR /\ A <_ B)) -> sum_k e. (M...M)B = [_M / k]_B)
178, 12, 163brtr4d 2695 . . . 4 |- ((M e. ZZ /\ A.k e. (M...M)(A e. RR /\ B e. RR /\ A <_ B)) -> sum_k e. (M...M)A <_ sum_k e. (M...M)B)
1817ex 371 . . 3 |- (M e. ZZ -> (A.k e. (M...M)(A e. RR /\ B e. RR /\ A <_ B) -> sum_k e. (M...M)A <_ sum_k e. (M...M)B))
19 fzssp1 6566 . . . . . . . . 9 |- ((M e. ZZ /\ m e. ZZ) -> (M...m) (_ (M...(m + 1)))
20 eluzel2 6484 . . . . . . . . 9 |- (m e. (ZZ>` M) -> M e. ZZ)
21 eluzelz 6483 . . . . . . . . 9 |- (m e. (ZZ>` M) -> m e. ZZ)
2219, 20, 21sylanc 473 . . . . . . . 8 |- (m e. (ZZ>` M) -> (M...m) (_ (M...(m + 1)))
2322sseld 2111 . . . . . . 7 |- (m e. (ZZ>` M) -> (k e. (M...m) -> k e. (M...(m + 1))))
2423imim1d 28 . . . . . 6 |- (m e. (ZZ>` M) -> ((k e. (M...(m + 1)) -> (A e. RR /\ B e. RR /\ A <_ B)) -> (k e. (M...m) -> (A e. RR /\ B e. RR /\ A <_ B))))
2524r19.20dv2 1749 . . . . 5 |- (m e. (ZZ>` M) -> (A.k e. (M...(m + 1))(A e. RR /\ B e. RR /\ A <_ B) -> A.k e. (M...m)(A e. RR /\ B e. RR /\ A <_ B)))
2625imim1d 28 . . . 4 |- (m e. (ZZ>` M) -> ((A.k e. (M...m)(A e. RR /\ B e. RR /\ A <_ B) -> sum_k e. (M...m)A <_ sum_k e. (M...m)B) -> (A.k e. (M...(m + 1))(A e. RR /\ B e. RR /\ A <_ B) -> sum_k e. (M...m)A <_ sum_k e. (M...m)B)))
27 fsump1s 7136 . . . . . . . . . 10 |- ((m e. (ZZ>` M) /\ A.k e. (M...(m + 1))A e. RR) -> sum_k e. (M...(m + 1))A = (sum_k e. (M...m)A + [_(m + 1) / k]_A))
2810r19.20si 1744 . . . . . . . . . 10 |- (A.k e. (M...(m + 1))(A e. RR /\ B e. RR /\ A <_ B) -> A.k e. (M...(m + 1))A e. RR)
2927, 28sylan2 453 . . . . . . . . 9 |- ((m e. (ZZ>` M) /\ A.k e. (M...(m + 1))(A e. RR /\ B e. RR /\ A <_ B)) -> sum_k e. (M...(m + 1))A = (sum_k e. (M...m)A + [_(m + 1) / k]_A))
3029adantr 389 . . . . . . . 8 |- (((m e. (ZZ>` M) /\ A.k e. (M...(m + 1))(A e. RR /\ B e. RR /\ A <_ B)) /\ sum_k e. (M...m)A <_ sum_k e. (M...m)B) -> sum_k e. (M...(m + 1))A = (sum_k e. (M...m)A + [_(m + 1) / k]_A))
31 pm3.27 321 . . . . . . . . 9 |- (((m e. (ZZ>` M) /\ A.k e. (M...(m + 1))(A e. RR /\ B e. RR /\ A <_ B)) /\ sum_k e. (M...m)A <_ sum_k e. (M...m)B) -> sum_k e. (M...m)A <_ sum_k e. (M...m)B)
32 leadd1 5714 . . . . . . . . . 10 |- ((sum_k e. (M...m)A e. RR /\ sum_k e. (M...m)B e. RR /\ [_(m + 1) / k]_A e. RR) -> (sum_k e. (M...m)A <_ sum_k e. (M...m)B <-> (sum_k e. (M...m)A + [_(m + 1) / k]_A) <_ (sum_k e. (M...m)B + [_(m + 1) / k]_A)))
3310a1i 8 . . . . . . . . . . . . . . 15 |- (m e. (ZZ>` M) -> ((A e. RR /\ B e. RR /\ A <_ B) -> A e. RR))
3423, 33imim12d 29 . . . . . . . . . . . . . 14 |- (m e. (ZZ>` M) -> ((k e. (M...(m + 1)) -> (A e. RR /\ B e. RR /\ A <_ B)) -> (k e. (M...m) -> A e. RR)))
3534r19.20dv2 1749 . . . . . . . . . . . . 13 |- (m e. (ZZ>` M) -> (A.k e. (M...(m + 1))(A e. RR /\ B e. RR /\ A <_ B) -> A.k e. (M...m)A e. RR))
3635imp 348 . . . . . . . . . . . 12 |- ((m e. (ZZ>` M) /\ A.k e. (M...(m + 1))(A e. RR /\ B e. RR /\ A <_ B)) -> A.k e. (M...m)A e. RR)
37 fsumrecl 7140 . . . . . . . . . . . 12 |- ((m e. (ZZ>` M) /\ A.k e. (M...m)A e. RR) -> sum_k e. (M...m)A e. RR)
3836, 37syldan 469 . . . . . . . . . . 11 |- ((m e. (ZZ>` M) /\ A.k e. (M...(m + 1))(A e. RR /\ B e. RR /\ A <_ B)) -> sum_k e. (M...m)A e. RR)
3938adantr 389 . . . . . . . . . 10 |- (((m e. (ZZ>` M) /\ A.k e. (M...(m + 1))(A e. RR /\ B e. RR /\ A <_ B)) /\ sum_k e. (M...m)A <_ sum_k e. (M...m)B) -> sum_k e. (M...m)A e. RR)
4014a1i 8 . . . . . . . . . . . . . . 15 |- (m e. (ZZ>` M) -> ((A e. RR /\ B e. RR /\ A <_ B) -> B e. RR))
4123, 40imim12d 29 . . . . . . . . . . . . . 14 |- (m e. (ZZ>` M) -> ((k e. (M...(m + 1)) -> (A e. RR /\ B e. RR /\ A <_ B)) -> (k e. (M...m) -> B e. RR)))
4241r19.20dv2 1749 . . . . . . . . . . . . 13 |- (m e. (ZZ>` M) -> (A.k e. (M...(m + 1))(A e. RR /\ B e. RR /\ A <_ B) -> A.k e. (M...m)B e. RR))
4342imp 348 . . . . . . . . . . . 12 |- ((m e. (ZZ>` M) /\ A.k e. (M...(m + 1))(A e. RR /\ B e. RR /\ A <_ B)) -> A.k e. (M...m)B e. RR)
44 fsumrecl 7140 . . . . . . . . . . . 12 |- ((m e. (ZZ>` M) /\ A.k e. (M...