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

Theorem mertenslem2 15778
Description: Lemma for mertens 15779. (Contributed by Mario Carneiro, 28-Apr-2014.)
Hypotheses
Ref Expression
mertens.1 ((πœ‘ ∧ 𝑗 ∈ β„•0) β†’ (πΉβ€˜π‘—) = 𝐴)
mertens.2 ((πœ‘ ∧ 𝑗 ∈ β„•0) β†’ (πΎβ€˜π‘—) = (absβ€˜π΄))
mertens.3 ((πœ‘ ∧ 𝑗 ∈ β„•0) β†’ 𝐴 ∈ β„‚)
mertens.4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (πΊβ€˜π‘˜) = 𝐡)
mertens.5 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 𝐡 ∈ β„‚)
mertens.6 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π»β€˜π‘˜) = Σ𝑗 ∈ (0...π‘˜)(𝐴 Β· (πΊβ€˜(π‘˜ βˆ’ 𝑗))))
mertens.7 (πœ‘ β†’ seq0( + , 𝐾) ∈ dom ⇝ )
mertens.8 (πœ‘ β†’ seq0( + , 𝐺) ∈ dom ⇝ )
mertens.9 (πœ‘ β†’ 𝐸 ∈ ℝ+)
mertens.10 𝑇 = {𝑧 ∣ βˆƒπ‘› ∈ (0...(𝑠 βˆ’ 1))𝑧 = (absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜))}
mertens.11 (πœ“ ↔ (𝑠 ∈ β„• ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘ )(absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜)) < ((𝐸 / 2) / (Σ𝑗 ∈ β„•0 (πΎβ€˜π‘—) + 1))))
Assertion
Ref Expression
mertenslem2 (πœ‘ β†’ βˆƒπ‘¦ ∈ β„•0 βˆ€π‘š ∈ (β„€β‰₯β€˜π‘¦)(absβ€˜Ξ£π‘— ∈ (0...π‘š)(𝐴 Β· Ξ£π‘˜ ∈ (β„€β‰₯β€˜((π‘š βˆ’ 𝑗) + 1))𝐡)) < 𝐸)
Distinct variable groups:   𝑗,π‘š,𝑛,𝑠,𝑦,𝑧,𝐡   𝑗,π‘˜,𝐺,π‘š,𝑛,𝑠,𝑦,𝑧   πœ‘,𝑗,π‘˜,π‘š,𝑦,𝑧   𝐴,π‘˜,π‘š,𝑛,𝑠,𝑦   𝑗,𝐸,π‘˜,π‘š,𝑛,𝑠,𝑦,𝑧   𝑗,𝐾,π‘˜,π‘š,𝑛,𝑠,𝑦,𝑧   𝑗,𝐹,π‘š,𝑛,𝑦   πœ“,𝑗,π‘˜,π‘š,𝑛,𝑦,𝑧   𝑇,𝑗,π‘˜,π‘š,𝑛,𝑦,𝑧   π‘˜,𝐻,π‘š,𝑦   πœ‘,𝑛,𝑠
Allowed substitution hints:   πœ“(𝑠)   𝐴(𝑧,𝑗)   𝐡(π‘˜)   𝑇(𝑠)   𝐹(𝑧,π‘˜,𝑠)   𝐻(𝑧,𝑗,𝑛,𝑠)

