Metamath Proof Explorer


Theorem 1arithlem4

Description: Lemma for 1arith . (Contributed by Mario Carneiro, 30-May-2014)

Ref Expression
Hypotheses 1arith.1 M = n p p pCnt n
1arithlem4.2 G = y if y y F y 1
1arithlem4.3 φ F : 0
1arithlem4.4 φ N
1arithlem4.5 φ q N q F q = 0
Assertion 1arithlem4 φ x F = M x

Proof

Step Hyp Ref Expression
1 1arith.1 M = n p p pCnt n
2 1arithlem4.2 G = y if y y F y 1
3 1arithlem4.3 φ F : 0
4 1arithlem4.4 φ N
5 1arithlem4.5 φ q N q F q = 0
6 3 ffvelrnda φ y F y 0
7 6 ralrimiva φ y F y 0
8 2 7 pcmptcl φ G : seq 1 × G :
9 8 simprd φ seq 1 × G :
10 9 4 ffvelrnd φ seq 1 × G N
11 1 1arithlem2 seq 1 × G N q M seq 1 × G N q = q pCnt seq 1 × G N
12 10 11 sylan φ q M seq 1 × G N q = q pCnt seq 1 × G N
13 7 adantr φ q y F y 0
14 4 adantr φ q N
15 simpr φ q q
16 fveq2 y = q F y = F q
17 2 13 14 15 16 pcmpt φ q q pCnt seq 1 × G N = if q N F q 0
18 14 nnred φ q N
19 prmz q q
20 19 zred q q
21 20 adantl φ q q
22 5 anassrs φ q N q F q = 0
23 22 ifeq2d φ q N q if q N F q F q = if q N F q 0
24 ifid if q N F q F q = F q
25 23 24 eqtr3di φ q N q if q N F q 0 = F q
26 iftrue q N if q N F q 0 = F q
27 26 adantl φ q q N if q N F q 0 = F q
28 18 21 25 27 lecasei φ q if q N F q 0 = F q
29 12 17 28 3eqtrrd φ q F q = M seq 1 × G N q
30 29 ralrimiva φ q F q = M seq 1 × G N q
31 1 1arithlem3 seq 1 × G N M seq 1 × G N : 0
32 10 31 syl φ M seq 1 × G N : 0
33 ffn F : 0 F Fn
34 ffn M seq 1 × G N : 0 M seq 1 × G N Fn
35 eqfnfv F Fn M seq 1 × G N Fn F = M seq 1 × G N q F q = M seq 1 × G N q
36 33 34 35 syl2an F : 0 M seq 1 × G N : 0 F = M seq 1 × G N q F q = M seq 1 × G N q
37 3 32 36 syl2anc φ F = M seq 1 × G N q F q = M seq 1 × G N q
38 30 37 mpbird φ F = M seq 1 × G N
39 fveq2 x = seq 1 × G N M x = M seq 1 × G N
40 39 rspceeqv seq 1 × G N F = M seq 1 × G N x F = M x
41 10 38 40 syl2anc φ x F = M x