Theorem cvganz 8561

Description: Equivalence that lets us conjoin the properties of two independent converging sequences. k may be free in ph and ps. Compare r19.40 2481, where the implication holds in only one direction.

Assertion

Ref	Expression
cvganz	|- ((E.j e. ZZ A.k e. ZZ (j <_ k -> ph) /\ E.j e. ZZ A.k e. ZZ (j <_ k -> ps)) <-> E.j e. ZZ A.k e. ZZ (j <_ k -> (ph /\ ps)))

Distinct variable groups:   j,k   ph,j   ps,j

Proof of Theorem cvganz

Step	Hyp	Ref	Expression
1		breq1 3510	. . . . . . 7 |- (j = m -> (j <_ k <-> m <_ k))
2	1	imbi1d 748	. . . . . 6 |- (j = m -> ((j <_ k -> ph) <-> (m <_ k -> ph)))
3	2	ralbidv 2373	. . . . 5 |- (j = m -> (A.k e. NN0 (j <_ k -> ph) <-> A.k e. NN0 (m <_ k -> ph)))
4	3	cbvrexv 2527	. . . 4 |- (E.j e. NN0 A.k e. NN0 (j <_ k -> ph) <-> E.m e. NN0 A.k e. NN0 (m <_ k -> ph))
5		breq1 3510	. . . . . . 7 |- (j = n -> (j <_ k <-> n <_ k))
6	5	imbi1d 748	. . . . . 6 |- (j = n -> ((j <_ k -> ps) <-> (n <_ k -> ps)))
7	6	ralbidv 2373	. . . . 5 |- (j = n -> (A.k e. NN0 (j <_ k -> ps) <-> A.k e. NN0 (n <_ k -> ps)))
8	7	cbvrexv 2527	. . . 4 |- (E.j e. NN0 A.k e. NN0 (j <_ k -> ps) <-> E.n e. NN0 A.k e. NN0 (n <_ k -> ps))
9		reeanv 2493	. . . . 5 |- (E.m e. NN0 E.n e. NN0 (A.k e. NN0 (m <_ k -> ph) /\ A.k e. NN0 (n <_ k -> ps)) <-> (E.m e. NN0 A.k e. NN0 (m <_ k -> ph) /\ E.n e. NN0 A.k e. NN0 (n <_ k -> ps)))
10		r19.26 2467	. . . . . . . . 9 |- (A.k e. NN0 ((m <_ k -> ph) /\ (n <_ k -> ps)) <-> (A.k e. NN0 (m <_ k -> ph) /\ A.k e. NN0 (n <_ k -> ps)))
11		nn0re 7657	. . . . . . . . . . . . . . 15 |- (m e. NN0 -> m e. RR)
12		nn0addge1 7680	. . . . . . . . . . . . . . 15 |- ((m e. RR /\ n e. NN0) -> m <_ (m + n))
13	11, 12	sylan 597	. . . . . . . . . . . . . 14 |- ((m e. NN0 /\ n e. NN0) -> m <_ (m + n))
14	13	adantr 447	. . . . . . . . . . . . 13 |- (((m e. NN0 /\ n e. NN0) /\ k e. NN0) -> m <_ (m + n))
15	11	ad2antrr 799	. . . . . . . . . . . . . 14 |- (((m e. NN0 /\ n e. NN0) /\ k e. NN0) -> m e. RR)
16		nn0addcl 7670	. . . . . . . . . . . . . . . 16 |- ((m e. NN0 /\ n e. NN0) -> (m + n) e. NN0)
17		nn0re 7657	. . . . . . . . . . . . . . . 16 |- ((m + n) e. NN0 -> (m + n) e. RR)
18	16, 17	syl 13	. . . . . . . . . . . . . . 15 |- ((m e. NN0 /\ n e. NN0) -> (m + n) e. RR)
19	18	adantr 447	. . . . . . . . . . . . . 14 |- (((m e. NN0 /\ n e. NN0) /\ k e. NN0) -> (m + n) e. RR)
20		nn0re 7657	. . . . . . . . . . . . . . 15 |- (k e. NN0 -> k e. RR)
21	20	adantl 448	. . . . . . . . . . . . . 14 |- (((m e. NN0 /\ n e. NN0) /\ k e. NN0) -> k e. RR)
22		letr 6884	. . . . . . . . . . . . . 14 |- ((m e. RR /\ (m + n) e. RR /\ k e. RR) -> ((m <_ (m + n) /\ (m + n) <_ k) -> m <_ k))
23	15, 19, 21, 22	syl111anc 1349	. . . . . . . . . . . . 13 |- (((m e. NN0 /\ n e. NN0) /\ k e. NN0) -> ((m <_ (m + n) /\ (m + n) <_ k) -> m <_ k))
24	14, 23	mpand 684	. . . . . . . . . . . 12 |- (((m e. NN0 /\ n e. NN0) /\ k e. NN0) -> ((m + n) <_ k -> m <_ k))
25		nn0re 7657	. . . . . . . . . . . . . . . 16 |- (n e. NN0 -> n e. RR)
26		nn0addge2 7681	. . . . . . . . . . . . . . . 16 |- ((n e. RR /\ m e. NN0) -> n <_ (m + n))
27	25, 26	sylan 597	. . . . . . . . . . . . . . 15 |- ((n e. NN0 /\ m e. NN0) -> n <_ (m + n))
28	27	ancoms 416	. . . . . . . . . . . . . 14 |- ((m e. NN0 /\ n e. NN0) -> n <_ (m + n))
29	28	adantr 447	. . . . . . . . . . . . 13 |- (((m e. NN0 /\ n e. NN0) /\ k e. NN0) -> n <_ (m + n))
30	25	ad2antlr 802	. . . . . . . . . . . . . 14 |- (((m e. NN0 /\ n e. NN0) /\ k e. NN0) -> n e. RR)
31		letr 6884	. . . . . . . . . . . . . 14 |- ((n e. RR /\ (m + n) e. RR /\ k e. RR) -> ((n <_ (m + n) /\ (m + n) <_ k) -> n <_ k))
32	30, 19, 21, 31	syl111anc 1349	. . . . . . . . . . . . 13 |- (((m e. NN0 /\ n e. NN0) /\ k e. NN0) -> ((n <_ (m + n) /\ (m + n) <_ k) -> n <_ k))
33	29, 32	mpand 684	. . . . . . . . . . . 12 |- (((m e. NN0 /\ n e. NN0) /\ k e. NN0) -> ((m + n) <_ k -> n <_ k))
34	24, 33	jcad 496	. . . . . . . . . . 11 |- (((m e. NN0 /\ n e. NN0) /\ k e. NN0) -> ((m + n) <_ k -> (m <_ k /\ n <_ k)))
35		prth 541	. . . . . . . . . . 11 |- (((m <_ k -> ph) /\ (n <_ k -> ps)) -> ((m <_ k /\ n <_ k) -> (ph /\ ps)))
36	34, 35	syl9 57	. . . . . . . . . 10 |- (((m e. NN0 /\ n e. NN0) /\ k e. NN0) -> (((m <_ k -> ph) /\ (n <_ k -> ps)) -> ((m + n) <_ k -> (ph /\ ps))))
37	36	ralimdva 2421	. . . . . . . . 9 |- ((m e. NN0 /\ n e. NN0) -> (A.k e. NN0 ((m <_ k -> ph) /\ (n <_ k -> ps)) -> A.k e. NN0 ((m + n) <_ k -> (ph /\ ps))))
38	10, 37	syl5bir 251	. . . . . . . 8 |- ((m e. NN0 /\ n e. NN0) -> ((A.k e. NN0 (m <_ k -> ph) /\ A.k e. NN0 (n <_ k -> ps)) -> A.k e. NN0 ((m + n) <_ k -> (ph /\ ps))))
39	38, 16	jctild 507	. . . . . . 7 |- ((m e. NN0 /\ n e. NN0) -> ((A.k e. NN0 (m <_ k -> ph) /\ A.k e. NN0 (n <_ k -> ps)) -> ((m + n) e. NN0 /\ A.k e. NN0 ((m + n) <_ k -> (ph /\ ps)))))
40		breq1 3510	. . . . . . . . . 10 |- (j = (m + n) -> (j <_ k <-> (m + n) <_ k))
41	40	imbi1d 748	. . . . . . . . 9 |- (j = (m + n) -> ((j <_ k -> (ph /\ ps)) <-> ((m + n) <_ k -> (ph /\ ps))))
42	41	ralbidv 2373	. . . . . . . 8 |- (j = (m + n) -> (A.k e. NN0 (j <_ k -> (ph /\ ps)) <-> A.k e. NN0 ((m + n) <_ k -> (ph /\ ps))))
43	42	rcla4ev 2620	. . . . . . 7 |- (((m + n) e. NN0 /\ A.k e. NN0 ((m + n) <_ k -> (ph /\ ps))) -> E.j e. NN0 A.k e. NN0 (j <_ k -> (ph /\ ps)))
44	39, 43	syl6 42	. . . . . 6 |- ((m e. NN0 /\ n e. NN0) -> ((A.k e. NN0 (m <_ k -> ph) /\ A.k e. NN0 (n <_ k -> ps)) -> E.j e. NN0 A.k e. NN0 (j <_ k -> (ph /\ ps))))
45	44	r19.23aivv 2465	. . . . 5 |- (E.m e. NN0 E.n e. NN0 (A.k e. NN0 (m <_ k -> ph) /\ A.k e. NN0 (n <_ k -> ps)) -> E.j e. NN0 A.k e. NN0 (j <_ k -> (ph /\ ps)))
46	9, 45	sylbir 244	. . . 4 |- ((E.m e. NN0 A.k e. NN0 (m <_ k -> ph) /\ E.n e. NN0 A.k e. NN0 (n <_ k -> ps)) -> E.j e. NN0 A.k e. NN0 (j <_ k -> (ph /\ ps)))
47	4, 8, 46	syl2anb 604	. . 3 |- ((E.j e. NN0 A.k e. NN0 (j <_ k -> ph) /\ E.j e. NN0 A.k e. NN0 (j <_ k -> ps)) -> E.j e. NN0 A.k e. NN0 (j <_ k -> (ph /\ ps)))
48		simpl 437	. . . . . . 7 |- ((ph /\ ps) -> ph)
49	48	imim2i 12	. . . . . 6 |- ((j <_ k -> (ph /\ ps)) -> (j <_ k -> ph))
50	49	ralimi 2418	. . . . 5 |- (A.k e. NN0 (j <_ k -> (ph /\ ps)) -> A.k e. NN0 (j <_ k -> ph))
51	50	reximi 2448	. . . 4 |- (E.j e. NN0 A.k e. NN0 (j <_ k -> (ph /\ ps)) -> E.j e. NN0 A.k e. NN0 (j <_ k -> ph))
52		simpr 442	. . . . . . 7 |- ((ph /\ ps) -> ps)
53	52	imim2i 12	. . . . . 6 |- ((j <_ k -> (ph /\ ps)) -> (j <_ k -> ps))
54	53	ralimi 2418	. . . . 5 |- (A.k e. NN0 (j <_ k -> (ph /\ ps)) -> A.k e. NN0 (j <_ k -> ps))
55	54	reximi 2448	. . . 4 |- (E.j e. NN0 A.k e. NN0 (j <_ k -> (ph /\ ps)) -> E.j e. NN0 A.k e. NN0 (j <_ k -> ps))
56	51, 55	jca 494	. . 3 |- (E.j e. NN0 A.k e. NN0 (j <_ k -> (ph /\ ps)) -> (E.j e. NN0 A.k e. NN0 (j <_ k -> ph) /\ E.j e. NN0 A.k e. NN0 (j <_ k -> ps)))
57	47, 56	impbii 223	. 2 |- ((E.j e. NN0 A.k e. NN0 (j <_ k -> ph) /\ E.j e. NN0 A.k e. NN0 (j <_ k -> ps)) <-> E.j e. NN0 A.k e. NN0 (j <_ k -> (ph /\ ps)))
58		0z 7696	. . . 4 |- 0 e. ZZ
59		nn0uz 7954	. . . . 5 |- NN0 = (ZZ>=` 0)
60	59	eqimss2i 2897	. . . 4 |- (ZZ>=` 0) C_ NN0
61		nn0ssz 7702	. . . 4 |- NN0 C_ ZZ
62	58, 60, 61, 58, 60, 61	cvg3i 8560	. . 3 |- (E.j e. ZZ A.k e. ZZ (j <_ k -> ph) <-> E.j e. NN0 A.k e. NN0 (j <_ k -> ph))
63	58, 60, 61, 58, 60, 61	cvg3i 8560	. . 3 |- (E.j e. ZZ A.k e. ZZ (j <_ k -> ps) <-> E.j e. NN0 A.k e. NN0 (j <_ k -> ps))
64	62, 63	anbi12i 710	. 2 |- ((E.j e. ZZ A.k e. ZZ (j <_ k -> ph) /\ E.j e. ZZ A.k e. ZZ (j <_ k -> ps)) <-> (E.j e. NN0 A.k e. NN0 (j <_ k -> ph) /\ E.j e. NN0 A.k e. NN0 (j <_ k -> ps)))
65	58, 60, 61, 58, 60, 61	cvg3i 8560	. 2 |- (E.j e. ZZ A.k e. ZZ (j <_ k -> (ph /\ ps)) <-> E.j e. NN0 A.k e. NN0 (j <_ k -> (ph /\ ps)))
66	57, 64, 65	3bitr4i 295	1 |- ((E.j e. ZZ A.k e. ZZ (j <_ k -> ph) /\ E.j e. ZZ A.k e. ZZ (j <_ k -> ps)) <-> E.j e. ZZ A.k e. ZZ (j <_ k -> (ph /\ ps)))

Syntax hints:   -> wi 3   <-> wb 219   /\ wa 337   = wceq 1586   e. wcel 1588  A.wral 2355  E.wrex 2356   class class class wbr 3507  ` cfv 4131  (class class class)co 4981  RRcr 6751  0cc0 6752   + caddc 6755   <_ cle 6841  NN0cn0 6993  ZZcz 6994  ZZ>=cuz 7933

This theorem is referenced by:  cvganuzi 8562

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-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-n 7441  df-n0 7649  df-z 7686  df-uz 7934

Copyright terms: Public domain