MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pcmpt Structured version   Visualization version   GIF version

Theorem pcmpt 16825
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 6892 . . . . . 6 (𝑝 = 1 β†’ (seq1( Β· , 𝐹)β€˜π‘) = (seq1( Β· , 𝐹)β€˜1))
32oveq2d 7425 . . . . 5 (𝑝 = 1 β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = (𝑃 pCnt (seq1( Β· , 𝐹)β€˜1)))
4 breq2 5153 . . . . . 6 (𝑝 = 1 β†’ (𝑃 ≀ 𝑝 ↔ 𝑃 ≀ 1))
54ifbid 4552 . . . . 5 (𝑝 = 1 β†’ if(𝑃 ≀ 𝑝, 𝐡, 0) = if(𝑃 ≀ 1, 𝐡, 0))
63, 5eqeq12d 2749 . . . 4 (𝑝 = 1 β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑝, 𝐡, 0) ↔ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜1)) = if(𝑃 ≀ 1, 𝐡, 0)))
76imbi2d 341 . . 3 (𝑝 = 1 β†’ ((πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑝, 𝐡, 0)) ↔ (πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜1)) = if(𝑃 ≀ 1, 𝐡, 0))))
8 fveq2 6892 . . . . . 6 (𝑝 = π‘˜ β†’ (seq1( Β· , 𝐹)β€˜π‘) = (seq1( Β· , 𝐹)β€˜π‘˜))
98oveq2d 7425 . . . . 5 (𝑝 = π‘˜ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)))
10 breq2 5153 . . . . . 6 (𝑝 = π‘˜ β†’ (𝑃 ≀ 𝑝 ↔ 𝑃 ≀ π‘˜))
1110ifbid 4552 . . . . 5 (𝑝 = π‘˜ β†’ if(𝑃 ≀ 𝑝, 𝐡, 0) = if(𝑃 ≀ π‘˜, 𝐡, 0))
129, 11eqeq12d 2749 . . . 4 (𝑝 = π‘˜ β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑝, 𝐡, 0) ↔ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0)))
1312imbi2d 341 . . 3 (𝑝 = π‘˜ β†’ ((πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑝, 𝐡, 0)) ↔ (πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0))))
14 fveq2 6892 . . . . . 6 (𝑝 = (π‘˜ + 1) β†’ (seq1( Β· , 𝐹)β€˜π‘) = (seq1( Β· , 𝐹)β€˜(π‘˜ + 1)))
1514oveq2d 7425 . . . . 5 (𝑝 = (π‘˜ + 1) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))))
16 breq2 5153 . . . . . 6 (𝑝 = (π‘˜ + 1) β†’ (𝑃 ≀ 𝑝 ↔ 𝑃 ≀ (π‘˜ + 1)))
1716ifbid 4552 . . . . 5 (𝑝 = (π‘˜ + 1) β†’ if(𝑃 ≀ 𝑝, 𝐡, 0) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0))
1815, 17eqeq12d 2749 . . . 4 (𝑝 = (π‘˜ + 1) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑝, 𝐡, 0) ↔ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0)))
1918imbi2d 341 . . 3 (𝑝 = (π‘˜ + 1) β†’ ((πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑝, 𝐡, 0)) ↔ (πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0))))
20 fveq2 6892 . . . . . 6 (𝑝 = 𝑁 β†’ (seq1( Β· , 𝐹)β€˜π‘) = (seq1( Β· , 𝐹)β€˜π‘))
2120oveq2d 7425 . . . . 5 (𝑝 = 𝑁 β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)))
22 breq2 5153 . . . . . 6 (𝑝 = 𝑁 β†’ (𝑃 ≀ 𝑝 ↔ 𝑃 ≀ 𝑁))
2322ifbid 4552 . . . . 5 (𝑝 = 𝑁 β†’ if(𝑃 ≀ 𝑝, 𝐡, 0) = if(𝑃 ≀ 𝑁, 𝐡, 0))
2421, 23eqeq12d 2749 . . . 4 (𝑝 = 𝑁 β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑝, 𝐡, 0) ↔ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑁, 𝐡, 0)))
2524imbi2d 341 . . 3 (𝑝 = 𝑁 β†’ ((πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑝, 𝐡, 0)) ↔ (πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑁, 𝐡, 0))))
26 pcmpt.4 . . . 4 (πœ‘ β†’ 𝑃 ∈ β„™)
27 1z 12592 . . . . . . . . 9 1 ∈ β„€
28 seq1 13979 . . . . . . . . 9 (1 ∈ β„€ β†’ (seq1( Β· , 𝐹)β€˜1) = (πΉβ€˜1))
2927, 28ax-mp 5 . . . . . . . 8 (seq1( Β· , 𝐹)β€˜1) = (πΉβ€˜1)
30 1nn 12223 . . . . . . . . 9 1 ∈ β„•
31 1nprm 16616 . . . . . . . . . . . 12 Β¬ 1 ∈ β„™
32 eleq1 2822 . . . . . . . . . . . 12 (𝑛 = 1 β†’ (𝑛 ∈ β„™ ↔ 1 ∈ β„™))
3331, 32mtbiri 327 . . . . . . . . . . 11 (𝑛 = 1 β†’ Β¬ 𝑛 ∈ β„™)
3433iffalsed 4540 . . . . . . . . . 10 (𝑛 = 1 β†’ if(𝑛 ∈ β„™, (𝑛↑𝐴), 1) = 1)
35 pcmpt.1 . . . . . . . . . 10 𝐹 = (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, (𝑛↑𝐴), 1))
36 1ex 11210 . . . . . . . . . 10 1 ∈ V
3734, 35, 36fvmpt 6999 . . . . . . . . 9 (1 ∈ β„• β†’ (πΉβ€˜1) = 1)
3830, 37ax-mp 5 . . . . . . . 8 (πΉβ€˜1) = 1
3929, 38eqtri 2761 . . . . . . 7 (seq1( Β· , 𝐹)β€˜1) = 1
4039oveq2i 7420 . . . . . 6 (𝑃 pCnt (seq1( Β· , 𝐹)β€˜1)) = (𝑃 pCnt 1)
41 pc1 16788 . . . . . 6 (𝑃 ∈ β„™ β†’ (𝑃 pCnt 1) = 0)
4240, 41eqtrid 2785 . . . . 5 (𝑃 ∈ β„™ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜1)) = 0)
43 prmgt1 16634 . . . . . . 7 (𝑃 ∈ β„™ β†’ 1 < 𝑃)
44 1re 11214 . . . . . . . 8 1 ∈ ℝ
45 prmuz2 16633 . . . . . . . . 9 (𝑃 ∈ β„™ β†’ 𝑃 ∈ (β„€β‰₯β€˜2))
46 eluzelre 12833 . . . . . . . . 9 (𝑃 ∈ (β„€β‰₯β€˜2) β†’ 𝑃 ∈ ℝ)
4745, 46syl 17 . . . . . . . 8 (𝑃 ∈ β„™ β†’ 𝑃 ∈ ℝ)
48 ltnle 11293 . . . . . . . 8 ((1 ∈ ℝ ∧ 𝑃 ∈ ℝ) β†’ (1 < 𝑃 ↔ Β¬ 𝑃 ≀ 1))
4944, 47, 48sylancr 588 . . . . . . 7 (𝑃 ∈ β„™ β†’ (1 < 𝑃 ↔ Β¬ 𝑃 ≀ 1))
5043, 49mpbid 231 . . . . . 6 (𝑃 ∈ β„™ β†’ Β¬ 𝑃 ≀ 1)
5150iffalsed 4540 . . . . 5 (𝑃 ∈ β„™ β†’ if(𝑃 ≀ 1, 𝐡, 0) = 0)
5242, 51eqtr4d 2776 . . . 4 (𝑃 ∈ β„™ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜1)) = if(𝑃 ≀ 1, 𝐡, 0))
5326, 52syl 17 . . 3 (πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜1)) = if(𝑃 ≀ 1, 𝐡, 0))
5426adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ 𝑃 ∈ β„™)
55 pcmpt.2 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ βˆ€π‘› ∈ β„™ 𝐴 ∈ β„•0)
5635, 55pcmptcl 16824 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝐹:β„•βŸΆβ„• ∧ seq1( Β· , 𝐹):β„•βŸΆβ„•))
5756simpld 496 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐹:β„•βŸΆβ„•)
58 peano2nn 12224 . . . . . . . . . . . . . . 15 (π‘˜ ∈ β„• β†’ (π‘˜ + 1) ∈ β„•)
59 ffvelcdm 7084 . . . . . . . . . . . . . . 15 ((𝐹:β„•βŸΆβ„• ∧ (π‘˜ + 1) ∈ β„•) β†’ (πΉβ€˜(π‘˜ + 1)) ∈ β„•)
6057, 58, 59syl2an 597 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜(π‘˜ + 1)) ∈ β„•)
6160adantrr 716 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (πΉβ€˜(π‘˜ + 1)) ∈ β„•)
6254, 61pccld 16783 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (𝑃 pCnt (πΉβ€˜(π‘˜ + 1))) ∈ β„•0)
6362nn0cnd 12534 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (𝑃 pCnt (πΉβ€˜(π‘˜ + 1))) ∈ β„‚)
6463addlidd 11415 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (0 + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))) = (𝑃 pCnt (πΉβ€˜(π‘˜ + 1))))
6558ad2antrl 727 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (π‘˜ + 1) ∈ β„•)
66 ovex 7442 . . . . . . . . . . . . . . 15 (𝑛↑𝐴) ∈ V
6766, 36ifex 4579 . . . . . . . . . . . . . 14 if(𝑛 ∈ β„™, (𝑛↑𝐴), 1) ∈ V
6867csbex 5312 . . . . . . . . . . . . 13 ⦋(π‘˜ + 1) / π‘›β¦Œif(𝑛 ∈ β„™, (𝑛↑𝐴), 1) ∈ V
6935fvmpts 7002 . . . . . . . . . . . . . 14 (((π‘˜ + 1) ∈ β„• ∧ ⦋(π‘˜ + 1) / π‘›β¦Œif(𝑛 ∈ β„™, (𝑛↑𝐴), 1) ∈ V) β†’ (πΉβ€˜(π‘˜ + 1)) = ⦋(π‘˜ + 1) / π‘›β¦Œif(𝑛 ∈ β„™, (𝑛↑𝐴), 1))
70 ovex 7442 . . . . . . . . . . . . . . 15 (π‘˜ + 1) ∈ V
71 nfv 1918 . . . . . . . . . . . . . . . 16 Ⅎ𝑛(π‘˜ + 1) ∈ β„™
72 nfcv 2904 . . . . . . . . . . . . . . . . 17 Ⅎ𝑛(π‘˜ + 1)
73 nfcv 2904 . . . . . . . . . . . . . . . . 17 Ⅎ𝑛↑
74 nfcsb1v 3919 . . . . . . . . . . . . . . . . 17 Ⅎ𝑛⦋(π‘˜ + 1) / π‘›β¦Œπ΄
7572, 73, 74nfov 7439 . . . . . . . . . . . . . . . 16 Ⅎ𝑛((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄)
76 nfcv 2904 . . . . . . . . . . . . . . . 16 Ⅎ𝑛1
7771, 75, 76nfif 4559 . . . . . . . . . . . . . . 15 Ⅎ𝑛if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1)
78 eleq1 2822 . . . . . . . . . . . . . . . 16 (𝑛 = (π‘˜ + 1) β†’ (𝑛 ∈ β„™ ↔ (π‘˜ + 1) ∈ β„™))
79 id 22 . . . . . . . . . . . . . . . . 17 (𝑛 = (π‘˜ + 1) β†’ 𝑛 = (π‘˜ + 1))
80 csbeq1a 3908 . . . . . . . . . . . . . . . . 17 (𝑛 = (π‘˜ + 1) β†’ 𝐴 = ⦋(π‘˜ + 1) / π‘›β¦Œπ΄)
8179, 80oveq12d 7427 . . . . . . . . . . . . . . . 16 (𝑛 = (π‘˜ + 1) β†’ (𝑛↑𝐴) = ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄))
8278, 81ifbieq1d 4553 . . . . . . . . . . . . . . 15 (𝑛 = (π‘˜ + 1) β†’ if(𝑛 ∈ β„™, (𝑛↑𝐴), 1) = if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1))
8370, 77, 82csbief 3929 . . . . . . . . . . . . . 14 ⦋(π‘˜ + 1) / π‘›β¦Œif(𝑛 ∈ β„™, (𝑛↑𝐴), 1) = if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1)
8469, 83eqtrdi 2789 . . . . . . . . . . . . 13 (((π‘˜ + 1) ∈ β„• ∧ ⦋(π‘˜ + 1) / π‘›β¦Œif(𝑛 ∈ β„™, (𝑛↑𝐴), 1) ∈ V) β†’ (πΉβ€˜(π‘˜ + 1)) = if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1))
8565, 68, 84sylancl 587 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (πΉβ€˜(π‘˜ + 1)) = if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1))
86 simprr 772 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (π‘˜ + 1) = 𝑃)
8786, 54eqeltrd 2834 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (π‘˜ + 1) ∈ β„™)
8887iftrued 4537 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1) = ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄))
8986csbeq1d 3898 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ ⦋(π‘˜ + 1) / π‘›β¦Œπ΄ = ⦋𝑃 / π‘›β¦Œπ΄)
90 nfcvd 2905 . . . . . . . . . . . . . . . 16 (𝑃 ∈ β„™ β†’ Ⅎ𝑛𝐡)
91 pcmpt.5 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑃 β†’ 𝐴 = 𝐡)
9290, 91csbiegf 3928 . . . . . . . . . . . . . . 15 (𝑃 ∈ β„™ β†’ ⦋𝑃 / π‘›β¦Œπ΄ = 𝐡)
9354, 92syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ ⦋𝑃 / π‘›β¦Œπ΄ = 𝐡)
9489, 93eqtrd 2773 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ ⦋(π‘˜ + 1) / π‘›β¦Œπ΄ = 𝐡)
9586, 94oveq12d 7427 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄) = (𝑃↑𝐡))
9685, 88, 953eqtrd 2777 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (πΉβ€˜(π‘˜ + 1)) = (𝑃↑𝐡))
9796oveq2d 7425 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (𝑃 pCnt (πΉβ€˜(π‘˜ + 1))) = (𝑃 pCnt (𝑃↑𝐡)))
9891eleq1d 2819 . . . . . . . . . . . . . 14 (𝑛 = 𝑃 β†’ (𝐴 ∈ β„•0 ↔ 𝐡 ∈ β„•0))
9998rspcv 3609 . . . . . . . . . . . . 13 (𝑃 ∈ β„™ β†’ (βˆ€π‘› ∈ β„™ 𝐴 ∈ β„•0 β†’ 𝐡 ∈ β„•0))
10026, 55, 99sylc 65 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐡 ∈ β„•0)
101100adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ 𝐡 ∈ β„•0)
102 pcidlem 16805 . . . . . . . . . . 11 ((𝑃 ∈ β„™ ∧ 𝐡 ∈ β„•0) β†’ (𝑃 pCnt (𝑃↑𝐡)) = 𝐡)
10354, 101, 102syl2anc 585 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (𝑃 pCnt (𝑃↑𝐡)) = 𝐡)
10464, 97, 1033eqtrd 2777 . . . . . . . . 9 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (0 + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))) = 𝐡)
105 oveq1 7416 . . . . . . . . . 10 ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = 0 β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))) = (0 + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))))
106105eqeq1d 2735 . . . . . . . . 9 ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = 0 β†’ (((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))) = 𝐡 ↔ (0 + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))) = 𝐡))
107104, 106syl5ibrcom 246 . . . . . . . 8 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = 0 β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))) = 𝐡))
108 nnre 12219 . . . . . . . . . . . . 13 (π‘˜ ∈ β„• β†’ π‘˜ ∈ ℝ)
109108ad2antrl 727 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ π‘˜ ∈ ℝ)
110 ltp1 12054 . . . . . . . . . . . . 13 (π‘˜ ∈ ℝ β†’ π‘˜ < (π‘˜ + 1))
111 peano2re 11387 . . . . . . . . . . . . . 14 (π‘˜ ∈ ℝ β†’ (π‘˜ + 1) ∈ ℝ)
112 ltnle 11293 . . . . . . . . . . . . . 14 ((π‘˜ ∈ ℝ ∧ (π‘˜ + 1) ∈ ℝ) β†’ (π‘˜ < (π‘˜ + 1) ↔ Β¬ (π‘˜ + 1) ≀ π‘˜))
113111, 112mpdan 686 . . . . . . . . . . . . 13 (π‘˜ ∈ ℝ β†’ (π‘˜ < (π‘˜ + 1) ↔ Β¬ (π‘˜ + 1) ≀ π‘˜))
114110, 113mpbid 231 . . . . . . . . . . . 12 (π‘˜ ∈ ℝ β†’ Β¬ (π‘˜ + 1) ≀ π‘˜)
115109, 114syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ Β¬ (π‘˜ + 1) ≀ π‘˜)
11686breq1d 5159 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ ((π‘˜ + 1) ≀ π‘˜ ↔ 𝑃 ≀ π‘˜))
117115, 116mtbid 324 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ Β¬ 𝑃 ≀ π‘˜)
118117iffalsed 4540 . . . . . . . . 9 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ if(𝑃 ≀ π‘˜, 𝐡, 0) = 0)
119118eqeq2d 2744 . . . . . . . 8 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0) ↔ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = 0))
120 simpr 486 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ β„•)
121 nnuz 12865 . . . . . . . . . . . . . 14 β„• = (β„€β‰₯β€˜1)
122120, 121eleqtrdi 2844 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ (β„€β‰₯β€˜1))
123 seqp1 13981 . . . . . . . . . . . . 13 (π‘˜ ∈ (β„€β‰₯β€˜1) β†’ (seq1( Β· , 𝐹)β€˜(π‘˜ + 1)) = ((seq1( Β· , 𝐹)β€˜π‘˜) Β· (πΉβ€˜(π‘˜ + 1))))
124122, 123syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (seq1( Β· , 𝐹)β€˜(π‘˜ + 1)) = ((seq1( Β· , 𝐹)β€˜π‘˜) Β· (πΉβ€˜(π‘˜ + 1))))
125124oveq2d 7425 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = (𝑃 pCnt ((seq1( Β· , 𝐹)β€˜π‘˜) Β· (πΉβ€˜(π‘˜ + 1)))))
12626adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 𝑃 ∈ β„™)
12756simprd 497 . . . . . . . . . . . . . 14 (πœ‘ β†’ seq1( Β· , 𝐹):β„•βŸΆβ„•)
128127ffvelcdmda 7087 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (seq1( Β· , 𝐹)β€˜π‘˜) ∈ β„•)
129 nnz 12579 . . . . . . . . . . . . . 14 ((seq1( Β· , 𝐹)β€˜π‘˜) ∈ β„• β†’ (seq1( Β· , 𝐹)β€˜π‘˜) ∈ β„€)
130 nnne0 12246 . . . . . . . . . . . . . 14 ((seq1( Β· , 𝐹)β€˜π‘˜) ∈ β„• β†’ (seq1( Β· , 𝐹)β€˜π‘˜) β‰  0)
131129, 130jca 513 . . . . . . . . . . . . 13 ((seq1( Β· , 𝐹)β€˜π‘˜) ∈ β„• β†’ ((seq1( Β· , 𝐹)β€˜π‘˜) ∈ β„€ ∧ (seq1( Β· , 𝐹)β€˜π‘˜) β‰  0))
132128, 131syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((seq1( Β· , 𝐹)β€˜π‘˜) ∈ β„€ ∧ (seq1( Β· , 𝐹)β€˜π‘˜) β‰  0))
133 nnz 12579 . . . . . . . . . . . . . 14 ((πΉβ€˜(π‘˜ + 1)) ∈ β„• β†’ (πΉβ€˜(π‘˜ + 1)) ∈ β„€)
134 nnne0 12246 . . . . . . . . . . . . . 14 ((πΉβ€˜(π‘˜ + 1)) ∈ β„• β†’ (πΉβ€˜(π‘˜ + 1)) β‰  0)
135133, 134jca 513 . . . . . . . . . . . . 13 ((πΉβ€˜(π‘˜ + 1)) ∈ β„• β†’ ((πΉβ€˜(π‘˜ + 1)) ∈ β„€ ∧ (πΉβ€˜(π‘˜ + 1)) β‰  0))
13660, 135syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((πΉβ€˜(π‘˜ + 1)) ∈ β„€ ∧ (πΉβ€˜(π‘˜ + 1)) β‰  0))
137 pcmul 16784 . . . . . . . . . . . 12 ((𝑃 ∈ β„™ ∧ ((seq1( Β· , 𝐹)β€˜π‘˜) ∈ β„€ ∧ (seq1( Β· , 𝐹)β€˜π‘˜) β‰  0) ∧ ((πΉβ€˜(π‘˜ + 1)) ∈ β„€ ∧ (πΉβ€˜(π‘˜ + 1)) β‰  0)) β†’ (𝑃 pCnt ((seq1( Β· , 𝐹)β€˜π‘˜) Β· (πΉβ€˜(π‘˜ + 1)))) = ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))))
138126, 132, 136, 137syl3anc 1372 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (𝑃 pCnt ((seq1( Β· , 𝐹)β€˜π‘˜) Β· (πΉβ€˜(π‘˜ + 1)))) = ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))))
139125, 138eqtrd 2773 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))))
140139adantrr 716 . . . . . . . . 9 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))))
141 prmnn 16611 . . . . . . . . . . . . . . 15 (𝑃 ∈ β„™ β†’ 𝑃 ∈ β„•)
14226, 141syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑃 ∈ β„•)
143142nnred 12227 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑃 ∈ ℝ)
144143adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ 𝑃 ∈ ℝ)
145144leidd 11780 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ 𝑃 ≀ 𝑃)
146145, 86breqtrrd 5177 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ 𝑃 ≀ (π‘˜ + 1))
147146iftrued 4537 . . . . . . . . 9 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0) = 𝐡)
148140, 147eqeq12d 2749 . . . . . . . 8 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0) ↔ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))) = 𝐡))
149107, 119, 1483imtr4d 294 . . . . . . 7 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) = 𝑃)) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0)))
150149expr 458 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((π‘˜ + 1) = 𝑃 β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0))))
151139adantrr 716 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))))
152 simplrr 777 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ (π‘˜ + 1) β‰  𝑃)
153152necomd 2997 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ 𝑃 β‰  (π‘˜ + 1))
15426ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ 𝑃 ∈ β„™)
155 simpr 486 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ (π‘˜ + 1) ∈ β„™)
15655ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ βˆ€π‘› ∈ β„™ 𝐴 ∈ β„•0)
15774nfel1 2920 . . . . . . . . . . . . . . . . . . 19 Ⅎ𝑛⦋(π‘˜ + 1) / π‘›β¦Œπ΄ ∈ β„•0
15880eleq1d 2819 . . . . . . . . . . . . . . . . . . 19 (𝑛 = (π‘˜ + 1) β†’ (𝐴 ∈ β„•0 ↔ ⦋(π‘˜ + 1) / π‘›β¦Œπ΄ ∈ β„•0))
159157, 158rspc 3601 . . . . . . . . . . . . . . . . . 18 ((π‘˜ + 1) ∈ β„™ β†’ (βˆ€π‘› ∈ β„™ 𝐴 ∈ β„•0 β†’ ⦋(π‘˜ + 1) / π‘›β¦Œπ΄ ∈ β„•0))
160155, 156, 159sylc 65 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ ⦋(π‘˜ + 1) / π‘›β¦Œπ΄ ∈ β„•0)
161 prmdvdsexpr 16654 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ β„™ ∧ (π‘˜ + 1) ∈ β„™ ∧ ⦋(π‘˜ + 1) / π‘›β¦Œπ΄ ∈ β„•0) β†’ (𝑃 βˆ₯ ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄) β†’ 𝑃 = (π‘˜ + 1)))
162154, 155, 160, 161syl3anc 1372 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ (𝑃 βˆ₯ ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄) β†’ 𝑃 = (π‘˜ + 1)))
163162necon3ad 2954 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ (𝑃 β‰  (π‘˜ + 1) β†’ Β¬ 𝑃 βˆ₯ ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄)))
164153, 163mpd 15 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ Β¬ 𝑃 βˆ₯ ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄))
16558ad2antrl 727 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (π‘˜ + 1) ∈ β„•)
166165, 68, 84sylancl 587 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (πΉβ€˜(π‘˜ + 1)) = if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1))
167 iftrue 4535 . . . . . . . . . . . . . . . 16 ((π‘˜ + 1) ∈ β„™ β†’ if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1) = ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄))
168166, 167sylan9eq 2793 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ (πΉβ€˜(π‘˜ + 1)) = ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄))
169168breq2d 5161 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ (𝑃 βˆ₯ (πΉβ€˜(π‘˜ + 1)) ↔ 𝑃 βˆ₯ ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄)))
170164, 169mtbird 325 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ Β¬ 𝑃 βˆ₯ (πΉβ€˜(π‘˜ + 1)))
17157adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ 𝐹:β„•βŸΆβ„•)
172171, 165, 59syl2anc 585 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (πΉβ€˜(π‘˜ + 1)) ∈ β„•)
173172adantr 482 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ (πΉβ€˜(π‘˜ + 1)) ∈ β„•)
174 pceq0 16804 . . . . . . . . . . . . . 14 ((𝑃 ∈ β„™ ∧ (πΉβ€˜(π‘˜ + 1)) ∈ β„•) β†’ ((𝑃 pCnt (πΉβ€˜(π‘˜ + 1))) = 0 ↔ Β¬ 𝑃 βˆ₯ (πΉβ€˜(π‘˜ + 1))))
175154, 173, 174syl2anc 585 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ ((𝑃 pCnt (πΉβ€˜(π‘˜ + 1))) = 0 ↔ Β¬ 𝑃 βˆ₯ (πΉβ€˜(π‘˜ + 1))))
176170, 175mpbird 257 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ (π‘˜ + 1) ∈ β„™) β†’ (𝑃 pCnt (πΉβ€˜(π‘˜ + 1))) = 0)
177 iffalse 4538 . . . . . . . . . . . . . . 15 (Β¬ (π‘˜ + 1) ∈ β„™ β†’ if((π‘˜ + 1) ∈ β„™, ((π‘˜ + 1)↑⦋(π‘˜ + 1) / π‘›β¦Œπ΄), 1) = 1)
178166, 177sylan9eq 2793 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ Β¬ (π‘˜ + 1) ∈ β„™) β†’ (πΉβ€˜(π‘˜ + 1)) = 1)
179178oveq2d 7425 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ Β¬ (π‘˜ + 1) ∈ β„™) β†’ (𝑃 pCnt (πΉβ€˜(π‘˜ + 1))) = (𝑃 pCnt 1))
18026, 41syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑃 pCnt 1) = 0)
181180ad2antrr 725 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ Β¬ (π‘˜ + 1) ∈ β„™) β†’ (𝑃 pCnt 1) = 0)
182179, 181eqtrd 2773 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) ∧ Β¬ (π‘˜ + 1) ∈ β„™) β†’ (𝑃 pCnt (πΉβ€˜(π‘˜ + 1))) = 0)
183176, 182pm2.61dan 812 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (𝑃 pCnt (πΉβ€˜(π‘˜ + 1))) = 0)
184183oveq2d 7425 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + (𝑃 pCnt (πΉβ€˜(π‘˜ + 1)))) = ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + 0))
18526adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ 𝑃 ∈ β„™)
186128adantrr 716 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (seq1( Β· , 𝐹)β€˜π‘˜) ∈ β„•)
187185, 186pccld 16783 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) ∈ β„•0)
188187nn0cnd 12534 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) ∈ β„‚)
189188addridd 11414 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) + 0) = (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)))
190151, 184, 1893eqtrd 2777 . . . . . . . . 9 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)))
191142adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ 𝑃 ∈ β„•)
192191nnred 12227 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ 𝑃 ∈ ℝ)
193165nnred 12227 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (π‘˜ + 1) ∈ ℝ)
194192, 193ltlend 11359 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (𝑃 < (π‘˜ + 1) ↔ (𝑃 ≀ (π‘˜ + 1) ∧ (π‘˜ + 1) β‰  𝑃)))
195 simprl 770 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ π‘˜ ∈ β„•)
196 nnleltp1 12617 . . . . . . . . . . . 12 ((𝑃 ∈ β„• ∧ π‘˜ ∈ β„•) β†’ (𝑃 ≀ π‘˜ ↔ 𝑃 < (π‘˜ + 1)))
197191, 195, 196syl2anc 585 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (𝑃 ≀ π‘˜ ↔ 𝑃 < (π‘˜ + 1)))
198 simprr 772 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (π‘˜ + 1) β‰  𝑃)
199198biantrud 533 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (𝑃 ≀ (π‘˜ + 1) ↔ (𝑃 ≀ (π‘˜ + 1) ∧ (π‘˜ + 1) β‰  𝑃)))
200194, 197, 1993bitr4rd 312 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ (𝑃 ≀ (π‘˜ + 1) ↔ 𝑃 ≀ π‘˜))
201200ifbid 4552 . . . . . . . . 9 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0) = if(𝑃 ≀ π‘˜, 𝐡, 0))
202190, 201eqeq12d 2749 . . . . . . . 8 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0) ↔ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0)))
203202biimprd 247 . . . . . . 7 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ (π‘˜ + 1) β‰  𝑃)) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0)))
204203expr 458 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((π‘˜ + 1) β‰  𝑃 β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0))))
205150, 204pm2.61dne 3029 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0)))
206205expcom 415 . . . 4 (π‘˜ ∈ β„• β†’ (πœ‘ β†’ ((𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0) β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0))))
207206a2d 29 . . 3 (π‘˜ ∈ β„• β†’ ((πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘˜)) = if(𝑃 ≀ π‘˜, 𝐡, 0)) β†’ (πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜(π‘˜ + 1))) = if(𝑃 ≀ (π‘˜ + 1), 𝐡, 0))))
2087, 13, 19, 25, 53, 207nnind 12230 . 2 (𝑁 ∈ β„• β†’ (πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑁, 𝐡, 0)))
2091, 208mpcom 38 1 (πœ‘ β†’ (𝑃 pCnt (seq1( Β· , 𝐹)β€˜π‘)) = if(𝑃 ≀ 𝑁, 𝐡, 0))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  Vcvv 3475  β¦‹csb 3894  ifcif 4529   class class class wbr 5149   ↦ cmpt 5232  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7409  β„cr 11109  0cc0 11110  1c1 11111   + caddc 11113   Β· cmul 11115   < clt 11248   ≀ cle 11249  β„•cn 12212  2c2 12267  β„•0cn0 12472  β„€cz 12558  β„€β‰₯cuz 12822  seqcseq 13966  β†‘cexp 14027   βˆ₯ cdvds 16197  β„™cprime 16608   pCnt cpc 16769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-2o 8467  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-sup 9437  df-inf 9438  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-n0 12473  df-z 12559  df-uz 12823  df-q 12933  df-rp 12975  df-fz 13485  df-fl 13757  df-mod 13835  df-seq 13967  df-exp 14028  df-cj 15046  df-re 15047  df-im 15048  df-sqrt 15182  df-abs 15183  df-dvds 16198  df-gcd 16436  df-prm 16609  df-pc 16770
This theorem is referenced by:  pcmpt2  16826  pcprod  16828  1arithlem4  16859  chtublem  26714  bposlem3  26789
  Copyright terms: Public domain W3C validator