Metamath Proof Explorer

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 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℙ ) → ( 𝐹 ‘ 𝑦 ) ∈ ℕ0 )
7 6 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ℙ ( 𝐹 ‘ 𝑦 ) ∈ ℕ0 )
8 2 7 pcmptcl ⊢ ( 𝜑 → ( 𝐺 : ℕ ⟶ ℕ ∧ seq 1 ( · , 𝐺 ) : ℕ ⟶ ℕ ) )
9 8 simprd ⊢ ( 𝜑 → seq 1 ( · , 𝐺 ) : ℕ ⟶ ℕ )
10 9 4 ffvelrnd ⊢ ( 𝜑 → ( 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 ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℕ 𝐹 = ( 𝑀 ‘ 𝑥 ) )