Metamath Proof Explorer


Theorem smflimsuplem1

Description: If H converges, the limsup of F is real. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smflimsuplem1.z Z = M
smflimsuplem1.e E = n Z x m n dom F m | sup ran m n F m x * <
smflimsuplem1.h H = n Z x E n sup ran m n F m x * <
smflimsuplem1.k φ K Z
Assertion smflimsuplem1 φ dom H K dom F K

Proof

Step Hyp Ref Expression
1 smflimsuplem1.z Z = M
2 smflimsuplem1.e E = n Z x m n dom F m | sup ran m n F m x * <
3 smflimsuplem1.h H = n Z x E n sup ran m n F m x * <
4 smflimsuplem1.k φ K Z
5 fveq2 m = j F m = F j
6 5 fveq1d m = j F m x = F j x
7 6 cbvmptv m n F m x = j n F j x
8 7 rneqi ran m n F m x = ran j n F j x
9 8 supeq1i sup ran m n F m x * < = sup ran j n F j x * <
10 9 mpteq2i x E n sup ran m n F m x * < = x E n sup ran j n F j x * <
11 10 a1i n = K x E n sup ran m n F m x * < = x E n sup ran j n F j x * <
12 fveq2 n = K E n = E K
13 fveq2 n = K n = K
14 13 mpteq1d n = K j n F j x = j K F j x
15 14 rneqd n = K ran j n F j x = ran j K F j x
16 15 supeq1d n = K sup ran j n F j x * < = sup ran j K F j x * <
17 12 16 mpteq12dv n = K x E n sup ran j n F j x * < = x E K sup ran j K F j x * <
18 11 17 eqtrd n = K x E n sup ran m n F m x * < = x E K sup ran j K F j x * <
19 fvex E K V
20 19 mptex x E K sup ran j K F j x * < V
21 20 a1i φ x E K sup ran j K F j x * < V
22 3 18 4 21 fvmptd3 φ H K = x E K sup ran j K F j x * <
23 22 dmeqd φ dom H K = dom x E K sup ran j K F j x * <
24 xrltso < Or *
25 24 supex sup ran j K F j x * < V
26 eqid x E K sup ran j K F j x * < = x E K sup ran j K F j x * <
27 25 26 dmmpti dom x E K sup ran j K F j x * < = E K
28 27 a1i φ dom x E K sup ran j K F j x * < = E K
29 5 dmeqd m = j dom F m = dom F j
30 29 cbviinv m n dom F m = j n dom F j
31 30 eleq2i x m n dom F m x j n dom F j
32 9 eleq1i sup ran m n F m x * < sup ran j n F j x * <
33 31 32 anbi12i x m n dom F m sup ran m n F m x * < x j n dom F j sup ran j n F j x * <
34 33 rabbia2 x m n dom F m | sup ran m n F m x * < = x j n dom F j | sup ran j n F j x * <
35 34 a1i n = K x m n dom F m | sup ran m n F m x * < = x j n dom F j | sup ran j n F j x * <
36 13 iineq1d n = K j n dom F j = j K dom F j
37 36 eleq2d n = K x j n dom F j x j K dom F j
38 16 eleq1d n = K sup ran j n F j x * < sup ran j K F j x * <
39 37 38 anbi12d n = K x j n dom F j sup ran j n F j x * < x j K dom F j sup ran j K F j x * <
40 39 rabbidva2 n = K x j n dom F j | sup ran j n F j x * < = x j K dom F j | sup ran j K F j x * <
41 35 40 eqtrd n = K x m n dom F m | sup ran m n F m x * < = x j K dom F j | sup ran j K F j x * <
42 eqid x j K dom F j | sup ran j K F j x * < = x j K dom F j | sup ran j K F j x * <
43 1 4 eluzelz2d φ K
44 uzid K K K
45 ne0i K K K
46 43 44 45 3syl φ K
47 fvex F j V
48 47 dmex dom F j V
49 48 rgenw j K dom F j V
50 49 a1i φ j K dom F j V
51 46 50 iinexd φ j K dom F j V
52 42 51 rabexd φ x j K dom F j | sup ran j K F j x * < V
53 2 41 4 52 fvmptd3 φ E K = x j K dom F j | sup ran j K F j x * <
54 23 28 53 3eqtrd φ dom H K = x j K dom F j | sup ran j K F j x * <
55 ssrab2 x j K dom F j | sup ran j K F j x * < j K dom F j
56 55 a1i φ x j K dom F j | sup ran j K F j x * < j K dom F j
57 43 44 syl φ K K
58 fveq2 j = K F j = F K
59 58 dmeqd j = K dom F j = dom F K
60 ssid dom F K dom F K
61 60 a1i φ dom F K dom F K
62 57 59 61 iinssd φ j K dom F j dom F K
63 56 62 sstrd φ x j K dom F j | sup ran j K F j x * < dom F K
64 54 63 eqsstrd φ dom H K dom F K