Metamath Proof Explorer

Theorem bposlem3

Description: Lemma for bpos . Since the binomial coefficient does not have any primes in the range ( 2 N / 3 , N ] or ( 2 N , +oo ) by bposlem2 and prmfac1 , respectively, and it does not have any in the range ( N , 2 N ] by hypothesis, the product of the primes up through 2 N / 3 must be sufficient to compose the whole binomial coefficient. (Contributed by Mario Carneiro, 13-Mar-2014)

Ref Expression
Hypotheses bpos.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 5 ) )
bpos.2 ⊢ ( 𝜑 → ¬ ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) )
bpos.3 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) )
bpos.4 ⊢ 𝐾 = ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) )
Assertion bposlem3 ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) = ( ( 2 · 𝑁 ) C 𝑁 ) )

Proof

Step Hyp Ref Expression
1 bpos.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 5 ) )
2 bpos.2 ⊢ ( 𝜑 → ¬ ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) )
3 bpos.3 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) )
4 bpos.4 ⊢ 𝐾 = ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) )
5 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℙ ) → 𝑛 ∈ ℙ )
6 5nn ⊢ 5 ∈ ℕ
7 eluznn ⊢ ( ( 5 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 5 ) ) → 𝑁 ∈ ℕ )
8 6 1 7 sylancr ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
9 8 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
10 fzctr ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( 0 ... ( 2 · 𝑁 ) ) )
11 bccl2 ⊢ ( 𝑁 ∈ ( 0 ... ( 2 · 𝑁 ) ) → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ )
12 9 10 11 3syl ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℙ ) → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ )
14 5 13 pccld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℙ ) → ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ0 )
15 14 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℙ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ0 )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ∀ 𝑛 ∈ ℙ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ0 )
17 2nn ⊢ 2 ∈ ℕ
18 nnmulcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 2 · 𝑁 ) ∈ ℕ )
19 17 8 18 sylancr ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℕ )
20 19 nnred ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
21 3nn ⊢ 3 ∈ ℕ
22 nndivre ⊢ ( ( ( 2 · 𝑁 ) ∈ ℝ ∧ 3 ∈ ℕ ) → ( ( 2 · 𝑁 ) / 3 ) ∈ ℝ )
23 20 21 22 sylancl ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) / 3 ) ∈ ℝ )
24 23 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) ) ∈ ℤ )
25 4 24 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
26 3re ⊢ 3 ∈ ℝ
27 26 a1i ⊢ ( 𝜑 → 3 ∈ ℝ )
28 5re ⊢ 5 ∈ ℝ
29 28 a1i ⊢ ( 𝜑 → 5 ∈ ℝ )
30 8 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
31 3lt5 ⊢ 3 < 5
32 26 28 31 ltleii ⊢ 3 ≤ 5
33 32 a1i ⊢ ( 𝜑 → 3 ≤ 5 )
34 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) → 5 ≤ 𝑁 )
35 1 34 syl ⊢ ( 𝜑 → 5 ≤ 𝑁 )
36 27 29 30 33 35 letrd ⊢ ( 𝜑 → 3 ≤ 𝑁 )
37 2re ⊢ 2 ∈ ℝ
38 2pos ⊢ 0 < 2
39 37 38 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
40 lemul2 ⊢ ( ( 3 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 3 ≤ 𝑁 ↔ ( 2 · 3 ) ≤ ( 2 · 𝑁 ) ) )
41 26 39 40 mp3an13 ⊢ ( 𝑁 ∈ ℝ → ( 3 ≤ 𝑁 ↔ ( 2 · 3 ) ≤ ( 2 · 𝑁 ) ) )
42 30 41 syl ⊢ ( 𝜑 → ( 3 ≤ 𝑁 ↔ ( 2 · 3 ) ≤ ( 2 · 𝑁 ) ) )
43 36 42 mpbid ⊢ ( 𝜑 → ( 2 · 3 ) ≤ ( 2 · 𝑁 ) )
44 3pos ⊢ 0 < 3
45 26 44 pm3.2i ⊢ ( 3 ∈ ℝ ∧ 0 < 3 )
46 lemuldiv ⊢ ( ( 2 ∈ ℝ ∧ ( 2 · 𝑁 ) ∈ ℝ ∧ ( 3 ∈ ℝ ∧ 0 < 3 ) ) → ( ( 2 · 3 ) ≤ ( 2 · 𝑁 ) ↔ 2 ≤ ( ( 2 · 𝑁 ) / 3 ) ) )
47 37 45 46 mp3an13 ⊢ ( ( 2 · 𝑁 ) ∈ ℝ → ( ( 2 · 3 ) ≤ ( 2 · 𝑁 ) ↔ 2 ≤ ( ( 2 · 𝑁 ) / 3 ) ) )
48 20 47 syl ⊢ ( 𝜑 → ( ( 2 · 3 ) ≤ ( 2 · 𝑁 ) ↔ 2 ≤ ( ( 2 · 𝑁 ) / 3 ) ) )
49 43 48 mpbid ⊢ ( 𝜑 → 2 ≤ ( ( 2 · 𝑁 ) / 3 ) )
50 2z ⊢ 2 ∈ ℤ
51 flge ⊢ ( ( ( ( 2 · 𝑁 ) / 3 ) ∈ ℝ ∧ 2 ∈ ℤ ) → ( 2 ≤ ( ( 2 · 𝑁 ) / 3 ) ↔ 2 ≤ ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) ) ) )
52 23 50 51 sylancl ⊢ ( 𝜑 → ( 2 ≤ ( ( 2 · 𝑁 ) / 3 ) ↔ 2 ≤ ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) ) ) )
53 49 52 mpbid ⊢ ( 𝜑 → 2 ≤ ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) ) )
54 53 4 breqtrrdi ⊢ ( 𝜑 → 2 ≤ 𝐾 )
55 50 eluz1i ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝐾 ∈ ℤ ∧ 2 ≤ 𝐾 ) )
56 25 54 55 sylanbrc ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 2 ) )
57 eluz2nn ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) → 𝐾 ∈ ℕ )
58 56 57 syl ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
59 58 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → 𝐾 ∈ ℕ )
60 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℙ )
61 oveq1 ⊢ ( 𝑛 = 𝑝 → ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) = ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) )
62 3 16 59 60 61 pcmpt ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) ) = if ( 𝑝 ≤ 𝐾 , ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) , 0 ) )
63 iftrue ⊢ ( 𝑝 ≤ 𝐾 → if ( 𝑝 ≤ 𝐾 , ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) , 0 ) = ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) )
64 63 adantl ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝐾 ) → if ( 𝑝 ≤ 𝐾 , ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) , 0 ) = ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) )
65 iffalse ⊢ ( ¬ 𝑝 ≤ 𝐾 → if ( 𝑝 ≤ 𝐾 , ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) , 0 ) = 0 )
66 65 adantl ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ¬ 𝑝 ≤ 𝐾 ) → if ( 𝑝 ≤ 𝐾 , ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) , 0 ) = 0 )
67 25 zred ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
68 prmz ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
69 68 zred ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℝ )
70 ltnle ⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑝 ∈ ℝ ) → ( 𝐾 < 𝑝 ↔ ¬ 𝑝 ≤ 𝐾 ) )
71 67 69 70 syl2an ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝐾 < 𝑝 ↔ ¬ 𝑝 ≤ 𝐾 ) )
72 71 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ¬ 𝑝 ≤ 𝐾 ) → 𝐾 < 𝑝 )
73 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁 ) ) → 𝑁 ∈ ℕ )
74 simplr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁 ) ) → 𝑝 ∈ ℙ )
75 37 a1i ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁 ) ) → 2 ∈ ℝ )
76 67 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁 ) ) → 𝐾 ∈ ℝ )
77 68 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁 ) ) → 𝑝 ∈ ℤ )
78 77 zred ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁 ) ) → 𝑝 ∈ ℝ )
79 54 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁 ) ) → 2 ≤ 𝐾 )
80 simprl ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁 ) ) → 𝐾 < 𝑝 )
81 75 76 78 79 80 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁 ) ) → 2 < 𝑝 )
82 4 80 eqbrtrrid ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁 ) ) → ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) ) < 𝑝 )
83 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁 ) ) → ( ( 2 · 𝑁 ) / 3 ) ∈ ℝ )
84 fllt ⊢ ( ( ( ( 2 · 𝑁 ) / 3 ) ∈ ℝ ∧ 𝑝 ∈ ℤ ) → ( ( ( 2 · 𝑁 ) / 3 ) < 𝑝 ↔ ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) ) < 𝑝 ) )
85 83 77 84 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁 ) ) → ( ( ( 2 · 𝑁 ) / 3 ) < 𝑝 ↔ ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) ) < 𝑝 ) )
86 82 85 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁 ) ) → ( ( 2 · 𝑁 ) / 3 ) < 𝑝 )
87 simprr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁 ) ) → 𝑝 ≤ 𝑁 )
88 73 74 81 86 87 bposlem2 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁 ) ) → ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) = 0 )
89 88 expr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝐾 < 𝑝 ) → ( 𝑝 ≤ 𝑁 → ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) = 0 ) )
90 rspe ⊢ ( ( 𝑝 ∈ ℙ ∧ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) ) → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) )
91 90 adantll ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) ) → ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) )
92 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) ) → ¬ ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) )
93 91 92 pm2.21dd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) ) → ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) = 0 )
94 93 expr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑁 < 𝑝 ) → ( 𝑝 ≤ ( 2 · 𝑁 ) → ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) = 0 ) )
95 12 nnzd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℤ )
96 9 faccld ⊢ ( 𝜑 → ( ! ‘ 𝑁 ) ∈ ℕ )
97 96 96 nnmulcld ⊢ ( 𝜑 → ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ∈ ℕ )
98 97 nnzd ⊢ ( 𝜑 → ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ∈ ℤ )
99 dvdsmul1 ⊢ ( ( ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℤ ∧ ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ∈ ℤ ) → ( ( 2 · 𝑁 ) C 𝑁 ) ∥ ( ( ( 2 · 𝑁 ) C 𝑁 ) · ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) )
100 95 98 99 syl2anc ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) C 𝑁 ) ∥ ( ( ( 2 · 𝑁 ) C 𝑁 ) · ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) )
101 bcctr ⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 · 𝑁 ) C 𝑁 ) = ( ( ! ‘ ( 2 · 𝑁 ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) )
102 9 101 syl ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) C 𝑁 ) = ( ( ! ‘ ( 2 · 𝑁 ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) )
103 102 oveq1d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) C 𝑁 ) · ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) = ( ( ( ! ‘ ( 2 · 𝑁 ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) · ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) )
104 19 nnnn0d ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℕ0 )
105 104 faccld ⊢ ( 𝜑 → ( ! ‘ ( 2 · 𝑁 ) ) ∈ ℕ )
106 105 nncnd ⊢ ( 𝜑 → ( ! ‘ ( 2 · 𝑁 ) ) ∈ ℂ )
107 97 nncnd ⊢ ( 𝜑 → ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ∈ ℂ )
108 97 nnne0d ⊢ ( 𝜑 → ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ≠ 0 )
109 106 107 108 divcan1d ⊢ ( 𝜑 → ( ( ( ! ‘ ( 2 · 𝑁 ) ) / ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) · ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) = ( ! ‘ ( 2 · 𝑁 ) ) )
110 103 109 eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) C 𝑁 ) · ( ( ! ‘ 𝑁 ) · ( ! ‘ 𝑁 ) ) ) = ( ! ‘ ( 2 · 𝑁 ) ) )
111 100 110 breqtrd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) C 𝑁 ) ∥ ( ! ‘ ( 2 · 𝑁 ) ) )
112 111 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ( 2 · 𝑁 ) C 𝑁 ) ∥ ( ! ‘ ( 2 · 𝑁 ) ) )
113 68 adantl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℤ )
114 95 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℤ )
115 105 nnzd ⊢ ( 𝜑 → ( ! ‘ ( 2 · 𝑁 ) ) ∈ ℤ )
116 115 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ! ‘ ( 2 · 𝑁 ) ) ∈ ℤ )
117 dvdstr ⊢ ( ( 𝑝 ∈ ℤ ∧ ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℤ ∧ ( ! ‘ ( 2 · 𝑁 ) ) ∈ ℤ ) → ( ( 𝑝 ∥ ( ( 2 · 𝑁 ) C 𝑁 ) ∧ ( ( 2 · 𝑁 ) C 𝑁 ) ∥ ( ! ‘ ( 2 · 𝑁 ) ) ) → 𝑝 ∥ ( ! ‘ ( 2 · 𝑁 ) ) ) )
118 113 114 116 117 syl3anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ∥ ( ( 2 · 𝑁 ) C 𝑁 ) ∧ ( ( 2 · 𝑁 ) C 𝑁 ) ∥ ( ! ‘ ( 2 · 𝑁 ) ) ) → 𝑝 ∥ ( ! ‘ ( 2 · 𝑁 ) ) ) )
119 112 118 mpan2d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( ( 2 · 𝑁 ) C 𝑁 ) → 𝑝 ∥ ( ! ‘ ( 2 · 𝑁 ) ) ) )
120 prmfac1 ⊢ ( ( ( 2 · 𝑁 ) ∈ ℕ0 ∧ 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( ! ‘ ( 2 · 𝑁 ) ) ) → 𝑝 ≤ ( 2 · 𝑁 ) )
121 120 3expia ⊢ ( ( ( 2 · 𝑁 ) ∈ ℕ0 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( ! ‘ ( 2 · 𝑁 ) ) → 𝑝 ≤ ( 2 · 𝑁 ) ) )
122 104 121 sylan ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( ! ‘ ( 2 · 𝑁 ) ) → 𝑝 ≤ ( 2 · 𝑁 ) ) )
123 119 122 syld ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( ( 2 · 𝑁 ) C 𝑁 ) → 𝑝 ≤ ( 2 · 𝑁 ) ) )
124 123 con3d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ¬ 𝑝 ≤ ( 2 · 𝑁 ) → ¬ 𝑝 ∥ ( ( 2 · 𝑁 ) C 𝑁 ) ) )
125 id ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℙ )
126 pceq0 ⊢ ( ( 𝑝 ∈ ℙ ∧ ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ ) → ( ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) = 0 ↔ ¬ 𝑝 ∥ ( ( 2 · 𝑁 ) C 𝑁 ) ) )
127 125 12 126 syl2anr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) = 0 ↔ ¬ 𝑝 ∥ ( ( 2 · 𝑁 ) C 𝑁 ) ) )
128 124 127 sylibrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ¬ 𝑝 ≤ ( 2 · 𝑁 ) → ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) = 0 ) )
129 128 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑁 < 𝑝 ) → ( ¬ 𝑝 ≤ ( 2 · 𝑁 ) → ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) = 0 ) )
130 94 129 pm2.61d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑁 < 𝑝 ) → ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) = 0 )
131 130 ex ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑁 < 𝑝 → ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) = 0 ) )
132 131 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝐾 < 𝑝 ) → ( 𝑁 < 𝑝 → ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) = 0 ) )
133 lelttric ⊢ ( ( 𝑝 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑝 ≤ 𝑁 ∨ 𝑁 < 𝑝 ) )
134 69 30 133 syl2anr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ≤ 𝑁 ∨ 𝑁 < 𝑝 ) )
135 134 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝐾 < 𝑝 ) → ( 𝑝 ≤ 𝑁 ∨ 𝑁 < 𝑝 ) )
136 89 132 135 mpjaod ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝐾 < 𝑝 ) → ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) = 0 )
137 72 136 syldan ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ¬ 𝑝 ≤ 𝐾 ) → ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) = 0 )
138 66 137 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ ¬ 𝑝 ≤ 𝐾 ) → if ( 𝑝 ≤ 𝐾 , ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) , 0 ) = ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) )
139 64 138 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → if ( 𝑝 ≤ 𝐾 , ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) , 0 ) = ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) )
140 62 139 eqtrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) ) = ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) )
141 140 ralrimiva ⊢ ( 𝜑 → ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) ) = ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) )
142 3 15 pcmptcl ⊢ ( 𝜑 → ( 𝐹 : ℕ ⟶ ℕ ∧ seq 1 ( · , 𝐹 ) : ℕ ⟶ ℕ ) )
143 142 simprd ⊢ ( 𝜑 → seq 1 ( · , 𝐹 ) : ℕ ⟶ ℕ )
144 143 58 ffvelcdmd ⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) ∈ ℕ )
145 144 nnnn0d ⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) ∈ ℕ0 )
146 12 nnnn0d ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ0 )
147 pc11 ⊢ ( ( ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) ∈ ℕ0 ∧ ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ0 ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) = ( ( 2 · 𝑁 ) C 𝑁 ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) ) = ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) )
148 145 146 147 syl2anc ⊢ ( 𝜑 → ( ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) = ( ( 2 · 𝑁 ) C 𝑁 ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) ) = ( 𝑝 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) )
149 141 148 mpbird ⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) = ( ( 2 · 𝑁 ) C 𝑁 ) )