Theorem cauimi 8565

Description: The imaginary part of a complex Caucy sequence is a Cauchy sequence.

Hypotheses

Ref	Expression
cauim.1	|- F:NN-->CC
cauim.2	|- A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < z))
cauim.3	|- G Fn NN
cauim.4	|- (x e. NN -> (G` x) = (Im` (F` x)))

Assertion

Ref	Expression
cauimi	|- A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((G` y) - (G` w))) < z))

Distinct variable groups:   y,z,w   x,y,w   x,F   x,G

Proof of Theorem cauimi

Step	Hyp	Ref	Expression
1		cauim.2	. 2 |- A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < z))
2		fveq2 4765	. . . . . . . . . . . . . . . . 17 |- (x = y -> (G` x) = (G` y))
3		fveq2 4765	. . . . . . . . . . . . . . . . . 18 |- (x = y -> (F` x) = (F` y))
4	3	fveq2d 4769	. . . . . . . . . . . . . . . . 17 |- (x = y -> (Im` (F` x)) = (Im` (F` y)))
5	2, 4	eqeq12d 2155	. . . . . . . . . . . . . . . 16 |- (x = y -> ((G` x) = (Im` (F` x)) <-> (G` y) = (Im` (F` y))))
6		cauim.4	. . . . . . . . . . . . . . . 16 |- (x e. NN -> (G` x) = (Im` (F` x)))
7	5, 6	vtoclga 2593	. . . . . . . . . . . . . . 15 |- (y e. NN -> (G` y) = (Im` (F` y)))
8		fveq2 4765	. . . . . . . . . . . . . . . . 17 |- (x = w -> (G` x) = (G` w))
9		fveq2 4765	. . . . . . . . . . . . . . . . . 18 |- (x = w -> (F` x) = (F` w))
10	9	fveq2d 4769	. . . . . . . . . . . . . . . . 17 |- (x = w -> (Im` (F` x)) = (Im` (F` w)))
11	8, 10	eqeq12d 2155	. . . . . . . . . . . . . . . 16 |- (x = w -> ((G` x) = (Im` (F` x)) <-> (G` w) = (Im` (F` w))))
12	11, 6	vtoclga 2593	. . . . . . . . . . . . . . 15 |- (w e. NN -> (G` w) = (Im` (F` w)))
13	7, 12	opreqan12d 4997	. . . . . . . . . . . . . 14 |- ((y e. NN /\ w e. NN) -> ((G` y) - (G` w)) = ((Im` (F` y)) - (Im` (F` w))))
14		cauim.1	. . . . . . . . . . . . . . . 16 |- F:NN-->CC
15	14	ffvelrni 4878	. . . . . . . . . . . . . . 15 |- (y e. NN -> (F` y) e. CC)
16	14	ffvelrni 4878	. . . . . . . . . . . . . . 15 |- (w e. NN -> (F` w) e. CC)
17		imsub 8443	. . . . . . . . . . . . . . 15 |- (((F` y) e. CC /\ (F` w) e. CC) -> (Im` ((F` y) - (F` w))) = ((Im` (F` y)) - (Im` (F` w))))
18	15, 16, 17	syl2an 603	. . . . . . . . . . . . . 14 |- ((y e. NN /\ w e. NN) -> (Im` ((F` y) - (F` w))) = ((Im` (F` y)) - (Im` (F` w))))
19	13, 18	eqtr4d 2176	. . . . . . . . . . . . 13 |- ((y e. NN /\ w e. NN) -> ((G` y) - (G` w)) = (Im` ((F` y) - (F` w))))
20	19	fveq2d 4769	. . . . . . . . . . . 12 |- ((y e. NN /\ w e. NN) -> (abs` ((G` y) - (G` w))) = (abs` (Im` ((F` y) - (F` w)))))
21		subcl 7020	. . . . . . . . . . . . . 14 |- (((F` y) e. CC /\ (F` w) e. CC) -> ((F` y) - (F` w)) e. CC)
22	15, 16, 21	syl2an 603	. . . . . . . . . . . . 13 |- ((y e. NN /\ w e. NN) -> ((F` y) - (F` w)) e. CC)
23		absimle 8506	. . . . . . . . . . . . 13 |- (((F` y) - (F` w)) e. CC -> (abs` (Im` ((F` y) - (F` w)))) <_ (abs` ((F` y) - (F` w))))
24	22, 23	syl 13	. . . . . . . . . . . 12 |- ((y e. NN /\ w e. NN) -> (abs` (Im` ((F` y) - (F` w)))) <_ (abs` ((F` y) - (F` w))))
25	20, 24	eqbrtrd 3527	. . . . . . . . . . 11 |- ((y e. NN /\ w e. NN) -> (abs` ((G` y) - (G` w))) <_ (abs` ((F` y) - (F` w))))
26	25	3adant3 1140	. . . . . . . . . 10 |- ((y e. NN /\ w e. NN /\ z e. RR) -> (abs` ((G` y) - (G` w))) <_ (abs` ((F` y) - (F` w))))
27		ffnfv 4893	. . . . . . . . . . . . . . . . 17 |- (G:NN-->RR <-> (G Fn NN /\ A.x e. NN (G` x) e. RR))
28		cauim.3	. . . . . . . . . . . . . . . . 17 |- G Fn NN
29	14	ffvelrni 4878	. . . . . . . . . . . . . . . . . . . 20 |- (x e. NN -> (F` x) e. CC)
30		imcl 8392	. . . . . . . . . . . . . . . . . . . 20 |- ((F` x) e. CC -> (Im` (F` x)) e. RR)
31	29, 30	syl 13	. . . . . . . . . . . . . . . . . . 19 |- (x e. NN -> (Im` (F` x)) e. RR)
32	6, 31	eqeltrd 2218	. . . . . . . . . . . . . . . . . 18 |- (x e. NN -> (G` x) e. RR)
33	32	rgen 2410	. . . . . . . . . . . . . . . . 17 |- A.x e. NN (G` x) e. RR
34	27, 28, 33	mpbir2an 1033	. . . . . . . . . . . . . . . 16 |- G:NN-->RR
35	34	ffvelrni 4878	. . . . . . . . . . . . . . 15 |- (y e. NN -> (G` y) e. RR)
36	34	ffvelrni 4878	. . . . . . . . . . . . . . 15 |- (w e. NN -> (G` w) e. RR)
37		resubcl 7078	. . . . . . . . . . . . . . 15 |- (((G` y) e. RR /\ (G` w) e. RR) -> ((G` y) - (G` w)) e. RR)
38	35, 36, 37	syl2an 603	. . . . . . . . . . . . . 14 |- ((y e. NN /\ w e. NN) -> ((G` y) - (G` w)) e. RR)
39	38	recnd 6819	. . . . . . . . . . . . 13 |- ((y e. NN /\ w e. NN) -> ((G` y) - (G` w)) e. CC)
40		abscl 8468	. . . . . . . . . . . . 13 |- (((G` y) - (G` w)) e. CC -> (abs` ((G` y) - (G` w))) e. RR)
41	39, 40	syl 13	. . . . . . . . . . . 12 |- ((y e. NN /\ w e. NN) -> (abs` ((G` y) - (G` w))) e. RR)
42	41	3adant3 1140	. . . . . . . . . . 11 |- ((y e. NN /\ w e. NN /\ z e. RR) -> (abs` ((G` y) - (G` w))) e. RR)
43		abscl 8468	. . . . . . . . . . . . 13 |- (((F` y) - (F` w)) e. CC -> (abs` ((F` y) - (F` w))) e. RR)
44	22, 43	syl 13	. . . . . . . . . . . 12 |- ((y e. NN /\ w e. NN) -> (abs` ((F` y) - (F` w))) e. RR)
45	44	3adant3 1140	. . . . . . . . . . 11 |- ((y e. NN /\ w e. NN /\ z e. RR) -> (abs` ((F` y) - (F` w))) e. RR)
46		simp3 1122	. . . . . . . . . . 11 |- ((y e. NN /\ w e. NN /\ z e. RR) -> z e. RR)
47		lelttr 6882	. . . . . . . . . . 11 |- (((abs` ((G` y) - (G` w))) e. RR /\ (abs` ((F` y) - (F` w))) e. RR /\ z e. RR) -> (((abs` ((G` y) - (G` w))) <_ (abs` ((F` y) - (F` w))) /\ (abs` ((F` y) - (F` w))) < z) -> (abs` ((G` y) - (G` w))) < z))
48	42, 45, 46, 47	syl111anc 1349	. . . . . . . . . 10 |- ((y e. NN /\ w e. NN /\ z e. RR) -> (((abs` ((G` y) - (G` w))) <_ (abs` ((F` y) - (F` w))) /\ (abs` ((F` y) - (F` w))) < z) -> (abs` ((G` y) - (G` w))) < z))
49	26, 48	mpand 684	. . . . . . . . 9 |- ((y e. NN /\ w e. NN /\ z e. RR) -> ((abs` ((F` y) - (F` w))) < z -> (abs` ((G` y) - (G` w))) < z))
50	49	3com13 1322	. . . . . . . 8 |- ((z e. RR /\ w e. NN /\ y e. NN) -> ((abs` ((F` y) - (F` w))) < z -> (abs` ((G` y) - (G` w))) < z))
51	50	3expa 1317	. . . . . . 7 |- (((z e. RR /\ w e. NN) /\ y e. NN) -> ((abs` ((F` y) - (F` w))) < z -> (abs` ((G` y) - (G` w))) < z))
52	51	imim2d 28	. . . . . 6 |- (((z e. RR /\ w e. NN) /\ y e. NN) -> ((w < y -> (abs` ((F` y) - (F` w))) < z) -> (w < y -> (abs` ((G` y) - (G` w))) < z)))
53	52	ralimdva 2421	. . . . 5 |- ((z e. RR /\ w e. NN) -> (A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < z) -> A.y e. NN (w < y -> (abs` ((G` y) - (G` w))) < z)))
54	53	reximdva 2453	. . . 4 |- (z e. RR -> (E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < z) -> E.w e. NN A.y e. NN (w < y -> (abs` ((G` y) - (G` w))) < z)))
55	54	imim2d 28	. . 3 |- (z e. RR -> ((0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < z)) -> (0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((G` y) - (G` w))) < z))))
56	55	ralimia 2416	. 2 |- (A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < z)) -> A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((G` y) - (G` w))) < z)))
57	1, 56	ax-mp 7	1 |- A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((G` y) - (G` w))) < z))

Syntax hints:   -> wi 3   /\ wa 337   /\ w3a 1102   = wceq 1586   e. wcel 1588  A.wral 2355  E.wrex 2356   class class class wbr 3507   Fn wfn 4126  -->wf 4127  ` cfv 4131  (class class class)co 4981  CCcc 6750  RRcr 6751  0cc0 6752   <_ cle 6841   < clt 6845   - cmin 6989  NNcn 6992  Imcim 8382  abscabs 8384

This theorem is referenced by:  caucvg3ai 8820  caucvg3lem 8822

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929  ax-inf2 5964

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-nel 2269  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-if 3181  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-int 3401  df-iun 3438  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-lim 3816  df-suc 3817  df-om 4086  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-f1 4144  df-fo 4145  df-f1o 4146  df-fv 4147  df-opr 4983  df-oprab 4984  df-mpt 5099  df-1st 5126  df-2nd 5127  df-iota 5219  df-rdg 5304  df-1o 5344  df-oadd 5346  df-omul 5347  df-er 5479  df-ec 5481  df-qs 5484  df-en 5588  df-dom 5589  df-sdom 5590  df-undef 5725  df-riota 5729  df-sup 5888  df-ni 6518  df-pli 6519  df-mi 6520  df-lti 6521  df-plpq 6553  df-mpq 6554  df-enq 6555  df-nq 6556  df-plq 6557  df-mq 6558  df-rq 6559  df-ltq 6560  df-1q 6561  df-np 6604  df-1p 6605  df-plp 6606  df-mp 6607  df-ltp 6608  df-plpr 6682  df-mpr 6683  df-enr 6684  df-nr 6685  df-plr 6686  df-mr 6687  df-ltr 6688  df-0r 6689  df-1r 6690  df-m1r 6691  df-c 6758  df-0 6759  df-1 6760  df-i 6761  df-r 6762  df-plus 6763  df-mul 6764  df-lt 6765  df-pnf 6846  df-mnf 6847  df-xr 6848  df-ltxr 6849  df-le 6850  df-sub 7009  df-neg 7011  df-div 7223  df-n 7441  df-2 7487  df-n0 7649  df-z 7686  df-seq1 8094  df-exp 8196  df-sqr 8304  df-re 8385  df-im 8386  df-cj 8387  df-abs 8388

Copyright terms: Public domain