| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ostth2.4 | . . . . 5
⊢ 𝑅 = ((log‘(𝐹‘𝑁)) / (log‘𝑁)) | 
| 2 |  | ostth.1 | . . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ 𝐴) | 
| 3 |  | ostth2.2 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘2)) | 
| 4 |  | eluz2b2 12963 | . . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 1 < 𝑁)) | 
| 5 | 3, 4 | sylib 218 | . . . . . . . . . 10
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 1 < 𝑁)) | 
| 6 | 5 | simpld 494 | . . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 7 |  | nnq 13004 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℚ) | 
| 8 | 6, 7 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℚ) | 
| 9 |  | qabsabv.a | . . . . . . . . 9
⊢ 𝐴 = (AbsVal‘𝑄) | 
| 10 |  | qrng.q | . . . . . . . . . 10
⊢ 𝑄 = (ℂfld
↾s ℚ) | 
| 11 | 10 | qrngbas 27663 | . . . . . . . . 9
⊢ ℚ =
(Base‘𝑄) | 
| 12 | 9, 11 | abvcl 20817 | . . . . . . . 8
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑁 ∈ ℚ) → (𝐹‘𝑁) ∈ ℝ) | 
| 13 | 2, 8, 12 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → (𝐹‘𝑁) ∈ ℝ) | 
| 14 |  | ostth2.3 | . . . . . . 7
⊢ (𝜑 → 1 < (𝐹‘𝑁)) | 
| 15 | 13, 14 | rplogcld 26671 | . . . . . 6
⊢ (𝜑 → (log‘(𝐹‘𝑁)) ∈
ℝ+) | 
| 16 | 6 | nnred 12281 | . . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 17 | 5 | simprd 495 | . . . . . . 7
⊢ (𝜑 → 1 < 𝑁) | 
| 18 | 16, 17 | rplogcld 26671 | . . . . . 6
⊢ (𝜑 → (log‘𝑁) ∈
ℝ+) | 
| 19 | 15, 18 | rpdivcld 13094 | . . . . 5
⊢ (𝜑 → ((log‘(𝐹‘𝑁)) / (log‘𝑁)) ∈
ℝ+) | 
| 20 | 1, 19 | eqeltrid 2845 | . . . 4
⊢ (𝜑 → 𝑅 ∈
ℝ+) | 
| 21 | 20 | rpred 13077 | . . 3
⊢ (𝜑 → 𝑅 ∈ ℝ) | 
| 22 | 20 | rpgt0d 13080 | . . 3
⊢ (𝜑 → 0 < 𝑅) | 
| 23 | 6 | nnnn0d 12587 | . . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 24 | 10, 9 | qabvle 27669 | . . . . . . . . 9
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0) → (𝐹‘𝑁) ≤ 𝑁) | 
| 25 | 2, 23, 24 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (𝐹‘𝑁) ≤ 𝑁) | 
| 26 | 6 | nnne0d 12316 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ≠ 0) | 
| 27 | 10 | qrng0 27665 | . . . . . . . . . . . 12
⊢ 0 =
(0g‘𝑄) | 
| 28 | 9, 11, 27 | abvgt0 20821 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑁 ∈ ℚ ∧ 𝑁 ≠ 0) → 0 < (𝐹‘𝑁)) | 
| 29 | 2, 8, 26, 28 | syl3anc 1373 | . . . . . . . . . 10
⊢ (𝜑 → 0 < (𝐹‘𝑁)) | 
| 30 | 13, 29 | elrpd 13074 | . . . . . . . . 9
⊢ (𝜑 → (𝐹‘𝑁) ∈
ℝ+) | 
| 31 | 30 | reeflogd 26666 | . . . . . . . 8
⊢ (𝜑 →
(exp‘(log‘(𝐹‘𝑁))) = (𝐹‘𝑁)) | 
| 32 | 6 | nnrpd 13075 | . . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈
ℝ+) | 
| 33 | 32 | reeflogd 26666 | . . . . . . . 8
⊢ (𝜑 →
(exp‘(log‘𝑁)) =
𝑁) | 
| 34 | 25, 31, 33 | 3brtr4d 5175 | . . . . . . 7
⊢ (𝜑 →
(exp‘(log‘(𝐹‘𝑁))) ≤ (exp‘(log‘𝑁))) | 
| 35 | 15 | rpred 13077 | . . . . . . . 8
⊢ (𝜑 → (log‘(𝐹‘𝑁)) ∈ ℝ) | 
| 36 | 32 | relogcld 26665 | . . . . . . . 8
⊢ (𝜑 → (log‘𝑁) ∈
ℝ) | 
| 37 |  | efle 16154 | . . . . . . . 8
⊢
(((log‘(𝐹‘𝑁)) ∈ ℝ ∧ (log‘𝑁) ∈ ℝ) →
((log‘(𝐹‘𝑁)) ≤ (log‘𝑁) ↔
(exp‘(log‘(𝐹‘𝑁))) ≤ (exp‘(log‘𝑁)))) | 
| 38 | 35, 36, 37 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → ((log‘(𝐹‘𝑁)) ≤ (log‘𝑁) ↔ (exp‘(log‘(𝐹‘𝑁))) ≤ (exp‘(log‘𝑁)))) | 
| 39 | 34, 38 | mpbird 257 | . . . . . 6
⊢ (𝜑 → (log‘(𝐹‘𝑁)) ≤ (log‘𝑁)) | 
| 40 | 18 | rpcnd 13079 | . . . . . . 7
⊢ (𝜑 → (log‘𝑁) ∈
ℂ) | 
| 41 | 40 | mulridd 11278 | . . . . . 6
⊢ (𝜑 → ((log‘𝑁) · 1) = (log‘𝑁)) | 
| 42 | 39, 41 | breqtrrd 5171 | . . . . 5
⊢ (𝜑 → (log‘(𝐹‘𝑁)) ≤ ((log‘𝑁) · 1)) | 
| 43 |  | 1red 11262 | . . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) | 
| 44 | 35, 43, 18 | ledivmuld 13130 | . . . . 5
⊢ (𝜑 → (((log‘(𝐹‘𝑁)) / (log‘𝑁)) ≤ 1 ↔ (log‘(𝐹‘𝑁)) ≤ ((log‘𝑁) · 1))) | 
| 45 | 42, 44 | mpbird 257 | . . . 4
⊢ (𝜑 → ((log‘(𝐹‘𝑁)) / (log‘𝑁)) ≤ 1) | 
| 46 | 1, 45 | eqbrtrid 5178 | . . 3
⊢ (𝜑 → 𝑅 ≤ 1) | 
| 47 |  | 0xr 11308 | . . . 4
⊢ 0 ∈
ℝ* | 
| 48 |  | 1re 11261 | . . . 4
⊢ 1 ∈
ℝ | 
| 49 |  | elioc2 13450 | . . . 4
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ) → (𝑅 ∈ (0(,]1) ↔ (𝑅 ∈ ℝ ∧ 0 < 𝑅 ∧ 𝑅 ≤ 1))) | 
| 50 | 47, 48, 49 | mp2an 692 | . . 3
⊢ (𝑅 ∈ (0(,]1) ↔ (𝑅 ∈ ℝ ∧ 0 <
𝑅 ∧ 𝑅 ≤ 1)) | 
| 51 | 21, 22, 46, 50 | syl3anbrc 1344 | . 2
⊢ (𝜑 → 𝑅 ∈ (0(,]1)) | 
| 52 | 10, 9 | qabsabv 27673 | . . . 4
⊢ (abs
↾ ℚ) ∈ 𝐴 | 
| 53 |  | fvres 6925 | . . . . . . . 8
⊢ (𝑦 ∈ ℚ → ((abs
↾ ℚ)‘𝑦) =
(abs‘𝑦)) | 
| 54 | 53 | oveq1d 7446 | . . . . . . 7
⊢ (𝑦 ∈ ℚ → (((abs
↾ ℚ)‘𝑦)↑𝑐𝑅) = ((abs‘𝑦)↑𝑐𝑅)) | 
| 55 | 54 | mpteq2ia 5245 | . . . . . 6
⊢ (𝑦 ∈ ℚ ↦ (((abs
↾ ℚ)‘𝑦)↑𝑐𝑅)) = (𝑦 ∈ ℚ ↦ ((abs‘𝑦)↑𝑐𝑅)) | 
| 56 | 55 | eqcomi 2746 | . . . . 5
⊢ (𝑦 ∈ ℚ ↦
((abs‘𝑦)↑𝑐𝑅)) = (𝑦 ∈ ℚ ↦ (((abs ↾
ℚ)‘𝑦)↑𝑐𝑅)) | 
| 57 | 9, 11, 56 | abvcxp 27659 | . . . 4
⊢ (((abs
↾ ℚ) ∈ 𝐴
∧ 𝑅 ∈ (0(,]1))
→ (𝑦 ∈ ℚ
↦ ((abs‘𝑦)↑𝑐𝑅)) ∈ 𝐴) | 
| 58 | 52, 51, 57 | sylancr 587 | . . 3
⊢ (𝜑 → (𝑦 ∈ ℚ ↦ ((abs‘𝑦)↑𝑐𝑅)) ∈ 𝐴) | 
| 59 |  | eluzelz 12888 | . . . . . 6
⊢ (𝑧 ∈
(ℤ≥‘2) → 𝑧 ∈ ℤ) | 
| 60 |  | zq 12996 | . . . . . 6
⊢ (𝑧 ∈ ℤ → 𝑧 ∈
ℚ) | 
| 61 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑦 = 𝑧 → (abs‘𝑦) = (abs‘𝑧)) | 
| 62 | 61 | oveq1d 7446 | . . . . . . 7
⊢ (𝑦 = 𝑧 → ((abs‘𝑦)↑𝑐𝑅) = ((abs‘𝑧)↑𝑐𝑅)) | 
| 63 |  | eqid 2737 | . . . . . . 7
⊢ (𝑦 ∈ ℚ ↦
((abs‘𝑦)↑𝑐𝑅)) = (𝑦 ∈ ℚ ↦ ((abs‘𝑦)↑𝑐𝑅)) | 
| 64 |  | ovex 7464 | . . . . . . 7
⊢
((abs‘𝑧)↑𝑐𝑅) ∈ V | 
| 65 | 62, 63, 64 | fvmpt 7016 | . . . . . 6
⊢ (𝑧 ∈ ℚ → ((𝑦 ∈ ℚ ↦
((abs‘𝑦)↑𝑐𝑅))‘𝑧) = ((abs‘𝑧)↑𝑐𝑅)) | 
| 66 | 59, 60, 65 | 3syl 18 | . . . . 5
⊢ (𝑧 ∈
(ℤ≥‘2) → ((𝑦 ∈ ℚ ↦ ((abs‘𝑦)↑𝑐𝑅))‘𝑧) = ((abs‘𝑧)↑𝑐𝑅)) | 
| 67 | 66 | adantl 481 | . . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ ((𝑦 ∈ ℚ
↦ ((abs‘𝑦)↑𝑐𝑅))‘𝑧) = ((abs‘𝑧)↑𝑐𝑅)) | 
| 68 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ 𝑧 ∈
(ℤ≥‘2)) | 
| 69 |  | eluz2b2 12963 | . . . . . . . . 9
⊢ (𝑧 ∈
(ℤ≥‘2) ↔ (𝑧 ∈ ℕ ∧ 1 < 𝑧)) | 
| 70 | 68, 69 | sylib 218 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ (𝑧 ∈ ℕ
∧ 1 < 𝑧)) | 
| 71 | 70 | simpld 494 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ 𝑧 ∈
ℕ) | 
| 72 | 71 | nnred 12281 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ 𝑧 ∈
ℝ) | 
| 73 | 71 | nnnn0d 12587 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ 𝑧 ∈
ℕ0) | 
| 74 | 73 | nn0ge0d 12590 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ 0 ≤ 𝑧) | 
| 75 | 72, 74 | absidd 15461 | . . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ (abs‘𝑧) =
𝑧) | 
| 76 | 75 | oveq1d 7446 | . . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ ((abs‘𝑧)↑𝑐𝑅) = (𝑧↑𝑐𝑅)) | 
| 77 | 72 | recnd 11289 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ 𝑧 ∈
ℂ) | 
| 78 | 71 | nnne0d 12316 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ 𝑧 ≠
0) | 
| 79 | 20 | rpcnd 13079 | . . . . . . 7
⊢ (𝜑 → 𝑅 ∈ ℂ) | 
| 80 | 79 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ 𝑅 ∈
ℂ) | 
| 81 | 77, 78, 80 | cxpefd 26754 | . . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ (𝑧↑𝑐𝑅) = (exp‘(𝑅 · (log‘𝑧)))) | 
| 82 |  | padic.j | . . . . . . . . . . 11
⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥))))) | 
| 83 |  | ostth.k | . . . . . . . . . . 11
⊢ 𝐾 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, 1)) | 
| 84 | 2 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ 𝐹 ∈ 𝐴) | 
| 85 | 3 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ 𝑁 ∈
(ℤ≥‘2)) | 
| 86 | 14 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ 1 < (𝐹‘𝑁)) | 
| 87 |  | eqid 2737 | . . . . . . . . . . 11
⊢
((log‘(𝐹‘𝑧)) / (log‘𝑧)) = ((log‘(𝐹‘𝑧)) / (log‘𝑧)) | 
| 88 |  | eqid 2737 | . . . . . . . . . . 11
⊢ if((𝐹‘𝑧) ≤ 1, 1, (𝐹‘𝑧)) = if((𝐹‘𝑧) ≤ 1, 1, (𝐹‘𝑧)) | 
| 89 |  | eqid 2737 | . . . . . . . . . . 11
⊢
((log‘𝑁) /
(log‘𝑧)) =
((log‘𝑁) /
(log‘𝑧)) | 
| 90 | 10, 9, 82, 83, 84, 85, 86, 1, 68, 87, 88, 89 | ostth2lem4 27680 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ (1 < (𝐹‘𝑧) ∧ 𝑅 ≤ ((log‘(𝐹‘𝑧)) / (log‘𝑧)))) | 
| 91 | 90 | simprd 495 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ 𝑅 ≤
((log‘(𝐹‘𝑧)) / (log‘𝑧))) | 
| 92 | 90 | simpld 494 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ 1 < (𝐹‘𝑧)) | 
| 93 |  | eqid 2737 | . . . . . . . . . . 11
⊢ if((𝐹‘𝑁) ≤ 1, 1, (𝐹‘𝑁)) = if((𝐹‘𝑁) ≤ 1, 1, (𝐹‘𝑁)) | 
| 94 |  | eqid 2737 | . . . . . . . . . . 11
⊢
((log‘𝑧) /
(log‘𝑁)) =
((log‘𝑧) /
(log‘𝑁)) | 
| 95 | 10, 9, 82, 83, 84, 68, 92, 87, 85, 1, 93, 94 | ostth2lem4 27680 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ (1 < (𝐹‘𝑁) ∧ ((log‘(𝐹‘𝑧)) / (log‘𝑧)) ≤ 𝑅)) | 
| 96 | 95 | simprd 495 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ ((log‘(𝐹‘𝑧)) / (log‘𝑧)) ≤ 𝑅) | 
| 97 | 21 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ 𝑅 ∈
ℝ) | 
| 98 | 59 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ 𝑧 ∈
ℤ) | 
| 99 | 98, 60 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ 𝑧 ∈
ℚ) | 
| 100 | 9, 11 | abvcl 20817 | . . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑧 ∈ ℚ) → (𝐹‘𝑧) ∈ ℝ) | 
| 101 | 84, 99, 100 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ (𝐹‘𝑧) ∈
ℝ) | 
| 102 | 9, 11, 27 | abvgt0 20821 | . . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0) → 0 < (𝐹‘𝑧)) | 
| 103 | 84, 99, 78, 102 | syl3anc 1373 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ 0 < (𝐹‘𝑧)) | 
| 104 | 101, 103 | elrpd 13074 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ (𝐹‘𝑧) ∈
ℝ+) | 
| 105 | 104 | relogcld 26665 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ (log‘(𝐹‘𝑧)) ∈ ℝ) | 
| 106 | 71 | nnrpd 13075 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ 𝑧 ∈
ℝ+) | 
| 107 | 106 | relogcld 26665 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ (log‘𝑧) ∈
ℝ) | 
| 108 |  | ef0 16127 | . . . . . . . . . . . . . 14
⊢
(exp‘0) = 1 | 
| 109 | 70 | simprd 495 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ 1 < 𝑧) | 
| 110 | 106 | reeflogd 26666 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ (exp‘(log‘𝑧)) = 𝑧) | 
| 111 | 109, 110 | breqtrrd 5171 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ 1 < (exp‘(log‘𝑧))) | 
| 112 | 108, 111 | eqbrtrid 5178 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ (exp‘0) < (exp‘(log‘𝑧))) | 
| 113 |  | 0re 11263 | . . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ | 
| 114 |  | eflt 16153 | . . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ (log‘𝑧) ∈ ℝ) → (0 <
(log‘𝑧) ↔
(exp‘0) < (exp‘(log‘𝑧)))) | 
| 115 | 113, 107,
114 | sylancr 587 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ (0 < (log‘𝑧) ↔ (exp‘0) <
(exp‘(log‘𝑧)))) | 
| 116 | 112, 115 | mpbird 257 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ 0 < (log‘𝑧)) | 
| 117 | 116 | gt0ne0d 11827 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ (log‘𝑧) ≠
0) | 
| 118 | 105, 107,
117 | redivcld 12095 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ ((log‘(𝐹‘𝑧)) / (log‘𝑧)) ∈ ℝ) | 
| 119 | 97, 118 | letri3d 11403 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ (𝑅 =
((log‘(𝐹‘𝑧)) / (log‘𝑧)) ↔ (𝑅 ≤ ((log‘(𝐹‘𝑧)) / (log‘𝑧)) ∧ ((log‘(𝐹‘𝑧)) / (log‘𝑧)) ≤ 𝑅))) | 
| 120 | 91, 96, 119 | mpbir2and 713 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ 𝑅 =
((log‘(𝐹‘𝑧)) / (log‘𝑧))) | 
| 121 | 120 | oveq1d 7446 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ (𝑅 ·
(log‘𝑧)) =
(((log‘(𝐹‘𝑧)) / (log‘𝑧)) · (log‘𝑧))) | 
| 122 | 105 | recnd 11289 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ (log‘(𝐹‘𝑧)) ∈ ℂ) | 
| 123 | 107 | recnd 11289 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ (log‘𝑧) ∈
ℂ) | 
| 124 | 122, 123,
117 | divcan1d 12044 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ (((log‘(𝐹‘𝑧)) / (log‘𝑧)) · (log‘𝑧)) = (log‘(𝐹‘𝑧))) | 
| 125 | 121, 124 | eqtrd 2777 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ (𝑅 ·
(log‘𝑧)) =
(log‘(𝐹‘𝑧))) | 
| 126 | 125 | fveq2d 6910 | . . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ (exp‘(𝑅
· (log‘𝑧))) =
(exp‘(log‘(𝐹‘𝑧)))) | 
| 127 | 104 | reeflogd 26666 | . . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ (exp‘(log‘(𝐹‘𝑧))) = (𝐹‘𝑧)) | 
| 128 | 81, 126, 127 | 3eqtrd 2781 | . . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ (𝑧↑𝑐𝑅) = (𝐹‘𝑧)) | 
| 129 | 67, 76, 128 | 3eqtrrd 2782 | . . 3
⊢ ((𝜑 ∧ 𝑧 ∈ (ℤ≥‘2))
→ (𝐹‘𝑧) = ((𝑦 ∈ ℚ ↦ ((abs‘𝑦)↑𝑐𝑅))‘𝑧)) | 
| 130 | 10, 9, 2, 58, 129 | ostthlem1 27671 | . 2
⊢ (𝜑 → 𝐹 = (𝑦 ∈ ℚ ↦ ((abs‘𝑦)↑𝑐𝑅))) | 
| 131 |  | oveq2 7439 | . . . 4
⊢ (𝑎 = 𝑅 → ((abs‘𝑦)↑𝑐𝑎) = ((abs‘𝑦)↑𝑐𝑅)) | 
| 132 | 131 | mpteq2dv 5244 | . . 3
⊢ (𝑎 = 𝑅 → (𝑦 ∈ ℚ ↦ ((abs‘𝑦)↑𝑐𝑎)) = (𝑦 ∈ ℚ ↦ ((abs‘𝑦)↑𝑐𝑅))) | 
| 133 | 132 | rspceeqv 3645 | . 2
⊢ ((𝑅 ∈ (0(,]1) ∧ 𝐹 = (𝑦 ∈ ℚ ↦ ((abs‘𝑦)↑𝑐𝑅))) → ∃𝑎 ∈ (0(,]1)𝐹 = (𝑦 ∈ ℚ ↦ ((abs‘𝑦)↑𝑐𝑎))) | 
| 134 | 51, 130, 133 | syl2anc 584 | 1
⊢ (𝜑 → ∃𝑎 ∈ (0(,]1)𝐹 = (𝑦 ∈ ℚ ↦ ((abs‘𝑦)↑𝑐𝑎))) |