Metamath Proof Explorer


Theorem dchrisum0re

Description: Suppose X is a non-principal Dirichlet character with sum_ n e. NN , X ( n ) / n = 0 . Then X is a real character. Part of Lemma 9.4.4 of Shapiro, p. 382. (Contributed by Mario Carneiro, 5-May-2016)

Ref Expression
Hypotheses 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 dchrisum0re ( 𝜑𝑋 : ( Base ‘ 𝑍 ) ⟶ ℝ )

Proof

Step Hyp Ref Expression
1 rpvmasum.z 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2 rpvmasum.l 𝐿 = ( ℤRHom ‘ 𝑍 )
3 rpvmasum.a ( 𝜑𝑁 ∈ ℕ )
4 rpvmasum2.g 𝐺 = ( DChr ‘ 𝑁 )
5 rpvmasum2.d 𝐷 = ( Base ‘ 𝐺 )
6 rpvmasum2.1 1 = ( 0g𝐺 )
7 rpvmasum2.w 𝑊 = { 𝑦 ∈ ( 𝐷 ∖ { 1 } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) = 0 }
8 dchrisum0.b ( 𝜑𝑋𝑊 )
9 eqid ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
10 7 ssrab3 𝑊 ⊆ ( 𝐷 ∖ { 1 } )
11 10 8 sselid ( 𝜑𝑋 ∈ ( 𝐷 ∖ { 1 } ) )
12 11 eldifad ( 𝜑𝑋𝐷 )
13 4 1 5 9 12 dchrf ( 𝜑𝑋 : ( Base ‘ 𝑍 ) ⟶ ℂ )
14 13 ffnd ( 𝜑𝑋 Fn ( Base ‘ 𝑍 ) )
15 13 ffvelrnda ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( 𝑋𝑥 ) ∈ ℂ )
16 fvco3 ( ( 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℂ ∧ 𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( ( ∗ ∘ 𝑋 ) ‘ 𝑥 ) = ( ∗ ‘ ( 𝑋𝑥 ) ) )
17 13 16 sylan ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( ( ∗ ∘ 𝑋 ) ‘ 𝑥 ) = ( ∗ ‘ ( 𝑋𝑥 ) ) )
18 logno1 ¬ ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1)
19 1red ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) → 1 ∈ ℝ )
20 eqid ( Unit ‘ 𝑍 ) = ( Unit ‘ 𝑍 )
21 3 nnnn0d ( 𝜑𝑁 ∈ ℕ0 )
22 1 zncrng ( 𝑁 ∈ ℕ0𝑍 ∈ CRing )
23 21 22 syl ( 𝜑𝑍 ∈ CRing )
24 crngring ( 𝑍 ∈ CRing → 𝑍 ∈ Ring )
25 23 24 syl ( 𝜑𝑍 ∈ Ring )
26 eqid ( 1r𝑍 ) = ( 1r𝑍 )
27 20 26 1unit ( 𝑍 ∈ Ring → ( 1r𝑍 ) ∈ ( Unit ‘ 𝑍 ) )
28 25 27 syl ( 𝜑 → ( 1r𝑍 ) ∈ ( Unit ‘ 𝑍 ) )
29 eqid ( 𝐿 “ { ( 1r𝑍 ) } ) = ( 𝐿 “ { ( 1r𝑍 ) } )
30 eqidd ( ( 𝜑𝑓𝑊 ) → ( 1r𝑍 ) = ( 1r𝑍 ) )
31 1 2 3 4 5 6 7 20 28 29 30 rpvmasum2 ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ) ∈ 𝑂(1) )
32 31 adantr ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ) ∈ 𝑂(1) )
33 3 phicld ( 𝜑 → ( ϕ ‘ 𝑁 ) ∈ ℕ )
34 33 nnnn0d ( 𝜑 → ( ϕ ‘ 𝑁 ) ∈ ℕ0 )
35 34 adantr ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ϕ ‘ 𝑁 ) ∈ ℕ0 )
36 35 nn0red ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ϕ ‘ 𝑁 ) ∈ ℝ )
37 fzfid ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
38 inss1 ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑥 ) )
39 ssfi ( ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ∧ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ∈ Fin )
40 37 38 39 sylancl ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ∈ Fin )
41 elinel1 ( 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) → 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
42 elfznn ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
43 42 adantl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
44 41 43 sylan2 ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ) → 𝑛 ∈ ℕ )
45 vmacl ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
46 nndivre ( ( ( Λ ‘ 𝑛 ) ∈ ℝ ∧ 𝑛 ∈ ℕ ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
47 45 46 mpancom ( 𝑛 ∈ ℕ → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
48 44 47 syl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
49 40 48 fsumrecl ( ( 𝜑𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
50 36 49 remulcld ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℝ )
51 relogcl ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℝ )
52 51 adantl ( ( 𝜑𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℝ )
53 1re 1 ∈ ℝ
54 4 5 dchrfi ( 𝑁 ∈ ℕ → 𝐷 ∈ Fin )
55 3 54 syl ( 𝜑𝐷 ∈ Fin )
56 difss ( 𝐷 ∖ { 1 } ) ⊆ 𝐷
57 10 56 sstri 𝑊𝐷
58 ssfi ( ( 𝐷 ∈ Fin ∧ 𝑊𝐷 ) → 𝑊 ∈ Fin )
59 55 57 58 sylancl ( 𝜑𝑊 ∈ Fin )
60 hashcl ( 𝑊 ∈ Fin → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
61 59 60 syl ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
62 61 nn0red ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℝ )
63 resubcl ( ( 1 ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ ) → ( 1 − ( ♯ ‘ 𝑊 ) ) ∈ ℝ )
64 53 62 63 sylancr ( 𝜑 → ( 1 − ( ♯ ‘ 𝑊 ) ) ∈ ℝ )
65 64 adantr ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 1 − ( ♯ ‘ 𝑊 ) ) ∈ ℝ )
66 52 65 remulcld ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ∈ ℝ )
67 50 66 resubcld ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ∈ ℝ )
68 67 recnd ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ∈ ℂ )
69 68 adantlr ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ∈ ℂ )
70 51 adantl ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℝ )
71 70 recnd ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℂ )
72 51 ad2antrl ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
73 66 ad2ant2r ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ∈ ℝ )
74 72 73 readdcld ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) + ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ∈ ℝ )
75 0red ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 0 ∈ ℝ )
76 50 ad2ant2r ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℝ )
77 2re 2 ∈ ℝ
78 77 a1i ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 2 ∈ ℝ )
79 62 ad2antrr ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℝ )
80 78 79 resubcld ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 2 − ( ♯ ‘ 𝑊 ) ) ∈ ℝ )
81 log1 ( log ‘ 1 ) = 0
82 simprr ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 1 ≤ 𝑥 )
83 1rp 1 ∈ ℝ+
84 simprl ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ+ )
85 logleb ( ( 1 ∈ ℝ+𝑥 ∈ ℝ+ ) → ( 1 ≤ 𝑥 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝑥 ) ) )
86 83 84 85 sylancr ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 1 ≤ 𝑥 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝑥 ) ) )
87 82 86 mpbid ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( log ‘ 1 ) ≤ ( log ‘ 𝑥 ) )
88 81 87 eqbrtrrid ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 0 ≤ ( log ‘ 𝑥 ) )
89 59 ad2antrr ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑊 ∈ Fin )
90 eqid ( invg𝐺 ) = ( invg𝐺 )
91 4 5 12 90 dchrinv ( 𝜑 → ( ( invg𝐺 ) ‘ 𝑋 ) = ( ∗ ∘ 𝑋 ) )
92 4 dchrabl ( 𝑁 ∈ ℕ → 𝐺 ∈ Abel )
93 3 92 syl ( 𝜑𝐺 ∈ Abel )
94 ablgrp ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
95 93 94 syl ( 𝜑𝐺 ∈ Grp )
96 5 90 grpinvcl ( ( 𝐺 ∈ Grp ∧ 𝑋𝐷 ) → ( ( invg𝐺 ) ‘ 𝑋 ) ∈ 𝐷 )
97 95 12 96 syl2anc ( 𝜑 → ( ( invg𝐺 ) ‘ 𝑋 ) ∈ 𝐷 )
98 91 97 eqeltrrd ( 𝜑 → ( ∗ ∘ 𝑋 ) ∈ 𝐷 )
99 eldifsni ( 𝑋 ∈ ( 𝐷 ∖ { 1 } ) → 𝑋1 )
100 11 99 syl ( 𝜑𝑋1 )
101 5 6 grpidcl ( 𝐺 ∈ Grp → 1𝐷 )
102 95 101 syl ( 𝜑1𝐷 )
103 5 90 95 12 102 grpinv11 ( 𝜑 → ( ( ( invg𝐺 ) ‘ 𝑋 ) = ( ( invg𝐺 ) ‘ 1 ) ↔ 𝑋 = 1 ) )
104 103 necon3bid ( 𝜑 → ( ( ( invg𝐺 ) ‘ 𝑋 ) ≠ ( ( invg𝐺 ) ‘ 1 ) ↔ 𝑋1 ) )
105 100 104 mpbird ( 𝜑 → ( ( invg𝐺 ) ‘ 𝑋 ) ≠ ( ( invg𝐺 ) ‘ 1 ) )
106 6 90 grpinvid ( 𝐺 ∈ Grp → ( ( invg𝐺 ) ‘ 1 ) = 1 )
107 95 106 syl ( 𝜑 → ( ( invg𝐺 ) ‘ 1 ) = 1 )
108 105 91 107 3netr3d ( 𝜑 → ( ∗ ∘ 𝑋 ) ≠ 1 )
109 eldifsn ( ( ∗ ∘ 𝑋 ) ∈ ( 𝐷 ∖ { 1 } ) ↔ ( ( ∗ ∘ 𝑋 ) ∈ 𝐷 ∧ ( ∗ ∘ 𝑋 ) ≠ 1 ) )
110 98 108 109 sylanbrc ( 𝜑 → ( ∗ ∘ 𝑋 ) ∈ ( 𝐷 ∖ { 1 } ) )
111 nnuz ℕ = ( ℤ ‘ 1 )
112 1zzd ( 𝜑 → 1 ∈ ℤ )
113 2fveq3 ( 𝑛 = 𝑚 → ( 𝑋 ‘ ( 𝐿𝑛 ) ) = ( 𝑋 ‘ ( 𝐿𝑚 ) ) )
114 id ( 𝑛 = 𝑚𝑛 = 𝑚 )
115 113 114 oveq12d ( 𝑛 = 𝑚 → ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) / 𝑛 ) = ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) )
116 115 fveq2d ( 𝑛 = 𝑚 → ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) / 𝑛 ) ) = ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) )
117 eqid ( 𝑛 ∈ ℕ ↦ ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) / 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) / 𝑛 ) ) )
118 fvex ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) ∈ V
119 116 117 118 fvmpt ( 𝑚 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) / 𝑛 ) ) ) ‘ 𝑚 ) = ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) )
120 119 adantl ( ( 𝜑𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) / 𝑛 ) ) ) ‘ 𝑚 ) = ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) )
121 nnre ( 𝑚 ∈ ℕ → 𝑚 ∈ ℝ )
122 121 adantl ( ( 𝜑𝑚 ∈ ℕ ) → 𝑚 ∈ ℝ )
123 122 cjred ( ( 𝜑𝑚 ∈ ℕ ) → ( ∗ ‘ 𝑚 ) = 𝑚 )
124 123 oveq2d ( ( 𝜑𝑚 ∈ ℕ ) → ( ( ∗ ‘ ( 𝑋 ‘ ( 𝐿𝑚 ) ) ) / ( ∗ ‘ 𝑚 ) ) = ( ( ∗ ‘ ( 𝑋 ‘ ( 𝐿𝑚 ) ) ) / 𝑚 ) )
125 13 adantr ( ( 𝜑𝑚 ∈ ℕ ) → 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℂ )
126 1 9 2 znzrhfo ( 𝑁 ∈ ℕ0𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) )
127 21 126 syl ( 𝜑𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) )
128 fof ( 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
129 127 128 syl ( 𝜑𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
130 nnz ( 𝑚 ∈ ℕ → 𝑚 ∈ ℤ )
131 ffvelrn ( ( 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) ∧ 𝑚 ∈ ℤ ) → ( 𝐿𝑚 ) ∈ ( Base ‘ 𝑍 ) )
132 129 130 131 syl2an ( ( 𝜑𝑚 ∈ ℕ ) → ( 𝐿𝑚 ) ∈ ( Base ‘ 𝑍 ) )
133 125 132 ffvelrnd ( ( 𝜑𝑚 ∈ ℕ ) → ( 𝑋 ‘ ( 𝐿𝑚 ) ) ∈ ℂ )
134 nncn ( 𝑚 ∈ ℕ → 𝑚 ∈ ℂ )
135 134 adantl ( ( 𝜑𝑚 ∈ ℕ ) → 𝑚 ∈ ℂ )
136 nnne0 ( 𝑚 ∈ ℕ → 𝑚 ≠ 0 )
137 136 adantl ( ( 𝜑𝑚 ∈ ℕ ) → 𝑚 ≠ 0 )
138 133 135 137 cjdivd ( ( 𝜑𝑚 ∈ ℕ ) → ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) = ( ( ∗ ‘ ( 𝑋 ‘ ( 𝐿𝑚 ) ) ) / ( ∗ ‘ 𝑚 ) ) )
139 fvco3 ( ( 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℂ ∧ ( 𝐿𝑚 ) ∈ ( Base ‘ 𝑍 ) ) → ( ( ∗ ∘ 𝑋 ) ‘ ( 𝐿𝑚 ) ) = ( ∗ ‘ ( 𝑋 ‘ ( 𝐿𝑚 ) ) ) )
140 125 132 139 syl2anc ( ( 𝜑𝑚 ∈ ℕ ) → ( ( ∗ ∘ 𝑋 ) ‘ ( 𝐿𝑚 ) ) = ( ∗ ‘ ( 𝑋 ‘ ( 𝐿𝑚 ) ) ) )
141 140 oveq1d ( ( 𝜑𝑚 ∈ ℕ ) → ( ( ( ∗ ∘ 𝑋 ) ‘ ( 𝐿𝑚 ) ) / 𝑚 ) = ( ( ∗ ‘ ( 𝑋 ‘ ( 𝐿𝑚 ) ) ) / 𝑚 ) )
142 124 138 141 3eqtr4d ( ( 𝜑𝑚 ∈ ℕ ) → ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) = ( ( ( ∗ ∘ 𝑋 ) ‘ ( 𝐿𝑚 ) ) / 𝑚 ) )
143 120 142 eqtrd ( ( 𝜑𝑚 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) / 𝑛 ) ) ) ‘ 𝑚 ) = ( ( ( ∗ ∘ 𝑋 ) ‘ ( 𝐿𝑚 ) ) / 𝑚 ) )
144 133 cjcld ( ( 𝜑𝑚 ∈ ℕ ) → ( ∗ ‘ ( 𝑋 ‘ ( 𝐿𝑚 ) ) ) ∈ ℂ )
145 144 135 137 divcld ( ( 𝜑𝑚 ∈ ℕ ) → ( ( ∗ ‘ ( 𝑋 ‘ ( 𝐿𝑚 ) ) ) / 𝑚 ) ∈ ℂ )
146 141 145 eqeltrd ( ( 𝜑𝑚 ∈ ℕ ) → ( ( ( ∗ ∘ 𝑋 ) ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ∈ ℂ )
147 eqid ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) )
148 1 2 3 4 5 6 12 100 147 dchrmusumlema ( 𝜑 → ∃ 𝑡𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) )
149 simprrl ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 )
150 8 adantr ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝑋𝑊 )
151 3 adantr ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝑁 ∈ ℕ )
152 12 adantr ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝑋𝐷 )
153 100 adantr ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝑋1 )
154 simprl ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝑐 ∈ ( 0 [,) +∞ ) )
155 simprrr ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) )
156 1 2 151 4 5 6 152 153 147 154 149 155 7 dchrvmaeq0 ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → ( 𝑋𝑊𝑡 = 0 ) )
157 150 156 mpbid ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝑡 = 0 )
158 149 157 breqtrd ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 0 )
159 158 rexlimdvaa ( 𝜑 → ( ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) → seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 0 ) )
160 159 exlimdv ( 𝜑 → ( ∃ 𝑡𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) → seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 0 ) )
161 148 160 mpd ( 𝜑 → seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 0 )
162 seqex seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) / 𝑛 ) ) ) ) ∈ V
163 162 a1i ( 𝜑 → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) / 𝑛 ) ) ) ) ∈ V )
164 2fveq3 ( 𝑎 = 𝑚 → ( 𝑋 ‘ ( 𝐿𝑎 ) ) = ( 𝑋 ‘ ( 𝐿𝑚 ) ) )
165 id ( 𝑎 = 𝑚𝑎 = 𝑚 )
166 164 165 oveq12d ( 𝑎 = 𝑚 → ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) = ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) )
167 ovex ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ∈ V
168 166 147 167 fvmpt ( 𝑚 ∈ ℕ → ( ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ‘ 𝑚 ) = ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) )
169 168 adantl ( ( 𝜑𝑚 ∈ ℕ ) → ( ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ‘ 𝑚 ) = ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) )
170 133 135 137 divcld ( ( 𝜑𝑚 ∈ ℕ ) → ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ∈ ℂ )
171 169 170 eqeltrd ( ( 𝜑𝑚 ∈ ℕ ) → ( ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ‘ 𝑚 ) ∈ ℂ )
172 111 112 171 serf ( 𝜑 → seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) : ℕ ⟶ ℂ )
173 172 ffvelrnda ( ( 𝜑𝑘 ∈ ℕ ) → ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ 𝑘 ) ∈ ℂ )
174 fzfid ( ( 𝜑𝑘 ∈ ℕ ) → ( 1 ... 𝑘 ) ∈ Fin )
175 simpl ( ( 𝜑𝑘 ∈ ℕ ) → 𝜑 )
176 elfznn ( 𝑚 ∈ ( 1 ... 𝑘 ) → 𝑚 ∈ ℕ )
177 175 176 170 syl2an ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑘 ) ) → ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ∈ ℂ )
178 174 177 fsumcj ( ( 𝜑𝑘 ∈ ℕ ) → ( ∗ ‘ Σ 𝑚 ∈ ( 1 ... 𝑘 ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) = Σ 𝑚 ∈ ( 1 ... 𝑘 ) ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) )
179 175 176 169 syl2an ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑘 ) ) → ( ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ‘ 𝑚 ) = ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) )
180 simpr ( ( 𝜑𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
181 180 111 eleqtrdi ( ( 𝜑𝑘 ∈ ℕ ) → 𝑘 ∈ ( ℤ ‘ 1 ) )
182 179 181 177 fsumser ( ( 𝜑𝑘 ∈ ℕ ) → Σ 𝑚 ∈ ( 1 ... 𝑘 ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) = ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ 𝑘 ) )
183 182 fveq2d ( ( 𝜑𝑘 ∈ ℕ ) → ( ∗ ‘ Σ 𝑚 ∈ ( 1 ... 𝑘 ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) = ( ∗ ‘ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ 𝑘 ) ) )
184 175 176 120 syl2an ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑘 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) / 𝑛 ) ) ) ‘ 𝑚 ) = ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) )
185 170 cjcld ( ( 𝜑𝑚 ∈ ℕ ) → ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) ∈ ℂ )
186 175 176 185 syl2an ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑘 ) ) → ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) ∈ ℂ )
187 184 181 186 fsumser ( ( 𝜑𝑘 ∈ ℕ ) → Σ 𝑚 ∈ ( 1 ... 𝑘 ) ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) / 𝑛 ) ) ) ) ‘ 𝑘 ) )
188 178 183 187 3eqtr3rd ( ( 𝜑𝑘 ∈ ℕ ) → ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) / 𝑛 ) ) ) ) ‘ 𝑘 ) = ( ∗ ‘ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ 𝑘 ) ) )
189 111 161 163 112 173 188 climcj ( 𝜑 → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) / 𝑛 ) ) ) ) ⇝ ( ∗ ‘ 0 ) )
190 cj0 ( ∗ ‘ 0 ) = 0
191 189 190 breqtrdi ( 𝜑 → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( ∗ ‘ ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) / 𝑛 ) ) ) ) ⇝ 0 )
192 111 112 143 146 191 isumclim ( 𝜑 → Σ 𝑚 ∈ ℕ ( ( ( ∗ ∘ 𝑋 ) ‘ ( 𝐿𝑚 ) ) / 𝑚 ) = 0 )
193 fveq1 ( 𝑦 = ( ∗ ∘ 𝑋 ) → ( 𝑦 ‘ ( 𝐿𝑚 ) ) = ( ( ∗ ∘ 𝑋 ) ‘ ( 𝐿𝑚 ) ) )
194 193 oveq1d ( 𝑦 = ( ∗ ∘ 𝑋 ) → ( ( 𝑦 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) = ( ( ( ∗ ∘ 𝑋 ) ‘ ( 𝐿𝑚 ) ) / 𝑚 ) )
195 194 sumeq2sdv ( 𝑦 = ( ∗ ∘ 𝑋 ) → Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) = Σ 𝑚 ∈ ℕ ( ( ( ∗ ∘ 𝑋 ) ‘ ( 𝐿𝑚 ) ) / 𝑚 ) )
196 195 eqeq1d ( 𝑦 = ( ∗ ∘ 𝑋 ) → ( Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) = 0 ↔ Σ 𝑚 ∈ ℕ ( ( ( ∗ ∘ 𝑋 ) ‘ ( 𝐿𝑚 ) ) / 𝑚 ) = 0 ) )
197 196 7 elrab2 ( ( ∗ ∘ 𝑋 ) ∈ 𝑊 ↔ ( ( ∗ ∘ 𝑋 ) ∈ ( 𝐷 ∖ { 1 } ) ∧ Σ 𝑚 ∈ ℕ ( ( ( ∗ ∘ 𝑋 ) ‘ ( 𝐿𝑚 ) ) / 𝑚 ) = 0 ) )
198 110 192 197 sylanbrc ( 𝜑 → ( ∗ ∘ 𝑋 ) ∈ 𝑊 )
199 198 ad2antrr ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ∗ ∘ 𝑋 ) ∈ 𝑊 )
200 8 ad2antrr ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑋𝑊 )
201 simplr ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ∗ ∘ 𝑋 ) ≠ 𝑋 )
202 89 199 200 201 nehash2 ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 2 ≤ ( ♯ ‘ 𝑊 ) )
203 suble0 ( ( 2 ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ ) → ( ( 2 − ( ♯ ‘ 𝑊 ) ) ≤ 0 ↔ 2 ≤ ( ♯ ‘ 𝑊 ) ) )
204 77 79 203 sylancr ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( 2 − ( ♯ ‘ 𝑊 ) ) ≤ 0 ↔ 2 ≤ ( ♯ ‘ 𝑊 ) ) )
205 202 204 mpbird ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 2 − ( ♯ ‘ 𝑊 ) ) ≤ 0 )
206 80 75 72 88 205 lemul2ad ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) · ( 2 − ( ♯ ‘ 𝑊 ) ) ) ≤ ( ( log ‘ 𝑥 ) · 0 ) )
207 df-2 2 = ( 1 + 1 )
208 207 oveq1i ( 2 − ( ♯ ‘ 𝑊 ) ) = ( ( 1 + 1 ) − ( ♯ ‘ 𝑊 ) )
209 1cnd ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 1 ∈ ℂ )
210 79 recnd ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℂ )
211 209 209 210 addsubassd ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( 1 + 1 ) − ( ♯ ‘ 𝑊 ) ) = ( 1 + ( 1 − ( ♯ ‘ 𝑊 ) ) ) )
212 208 211 syl5eq ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 2 − ( ♯ ‘ 𝑊 ) ) = ( 1 + ( 1 − ( ♯ ‘ 𝑊 ) ) ) )
213 212 oveq2d ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) · ( 2 − ( ♯ ‘ 𝑊 ) ) ) = ( ( log ‘ 𝑥 ) · ( 1 + ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) )
214 71 adantrr ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( log ‘ 𝑥 ) ∈ ℂ )
215 64 ad2antrr ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 1 − ( ♯ ‘ 𝑊 ) ) ∈ ℝ )
216 215 recnd ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 1 − ( ♯ ‘ 𝑊 ) ) ∈ ℂ )
217 214 209 216 adddid ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) · ( 1 + ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) = ( ( ( log ‘ 𝑥 ) · 1 ) + ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) )
218 214 mulid1d ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) · 1 ) = ( log ‘ 𝑥 ) )
219 218 oveq1d ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( log ‘ 𝑥 ) · 1 ) + ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) = ( ( log ‘ 𝑥 ) + ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) )
220 213 217 219 3eqtrd ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) · ( 2 − ( ♯ ‘ 𝑊 ) ) ) = ( ( log ‘ 𝑥 ) + ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) )
221 214 mul01d ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) · 0 ) = 0 )
222 206 220 221 3brtr3d ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) + ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ≤ 0 )
223 33 nnred ( 𝜑 → ( ϕ ‘ 𝑁 ) ∈ ℝ )
224 223 ad2antrr ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ϕ ‘ 𝑁 ) ∈ ℝ )
225 49 ad2ant2r ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
226 34 ad2antrr ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ϕ ‘ 𝑁 ) ∈ ℕ0 )
227 226 nn0ge0d ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 0 ≤ ( ϕ ‘ 𝑁 ) )
228 44 45 syl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
229 vmage0 ( 𝑛 ∈ ℕ → 0 ≤ ( Λ ‘ 𝑛 ) )
230 44 229 syl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ) → 0 ≤ ( Λ ‘ 𝑛 ) )
231 44 nnred ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ) → 𝑛 ∈ ℝ )
232 44 nngt0d ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ) → 0 < 𝑛 )
233 divge0 ( ( ( ( Λ ‘ 𝑛 ) ∈ ℝ ∧ 0 ≤ ( Λ ‘ 𝑛 ) ) ∧ ( 𝑛 ∈ ℝ ∧ 0 < 𝑛 ) ) → 0 ≤ ( ( Λ ‘ 𝑛 ) / 𝑛 ) )
234 228 230 231 232 233 syl22anc ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ) → 0 ≤ ( ( Λ ‘ 𝑛 ) / 𝑛 ) )
235 40 48 234 fsumge0 ( ( 𝜑𝑥 ∈ ℝ+ ) → 0 ≤ Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) )
236 235 ad2ant2r ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 0 ≤ Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) )
237 224 225 227 236 mulge0d ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 0 ≤ ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) )
238 74 75 76 222 237 letrd ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) + ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ≤ ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) )
239 leaddsub ( ( ( log ‘ 𝑥 ) ∈ ℝ ∧ ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ∈ ℝ ∧ ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℝ ) → ( ( ( log ‘ 𝑥 ) + ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ≤ ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ↔ ( log ‘ 𝑥 ) ≤ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ) )
240 72 73 76 239 syl3anc ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( log ‘ 𝑥 ) + ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ≤ ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ↔ ( log ‘ 𝑥 ) ≤ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ) )
241 238 240 mpbid ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( log ‘ 𝑥 ) ≤ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) )
242 72 88 absidd ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( log ‘ 𝑥 ) ) = ( log ‘ 𝑥 ) )
243 67 ad2ant2r ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ∈ ℝ )
244 75 72 243 88 241 letrd ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 0 ≤ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) )
245 243 244 absidd ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ) = ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) )
246 241 242 245 3brtr4d ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( log ‘ 𝑥 ) ) ≤ ( abs ‘ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝐿 “ { ( 1r𝑍 ) } ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ) )
247 19 32 69 71 246 o1le ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) → ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) )
248 247 ex ( 𝜑 → ( ( ∗ ∘ 𝑋 ) ≠ 𝑋 → ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) ) )
249 248 necon1bd ( 𝜑 → ( ¬ ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) → ( ∗ ∘ 𝑋 ) = 𝑋 ) )
250 18 249 mpi ( 𝜑 → ( ∗ ∘ 𝑋 ) = 𝑋 )
251 250 adantr ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( ∗ ∘ 𝑋 ) = 𝑋 )
252 251 fveq1d ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( ( ∗ ∘ 𝑋 ) ‘ 𝑥 ) = ( 𝑋𝑥 ) )
253 17 252 eqtr3d ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( ∗ ‘ ( 𝑋𝑥 ) ) = ( 𝑋𝑥 ) )
254 15 253 cjrebd ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( 𝑋𝑥 ) ∈ ℝ )
255 254 ralrimiva ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝑍 ) ( 𝑋𝑥 ) ∈ ℝ )
256 ffnfv ( 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℝ ↔ ( 𝑋 Fn ( Base ‘ 𝑍 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑍 ) ( 𝑋𝑥 ) ∈ ℝ ) )
257 14 255 256 sylanbrc ( 𝜑𝑋 : ( Base ‘ 𝑍 ) ⟶ ℝ )