ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pcmpt GIF version

Theorem pcmpt 12340
Description: Construct a function with given prime count characteristics. (Contributed by Mario Carneiro, 12-Mar-2014.)
Hypotheses
Ref Expression
pcmpt.1 𝐹 = (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, (𝑛↑𝐴), 1))
pcmpt.2 (πœ‘ β†’ βˆ€π‘› ∈ β„™ 𝐴 ∈ β„•0)
pcmpt.3 (πœ‘ β†’ 𝑁 ∈ β„•)
pcmpt.4 (πœ‘ β†’ 𝑃 ∈ β„™)
pcmpt.5 (𝑛 = 𝑃 β†’ 𝐴 = 𝐡)
Assertion
Ref Expression
pcmpt (πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑁, 𝐡, 0))
Distinct variable groups:   𝐡,𝑛   𝑃,𝑛
Allowed substitution hints:   πœ‘(𝑛)   𝐴(𝑛)   𝐹(𝑛)   𝑁(𝑛)

Proof of Theorem pcmpt
Dummy variables π‘˜ 𝑝 𝑖 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pcmpt.3 . 2 (πœ‘ β†’ 𝑁 ∈ β„•)
2 fveq2 5515 . . . . . 6 (𝑝 = 1 β†’ (seq1( Β· , 𝐹)β€˜π‘) = (seq1( Β· , 𝐹)β€˜1))
32oveq2d 5890 . . . . 5 (𝑝 = 1 β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = (𝑃 pCnt (seq1( Β· , 𝐹)β€˜1)))
4 breq2 4007 . . . . . 6 (𝑝 = 1 β†’ (𝑃 ≀ 𝑝 ↔ 𝑃 ≀ 1))
54ifbid 3555 . . . . 5 (𝑝 = 1 β†’ if(𝑃 ≀ 𝑝, 𝐡, 0) = if(𝑃 ≀ 1, 𝐡, 0))
63, 5eqeq12d 2192 . . . 4 (𝑝 = 1 β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑝, 𝐡, 0) ↔ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜1)) = if(𝑃 ≀ 1, 𝐡, 0)))
76imbi2d 230 . . 3 (𝑝 = 1 β†’ ((πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑝, 𝐡, 0)) ↔ (πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜1)) = if(𝑃 ≀ 1, 𝐡, 0))))
8 fveq2 5515 . . . . . 6 (𝑝 = π‘˜ β†’ (seq1( Β· , 𝐹)β€˜π‘) = (seq1( Β· , 𝐹)β€˜π‘˜))
98oveq2d 5890 . . . . 5 (𝑝 = π‘˜ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)))
10 breq2 4007 . . . . . 6 (𝑝 = π‘˜ β†’ (𝑃 ≀ 𝑝 ↔ 𝑃 ≀ π‘˜))
1110ifbid 3555 . . . . 5 (𝑝 = π‘˜ β†’ if(𝑃 ≀ 𝑝, 𝐡, 0) = if(𝑃 ≀ π‘˜, 𝐡, 0))
129, 11eqeq12d 2192 . . . 4 (𝑝 = π‘˜ β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑝, 𝐡, 0) ↔ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0)))
1312imbi2d 230 . . 3 (𝑝 = π‘˜ β†’ ((πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑝, 𝐡, 0)) ↔ (πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0))))
14 fveq2 5515 . . . . . 6 (𝑝 = (π‘˜ + 1) β†’ (seq1( Β· , 𝐹)β€˜π‘) = (seq1( Β· , 𝐹)β€˜(π‘˜ + 1)))
1514oveq2d 5890 . . . . 5 (𝑝 = (π‘˜ + 1) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))))
16 breq2 4007 . . . . . 6 (𝑝 = (π‘˜ + 1) β†’ (𝑃 ≀ 𝑝 ↔ 𝑃 ≀ (π‘˜ + 1)))
1716ifbid 3555 . . . . 5 (𝑝 = (π‘˜ + 1) β†’ if(𝑃 ≀ 𝑝, 𝐡, 0) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0))
1815, 17eqeq12d 2192 . . . 4 (𝑝 = (π‘˜ + 1) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑝, 𝐡, 0) ↔ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0)))
1918imbi2d 230 . . 3 (𝑝 = (π‘˜ + 1) β†’ ((πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑝, 𝐡, 0)) ↔ (πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0))))
20 fveq2 5515 . . . . . 6 (𝑝 = 𝑁 β†’ (seq1( Β· , 𝐹)β€˜π‘) = (seq1( Β· , 𝐹)β€˜π‘))
2120oveq2d 5890 . . . . 5 (𝑝 = 𝑁 β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)))
22 breq2 4007 . . . . . 6 (𝑝 = 𝑁 β†’ (𝑃 ≀ 𝑝 ↔ 𝑃 ≀ 𝑁))
2322ifbid 3555 . . . . 5 (𝑝 = 𝑁 β†’ if(𝑃 ≀ 𝑝, 𝐡, 0) = if(𝑃 ≀ 𝑁, 𝐡, 0))
2421, 23eqeq12d 2192 . . . 4 (𝑝 = 𝑁 β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑝, 𝐡, 0) ↔ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑁, 𝐡, 0)))
2524imbi2d 230 . . 3 (𝑝 = 𝑁 β†’ ((πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑝, 𝐡, 0)) ↔ (πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑁, 𝐡, 0))))
26 pcmpt.4 . . . . 5 (πœ‘ β†’ 𝑃 ∈ β„™)
27 pc1 12304 . . . . 5 (𝑃 ∈ β„™ β†’ (𝑃 pCnt 1) = 0)
2826, 27syl 14 . . . 4 (πœ‘ β†’ (𝑃 pCnt 1) = 0)
29 1zzd 9279 . . . . . . 7 (πœ‘ β†’ 1 ∈ β„€)
30 elnnuz 9563 . . . . . . . 8 (𝑖 ∈ β„• ↔ 𝑖 ∈ (β„€β‰₯β€˜1))
31 simpr 110 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ 𝑖 ∈ β„•)
3231adantr 276 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑖 ∈ β„•) ∧ 𝑖 ∈ β„™) β†’ 𝑖 ∈ β„•)
33 simpr 110 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑖 ∈ β„•) ∧ 𝑖 ∈ β„™) β†’ 𝑖 ∈ β„™)
34 pcmpt.2 . . . . . . . . . . . . . 14 (πœ‘ β†’ βˆ€π‘› ∈ β„™ 𝐴 ∈ β„•0)
3534ad2antrr 488 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑖 ∈ β„•) ∧ 𝑖 ∈ β„™) β†’ βˆ€π‘› ∈ β„™ 𝐴 ∈ β„•0)
36 nfcsb1v 3090 . . . . . . . . . . . . . . 15 Ⅎ𝑛⦋𝑖 / π‘›β¦Œπ΄
3736nfel1 2330 . . . . . . . . . . . . . 14 Ⅎ𝑛⦋𝑖 / π‘›β¦Œπ΄ ∈ β„•0
38 csbeq1a 3066 . . . . . . . . . . . . . . 15 (𝑛 = 𝑖 β†’ 𝐴 = ⦋𝑖 / π‘›β¦Œπ΄)
3938eleq1d 2246 . . . . . . . . . . . . . 14 (𝑛 = 𝑖 β†’ (𝐴 ∈ β„•0 ↔ ⦋𝑖 / π‘›β¦Œπ΄ ∈ β„•0))
4037, 39rspc 2835 . . . . . . . . . . . . 13 (𝑖 ∈ β„™ β†’ (βˆ€π‘› ∈ β„™ 𝐴 ∈ β„•0 β†’ ⦋𝑖 / π‘›β¦Œπ΄ ∈ β„•0))
4133, 35, 40sylc 62 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑖 ∈ β„•) ∧ 𝑖 ∈ β„™) β†’ ⦋𝑖 / π‘›β¦Œπ΄ ∈ β„•0)
4232, 41nnexpcld 10675 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑖 ∈ β„•) ∧ 𝑖 ∈ β„™) β†’ (𝑖↑⦋𝑖 / π‘›β¦Œπ΄) ∈ β„•)
43 1nn 8929 . . . . . . . . . . . 12 1 ∈ β„•
4443a1i 9 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑖 ∈ β„•) ∧ Β¬ 𝑖 ∈ β„™) β†’ 1 ∈ β„•)
45 prmdc 12129 . . . . . . . . . . . 12 (𝑖 ∈ β„• β†’ DECID 𝑖 ∈ β„™)
4645adantl 277 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ DECID 𝑖 ∈ β„™)
4742, 44, 46ifcldadc 3563 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ if(𝑖 ∈ β„™, (𝑖↑⦋𝑖 / π‘›β¦Œπ΄), 1) ∈ β„•)
48 nfcv 2319 . . . . . . . . . . 11 Ⅎ𝑛𝑖
4948nfel1 2330 . . . . . . . . . . . 12 Ⅎ𝑛 𝑖 ∈ β„™
50 nfcv 2319 . . . . . . . . . . . . 13 Ⅎ𝑛↑
5148, 50, 36nfov 5904 . . . . . . . . . . . 12 Ⅎ𝑛(𝑖↑⦋𝑖 / π‘›β¦Œπ΄)
52 nfcv 2319 . . . . . . . . . . . 12 Ⅎ𝑛1
5349, 51, 52nfif 3562 . . . . . . . . . . 11 Ⅎ𝑛if(𝑖 ∈ β„™, (𝑖↑⦋𝑖 / π‘›β¦Œπ΄), 1)
54 eleq1 2240 . . . . . . . . . . . 12 (𝑛 = 𝑖 β†’ (𝑛 ∈ β„™ ↔ 𝑖 ∈ β„™))
55 id 19 . . . . . . . . . . . . 13 (𝑛 = 𝑖 β†’ 𝑛 = 𝑖)
5655, 38oveq12d 5892 . . . . . . . . . . . 12 (𝑛 = 𝑖 β†’ (𝑛↑𝐴) = (𝑖↑⦋𝑖 / π‘›β¦Œπ΄))
5754, 56ifbieq1d 3556 . . . . . . . . . . 11 (𝑛 = 𝑖 β†’ if(𝑛 ∈ β„™, (𝑛↑𝐴), 1) = if(𝑖 ∈ β„™, (𝑖↑⦋𝑖 / π‘›β¦Œπ΄), 1))
58 pcmpt.1 . . . . . . . . . . 11 𝐹 = (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, (𝑛↑𝐴), 1))
5948, 53, 57, 58fvmptf 5608 . . . . . . . . . 10 ((𝑖 ∈ β„• ∧ if(𝑖 ∈ β„™, (𝑖↑⦋𝑖 / π‘›β¦Œπ΄), 1) ∈ β„•) β†’ (πΉβ€˜π‘–) = if(𝑖 ∈ β„™, (𝑖↑⦋𝑖 / π‘›β¦Œπ΄), 1))
6031, 47, 59syl2anc 411 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ (πΉβ€˜π‘–) = if(𝑖 ∈ β„™, (𝑖↑⦋𝑖 / π‘›β¦Œπ΄), 1))
6160, 47eqeltrd 2254 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ (πΉβ€˜π‘–) ∈ β„•)
6230, 61sylan2br 288 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜1)) β†’ (πΉβ€˜π‘–) ∈ β„•)
63 nnmulcl 8939 . . . . . . . 8 ((𝑖 ∈ β„• ∧ 𝑗 ∈ β„•) β†’ (𝑖 Β· 𝑗) ∈ β„•)
6463adantl 277 . . . . . . 7 ((πœ‘ ∧ (𝑖 ∈ β„• ∧ 𝑗 ∈ β„•)) β†’ (𝑖 Β· 𝑗) ∈ β„•)
6529, 62, 64seq3-1 10459 . . . . . 6 (πœ‘ β†’ (seq1( Β· , 𝐹)β€˜1) = (πΉβ€˜1))
66 1nprm 12113 . . . . . . . . . 10 Β¬ 1 ∈ β„™
67 eleq1 2240 . . . . . . . . . 10 (𝑛 = 1 β†’ (𝑛 ∈ β„™ ↔ 1 ∈ β„™))
6866, 67mtbiri 675 . . . . . . . . 9 (𝑛 = 1 β†’ Β¬ 𝑛 ∈ β„™)
6968iffalsed 3544 . . . . . . . 8 (𝑛 = 1 β†’ if(𝑛 ∈ β„™, (𝑛↑𝐴), 1) = 1)
70 1ex 7951 . . . . . . . 8 1 ∈ V
7169, 58, 70fvmpt 5593 . . . . . . 7 (1 ∈ β„• β†’ (πΉβ€˜1) = 1)
7243, 71ax-mp 5 . . . . . 6 (πΉβ€˜1) = 1
7365, 72eqtrdi 2226 . . . . 5 (πœ‘ β†’ (seq1( Β· , 𝐹)β€˜1) = 1)
7473oveq2d 5890 . . . 4 (πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜1)) = (𝑃 pCnt 1))
75 prmgt1 12131 . . . . . . 7 (𝑃 ∈ β„™ β†’ 1 < 𝑃)
76 1z 9278 . . . . . . . 8 1 ∈ β„€
77 prmz 12110 . . . . . . . 8 (𝑃 ∈ β„™ β†’ 𝑃 ∈ β„€)
78 zltnle 9298 . . . . . . . 8 ((1 ∈ β„€ ∧ 𝑃 ∈ β„€) β†’ (1 < 𝑃 ↔ Β¬ 𝑃 ≀ 1))
7976, 77, 78sylancr 414 . . . . . . 7 (𝑃 ∈ β„™ β†’ (1 < 𝑃 ↔ Β¬ 𝑃 ≀ 1))
8075, 79mpbid 147 . . . . . 6 (𝑃 ∈ β„™ β†’ Β¬ 𝑃 ≀ 1)
8180iffalsed 3544 . . . . 5 (𝑃 ∈ β„™ β†’ if(𝑃 ≀ 1, 𝐡, 0) = 0)
8226, 81syl 14 . . . 4 (πœ‘ β†’ if(𝑃 ≀ 1, 𝐡, 0) = 0)
8328, 74, 823eqtr4d 2220 . . 3 (πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜1)) = if(𝑃 ≀ 1, 𝐡, 0))
8426adantr 276 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ 𝑃 ∈ β„™)
8558, 34pcmptcl 12339 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝐹:β„•βŸΆβ„• ∧ seq1( Β· , 𝐹):β„•βŸΆβ„•))
8685simpld 112 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐹:β„•βŸΆβ„•)
87 peano2nn 8930 . . . . . . . . . . . . . . 15 (π‘˜ ∈ β„• β†’ (π‘˜ + 1) ∈ β„•)
88 ffvelcdm 5649 . . . . . . . . . . . . . . 15 ((𝐹:β„•βŸΆβ„• ∧ (π‘˜ + 1) ∈ β„•) β†’ (πΉβ€˜(π‘˜ + 1)) ∈ β„•)
8986, 87, 88syl2an 289 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜(π‘˜ + 1)) ∈ β„•)
9089adantrr 479 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (πΉβ€˜(π‘˜ + 1)) ∈ β„•)
9184, 90pccld 12299 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (𝑃 pCnt (πΉβ€˜(π‘˜ + 1))) ∈ β„•0)
9291nn0cnd 9230 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (𝑃 pCnt (πΉβ€˜(π‘˜ + 1))) ∈ β„‚)
9392addid2d 8106 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (0 + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))) = (𝑃 pCnt (πΉβ€˜(π‘˜ + 1))))
9487ad2antrl 490 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (π‘˜ + 1) ∈ β„•)
9587ad2antlr 489 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ (π‘˜ + 1) ∈ β„™) β†’ (π‘˜ + 1) ∈ β„•)
96 simpr 110 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ (π‘˜ + 1) ∈ β„™) β†’ (π‘˜ + 1) ∈ β„™)
9734ad2antrr 488 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ (π‘˜ + 1) ∈ β„™) β†’ βˆ€π‘› ∈ β„™ 𝐴 ∈ β„•0)
98 nfcsb1v 3090 . . . . . . . . . . . . . . . . . . 19 Ⅎ𝑛⦋(π‘˜ + 1) / π‘›β¦Œπ΄
9998nfel1 2330 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑛⦋(π‘˜ + 1) / π‘›β¦Œπ΄ ∈ β„•0
100 csbeq1a 3066 . . . . . . . . . . . . . . . . . . 19 (𝑛 = (π‘˜ + 1) β†’ 𝐴 = ⦋(π‘˜ + 1) / π‘›β¦Œπ΄)
101100eleq1d 2246 . . . . . . . . . . . . . . . . . 18 (𝑛 = (π‘˜ + 1) β†’ (𝐴 ∈ β„•0 ↔ ⦋(π‘˜ + 1) / π‘›β¦Œπ΄ ∈ β„•0))
10299, 101rspc 2835 . . . . . . . . . . . . . . . . 17 ((π‘˜ + 1) ∈ β„™ β†’ (βˆ€π‘› ∈ β„™ 𝐴 ∈ β„•0 β†’ ⦋(π‘˜ + 1) / π‘›β¦Œπ΄ ∈ β„•0))
10396, 97, 102sylc 62 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ (π‘˜ + 1) ∈ β„™) β†’ ⦋(π‘˜ + 1) / π‘›β¦Œπ΄ ∈ β„•0)
10495, 103nnexpcld 10675 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ (π‘˜ + 1) ∈ β„™) β†’ ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄) ∈ β„•)
10543a1i 9 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ Β¬ (π‘˜ + 1) ∈ β„™) β†’ 1 ∈ β„•)
10687adantl 277 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘˜ + 1) ∈ β„•)
107 prmdc 12129 . . . . . . . . . . . . . . . 16 ((π‘˜ + 1) ∈ β„• β†’ DECID (π‘˜ + 1) ∈ β„™)
108106, 107syl 14 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ DECID (π‘˜ + 1) ∈ β„™)
109104, 105, 108ifcldadc 3563 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1) ∈ β„•)
110109adantrr 479 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1) ∈ β„•)
111 nfcv 2319 . . . . . . . . . . . . . 14 Ⅎ𝑛(π‘˜ + 1)
112 nfv 1528 . . . . . . . . . . . . . . 15 Ⅎ𝑛(π‘˜ + 1) ∈ β„™
113111, 50, 98nfov 5904 . . . . . . . . . . . . . . 15 Ⅎ𝑛((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄)
114112, 113, 52nfif 3562 . . . . . . . . . . . . . 14 Ⅎ𝑛if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1)
115 eleq1 2240 . . . . . . . . . . . . . . 15 (𝑛 = (π‘˜ + 1) β†’ (𝑛 ∈ β„™ ↔ (π‘˜ + 1) ∈ β„™))
116 id 19 . . . . . . . . . . . . . . . 16 (𝑛 = (π‘˜ + 1) β†’ 𝑛 = (π‘˜ + 1))
117116, 100oveq12d 5892 . . . . . . . . . . . . . . 15 (𝑛 = (π‘˜ + 1) β†’ (𝑛↑𝐴) = ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄))
118115, 117ifbieq1d 3556 . . . . . . . . . . . . . 14 (𝑛 = (π‘˜ + 1) β†’ if(𝑛 ∈ β„™, (𝑛↑𝐴), 1) = if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1))
119111, 114, 118, 58fvmptf 5608 . . . . . . . . . . . . 13 (((π‘˜ + 1) ∈ β„• ∧ if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1) ∈ β„•) β†’ (πΉβ€˜(π‘˜ + 1)) = if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1))
12094, 110, 119syl2anc 411 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (πΉβ€˜(π‘˜ + 1)) = if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1))
121 simprr 531 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (π‘˜ + 1) = 𝑃)
122121, 84eqeltrd 2254 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (π‘˜ + 1) ∈ β„™)
123122iftrued 3541 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1) = ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄))
124121csbeq1d 3064 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ ⦋(π‘˜ + 1) / π‘›β¦Œπ΄ = ⦋𝑃 / π‘›β¦Œπ΄)
125 nfcvd 2320 . . . . . . . . . . . . . . . 16 (𝑃 ∈ β„™ β†’ Ⅎ𝑛𝐡)
126 pcmpt.5 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑃 β†’ 𝐴 = 𝐡)
127125, 126csbiegf 3100 . . . . . . . . . . . . . . 15 (𝑃 ∈ β„™ β†’ ⦋𝑃 / π‘›β¦Œπ΄ = 𝐡)
12884, 127syl 14 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ ⦋𝑃 / π‘›β¦Œπ΄ = 𝐡)
129124, 128eqtrd 2210 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ ⦋(π‘˜ + 1) / π‘›β¦Œπ΄ = 𝐡)
130121, 129oveq12d 5892 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄) = (𝑃↑𝐡))
131120, 123, 1303eqtrd 2214 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (πΉβ€˜(π‘˜ + 1)) = (𝑃↑𝐡))
132131oveq2d 5890 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (𝑃 pCnt (πΉβ€˜(π‘˜ + 1))) = (𝑃 pCnt (𝑃↑𝐡)))
133126eleq1d 2246 . . . . . . . . . . . . . 14 (𝑛 = 𝑃 β†’ (𝐴 ∈ β„•0 ↔ 𝐡 ∈ β„•0))
134133rspcv 2837 . . . . . . . . . . . . 13 (𝑃 ∈ β„™ β†’ (βˆ€π‘› ∈ β„™ 𝐴 ∈ β„•0 β†’ 𝐡 ∈ β„•0))
13526, 34, 134sylc 62 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐡 ∈ β„•0)
136135adantr 276 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ 𝐡 ∈ β„•0)
137 pcidlem 12321 . . . . . . . . . . 11 ((𝑃 ∈ β„™ ∧ 𝐡 ∈ β„•0) β†’ (𝑃 pCnt (𝑃↑𝐡)) = 𝐡)
13826, 136, 137syl2an2r 595 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (𝑃 pCnt (𝑃↑𝐡)) = 𝐡)
13993, 132, 1383eqtrd 2214 . . . . . . . . 9 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (0 + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))) = 𝐡)
140 oveq1 5881 . . . . . . . . . 10 ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = 0 β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))) = (0 + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))))
141140eqeq1d 2186 . . . . . . . . 9 ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = 0 β†’ (((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))) = 𝐡 ↔ (0 + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))) = 𝐡))
142139, 141syl5ibrcom 157 . . . . . . . 8 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = 0 β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))) = 𝐡))
143 nnre 8925 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„• β†’ π‘˜ ∈ ℝ)
144143ltp1d 8886 . . . . . . . . . . . . 13 (π‘˜ ∈ β„• β†’ π‘˜ < (π‘˜ + 1))
145 nnz 9271 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„€)
14687nnzd 9373 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„• β†’ (π‘˜ + 1) ∈ β„€)
147 zltnle 9298 . . . . . . . . . . . . . 14 ((π‘˜ ∈ β„€ ∧ (π‘˜ + 1) ∈ β„€) β†’ (π‘˜ < (π‘˜ + 1) ↔ Β¬ (π‘˜ + 1) ≀ π‘˜))
148145, 146, 147syl2anc 411 . . . . . . . . . . . . 13 (π‘˜ ∈ β„• β†’ (π‘˜ < (π‘˜ + 1) ↔ Β¬ (π‘˜ + 1) ≀ π‘˜))
149144, 148mpbid 147 . . . . . . . . . . . 12 (π‘˜ ∈ β„• β†’ Β¬ (π‘˜ + 1) ≀ π‘˜)
150149ad2antrl 490 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ Β¬ (π‘˜ + 1) ≀ π‘˜)
151121breq1d 4013 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ ((π‘˜ + 1) ≀ π‘˜ ↔ 𝑃 ≀ π‘˜))
152150, 151mtbid 672 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ Β¬ 𝑃 ≀ π‘˜)
153152iffalsed 3544 . . . . . . . . 9 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ if(𝑃 ≀ π‘˜, 𝐡, 0) = 0)
154153eqeq2d 2189 . . . . . . . 8 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0) ↔ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = 0))
155 simpr 110 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ β„•)
156 nnuz 9562 . . . . . . . . . . . . . 14 β„• = (β„€β‰₯β€˜1)
157155, 156eleqtrdi 2270 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ (β„€β‰₯β€˜1))
15862adantlr 477 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑖 ∈ (β„€β‰₯β€˜1)) β†’ (πΉβ€˜π‘–) ∈ β„•)
15963adantl 277 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ (𝑖 ∈ β„• ∧ 𝑗 ∈ β„•)) β†’ (𝑖 Β· 𝑗) ∈ β„•)
160157, 158, 159seq3p1 10461 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (seq1( Β· , 𝐹)β€˜(π‘˜ + 1)) = ((seq1( Β· , 𝐹)β€˜π‘˜) Β· (πΉβ€˜(π‘˜ + 1))))
161160oveq2d 5890 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = (𝑃 pCnt ((seq1( Β· , 𝐹)β€˜π‘˜) Β· (πΉβ€˜(π‘˜ + 1)))))
16226adantr 276 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 𝑃 ∈ β„™)
16385simprd 114 . . . . . . . . . . . . . 14 (πœ‘ β†’ seq1( Β· , 𝐹):β„•βŸΆβ„•)
164163ffvelcdmda 5651 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (seq1( Β· , 𝐹)β€˜π‘˜) ∈ β„•)
165 nnz 9271 . . . . . . . . . . . . . 14 ((seq1( Β· , 𝐹)β€˜π‘˜) ∈ β„• β†’ (seq1( Β· , 𝐹)β€˜π‘˜) ∈ β„€)
166 nnne0 8946 . . . . . . . . . . . . . 14 ((seq1( Β· , 𝐹)β€˜π‘˜) ∈ β„• β†’ (seq1( Β· , 𝐹)β€˜π‘˜) β‰  0)
167165, 166jca 306 . . . . . . . . . . . . 13 ((seq1( Β· , 𝐹)β€˜π‘˜) ∈ β„• β†’ ((seq1( Β· , 𝐹)β€˜π‘˜) ∈ β„€ ∧ (seq1( Β· , 𝐹)β€˜π‘˜) β‰  0))
168164, 167syl 14 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((seq1( Β· , 𝐹)β€˜π‘˜) ∈ β„€ ∧ (seq1( Β· , 𝐹)β€˜π‘˜) β‰  0))
169 nnz 9271 . . . . . . . . . . . . . 14 ((πΉβ€˜(π‘˜ + 1)) ∈ β„• β†’ (πΉβ€˜(π‘˜ + 1)) ∈ β„€)
170 nnne0 8946 . . . . . . . . . . . . . 14 ((πΉβ€˜(π‘˜ + 1)) ∈ β„• β†’ (πΉβ€˜(π‘˜ + 1)) β‰  0)
171169, 170jca 306 . . . . . . . . . . . . 13 ((πΉβ€˜(π‘˜ + 1)) ∈ β„• β†’ ((πΉβ€˜(π‘˜ + 1)) ∈ β„€ ∧ (πΉβ€˜(π‘˜ + 1)) β‰  0))
17289, 171syl 14 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((πΉβ€˜(π‘˜ + 1)) ∈ β„€ ∧ (πΉβ€˜(π‘˜ + 1)) β‰  0))
173 pcmul 12300 . . . . . . . . . . . 12 ((𝑃 ∈ β„™ ∧ ((seq1( Β· , 𝐹)β€˜π‘˜) ∈ β„€ ∧ (seq1( Β· , 𝐹)β€˜π‘˜) β‰  0) ∧ ((πΉβ€˜(π‘˜ + 1)) ∈ β„€ ∧ (πΉβ€˜(π‘˜ + 1)) β‰  0)) β†’ (𝑃 pCnt ((seq1( Β· , 𝐹)β€˜π‘˜) Β· (πΉβ€˜(π‘˜ + 1)))) = ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))))
174162, 168, 172, 173syl3anc 1238 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (𝑃 pCnt ((seq1( Β· , 𝐹)β€˜π‘˜) Β· (πΉβ€˜(π‘˜ + 1)))) = ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))))
175161, 174eqtrd 2210 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))))
176175adantrr 479 . . . . . . . . 9 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))))
177 prmnn 12109 . . . . . . . . . . . . . . 15 (𝑃 ∈ β„™ β†’ 𝑃 ∈ β„•)
17826, 177syl 14 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑃 ∈ β„•)
179178nnred 8931 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑃 ∈ ℝ)
180179adantr 276 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ 𝑃 ∈ ℝ)
181180leidd 8470 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ 𝑃 ≀ 𝑃)
182181, 121breqtrrd 4031 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ 𝑃 ≀ (π‘˜ + 1))
183182iftrued 3541 . . . . . . . . 9 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0) = 𝐡)
184176, 183eqeq12d 2192 . . . . . . . 8 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0) ↔ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))) = 𝐡))
185142, 154, 1843imtr4d 203 . . . . . . 7 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0)))
186185expr 375 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((π‘˜ + 1) = 𝑃 β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0))))
187175adantrr 479 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))))
188 simplrr 536 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ (π‘˜ + 1) β‰  𝑃)
189188necomd 2433 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ 𝑃 β‰  (π‘˜ + 1))
19026ad2antrr 488 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ 𝑃 ∈ β„™)
191 simpr 110 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ (π‘˜ + 1) ∈ β„™)
19234ad2antrr 488 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ βˆ€π‘› ∈ β„™ 𝐴 ∈ β„•0)
193191, 192, 102sylc 62 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ ⦋(π‘˜ + 1) / π‘›β¦Œπ΄ ∈ β„•0)
194 prmdvdsexpr 12149 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ β„™ ∧ (π‘˜ + 1) ∈ β„™ ∧ ⦋(π‘˜ + 1) / π‘›β¦Œπ΄ ∈ β„•0) β†’ (𝑃 βˆ₯ ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄) β†’ 𝑃 = (π‘˜ + 1)))
195190, 191, 193, 194syl3anc 1238 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ (𝑃 βˆ₯ ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄) β†’ 𝑃 = (π‘˜ + 1)))
196195necon3ad 2389 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ (𝑃 β‰  (π‘˜ + 1) β†’ Β¬ 𝑃 βˆ₯ ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄)))
197189, 196mpd 13 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ Β¬ 𝑃 βˆ₯ ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄))
19887ad2antrl 490 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (π‘˜ + 1) ∈ β„•)
199109adantrr 479 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1) ∈ β„•)
200198, 199, 119syl2anc 411 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (πΉβ€˜(π‘˜ + 1)) = if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1))
201 iftrue 3539 . . . . . . . . . . . . . . . 16 ((π‘˜ + 1) ∈ β„™ β†’ if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1) = ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄))
202200, 201sylan9eq 2230 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ (πΉβ€˜(π‘˜ + 1)) = ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄))
203202breq2d 4015 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ (𝑃 βˆ₯ (πΉβ€˜(π‘˜ + 1)) ↔ 𝑃 βˆ₯ ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄)))
204197, 203mtbird 673 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ Β¬ 𝑃 βˆ₯ (πΉβ€˜(π‘˜ + 1)))
20586, 198, 88syl2an2r 595 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (πΉβ€˜(π‘˜ + 1)) ∈ β„•)
206205adantr 276 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ (πΉβ€˜(π‘˜ + 1)) ∈ β„•)
207 pceq0 12320 . . . . . . . . . . . . . 14 ((𝑃 ∈ β„™ ∧ (πΉβ€˜(π‘˜ + 1)) ∈ β„•) β†’ ((𝑃 pCnt (πΉβ€˜(π‘˜ + 1))) = 0 ↔ Β¬ 𝑃 βˆ₯ (πΉβ€˜(π‘˜ + 1))))
208190, 206, 207syl2anc 411 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ ((𝑃 pCnt (πΉβ€˜(π‘˜ + 1))) = 0 ↔ Β¬ 𝑃 βˆ₯ (πΉβ€˜(π‘˜ + 1))))
209204, 208mpbird 167 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ (𝑃 pCnt (πΉβ€˜(π‘˜ + 1))) = 0)
210 iffalse 3542 . . . . . . . . . . . . . . 15 (Β¬ (π‘˜ + 1) ∈ β„™ β†’ if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1) = 1)
211200, 210sylan9eq 2230 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ Β¬ (π‘˜ + 1) ∈ β„™) β†’ (πΉβ€˜(π‘˜ + 1)) = 1)
212211oveq2d 5890 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ Β¬ (π‘˜ + 1) ∈ β„™) β†’ (𝑃 pCnt (πΉβ€˜(π‘˜ + 1))) = (𝑃 pCnt 1))
21328ad2antrr 488 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ Β¬ (π‘˜ + 1) ∈ β„™) β†’ (𝑃 pCnt 1) = 0)
214212, 213eqtrd 2210 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ Β¬ (π‘˜ + 1) ∈ β„™) β†’ (𝑃 pCnt (πΉβ€˜(π‘˜ + 1))) = 0)
215 exmiddc 836 . . . . . . . . . . . . 13 (DECID (π‘˜ + 1) ∈ β„™ β†’ ((π‘˜ + 1) ∈ β„™ ∨ Β¬ (π‘˜ + 1) ∈ β„™))
216198, 107, 2153syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ ((π‘˜ + 1) ∈ β„™ ∨ Β¬ (π‘˜ + 1) ∈ β„™))
217209, 214, 216mpjaodan 798 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (𝑃 pCnt (πΉβ€˜(π‘˜ + 1))) = 0)
218217oveq2d 5890 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))) = ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + 0))
21926adantr 276 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ 𝑃 ∈ β„™)
220164adantrr 479 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (seq1( Β· , 𝐹)β€˜π‘˜) ∈ β„•)
221219, 220pccld 12299 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) ∈ β„•0)
222221nn0cnd 9230 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) ∈ β„‚)
223222addid1d 8105 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + 0) = (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)))
224187, 218, 2233eqtrd 2214 . . . . . . . . 9 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)))
225219, 77syl 14 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ 𝑃 ∈ β„€)
226146ad2antrl 490 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (π‘˜ + 1) ∈ β„€)
227 zltlen 9330 . . . . . . . . . . . 12 ((𝑃 ∈ β„€ ∧ (π‘˜ + 1) ∈ β„€) β†’ (𝑃 < (π‘˜ + 1) ↔ (𝑃 ≀ (π‘˜ + 1) ∧ (π‘˜ + 1) β‰  𝑃)))
228225, 226, 227syl2anc 411 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (𝑃 < (π‘˜ + 1) ↔ (𝑃 ≀ (π‘˜ + 1) ∧ (π‘˜ + 1) β‰  𝑃)))
229 simprl 529 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ π‘˜ ∈ β„•)
230 nnleltp1 9311 . . . . . . . . . . . 12 ((𝑃 ∈ β„• ∧ π‘˜ ∈ β„•) β†’ (𝑃 ≀ π‘˜ ↔ 𝑃 < (π‘˜ + 1)))
231178, 229, 230syl2an2r 595 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (𝑃 ≀ π‘˜ ↔ 𝑃 < (π‘˜ + 1)))
232 simprr 531 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (π‘˜ + 1) β‰  𝑃)
233232biantrud 304 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (𝑃 ≀ (π‘˜ + 1) ↔ (𝑃 ≀ (π‘˜ + 1) ∧ (π‘˜ + 1) β‰  𝑃)))
234228, 231, 2333bitr4rd 221 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (𝑃 ≀ (π‘˜ + 1) ↔ 𝑃 ≀ π‘˜))
235234ifbid 3555 . . . . . . . . 9 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0) = if(𝑃 ≀ π‘˜, 𝐡, 0))
236224, 235eqeq12d 2192 . . . . . . . 8 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0) ↔ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0)))
237236biimprd 158 . . . . . . 7 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0)))
238237expr 375 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((π‘˜ + 1) β‰  𝑃 β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0))))
239106nnzd 9373 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘˜ + 1) ∈ β„€)
240162, 77syl 14 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 𝑃 ∈ β„€)
241 zdceq 9327 . . . . . . . 8 (((π‘˜ + 1) ∈ β„€ ∧ 𝑃 ∈ β„€) β†’ DECID (π‘˜ + 1) = 𝑃)
242239, 240, 241syl2anc 411 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ DECID (π‘˜ + 1) = 𝑃)
243 dcne 2358 . . . . . . 7 (DECID (π‘˜ + 1) = 𝑃 ↔ ((π‘˜ + 1) = 𝑃 ∨ (π‘˜ + 1) β‰  𝑃))
244242, 243sylib 122 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((π‘˜ + 1) = 𝑃 ∨ (π‘˜ + 1) β‰  𝑃))
245186, 238, 244mpjaod 718 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0)))
246245expcom 116 . . . 4 (π‘˜ ∈ β„• β†’ (πœ‘ β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0))))
247246a2d 26 . . 3 (π‘˜ ∈ β„• β†’ ((πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0)) β†’ (πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0))))
2487, 13, 19, 25, 83, 247nnind 8934 . 2 (𝑁 ∈ β„• β†’ (πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑁, 𝐡, 0)))
2491, 248mpcom 36 1 (πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑁, 𝐡, 0))
Colors of variables: wff set class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 708  DECID wdc 834   = wceq 1353   ∈ wcel 2148   β‰  wne 2347  βˆ€wral 2455  β¦‹csb 3057  ifcif 3534   class class class wbr 4003   ↦ cmpt 4064  βŸΆwf 5212  β€˜cfv 5216  (class class class)co 5874  β„cr 7809  0cc0 7810  1c1 7811   + caddc 7813   Β· cmul 7815   < clt 7991   ≀ cle 7992  β„•cn 8918  β„•0cn0 9175  β„€cz 9252  β„€β‰₯cuz 9527  seqcseq 10444  β†‘cexp 10518   βˆ₯ cdvds 11793  β„™cprime 12106   pCnt cpc 12283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4118  ax-sep 4121  ax-nul 4129  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536  ax-iinf 4587  ax-cnex 7901  ax-resscn 7902  ax-1cn 7903  ax-1re 7904  ax-icn 7905  ax-addcl 7906  ax-addrcl 7907  ax-mulcl 7908  ax-mulrcl 7909  ax-addcom 7910  ax-mulcom 7911  ax-addass 7912  ax-mulass 7913  ax-distr 7914  ax-i2m1 7915  ax-0lt1 7916  ax-1rid 7917  ax-0id 7918  ax-rnegex 7919  ax-precex 7920  ax-cnre 7921  ax-pre-ltirr 7922  ax-pre-ltwlin 7923  ax-pre-lttrn 7924  ax-pre-apti 7925  ax-pre-ltadd 7926  ax-pre-mulgt0 7927  ax-pre-mulext 7928  ax-arch 7929  ax-caucvg 7930
This theorem depends on definitions:  df-bi 117  df-stab 831  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-iun 3888  df-br 4004  df-opab 4065  df-mpt 4066  df-tr 4102  df-id 4293  df-po 4296  df-iso 4297  df-iord 4366  df-on 4368  df-ilim 4369  df-suc 4371  df-iom 4590  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-res 4638  df-ima 4639  df-iota 5178  df-fun 5218  df-fn 5219  df-f 5220  df-f1 5221  df-fo 5222  df-f1o 5223  df-fv 5224  df-isom 5225  df-riota 5830  df-ov 5877  df-oprab 5878  df-mpo 5879  df-1st 6140  df-2nd 6141  df-recs 6305  df-frec 6391  df-1o 6416  df-2o 6417  df-er 6534  df-en 6740  df-fin 6742  df-sup 6982  df-inf 6983  df-pnf 7993  df-mnf 7994  df-xr 7995  df-ltxr 7996  df-le 7997  df-sub 8129  df-neg 8130  df-reap 8531  df-ap 8538  df-div 8629  df-inn 8919  df-2 8977  df-3 8978  df-4 8979  df-n0 9176  df-z 9253  df-uz 9528  df-q 9619  df-rp 9653  df-fz 10008  df-fzo 10142  df-fl 10269  df-mod 10322  df-seqfrec 10445  df-exp 10519  df-cj 10850  df-re 10851  df-im 10852  df-rsqrt 11006  df-abs 11007  df-dvds 11794  df-gcd 11943  df-prm 12107  df-pc 12284
This theorem is referenced by:  pcmpt2  12341  pcprod  12343  1arithlem4  12363
  Copyright terms: Public domain W3C validator