Proof of Theorem mertenslem2
Dummy variables 𝑑 𝑀 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 12814 . . 3 β„• = (β„€β‰₯β€˜1)
2 1zzd 12542 . . 3 (πœ‘ β†’ 1 ∈ β„€)
3 mertens.9 . . . . 5 (πœ‘ β†’ 𝐸 ∈ ℝ+)
43rphalfcld 12977 . . . 4 (πœ‘ β†’ (𝐸 / 2) ∈ ℝ+)
5 nn0uz 12813 . . . . . 6 β„•0 = (β„€β‰₯β€˜0)
6 0zd 12519 . . . . . 6 (πœ‘ β†’ 0 ∈ β„€)
7 eqidd 2734 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ β„•0) β†’ (πΎβ€˜π‘—) = (πΎβ€˜π‘—))
8 mertens.2 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ β„•0) β†’ (πΎβ€˜π‘—) = (absβ€˜π΄))
9 mertens.3 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ β„•0) β†’ 𝐴 ∈ β„‚)
109abscld 15330 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ β„•0) β†’ (absβ€˜π΄) ∈ ℝ)
118, 10eqeltrd 2834 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ β„•0) β†’ (πΎβ€˜π‘—) ∈ ℝ)
12 mertens.7 . . . . . 6 (πœ‘ β†’ seq0( + , 𝐾) ∈ dom ⇝ )
135, 6, 7, 11, 12isumrecl 15658 . . . . 5 (πœ‘ β†’ Σ𝑗 ∈ β„•0 (πΎβ€˜π‘—) ∈ ℝ)
149absge0d 15338 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ β„•0) β†’ 0 ≀ (absβ€˜π΄))
1514, 8breqtrrd 5137 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ β„•0) β†’ 0 ≀ (πΎβ€˜π‘—))
165, 6, 7, 11, 12, 15isumge0 15659 . . . . 5 (πœ‘ β†’ 0 ≀ Σ𝑗 ∈ β„•0 (πΎβ€˜π‘—))
1713, 16ge0p1rpd 12995 . . . 4 (πœ‘ β†’ (Σ𝑗 ∈ β„•0 (πΎβ€˜π‘—) + 1) ∈ ℝ+)
184, 17rpdivcld 12982 . . 3 (πœ‘ β†’ ((𝐸 / 2) / (Σ𝑗 ∈ β„•0 (πΎβ€˜π‘—) + 1)) ∈ ℝ+)
19 eqidd 2734 . . 3 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (seq0( + , 𝐺)β€˜π‘š) = (seq0( + , 𝐺)β€˜π‘š))
20 mertens.4 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (πΊβ€˜π‘˜) = 𝐡)
21 mertens.5 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ 𝐡 ∈ β„‚)
22 mertens.8 . . . 4 (πœ‘ β†’ seq0( + , 𝐺) ∈ dom ⇝ )
235, 6, 20, 21, 22isumclim2 15651 . . 3 (πœ‘ β†’ seq0( + , 𝐺) ⇝ Ξ£π‘˜ ∈ β„•0 𝐡)
241, 2, 18, 19, 23climi2 15402 . 2 (πœ‘ β†’ βˆƒπ‘  ∈ β„• βˆ€π‘š ∈ (β„€β‰₯β€˜π‘ )(absβ€˜((seq0( + , 𝐺)β€˜π‘š) βˆ’ Ξ£π‘˜ ∈ β„•0 𝐡)) < ((𝐸 / 2) / (Σ𝑗 ∈ β„•0 (πΎβ€˜π‘—) + 1)))
25 eluznn 12851 . . . . . . . 8 ((𝑠 ∈ β„• ∧ π‘š ∈ (β„€β‰₯β€˜π‘ )) β†’ π‘š ∈ β„•)
2620, 21eqeltrd 2834 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (πΊβ€˜π‘˜) ∈ β„‚)
275, 6, 26serf 13945 . . . . . . . . . . . 12 (πœ‘ β†’ seq0( + , 𝐺):β„•0βŸΆβ„‚)
28 nnnn0 12428 . . . . . . . . . . . 12 (π‘š ∈ β„• β†’ π‘š ∈ β„•0)
29 ffvelcdm 7036 . . . . . . . . . . . 12 ((seq0( + , 𝐺):β„•0βŸΆβ„‚ ∧ π‘š ∈ β„•0) β†’ (seq0( + , 𝐺)β€˜π‘š) ∈ β„‚)
3027, 28, 29syl2an 597 . . . . . . . . . . 11 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (seq0( + , 𝐺)β€˜π‘š) ∈ β„‚)
315, 6, 20, 21, 22isumcl 15654 . . . . . . . . . . . 12 (πœ‘ β†’ Ξ£π‘˜ ∈ β„•0 𝐡 ∈ β„‚)
3231adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ π‘š ∈ β„•) β†’ Ξ£π‘˜ ∈ β„•0 𝐡 ∈ β„‚)
3330, 32abssubd 15347 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (absβ€˜((seq0( + , 𝐺)β€˜π‘š) βˆ’ Ξ£π‘˜ ∈ β„•0 𝐡)) = (absβ€˜(Ξ£π‘˜ ∈ β„•0 𝐡 βˆ’ (seq0( + , 𝐺)β€˜π‘š))))
34 eqid 2733 . . . . . . . . . . . . . 14 (β„€β‰₯β€˜(π‘š + 1)) = (β„€β‰₯β€˜(π‘š + 1))
3528adantl 483 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ β„•) β†’ π‘š ∈ β„•0)
36 peano2nn0 12461 . . . . . . . . . . . . . . . 16 (π‘š ∈ β„•0 β†’ (π‘š + 1) ∈ β„•0)
3735, 36syl 17 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (π‘š + 1) ∈ β„•0)
3837nn0zd 12533 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (π‘š + 1) ∈ β„€)
39 simpll 766 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜(π‘š + 1))) β†’ πœ‘)
40 eluznn0 12850 . . . . . . . . . . . . . . . 16 (((π‘š + 1) ∈ β„•0 ∧ π‘˜ ∈ (β„€β‰₯β€˜(π‘š + 1))) β†’ π‘˜ ∈ β„•0)
4137, 40sylan 581 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜(π‘š + 1))) β†’ π‘˜ ∈ β„•0)
4239, 41, 20syl2anc 585 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘š ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜(π‘š + 1))) β†’ (πΊβ€˜π‘˜) = 𝐡)
4339, 41, 21syl2anc 585 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘š ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜(π‘š + 1))) β†’ 𝐡 ∈ β„‚)
4422adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ β„•) β†’ seq0( + , 𝐺) ∈ dom ⇝ )
4526adantlr 714 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘š ∈ β„•) ∧ π‘˜ ∈ β„•0) β†’ (πΊβ€˜π‘˜) ∈ β„‚)
465, 37, 45iserex 15550 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (seq0( + , 𝐺) ∈ dom ⇝ ↔ seq(π‘š + 1)( + , 𝐺) ∈ dom ⇝ ))
4744, 46mpbid 231 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘š ∈ β„•) β†’ seq(π‘š + 1)( + , 𝐺) ∈ dom ⇝ )
4834, 38, 42, 43, 47isumcl 15654 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ β„•) β†’ Ξ£π‘˜ ∈ (β„€β‰₯β€˜(π‘š + 1))𝐡 ∈ β„‚)
4930, 48pncan2d 11522 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (((seq0( + , 𝐺)β€˜π‘š) + Ξ£π‘˜ ∈ (β„€β‰₯β€˜(π‘š + 1))𝐡) βˆ’ (seq0( + , 𝐺)β€˜π‘š)) = Ξ£π‘˜ ∈ (β„€β‰₯β€˜(π‘š + 1))𝐡)
5020adantlr 714 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ β„•) ∧ π‘˜ ∈ β„•0) β†’ (πΊβ€˜π‘˜) = 𝐡)
5121adantlr 714 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ β„•) ∧ π‘˜ ∈ β„•0) β†’ 𝐡 ∈ β„‚)
525, 34, 37, 50, 51, 44isumsplit 15733 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘š ∈ β„•) β†’ Ξ£π‘˜ ∈ β„•0 𝐡 = (Ξ£π‘˜ ∈ (0...((π‘š + 1) βˆ’ 1))𝐡 + Ξ£π‘˜ ∈ (β„€β‰₯β€˜(π‘š + 1))𝐡))
53 nncn 12169 . . . . . . . . . . . . . . . . . . . 20 (π‘š ∈ β„• β†’ π‘š ∈ β„‚)
5453adantl 483 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘š ∈ β„•) β†’ π‘š ∈ β„‚)
55 ax-1cn 11117 . . . . . . . . . . . . . . . . . . 19 1 ∈ β„‚
56 pncan 11415 . . . . . . . . . . . . . . . . . . 19 ((π‘š ∈ β„‚ ∧ 1 ∈ β„‚) β†’ ((π‘š + 1) βˆ’ 1) = π‘š)
5754, 55, 56sylancl 587 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘š ∈ β„•) β†’ ((π‘š + 1) βˆ’ 1) = π‘š)
5857oveq2d 7377 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (0...((π‘š + 1) βˆ’ 1)) = (0...π‘š))
5958sumeq1d 15594 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ β„•) β†’ Ξ£π‘˜ ∈ (0...((π‘š + 1) βˆ’ 1))𝐡 = Ξ£π‘˜ ∈ (0...π‘š)𝐡)
60 simpl 484 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘š ∈ β„•) β†’ πœ‘)
61 elfznn0 13543 . . . . . . . . . . . . . . . . . 18 (π‘˜ ∈ (0...π‘š) β†’ π‘˜ ∈ β„•0)
6260, 61, 20syl2an 597 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘š ∈ β„•) ∧ π‘˜ ∈ (0...π‘š)) β†’ (πΊβ€˜π‘˜) = 𝐡)
6335, 5eleqtrdi 2844 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„•) β†’ π‘š ∈ (β„€β‰₯β€˜0))
6460, 61, 21syl2an 597 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘š ∈ β„•) ∧ π‘˜ ∈ (0...π‘š)) β†’ 𝐡 ∈ β„‚)
6562, 63, 64fsumser 15623 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘š ∈ β„•) β†’ Ξ£π‘˜ ∈ (0...π‘š)𝐡 = (seq0( + , 𝐺)β€˜π‘š))
6659, 65eqtrd 2773 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ β„•) β†’ Ξ£π‘˜ ∈ (0...((π‘š + 1) βˆ’ 1))𝐡 = (seq0( + , 𝐺)β€˜π‘š))
6766oveq1d 7376 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (Ξ£π‘˜ ∈ (0...((π‘š + 1) βˆ’ 1))𝐡 + Ξ£π‘˜ ∈ (β„€β‰₯β€˜(π‘š + 1))𝐡) = ((seq0( + , 𝐺)β€˜π‘š) + Ξ£π‘˜ ∈ (β„€β‰₯β€˜(π‘š + 1))𝐡))
6852, 67eqtrd 2773 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ β„•) β†’ Ξ£π‘˜ ∈ β„•0 𝐡 = ((seq0( + , 𝐺)β€˜π‘š) + Ξ£π‘˜ ∈ (β„€β‰₯β€˜(π‘š + 1))𝐡))
6968oveq1d 7376 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (Ξ£π‘˜ ∈ β„•0 𝐡 βˆ’ (seq0( + , 𝐺)β€˜π‘š)) = (((seq0( + , 𝐺)β€˜π‘š) + Ξ£π‘˜ ∈ (β„€β‰₯β€˜(π‘š + 1))𝐡) βˆ’ (seq0( + , 𝐺)β€˜π‘š)))
7042sumeq2dv 15596 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ β„•) β†’ Ξ£π‘˜ ∈ (β„€β‰₯β€˜(π‘š + 1))(πΊβ€˜π‘˜) = Ξ£π‘˜ ∈ (β„€β‰₯β€˜(π‘š + 1))𝐡)
7149, 69, 703eqtr4d 2783 . . . . . . . . . . 11 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (Ξ£π‘˜ ∈ β„•0 𝐡 βˆ’ (seq0( + , 𝐺)β€˜π‘š)) = Ξ£π‘˜ ∈ (β„€β‰₯β€˜(π‘š + 1))(πΊβ€˜π‘˜))
7271fveq2d 6850 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (absβ€˜(Ξ£π‘˜ ∈ β„•0 𝐡 βˆ’ (seq0( + , 𝐺)β€˜π‘š))) = (absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(π‘š + 1))(πΊβ€˜π‘˜)))
7333, 72eqtrd 2773 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (absβ€˜((seq0( + , 𝐺)β€˜π‘š) βˆ’ Ξ£π‘˜ ∈ β„•0 𝐡)) = (absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(π‘š + 1))(πΊβ€˜π‘˜)))
7473breq1d 5119 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ β„•) β†’ ((absβ€˜((seq0( + , 𝐺)β€˜π‘š) βˆ’ Ξ£π‘˜ ∈ β„•0 𝐡)) < ((𝐸 / 2) / (Σ𝑗 ∈ β„•0 (πΎβ€˜π‘—) + 1)) ↔ (absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(π‘š + 1))(πΊβ€˜π‘˜)) < ((𝐸 / 2) / (Σ𝑗 ∈ β„•0 (πΎβ€˜π‘—) + 1))))
7525, 74sylan2 594 . . . . . . 7 ((πœ‘ ∧ (𝑠 ∈ β„• ∧ π‘š ∈ (β„€β‰₯β€˜π‘ ))) β†’ ((absβ€˜((seq0( + , 𝐺)β€˜π‘š) βˆ’ Ξ£π‘˜ ∈ β„•0 𝐡)) < ((𝐸 / 2) / (Σ𝑗 ∈ β„•0 (πΎβ€˜π‘—) + 1)) ↔ (absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(π‘š + 1))(πΊβ€˜π‘˜)) < ((𝐸 / 2) / (Σ𝑗 ∈ β„•0 (πΎβ€˜π‘—) + 1))))
7675anassrs 469 . . . . . 6 (((πœ‘ ∧ 𝑠 ∈ β„•) ∧ π‘š ∈ (β„€β‰₯β€˜π‘ )) β†’ ((absβ€˜((seq0( + , 𝐺)β€˜π‘š) βˆ’ Ξ£π‘˜ ∈ β„•0 𝐡)) < ((𝐸 / 2) / (Σ𝑗 ∈ β„•0 (πΎβ€˜π‘—) + 1)) ↔ (absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(π‘š + 1))(πΊβ€˜π‘˜)) < ((𝐸 / 2) / (Σ𝑗 ∈ β„•0 (πΎβ€˜π‘—) + 1))))
7776ralbidva 3169 . . . . 5 ((πœ‘ ∧ 𝑠 ∈ β„•) β†’ (βˆ€π‘š ∈ (β„€β‰₯β€˜π‘ )(absβ€˜((seq0( + , 𝐺)β€˜π‘š) βˆ’ Ξ£π‘˜ ∈ β„•0 𝐡)) < ((𝐸 / 2) / (Σ𝑗 ∈ β„•0 (πΎβ€˜π‘—) + 1)) ↔ βˆ€π‘š ∈ (β„€β‰₯β€˜π‘ )(absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(π‘š + 1))(πΊβ€˜π‘˜)) < ((𝐸 / 2) / (Σ𝑗 ∈ β„•0 (πΎβ€˜π‘—) + 1))))
78 fvoveq1 7384 . . . . . . . . 9 (π‘š = 𝑛 β†’ (β„€β‰₯β€˜(π‘š + 1)) = (β„€β‰₯β€˜(𝑛 + 1)))
7978sumeq1d 15594 . . . . . . . 8 (π‘š = 𝑛 β†’ Ξ£π‘˜ ∈ (β„€β‰₯β€˜(π‘š + 1))(πΊβ€˜π‘˜) = Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜))
8079fveq2d 6850 . . . . . . 7 (π‘š = 𝑛 β†’ (absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(π‘š + 1))(πΊβ€˜π‘˜)) = (absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜)))
8180breq1d 5119 . . . . . 6 (π‘š = 𝑛 β†’ ((absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(π‘š + 1))(πΊβ€˜π‘˜)) < ((𝐸 / 2) / (Σ𝑗 ∈ β„•0 (πΎβ€˜π‘—) + 1)) ↔ (absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜)) < ((𝐸 / 2) / (Σ𝑗 ∈ β„•0 (πΎβ€˜π‘—) + 1))))
8281cbvralvw 3224 . . . . 5 (βˆ€π‘š ∈ (β„€β‰₯β€˜π‘ )(absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(π‘š + 1))(πΊβ€˜π‘˜)) < ((𝐸 / 2) / (Σ𝑗 ∈ β„•0 (πΎβ€˜π‘—) + 1)) ↔ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘ )(absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜)) < ((𝐸 / 2) / (Σ𝑗 ∈ β„•0 (πΎβ€˜π‘—) + 1)))
8377, 82bitrdi 287 . . . 4 ((πœ‘ ∧ 𝑠 ∈ β„•) β†’ (βˆ€π‘š ∈ (β„€β‰₯β€˜π‘ )(absβ€˜((seq0( + , 𝐺)β€˜π‘š) βˆ’ Ξ£π‘˜ ∈ β„•0 𝐡)) < ((𝐸 / 2) / (Σ𝑗 ∈ β„•0 (πΎβ€˜π‘—) + 1)) ↔ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘ )(absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜)) < ((𝐸 / 2) / (Σ𝑗 ∈ β„•0 (πΎβ€˜π‘—) + 1))))
84 mertens.11 . . . . . 6 (πœ“ ↔ (𝑠 ∈ β„• ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘ )(absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜)) < ((𝐸 / 2) / (Σ𝑗 ∈ β„•0 (πΎβ€˜π‘—) + 1))))
85 0zd 12519 . . . . . . . . 9 ((πœ‘ ∧ πœ“) β†’ 0 ∈ β„€)
864adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ (𝐸 / 2) ∈ ℝ+)
8784simplbi 499 . . . . . . . . . . . . 13 (πœ“ β†’ 𝑠 ∈ β„•)
8887adantl 483 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ“) β†’ 𝑠 ∈ β„•)
8988nnrpd 12963 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ 𝑠 ∈ ℝ+)
9086, 89rpdivcld 12982 . . . . . . . . . 10 ((πœ‘ ∧ πœ“) β†’ ((𝐸 / 2) / 𝑠) ∈ ℝ+)
91 mertens.10 . . . . . . . . . . . . 13 𝑇 = {𝑧 ∣ βˆƒπ‘› ∈ (0...(𝑠 βˆ’ 1))𝑧 = (absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜))}
92 eqid 2733 . . . . . . . . . . . . . . . . . 18 (β„€β‰₯β€˜(𝑛 + 1)) = (β„€β‰₯β€˜(𝑛 + 1))
93 elfznn0 13543 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (0...(𝑠 βˆ’ 1)) β†’ 𝑛 ∈ β„•0)
9493adantl 483 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ πœ“) ∧ 𝑛 ∈ (0...(𝑠 βˆ’ 1))) β†’ 𝑛 ∈ β„•0)
95 peano2nn0 12461 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ β„•0 β†’ (𝑛 + 1) ∈ β„•0)
9694, 95syl 17 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ πœ“) ∧ 𝑛 ∈ (0...(𝑠 βˆ’ 1))) β†’ (𝑛 + 1) ∈ β„•0)
9796nn0zd 12533 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ πœ“) ∧ 𝑛 ∈ (0...(𝑠 βˆ’ 1))) β†’ (𝑛 + 1) ∈ β„€)
98 eqidd 2734 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ πœ“) ∧ 𝑛 ∈ (0...(𝑠 βˆ’ 1))) ∧ π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))) β†’ (πΊβ€˜π‘˜) = (πΊβ€˜π‘˜))
99 simplll 774 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ πœ“) ∧ 𝑛 ∈ (0...(𝑠 βˆ’ 1))) ∧ π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))) β†’ πœ‘)
100 eluznn0 12850 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 + 1) ∈ β„•0 ∧ π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))) β†’ π‘˜ ∈ β„•0)
10196, 100sylan 581 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ πœ“) ∧ 𝑛 ∈ (0...(𝑠 βˆ’ 1))) ∧ π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))) β†’ π‘˜ ∈ β„•0)
10299, 101, 26syl2anc 585 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ πœ“) ∧ 𝑛 ∈ (0...(𝑠 βˆ’ 1))) ∧ π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))) β†’ (πΊβ€˜π‘˜) ∈ β„‚)
10322ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ πœ“) ∧ 𝑛 ∈ (0...(𝑠 βˆ’ 1))) β†’ seq0( + , 𝐺) ∈ dom ⇝ )
10426ad4ant14 751 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ πœ“) ∧ 𝑛 ∈ (0...(𝑠 βˆ’ 1))) ∧ π‘˜ ∈ β„•0) β†’ (πΊβ€˜π‘˜) ∈ β„‚)
1055, 96, 104iserex 15550 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ πœ“) ∧ 𝑛 ∈ (0...(𝑠 βˆ’ 1))) β†’ (seq0( + , 𝐺) ∈ dom ⇝ ↔ seq(𝑛 + 1)( + , 𝐺) ∈ dom ⇝ ))
106103, 105mpbid 231 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ πœ“) ∧ 𝑛 ∈ (0...(𝑠 βˆ’ 1))) β†’ seq(𝑛 + 1)( + , 𝐺) ∈ dom ⇝ )
10792, 97, 98, 102, 106isumcl 15654 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ πœ“) ∧ 𝑛 ∈ (0...(𝑠 βˆ’ 1))) β†’ Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜) ∈ β„‚)
108107abscld 15330 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ πœ“) ∧ 𝑛 ∈ (0...(𝑠 βˆ’ 1))) β†’ (absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜)) ∈ ℝ)
109 eleq1a 2829 . . . . . . . . . . . . . . . 16 ((absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜)) ∈ ℝ β†’ (𝑧 = (absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜)) β†’ 𝑧 ∈ ℝ))
110108, 109syl 17 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ πœ“) ∧ 𝑛 ∈ (0...(𝑠 βˆ’ 1))) β†’ (𝑧 = (absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜)) β†’ 𝑧 ∈ ℝ))
111110rexlimdva 3149 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ“) β†’ (βˆƒπ‘› ∈ (0...(𝑠 βˆ’ 1))𝑧 = (absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜)) β†’ 𝑧 ∈ ℝ))
112111abssdv 4029 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ“) β†’ {𝑧 ∣ βˆƒπ‘› ∈ (0...(𝑠 βˆ’ 1))𝑧 = (absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜))} βŠ† ℝ)
11391, 112eqsstrid 3996 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ“) β†’ 𝑇 βŠ† ℝ)
114 fzfid 13887 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ“) β†’ (0...(𝑠 βˆ’ 1)) ∈ Fin)
115 abrexfi 9302 . . . . . . . . . . . . . . 15 ((0...(𝑠 βˆ’ 1)) ∈ Fin β†’ {𝑧 ∣ βˆƒπ‘› ∈ (0...(𝑠 βˆ’ 1))𝑧 = (absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜))} ∈ Fin)
116114, 115syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ“) β†’ {𝑧 ∣ βˆƒπ‘› ∈ (0...(𝑠 βˆ’ 1))𝑧 = (absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜))} ∈ Fin)
11791, 116eqeltrid 2838 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ“) β†’ 𝑇 ∈ Fin)
118 nnm1nn0 12462 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ β„• β†’ (𝑠 βˆ’ 1) ∈ β„•0)
11988, 118syl 17 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ πœ“) β†’ (𝑠 βˆ’ 1) ∈ β„•0)
120119, 5eleqtrdi 2844 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ πœ“) β†’ (𝑠 βˆ’ 1) ∈ (β„€β‰₯β€˜0))
121 eluzfz1 13457 . . . . . . . . . . . . . . . . 17 ((𝑠 βˆ’ 1) ∈ (β„€β‰₯β€˜0) β†’ 0 ∈ (0...(𝑠 βˆ’ 1)))
122120, 121syl 17 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ πœ“) β†’ 0 ∈ (0...(𝑠 βˆ’ 1)))
123 nnnn0 12428 . . . . . . . . . . . . . . . . . . . . 21 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„•0)
124123, 20sylan2 594 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (πΊβ€˜π‘˜) = 𝐡)
125124sumeq2dv 15596 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ Ξ£π‘˜ ∈ β„• (πΊβ€˜π‘˜) = Ξ£π‘˜ ∈ β„• 𝐡)
126125adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ πœ“) β†’ Ξ£π‘˜ ∈ β„• (πΊβ€˜π‘˜) = Ξ£π‘˜ ∈ β„• 𝐡)
127126fveq2d 6850 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ πœ“) β†’ (absβ€˜Ξ£π‘˜ ∈ β„• (πΊβ€˜π‘˜)) = (absβ€˜Ξ£π‘˜ ∈ β„• 𝐡))
128127eqcomd 2739 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ πœ“) β†’ (absβ€˜Ξ£π‘˜ ∈ β„• 𝐡) = (absβ€˜Ξ£π‘˜ ∈ β„• (πΊβ€˜π‘˜)))
129 fv0p1e1 12284 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 0 β†’ (β„€β‰₯β€˜(𝑛 + 1)) = (β„€β‰₯β€˜1))
130129, 1eqtr4di 2791 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 0 β†’ (β„€β‰₯β€˜(𝑛 + 1)) = β„•)
131130sumeq1d 15594 . . . . . . . . . . . . . . . . . 18 (𝑛 = 0 β†’ Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜) = Ξ£π‘˜ ∈ β„• (πΊβ€˜π‘˜))
132131fveq2d 6850 . . . . . . . . . . . . . . . . 17 (𝑛 = 0 β†’ (absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜)) = (absβ€˜Ξ£π‘˜ ∈ β„• (πΊβ€˜π‘˜)))
133132rspceeqv 3599 . . . . . . . . . . . . . . . 16 ((0 ∈ (0...(𝑠 βˆ’ 1)) ∧ (absβ€˜Ξ£π‘˜ ∈ β„• 𝐡) = (absβ€˜Ξ£π‘˜ ∈ β„• (πΊβ€˜π‘˜))) β†’ βˆƒπ‘› ∈ (0...(𝑠 βˆ’ 1))(absβ€˜Ξ£π‘˜ ∈ β„• 𝐡) = (absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜)))
134122, 128, 133syl2anc 585 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ πœ“) β†’ βˆƒπ‘› ∈ (0...(𝑠 βˆ’ 1))(absβ€˜Ξ£π‘˜ ∈ β„• 𝐡) = (absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜)))
135 fvex 6859 . . . . . . . . . . . . . . . 16 (absβ€˜Ξ£π‘˜ ∈ β„• 𝐡) ∈ V
136 eqeq1 2737 . . . . . . . . . . . . . . . . 17 (𝑧 = (absβ€˜Ξ£π‘˜ ∈ β„• 𝐡) β†’ (𝑧 = (absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜)) ↔ (absβ€˜Ξ£π‘˜ ∈ β„• 𝐡) = (absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜))))
137136rexbidv 3172 . . . . . . . . . . . . . . . 16 (𝑧 = (absβ€˜Ξ£π‘˜ ∈ β„• 𝐡) β†’ (βˆƒπ‘› ∈ (0...(𝑠 βˆ’ 1))𝑧 = (absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜)) ↔ βˆƒπ‘› ∈ (0...(𝑠 βˆ’ 1))(absβ€˜Ξ£π‘˜ ∈ β„• 𝐡) = (absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜))))
138135, 137, 91elab2 3638 . . . . . . . . . . . . . . 15 ((absβ€˜Ξ£π‘˜ ∈ β„• 𝐡) ∈ 𝑇 ↔ βˆƒπ‘› ∈ (0...(𝑠 βˆ’ 1))(absβ€˜Ξ£π‘˜ ∈ β„• 𝐡) = (absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜)))
139134, 138sylibr 233 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ“) β†’ (absβ€˜Ξ£π‘˜ ∈ β„• 𝐡) ∈ 𝑇)
140139ne0d 4299 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ“) β†’ 𝑇 β‰  βˆ…)
141 ltso 11243 . . . . . . . . . . . . . 14 < Or ℝ
142 fisupcl 9413 . . . . . . . . . . . . . 14 (( < Or ℝ ∧ (𝑇 ∈ Fin ∧ 𝑇 β‰  βˆ… ∧ 𝑇 βŠ† ℝ)) β†’ sup(𝑇, ℝ, < ) ∈ 𝑇)
143141, 142mpan 689 . . . . . . . . . . . . 13 ((𝑇 ∈ Fin ∧ 𝑇 β‰  βˆ… ∧ 𝑇 βŠ† ℝ) β†’ sup(𝑇, ℝ, < ) ∈ 𝑇)
144117, 140, 113, 143syl3anc 1372 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ“) β†’ sup(𝑇, ℝ, < ) ∈ 𝑇)
145113, 144sseldd 3949 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ sup(𝑇, ℝ, < ) ∈ ℝ)
146 0red 11166 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ“) β†’ 0 ∈ ℝ)
147123, 21sylan2 594 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 𝐡 ∈ β„‚)
148 1nn0 12437 . . . . . . . . . . . . . . . . . 18 1 ∈ β„•0
149148a1i 11 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 1 ∈ β„•0)
1505, 149, 26iserex 15550 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (seq0( + , 𝐺) ∈ dom ⇝ ↔ seq1( + , 𝐺) ∈ dom ⇝ ))
15122, 150mpbid 231 . . . . . . . . . . . . . . 15 (πœ‘ β†’ seq1( + , 𝐺) ∈ dom ⇝ )
1521, 2, 124, 147, 151isumcl 15654 . . . . . . . . . . . . . 14 (πœ‘ β†’ Ξ£π‘˜ ∈ β„• 𝐡 ∈ β„‚)
153152adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ“) β†’ Ξ£π‘˜ ∈ β„• 𝐡 ∈ β„‚)
154153abscld 15330 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ“) β†’ (absβ€˜Ξ£π‘˜ ∈ β„• 𝐡) ∈ ℝ)
155153absge0d 15338 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ“) β†’ 0 ≀ (absβ€˜Ξ£π‘˜ ∈ β„• 𝐡))
156 fimaxre2 12108 . . . . . . . . . . . . . 14 ((𝑇 βŠ† ℝ ∧ 𝑇 ∈ Fin) β†’ βˆƒπ‘§ ∈ ℝ βˆ€π‘€ ∈ 𝑇 𝑀 ≀ 𝑧)
157113, 117, 156syl2anc 585 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ“) β†’ βˆƒπ‘§ ∈ ℝ βˆ€π‘€ ∈ 𝑇 𝑀 ≀ 𝑧)
158113, 140, 157, 139suprubd 12125 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ“) β†’ (absβ€˜Ξ£π‘˜ ∈ β„• 𝐡) ≀ sup(𝑇, ℝ, < ))
159146, 154, 145, 155, 158letrd 11320 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ 0 ≀ sup(𝑇, ℝ, < ))
160145, 159ge0p1rpd 12995 . . . . . . . . . 10 ((πœ‘ ∧ πœ“) β†’ (sup(𝑇, ℝ, < ) + 1) ∈ ℝ+)
16190, 160rpdivcld 12982 . . . . . . . . 9 ((πœ‘ ∧ πœ“) β†’ (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ+)
162 fveq2 6846 . . . . . . . . . . 11 (𝑛 = π‘š β†’ (πΎβ€˜π‘›) = (πΎβ€˜π‘š))
163 eqid 2733 . . . . . . . . . . 11 (𝑛 ∈ β„•0 ↦ (πΎβ€˜π‘›)) = (𝑛 ∈ β„•0 ↦ (πΎβ€˜π‘›))
164 fvex 6859 . . . . . . . . . . 11 (πΎβ€˜π‘š) ∈ V
165162, 163, 164fvmpt 6952 . . . . . . . . . 10 (π‘š ∈ β„•0 β†’ ((𝑛 ∈ β„•0 ↦ (πΎβ€˜π‘›))β€˜π‘š) = (πΎβ€˜π‘š))
166165adantl 483 . . . . . . . . 9 (((πœ‘ ∧ πœ“) ∧ π‘š ∈ β„•0) β†’ ((𝑛 ∈ β„•0 ↦ (πΎβ€˜π‘›))β€˜π‘š) = (πΎβ€˜π‘š))
167 nn0ex 12427 . . . . . . . . . . . . 13 β„•0 ∈ V
168167mptex 7177 . . . . . . . . . . . 12 (𝑛 ∈ β„•0 ↦ (πΎβ€˜π‘›)) ∈ V
169168a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ (𝑛 ∈ β„•0 ↦ (πΎβ€˜π‘›)) ∈ V)
170 elnn0uz 12816 . . . . . . . . . . . . . 14 (𝑗 ∈ β„•0 ↔ 𝑗 ∈ (β„€β‰₯β€˜0))
171 fveq2 6846 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑗 β†’ (πΎβ€˜π‘›) = (πΎβ€˜π‘—))
172 fvex 6859 . . . . . . . . . . . . . . . 16 (πΎβ€˜π‘—) ∈ V
173171, 163, 172fvmpt 6952 . . . . . . . . . . . . . . 15 (𝑗 ∈ β„•0 β†’ ((𝑛 ∈ β„•0 ↦ (πΎβ€˜π‘›))β€˜π‘—) = (πΎβ€˜π‘—))
174173adantl 483 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑗 ∈ β„•0) β†’ ((𝑛 ∈ β„•0 ↦ (πΎβ€˜π‘›))β€˜π‘—) = (πΎβ€˜π‘—))
175170, 174sylan2br 596 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ (β„€β‰₯β€˜0)) β†’ ((𝑛 ∈ β„•0 ↦ (πΎβ€˜π‘›))β€˜π‘—) = (πΎβ€˜π‘—))
1766, 175seqfeq 13942 . . . . . . . . . . . 12 (πœ‘ β†’ seq0( + , (𝑛 ∈ β„•0 ↦ (πΎβ€˜π‘›))) = seq0( + , 𝐾))
177176, 12eqeltrd 2834 . . . . . . . . . . 11 (πœ‘ β†’ seq0( + , (𝑛 ∈ β„•0 ↦ (πΎβ€˜π‘›))) ∈ dom ⇝ )
178174, 8eqtrd 2773 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ β„•0) β†’ ((𝑛 ∈ β„•0 ↦ (πΎβ€˜π‘›))β€˜π‘—) = (absβ€˜π΄))
179178, 10eqeltrd 2834 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ β„•0) β†’ ((𝑛 ∈ β„•0 ↦ (πΎβ€˜π‘›))β€˜π‘—) ∈ ℝ)
180179recnd 11191 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ β„•0) β†’ ((𝑛 ∈ β„•0 ↦ (πΎβ€˜π‘›))β€˜π‘—) ∈ β„‚)
1815, 6, 169, 177, 180serf0 15574 . . . . . . . . . 10 (πœ‘ β†’ (𝑛 ∈ β„•0 ↦ (πΎβ€˜π‘›)) ⇝ 0)
182181adantr 482 . . . . . . . . 9 ((πœ‘ ∧ πœ“) β†’ (𝑛 ∈ β„•0 ↦ (πΎβ€˜π‘›)) ⇝ 0)
1835, 85, 161, 166, 182climi0 15403 . . . . . . . 8 ((πœ‘ ∧ πœ“) β†’ βˆƒπ‘‘ ∈ β„•0 βˆ€π‘š ∈ (β„€β‰₯β€˜π‘‘)(absβ€˜(πΎβ€˜π‘š)) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
184 simplll 774 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ πœ“) ∧ 𝑑 ∈ β„•0) ∧ π‘š ∈ (β„€β‰₯β€˜π‘‘)) β†’ πœ‘)
185 eluznn0 12850 . . . . . . . . . . . . . . 15 ((𝑑 ∈ β„•0 ∧ π‘š ∈ (β„€β‰₯β€˜π‘‘)) β†’ π‘š ∈ β„•0)
186185adantll 713 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ πœ“) ∧ 𝑑 ∈ β„•0) ∧ π‘š ∈ (β„€β‰₯β€˜π‘‘)) β†’ π‘š ∈ β„•0)
18711, 15absidd 15316 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑗 ∈ β„•0) β†’ (absβ€˜(πΎβ€˜π‘—)) = (πΎβ€˜π‘—))
188187ralrimiva 3140 . . . . . . . . . . . . . . 15 (πœ‘ β†’ βˆ€π‘— ∈ β„•0 (absβ€˜(πΎβ€˜π‘—)) = (πΎβ€˜π‘—))
189 fveq2 6846 . . . . . . . . . . . . . . . . . 18 (𝑗 = π‘š β†’ (πΎβ€˜π‘—) = (πΎβ€˜π‘š))
190189fveq2d 6850 . . . . . . . . . . . . . . . . 17 (𝑗 = π‘š β†’ (absβ€˜(πΎβ€˜π‘—)) = (absβ€˜(πΎβ€˜π‘š)))
191190, 189eqeq12d 2749 . . . . . . . . . . . . . . . 16 (𝑗 = π‘š β†’ ((absβ€˜(πΎβ€˜π‘—)) = (πΎβ€˜π‘—) ↔ (absβ€˜(πΎβ€˜π‘š)) = (πΎβ€˜π‘š)))
192191rspccva 3582 . . . . . . . . . . . . . . 15 ((βˆ€π‘— ∈ β„•0 (absβ€˜(πΎβ€˜π‘—)) = (πΎβ€˜π‘—) ∧ π‘š ∈ β„•0) β†’ (absβ€˜(πΎβ€˜π‘š)) = (πΎβ€˜π‘š))
193188, 192sylan 581 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘š ∈ β„•0) β†’ (absβ€˜(πΎβ€˜π‘š)) = (πΎβ€˜π‘š))
194184, 186, 193syl2anc 585 . . . . . . . . . . . . 13 ((((πœ‘ ∧ πœ“) ∧ 𝑑 ∈ β„•0) ∧ π‘š ∈ (β„€β‰₯β€˜π‘‘)) β†’ (absβ€˜(πΎβ€˜π‘š)) = (πΎβ€˜π‘š))
195194breq1d 5119 . . . . . . . . . . . 12 ((((πœ‘ ∧ πœ“) ∧ 𝑑 ∈ β„•0) ∧ π‘š ∈ (β„€β‰₯β€˜π‘‘)) β†’ ((absβ€˜(πΎβ€˜π‘š)) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ (πΎβ€˜π‘š) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
196195ralbidva 3169 . . . . . . . . . . 11 (((πœ‘ ∧ πœ“) ∧ 𝑑 ∈ β„•0) β†’ (βˆ€π‘š ∈ (β„€β‰₯β€˜π‘‘)(absβ€˜(πΎβ€˜π‘š)) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ βˆ€π‘š ∈ (β„€β‰₯β€˜π‘‘)(πΎβ€˜π‘š) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
197162breq1d 5119 . . . . . . . . . . . 12 (𝑛 = π‘š β†’ ((πΎβ€˜π‘›) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ (πΎβ€˜π‘š) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
198197cbvralvw 3224 . . . . . . . . . . 11 (βˆ€π‘› ∈ (β„€β‰₯β€˜π‘‘)(πΎβ€˜π‘›) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ βˆ€π‘š ∈ (β„€β‰₯β€˜π‘‘)(πΎβ€˜π‘š) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))
199196, 198bitr4di 289 . . . . . . . . . 10 (((πœ‘ ∧ πœ“) ∧ 𝑑 ∈ β„•0) β†’ (βˆ€π‘š ∈ (β„€β‰₯β€˜π‘‘)(absβ€˜(πΎβ€˜π‘š)) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘‘)(πΎβ€˜π‘›) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
200 mertens.1 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ β„•0) β†’ (πΉβ€˜π‘—) = 𝐴)
201200ad4ant14 751 . . . . . . . . . . . 12 ((((πœ‘ ∧ πœ“) ∧ (𝑑 ∈ β„•0 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘‘)(πΎβ€˜π‘›) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ∧ 𝑗 ∈ β„•0) β†’ (πΉβ€˜π‘—) = 𝐴)
2028ad4ant14 751 . . . . . . . . . . . 12 ((((πœ‘ ∧ πœ“) ∧ (𝑑 ∈ β„•0 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘‘)(πΎβ€˜π‘›) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ∧ 𝑗 ∈ β„•0) β†’ (πΎβ€˜π‘—) = (absβ€˜π΄))
2039ad4ant14 751 . . . . . . . . . . . 12 ((((πœ‘ ∧ πœ“) ∧ (𝑑 ∈ β„•0 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘‘)(πΎβ€˜π‘›) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ∧ 𝑗 ∈ β„•0) β†’ 𝐴 ∈ β„‚)
20420ad4ant14 751 . . . . . . . . . . . 12 ((((πœ‘ ∧ πœ“) ∧ (𝑑 ∈ β„•0 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘‘)(πΎβ€˜π‘›) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ∧ π‘˜ ∈ β„•0) β†’ (πΊβ€˜π‘˜) = 𝐡)
20521ad4ant14 751 . . . . . . . . . . . 12 ((((πœ‘ ∧ πœ“) ∧ (𝑑 ∈ β„•0 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘‘)(πΎβ€˜π‘›) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ∧ π‘˜ ∈ β„•0) β†’ 𝐡 ∈ β„‚)
206 mertens.6 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•0) β†’ (π»β€˜π‘˜) = Σ𝑗 ∈ (0...π‘˜)(𝐴 Β· (πΊβ€˜(π‘˜ βˆ’ 𝑗))))
207206ad4ant14 751 . . . . . . . . . . . 12 ((((πœ‘ ∧ πœ“) ∧ (𝑑 ∈ β„•0 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘‘)(πΎβ€˜π‘›) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ∧ π‘˜ ∈ β„•0) β†’ (π»β€˜π‘˜) = Σ𝑗 ∈ (0...π‘˜)(𝐴 Β· (πΊβ€˜(π‘˜ βˆ’ 𝑗))))
20812ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ πœ“) ∧ (𝑑 ∈ β„•0 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘‘)(πΎβ€˜π‘›) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) β†’ seq0( + , 𝐾) ∈ dom ⇝ )
20922ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ πœ“) ∧ (𝑑 ∈ β„•0 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘‘)(πΎβ€˜π‘›) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) β†’ seq0( + , 𝐺) ∈ dom ⇝ )
2103ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ πœ“) ∧ (𝑑 ∈ β„•0 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘‘)(πΎβ€˜π‘›) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) β†’ 𝐸 ∈ ℝ+)
211198anbi2i 624 . . . . . . . . . . . . . . 15 ((𝑑 ∈ β„•0 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘‘)(πΎβ€˜π‘›) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) ↔ (𝑑 ∈ β„•0 ∧ βˆ€π‘š ∈ (β„€β‰₯β€˜π‘‘)(πΎβ€˜π‘š) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))
212211anbi2i 624 . . . . . . . . . . . . . 14 ((πœ“ ∧ (𝑑 ∈ β„•0 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘‘)(πΎβ€˜π‘›) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ↔ (πœ“ ∧ (𝑑 ∈ β„•0 ∧ βˆ€π‘š ∈ (β„€β‰₯β€˜π‘‘)(πΎβ€˜π‘š) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))))
213212biimpi 215 . . . . . . . . . . . . 13 ((πœ“ ∧ (𝑑 ∈ β„•0 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘‘)(πΎβ€˜π‘›) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) β†’ (πœ“ ∧ (𝑑 ∈ β„•0 ∧ βˆ€π‘š ∈ (β„€β‰₯β€˜π‘‘)(πΎβ€˜π‘š) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))))
214213adantll 713 . . . . . . . . . . . 12 (((πœ‘ ∧ πœ“) ∧ (𝑑 ∈ β„•0 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘‘)(πΎβ€˜π‘›) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) β†’ (πœ“ ∧ (𝑑 ∈ β„•0 ∧ βˆ€π‘š ∈ (β„€β‰₯β€˜π‘‘)(πΎβ€˜π‘š) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))))
215113, 140, 1573jca 1129 . . . . . . . . . . . . . 14 ((πœ‘ ∧ πœ“) β†’ (𝑇 βŠ† ℝ ∧ 𝑇 β‰  βˆ… ∧ βˆƒπ‘§ ∈ ℝ βˆ€π‘€ ∈ 𝑇 𝑀 ≀ 𝑧))
216159, 215jca 513 . . . . . . . . . . . . 13 ((πœ‘ ∧ πœ“) β†’ (0 ≀ sup(𝑇, ℝ, < ) ∧ (𝑇 βŠ† ℝ ∧ 𝑇 β‰  βˆ… ∧ βˆƒπ‘§ ∈ ℝ βˆ€π‘€ ∈ 𝑇 𝑀 ≀ 𝑧)))
217216adantr 482 . . . . . . . . . . . 12 (((πœ‘ ∧ πœ“) ∧ (𝑑 ∈ β„•0 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘‘)(πΎβ€˜π‘›) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) β†’ (0 ≀ sup(𝑇, ℝ, < ) ∧ (𝑇 βŠ† ℝ ∧ 𝑇 β‰  βˆ… ∧ βˆƒπ‘§ ∈ ℝ βˆ€π‘€ ∈ 𝑇 𝑀 ≀ 𝑧)))
218201, 202, 203, 204, 205, 207, 208, 209, 210, 91, 84, 214, 217mertenslem1 15777 . . . . . . . . . . 11 (((πœ‘ ∧ πœ“) ∧ (𝑑 ∈ β„•0 ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘‘)(πΎβ€˜π‘›) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) β†’ βˆƒπ‘¦ ∈ β„•0 βˆ€π‘š ∈ (β„€β‰₯β€˜π‘¦)(absβ€˜Ξ£π‘— ∈ (0...π‘š)(𝐴 Β· Ξ£π‘˜ ∈ (β„€β‰₯β€˜((π‘š βˆ’ 𝑗) + 1))𝐡)) < 𝐸)
219218expr 458 . . . . . . . . . 10 (((πœ‘ ∧ πœ“) ∧ 𝑑 ∈ β„•0) β†’ (βˆ€π‘› ∈ (β„€β‰₯β€˜π‘‘)(πΎβ€˜π‘›) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) β†’ βˆƒπ‘¦ ∈ β„•0 βˆ€π‘š ∈ (β„€β‰₯β€˜π‘¦)(absβ€˜Ξ£π‘— ∈ (0...π‘š)(𝐴 Β· Ξ£π‘˜ ∈ (β„€β‰₯β€˜((π‘š βˆ’ 𝑗) + 1))𝐡)) < 𝐸))
220199, 219sylbid 239 . . . . . . . . 9 (((πœ‘ ∧ πœ“) ∧ 𝑑 ∈ β„•0) β†’ (βˆ€π‘š ∈ (β„€β‰₯β€˜π‘‘)(absβ€˜(πΎβ€˜π‘š)) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) β†’ βˆƒπ‘¦ ∈ β„•0 βˆ€π‘š ∈ (β„€β‰₯β€˜π‘¦)(absβ€˜Ξ£π‘— ∈ (0...π‘š)(𝐴 Β· Ξ£π‘˜ ∈ (β„€β‰₯β€˜((π‘š βˆ’ 𝑗) + 1))𝐡)) < 𝐸))
221220rexlimdva 3149 . . . . . . . 8 ((πœ‘ ∧ πœ“) β†’ (βˆƒπ‘‘ ∈ β„•0 βˆ€π‘š ∈ (β„€β‰₯β€˜π‘‘)(absβ€˜(πΎβ€˜π‘š)) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) β†’ βˆƒπ‘¦ ∈ β„•0 βˆ€π‘š ∈ (β„€β‰₯β€˜π‘¦)(absβ€˜Ξ£π‘— ∈ (0...π‘š)(𝐴 Β· Ξ£π‘˜ ∈ (β„€β‰₯β€˜((π‘š βˆ’ 𝑗) + 1))𝐡)) < 𝐸))
222183, 221mpd 15 . . . . . . 7 ((πœ‘ ∧ πœ“) β†’ βˆƒπ‘¦ ∈ β„•0 βˆ€π‘š ∈ (β„€β‰₯β€˜π‘¦)(absβ€˜Ξ£π‘— ∈ (0...π‘š)(𝐴 Β· Ξ£π‘˜ ∈ (β„€β‰₯β€˜((π‘š βˆ’ 𝑗) + 1))𝐡)) < 𝐸)
223222ex 414 . . . . . 6 (πœ‘ β†’ (πœ“ β†’ βˆƒπ‘¦ ∈ β„•0 βˆ€π‘š ∈ (β„€β‰₯β€˜π‘¦)(absβ€˜Ξ£π‘— ∈ (0...π‘š)(𝐴 Β· Ξ£π‘˜ ∈ (β„€β‰₯β€˜((π‘š βˆ’ 𝑗) + 1))𝐡)) < 𝐸))
22484, 223biimtrrid 242 . . . . 5 (πœ‘ β†’ ((𝑠 ∈ β„• ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘ )(absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜)) < ((𝐸 / 2) / (Σ𝑗 ∈ β„•0 (πΎβ€˜π‘—) + 1))) β†’ βˆƒπ‘¦ ∈ β„•0 βˆ€π‘š ∈ (β„€β‰₯β€˜π‘¦)(absβ€˜Ξ£π‘— ∈ (0...π‘š)(𝐴 Β· Ξ£π‘˜ ∈ (β„€β‰₯β€˜((π‘š βˆ’ 𝑗) + 1))𝐡)) < 𝐸))
225224expdimp 454 . . . 4 ((πœ‘ ∧ 𝑠 ∈ β„•) β†’ (βˆ€π‘› ∈ (β„€β‰₯β€˜π‘ )(absβ€˜Ξ£π‘˜ ∈ (β„€β‰₯β€˜(𝑛 + 1))(πΊβ€˜π‘˜)) < ((𝐸 / 2) / (Σ𝑗 ∈ β„•0 (πΎβ€˜π‘—) + 1)) β†’ βˆƒπ‘¦ ∈ β„•0 βˆ€π‘š ∈ (β„€β‰₯β€˜π‘¦)(absβ€˜Ξ£π‘— ∈ (0...π‘š)(𝐴 Β· Ξ£π‘˜ ∈ (β„€β‰₯β€˜((π‘š βˆ’ 𝑗) + 1))𝐡)) < 𝐸))
22683, 225sylbid 239 . . 3 ((πœ‘ ∧ 𝑠 ∈ β„•) β†’ (βˆ€π‘š ∈ (β„€β‰₯β€˜π‘ )(absβ€˜((seq0( + , 𝐺)β€˜π‘š) βˆ’ Ξ£π‘˜ ∈ β„•0 𝐡)) < ((𝐸 / 2) / (Σ𝑗 ∈ β„•0 (πΎβ€˜π‘—) + 1)) β†’ βˆƒπ‘¦ ∈ β„•0 βˆ€π‘š ∈ (β„€β‰₯β€˜π‘¦)(absβ€˜Ξ£π‘— ∈ (0...π‘š)(𝐴 Β· Ξ£π‘˜ ∈ (β„€β‰₯β€˜((π‘š βˆ’ 𝑗) + 1))𝐡)) < 𝐸))
227226rexlimdva 3149 . 2 (πœ‘ β†’ (βˆƒπ‘  ∈ β„• βˆ€π‘š ∈ (β„€β‰₯β€˜π‘ )(absβ€˜((seq0( + , 𝐺)β€˜π‘š) βˆ’ Ξ£π‘˜ ∈ β„•0 𝐡)) < ((𝐸 / 2) / (Σ𝑗 ∈ β„•0 (πΎβ€˜π‘—) + 1)) β†’ βˆƒπ‘¦ ∈ β„•0 βˆ€π‘š ∈ (β„€β‰₯β€˜π‘¦)(absβ€˜Ξ£π‘— ∈ (0...π‘š)(𝐴 Β· Ξ£π‘˜ ∈ (β„€β‰₯β€˜((π‘š βˆ’ 𝑗) + 1))𝐡)) < 𝐸))
22824, 227mpd 15 1 (πœ‘ β†’ βˆƒπ‘¦ ∈ β„•0 βˆ€π‘š ∈ (β„€β‰₯β€˜π‘¦)(absβ€˜Ξ£π‘— ∈ (0...π‘š)(𝐴 Β· Ξ£π‘˜ ∈ (β„€β‰₯β€˜((π‘š βˆ’ 𝑗) + 1))𝐡)) < 𝐸)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  {cab 2710   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  Vcvv 3447   βŠ† wss 3914  βˆ…c0 4286   class class class wbr 5109   ↦ cmpt 5192   Or wor 5548  dom cdm 5637  βŸΆwf 6496  β€˜cfv 6500  (class class class)co 7361  Fincfn 8889  supcsup 9384  β„‚cc 11057  β„cr 11058  0cc0 11059  1c1 11060   + caddc 11062   Β· cmul 11064   < clt 11197   ≀ cle 11198   βˆ’ cmin 11393   / cdiv 11820  β„•cn 12161  2c2 12216  β„•0cn0 12421  β„€β‰₯cuz 12771  β„+crp 12923  ...cfz 13433  seqcseq 13915  abscabs 15128   ⇝ cli 15375  Ξ£csu 15579
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-rep 5246  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-inf2 9585  ax-cnex 11115  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135  ax-pre-mulgt0 11136  ax-pre-sup 11137
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 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-int 4912  df-iun 4960  df-br 5110  df-opab 5172  df-mpt 5193  df-tr 5227  df-id 5535  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5592  df-se 5593  df-we 5594  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-pred 6257  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7317  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7807  df-1st 7925  df-2nd 7926  df-frecs 8216  df-wrecs 8247  df-recs 8321  df-rdg 8360  df-1o 8416  df-er 8654  df-pm 8774  df-en 8890  df-dom 8891  df-sdom 8892  df-fin 8893  df-sup 9386  df-inf 9387  df-oi 9454  df-card 9883  df-pnf 11199  df-mnf 11200  df-xr 11201  df-ltxr 11202  df-le 11203  df-sub 11395  df-neg 11396  df-div 11821  df-nn 12162  df-2 12224  df-3 12225  df-n0 12422  df-z 12508  df-uz 12772  df-rp 12924  df-ico 13279  df-fz 13434  df-fzo 13577  df-fl 13706  df-seq 13916  df-exp 13977  df-hash 14240  df-cj 14993  df-re 14994  df-im 14995  df-sqrt 15129  df-abs 15130  df-limsup 15362  df-clim 15379  df-rlim 15380  df-sum 15580
This theorem is referenced by:  mertens  15779
  Copyright terms: Public domain W3C validator