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

Theorem dchrisum0re 26996
Description: Suppose 𝑋 is a non-principal Dirichlet character with Σ𝑛 ∈ β„•, 𝑋(𝑛) / 𝑛 = 0. Then 𝑋 is a real character. Part of Lemma 9.4.4 of [Shapiro], p. 382. (Contributed by Mario Carneiro, 5-May-2016.)
Hypotheses
Ref Expression
rpvmasum.z 𝑍 = (β„€/nβ„€β€˜π‘)
rpvmasum.l 𝐿 = (β„€RHomβ€˜π‘)
rpvmasum.a (πœ‘ β†’ 𝑁 ∈ β„•)
rpvmasum2.g 𝐺 = (DChrβ€˜π‘)
rpvmasum2.d 𝐷 = (Baseβ€˜πΊ)
rpvmasum2.1 1 = (0gβ€˜πΊ)
rpvmasum2.w π‘Š = {𝑦 ∈ (𝐷 βˆ– { 1 }) ∣ Ξ£π‘š ∈ β„• ((π‘¦β€˜(πΏβ€˜π‘š)) / π‘š) = 0}
dchrisum0.b (πœ‘ β†’ 𝑋 ∈ π‘Š)
Assertion
Ref Expression
dchrisum0re (πœ‘ β†’ 𝑋:(Baseβ€˜π‘)βŸΆβ„)
Distinct variable groups:   𝑦,π‘š, 1   π‘š,𝑁,𝑦   πœ‘,π‘š   π‘š,𝑍,𝑦   𝐷,π‘š,𝑦   π‘š,𝐿,𝑦   π‘š,𝑋,𝑦
Allowed substitution hints:   πœ‘(𝑦)   𝐺(𝑦,π‘š)   π‘Š(𝑦,π‘š)

