Metamath Proof Explorer

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 mulid1d ⊢ ( 𝜑 → ( ( 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 ‘ 𝑦 ) ↑𝑐 𝑎 ) ) )