Proof of Theorem ostth2lem3
Step | Hyp | Ref
| Expression |
1 | | ostth.1 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ 𝐴) |
2 | | ostth2.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘2)) |
3 | | eluz2b2 12068 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 1 < 𝑁)) |
4 | 2, 3 | sylib 210 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 1 < 𝑁)) |
5 | 4 | simpld 490 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℕ) |
6 | | nnq 12109 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℚ) |
7 | 5, 6 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℚ) |
8 | | qabsabv.a |
. . . . . . 7
⊢ 𝐴 = (AbsVal‘𝑄) |
9 | | qrng.q |
. . . . . . . 8
⊢ 𝑄 = (ℂfld
↾s ℚ) |
10 | 9 | qrngbas 25760 |
. . . . . . 7
⊢ ℚ =
(Base‘𝑄) |
11 | 8, 10 | abvcl 19216 |
. . . . . 6
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑁 ∈ ℚ) → (𝐹‘𝑁) ∈ ℝ) |
12 | 1, 7, 11 | syl2anc 579 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝑁) ∈ ℝ) |
13 | 12 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝐹‘𝑁) ∈ ℝ) |
14 | 13 | recnd 10405 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝐹‘𝑁) ∈ ℂ) |
15 | | ostth2.7 |
. . . . . . 7
⊢ 𝑇 = if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)) |
16 | | 1re 10376 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
17 | | ostth2.5 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘2)) |
18 | | eluz2b2 12068 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈
(ℤ≥‘2) ↔ (𝑀 ∈ ℕ ∧ 1 < 𝑀)) |
19 | 17, 18 | sylib 210 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 1 < 𝑀)) |
20 | 19 | simpld 490 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℕ) |
21 | | nnq 12109 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℚ) |
22 | 20, 21 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℚ) |
23 | 8, 10 | abvcl 19216 |
. . . . . . . . 9
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ) → (𝐹‘𝑀) ∈ ℝ) |
24 | 1, 22, 23 | syl2anc 579 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝑀) ∈ ℝ) |
25 | | ifcl 4351 |
. . . . . . . 8
⊢ ((1
∈ ℝ ∧ (𝐹‘𝑀) ∈ ℝ) → if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)) ∈ ℝ) |
26 | 16, 24, 25 | sylancr 581 |
. . . . . . 7
⊢ (𝜑 → if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀)) ∈ ℝ) |
27 | 15, 26 | syl5eqel 2863 |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈ ℝ) |
28 | 27 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑇 ∈ ℝ) |
29 | | 0red 10380 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℝ) |
30 | | 1red 10377 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℝ) |
31 | | 0lt1 10897 |
. . . . . . . . . 10
⊢ 0 <
1 |
32 | 31 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 < 1) |
33 | | max2 12330 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑀) ∈ ℝ ∧ 1 ∈ ℝ)
→ 1 ≤ if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀))) |
34 | 24, 30, 33 | syl2anc 579 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ≤ if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀))) |
35 | 34, 15 | syl6breqr 4928 |
. . . . . . . . 9
⊢ (𝜑 → 1 ≤ 𝑇) |
36 | 29, 30, 27, 32, 35 | ltletrd 10536 |
. . . . . . . 8
⊢ (𝜑 → 0 < 𝑇) |
37 | 36 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 0 < 𝑇) |
38 | 28, 37 | elrpd 12178 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑇 ∈
ℝ+) |
39 | 38 | rpge0d 12185 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 0 ≤ 𝑇) |
40 | | ostth2.8 |
. . . . . . . 8
⊢ 𝑈 = ((log‘𝑁) / (log‘𝑀)) |
41 | 5 | nnred 11391 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℝ) |
42 | 4 | simprd 491 |
. . . . . . . . . 10
⊢ (𝜑 → 1 < 𝑁) |
43 | 41, 42 | rplogcld 24812 |
. . . . . . . . 9
⊢ (𝜑 → (log‘𝑁) ∈
ℝ+) |
44 | 20 | nnred 11391 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℝ) |
45 | 19 | simprd 491 |
. . . . . . . . . 10
⊢ (𝜑 → 1 < 𝑀) |
46 | 44, 45 | rplogcld 24812 |
. . . . . . . . 9
⊢ (𝜑 → (log‘𝑀) ∈
ℝ+) |
47 | 43, 46 | rpdivcld 12198 |
. . . . . . . 8
⊢ (𝜑 → ((log‘𝑁) / (log‘𝑀)) ∈
ℝ+) |
48 | 40, 47 | syl5eqel 2863 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈
ℝ+) |
49 | 48 | rpred 12181 |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈ ℝ) |
50 | 49 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑈 ∈ ℝ) |
51 | 28, 39, 50 | recxpcld 24906 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑇↑𝑐𝑈) ∈ ℝ) |
52 | 51 | recnd 10405 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑇↑𝑐𝑈) ∈ ℂ) |
53 | 38, 50 | rpcxpcld 24915 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑇↑𝑐𝑈) ∈
ℝ+) |
54 | 53 | rpne0d 12186 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑇↑𝑐𝑈) ≠ 0) |
55 | | nnnn0 11650 |
. . . 4
⊢ (𝑋 ∈ ℕ → 𝑋 ∈
ℕ0) |
56 | 55 | adantl 475 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑋 ∈
ℕ0) |
57 | 14, 52, 54, 56 | expdivd 13341 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (((𝐹‘𝑁) / (𝑇↑𝑐𝑈))↑𝑋) = (((𝐹‘𝑁)↑𝑋) / ((𝑇↑𝑐𝑈)↑𝑋))) |
58 | | reexpcl 13195 |
. . . . . 6
⊢ (((𝐹‘𝑁) ∈ ℝ ∧ 𝑋 ∈ ℕ0) → ((𝐹‘𝑁)↑𝑋) ∈ ℝ) |
59 | 12, 55, 58 | syl2an 589 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝐹‘𝑁)↑𝑋) ∈ ℝ) |
60 | 20 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑀 ∈ ℕ) |
61 | 60 | nnred 11391 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑀 ∈ ℝ) |
62 | | nnre 11382 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℕ → 𝑋 ∈
ℝ) |
63 | 62 | adantl 475 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑋 ∈ ℝ) |
64 | 63, 50 | remulcld 10407 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑋 · 𝑈) ∈ ℝ) |
65 | 56 | nn0ge0d 11705 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 0 ≤ 𝑋) |
66 | 48 | rpge0d 12185 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ 𝑈) |
67 | 66 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 0 ≤ 𝑈) |
68 | 63, 50, 65, 67 | mulge0d 10952 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 0 ≤ (𝑋 · 𝑈)) |
69 | | flge0nn0 12940 |
. . . . . . . . . 10
⊢ (((𝑋 · 𝑈) ∈ ℝ ∧ 0 ≤ (𝑋 · 𝑈)) → (⌊‘(𝑋 · 𝑈)) ∈
ℕ0) |
70 | 64, 68, 69 | syl2anc 579 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) →
(⌊‘(𝑋 ·
𝑈)) ∈
ℕ0) |
71 | | peano2nn0 11684 |
. . . . . . . . 9
⊢
((⌊‘(𝑋
· 𝑈)) ∈
ℕ0 → ((⌊‘(𝑋 · 𝑈)) + 1) ∈
ℕ0) |
72 | 70, 71 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) →
((⌊‘(𝑋 ·
𝑈)) + 1) ∈
ℕ0) |
73 | 72 | nn0red 11703 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) →
((⌊‘(𝑋 ·
𝑈)) + 1) ∈
ℝ) |
74 | 61, 73 | remulcld 10407 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) ∈ ℝ) |
75 | 28, 72 | reexpcld 13344 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1)) ∈ ℝ) |
76 | 74, 75 | remulcld 10407 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))) ∈ ℝ) |
77 | | peano2re 10549 |
. . . . . . . . 9
⊢ (𝑈 ∈ ℝ → (𝑈 + 1) ∈
ℝ) |
78 | 50, 77 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑈 + 1) ∈ ℝ) |
79 | 63, 78 | remulcld 10407 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑋 · (𝑈 + 1)) ∈ ℝ) |
80 | 61, 79 | remulcld 10407 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑀 · (𝑋 · (𝑈 + 1))) ∈ ℝ) |
81 | 51, 56 | reexpcld 13344 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑇↑𝑐𝑈)↑𝑋) ∈ ℝ) |
82 | 81, 28 | remulcld 10407 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇) ∈ ℝ) |
83 | 80, 82 | remulcld 10407 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀 · (𝑋 · (𝑈 + 1))) · (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇)) ∈ ℝ) |
84 | 1 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝐹 ∈ 𝐴) |
85 | 7 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑁 ∈ ℚ) |
86 | 9, 8 | qabvexp 25767 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝐴 ∧ 𝑁 ∈ ℚ ∧ 𝑋 ∈ ℕ0) → (𝐹‘(𝑁↑𝑋)) = ((𝐹‘𝑁)↑𝑋)) |
87 | 84, 85, 56, 86 | syl3anc 1439 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝐹‘(𝑁↑𝑋)) = ((𝐹‘𝑁)↑𝑋)) |
88 | 63 | recnd 10405 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑋 ∈ ℂ) |
89 | 43 | rpred 12181 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (log‘𝑁) ∈
ℝ) |
90 | 89 | recnd 10405 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (log‘𝑁) ∈
ℂ) |
91 | 90 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (log‘𝑁) ∈
ℂ) |
92 | 46 | rpred 12181 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (log‘𝑀) ∈
ℝ) |
93 | 92 | recnd 10405 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (log‘𝑀) ∈
ℂ) |
94 | 93 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (log‘𝑀) ∈
ℂ) |
95 | 46 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (log‘𝑀) ∈
ℝ+) |
96 | 95 | rpne0d 12186 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (log‘𝑀) ≠ 0) |
97 | 88, 91, 94, 96 | divassd 11186 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑋 · (log‘𝑁)) / (log‘𝑀)) = (𝑋 · ((log‘𝑁) / (log‘𝑀)))) |
98 | 40 | oveq2i 6933 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 · 𝑈) = (𝑋 · ((log‘𝑁) / (log‘𝑀))) |
99 | 97, 98 | syl6eqr 2832 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑋 · (log‘𝑁)) / (log‘𝑀)) = (𝑋 · 𝑈)) |
100 | 99 | oveq1d 6937 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (((𝑋 · (log‘𝑁)) / (log‘𝑀)) · (log‘𝑀)) = ((𝑋 · 𝑈) · (log‘𝑀))) |
101 | 88, 91 | mulcld 10397 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑋 · (log‘𝑁)) ∈ ℂ) |
102 | 101, 94, 96 | divcan1d 11152 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (((𝑋 · (log‘𝑁)) / (log‘𝑀)) · (log‘𝑀)) = (𝑋 · (log‘𝑁))) |
103 | 100, 102 | eqtr3d 2816 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑋 · 𝑈) · (log‘𝑀)) = (𝑋 · (log‘𝑁))) |
104 | | flltp1 12920 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 · 𝑈) ∈ ℝ → (𝑋 · 𝑈) < ((⌊‘(𝑋 · 𝑈)) + 1)) |
105 | 64, 104 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑋 · 𝑈) < ((⌊‘(𝑋 · 𝑈)) + 1)) |
106 | 64, 73, 95, 105 | ltmul1dd 12236 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑋 · 𝑈) · (log‘𝑀)) < (((⌊‘(𝑋 · 𝑈)) + 1) · (log‘𝑀))) |
107 | 103, 106 | eqbrtrrd 4910 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑋 · (log‘𝑁)) < (((⌊‘(𝑋 · 𝑈)) + 1) · (log‘𝑀))) |
108 | 89 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (log‘𝑁) ∈
ℝ) |
109 | 63, 108 | remulcld 10407 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑋 · (log‘𝑁)) ∈ ℝ) |
110 | 92 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (log‘𝑀) ∈
ℝ) |
111 | 73, 110 | remulcld 10407 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) →
(((⌊‘(𝑋
· 𝑈)) + 1) ·
(log‘𝑀)) ∈
ℝ) |
112 | | eflt 15249 |
. . . . . . . . . . . 12
⊢ (((𝑋 · (log‘𝑁)) ∈ ℝ ∧
(((⌊‘(𝑋
· 𝑈)) + 1) ·
(log‘𝑀)) ∈
ℝ) → ((𝑋
· (log‘𝑁))
< (((⌊‘(𝑋
· 𝑈)) + 1) ·
(log‘𝑀)) ↔
(exp‘(𝑋 ·
(log‘𝑁))) <
(exp‘(((⌊‘(𝑋 · 𝑈)) + 1) · (log‘𝑀))))) |
113 | 109, 111,
112 | syl2anc 579 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑋 · (log‘𝑁)) < (((⌊‘(𝑋 · 𝑈)) + 1) · (log‘𝑀)) ↔ (exp‘(𝑋 · (log‘𝑁))) <
(exp‘(((⌊‘(𝑋 · 𝑈)) + 1) · (log‘𝑀))))) |
114 | 107, 113 | mpbid 224 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (exp‘(𝑋 · (log‘𝑁))) <
(exp‘(((⌊‘(𝑋 · 𝑈)) + 1) · (log‘𝑀)))) |
115 | 5 | nnrpd 12179 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
ℝ+) |
116 | | nnz 11751 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℕ → 𝑋 ∈
ℤ) |
117 | | reexplog 24778 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ+
∧ 𝑋 ∈ ℤ)
→ (𝑁↑𝑋) = (exp‘(𝑋 · (log‘𝑁)))) |
118 | 115, 116,
117 | syl2an 589 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑁↑𝑋) = (exp‘(𝑋 · (log‘𝑁)))) |
119 | 60 | nnrpd 12179 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑀 ∈
ℝ+) |
120 | 72 | nn0zd 11832 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) →
((⌊‘(𝑋 ·
𝑈)) + 1) ∈
ℤ) |
121 | | reexplog 24778 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℝ+
∧ ((⌊‘(𝑋
· 𝑈)) + 1) ∈
ℤ) → (𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) =
(exp‘(((⌊‘(𝑋 · 𝑈)) + 1) · (log‘𝑀)))) |
122 | 119, 120,
121 | syl2anc 579 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) =
(exp‘(((⌊‘(𝑋 · 𝑈)) + 1) · (log‘𝑀)))) |
123 | 114, 118,
122 | 3brtr4d 4918 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑁↑𝑋) < (𝑀↑((⌊‘(𝑋 · 𝑈)) + 1))) |
124 | | nnexpcl 13191 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ ℕ0)
→ (𝑁↑𝑋) ∈
ℕ) |
125 | 5, 55, 124 | syl2an 589 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑁↑𝑋) ∈ ℕ) |
126 | 60, 72 | nnexpcld 13351 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) ∈ ℕ) |
127 | | nnltlem1 11796 |
. . . . . . . . . 10
⊢ (((𝑁↑𝑋) ∈ ℕ ∧ (𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) ∈ ℕ) → ((𝑁↑𝑋) < (𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) ↔ (𝑁↑𝑋) ≤ ((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1))) |
128 | 125, 126,
127 | syl2anc 579 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑁↑𝑋) < (𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) ↔ (𝑁↑𝑋) ≤ ((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1))) |
129 | 123, 128 | mpbid 224 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑁↑𝑋) ≤ ((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1)) |
130 | 125 | nnnn0d 11702 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑁↑𝑋) ∈
ℕ0) |
131 | | nn0uz 12028 |
. . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘0) |
132 | 130, 131 | syl6eleq 2869 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑁↑𝑋) ∈
(ℤ≥‘0)) |
133 | 126 | nnzd 11833 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) ∈ ℤ) |
134 | | peano2zm 11772 |
. . . . . . . . . 10
⊢ ((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) ∈ ℤ → ((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1) ∈
ℤ) |
135 | 133, 134 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1) ∈
ℤ) |
136 | | elfz5 12651 |
. . . . . . . . 9
⊢ (((𝑁↑𝑋) ∈ (ℤ≥‘0)
∧ ((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1) ∈ ℤ) →
((𝑁↑𝑋) ∈ (0...((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1)) ↔ (𝑁↑𝑋) ≤ ((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1))) |
137 | 132, 135,
136 | syl2anc 579 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑁↑𝑋) ∈ (0...((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1)) ↔ (𝑁↑𝑋) ≤ ((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1))) |
138 | 129, 137 | mpbird 249 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑁↑𝑋) ∈ (0...((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1))) |
139 | | padic.j |
. . . . . . . . . 10
⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥))))) |
140 | | ostth.k |
. . . . . . . . . 10
⊢ 𝐾 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, 1)) |
141 | | ostth2.3 |
. . . . . . . . . 10
⊢ (𝜑 → 1 < (𝐹‘𝑁)) |
142 | | ostth2.4 |
. . . . . . . . . 10
⊢ 𝑅 = ((log‘(𝐹‘𝑁)) / (log‘𝑁)) |
143 | | ostth2.6 |
. . . . . . . . . 10
⊢ 𝑆 = ((log‘(𝐹‘𝑀)) / (log‘𝑀)) |
144 | 9, 8, 139, 140, 1, 2, 141, 142, 17, 143, 15 | ostth2lem2 25775 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((⌊‘(𝑋 · 𝑈)) + 1) ∈ ℕ0 ∧
(𝑁↑𝑋) ∈ (0...((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1))) → (𝐹‘(𝑁↑𝑋)) ≤ ((𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1)))) |
145 | 144 | 3expia 1111 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((⌊‘(𝑋 · 𝑈)) + 1) ∈ ℕ0) →
((𝑁↑𝑋) ∈ (0...((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1)) → (𝐹‘(𝑁↑𝑋)) ≤ ((𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))))) |
146 | 72, 145 | syldan 585 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑁↑𝑋) ∈ (0...((𝑀↑((⌊‘(𝑋 · 𝑈)) + 1)) − 1)) → (𝐹‘(𝑁↑𝑋)) ≤ ((𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))))) |
147 | 138, 146 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝐹‘(𝑁↑𝑋)) ≤ ((𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1)))) |
148 | 87, 147 | eqbrtrrd 4910 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝐹‘𝑁)↑𝑋) ≤ ((𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1)))) |
149 | 80, 75 | remulcld 10407 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀 · (𝑋 · (𝑈 + 1))) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))) ∈ ℝ) |
150 | | peano2re 10549 |
. . . . . . . . . 10
⊢ ((𝑋 · 𝑈) ∈ ℝ → ((𝑋 · 𝑈) + 1) ∈ ℝ) |
151 | 64, 150 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑋 · 𝑈) + 1) ∈ ℝ) |
152 | 70 | nn0red 11703 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) →
(⌊‘(𝑋 ·
𝑈)) ∈
ℝ) |
153 | | 1red 10377 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 1 ∈
ℝ) |
154 | | flle 12919 |
. . . . . . . . . . 11
⊢ ((𝑋 · 𝑈) ∈ ℝ →
(⌊‘(𝑋 ·
𝑈)) ≤ (𝑋 · 𝑈)) |
155 | 64, 154 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) →
(⌊‘(𝑋 ·
𝑈)) ≤ (𝑋 · 𝑈)) |
156 | 152, 64, 153, 155 | leadd1dd 10989 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) →
((⌊‘(𝑋 ·
𝑈)) + 1) ≤ ((𝑋 · 𝑈) + 1)) |
157 | | nnge1 11404 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℕ → 1 ≤
𝑋) |
158 | 157 | adantl 475 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 1 ≤ 𝑋) |
159 | 153, 63, 64, 158 | leadd2dd 10990 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑋 · 𝑈) + 1) ≤ ((𝑋 · 𝑈) + 𝑋)) |
160 | 50 | recnd 10405 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑈 ∈ ℂ) |
161 | 153 | recnd 10405 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 1 ∈
ℂ) |
162 | 88, 160, 161 | adddid 10401 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑋 · (𝑈 + 1)) = ((𝑋 · 𝑈) + (𝑋 · 1))) |
163 | 88 | mulid1d 10394 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑋 · 1) = 𝑋) |
164 | 163 | oveq2d 6938 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑋 · 𝑈) + (𝑋 · 1)) = ((𝑋 · 𝑈) + 𝑋)) |
165 | 162, 164 | eqtrd 2814 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑋 · (𝑈 + 1)) = ((𝑋 · 𝑈) + 𝑋)) |
166 | 159, 165 | breqtrrd 4914 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑋 · 𝑈) + 1) ≤ (𝑋 · (𝑈 + 1))) |
167 | 73, 151, 79, 156, 166 | letrd 10533 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) →
((⌊‘(𝑋 ·
𝑈)) + 1) ≤ (𝑋 · (𝑈 + 1))) |
168 | 60 | nngt0d 11424 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 0 < 𝑀) |
169 | | lemul2 11230 |
. . . . . . . . 9
⊢
((((⌊‘(𝑋
· 𝑈)) + 1) ∈
ℝ ∧ (𝑋 ·
(𝑈 + 1)) ∈ ℝ
∧ (𝑀 ∈ ℝ
∧ 0 < 𝑀)) →
(((⌊‘(𝑋
· 𝑈)) + 1) ≤
(𝑋 · (𝑈 + 1)) ↔ (𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) ≤ (𝑀 · (𝑋 · (𝑈 + 1))))) |
170 | 73, 79, 61, 168, 169 | syl112anc 1442 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) →
(((⌊‘(𝑋
· 𝑈)) + 1) ≤
(𝑋 · (𝑈 + 1)) ↔ (𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) ≤ (𝑀 · (𝑋 · (𝑈 + 1))))) |
171 | 167, 170 | mpbid 224 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) ≤ (𝑀 · (𝑋 · (𝑈 + 1)))) |
172 | | expgt0 13211 |
. . . . . . . . 9
⊢ ((𝑇 ∈ ℝ ∧
((⌊‘(𝑋 ·
𝑈)) + 1) ∈ ℤ
∧ 0 < 𝑇) → 0
< (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))) |
173 | 28, 120, 37, 172 | syl3anc 1439 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 0 < (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))) |
174 | | lemul1 11229 |
. . . . . . . 8
⊢ (((𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) ∈ ℝ ∧ (𝑀 · (𝑋 · (𝑈 + 1))) ∈ ℝ ∧ ((𝑇↑((⌊‘(𝑋 · 𝑈)) + 1)) ∈ ℝ ∧ 0 < (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1)))) → ((𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) ≤ (𝑀 · (𝑋 · (𝑈 + 1))) ↔ ((𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))) ≤ ((𝑀 · (𝑋 · (𝑈 + 1))) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))))) |
175 | 74, 80, 75, 173, 174 | syl112anc 1442 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) ≤ (𝑀 · (𝑋 · (𝑈 + 1))) ↔ ((𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))) ≤ ((𝑀 · (𝑋 · (𝑈 + 1))) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))))) |
176 | 171, 175 | mpbid 224 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))) ≤ ((𝑀 · (𝑋 · (𝑈 + 1))) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1)))) |
177 | 28 | recnd 10405 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑇 ∈ ℂ) |
178 | 177, 70 | expp1d 13328 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1)) = ((𝑇↑(⌊‘(𝑋 · 𝑈))) · 𝑇)) |
179 | 35 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 1 ≤ 𝑇) |
180 | | remulcl 10357 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝑈 · 𝑋) ∈ ℝ) |
181 | 49, 62, 180 | syl2an 589 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑈 · 𝑋) ∈ ℝ) |
182 | 88, 160 | mulcomd 10398 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑋 · 𝑈) = (𝑈 · 𝑋)) |
183 | 155, 182 | breqtrd 4912 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) →
(⌊‘(𝑋 ·
𝑈)) ≤ (𝑈 · 𝑋)) |
184 | 28, 179, 152, 181, 183 | cxplead 24904 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑇↑𝑐(⌊‘(𝑋 · 𝑈))) ≤ (𝑇↑𝑐(𝑈 · 𝑋))) |
185 | | cxpexp 24851 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ ℂ ∧
(⌊‘(𝑋 ·
𝑈)) ∈
ℕ0) → (𝑇↑𝑐(⌊‘(𝑋 · 𝑈))) = (𝑇↑(⌊‘(𝑋 · 𝑈)))) |
186 | 177, 70, 185 | syl2anc 579 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑇↑𝑐(⌊‘(𝑋 · 𝑈))) = (𝑇↑(⌊‘(𝑋 · 𝑈)))) |
187 | 38, 50, 88 | cxpmuld 24919 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑇↑𝑐(𝑈 · 𝑋)) = ((𝑇↑𝑐𝑈)↑𝑐𝑋)) |
188 | | cxpexp 24851 |
. . . . . . . . . . . 12
⊢ (((𝑇↑𝑐𝑈) ∈ ℂ ∧ 𝑋 ∈ ℕ0)
→ ((𝑇↑𝑐𝑈)↑𝑐𝑋) = ((𝑇↑𝑐𝑈)↑𝑋)) |
189 | 52, 56, 188 | syl2anc 579 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑇↑𝑐𝑈)↑𝑐𝑋) = ((𝑇↑𝑐𝑈)↑𝑋)) |
190 | 187, 189 | eqtrd 2814 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑇↑𝑐(𝑈 · 𝑋)) = ((𝑇↑𝑐𝑈)↑𝑋)) |
191 | 184, 186,
190 | 3brtr3d 4917 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑇↑(⌊‘(𝑋 · 𝑈))) ≤ ((𝑇↑𝑐𝑈)↑𝑋)) |
192 | 28, 70 | reexpcld 13344 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑇↑(⌊‘(𝑋 · 𝑈))) ∈ ℝ) |
193 | 192, 81, 38 | lemul1d 12224 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑇↑(⌊‘(𝑋 · 𝑈))) ≤ ((𝑇↑𝑐𝑈)↑𝑋) ↔ ((𝑇↑(⌊‘(𝑋 · 𝑈))) · 𝑇) ≤ (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇))) |
194 | 191, 193 | mpbid 224 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑇↑(⌊‘(𝑋 · 𝑈))) · 𝑇) ≤ (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇)) |
195 | 178, 194 | eqbrtrd 4908 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1)) ≤ (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇)) |
196 | | nngt0 11407 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℕ → 0 <
𝑋) |
197 | 196 | adantl 475 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 0 < 𝑋) |
198 | | 0red 10380 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 0 ∈
ℝ) |
199 | 48 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑈 ∈
ℝ+) |
200 | 199 | rpgt0d 12184 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 0 < 𝑈) |
201 | 50 | ltp1d 11308 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑈 < (𝑈 + 1)) |
202 | 198, 50, 78, 200, 201 | lttrd 10537 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 0 < (𝑈 + 1)) |
203 | 63, 78, 197, 202 | mulgt0d 10531 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 0 < (𝑋 · (𝑈 + 1))) |
204 | 61, 79, 168, 203 | mulgt0d 10531 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 0 < (𝑀 · (𝑋 · (𝑈 + 1)))) |
205 | | lemul2 11230 |
. . . . . . . 8
⊢ (((𝑇↑((⌊‘(𝑋 · 𝑈)) + 1)) ∈ ℝ ∧ (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇) ∈ ℝ ∧ ((𝑀 · (𝑋 · (𝑈 + 1))) ∈ ℝ ∧ 0 < (𝑀 · (𝑋 · (𝑈 + 1))))) → ((𝑇↑((⌊‘(𝑋 · 𝑈)) + 1)) ≤ (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇) ↔ ((𝑀 · (𝑋 · (𝑈 + 1))) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))) ≤ ((𝑀 · (𝑋 · (𝑈 + 1))) · (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇)))) |
206 | 75, 82, 80, 204, 205 | syl112anc 1442 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑇↑((⌊‘(𝑋 · 𝑈)) + 1)) ≤ (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇) ↔ ((𝑀 · (𝑋 · (𝑈 + 1))) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))) ≤ ((𝑀 · (𝑋 · (𝑈 + 1))) · (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇)))) |
207 | 195, 206 | mpbid 224 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀 · (𝑋 · (𝑈 + 1))) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))) ≤ ((𝑀 · (𝑋 · (𝑈 + 1))) · (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇))) |
208 | 76, 149, 83, 176, 207 | letrd 10533 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀 · ((⌊‘(𝑋 · 𝑈)) + 1)) · (𝑇↑((⌊‘(𝑋 · 𝑈)) + 1))) ≤ ((𝑀 · (𝑋 · (𝑈 + 1))) · (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇))) |
209 | 59, 76, 83, 148, 208 | letrd 10533 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝐹‘𝑁)↑𝑋) ≤ ((𝑀 · (𝑋 · (𝑈 + 1))) · (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇))) |
210 | 80 | recnd 10405 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑀 · (𝑋 · (𝑈 + 1))) ∈ ℂ) |
211 | 81 | recnd 10405 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑇↑𝑐𝑈)↑𝑋) ∈ ℂ) |
212 | 210, 211,
177 | mul12d 10585 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀 · (𝑋 · (𝑈 + 1))) · (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇)) = (((𝑇↑𝑐𝑈)↑𝑋) · ((𝑀 · (𝑋 · (𝑈 + 1))) · 𝑇))) |
213 | 61 | recnd 10405 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑀 ∈ ℂ) |
214 | 79 | recnd 10405 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑋 · (𝑈 + 1)) ∈ ℂ) |
215 | 213, 214,
177 | mul32d 10586 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀 · (𝑋 · (𝑈 + 1))) · 𝑇) = ((𝑀 · 𝑇) · (𝑋 · (𝑈 + 1)))) |
216 | 213, 177 | mulcld 10397 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑀 · 𝑇) ∈ ℂ) |
217 | 78 | recnd 10405 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑈 + 1) ∈ ℂ) |
218 | 216, 88, 217 | mul12d 10585 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀 · 𝑇) · (𝑋 · (𝑈 + 1))) = (𝑋 · ((𝑀 · 𝑇) · (𝑈 + 1)))) |
219 | 215, 218 | eqtrd 2814 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀 · (𝑋 · (𝑈 + 1))) · 𝑇) = (𝑋 · ((𝑀 · 𝑇) · (𝑈 + 1)))) |
220 | 219 | oveq2d 6938 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (((𝑇↑𝑐𝑈)↑𝑋) · ((𝑀 · (𝑋 · (𝑈 + 1))) · 𝑇)) = (((𝑇↑𝑐𝑈)↑𝑋) · (𝑋 · ((𝑀 · 𝑇) · (𝑈 + 1))))) |
221 | 212, 220 | eqtrd 2814 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀 · (𝑋 · (𝑈 + 1))) · (((𝑇↑𝑐𝑈)↑𝑋) · 𝑇)) = (((𝑇↑𝑐𝑈)↑𝑋) · (𝑋 · ((𝑀 · 𝑇) · (𝑈 + 1))))) |
222 | 209, 221 | breqtrd 4912 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝐹‘𝑁)↑𝑋) ≤ (((𝑇↑𝑐𝑈)↑𝑋) · (𝑋 · ((𝑀 · 𝑇) · (𝑈 + 1))))) |
223 | 61, 28 | remulcld 10407 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑀 · 𝑇) ∈ ℝ) |
224 | 223, 78 | remulcld 10407 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑀 · 𝑇) · (𝑈 + 1)) ∈ ℝ) |
225 | 63, 224 | remulcld 10407 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (𝑋 · ((𝑀 · 𝑇) · (𝑈 + 1))) ∈ ℝ) |
226 | 116 | adantl 475 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → 𝑋 ∈ ℤ) |
227 | 53, 226 | rpexpcld 13353 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((𝑇↑𝑐𝑈)↑𝑋) ∈
ℝ+) |
228 | 59, 225, 227 | ledivmuld 12234 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → ((((𝐹‘𝑁)↑𝑋) / ((𝑇↑𝑐𝑈)↑𝑋)) ≤ (𝑋 · ((𝑀 · 𝑇) · (𝑈 + 1))) ↔ ((𝐹‘𝑁)↑𝑋) ≤ (((𝑇↑𝑐𝑈)↑𝑋) · (𝑋 · ((𝑀 · 𝑇) · (𝑈 + 1)))))) |
229 | 222, 228 | mpbird 249 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (((𝐹‘𝑁)↑𝑋) / ((𝑇↑𝑐𝑈)↑𝑋)) ≤ (𝑋 · ((𝑀 · 𝑇) · (𝑈 + 1)))) |
230 | 57, 229 | eqbrtrd 4908 |
1
⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (((𝐹‘𝑁) / (𝑇↑𝑐𝑈))↑𝑋) ≤ (𝑋 · ((𝑀 · 𝑇) · (𝑈 + 1)))) |