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 sseldi ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐷 ∖ { 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 ‘ 𝑍 ) ⟶ ℝ )