Theorem cvgcmp3cetlem1 7132

Description: Lemma for cvgcmp3cet 7134.

Hypotheses

Ref	Expression
cvgcmp3ce.1	|- A e. V
cvgcmp3ce.2	|- B e. NN
cvgcmp3ce.3	|- F:NN-->RR
cvgcmp3ce.4	|- (x e. NN -> 0 <_ (F` x))
cvgcmp3ce.5	|- ( + seq1 F) ~~> A
cvgcmp3cetlem1.6	|- (ph <-> ((C e. RR /\ 0 <_ C) /\ (G:NN-->CC /\ A.x e. NN (B < x -> (abs` (G` x)) <_ (C x. (F` x))))))

Assertion

Ref	Expression
cvgcmp3cetlem1	|- (ph -> E.y( + seq1 G) ~~> y)

Distinct variable groups:   x,B   x,F   x,y,G   x,C   ph,y

Proof of Theorem cvgcmp3cetlem1

Step	Hyp	Ref	Expression
1		opreq2 3960	. . . 4 |- (G = if(ph, G, (NN X. {0})) -> ( + seq1 G) = ( + seq1 if(ph, G, (NN X. {0}))))
2	1	breq1d 2624	. . 3 |- (G = if(ph, G, (NN X. {0})) -> (( + seq1 G) ~~> y <-> ( + seq1 if(ph, G, (NN X. {0}))) ~~> y))
3	2	exbidv 1277	. 2 |- (G = if(ph, G, (NN X. {0})) -> (E.y( + seq1 G) ~~> y <-> E.y( + seq1 if(ph, G, (NN X. {0}))) ~~> y))
4		cvgcmp3ce.1	. . 3 |- A e. V
5		cvgcmp3ce.2	. . 3 |- B e. NN
6		cvgcmp3ce.3	. . 3 |- F:NN-->RR
7		fveq2 3715	. . . . 5 |- (x = z -> (F` x) = (F` z))
8	7	breq2d 2625	. . . 4 |- (x = z -> (0 <_ (F` x) <-> 0 <_ (F` z)))
9		cvgcmp3ce.4	. . . 4 |- (x e. NN -> 0 <_ (F` x))
10	8, 9	vtoclga 1848	. . 3 |- (z e. NN -> 0 <_ (F` z))
11		cvgcmp3ce.5	. . 3 |- ( + seq1 F) ~~> A
12		feq1 3612	. . . . . . . . 9 |- (G = if(ph, G, (NN X. {0})) -> (G:NN-->CC <-> if(ph, G, (NN X. {0})):NN-->CC))
13		fveq1 3714	. . . . . . . . . . . . 13 |- (G = if(ph, G, (NN X. {0})) -> (G` z) = (if(ph, G, (NN X. {0}))` z))
14	13	fveq2d 3719	. . . . . . . . . . . 12 |- (G = if(ph, G, (NN X. {0})) -> (abs` (G` z)) = (abs` (if(ph, G, (NN X. {0}))` z)))
15	14	breq1d 2624	. . . . . . . . . . 11 |- (G = if(ph, G, (NN X. {0})) -> ((abs` (G` z)) <_ (C x. (F` z)) <-> (abs` (if(ph, G, (NN X. {0}))` z)) <_ (C x. (F` z))))
16	15	imbi2d 611	. . . . . . . . . 10 |- (G = if(ph, G, (NN X. {0})) -> ((B < z -> (abs` (G` z)) <_ (C x. (F` z))) <-> (B < z -> (abs` (if(ph, G, (NN X. {0}))` z)) <_ (C x. (F` z)))))
17	16	ralbidv 1660	. . . . . . . . 9 |- (G = if(ph, G, (NN X. {0})) -> (A.z e. NN (B < z -> (abs` (G` z)) <_ (C x. (F` z))) <-> A.z e. NN (B < z -> (abs` (if(ph, G, (NN X. {0}))` z)) <_ (C x. (F` z)))))
18	12, 17	anbi12d 627	. . . . . . . 8 |- (G = if(ph, G, (NN X. {0})) -> ((G:NN-->CC /\ A.z e. NN (B < z -> (abs` (G` z)) <_ (C x. (F` z)))) <-> (if(ph, G, (NN X. {0})):NN-->CC /\ A.z e. NN (B < z -> (abs` (if(ph, G, (NN X. {0}))` z)) <_ (C x. (F` z))))))
19	18	anbi2d 615	. . . . . . 7 |- (G = if(ph, G, (NN X. {0})) -> (((C e. RR /\ 0 <_ C) /\ (G:NN-->CC /\ A.z e. NN (B < z -> (abs` (G` z)) <_ (C x. (F` z))))) <-> ((C e. RR /\ 0 <_ C) /\ (if(ph, G, (NN X. {0})):NN-->CC /\ A.z e. NN (B < z -> (abs` (if(ph, G, (NN X. {0}))` z)) <_ (C x. (F` z)))))))
20		cvgcmp3cetlem1.6	. . . . . . . 8 |- (ph <-> ((C e. RR /\ 0 <_ C) /\ (G:NN-->CC /\ A.x e. NN (B < x -> (abs` (G` x)) <_ (C x. (F` x))))))
21		breq2 2618	. . . . . . . . . . . 12 |- (x = z -> (B < x <-> B < z))
22		fveq2 3715	. . . . . . . . . . . . . 14 |- (x = z -> (G` x) = (G` z))
23	22	fveq2d 3719	. . . . . . . . . . . . 13 |- (x = z -> (abs` (G` x)) = (abs` (G` z)))
24	7	opreq2d 3967	. . . . . . . . . . . . 13 |- (x = z -> (C x. (F` x)) = (C x. (F` z)))
25	23, 24	breq12d 2626	. . . . . . . . . . . 12 |- (x = z -> ((abs` (G` x)) <_ (C x. (F` x)) <-> (abs` (G` z)) <_ (C x. (F` z))))
26	21, 25	imbi12d 625	. . . . . . . . . . 11 |- (x = z -> ((B < x -> (abs` (G` x)) <_ (C x. (F` x))) <-> (B < z -> (abs` (G` z)) <_ (C x. (F` z)))))
27	26	cbvralv 1796	. . . . . . . . . 10 |- (A.x e. NN (B < x -> (abs` (G` x)) <_ (C x. (F` x))) <-> A.z e. NN (B < z -> (abs` (G` z)) <_ (C x. (F` z))))
28	27	anbi2i 480	. . . . . . . . 9 |- ((G:NN-->CC /\ A.x e. NN (B < x -> (abs` (G` x)) <_ (C x. (F` x)))) <-> (G:NN-->CC /\ A.z e. NN (B < z -> (abs` (G` z)) <_ (C x. (F` z)))))
29	28	anbi2i 480	. . . . . . . 8 |- (((C e. RR /\ 0 <_ C) /\ (G:NN-->CC /\ A.x e. NN (B < x -> (abs` (G` x)) <_ (C x. (F` x))))) <-> ((C e. RR /\ 0 <_ C) /\ (G:NN-->CC /\ A.z e. NN (B < z -> (abs` (G` z)) <_ (C x. (F` z))))))
30	20, 29	bitr 173	. . . . . . 7 |- (ph <-> ((C e. RR /\ 0 <_ C) /\ (G:NN-->CC /\ A.z e. NN (B < z -> (abs` (G` z)) <_ (C x. (F` z))))))
31	19, 30	syl5bb 531	. . . . . 6 |- (G = if(ph, G, (NN X. {0})) -> (ph <-> ((C e. RR /\ 0 <_ C) /\ (if(ph, G, (NN X. {0})):NN-->CC /\ A.z e. NN (B < z -> (abs` (if(ph, G, (NN X. {0}))` z)) <_ (C x. (F` z)))))))
32		eleq1 1531	. . . . . . . 8 |- (C = if(ph, C, 0) -> (C e. RR <-> if(ph, C, 0) e. RR))
33		breq2 2618	. . . . . . . 8 |- (C = if(ph, C, 0) -> (0 <_ C <-> 0 <_ if(ph, C, 0)))
34	32, 33	anbi12d 627	. . . . . . 7 |- (C = if(ph, C, 0) -> ((C e. RR /\ 0 <_ C) <-> (if(ph, C, 0) e. RR /\ 0 <_ if(ph, C, 0))))
35		opreq1 3959	. . . . . . . . . . 11 |- (C = if(ph, C, 0) -> (C x. (F` z)) = (if(ph, C, 0) x. (F` z)))
36	35	breq2d 2625	. . . . . . . . . 10 |- (C = if(ph, C, 0) -> ((abs` (if(ph, G, (NN X. {0}))` z)) <_ (C x. (F` z)) <-> (abs` (if(ph, G, (NN X. {0}))` z)) <_ (if(ph, C, 0) x. (F` z))))
37	36	imbi2d 611	. . . . . . . . 9 |- (C = if(ph, C, 0) -> ((B < z -> (abs` (if(ph, G, (NN X. {0}))` z)) <_ (C x. (F` z))) <-> (B < z -> (abs` (if(ph, G, (NN X. {0}))` z)) <_ (if(ph, C, 0) x. (F` z)))))
38	37	ralbidv 1660	. . . . . . . 8 |- (C = if(ph, C, 0) -> (A.z e. NN (B < z -> (abs` (if(ph, G, (NN X. {0}))` z)) <_ (C x. (F` z))) <-> A.z e. NN (B < z -> (abs` (if(ph, G, (NN X. {0}))` z)) <_ (if(ph, C,