Proof of Theorem dchrisum0re
Dummy variables π‘˜ 𝑛 π‘₯ 𝑓 𝑐 𝑑 π‘Ž are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rpvmasum2.g . . . 4 𝐺 = (DChrβ€˜π‘)
2 rpvmasum.z . . . 4 𝑍 = (β„€/nβ„€β€˜π‘)
3 rpvmasum2.d . . . 4 𝐷 = (Baseβ€˜πΊ)
4 eqid 2733 . . . 4 (Baseβ€˜π‘) = (Baseβ€˜π‘)
5 rpvmasum2.w . . . . . . 7 π‘Š = {𝑦 ∈ (𝐷 βˆ– { 1 }) ∣ Ξ£π‘š ∈ β„• ((π‘¦β€˜(πΏβ€˜π‘š)) / π‘š) = 0}
65ssrab3 4079 . . . . . 6 π‘Š βŠ† (𝐷 βˆ– { 1 })
7 dchrisum0.b . . . . . 6 (πœ‘ β†’ 𝑋 ∈ π‘Š)
86, 7sselid 3979 . . . . 5 (πœ‘ β†’ 𝑋 ∈ (𝐷 βˆ– { 1 }))
98eldifad 3959 . . . 4 (πœ‘ β†’ 𝑋 ∈ 𝐷)
101, 2, 3, 4, 9dchrf 26725 . . 3 (πœ‘ β†’ 𝑋:(Baseβ€˜π‘)βŸΆβ„‚)
1110ffnd 6715 . 2 (πœ‘ β†’ 𝑋 Fn (Baseβ€˜π‘))
1210ffvelcdmda 7082 . . . 4 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘)) β†’ (π‘‹β€˜π‘₯) ∈ β„‚)
13 fvco3 6986 . . . . . 6 ((𝑋:(Baseβ€˜π‘)βŸΆβ„‚ ∧ π‘₯ ∈ (Baseβ€˜π‘)) β†’ ((βˆ— ∘ 𝑋)β€˜π‘₯) = (βˆ—β€˜(π‘‹β€˜π‘₯)))
1410, 13sylan 581 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘)) β†’ ((βˆ— ∘ 𝑋)β€˜π‘₯) = (βˆ—β€˜(π‘‹β€˜π‘₯)))
15 logno1 26126 . . . . . . . 8 Β¬ (π‘₯ ∈ ℝ+ ↦ (logβ€˜π‘₯)) ∈ 𝑂(1)
16 1red 11211 . . . . . . . . . . 11 ((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) β†’ 1 ∈ ℝ)
17 rpvmasum.l . . . . . . . . . . . . 13 𝐿 = (β„€RHomβ€˜π‘)
18 rpvmasum.a . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑁 ∈ β„•)
19 rpvmasum2.1 . . . . . . . . . . . . 13 1 = (0gβ€˜πΊ)
20 eqid 2733 . . . . . . . . . . . . 13 (Unitβ€˜π‘) = (Unitβ€˜π‘)
2118nnnn0d 12528 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑁 ∈ β„•0)
222zncrng 21084 . . . . . . . . . . . . . . . 16 (𝑁 ∈ β„•0 β†’ 𝑍 ∈ CRing)
2321, 22syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑍 ∈ CRing)
24 crngring 20059 . . . . . . . . . . . . . . 15 (𝑍 ∈ CRing β†’ 𝑍 ∈ Ring)
2523, 24syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑍 ∈ Ring)
26 eqid 2733 . . . . . . . . . . . . . . 15 (1rβ€˜π‘) = (1rβ€˜π‘)
2720, 261unit 20177 . . . . . . . . . . . . . 14 (𝑍 ∈ Ring β†’ (1rβ€˜π‘) ∈ (Unitβ€˜π‘))
2825, 27syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ (1rβ€˜π‘) ∈ (Unitβ€˜π‘))
29 eqid 2733 . . . . . . . . . . . . 13 (◑𝐿 β€œ {(1rβ€˜π‘)}) = (◑𝐿 β€œ {(1rβ€˜π‘)})
30 eqidd 2734 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑓 ∈ π‘Š) β†’ (1rβ€˜π‘) = (1rβ€˜π‘))
312, 17, 18, 1, 3, 19, 5, 20, 28, 29, 30rpvmasum2 26995 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘₯ ∈ ℝ+ ↦ (((Ο•β€˜π‘) Β· Σ𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))((Ξ›β€˜π‘›) / 𝑛)) βˆ’ ((logβ€˜π‘₯) Β· (1 βˆ’ (β™―β€˜π‘Š))))) ∈ 𝑂(1))
3231adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) β†’ (π‘₯ ∈ ℝ+ ↦ (((Ο•β€˜π‘) Β· Σ𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))((Ξ›β€˜π‘›) / 𝑛)) βˆ’ ((logβ€˜π‘₯) Β· (1 βˆ’ (β™―β€˜π‘Š))))) ∈ 𝑂(1))
3318phicld 16701 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (Ο•β€˜π‘) ∈ β„•)
3433nnnn0d 12528 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (Ο•β€˜π‘) ∈ β„•0)
3534adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ (Ο•β€˜π‘) ∈ β„•0)
3635nn0red 12529 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ (Ο•β€˜π‘) ∈ ℝ)
37 fzfid 13934 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ (1...(βŒŠβ€˜π‘₯)) ∈ Fin)
38 inss1 4227 . . . . . . . . . . . . . . . . 17 ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)})) βŠ† (1...(βŒŠβ€˜π‘₯))
39 ssfi 9169 . . . . . . . . . . . . . . . . 17 (((1...(βŒŠβ€˜π‘₯)) ∈ Fin ∧ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)})) βŠ† (1...(βŒŠβ€˜π‘₯))) β†’ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)})) ∈ Fin)
4037, 38, 39sylancl 587 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)})) ∈ Fin)
41 elinel1 4194 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)})) β†’ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯)))
42 elfznn 13526 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...(βŒŠβ€˜π‘₯)) β†’ 𝑛 ∈ β„•)
4342adantl 483 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 𝑛 ∈ β„•)
4441, 43sylan2 594 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))) β†’ 𝑛 ∈ β„•)
45 vmacl 26602 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ β„• β†’ (Ξ›β€˜π‘›) ∈ ℝ)
46 nndivre 12249 . . . . . . . . . . . . . . . . . 18 (((Ξ›β€˜π‘›) ∈ ℝ ∧ 𝑛 ∈ β„•) β†’ ((Ξ›β€˜π‘›) / 𝑛) ∈ ℝ)
4745, 46mpancom 687 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ β„• β†’ ((Ξ›β€˜π‘›) / 𝑛) ∈ ℝ)
4844, 47syl 17 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))) β†’ ((Ξ›β€˜π‘›) / 𝑛) ∈ ℝ)
4940, 48fsumrecl 15676 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ Σ𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))((Ξ›β€˜π‘›) / 𝑛) ∈ ℝ)
5036, 49remulcld 11240 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ ((Ο•β€˜π‘) Β· Σ𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))((Ξ›β€˜π‘›) / 𝑛)) ∈ ℝ)
51 relogcl 26066 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ ℝ+ β†’ (logβ€˜π‘₯) ∈ ℝ)
5251adantl 483 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ (logβ€˜π‘₯) ∈ ℝ)
53 1re 11210 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
541, 3dchrfi 26738 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ β„• β†’ 𝐷 ∈ Fin)
5518, 54syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐷 ∈ Fin)
56 difss 4130 . . . . . . . . . . . . . . . . . . . . 21 (𝐷 βˆ– { 1 }) βŠ† 𝐷
576, 56sstri 3990 . . . . . . . . . . . . . . . . . . . 20 π‘Š βŠ† 𝐷
58 ssfi 9169 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ Fin ∧ π‘Š βŠ† 𝐷) β†’ π‘Š ∈ Fin)
5955, 57, 58sylancl 587 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ π‘Š ∈ Fin)
60 hashcl 14312 . . . . . . . . . . . . . . . . . . 19 (π‘Š ∈ Fin β†’ (β™―β€˜π‘Š) ∈ β„•0)
6159, 60syl 17 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (β™―β€˜π‘Š) ∈ β„•0)
6261nn0red 12529 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (β™―β€˜π‘Š) ∈ ℝ)
63 resubcl 11520 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ ∧ (β™―β€˜π‘Š) ∈ ℝ) β†’ (1 βˆ’ (β™―β€˜π‘Š)) ∈ ℝ)
6453, 62, 63sylancr 588 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (1 βˆ’ (β™―β€˜π‘Š)) ∈ ℝ)
6564adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ (1 βˆ’ (β™―β€˜π‘Š)) ∈ ℝ)
6652, 65remulcld 11240 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ ((logβ€˜π‘₯) Β· (1 βˆ’ (β™―β€˜π‘Š))) ∈ ℝ)
6750, 66resubcld 11638 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ (((Ο•β€˜π‘) Β· Σ𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))((Ξ›β€˜π‘›) / 𝑛)) βˆ’ ((logβ€˜π‘₯) Β· (1 βˆ’ (β™―β€˜π‘Š)))) ∈ ℝ)
6867recnd 11238 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ (((Ο•β€˜π‘) Β· Σ𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))((Ξ›β€˜π‘›) / 𝑛)) βˆ’ ((logβ€˜π‘₯) Β· (1 βˆ’ (β™―β€˜π‘Š)))) ∈ β„‚)
6968adantlr 714 . . . . . . . . . . 11 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ π‘₯ ∈ ℝ+) β†’ (((Ο•β€˜π‘) Β· Σ𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))((Ξ›β€˜π‘›) / 𝑛)) βˆ’ ((logβ€˜π‘₯) Β· (1 βˆ’ (β™―β€˜π‘Š)))) ∈ β„‚)
7051adantl 483 . . . . . . . . . . . 12 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ π‘₯ ∈ ℝ+) β†’ (logβ€˜π‘₯) ∈ ℝ)
7170recnd 11238 . . . . . . . . . . 11 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ π‘₯ ∈ ℝ+) β†’ (logβ€˜π‘₯) ∈ β„‚)
7251ad2antrl 727 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ (logβ€˜π‘₯) ∈ ℝ)
7366ad2ant2r 746 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ ((logβ€˜π‘₯) Β· (1 βˆ’ (β™―β€˜π‘Š))) ∈ ℝ)
7472, 73readdcld 11239 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ ((logβ€˜π‘₯) + ((logβ€˜π‘₯) Β· (1 βˆ’ (β™―β€˜π‘Š)))) ∈ ℝ)
75 0red 11213 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ 0 ∈ ℝ)
7650ad2ant2r 746 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ ((Ο•β€˜π‘) Β· Σ𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))((Ξ›β€˜π‘›) / 𝑛)) ∈ ℝ)
77 2re 12282 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
7877a1i 11 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ 2 ∈ ℝ)
7962ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ (β™―β€˜π‘Š) ∈ ℝ)
8078, 79resubcld 11638 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ (2 βˆ’ (β™―β€˜π‘Š)) ∈ ℝ)
81 log1 26076 . . . . . . . . . . . . . . . . 17 (logβ€˜1) = 0
82 simprr 772 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ 1 ≀ π‘₯)
83 1rp 12974 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ+
84 simprl 770 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ π‘₯ ∈ ℝ+)
85 logleb 26093 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℝ+ ∧ π‘₯ ∈ ℝ+) β†’ (1 ≀ π‘₯ ↔ (logβ€˜1) ≀ (logβ€˜π‘₯)))
8683, 84, 85sylancr 588 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ (1 ≀ π‘₯ ↔ (logβ€˜1) ≀ (logβ€˜π‘₯)))
8782, 86mpbid 231 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ (logβ€˜1) ≀ (logβ€˜π‘₯))
8881, 87eqbrtrrid 5183 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ 0 ≀ (logβ€˜π‘₯))
8959ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ π‘Š ∈ Fin)
90 eqid 2733 . . . . . . . . . . . . . . . . . . . . . . 23 (invgβ€˜πΊ) = (invgβ€˜πΊ)
911, 3, 9, 90dchrinv 26744 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ((invgβ€˜πΊ)β€˜π‘‹) = (βˆ— ∘ 𝑋))
921dchrabl 26737 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ β„• β†’ 𝐺 ∈ Abel)
9318, 92syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 𝐺 ∈ Abel)
94 ablgrp 19646 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐺 ∈ Abel β†’ 𝐺 ∈ Grp)
9593, 94syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ 𝐺 ∈ Grp)
963, 90grpinvcl 18868 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐷) β†’ ((invgβ€˜πΊ)β€˜π‘‹) ∈ 𝐷)
9795, 9, 96syl2anc 585 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ((invgβ€˜πΊ)β€˜π‘‹) ∈ 𝐷)
9891, 97eqeltrrd 2835 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (βˆ— ∘ 𝑋) ∈ 𝐷)
99 eldifsni 4792 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑋 ∈ (𝐷 βˆ– { 1 }) β†’ 𝑋 β‰  1 )
1008, 99syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ 𝑋 β‰  1 )
1013, 19grpidcl 18846 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐺 ∈ Grp β†’ 1 ∈ 𝐷)
10295, 101syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 1 ∈ 𝐷)
1033, 90, 95, 9, 102grpinv11 18888 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (((invgβ€˜πΊ)β€˜π‘‹) = ((invgβ€˜πΊ)β€˜ 1 ) ↔ 𝑋 = 1 ))
104103necon3bid 2986 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (((invgβ€˜πΊ)β€˜π‘‹) β‰  ((invgβ€˜πΊ)β€˜ 1 ) ↔ 𝑋 β‰  1 ))
105100, 104mpbird 257 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ((invgβ€˜πΊ)β€˜π‘‹) β‰  ((invgβ€˜πΊ)β€˜ 1 ))
10619, 90grpinvid 18880 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 ∈ Grp β†’ ((invgβ€˜πΊ)β€˜ 1 ) = 1 )
10795, 106syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ((invgβ€˜πΊ)β€˜ 1 ) = 1 )
108105, 91, 1073netr3d 3018 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (βˆ— ∘ 𝑋) β‰  1 )
109 eldifsn 4789 . . . . . . . . . . . . . . . . . . . . 21 ((βˆ— ∘ 𝑋) ∈ (𝐷 βˆ– { 1 }) ↔ ((βˆ— ∘ 𝑋) ∈ 𝐷 ∧ (βˆ— ∘ 𝑋) β‰  1 ))
11098, 108, 109sylanbrc 584 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (βˆ— ∘ 𝑋) ∈ (𝐷 βˆ– { 1 }))
111 nnuz 12861 . . . . . . . . . . . . . . . . . . . . 21 β„• = (β„€β‰₯β€˜1)
112 1zzd 12589 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 1 ∈ β„€)
113 2fveq3 6893 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = π‘š β†’ (π‘‹β€˜(πΏβ€˜π‘›)) = (π‘‹β€˜(πΏβ€˜π‘š)))
114 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = π‘š β†’ 𝑛 = π‘š)
115113, 114oveq12d 7422 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = π‘š β†’ ((π‘‹β€˜(πΏβ€˜π‘›)) / 𝑛) = ((π‘‹β€˜(πΏβ€˜π‘š)) / π‘š))
116115fveq2d 6892 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = π‘š β†’ (βˆ—β€˜((π‘‹β€˜(πΏβ€˜π‘›)) / 𝑛)) = (βˆ—β€˜((π‘‹β€˜(πΏβ€˜π‘š)) / π‘š)))
117 eqid 2733 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ β„• ↦ (βˆ—β€˜((π‘‹β€˜(πΏβ€˜π‘›)) / 𝑛))) = (𝑛 ∈ β„• ↦ (βˆ—β€˜((π‘‹β€˜(πΏβ€˜π‘›)) / 𝑛)))
118 fvex 6901 . . . . . . . . . . . . . . . . . . . . . . . 24 (βˆ—β€˜((π‘‹β€˜(πΏβ€˜π‘š)) / π‘š)) ∈ V
119116, 117, 118fvmpt 6994 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘š ∈ β„• β†’ ((𝑛 ∈ β„• ↦ (βˆ—β€˜((π‘‹β€˜(πΏβ€˜π‘›)) / 𝑛)))β€˜π‘š) = (βˆ—β€˜((π‘‹β€˜(πΏβ€˜π‘š)) / π‘š)))
120119adantl 483 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘š ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ (βˆ—β€˜((π‘‹β€˜(πΏβ€˜π‘›)) / 𝑛)))β€˜π‘š) = (βˆ—β€˜((π‘‹β€˜(πΏβ€˜π‘š)) / π‘š)))
121 nnre 12215 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘š ∈ β„• β†’ π‘š ∈ ℝ)
122121adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ π‘š ∈ β„•) β†’ π‘š ∈ ℝ)
123122cjred 15169 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (βˆ—β€˜π‘š) = π‘š)
124123oveq2d 7420 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ π‘š ∈ β„•) β†’ ((βˆ—β€˜(π‘‹β€˜(πΏβ€˜π‘š))) / (βˆ—β€˜π‘š)) = ((βˆ—β€˜(π‘‹β€˜(πΏβ€˜π‘š))) / π‘š))
12510adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ π‘š ∈ β„•) β†’ 𝑋:(Baseβ€˜π‘)βŸΆβ„‚)
1262, 4, 17znzrhfo 21087 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ β„•0 β†’ 𝐿:℀–ontoβ†’(Baseβ€˜π‘))
12721, 126syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ 𝐿:℀–ontoβ†’(Baseβ€˜π‘))
128 fof 6802 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐿:℀–ontoβ†’(Baseβ€˜π‘) β†’ 𝐿:β„€βŸΆ(Baseβ€˜π‘))
129127, 128syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ 𝐿:β„€βŸΆ(Baseβ€˜π‘))
130 nnz 12575 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘š ∈ β„• β†’ π‘š ∈ β„€)
131 ffvelcdm 7079 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐿:β„€βŸΆ(Baseβ€˜π‘) ∧ π‘š ∈ β„€) β†’ (πΏβ€˜π‘š) ∈ (Baseβ€˜π‘))
132129, 130, 131syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (πΏβ€˜π‘š) ∈ (Baseβ€˜π‘))
133125, 132ffvelcdmd 7083 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (π‘‹β€˜(πΏβ€˜π‘š)) ∈ β„‚)
134 nncn 12216 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘š ∈ β„• β†’ π‘š ∈ β„‚)
135134adantl 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘š ∈ β„•) β†’ π‘š ∈ β„‚)
136 nnne0 12242 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘š ∈ β„• β†’ π‘š β‰  0)
137136adantl 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘š ∈ β„•) β†’ π‘š β‰  0)
138133, 135, 137cjdivd 15166 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (βˆ—β€˜((π‘‹β€˜(πΏβ€˜π‘š)) / π‘š)) = ((βˆ—β€˜(π‘‹β€˜(πΏβ€˜π‘š))) / (βˆ—β€˜π‘š)))
139 fvco3 6986 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑋:(Baseβ€˜π‘)βŸΆβ„‚ ∧ (πΏβ€˜π‘š) ∈ (Baseβ€˜π‘)) β†’ ((βˆ— ∘ 𝑋)β€˜(πΏβ€˜π‘š)) = (βˆ—β€˜(π‘‹β€˜(πΏβ€˜π‘š))))
140125, 132, 139syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘š ∈ β„•) β†’ ((βˆ— ∘ 𝑋)β€˜(πΏβ€˜π‘š)) = (βˆ—β€˜(π‘‹β€˜(πΏβ€˜π‘š))))
141140oveq1d 7419 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (((βˆ— ∘ 𝑋)β€˜(πΏβ€˜π‘š)) / π‘š) = ((βˆ—β€˜(π‘‹β€˜(πΏβ€˜π‘š))) / π‘š))
142124, 138, 1413eqtr4d 2783 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (βˆ—β€˜((π‘‹β€˜(πΏβ€˜π‘š)) / π‘š)) = (((βˆ— ∘ 𝑋)β€˜(πΏβ€˜π‘š)) / π‘š))
143120, 142eqtrd 2773 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘š ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ (βˆ—β€˜((π‘‹β€˜(πΏβ€˜π‘›)) / 𝑛)))β€˜π‘š) = (((βˆ— ∘ 𝑋)β€˜(πΏβ€˜π‘š)) / π‘š))
144133cjcld 15139 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (βˆ—β€˜(π‘‹β€˜(πΏβ€˜π‘š))) ∈ β„‚)
145144, 135, 137divcld 11986 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘š ∈ β„•) β†’ ((βˆ—β€˜(π‘‹β€˜(πΏβ€˜π‘š))) / π‘š) ∈ β„‚)
146141, 145eqeltrd 2834 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (((βˆ— ∘ 𝑋)β€˜(πΏβ€˜π‘š)) / π‘š) ∈ β„‚)
147 eqid 2733 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž)) = (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž))
1482, 17, 18, 1, 3, 19, 9, 100, 147dchrmusumlema 26976 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ βˆƒπ‘‘βˆƒπ‘ ∈ (0[,)+∞)(seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž))) ⇝ 𝑑 ∧ βˆ€π‘¦ ∈ (1[,)+∞)(absβ€˜((seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž)))β€˜(βŒŠβ€˜π‘¦)) βˆ’ 𝑑)) ≀ (𝑐 / 𝑦)))
149 simprrl 780 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž))) ⇝ 𝑑 ∧ βˆ€π‘¦ ∈ (1[,)+∞)(absβ€˜((seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž)))β€˜(βŒŠβ€˜π‘¦)) βˆ’ 𝑑)) ≀ (𝑐 / 𝑦)))) β†’ seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž))) ⇝ 𝑑)
1507adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž))) ⇝ 𝑑 ∧ βˆ€π‘¦ ∈ (1[,)+∞)(absβ€˜((seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž)))β€˜(βŒŠβ€˜π‘¦)) βˆ’ 𝑑)) ≀ (𝑐 / 𝑦)))) β†’ 𝑋 ∈ π‘Š)
15118adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((πœ‘ ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž))) ⇝ 𝑑 ∧ βˆ€π‘¦ ∈ (1[,)+∞)(absβ€˜((seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž)))β€˜(βŒŠβ€˜π‘¦)) βˆ’ 𝑑)) ≀ (𝑐 / 𝑦)))) β†’ 𝑁 ∈ β„•)
1529adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((πœ‘ ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž))) ⇝ 𝑑 ∧ βˆ€π‘¦ ∈ (1[,)+∞)(absβ€˜((seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž)))β€˜(βŒŠβ€˜π‘¦)) βˆ’ 𝑑)) ≀ (𝑐 / 𝑦)))) β†’ 𝑋 ∈ 𝐷)
153100adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((πœ‘ ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž))) ⇝ 𝑑 ∧ βˆ€π‘¦ ∈ (1[,)+∞)(absβ€˜((seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž)))β€˜(βŒŠβ€˜π‘¦)) βˆ’ 𝑑)) ≀ (𝑐 / 𝑦)))) β†’ 𝑋 β‰  1 )
154 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((πœ‘ ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž))) ⇝ 𝑑 ∧ βˆ€π‘¦ ∈ (1[,)+∞)(absβ€˜((seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž)))β€˜(βŒŠβ€˜π‘¦)) βˆ’ 𝑑)) ≀ (𝑐 / 𝑦)))) β†’ 𝑐 ∈ (0[,)+∞))
155 simprrr 781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((πœ‘ ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž))) ⇝ 𝑑 ∧ βˆ€π‘¦ ∈ (1[,)+∞)(absβ€˜((seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž)))β€˜(βŒŠβ€˜π‘¦)) βˆ’ 𝑑)) ≀ (𝑐 / 𝑦)))) β†’ βˆ€π‘¦ ∈ (1[,)+∞)(absβ€˜((seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž)))β€˜(βŒŠβ€˜π‘¦)) βˆ’ 𝑑)) ≀ (𝑐 / 𝑦))
1562, 17, 151, 1, 3, 19, 152, 153, 147, 154, 149, 155, 5dchrvmaeq0 26987 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž))) ⇝ 𝑑 ∧ βˆ€π‘¦ ∈ (1[,)+∞)(absβ€˜((seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž)))β€˜(βŒŠβ€˜π‘¦)) βˆ’ 𝑑)) ≀ (𝑐 / 𝑦)))) β†’ (𝑋 ∈ π‘Š ↔ 𝑑 = 0))
157150, 156mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž))) ⇝ 𝑑 ∧ βˆ€π‘¦ ∈ (1[,)+∞)(absβ€˜((seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž)))β€˜(βŒŠβ€˜π‘¦)) βˆ’ 𝑑)) ≀ (𝑐 / 𝑦)))) β†’ 𝑑 = 0)
158149, 157breqtrd 5173 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž))) ⇝ 𝑑 ∧ βˆ€π‘¦ ∈ (1[,)+∞)(absβ€˜((seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž)))β€˜(βŒŠβ€˜π‘¦)) βˆ’ 𝑑)) ≀ (𝑐 / 𝑦)))) β†’ seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž))) ⇝ 0)
159158rexlimdvaa 3157 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ (βˆƒπ‘ ∈ (0[,)+∞)(seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž))) ⇝ 𝑑 ∧ βˆ€π‘¦ ∈ (1[,)+∞)(absβ€˜((seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž)))β€˜(βŒŠβ€˜π‘¦)) βˆ’ 𝑑)) ≀ (𝑐 / 𝑦)) β†’ seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž))) ⇝ 0))
160159exlimdv 1937 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (βˆƒπ‘‘βˆƒπ‘ ∈ (0[,)+∞)(seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž))) ⇝ 𝑑 ∧ βˆ€π‘¦ ∈ (1[,)+∞)(absβ€˜((seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž)))β€˜(βŒŠβ€˜π‘¦)) βˆ’ 𝑑)) ≀ (𝑐 / 𝑦)) β†’ seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž))) ⇝ 0))
161148, 160mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž))) ⇝ 0)
162 seqex 13964 . . . . . . . . . . . . . . . . . . . . . . . 24 seq1( + , (𝑛 ∈ β„• ↦ (βˆ—β€˜((π‘‹β€˜(πΏβ€˜π‘›)) / 𝑛)))) ∈ V
163162a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ seq1( + , (𝑛 ∈ β„• ↦ (βˆ—β€˜((π‘‹β€˜(πΏβ€˜π‘›)) / 𝑛)))) ∈ V)
164 2fveq3 6893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (π‘Ž = π‘š β†’ (π‘‹β€˜(πΏβ€˜π‘Ž)) = (π‘‹β€˜(πΏβ€˜π‘š)))
165 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (π‘Ž = π‘š β†’ π‘Ž = π‘š)
166164, 165oveq12d 7422 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (π‘Ž = π‘š β†’ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž) = ((π‘‹β€˜(πΏβ€˜π‘š)) / π‘š))
167 ovex 7437 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((π‘‹β€˜(πΏβ€˜π‘š)) / π‘š) ∈ V
168166, 147, 167fvmpt 6994 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π‘š ∈ β„• β†’ ((π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž))β€˜π‘š) = ((π‘‹β€˜(πΏβ€˜π‘š)) / π‘š))
169168adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ π‘š ∈ β„•) β†’ ((π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž))β€˜π‘š) = ((π‘‹β€˜(πΏβ€˜π‘š)) / π‘š))
170133, 135, 137divcld 11986 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ π‘š ∈ β„•) β†’ ((π‘‹β€˜(πΏβ€˜π‘š)) / π‘š) ∈ β„‚)
171169, 170eqeltrd 2834 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ π‘š ∈ β„•) β†’ ((π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž))β€˜π‘š) ∈ β„‚)
172111, 112, 171serf 13992 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž))):β„•βŸΆβ„‚)
173172ffvelcdmda 7082 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž)))β€˜π‘˜) ∈ β„‚)
174 fzfid 13934 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1...π‘˜) ∈ Fin)
175 simpl 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ πœ‘)
176 elfznn 13526 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘š ∈ (1...π‘˜) β†’ π‘š ∈ β„•)
177175, 176, 170syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘š ∈ (1...π‘˜)) β†’ ((π‘‹β€˜(πΏβ€˜π‘š)) / π‘š) ∈ β„‚)
178174, 177fsumcj 15752 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (βˆ—β€˜Ξ£π‘š ∈ (1...π‘˜)((π‘‹β€˜(πΏβ€˜π‘š)) / π‘š)) = Ξ£π‘š ∈ (1...π‘˜)(βˆ—β€˜((π‘‹β€˜(πΏβ€˜π‘š)) / π‘š)))
179175, 176, 169syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘š ∈ (1...π‘˜)) β†’ ((π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž))β€˜π‘š) = ((π‘‹β€˜(πΏβ€˜π‘š)) / π‘š))
180 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ β„•)
181180, 111eleqtrdi 2844 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ (β„€β‰₯β€˜1))
182179, 181, 177fsumser 15672 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ Ξ£π‘š ∈ (1...π‘˜)((π‘‹β€˜(πΏβ€˜π‘š)) / π‘š) = (seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž)))β€˜π‘˜))
183182fveq2d 6892 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (βˆ—β€˜Ξ£π‘š ∈ (1...π‘˜)((π‘‹β€˜(πΏβ€˜π‘š)) / π‘š)) = (βˆ—β€˜(seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž)))β€˜π‘˜)))
184175, 176, 120syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘š ∈ (1...π‘˜)) β†’ ((𝑛 ∈ β„• ↦ (βˆ—β€˜((π‘‹β€˜(πΏβ€˜π‘›)) / 𝑛)))β€˜π‘š) = (βˆ—β€˜((π‘‹β€˜(πΏβ€˜π‘š)) / π‘š)))
185170cjcld 15139 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (βˆ—β€˜((π‘‹β€˜(πΏβ€˜π‘š)) / π‘š)) ∈ β„‚)
186175, 176, 185syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘š ∈ (1...π‘˜)) β†’ (βˆ—β€˜((π‘‹β€˜(πΏβ€˜π‘š)) / π‘š)) ∈ β„‚)
187184, 181, 186fsumser 15672 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ Ξ£π‘š ∈ (1...π‘˜)(βˆ—β€˜((π‘‹β€˜(πΏβ€˜π‘š)) / π‘š)) = (seq1( + , (𝑛 ∈ β„• ↦ (βˆ—β€˜((π‘‹β€˜(πΏβ€˜π‘›)) / 𝑛))))β€˜π‘˜))
188178, 183, 1873eqtr3rd 2782 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , (𝑛 ∈ β„• ↦ (βˆ—β€˜((π‘‹β€˜(πΏβ€˜π‘›)) / 𝑛))))β€˜π‘˜) = (βˆ—β€˜(seq1( + , (π‘Ž ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘Ž)) / π‘Ž)))β€˜π‘˜)))
189111, 161, 163, 112, 173, 188climcj 15545 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ seq1( + , (𝑛 ∈ β„• ↦ (βˆ—β€˜((π‘‹β€˜(πΏβ€˜π‘›)) / 𝑛)))) ⇝ (βˆ—β€˜0))
190 cj0 15101 . . . . . . . . . . . . . . . . . . . . . 22 (βˆ—β€˜0) = 0
191189, 190breqtrdi 5188 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ seq1( + , (𝑛 ∈ β„• ↦ (βˆ—β€˜((π‘‹β€˜(πΏβ€˜π‘›)) / 𝑛)))) ⇝ 0)
192111, 112, 143, 146, 191isumclim 15699 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ Ξ£π‘š ∈ β„• (((βˆ— ∘ 𝑋)β€˜(πΏβ€˜π‘š)) / π‘š) = 0)
193 fveq1 6887 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = (βˆ— ∘ 𝑋) β†’ (π‘¦β€˜(πΏβ€˜π‘š)) = ((βˆ— ∘ 𝑋)β€˜(πΏβ€˜π‘š)))
194193oveq1d 7419 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (βˆ— ∘ 𝑋) β†’ ((π‘¦β€˜(πΏβ€˜π‘š)) / π‘š) = (((βˆ— ∘ 𝑋)β€˜(πΏβ€˜π‘š)) / π‘š))
195194sumeq2sdv 15646 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (βˆ— ∘ 𝑋) β†’ Ξ£π‘š ∈ β„• ((π‘¦β€˜(πΏβ€˜π‘š)) / π‘š) = Ξ£π‘š ∈ β„• (((βˆ— ∘ 𝑋)β€˜(πΏβ€˜π‘š)) / π‘š))
196195eqeq1d 2735 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (βˆ— ∘ 𝑋) β†’ (Ξ£π‘š ∈ β„• ((π‘¦β€˜(πΏβ€˜π‘š)) / π‘š) = 0 ↔ Ξ£π‘š ∈ β„• (((βˆ— ∘ 𝑋)β€˜(πΏβ€˜π‘š)) / π‘š) = 0))
197196, 5elrab2 3685 . . . . . . . . . . . . . . . . . . . 20 ((βˆ— ∘ 𝑋) ∈ π‘Š ↔ ((βˆ— ∘ 𝑋) ∈ (𝐷 βˆ– { 1 }) ∧ Ξ£π‘š ∈ β„• (((βˆ— ∘ 𝑋)β€˜(πΏβ€˜π‘š)) / π‘š) = 0))
198110, 192, 197sylanbrc 584 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (βˆ— ∘ 𝑋) ∈ π‘Š)
199198ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ (βˆ— ∘ 𝑋) ∈ π‘Š)
2007ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ 𝑋 ∈ π‘Š)
201 simplr 768 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ (βˆ— ∘ 𝑋) β‰  𝑋)
20289, 199, 200, 201nehash2 14431 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ 2 ≀ (β™―β€˜π‘Š))
203 suble0 11724 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℝ ∧ (β™―β€˜π‘Š) ∈ ℝ) β†’ ((2 βˆ’ (β™―β€˜π‘Š)) ≀ 0 ↔ 2 ≀ (β™―β€˜π‘Š)))
20477, 79, 203sylancr 588 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ ((2 βˆ’ (β™―β€˜π‘Š)) ≀ 0 ↔ 2 ≀ (β™―β€˜π‘Š)))
205202, 204mpbird 257 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ (2 βˆ’ (β™―β€˜π‘Š)) ≀ 0)
20680, 75, 72, 88, 205lemul2ad 12150 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ ((logβ€˜π‘₯) Β· (2 βˆ’ (β™―β€˜π‘Š))) ≀ ((logβ€˜π‘₯) Β· 0))
207 df-2 12271 . . . . . . . . . . . . . . . . . . 19 2 = (1 + 1)
208207oveq1i 7414 . . . . . . . . . . . . . . . . . 18 (2 βˆ’ (β™―β€˜π‘Š)) = ((1 + 1) βˆ’ (β™―β€˜π‘Š))
209 1cnd 11205 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ 1 ∈ β„‚)
21079recnd 11238 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ (β™―β€˜π‘Š) ∈ β„‚)
211209, 209, 210addsubassd 11587 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ ((1 + 1) βˆ’ (β™―β€˜π‘Š)) = (1 + (1 βˆ’ (β™―β€˜π‘Š))))
212208, 211eqtrid 2785 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ (2 βˆ’ (β™―β€˜π‘Š)) = (1 + (1 βˆ’ (β™―β€˜π‘Š))))
213212oveq2d 7420 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ ((logβ€˜π‘₯) Β· (2 βˆ’ (β™―β€˜π‘Š))) = ((logβ€˜π‘₯) Β· (1 + (1 βˆ’ (β™―β€˜π‘Š)))))
21471adantrr 716 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ (logβ€˜π‘₯) ∈ β„‚)
21564ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ (1 βˆ’ (β™―β€˜π‘Š)) ∈ ℝ)
216215recnd 11238 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ (1 βˆ’ (β™―β€˜π‘Š)) ∈ β„‚)
217214, 209, 216adddid 11234 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ ((logβ€˜π‘₯) Β· (1 + (1 βˆ’ (β™―β€˜π‘Š)))) = (((logβ€˜π‘₯) Β· 1) + ((logβ€˜π‘₯) Β· (1 βˆ’ (β™―β€˜π‘Š)))))
218214mulridd 11227 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ ((logβ€˜π‘₯) Β· 1) = (logβ€˜π‘₯))
219218oveq1d 7419 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ (((logβ€˜π‘₯) Β· 1) + ((logβ€˜π‘₯) Β· (1 βˆ’ (β™―β€˜π‘Š)))) = ((logβ€˜π‘₯) + ((logβ€˜π‘₯) Β· (1 βˆ’ (β™―β€˜π‘Š)))))
220213, 217, 2193eqtrd 2777 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ ((logβ€˜π‘₯) Β· (2 βˆ’ (β™―β€˜π‘Š))) = ((logβ€˜π‘₯) + ((logβ€˜π‘₯) Β· (1 βˆ’ (β™―β€˜π‘Š)))))
221214mul01d 11409 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ ((logβ€˜π‘₯) Β· 0) = 0)
222206, 220, 2213brtr3d 5178 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ ((logβ€˜π‘₯) + ((logβ€˜π‘₯) Β· (1 βˆ’ (β™―β€˜π‘Š)))) ≀ 0)
22333nnred 12223 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (Ο•β€˜π‘) ∈ ℝ)
224223ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ (Ο•β€˜π‘) ∈ ℝ)
22549ad2ant2r 746 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ Σ𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))((Ξ›β€˜π‘›) / 𝑛) ∈ ℝ)
22634ad2antrr 725 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ (Ο•β€˜π‘) ∈ β„•0)
227226nn0ge0d 12531 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ 0 ≀ (Ο•β€˜π‘))
22844, 45syl 17 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))) β†’ (Ξ›β€˜π‘›) ∈ ℝ)
229 vmage0 26605 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ β„• β†’ 0 ≀ (Ξ›β€˜π‘›))
23044, 229syl 17 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))) β†’ 0 ≀ (Ξ›β€˜π‘›))
23144nnred 12223 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))) β†’ 𝑛 ∈ ℝ)
23244nngt0d 12257 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))) β†’ 0 < 𝑛)
233 divge0 12079 . . . . . . . . . . . . . . . . . 18 ((((Ξ›β€˜π‘›) ∈ ℝ ∧ 0 ≀ (Ξ›β€˜π‘›)) ∧ (𝑛 ∈ ℝ ∧ 0 < 𝑛)) β†’ 0 ≀ ((Ξ›β€˜π‘›) / 𝑛))
234228, 230, 231, 232, 233syl22anc 838 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘₯ ∈ ℝ+) ∧ 𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))) β†’ 0 ≀ ((Ξ›β€˜π‘›) / 𝑛))
23540, 48, 234fsumge0 15737 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ 0 ≀ Σ𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))((Ξ›β€˜π‘›) / 𝑛))
236235ad2ant2r 746 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ 0 ≀ Σ𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))((Ξ›β€˜π‘›) / 𝑛))
237224, 225, 227, 236mulge0d 11787 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ 0 ≀ ((Ο•β€˜π‘) Β· Σ𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))((Ξ›β€˜π‘›) / 𝑛)))
23874, 75, 76, 222, 237letrd 11367 . . . . . . . . . . . . 13 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ ((logβ€˜π‘₯) + ((logβ€˜π‘₯) Β· (1 βˆ’ (β™―β€˜π‘Š)))) ≀ ((Ο•β€˜π‘) Β· Σ𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))((Ξ›β€˜π‘›) / 𝑛)))
239 leaddsub 11686 . . . . . . . . . . . . . 14 (((logβ€˜π‘₯) ∈ ℝ ∧ ((logβ€˜π‘₯) Β· (1 βˆ’ (β™―β€˜π‘Š))) ∈ ℝ ∧ ((Ο•β€˜π‘) Β· Σ𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))((Ξ›β€˜π‘›) / 𝑛)) ∈ ℝ) β†’ (((logβ€˜π‘₯) + ((logβ€˜π‘₯) Β· (1 βˆ’ (β™―β€˜π‘Š)))) ≀ ((Ο•β€˜π‘) Β· Σ𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))((Ξ›β€˜π‘›) / 𝑛)) ↔ (logβ€˜π‘₯) ≀ (((Ο•β€˜π‘) Β· Σ𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))((Ξ›β€˜π‘›) / 𝑛)) βˆ’ ((logβ€˜π‘₯) Β· (1 βˆ’ (β™―β€˜π‘Š))))))
24072, 73, 76, 239syl3anc 1372 . . . . . . . . . . . . 13 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ (((logβ€˜π‘₯) + ((logβ€˜π‘₯) Β· (1 βˆ’ (β™―β€˜π‘Š)))) ≀ ((Ο•β€˜π‘) Β· Σ𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))((Ξ›β€˜π‘›) / 𝑛)) ↔ (logβ€˜π‘₯) ≀ (((Ο•β€˜π‘) Β· Σ𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))((Ξ›β€˜π‘›) / 𝑛)) βˆ’ ((logβ€˜π‘₯) Β· (1 βˆ’ (β™―β€˜π‘Š))))))
241238, 240mpbid 231 . . . . . . . . . . . 12 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ (logβ€˜π‘₯) ≀ (((Ο•β€˜π‘) Β· Σ𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))((Ξ›β€˜π‘›) / 𝑛)) βˆ’ ((logβ€˜π‘₯) Β· (1 βˆ’ (β™―β€˜π‘Š)))))
24272, 88absidd 15365 . . . . . . . . . . . 12 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ (absβ€˜(logβ€˜π‘₯)) = (logβ€˜π‘₯))
24367ad2ant2r 746 . . . . . . . . . . . . 13 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ (((Ο•β€˜π‘) Β· Σ𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))((Ξ›β€˜π‘›) / 𝑛)) βˆ’ ((logβ€˜π‘₯) Β· (1 βˆ’ (β™―β€˜π‘Š)))) ∈ ℝ)
24475, 72, 243, 88, 241letrd 11367 . . . . . . . . . . . . 13 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ 0 ≀ (((Ο•β€˜π‘) Β· Σ𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))((Ξ›β€˜π‘›) / 𝑛)) βˆ’ ((logβ€˜π‘₯) Β· (1 βˆ’ (β™―β€˜π‘Š)))))
245243, 244absidd 15365 . . . . . . . . . . . 12 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ (absβ€˜(((Ο•β€˜π‘) Β· Σ𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))((Ξ›β€˜π‘›) / 𝑛)) βˆ’ ((logβ€˜π‘₯) Β· (1 βˆ’ (β™―β€˜π‘Š))))) = (((Ο•β€˜π‘) Β· Σ𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))((Ξ›β€˜π‘›) / 𝑛)) βˆ’ ((logβ€˜π‘₯) Β· (1 βˆ’ (β™―β€˜π‘Š)))))
246241, 242, 2453brtr4d 5179 . . . . . . . . . . 11 (((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) ∧ (π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯)) β†’ (absβ€˜(logβ€˜π‘₯)) ≀ (absβ€˜(((Ο•β€˜π‘) Β· Σ𝑛 ∈ ((1...(βŒŠβ€˜π‘₯)) ∩ (◑𝐿 β€œ {(1rβ€˜π‘)}))((Ξ›β€˜π‘›) / 𝑛)) βˆ’ ((logβ€˜π‘₯) Β· (1 βˆ’ (β™―β€˜π‘Š))))))
24716, 32, 69, 71, 246o1le 15595 . . . . . . . . . 10 ((πœ‘ ∧ (βˆ— ∘ 𝑋) β‰  𝑋) β†’ (π‘₯ ∈ ℝ+ ↦ (logβ€˜π‘₯)) ∈ 𝑂(1))
248247ex 414 . . . . . . . . 9 (πœ‘ β†’ ((βˆ— ∘ 𝑋) β‰  𝑋 β†’ (π‘₯ ∈ ℝ+ ↦ (logβ€˜π‘₯)) ∈ 𝑂(1)))
249248necon1bd 2959 . . . . . . . 8 (πœ‘ β†’ (Β¬ (π‘₯ ∈ ℝ+ ↦ (logβ€˜π‘₯)) ∈ 𝑂(1) β†’ (βˆ— ∘ 𝑋) = 𝑋))
25015, 249mpi 20 . . . . . . 7 (πœ‘ β†’ (βˆ— ∘ 𝑋) = 𝑋)
251250adantr 482 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘)) β†’ (βˆ— ∘ 𝑋) = 𝑋)
252251fveq1d 6890 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘)) β†’ ((βˆ— ∘ 𝑋)β€˜π‘₯) = (π‘‹β€˜π‘₯))
25314, 252eqtr3d 2775 . . . 4 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘)) β†’ (βˆ—β€˜(π‘‹β€˜π‘₯)) = (π‘‹β€˜π‘₯))
25412, 253cjrebd 15145 . . 3 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘)) β†’ (π‘‹β€˜π‘₯) ∈ ℝ)
255254ralrimiva 3147 . 2 (πœ‘ β†’ βˆ€π‘₯ ∈ (Baseβ€˜π‘)(π‘‹β€˜π‘₯) ∈ ℝ)
256 ffnfv 7113 . 2 (𝑋:(Baseβ€˜π‘)βŸΆβ„ ↔ (𝑋 Fn (Baseβ€˜π‘) ∧ βˆ€π‘₯ ∈ (Baseβ€˜π‘)(π‘‹β€˜π‘₯) ∈ ℝ))
25711, 255, 256sylanbrc 584 1 (πœ‘ β†’ 𝑋:(Baseβ€˜π‘)βŸΆβ„)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  {crab 3433  Vcvv 3475   βˆ– cdif 3944   ∩ cin 3946   βŠ† wss 3947  {csn 4627   class class class wbr 5147   ↦ cmpt 5230  β—‘ccnv 5674   β€œ cima 5678   ∘ ccom 5679   Fn wfn 6535  βŸΆwf 6536  β€“ontoβ†’wfo 6538  β€˜cfv 6540  (class class class)co 7404  Fincfn 8935  β„‚cc 11104  β„cr 11105  0cc0 11106  1c1 11107   + caddc 11109   Β· cmul 11111  +∞cpnf 11241   < clt 11244   ≀ cle 11245   βˆ’ cmin 11440   / cdiv 11867  β„•cn 12208  2c2 12263  β„•0cn0 12468  β„€cz 12554  β„€β‰₯cuz 12818  β„+crp 12970  [,)cico 13322  ...cfz 13480  βŒŠcfl 13751  seqcseq 13962  β™―chash 14286  βˆ—ccj 15039  abscabs 15177   ⇝ cli 15424  π‘‚(1)co1 15426  Ξ£csu 15628  Ο•cphi 16693  Basecbs 17140  0gc0g 17381  Grpcgrp 18815  invgcminusg 18816  Abelcabl 19642  1rcur 19996  Ringcrg 20047  CRingccrg 20048  Unitcui 20158  β„€RHomczrh 21033  β„€/nβ„€czn 21036  logclog 26045  Ξ›cvma 26576  DChrcdchr 26715
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 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185  ax-mulf 11186
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 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-disj 5113  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-of 7665  df-rpss 7708  df-om 7851  df-1st 7970  df-2nd 7971  df-supp 8142  df-tpos 8206  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-oadd 8465  df-omul 8466  df-er 8699  df-ec 8701  df-qs 8705  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-fi 9402  df-sup 9433  df-inf 9434  df-oi 9501  df-dju 9892  df-card 9930  df-acn 9933  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-xnn0 12541  df-z 12555  df-dec 12674  df-uz 12819  df-q 12929  df-rp 12971  df-xneg 13088  df-xadd 13089  df-xmul 13090  df-ioo 13324  df-ioc 13325  df-ico 13326  df-icc 13327  df-fz 13481  df-fzo 13624  df-fl 13753  df-mod 13831  df-seq 13963  df-exp 14024  df-fac 14230  df-bc 14259  df-hash 14287  df-word 14461  df-concat 14517  df-s1 14542  df-shft 15010  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-limsup 15411  df-clim 15428  df-rlim 15429  df-o1 15430  df-lo1 15431  df-sum 15629  df-ef 16007  df-e 16008  df-sin 16009  df-cos 16010  df-tan 16011  df-pi 16012  df-dvds 16194  df-gcd 16432  df-prm 16605  df-phi 16695  df-pc 16766  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-plusg 17206  df-mulr 17207  df-starv 17208  df-sca 17209  df-vsca 17210  df-ip 17211  df-tset 17212  df-ple 17213  df-ds 17215  df-unif 17216  df-hom 17217  df-cco 17218  df-rest 17364  df-topn 17365  df-0g 17383  df-gsum 17384  df-topgen 17385  df-pt 17386  df-prds 17389  df-xrs 17444  df-qtop 17449  df-imas 17450  df-qus 17451  df-xps 17452  df-mre 17526  df-mrc 17527  df-acs 17529  df-mgm 18557  df-sgrp 18606  df-mnd 18622  df-mhm 18667  df-submnd 18668  df-grp 18818  df-minusg 18819  df-sbg 18820  df-mulg 18945  df-subg 18997  df-nsg 18998  df-eqg 18999  df-ghm 19084  df-gim 19127  df-ga 19148  df-cntz 19175  df-oppg 19203  df-od 19389  df-gex 19390  df-pgp 19391  df-lsm 19497  df-pj1 19498  df-cmn 19643  df-abl 19644  df-cyg 19738  df-dprd 19857  df-dpj 19858  df-mgp 19980  df-ur 19997  df-ring 20049  df-cring 20050  df-oppr 20139  df-dvdsr 20160  df-unit 20161  df-invr 20191  df-dvr 20204  df-rnghom 20240  df-drng 20306  df-subrg 20349  df-lmod 20461  df-lss 20531  df-lsp 20571  df-sra 20773  df-rgmod 20774  df-lidl 20775  df-rsp 20776  df-2idl 20844  df-psmet 20921  df-xmet 20922  df-met 20923  df-bl 20924  df-mopn 20925  df-fbas 20926  df-fg 20927  df-cnfld 20930  df-zring 21003  df-zrh 21037  df-zn 21040  df-top 22378  df-topon 22395  df-topsp 22417  df-bases 22431  df-cld 22505  df-ntr 22506  df-cls 22507  df-nei 22584  df-lp 22622  df-perf 22623  df-cn 22713  df-cnp 22714  df-haus 22801  df-cmp 22873  df-tx 23048  df-hmeo 23241  df-fil 23332  df-fm 23424  df-flim 23425  df-flf 23426  df-xms 23808  df-ms 23809  df-tms 23810  df-cncf 24376  df-0p 25169  df-limc 25365  df-dv 25366  df-ply 25684  df-idp 25685  df-coe 25686  df-dgr 25687  df-quot 25786  df-ulm 25871  df-log 26047  df-cxp 26048  df-atan 26352  df-em 26477  df-cht 26581  df-vma 26582  df-chp 26583  df-ppi 26584  df-mu 26585  df-dchr 26716
This theorem is referenced by:  dchrisum0  27003
  Copyright terms: Public domain W3C validator