Metamath Proof Explorer


Theorem ulm2

Description: Simplify ulmval when F and G are known to be functions. (Contributed by Mario Carneiro, 26-Feb-2015)

Ref Expression
Hypotheses ulm2.z Z = M
ulm2.m φ M
ulm2.f φ F : Z S
ulm2.b φ k Z z S F k z = B
ulm2.a φ z S G z = A
ulm2.g φ G : S
ulm2.s φ S V
Assertion ulm2 φ F u S G x + j Z k j z S B A < x

Proof

Step Hyp Ref Expression
1 ulm2.z Z = M
2 ulm2.m φ M
3 ulm2.f φ F : Z S
4 ulm2.b φ k Z z S F k z = B
5 ulm2.a φ z S G z = A
6 ulm2.g φ G : S
7 ulm2.s φ S V
8 ulmval S V F u S G n F : n S G : S x + j n k j z S F k z G z < x
9 7 8 syl φ F u S G n F : n S G : S x + j n k j z S F k z G z < x
10 3anan12 F : n S G : S x + j n k j z S F k z G z < x G : S F : n S x + j n k j z S F k z G z < x
11 3 fdmd φ dom F = Z
12 fdm F : n S dom F = n
13 11 12 sylan9req φ F : n S Z = n
14 1 13 eqtr3id φ F : n S M = n
15 2 adantr φ F : n S M
16 uz11 M M = n M = n
17 15 16 syl φ F : n S M = n M = n
18 14 17 mpbid φ F : n S M = n
19 18 eqcomd φ F : n S n = M
20 fveq2 n = M n = M
21 20 1 eqtr4di n = M n = Z
22 21 feq2d n = M F : n S F : Z S
23 22 biimparc F : Z S n = M F : n S
24 3 23 sylan φ n = M F : n S
25 19 24 impbida φ F : n S n = M
26 25 anbi1d φ F : n S x + j n k j z S F k z G z < x n = M x + j n k j z S F k z G z < x
27 6 biantrurd φ F : n S x + j n k j z S F k z G z < x G : S F : n S x + j n k j z S F k z G z < x
28 simp-4l φ n = M j n k j z S φ
29 simpr φ n = M n = M
30 uzid M M M
31 2 30 syl φ M M
32 31 1 eleqtrrdi φ M Z
33 32 adantr φ n = M M Z
34 29 33 eqeltrd φ n = M n Z
35 1 uztrn2 n Z j n j Z
36 34 35 sylan φ n = M j n j Z
37 1 uztrn2 j Z k j k Z
38 36 37 sylan φ n = M j n k j k Z
39 38 adantr φ n = M j n k j z S k Z
40 simpr φ n = M j n k j z S z S
41 28 39 40 4 syl12anc φ n = M j n k j z S F k z = B
42 28 5 sylancom φ n = M j n k j z S G z = A
43 41 42 oveq12d φ n = M j n k j z S F k z G z = B A
44 43 fveq2d φ n = M j n k j z S F k z G z = B A
45 44 breq1d φ n = M j n k j z S F k z G z < x B A < x
46 45 ralbidva φ n = M j n k j z S F k z G z < x z S B A < x
47 46 ralbidva φ n = M j n k j z S F k z G z < x k j z S B A < x
48 47 rexbidva φ n = M j n k j z S F k z G z < x j n k j z S B A < x
49 48 ralbidv φ n = M x + j n k j z S F k z G z < x x + j n k j z S B A < x
50 49 pm5.32da φ n = M x + j n k j z S F k z G z < x n = M x + j n k j z S B A < x
51 26 27 50 3bitr3d φ G : S F : n S x + j n k j z S F k z G z < x n = M x + j n k j z S B A < x
52 10 51 syl5bb φ F : n S G : S x + j n k j z S F k z G z < x n = M x + j n k j z S B A < x
53 52 rexbidv φ n F : n S G : S x + j n k j z S F k z G z < x n n = M x + j n k j z S B A < x
54 21 rexeqdv n = M j n k j z S B A < x j Z k j z S B A < x
55 54 ralbidv n = M x + j n k j z S B A < x x + j Z k j z S B A < x
56 55 ceqsrexv M n n = M x + j n k j z S B A < x x + j Z k j z S B A < x
57 2 56 syl φ n n = M x + j n k j z S B A < x x + j Z k j z S B A < x
58 9 53 57 3bitrd φ F u S G x + j Z k j z S B A < x