MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prodmo Unicode version

Theorem prodmo 13743
Description: A product has at most one limit. (Contributed by Scott Fenton, 4-Dec-2017.)
Hypotheses
Ref Expression
prodmo.1
prodmo.2
prodmo.3
Assertion
Ref Expression
prodmo
Distinct variable groups:   , ,   , ,   , ,   , , , ,   , , ,   , , , ,   , ,   ,   , ,   , , , ,   , ,   ,

Proof of Theorem prodmo
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 3simpb 994 . . . . . . 7
21reximi 2925 . . . . . 6
3 3simpb 994 . . . . . . 7
43reximi 2925 . . . . . 6
5 fveq2 5871 . . . . . . . . . . . 12
65sseq2d 3531 . . . . . . . . . . 11
7 seqeq1 12110 . . . . . . . . . . . 12
87breq1d 4462 . . . . . . . . . . 11
96, 8anbi12d 710 . . . . . . . . . 10
109cbvrexv 3085 . . . . . . . . 9
1110anbi2i 694 . . . . . . . 8
12 reeanv 3025 . . . . . . . 8
1311, 12bitr4i 252 . . . . . . 7
14 simprlr 764 . . . . . . . . . . . . 13
1514adantl 466 . . . . . . . . . . . 12
16 prodmo.1 . . . . . . . . . . . . 13
17 prodmo.2 . . . . . . . . . . . . . 14
1817adantlr 714 . . . . . . . . . . . . 13
19 simprll 763 . . . . . . . . . . . . 13
20 simprlr 764 . . . . . . . . . . . . 13
21 simprll 763 . . . . . . . . . . . . . 14
2221adantl 466 . . . . . . . . . . . . 13
23 simprrl 765 . . . . . . . . . . . . . 14
2423adantl 466 . . . . . . . . . . . . 13
2516, 18, 19, 20, 22, 24prodrb 13739 . . . . . . . . . . . 12
2615, 25mpbid 210 . . . . . . . . . . 11
27 simprrr 766 . . . . . . . . . . . 12
2827adantl 466 . . . . . . . . . . 11
29 climuni 13375 . . . . . . . . . . 11
3026, 28, 29syl2anc 661 . . . . . . . . . 10
3130expcom 435 . . . . . . . . 9
3231ex 434 . . . . . . . 8
3332rexlimivv 2954 . . . . . . 7
3413, 33sylbi 195 . . . . . 6
352, 4, 34syl2an 477 . . . . 5
36 prodmo.3 . . . . . . . . . 10
3716, 17, 36prodmolem2 13742 . . . . . . . . 9
38 equcomi 1793 . . . . . . . . 9
3937, 38syl6 33 . . . . . . . 8
4039expimpd 603 . . . . . . 7
4140com12 31 . . . . . 6
4241ancoms 453 . . . . 5
4316, 17, 36prodmolem2 13742 . . . . . . 7
4443expimpd 603 . . . . . 6
4544com12 31 . . . . 5
46 reeanv 3025 . . . . . . . 8
47 eeanv 1988 . . . . . . . . 9
48472rexbii 2960 . . . . . . . 8
49 oveq2 6304 . . . . . . . . . . . . . 14
50 f1oeq2 5813 . . . . . . . . . . . . . 14
5149, 50syl 16 . . . . . . . . . . . . 13
52 fveq2 5871 . . . . . . . . . . . . . 14
5352eqeq2d 2471 . . . . . . . . . . . . 13
5451, 53anbi12d 710 . . . . . . . . . . . 12
5554exbidv 1714 . . . . . . . . . . 11
56 f1oeq1 5812 . . . . . . . . . . . . 13
57 fveq1 5870 . . . . . . . . . . . . . . . . . . 19
5857csbeq1d 3441 . . . . . . . . . . . . . . . . . 18
5958mpteq2dv 4539 . . . . . . . . . . . . . . . . 17
6036, 59syl5eq 2510 . . . . . . . . . . . . . . . 16
6160seqeq3d 12115 . . . . . . . . . . . . . . 15
6261fveq1d 5873 . . . . . . . . . . . . . 14
6362eqeq2d 2471 . . . . . . . . . . . . 13
6456, 63anbi12d 710 . . . . . . . . . . . 12
6564cbvexv 2024 . . . . . . . . . . 11
6655, 65syl6bb 261 . . . . . . . . . 10
6766cbvrexv 3085 . . . . . . . . 9
6867anbi2i 694 . . . . . . . 8
6946, 48, 683bitr4i 277 . . . . . . 7
70 an4 824 . . . . . . . . . 10
71 simpll 753 . . . . . . . . . . . . . 14
7271, 17sylan 471 . . . . . . . . . . . . 13
73 fveq2 5871 . . . . . . . . . . . . . . . 16
7473csbeq1d 3441 . . . . . . . . . . . . . . 15
7574cbvmptv 4543 . . . . . . . . . . . . . 14
7636, 75eqtri 2486 . . . . . . . . . . . . 13
77 fveq2 5871 . . . . . . . . . . . . . . 15
7877csbeq1d 3441 . . . . . . . . . . . . . 14
7978cbvmptv 4543 . . . . . . . . . . . . 13
80 simplr 755 . . . . . . . . . . . . 13
81 simprl 756 . . . . . . . . . . . . 13
82 simprr 757 . . . . . . . . . . . . 13
8316, 72, 76, 79, 80, 81, 82prodmolem3 13740 . . . . . . . . . . . 12
84 eqeq12 2476 . . . . . . . . . . . 12
8583, 84syl5ibrcom 222 . . . . . . . . . . 11
8685expimpd 603 . . . . . . . . . 10
8770, 86syl5bi 217 . . . . . . . . 9
8887exlimdvv 1725 . . . . . . . 8
8988rexlimdvva 2956 . . . . . . 7
9069, 89syl5bir 218 . . . . . 6
9190com12 31 . . . . 5
9235, 42, 45, 91ccase 946 . . . 4
9392com12 31 . . 3
9493alrimivv 1720 . 2
95 breq2 4456 . . . . . 6
96953anbi3d 1305 . . . . 5
9796rexbidv 2968 . . . 4