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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 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		ffvelcdm	⊢ ( ( 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) ∧ 𝑚 ∈ ℤ ) → ( 𝐿 ‘ 𝑚 ) ∈ ( Base ‘ 𝑍 ) )
132	129 130 131	syl2an	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐿 ‘ 𝑚 ) ∈ ( Base ‘ 𝑍 ) )
133	125 132	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ∈ ℂ )
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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 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	eqtrid	⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 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	mulridd	⊢ ( ( ( 𝜑 ∧ ( ∗ ∘ 𝑋 ) ≠ 𝑋 ) ∧ ( 𝑥 ∈ ℝ+ ∧ 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 ‘ 𝑍 ) ⟶ ℝ )