Metamath Proof Explorer


Theorem ulmshftlem

Description: Lemma for ulmshft . (Contributed by Mario Carneiro, 24-Mar-2015)

Ref Expression
Hypotheses ulmshft.z Z = M
ulmshft.w W = M + K
ulmshft.m φ M
ulmshft.k φ K
ulmshft.f φ F : Z S
ulmshft.h φ H = n W F n K
Assertion ulmshftlem φ F u S G H u S G

Proof

Step Hyp Ref Expression
1 ulmshft.z Z = M
2 ulmshft.w W = M + K
3 ulmshft.m φ M
4 ulmshft.k φ K
5 ulmshft.f φ F : Z S
6 ulmshft.h φ H = n W F n K
7 3 ad2antrr φ F u S G x + M
8 5 ad2antrr φ F u S G x + F : Z S
9 eqidd φ F u S G x + m Z z S F m z = F m z
10 eqidd φ F u S G x + z S G z = G z
11 simplr φ F u S G x + F u S G
12 simpr φ F u S G x + x +
13 1 7 8 9 10 11 12 ulmi φ F u S G x + i Z m i z S F m z G z < x
14 simpr φ F u S G x + i Z i Z
15 14 1 eleqtrdi φ F u S G x + i Z i M
16 4 ad3antrrr φ F u S G x + i Z K
17 eluzadd i M K i + K M + K
18 15 16 17 syl2anc φ F u S G x + i Z i + K M + K
19 18 2 eleqtrrdi φ F u S G x + i Z i + K W
20 eluzelz i M i
21 15 20 syl φ F u S G x + i Z i
22 21 adantr φ F u S G x + i Z k i + K i
23 4 adantr φ F u S G K
24 23 ad3antrrr φ F u S G x + i Z k i + K K
25 simpr φ F u S G x + i Z k i + K k i + K
26 eluzsub i K k i + K k K i
27 22 24 25 26 syl3anc φ F u S G x + i Z k i + K k K i
28 fveq2 m = k K F m = F k K
29 28 fveq1d m = k K F m z = F k K z
30 29 fvoveq1d m = k K F m z G z = F k K z G z
31 30 breq1d m = k K F m z G z < x F k K z G z < x
32 31 ralbidv m = k K z S F m z G z < x z S F k K z G z < x
33 32 rspcv k K i m i z S F m z G z < x z S F k K z G z < x
34 27 33 syl φ F u S G x + i Z k i + K m i z S F m z G z < x z S F k K z G z < x
35 34 ralrimdva φ F u S G x + i Z m i z S F m z G z < x k i + K z S F k K z G z < x
36 fveq2 j = i + K j = i + K
37 36 raleqdv j = i + K k j z S F k K z G z < x k i + K z S F k K z G z < x
38 37 rspcev i + K W k i + K z S F k K z G z < x j W k j z S F k K z G z < x
39 19 35 38 syl6an φ F u S G x + i Z m i z S F m z G z < x j W k j z S F k K z G z < x
40 39 rexlimdva φ F u S G x + i Z m i z S F m z G z < x j W k j z S F k K z G z < x
41 13 40 mpd φ F u S G x + j W k j z S F k K z G z < x
42 41 ralrimiva φ F u S G x + j W k j z S F k K z G z < x
43 3 4 zaddcld φ M + K
44 43 adantr φ F u S G M + K
45 5 adantr φ n W F : Z S
46 3 adantr φ n W M
47 4 adantr φ n W K
48 simpr φ n W n W
49 48 2 eleqtrdi φ n W n M + K
50 eluzsub M K n M + K n K M
51 46 47 49 50 syl3anc φ n W n K M
52 51 1 eleqtrrdi φ n W n K Z
53 45 52 ffvelrnd φ n W F n K S
54 6 53 fmpt3d φ H : W S
55 54 adantr φ F u S G H : W S
56 6 ad2antrr φ F u S G k W z S H = n W F n K
57 56 fveq1d φ F u S G k W z S H k = n W F n K k
58 fvoveq1 n = k F n K = F k K
59 eqid n W F n K = n W F n K
60 fvex F k K V
61 58 59 60 fvmpt k W n W F n K k = F k K
62 61 ad2antrl φ F u S G k W z S n W F n K k = F k K
63 57 62 eqtrd φ F u S G k W z S H k = F k K
64 63 fveq1d φ F u S G k W z S H k z = F k K z
65 eqidd φ F u S G z S G z = G z
66 ulmcl F u S G G : S
67 66 adantl φ F u S G G : S
68 ulmscl F u S G S V
69 68 adantl φ F u S G S V
70 2 44 55 64 65 67 69 ulm2 φ F u S G H u S G x + j W k j z S F k K z G z < x
71 42 70 mpbird φ F u S G H u S G
72 71 ex φ F u S G H u S G