Theorem 1arithlem4

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

	Ref	Expression
Hypotheses	1arith.1	⊢ 𝑀 = ( 𝑛 ∈ ℕ ↦ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) )
	1arithlem4.2	⊢ 𝐺 = ( 𝑦 ∈ ℕ ↦ if ( 𝑦 ∈ ℙ , ( 𝑦 ↑ ( 𝐹 ‘ 𝑦 ) ) , 1 ) )
	1arithlem4.3	⊢ ( 𝜑 → 𝐹 : ℙ ⟶ ℕ0 )
	1arithlem4.4	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	1arithlem4.5	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ ℙ ∧ 𝑁 ≤ 𝑞 ) ) → ( 𝐹 ‘ 𝑞 ) = 0 )
Assertion	1arithlem4	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℕ 𝐹 = ( 𝑀 ‘ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		1arith.1	⊢ 𝑀 = ( 𝑛 ∈ ℕ ↦ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) )
2		1arithlem4.2	⊢ 𝐺 = ( 𝑦 ∈ ℕ ↦ if ( 𝑦 ∈ ℙ , ( 𝑦 ↑ ( 𝐹 ‘ 𝑦 ) ) , 1 ) )
3		1arithlem4.3	⊢ ( 𝜑 → 𝐹 : ℙ ⟶ ℕ0 )
4		1arithlem4.4	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
5		1arithlem4.5	⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ ℙ ∧ 𝑁 ≤ 𝑞 ) ) → ( 𝐹 ‘ 𝑞 ) = 0 )
6	3	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℙ ) → ( 𝐹 ‘ 𝑦 ) ∈ ℕ0 )
7	6	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ ℙ ( 𝐹 ‘ 𝑦 ) ∈ ℕ0 )
8	2 7	pcmptcl	⊢ ( 𝜑 → ( 𝐺 : ℕ ⟶ ℕ ∧ seq 1 ( · , 𝐺 ) : ℕ ⟶ ℕ ) )
9	8	simprd	⊢ ( 𝜑 → seq 1 ( · , 𝐺 ) : ℕ ⟶ ℕ )
10	9 4	ffvelcdmd	⊢ ( 𝜑 → ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) ∈ ℕ )
11	1	1arithlem2	⊢ ( ( ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) ∈ ℕ ∧ 𝑞 ∈ ℙ ) → ( ( 𝑀 ‘ ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) ) ‘ 𝑞 ) = ( 𝑞 pCnt ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) ) )
12	10 11	sylan	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) → ( ( 𝑀 ‘ ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) ) ‘ 𝑞 ) = ( 𝑞 pCnt ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) ) )
13	7	adantr	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) → ∀ 𝑦 ∈ ℙ ( 𝐹 ‘ 𝑦 ) ∈ ℕ0 )
14	4	adantr	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) → 𝑁 ∈ ℕ )
15		simpr	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) → 𝑞 ∈ ℙ )
16		fveq2	⊢ ( 𝑦 = 𝑞 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑞 ) )
17	2 13 14 15 16	pcmpt	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) → ( 𝑞 pCnt ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) ) = if ( 𝑞 ≤ 𝑁 , ( 𝐹 ‘ 𝑞 ) , 0 ) )
18	14	nnred	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) → 𝑁 ∈ ℝ )
19		prmz	⊢ ( 𝑞 ∈ ℙ → 𝑞 ∈ ℤ )
20	19	zred	⊢ ( 𝑞 ∈ ℙ → 𝑞 ∈ ℝ )
21	20	adantl	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) → 𝑞 ∈ ℝ )
22	5	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑁 ≤ 𝑞 ) → ( 𝐹 ‘ 𝑞 ) = 0 )
23	22	ifeq2d	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑁 ≤ 𝑞 ) → if ( 𝑞 ≤ 𝑁 , ( 𝐹 ‘ 𝑞 ) , ( 𝐹 ‘ 𝑞 ) ) = if ( 𝑞 ≤ 𝑁 , ( 𝐹 ‘ 𝑞 ) , 0 ) )
24		ifid	⊢ if ( 𝑞 ≤ 𝑁 , ( 𝐹 ‘ 𝑞 ) , ( 𝐹 ‘ 𝑞 ) ) = ( 𝐹 ‘ 𝑞 )
25	23 24	eqtr3di	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑁 ≤ 𝑞 ) → if ( 𝑞 ≤ 𝑁 , ( 𝐹 ‘ 𝑞 ) , 0 ) = ( 𝐹 ‘ 𝑞 ) )
26		iftrue	⊢ ( 𝑞 ≤ 𝑁 → if ( 𝑞 ≤ 𝑁 , ( 𝐹 ‘ 𝑞 ) , 0 ) = ( 𝐹 ‘ 𝑞 ) )
27	26	adantl	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ≤ 𝑁 ) → if ( 𝑞 ≤ 𝑁 , ( 𝐹 ‘ 𝑞 ) , 0 ) = ( 𝐹 ‘ 𝑞 ) )
28	18 21 25 27	lecasei	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) → if ( 𝑞 ≤ 𝑁 , ( 𝐹 ‘ 𝑞 ) , 0 ) = ( 𝐹 ‘ 𝑞 ) )
29	12 17 28	3eqtrrd	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) → ( 𝐹 ‘ 𝑞 ) = ( ( 𝑀 ‘ ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) ) ‘ 𝑞 ) )
30	29	ralrimiva	⊢ ( 𝜑 → ∀ 𝑞 ∈ ℙ ( 𝐹 ‘ 𝑞 ) = ( ( 𝑀 ‘ ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) ) ‘ 𝑞 ) )
31	1	1arithlem3	⊢ ( ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) ∈ ℕ → ( 𝑀 ‘ ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) ) : ℙ ⟶ ℕ0 )
32	10 31	syl	⊢ ( 𝜑 → ( 𝑀 ‘ ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) ) : ℙ ⟶ ℕ0 )
33		ffn	⊢ ( 𝐹 : ℙ ⟶ ℕ0 → 𝐹 Fn ℙ )
34		ffn	⊢ ( ( 𝑀 ‘ ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) ) : ℙ ⟶ ℕ0 → ( 𝑀 ‘ ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) ) Fn ℙ )
35		eqfnfv	⊢ ( ( 𝐹 Fn ℙ ∧ ( 𝑀 ‘ ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) ) Fn ℙ ) → ( 𝐹 = ( 𝑀 ‘ ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) ) ↔ ∀ 𝑞 ∈ ℙ ( 𝐹 ‘ 𝑞 ) = ( ( 𝑀 ‘ ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) ) ‘ 𝑞 ) ) )
36	33 34 35	syl2an	⊢ ( ( 𝐹 : ℙ ⟶ ℕ0 ∧ ( 𝑀 ‘ ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) ) : ℙ ⟶ ℕ0 ) → ( 𝐹 = ( 𝑀 ‘ ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) ) ↔ ∀ 𝑞 ∈ ℙ ( 𝐹 ‘ 𝑞 ) = ( ( 𝑀 ‘ ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) ) ‘ 𝑞 ) ) )
37	3 32 36	syl2anc	⊢ ( 𝜑 → ( 𝐹 = ( 𝑀 ‘ ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) ) ↔ ∀ 𝑞 ∈ ℙ ( 𝐹 ‘ 𝑞 ) = ( ( 𝑀 ‘ ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) ) ‘ 𝑞 ) ) )
38	30 37	mpbird	⊢ ( 𝜑 → 𝐹 = ( 𝑀 ‘ ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) ) )
39		fveq2	⊢ ( 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) → ( 𝑀 ‘ 𝑥 ) = ( 𝑀 ‘ ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) ) )
40	39	rspceeqv	⊢ ( ( ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) ∈ ℕ ∧ 𝐹 = ( 𝑀 ‘ ( seq 1 ( · , 𝐺 ) ‘ 𝑁 ) ) ) → ∃ 𝑥 ∈ ℕ 𝐹 = ( 𝑀 ‘ 𝑥 ) )
41	10 38 40	syl2anc	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℕ 𝐹 = ( 𝑀 ‘ 𝑥 ) )