1arithlem4

	Ref	Expression
Hypotheses	1arith.1	$⊢ M = (n \in ℕ ⟼ (p \in ℙ ⟼ p pCnt n))$
	1arithlem4.2	$⊢ G = (y \in ℕ ⟼ if (y \in ℙ, y^{F (y)}, 1))$
	1arithlem4.3	$⊢ φ \to F : ℙ ⟶ ℕ_{0}$
	1arithlem4.4	$⊢ φ \to N \in ℕ$
	1arithlem4.5	$⊢ (φ \land (q \in ℙ \land N \leq q)) \to F (q) = 0$
Assertion	1arithlem4	$⊢ φ \to \exists x \in ℕ F = M (x)$

Proof

Step	Hyp	Ref	Expression
1		1arith.1	$⊢ M = (n \in ℕ ⟼ (p \in ℙ ⟼ p pCnt n))$
2		1arithlem4.2	$⊢ G = (y \in ℕ ⟼ if (y \in ℙ, y^{F (y)}, 1))$
3		1arithlem4.3	$⊢ φ \to F : ℙ ⟶ ℕ_{0}$
4		1arithlem4.4	$⊢ φ \to N \in ℕ$
5		1arithlem4.5	$⊢ (φ \land (q \in ℙ \land N \leq q)) \to F (q) = 0$
6	3	ffvelcdmda	$⊢ (φ \land y \in ℙ) \to F (y) \in ℕ_{0}$
7	6	ralrimiva	$⊢ φ \to \forall y \in ℙ F (y) \in ℕ_{0}$
8	2 7	pcmptcl	$⊢ φ \to (G : ℕ ⟶ ℕ \land seq 1 (\times G) : ℕ ⟶ ℕ)$
9	8	simprd	$⊢ φ \to seq 1 (\times G) : ℕ ⟶ ℕ$
10	9 4	ffvelcdmd	$⊢ φ \to seq 1 (\times G) (N) \in ℕ$
11	1	1arithlem2	$⊢ (seq 1 (\times G) (N) \in ℕ \land q \in ℙ) \to M (seq 1 (\times G) (N)) (q) = q pCnt seq 1 (\times G) (N)$
12	10 11	sylan	$⊢ (φ \land q \in ℙ) \to M (seq 1 (\times G) (N)) (q) = q pCnt seq 1 (\times G) (N)$
13	7	adantr	$⊢ (φ \land q \in ℙ) \to \forall y \in ℙ F (y) \in ℕ_{0}$
14	4	adantr	$⊢ (φ \land q \in ℙ) \to N \in ℕ$
15		simpr	$⊢ (φ \land q \in ℙ) \to q \in ℙ$
16		fveq2	$⊢ y = q \to F (y) = F (q)$
17	2 13 14 15 16	pcmpt	$⊢ (φ \land q \in ℙ) \to q pCnt seq 1 (\times G) (N) = if (q \leq N, F (q), 0)$
18	14	nnred	$⊢ (φ \land q \in ℙ) \to N \in ℝ$
19		prmz	$⊢ q \in ℙ \to q \in ℤ$
20	19	zred	$⊢ q \in ℙ \to q \in ℝ$
21	20	adantl	$⊢ (φ \land q \in ℙ) \to q \in ℝ$
22	5	anassrs	$⊢ ((φ \land q \in ℙ) \land N \leq q) \to F (q) = 0$
23	22	ifeq2d	$⊢ ((φ \land q \in ℙ) \land N \leq q) \to if (q \leq N, F (q), F (q)) = if (q \leq N, F (q), 0)$
24		ifid	$⊢ if (q \leq N, F (q), F (q)) = F (q)$
25	23 24	eqtr3di	$⊢ ((φ \land q \in ℙ) \land N \leq q) \to if (q \leq N, F (q), 0) = F (q)$
26		iftrue	$⊢ q \leq N \to if (q \leq N, F (q), 0) = F (q)$
27	26	adantl	$⊢ ((φ \land q \in ℙ) \land q \leq N) \to if (q \leq N, F (q), 0) = F (q)$
28	18 21 25 27	lecasei	$⊢ (φ \land q \in ℙ) \to if (q \leq N, F (q), 0) = F (q)$
29	12 17 28	3eqtrrd	$⊢ (φ \land q \in ℙ) \to F (q) = M (seq 1 (\times G) (N)) (q)$
30	29	ralrimiva	$⊢ φ \to \forall q \in ℙ F (q) = M (seq 1 (\times G) (N)) (q)$
31	1	1arithlem3	$⊢ seq 1 (\times G) (N) \in ℕ \to M (seq 1 (\times G) (N)) : ℙ ⟶ ℕ_{0}$
32	10 31	syl	$⊢ φ \to M (seq 1 (\times G) (N)) : ℙ ⟶ ℕ_{0}$
33		ffn	$⊢ F : ℙ ⟶ ℕ_{0} \to F Fn ℙ$
34		ffn	$⊢ M (seq 1 (\times G) (N)) : ℙ ⟶ ℕ_{0} \to M (seq 1 (\times G) (N)) Fn ℙ$
35		eqfnfv	$⊢ (F Fn ℙ \land M (seq 1 (\times G) (N)) Fn ℙ) \to (F = M (seq 1 (\times G) (N)) \leftrightarrow \forall q \in ℙ F (q) = M (seq 1 (\times G) (N)) (q))$
36	33 34 35	syl2an	$⊢ (F : ℙ ⟶ ℕ_{0} \land M (seq 1 (\times G) (N)) : ℙ ⟶ ℕ_{0}) \to (F = M (seq 1 (\times G) (N)) \leftrightarrow \forall q \in ℙ F (q) = M (seq 1 (\times G) (N)) (q))$
37	3 32 36	syl2anc	$⊢ φ \to (F = M (seq 1 (\times G) (N)) \leftrightarrow \forall q \in ℙ F (q) = M (seq 1 (\times G) (N)) (q))$
38	30 37	mpbird	$⊢ φ \to F = M (seq 1 (\times G) (N))$
39		fveq2	$⊢ x = seq 1 (\times G) (N) \to M (x) = M (seq 1 (\times G) (N))$
40	39	rspceeqv	$⊢ (seq 1 (\times G) (N) \in ℕ \land F = M (seq 1 (\times G) (N))) \to \exists x \in ℕ F = M (x)$
41	10 38 40	syl2anc	$⊢ φ \to \exists x \in ℕ F = M (x)$

Metamath Proof Explorer

Theorem 1arithlem4

Proof