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 ( 𝜑 → ∃ 𝑥 ∈ ℕ 𝐹 = ( 𝑀𝑥 ) )