Theorem ostth2

Description: - Lemma for ostth : regular case. (Contributed by Mario Carneiro, 10-Sep-2014)

	Ref	Expression
Hypotheses	qrng.q	⊢ 𝑄 = ( ℂfld ↾s ℚ )
	qabsabv.a	⊢ 𝐴 = ( AbsVal ‘ 𝑄 )
	padic.j	⊢ 𝐽 = ( 𝑞 ∈ ℙ ↦ ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑞 ↑ - ( 𝑞 pCnt 𝑥 ) ) ) ) )
	ostth.k	⊢ 𝐾 = ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , 1 ) )
	ostth.1	⊢ ( 𝜑 → 𝐹 ∈ 𝐴 )
	ostth2.2	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
	ostth2.3	⊢ ( 𝜑 → 1 < ( 𝐹 ‘ 𝑁 ) )
	ostth2.4	⊢ 𝑅 = ( ( log ‘ ( 𝐹 ‘ 𝑁 ) ) / ( log ‘ 𝑁 ) )
Assertion	ostth2	⊢ ( 𝜑 → ∃ 𝑎 ∈ ( 0 (,] 1 ) 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) )

Proof

Step	Hyp	Ref	Expression
1		qrng.q	⊢ 𝑄 = ( ℂfld ↾s ℚ )
2		qabsabv.a	⊢ 𝐴 = ( AbsVal ‘ 𝑄 )
3		padic.j	⊢ 𝐽 = ( 𝑞 ∈ ℙ ↦ ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑞 ↑ - ( 𝑞 pCnt 𝑥 ) ) ) ) )
4		ostth.k	⊢ 𝐾 = ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , 1 ) )
5		ostth.1	⊢ ( 𝜑 → 𝐹 ∈ 𝐴 )
6		ostth2.2	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
7		ostth2.3	⊢ ( 𝜑 → 1 < ( 𝐹 ‘ 𝑁 ) )
8		ostth2.4	⊢ 𝑅 = ( ( log ‘ ( 𝐹 ‘ 𝑁 ) ) / ( log ‘ 𝑁 ) )
9		eluz2b2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑁 ∈ ℕ ∧ 1 < 𝑁 ) )
10	6 9	sylib	⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ∧ 1 < 𝑁 ) )
11	10	simpld	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
12		nnq	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℚ )
13	11 12	syl	⊢ ( 𝜑 → 𝑁 ∈ ℚ )
14	1	qrngbas	⊢ ℚ = ( Base ‘ 𝑄 )
15	2 14	abvcl	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑁 ∈ ℚ ) → ( 𝐹 ‘ 𝑁 ) ∈ ℝ )
16	5 13 15	syl2anc	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ∈ ℝ )
17	16 7	rplogcld	⊢ ( 𝜑 → ( log ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ+ )
18	11	nnred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
19	10	simprd	⊢ ( 𝜑 → 1 < 𝑁 )
20	18 19	rplogcld	⊢ ( 𝜑 → ( log ‘ 𝑁 ) ∈ ℝ+ )
21	17 20	rpdivcld	⊢ ( 𝜑 → ( ( log ‘ ( 𝐹 ‘ 𝑁 ) ) / ( log ‘ 𝑁 ) ) ∈ ℝ+ )
22	8 21	eqeltrid	⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
23	22	rpred	⊢ ( 𝜑 → 𝑅 ∈ ℝ )
24	22	rpgt0d	⊢ ( 𝜑 → 0 < 𝑅 )
25	11	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
26	1 2	qabvle	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑁 ) ≤ 𝑁 )
27	5 25 26	syl2anc	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ≤ 𝑁 )
28	11	nnne0d	⊢ ( 𝜑 → 𝑁 ≠ 0 )
29	1	qrng0	⊢ 0 = ( 0g ‘ 𝑄 )
30	2 14 29	abvgt0	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑁 ∈ ℚ ∧ 𝑁 ≠ 0 ) → 0 < ( 𝐹 ‘ 𝑁 ) )
31	5 13 28 30	syl3anc	⊢ ( 𝜑 → 0 < ( 𝐹 ‘ 𝑁 ) )
32	16 31	elrpd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ∈ ℝ+ )
33	32	reeflogd	⊢ ( 𝜑 → ( exp ‘ ( log ‘ ( 𝐹 ‘ 𝑁 ) ) ) = ( 𝐹 ‘ 𝑁 ) )
34	11	nnrpd	⊢ ( 𝜑 → 𝑁 ∈ ℝ+ )
35	34	reeflogd	⊢ ( 𝜑 → ( exp ‘ ( log ‘ 𝑁 ) ) = 𝑁 )
36	27 33 35	3brtr4d	⊢ ( 𝜑 → ( exp ‘ ( log ‘ ( 𝐹 ‘ 𝑁 ) ) ) ≤ ( exp ‘ ( log ‘ 𝑁 ) ) )
37	17	rpred	⊢ ( 𝜑 → ( log ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ )
38	34	relogcld	⊢ ( 𝜑 → ( log ‘ 𝑁 ) ∈ ℝ )
39		efle	⊢ ( ( ( log ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ ∧ ( log ‘ 𝑁 ) ∈ ℝ ) → ( ( log ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( log ‘ 𝑁 ) ↔ ( exp ‘ ( log ‘ ( 𝐹 ‘ 𝑁 ) ) ) ≤ ( exp ‘ ( log ‘ 𝑁 ) ) ) )
40	37 38 39	syl2anc	⊢ ( 𝜑 → ( ( log ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( log ‘ 𝑁 ) ↔ ( exp ‘ ( log ‘ ( 𝐹 ‘ 𝑁 ) ) ) ≤ ( exp ‘ ( log ‘ 𝑁 ) ) ) )
41	36 40	mpbird	⊢ ( 𝜑 → ( log ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( log ‘ 𝑁 ) )
42	20	rpcnd	⊢ ( 𝜑 → ( log ‘ 𝑁 ) ∈ ℂ )
43	42	mulridd	⊢ ( 𝜑 → ( ( log ‘ 𝑁 ) · 1 ) = ( log ‘ 𝑁 ) )
44	41 43	breqtrrd	⊢ ( 𝜑 → ( log ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( ( log ‘ 𝑁 ) · 1 ) )
45		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
46	37 45 20	ledivmuld	⊢ ( 𝜑 → ( ( ( log ‘ ( 𝐹 ‘ 𝑁 ) ) / ( log ‘ 𝑁 ) ) ≤ 1 ↔ ( log ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( ( log ‘ 𝑁 ) · 1 ) ) )
47	44 46	mpbird	⊢ ( 𝜑 → ( ( log ‘ ( 𝐹 ‘ 𝑁 ) ) / ( log ‘ 𝑁 ) ) ≤ 1 )
48	8 47	eqbrtrid	⊢ ( 𝜑 → 𝑅 ≤ 1 )
49		0xr	⊢ 0 ∈ ℝ*
50		1re	⊢ 1 ∈ ℝ
51		elioc2	⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ ) → ( 𝑅 ∈ ( 0 (,] 1 ) ↔ ( 𝑅 ∈ ℝ ∧ 0 < 𝑅 ∧ 𝑅 ≤ 1 ) ) )
52	49 50 51	mp2an	⊢ ( 𝑅 ∈ ( 0 (,] 1 ) ↔ ( 𝑅 ∈ ℝ ∧ 0 < 𝑅 ∧ 𝑅 ≤ 1 ) )
53	23 24 48 52	syl3anbrc	⊢ ( 𝜑 → 𝑅 ∈ ( 0 (,] 1 ) )
54	1 2	qabsabv	⊢ ( abs ↾ ℚ ) ∈ 𝐴
55		fvres	⊢ ( 𝑦 ∈ ℚ → ( ( abs ↾ ℚ ) ‘ 𝑦 ) = ( abs ‘ 𝑦 ) )
56	55	oveq1d	⊢ ( 𝑦 ∈ ℚ → ( ( ( abs ↾ ℚ ) ‘ 𝑦 ) ↑𝑐 𝑅 ) = ( ( abs ‘ 𝑦 ) ↑𝑐 𝑅 ) )
57	56	mpteq2ia	⊢ ( 𝑦 ∈ ℚ ↦ ( ( ( abs ↾ ℚ ) ‘ 𝑦 ) ↑𝑐 𝑅 ) ) = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑅 ) )
58	57	eqcomi	⊢ ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑅 ) ) = ( 𝑦 ∈ ℚ ↦ ( ( ( abs ↾ ℚ ) ‘ 𝑦 ) ↑𝑐 𝑅 ) )
59	2 14 58	abvcxp	⊢ ( ( ( abs ↾ ℚ ) ∈ 𝐴 ∧ 𝑅 ∈ ( 0 (,] 1 ) ) → ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ∈ 𝐴 )
60	54 53 59	sylancr	⊢ ( 𝜑 → ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ∈ 𝐴 )
61		eluzelz	⊢ ( 𝑧 ∈ ( ℤ≥ ‘ 2 ) → 𝑧 ∈ ℤ )
62		zq	⊢ ( 𝑧 ∈ ℤ → 𝑧 ∈ ℚ )
63		fveq2	⊢ ( 𝑦 = 𝑧 → ( abs ‘ 𝑦 ) = ( abs ‘ 𝑧 ) )
64	63	oveq1d	⊢ ( 𝑦 = 𝑧 → ( ( abs ‘ 𝑦 ) ↑𝑐 𝑅 ) = ( ( abs ‘ 𝑧 ) ↑𝑐 𝑅 ) )
65		eqid	⊢ ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑅 ) ) = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑅 ) )
66		ovex	⊢ ( ( abs ‘ 𝑧 ) ↑𝑐 𝑅 ) ∈ V
67	64 65 66	fvmpt	⊢ ( 𝑧 ∈ ℚ → ( ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ‘ 𝑧 ) = ( ( abs ‘ 𝑧 ) ↑𝑐 𝑅 ) )
68	61 62 67	3syl	⊢ ( 𝑧 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ‘ 𝑧 ) = ( ( abs ‘ 𝑧 ) ↑𝑐 𝑅 ) )
69	68	adantl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ‘ 𝑧 ) = ( ( abs ‘ 𝑧 ) ↑𝑐 𝑅 ) )
70		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑧 ∈ ( ℤ≥ ‘ 2 ) )
71		eluz2b2	⊢ ( 𝑧 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑧 ∈ ℕ ∧ 1 < 𝑧 ) )
72	70 71	sylib	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑧 ∈ ℕ ∧ 1 < 𝑧 ) )
73	72	simpld	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑧 ∈ ℕ )
74	73	nnred	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑧 ∈ ℝ )
75	73	nnnn0d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑧 ∈ ℕ0 )
76	75	nn0ge0d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → 0 ≤ 𝑧 )
77	74 76	absidd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( abs ‘ 𝑧 ) = 𝑧 )
78	77	oveq1d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( abs ‘ 𝑧 ) ↑𝑐 𝑅 ) = ( 𝑧 ↑𝑐 𝑅 ) )
79	74	recnd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑧 ∈ ℂ )
80	73	nnne0d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑧 ≠ 0 )
81	22	rpcnd	⊢ ( 𝜑 → 𝑅 ∈ ℂ )
82	81	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑅 ∈ ℂ )
83	79 80 82	cxpefd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑧 ↑𝑐 𝑅 ) = ( exp ‘ ( 𝑅 · ( log ‘ 𝑧 ) ) ) )
84	5	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐹 ∈ 𝐴 )
85	6	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
86	7	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → 1 < ( 𝐹 ‘ 𝑁 ) )
87		eqid	⊢ ( ( log ‘ ( 𝐹 ‘ 𝑧 ) ) / ( log ‘ 𝑧 ) ) = ( ( log ‘ ( 𝐹 ‘ 𝑧 ) ) / ( log ‘ 𝑧 ) )
88		eqid	⊢ if ( ( 𝐹 ‘ 𝑧 ) ≤ 1 , 1 , ( 𝐹 ‘ 𝑧 ) ) = if ( ( 𝐹 ‘ 𝑧 ) ≤ 1 , 1 , ( 𝐹 ‘ 𝑧 ) )
89		eqid	⊢ ( ( log ‘ 𝑁 ) / ( log ‘ 𝑧 ) ) = ( ( log ‘ 𝑁 ) / ( log ‘ 𝑧 ) )
90	1 2 3 4 84 85 86 8 70 87 88 89	ostth2lem4	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( 1 < ( 𝐹 ‘ 𝑧 ) ∧ 𝑅 ≤ ( ( log ‘ ( 𝐹 ‘ 𝑧 ) ) / ( log ‘ 𝑧 ) ) ) )
91	90	simprd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑅 ≤ ( ( log ‘ ( 𝐹 ‘ 𝑧 ) ) / ( log ‘ 𝑧 ) ) )
92	90	simpld	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → 1 < ( 𝐹 ‘ 𝑧 ) )
93		eqid	⊢ if ( ( 𝐹 ‘ 𝑁 ) ≤ 1 , 1 , ( 𝐹 ‘ 𝑁 ) ) = if ( ( 𝐹 ‘ 𝑁 ) ≤ 1 , 1 , ( 𝐹 ‘ 𝑁 ) )
94		eqid	⊢ ( ( log ‘ 𝑧 ) / ( log ‘ 𝑁 ) ) = ( ( log ‘ 𝑧 ) / ( log ‘ 𝑁 ) )
95	1 2 3 4 84 70 92 87 85 8 93 94	ostth2lem4	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( 1 < ( 𝐹 ‘ 𝑁 ) ∧ ( ( log ‘ ( 𝐹 ‘ 𝑧 ) ) / ( log ‘ 𝑧 ) ) ≤ 𝑅 ) )
96	95	simprd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( log ‘ ( 𝐹 ‘ 𝑧 ) ) / ( log ‘ 𝑧 ) ) ≤ 𝑅 )
97	23	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑅 ∈ ℝ )
98	61	adantl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑧 ∈ ℤ )
99	98 62	syl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑧 ∈ ℚ )
100	2 14	abvcl	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑧 ∈ ℚ ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
101	84 99 100	syl2anc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
102	2 14 29	abvgt0	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) → 0 < ( 𝐹 ‘ 𝑧 ) )
103	84 99 80 102	syl3anc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → 0 < ( 𝐹 ‘ 𝑧 ) )
104	101 103	elrpd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ+ )
105	104	relogcld	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( log ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ )
106	73	nnrpd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑧 ∈ ℝ+ )
107	106	relogcld	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( log ‘ 𝑧 ) ∈ ℝ )
108		ef0	⊢ ( exp ‘ 0 ) = 1
109	72	simprd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → 1 < 𝑧 )
110	106	reeflogd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( exp ‘ ( log ‘ 𝑧 ) ) = 𝑧 )
111	109 110	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → 1 < ( exp ‘ ( log ‘ 𝑧 ) ) )
112	108 111	eqbrtrid	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( exp ‘ 0 ) < ( exp ‘ ( log ‘ 𝑧 ) ) )
113		0re	⊢ 0 ∈ ℝ
114		eflt	⊢ ( ( 0 ∈ ℝ ∧ ( log ‘ 𝑧 ) ∈ ℝ ) → ( 0 < ( log ‘ 𝑧 ) ↔ ( exp ‘ 0 ) < ( exp ‘ ( log ‘ 𝑧 ) ) ) )
115	113 107 114	sylancr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( 0 < ( log ‘ 𝑧 ) ↔ ( exp ‘ 0 ) < ( exp ‘ ( log ‘ 𝑧 ) ) ) )
116	112 115	mpbird	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → 0 < ( log ‘ 𝑧 ) )
117	116	gt0ne0d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( log ‘ 𝑧 ) ≠ 0 )
118	105 107 117	redivcld	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( log ‘ ( 𝐹 ‘ 𝑧 ) ) / ( log ‘ 𝑧 ) ) ∈ ℝ )
119	97 118	letri3d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑅 = ( ( log ‘ ( 𝐹 ‘ 𝑧 ) ) / ( log ‘ 𝑧 ) ) ↔ ( 𝑅 ≤ ( ( log ‘ ( 𝐹 ‘ 𝑧 ) ) / ( log ‘ 𝑧 ) ) ∧ ( ( log ‘ ( 𝐹 ‘ 𝑧 ) ) / ( log ‘ 𝑧 ) ) ≤ 𝑅 ) ) )
120	91 96 119	mpbir2and	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑅 = ( ( log ‘ ( 𝐹 ‘ 𝑧 ) ) / ( log ‘ 𝑧 ) ) )
121	120	oveq1d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑅 · ( log ‘ 𝑧 ) ) = ( ( ( log ‘ ( 𝐹 ‘ 𝑧 ) ) / ( log ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) )
122	105	recnd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( log ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℂ )
123	107	recnd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( log ‘ 𝑧 ) ∈ ℂ )
124	122 123 117	divcan1d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ( log ‘ ( 𝐹 ‘ 𝑧 ) ) / ( log ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) = ( log ‘ ( 𝐹 ‘ 𝑧 ) ) )
125	121 124	eqtrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑅 · ( log ‘ 𝑧 ) ) = ( log ‘ ( 𝐹 ‘ 𝑧 ) ) )
126	125	fveq2d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( exp ‘ ( 𝑅 · ( log ‘ 𝑧 ) ) ) = ( exp ‘ ( log ‘ ( 𝐹 ‘ 𝑧 ) ) ) )
127	104	reeflogd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( exp ‘ ( log ‘ ( 𝐹 ‘ 𝑧 ) ) ) = ( 𝐹 ‘ 𝑧 ) )
128	83 126 127	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑧 ↑𝑐 𝑅 ) = ( 𝐹 ‘ 𝑧 ) )
129	69 78 128	3eqtrrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐹 ‘ 𝑧 ) = ( ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ‘ 𝑧 ) )
130	1 2 5 60 129	ostthlem1	⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑅 ) ) )
131		oveq2	⊢ ( 𝑎 = 𝑅 → ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) = ( ( abs ‘ 𝑦 ) ↑𝑐 𝑅 ) )
132	131	mpteq2dv	⊢ ( 𝑎 = 𝑅 → ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑅 ) ) )
133	132	rspceeqv	⊢ ( ( 𝑅 ∈ ( 0 (,] 1 ) ∧ 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑅 ) ) ) → ∃ 𝑎 ∈ ( 0 (,] 1 ) 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) )
134	53 130 133	syl2anc	⊢ ( 𝜑 → ∃ 𝑎 ∈ ( 0 (,] 1 ) 𝐹 = ( 𝑦 ∈ ℚ ↦ ( ( abs ‘ 𝑦 ) ↑𝑐 𝑎 ) ) )