Proof of Theorem ostth2lem3
| Step | Hyp | Ref
| Expression |
| 1 | | ostth.1 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ 𝐴) |
| 2 | | ostth2.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘2)) |
| 3 | | eluz2b2 12963 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 1 < 𝑁)) |
| 4 | 2, 3 | sylib 218 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 1 < 𝑁)) |
| 5 | 4 | simpld 494 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 6 | | nnq 13004 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℚ) |
| 7 | 5, 6 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℚ) |
| 8 | | qabsabv.a |
. . . . . . 7
⊢ 𝐴 = (AbsVal‘𝑄) |
| 9 | | qrng.q |
. . . . . . . 8
⊢ 𝑄 = (ℂfld
↾s ℚ) |
| 10 | 9 | qrngbas 27663 |
. . . . . . 7
⊢ ℚ =
(Base‘𝑄) |
| 11 | 8, 10 | abvcl 20817 |
. . . . . 6
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑁 ∈ ℚ) → (𝐹‘𝑁) ∈ ℝ) |
| 12 | 1, 7, 11 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝑁) ∈ ℝ) |
| 13 | 12 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝐹‘𝑁) ∈ ℝ) |
| 14 | 13 | recnd 11289 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝐹‘𝑁) ∈ ℂ) |
| 15 | | ostth2.7 |
. . . . . . 7
⊢ 𝑇 = if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)) |
| 16 | | 1re 11261 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
| 17 | | ostth2.5 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘2)) |
| 18 | | eluz2b2 12963 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈
(ℤ≥‘2) ↔ (𝑀 ∈ ℕ ∧ 1 < 𝑀)) |
| 19 | 17, 18 | sylib 218 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 1 < 𝑀)) |
| 20 | 19 | simpld 494 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 21 | | nnq 13004 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℚ) |
| 22 | 20, 21 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℚ) |
| 23 | 8, 10 | abvcl 20817 |
. . . . . . . . 9
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → (𝐹‘𝑀) ∈ ℝ) |
| 24 | 1, 22, 23 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝑀) ∈ ℝ) |
| 25 | | ifcl 4571 |
. . . . . . . 8
⊢ ((1
∈ ℝ ∧ (𝐹‘𝑀) ∈ ℝ) → if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)) ∈ ℝ) |
| 26 | 16, 24, 25 | sylancr 587 |
. . . . . . 7
⊢ (𝜑 → if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)) ∈ ℝ) |
| 27 | 15, 26 | eqeltrid 2845 |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈ ℝ) |
| 28 | 27 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑇 ∈ ℝ) |
| 29 | | 0red 11264 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℝ) |
| 30 | | 1red 11262 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℝ) |
| 31 | | 0lt1 11785 |
. . . . . . . . . 10
⊢ 0 <
1 |
| 32 | 31 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 < 1) |
| 33 | | max2 13229 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑀) ∈ ℝ ∧ 1 ∈ ℝ)
→ 1 ≤ if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀))) |
| 34 | 24, 30, 33 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ≤ if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀))) |
| 35 | 34, 15 | breqtrrdi 5185 |
. . . . . . . . 9
⊢ (𝜑 → 1 ≤ 𝑇) |
| 36 | 29, 30, 27, 32, 35 | ltletrd 11421 |
. . . . . . . 8
⊢ (𝜑 → 0 < 𝑇) |
| 37 | 36 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 0 < 𝑇) |
| 38 | 28, 37 | elrpd 13074 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑇 ∈
ℝ+) |
| 39 | 38 | rpge0d 13081 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 0 ≤ 𝑇) |
| 40 | | ostth2.8 |
. . . . . . . 8
⊢ 𝑈 = ((log‘𝑁) / (log‘𝑀)) |
| 41 | 5 | nnred 12281 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 42 | 4 | simprd 495 |
. . . . . . . . . 10
⊢ (𝜑 → 1 < 𝑁) |
| 43 | 41, 42 | rplogcld 26671 |
. . . . . . . . 9
⊢ (𝜑 → (log‘𝑁) ∈
ℝ+) |
| 44 | 20 | nnred 12281 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 45 | 19 | simprd 495 |
. . . . . . . . . 10
⊢ (𝜑 → 1 < 𝑀) |
| 46 | 44, 45 | rplogcld 26671 |
. . . . . . . . 9
⊢ (𝜑 → (log‘𝑀) ∈
ℝ+) |
| 47 | 43, 46 | rpdivcld 13094 |
. . . . . . . 8
⊢ (𝜑 → ((log‘𝑁) / (log‘𝑀)) ∈
ℝ+) |
| 48 | 40, 47 | eqeltrid 2845 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈
ℝ+) |
| 49 | 48 | rpred 13077 |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈ ℝ) |
| 50 | 49 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑈 ∈ ℝ) |
| 51 | 28, 39, 50 | recxpcld 26765 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑇↑𝑐𝑈) ∈ ℝ) |
| 52 | 51 | recnd 11289 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑇↑𝑐𝑈) ∈ ℂ) |
| 53 | 38, 50 | rpcxpcld 26775 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑇↑𝑐𝑈) ∈
ℝ+) |
| 54 | 53 | rpne0d 13082 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑇↑𝑐𝑈) ≠ 0) |
| 55 | | nnnn0 12533 |
. . . 4
⊢ (𝑋 ∈ ℕ → 𝑋 ∈
ℕ0) |
| 56 | 55 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑋 ∈
ℕ0) |
| 57 | 14, 52, 54, 56 | expdivd 14200 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (((𝐹‘𝑁) / (𝑇↑𝑐𝑈))↑𝑋) = (((𝐹‘𝑁)↑𝑋) / ((𝑇↑𝑐𝑈)↑𝑋))) |
| 58 | | reexpcl 14119 |
. . . . . 6
⊢ (((𝐹‘𝑁) ∈ ℝ ∧ 𝑋 ∈ ℕ0) → ((𝐹‘𝑁)↑𝑋) ∈ ℝ) |
| 59 | 12, 55, 58 | syl2an 596 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝐹‘𝑁)↑𝑋) ∈ ℝ) |
| 60 | 20 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑀 ∈ ℕ) |
| 61 | 60 | nnred 12281 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑀 ∈ ℝ) |
| 62 | | nnre 12273 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℕ → 𝑋 ∈
ℝ) |
| 63 | 62 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑋 ∈ ℝ) |
| 64 | 63, 50 | remulcld 11291 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑋 · 𝑈) ∈ ℝ) |
| 65 | 56 | nn0ge0d 12590 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 0 ≤ 𝑋) |
| 66 | 48 | rpge0d 13081 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ 𝑈) |
| 67 | 66 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 0 ≤ 𝑈) |
| 68 | 63, 50, 65, 67 | mulge0d 11840 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 0 ≤ (𝑋 · 𝑈)) |
| 69 | | flge0nn0 13860 |
. . . . . . . . . 10
⊢ (((𝑋 · 𝑈) ∈ ℝ ∧ 0 ≤ (𝑋 · 𝑈)) → (⌊‘(𝑋 · 𝑈)) ∈
ℕ0) |
| 70 | 64, 68, 69 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) →
(⌊‘(𝑋 ·
𝑈)) ∈
ℕ0) |
| 71 | | peano2nn0 12566 |
. . . . . . . . 9
⊢
((⌊‘(𝑋
· 𝑈)) ∈
ℕ0 → ((⌊‘(𝑋 · 𝑈)) + 1) ∈
ℕ0) |
| 72 | 70, 71 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) →
((⌊‘(𝑋 ·
𝑈)) + 1) ∈
ℕ0) |
| 73 | 72 | nn0red 12588 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) →
((⌊‘(𝑋 ·
𝑈)) + 1) ∈
ℝ) |
| 74 | 61, 73 | remulcld 11291 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) ∈ ℝ) |
| 75 | 28, 72 | reexpcld 14203 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1)) ∈ ℝ) |
| 76 | 74, 75 | remulcld 11291 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))) ∈ ℝ) |
| 77 | | peano2re 11434 |
. . . . . . . . 9
⊢ (𝑈 ∈ ℝ → (𝑈 + 1) ∈
ℝ) |
| 78 | 50, 77 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑈 + 1) ∈ ℝ) |
| 79 | 63, 78 | remulcld 11291 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑋 · (𝑈 + 1)) ∈ ℝ) |
| 80 | 61, 79 | remulcld 11291 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑀 · (𝑋 · (𝑈 + 1))) ∈ ℝ) |
| 81 | 51, 56 | reexpcld 14203 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑇↑𝑐𝑈)↑𝑋) ∈ ℝ) |
| 82 | 81, 28 | remulcld 11291 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇) ∈ ℝ) |
| 83 | 80, 82 | remulcld 11291 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀 · (𝑋 · (𝑈 + 1))) · (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇)) ∈ ℝ) |
| 84 | 9, 8 | qabvexp 27670 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑁 ∈ ℚ ∧ 𝑋 ∈ ℕ0) → (𝐹‘(𝑁↑𝑋)) = ((𝐹‘𝑁)↑𝑋)) |
| 85 | 1, 7, 55, 84 | syl2an3an 1424 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝐹‘(𝑁↑𝑋)) = ((𝐹‘𝑁)↑𝑋)) |
| 86 | 63 | recnd 11289 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑋 ∈ ℂ) |
| 87 | 43 | rpred 13077 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (log‘𝑁) ∈
ℝ) |
| 88 | 87 | recnd 11289 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (log‘𝑁) ∈
ℂ) |
| 89 | 88 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (log‘𝑁) ∈
ℂ) |
| 90 | 46 | rpred 13077 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (log‘𝑀) ∈
ℝ) |
| 91 | 90 | recnd 11289 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (log‘𝑀) ∈
ℂ) |
| 92 | 91 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (log‘𝑀) ∈
ℂ) |
| 93 | 46 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (log‘𝑀) ∈
ℝ+) |
| 94 | 93 | rpne0d 13082 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (log‘𝑀) ≠ 0) |
| 95 | 86, 89, 92, 94 | divassd 12078 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑋 · (log‘𝑁)) / (log‘𝑀)) = (𝑋 · ((log‘𝑁) / (log‘𝑀)))) |
| 96 | 40 | oveq2i 7442 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 · 𝑈) = (𝑋 · ((log‘𝑁) / (log‘𝑀))) |
| 97 | 95, 96 | eqtr4di 2795 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑋 · (log‘𝑁)) / (log‘𝑀)) = (𝑋 · 𝑈)) |
| 98 | 97 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (((𝑋 · (log‘𝑁)) / (log‘𝑀)) · (log‘𝑀)) = ((𝑋 · 𝑈) · (log‘𝑀))) |
| 99 | 86, 89 | mulcld 11281 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑋 · (log‘𝑁)) ∈ ℂ) |
| 100 | 99, 92, 94 | divcan1d 12044 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (((𝑋 · (log‘𝑁)) / (log‘𝑀)) · (log‘𝑀)) = (𝑋 · (log‘𝑁))) |
| 101 | 98, 100 | eqtr3d 2779 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑋 · 𝑈) · (log‘𝑀)) = (𝑋 · (log‘𝑁))) |
| 102 | | flltp1 13840 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 · 𝑈) ∈ ℝ → (𝑋 · 𝑈) < ((⌊‘(𝑋 · 𝑈)) + 1)) |
| 103 | 64, 102 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑋 · 𝑈) < ((⌊‘(𝑋 · 𝑈)) + 1)) |
| 104 | 64, 73, 93, 103 | ltmul1dd 13132 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑋 · 𝑈) · (log‘𝑀)) < (((⌊‘(𝑋 · 𝑈)) + 1) · (log‘𝑀))) |
| 105 | 101, 104 | eqbrtrrd 5167 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑋 · (log‘𝑁)) < (((⌊‘(𝑋 · 𝑈)) + 1) · (log‘𝑀))) |
| 106 | 87 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (log‘𝑁) ∈
ℝ) |
| 107 | 63, 106 | remulcld 11291 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑋 · (log‘𝑁)) ∈ ℝ) |
| 108 | 90 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (log‘𝑀) ∈
ℝ) |
| 109 | 73, 108 | remulcld 11291 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) →
(((⌊‘(𝑋
· 𝑈)) + 1) ·
(log‘𝑀)) ∈
ℝ) |
| 110 | | eflt 16153 |
. . . . . . . . . . . 12
⊢ (((𝑋 · (log‘𝑁)) ∈ ℝ ∧
(((⌊‘(𝑋
· 𝑈)) + 1) ·
(log‘𝑀)) ∈
ℝ) → ((𝑋
· (log‘𝑁))
< (((⌊‘(𝑋
· 𝑈)) + 1) ·
(log‘𝑀)) ↔
(exp‘(𝑋 ·
(log‘𝑁))) <
(exp‘(((⌊‘(𝑋 · 𝑈)) + 1) · (log‘𝑀))))) |
| 111 | 107, 109,
110 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑋 · (log‘𝑁)) < (((⌊‘(𝑋 · 𝑈)) + 1) · (log‘𝑀)) ↔ (exp‘(𝑋 · (log‘𝑁))) <
(exp‘(((⌊‘(𝑋 · 𝑈)) + 1) · (log‘𝑀))))) |
| 112 | 105, 111 | mpbid 232 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (exp‘(𝑋 · (log‘𝑁))) <
(exp‘(((⌊‘(𝑋 · 𝑈)) + 1) · (log‘𝑀)))) |
| 113 | 5 | nnrpd 13075 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
ℝ+) |
| 114 | | nnz 12634 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℕ → 𝑋 ∈
ℤ) |
| 115 | | reexplog 26637 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ+
∧ 𝑋 ∈ ℤ)
→ (𝑁↑𝑋) = (exp‘(𝑋 · (log‘𝑁)))) |
| 116 | 113, 114,
115 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑁↑𝑋) = (exp‘(𝑋 · (log‘𝑁)))) |
| 117 | 60 | nnrpd 13075 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑀 ∈
ℝ+) |
| 118 | 72 | nn0zd 12639 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) →
((⌊‘(𝑋 ·
𝑈)) + 1) ∈
ℤ) |
| 119 | | reexplog 26637 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℝ+
∧ ((⌊‘(𝑋
· 𝑈)) + 1) ∈
ℤ) → (𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) =
(exp‘(((⌊‘(𝑋 · 𝑈)) + 1) · (log‘𝑀)))) |
| 120 | 117, 118,
119 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) =
(exp‘(((⌊‘(𝑋 · 𝑈)) + 1) · (log‘𝑀)))) |
| 121 | 112, 116,
120 | 3brtr4d 5175 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑁↑𝑋) < (𝑀↑((⌊‘(𝑋 · 𝑈)) + 1))) |
| 122 | | nnexpcl 14115 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ ℕ0)
→ (𝑁↑𝑋) ∈
ℕ) |
| 123 | 5, 55, 122 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑁↑𝑋) ∈ ℕ) |
| 124 | 60, 72 | nnexpcld 14284 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) ∈ ℕ) |
| 125 | | nnltlem1 12685 |
. . . . . . . . . 10
⊢ (((𝑁↑𝑋) ∈ ℕ ∧ (𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) ∈ ℕ) → ((𝑁↑𝑋) < (𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) ↔ (𝑁↑𝑋) ≤ ((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1))) |
| 126 | 123, 124,
125 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑁↑𝑋) < (𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) ↔ (𝑁↑𝑋) ≤ ((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1))) |
| 127 | 121, 126 | mpbid 232 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑁↑𝑋) ≤ ((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1)) |
| 128 | 123 | nnnn0d 12587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑁↑𝑋) ∈
ℕ0) |
| 129 | | nn0uz 12920 |
. . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘0) |
| 130 | 128, 129 | eleqtrdi 2851 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑁↑𝑋) ∈
(ℤ≥‘0)) |
| 131 | 124 | nnzd 12640 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) ∈ ℤ) |
| 132 | | peano2zm 12660 |
. . . . . . . . . 10
⊢ ((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) ∈ ℤ → ((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1) ∈
ℤ) |
| 133 | 131, 132 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1) ∈
ℤ) |
| 134 | | elfz5 13556 |
. . . . . . . . 9
⊢ (((𝑁↑𝑋) ∈ (ℤ≥‘0)
∧ ((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1) ∈ ℤ) →
((𝑁↑𝑋) ∈ (0...((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1)) ↔ (𝑁↑𝑋) ≤ ((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1))) |
| 135 | 130, 133,
134 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑁↑𝑋) ∈ (0...((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1)) ↔ (𝑁↑𝑋) ≤ ((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1))) |
| 136 | 127, 135 | mpbird 257 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑁↑𝑋) ∈ (0...((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1))) |
| 137 | | padic.j |
. . . . . . . . . 10
⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥))))) |
| 138 | | ostth.k |
. . . . . . . . . 10
⊢ 𝐾 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, 1)) |
| 139 | | ostth2.3 |
. . . . . . . . . 10
⊢ (𝜑 → 1 < (𝐹‘𝑁)) |
| 140 | | ostth2.4 |
. . . . . . . . . 10
⊢ 𝑅 = ((log‘(𝐹‘𝑁)) / (log‘𝑁)) |
| 141 | | ostth2.6 |
. . . . . . . . . 10
⊢ 𝑆 = ((log‘(𝐹‘𝑀)) / (log‘𝑀)) |
| 142 | 9, 8, 137, 138, 1, 2, 139, 140, 17, 141, 15 | ostth2lem2 27678 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((⌊‘(𝑋 · 𝑈)) + 1) ∈ ℕ0 ∧
(𝑁↑𝑋) ∈ (0...((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1))) → (𝐹‘(𝑁↑𝑋)) ≤ ((𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1)))) |
| 143 | 142 | 3expia 1122 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((⌊‘(𝑋 · 𝑈)) + 1) ∈ ℕ0) →
((𝑁↑𝑋) ∈ (0...((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1)) → (𝐹‘(𝑁↑𝑋)) ≤ ((𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))))) |
| 144 | 72, 143 | syldan 591 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑁↑𝑋) ∈ (0...((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1)) → (𝐹‘(𝑁↑𝑋)) ≤ ((𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))))) |
| 145 | 136, 144 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝐹‘(𝑁↑𝑋)) ≤ ((𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1)))) |
| 146 | 85, 145 | eqbrtrrd 5167 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝐹‘𝑁)↑𝑋) ≤ ((𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1)))) |
| 147 | 80, 75 | remulcld 11291 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀 · (𝑋 · (𝑈 + 1))) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))) ∈ ℝ) |
| 148 | | peano2re 11434 |
. . . . . . . . . 10
⊢ ((𝑋 · 𝑈) ∈ ℝ → ((𝑋 · 𝑈) + 1) ∈ ℝ) |
| 149 | 64, 148 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑋 · 𝑈) + 1) ∈ ℝ) |
| 150 | 70 | nn0red 12588 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) →
(⌊‘(𝑋 ·
𝑈)) ∈
ℝ) |
| 151 | | 1red 11262 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 1 ∈
ℝ) |
| 152 | | flle 13839 |
. . . . . . . . . . 11
⊢ ((𝑋 · 𝑈) ∈ ℝ →
(⌊‘(𝑋 ·
𝑈)) ≤ (𝑋 · 𝑈)) |
| 153 | 64, 152 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) →
(⌊‘(𝑋 ·
𝑈)) ≤ (𝑋 · 𝑈)) |
| 154 | 150, 64, 151, 153 | leadd1dd 11877 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) →
((⌊‘(𝑋 ·
𝑈)) + 1) ≤ ((𝑋 · 𝑈) + 1)) |
| 155 | | nnge1 12294 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℕ → 1 ≤
𝑋) |
| 156 | 155 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 1 ≤ 𝑋) |
| 157 | 151, 63, 64, 156 | leadd2dd 11878 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑋 · 𝑈) + 1) ≤ ((𝑋 · 𝑈) + 𝑋)) |
| 158 | 50 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑈 ∈ ℂ) |
| 159 | 151 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 1 ∈
ℂ) |
| 160 | 86, 158, 159 | adddid 11285 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑋 · (𝑈 + 1)) = ((𝑋 · 𝑈) + (𝑋 · 1))) |
| 161 | 86 | mulridd 11278 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑋 · 1) = 𝑋) |
| 162 | 161 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑋 · 𝑈) + (𝑋 · 1)) = ((𝑋 · 𝑈) + 𝑋)) |
| 163 | 160, 162 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑋 · (𝑈 + 1)) = ((𝑋 · 𝑈) + 𝑋)) |
| 164 | 157, 163 | breqtrrd 5171 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑋 · 𝑈) + 1) ≤ (𝑋 · (𝑈 + 1))) |
| 165 | 73, 149, 79, 154, 164 | letrd 11418 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) →
((⌊‘(𝑋 ·
𝑈)) + 1) ≤ (𝑋 · (𝑈 + 1))) |
| 166 | 60 | nngt0d 12315 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 0 < 𝑀) |
| 167 | | lemul2 12120 |
. . . . . . . . 9
⊢
((((⌊‘(𝑋
· 𝑈)) + 1) ∈
ℝ ∧ (𝑋 ·
(𝑈 + 1)) ∈ ℝ
∧ (𝑀 ∈ ℝ
∧ 0 < 𝑀)) →
(((⌊‘(𝑋
· 𝑈)) + 1) ≤
(𝑋 · (𝑈 + 1)) ↔ (𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) ≤ (𝑀 · (𝑋 · (𝑈 + 1))))) |
| 168 | 73, 79, 61, 166, 167 | syl112anc 1376 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) →
(((⌊‘(𝑋
· 𝑈)) + 1) ≤
(𝑋 · (𝑈 + 1)) ↔ (𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) ≤ (𝑀 · (𝑋 · (𝑈 + 1))))) |
| 169 | 165, 168 | mpbid 232 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) ≤ (𝑀 · (𝑋 · (𝑈 + 1)))) |
| 170 | | expgt0 14136 |
. . . . . . . . 9
⊢ ((𝑇 ∈ ℝ ∧
((⌊‘(𝑋 ·
𝑈)) + 1) ∈ ℤ
∧ 0 < 𝑇) → 0
< (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))) |
| 171 | 28, 118, 37, 170 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 0 < (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))) |
| 172 | | lemul1 12119 |
. . . . . . . 8
⊢ (((𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) ∈ ℝ ∧ (𝑀 · (𝑋 · (𝑈 + 1))) ∈ ℝ ∧ ((𝑇↑((⌊‘(𝑋 · 𝑈)) + 1)) ∈ ℝ ∧ 0 < (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1)))) → ((𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) ≤ (𝑀 · (𝑋 · (𝑈 + 1))) ↔ ((𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))) ≤ ((𝑀 · (𝑋 · (𝑈 + 1))) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))))) |
| 173 | 74, 80, 75, 171, 172 | syl112anc 1376 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) ≤ (𝑀 · (𝑋 · (𝑈 + 1))) ↔ ((𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))) ≤ ((𝑀 · (𝑋 · (𝑈 + 1))) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))))) |
| 174 | 169, 173 | mpbid 232 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))) ≤ ((𝑀 · (𝑋 · (𝑈 + 1))) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1)))) |
| 175 | 28 | recnd 11289 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑇 ∈ ℂ) |
| 176 | 175, 70 | expp1d 14187 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1)) = ((𝑇↑(⌊‘(𝑋 · 𝑈))) · 𝑇)) |
| 177 | 35 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 1 ≤ 𝑇) |
| 178 | | remulcl 11240 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝑈 · 𝑋) ∈ ℝ) |
| 179 | 49, 62, 178 | syl2an 596 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑈 · 𝑋) ∈ ℝ) |
| 180 | 86, 158 | mulcomd 11282 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑋 · 𝑈) = (𝑈 · 𝑋)) |
| 181 | 153, 180 | breqtrd 5169 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) →
(⌊‘(𝑋 ·
𝑈)) ≤ (𝑈 · 𝑋)) |
| 182 | 28, 177, 150, 179, 181 | cxplead 26763 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑇↑𝑐(⌊‘(𝑋 · 𝑈))) ≤ (𝑇↑𝑐(𝑈 · 𝑋))) |
| 183 | | cxpexp 26710 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ ℂ ∧
(⌊‘(𝑋 ·
𝑈)) ∈
ℕ0) → (𝑇↑𝑐(⌊‘(𝑋 · 𝑈))) = (𝑇↑(⌊‘(𝑋 · 𝑈)))) |
| 184 | 175, 70, 183 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑇↑𝑐(⌊‘(𝑋 · 𝑈))) = (𝑇↑(⌊‘(𝑋 · 𝑈)))) |
| 185 | 38, 50, 86 | cxpmuld 26779 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑇↑𝑐(𝑈 · 𝑋)) = ((𝑇↑𝑐𝑈)↑𝑐𝑋)) |
| 186 | | cxpexp 26710 |
. . . . . . . . . . . 12
⊢ (((𝑇↑𝑐𝑈) ∈ ℂ ∧ 𝑋 ∈ ℕ0)
→ ((𝑇↑𝑐𝑈)↑𝑐𝑋) = ((𝑇↑𝑐𝑈)↑𝑋)) |
| 187 | 52, 56, 186 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑇↑𝑐𝑈)↑𝑐𝑋) = ((𝑇↑𝑐𝑈)↑𝑋)) |
| 188 | 185, 187 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑇↑𝑐(𝑈 · 𝑋)) = ((𝑇↑𝑐𝑈)↑𝑋)) |
| 189 | 182, 184,
188 | 3brtr3d 5174 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑇↑(⌊‘(𝑋 · 𝑈))) ≤ ((𝑇↑𝑐𝑈)↑𝑋)) |
| 190 | 28, 70 | reexpcld 14203 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑇↑(⌊‘(𝑋 · 𝑈))) ∈ ℝ) |
| 191 | 190, 81, 38 | lemul1d 13120 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑇↑(⌊‘(𝑋 · 𝑈))) ≤ ((𝑇↑𝑐𝑈)↑𝑋) ↔ ((𝑇↑(⌊‘(𝑋 · 𝑈))) · 𝑇) ≤ (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇))) |
| 192 | 189, 191 | mpbid 232 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑇↑(⌊‘(𝑋 · 𝑈))) · 𝑇) ≤ (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇)) |
| 193 | 176, 192 | eqbrtrd 5165 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1)) ≤ (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇)) |
| 194 | | nngt0 12297 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℕ → 0 <
𝑋) |
| 195 | 194 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 0 < 𝑋) |
| 196 | | 0red 11264 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 0 ∈
ℝ) |
| 197 | 48 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑈 ∈
ℝ+) |
| 198 | 197 | rpgt0d 13080 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 0 < 𝑈) |
| 199 | 50 | ltp1d 12198 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑈 < (𝑈 + 1)) |
| 200 | 196, 50, 78, 198, 199 | lttrd 11422 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 0 < (𝑈 + 1)) |
| 201 | 63, 78, 195, 200 | mulgt0d 11416 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 0 < (𝑋 · (𝑈 + 1))) |
| 202 | 61, 79, 166, 201 | mulgt0d 11416 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 0 < (𝑀 · (𝑋 · (𝑈 + 1)))) |
| 203 | | lemul2 12120 |
. . . . . . . 8
⊢ (((𝑇↑((⌊‘(𝑋 · 𝑈)) + 1)) ∈ ℝ ∧ (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇) ∈ ℝ ∧ ((𝑀 · (𝑋 · (𝑈 + 1))) ∈ ℝ ∧ 0 < (𝑀 · (𝑋 · (𝑈 + 1))))) → ((𝑇↑((⌊‘(𝑋 · 𝑈)) + 1)) ≤ (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇) ↔ ((𝑀 · (𝑋 · (𝑈 + 1))) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))) ≤ ((𝑀 · (𝑋 · (𝑈 + 1))) · (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇)))) |
| 204 | 75, 82, 80, 202, 203 | syl112anc 1376 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑇↑((⌊‘(𝑋 · 𝑈)) + 1)) ≤ (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇) ↔ ((𝑀 · (𝑋 · (𝑈 + 1))) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))) ≤ ((𝑀 · (𝑋 · (𝑈 + 1))) · (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇)))) |
| 205 | 193, 204 | mpbid 232 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀 · (𝑋 · (𝑈 + 1))) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))) ≤ ((𝑀 · (𝑋 · (𝑈 + 1))) · (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇))) |
| 206 | 76, 147, 83, 174, 205 | letrd 11418 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))) ≤ ((𝑀 · (𝑋 · (𝑈 + 1))) · (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇))) |
| 207 | 59, 76, 83, 146, 206 | letrd 11418 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝐹‘𝑁)↑𝑋) ≤ ((𝑀 · (𝑋 · (𝑈 + 1))) · (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇))) |
| 208 | 80 | recnd 11289 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑀 · (𝑋 · (𝑈 + 1))) ∈ ℂ) |
| 209 | 81 | recnd 11289 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑇↑𝑐𝑈)↑𝑋) ∈ ℂ) |
| 210 | 208, 209,
175 | mul12d 11470 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀 · (𝑋 · (𝑈 + 1))) · (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇)) = (((𝑇↑𝑐𝑈)↑𝑋) · ((𝑀 · (𝑋 · (𝑈 + 1))) · 𝑇))) |
| 211 | 61 | recnd 11289 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑀 ∈ ℂ) |
| 212 | 79 | recnd 11289 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑋 · (𝑈 + 1)) ∈ ℂ) |
| 213 | 211, 212,
175 | mul32d 11471 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀 · (𝑋 · (𝑈 + 1))) · 𝑇) = ((𝑀 · 𝑇) · (𝑋 · (𝑈 + 1)))) |
| 214 | 211, 175 | mulcld 11281 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑀 · 𝑇) ∈ ℂ) |
| 215 | 78 | recnd 11289 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑈 + 1) ∈ ℂ) |
| 216 | 214, 86, 215 | mul12d 11470 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀 · 𝑇) · (𝑋 · (𝑈 + 1))) = (𝑋 · ((𝑀 · 𝑇) · (𝑈 + 1)))) |
| 217 | 213, 216 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀 · (𝑋 · (𝑈 + 1))) · 𝑇) = (𝑋 · ((𝑀 · 𝑇) · (𝑈 + 1)))) |
| 218 | 217 | oveq2d 7447 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (((𝑇↑𝑐𝑈)↑𝑋) · ((𝑀 · (𝑋 · (𝑈 + 1))) · 𝑇)) = (((𝑇↑𝑐𝑈)↑𝑋) · (𝑋 · ((𝑀 · 𝑇) · (𝑈 + 1))))) |
| 219 | 210, 218 | eqtrd 2777 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀 · (𝑋 · (𝑈 + 1))) · (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇)) = (((𝑇↑𝑐𝑈)↑𝑋) · (𝑋 · ((𝑀 · 𝑇) · (𝑈 + 1))))) |
| 220 | 207, 219 | breqtrd 5169 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝐹‘𝑁)↑𝑋) ≤ (((𝑇↑𝑐𝑈)↑𝑋) · (𝑋 · ((𝑀 · 𝑇) · (𝑈 + 1))))) |
| 221 | 61, 28 | remulcld 11291 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑀 · 𝑇) ∈ ℝ) |
| 222 | 221, 78 | remulcld 11291 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀 · 𝑇) · (𝑈 + 1)) ∈ ℝ) |
| 223 | 63, 222 | remulcld 11291 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑋 · ((𝑀 · 𝑇) · (𝑈 + 1))) ∈ ℝ) |
| 224 | 114 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑋 ∈ ℤ) |
| 225 | 53, 224 | rpexpcld 14286 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑇↑𝑐𝑈)↑𝑋) ∈
ℝ+) |
| 226 | 59, 223, 225 | ledivmuld 13130 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((((𝐹‘𝑁)↑𝑋) / ((𝑇↑𝑐𝑈)↑𝑋)) ≤ (𝑋 · ((𝑀 · 𝑇) · (𝑈 + 1))) ↔ ((𝐹‘𝑁)↑𝑋) ≤ (((𝑇↑𝑐𝑈)↑𝑋) · (𝑋 · ((𝑀 · 𝑇) · (𝑈 + 1)))))) |
| 227 | 220, 226 | mpbird 257 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (((𝐹‘𝑁)↑𝑋) / ((𝑇↑𝑐𝑈)↑𝑋)) ≤ (𝑋 · ((𝑀 · 𝑇) · (𝑈 + 1)))) |
| 228 | 57, 227 | eqbrtrd 5165 |
1
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (((𝐹‘𝑁) / (𝑇↑𝑐𝑈))↑𝑋) ≤ (𝑋 · ((𝑀 · 𝑇) · (𝑈 + 1)))) |