Proof of Theorem faclbnd4lem2
Step | Hyp | Ref
| Expression |
1 | | oveq1 7282 |
. . . . 5
⊢ (𝑀 = if(𝑀 ∈ ℕ0, 𝑀, 1) → (𝑀↑(𝑁 − 1)) = (if(𝑀 ∈ ℕ0, 𝑀, 1)↑(𝑁 − 1))) |
2 | 1 | oveq2d 7291 |
. . . 4
⊢ (𝑀 = if(𝑀 ∈ ℕ0, 𝑀, 1) → (((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) = (((𝑁 − 1)↑𝐾) · (if(𝑀 ∈ ℕ0, 𝑀, 1)↑(𝑁 − 1)))) |
3 | | id 22 |
. . . . . . 7
⊢ (𝑀 = if(𝑀 ∈ ℕ0, 𝑀, 1) → 𝑀 = if(𝑀 ∈ ℕ0, 𝑀, 1)) |
4 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑀 = if(𝑀 ∈ ℕ0, 𝑀, 1) → (𝑀 + 𝐾) = (if(𝑀 ∈ ℕ0, 𝑀, 1) + 𝐾)) |
5 | 3, 4 | oveq12d 7293 |
. . . . . 6
⊢ (𝑀 = if(𝑀 ∈ ℕ0, 𝑀, 1) → (𝑀↑(𝑀 + 𝐾)) = (if(𝑀 ∈ ℕ0, 𝑀, 1)↑(if(𝑀 ∈ ℕ0, 𝑀, 1) + 𝐾))) |
6 | 5 | oveq2d 7291 |
. . . . 5
⊢ (𝑀 = if(𝑀 ∈ ℕ0, 𝑀, 1) → ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) = ((2↑(𝐾↑2)) · (if(𝑀 ∈ ℕ0, 𝑀, 1)↑(if(𝑀 ∈ ℕ0, 𝑀, 1) + 𝐾)))) |
7 | 6 | oveq1d 7290 |
. . . 4
⊢ (𝑀 = if(𝑀 ∈ ℕ0, 𝑀, 1) → (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) = (((2↑(𝐾↑2)) · (if(𝑀 ∈ ℕ0, 𝑀, 1)↑(if(𝑀 ∈ ℕ0, 𝑀, 1) + 𝐾))) · (!‘(𝑁 − 1)))) |
8 | 2, 7 | breq12d 5087 |
. . 3
⊢ (𝑀 = if(𝑀 ∈ ℕ0, 𝑀, 1) → ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) ↔ (((𝑁 − 1)↑𝐾) · (if(𝑀 ∈ ℕ0, 𝑀, 1)↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑(if(𝑀 ∈ ℕ0,
𝑀, 1) + 𝐾))) · (!‘(𝑁 − 1))))) |
9 | | oveq1 7282 |
. . . . 5
⊢ (𝑀 = if(𝑀 ∈ ℕ0, 𝑀, 1) → (𝑀↑𝑁) = (if(𝑀 ∈ ℕ0, 𝑀, 1)↑𝑁)) |
10 | 9 | oveq2d 7291 |
. . . 4
⊢ (𝑀 = if(𝑀 ∈ ℕ0, 𝑀, 1) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) = ((𝑁↑(𝐾 + 1)) · (if(𝑀 ∈ ℕ0, 𝑀, 1)↑𝑁))) |
11 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑀 = if(𝑀 ∈ ℕ0, 𝑀, 1) → (𝑀 + (𝐾 + 1)) = (if(𝑀 ∈ ℕ0, 𝑀, 1) + (𝐾 + 1))) |
12 | 3, 11 | oveq12d 7293 |
. . . . . 6
⊢ (𝑀 = if(𝑀 ∈ ℕ0, 𝑀, 1) → (𝑀↑(𝑀 + (𝐾 + 1))) = (if(𝑀 ∈ ℕ0, 𝑀, 1)↑(if(𝑀 ∈ ℕ0, 𝑀, 1) + (𝐾 + 1)))) |
13 | 12 | oveq2d 7291 |
. . . . 5
⊢ (𝑀 = if(𝑀 ∈ ℕ0, 𝑀, 1) → ((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) = ((2↑((𝐾 + 1)↑2)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑(if(𝑀 ∈ ℕ0,
𝑀, 1) + (𝐾 + 1))))) |
14 | 13 | oveq1d 7290 |
. . . 4
⊢ (𝑀 = if(𝑀 ∈ ℕ0, 𝑀, 1) → (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) = (((2↑((𝐾 + 1)↑2)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑(if(𝑀 ∈ ℕ0,
𝑀, 1) + (𝐾 + 1)))) · (!‘𝑁))) |
15 | 10, 14 | breq12d 5087 |
. . 3
⊢ (𝑀 = if(𝑀 ∈ ℕ0, 𝑀, 1) → (((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)) ↔ ((𝑁↑(𝐾 + 1)) · (if(𝑀 ∈ ℕ0, 𝑀, 1)↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑(if(𝑀 ∈ ℕ0,
𝑀, 1) + (𝐾 + 1)))) · (!‘𝑁)))) |
16 | 8, 15 | imbi12d 345 |
. 2
⊢ (𝑀 = if(𝑀 ∈ ℕ0, 𝑀, 1) → (((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁))) ↔ ((((𝑁 − 1)↑𝐾) · (if(𝑀 ∈ ℕ0, 𝑀, 1)↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑(if(𝑀 ∈ ℕ0,
𝑀, 1) + 𝐾))) · (!‘(𝑁 − 1))) → ((𝑁↑(𝐾 + 1)) · (if(𝑀 ∈ ℕ0, 𝑀, 1)↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑(if(𝑀 ∈ ℕ0,
𝑀, 1) + (𝐾 + 1)))) · (!‘𝑁))))) |
17 | | oveq2 7283 |
. . . . 5
⊢ (𝐾 = if(𝐾 ∈ ℕ0, 𝐾, 1) → ((𝑁 − 1)↑𝐾) = ((𝑁 − 1)↑if(𝐾 ∈ ℕ0, 𝐾, 1))) |
18 | 17 | oveq1d 7290 |
. . . 4
⊢ (𝐾 = if(𝐾 ∈ ℕ0, 𝐾, 1) → (((𝑁 − 1)↑𝐾) · (if(𝑀 ∈ ℕ0, 𝑀, 1)↑(𝑁 − 1))) = (((𝑁 − 1)↑if(𝐾 ∈ ℕ0, 𝐾, 1)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑(𝑁 − 1)))) |
19 | | oveq1 7282 |
. . . . . . 7
⊢ (𝐾 = if(𝐾 ∈ ℕ0, 𝐾, 1) → (𝐾↑2) = (if(𝐾 ∈ ℕ0, 𝐾, 1)↑2)) |
20 | 19 | oveq2d 7291 |
. . . . . 6
⊢ (𝐾 = if(𝐾 ∈ ℕ0, 𝐾, 1) → (2↑(𝐾↑2)) = (2↑(if(𝐾 ∈ ℕ0,
𝐾,
1)↑2))) |
21 | | oveq2 7283 |
. . . . . . 7
⊢ (𝐾 = if(𝐾 ∈ ℕ0, 𝐾, 1) → (if(𝑀 ∈ ℕ0,
𝑀, 1) + 𝐾) = (if(𝑀 ∈ ℕ0, 𝑀, 1) + if(𝐾 ∈ ℕ0, 𝐾, 1))) |
22 | 21 | oveq2d 7291 |
. . . . . 6
⊢ (𝐾 = if(𝐾 ∈ ℕ0, 𝐾, 1) → (if(𝑀 ∈ ℕ0,
𝑀, 1)↑(if(𝑀 ∈ ℕ0,
𝑀, 1) + 𝐾)) = (if(𝑀 ∈ ℕ0, 𝑀, 1)↑(if(𝑀 ∈ ℕ0, 𝑀, 1) + if(𝐾 ∈ ℕ0, 𝐾, 1)))) |
23 | 20, 22 | oveq12d 7293 |
. . . . 5
⊢ (𝐾 = if(𝐾 ∈ ℕ0, 𝐾, 1) → ((2↑(𝐾↑2)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑(if(𝑀 ∈ ℕ0,
𝑀, 1) + 𝐾))) = ((2↑(if(𝐾 ∈ ℕ0, 𝐾, 1)↑2)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑(if(𝑀 ∈ ℕ0,
𝑀, 1) + if(𝐾 ∈ ℕ0,
𝐾, 1))))) |
24 | 23 | oveq1d 7290 |
. . . 4
⊢ (𝐾 = if(𝐾 ∈ ℕ0, 𝐾, 1) → (((2↑(𝐾↑2)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑(if(𝑀 ∈ ℕ0,
𝑀, 1) + 𝐾))) · (!‘(𝑁 − 1))) = (((2↑(if(𝐾 ∈ ℕ0,
𝐾, 1)↑2)) ·
(if(𝑀 ∈
ℕ0, 𝑀,
1)↑(if(𝑀 ∈
ℕ0, 𝑀, 1)
+ if(𝐾 ∈
ℕ0, 𝐾,
1)))) · (!‘(𝑁
− 1)))) |
25 | 18, 24 | breq12d 5087 |
. . 3
⊢ (𝐾 = if(𝐾 ∈ ℕ0, 𝐾, 1) → ((((𝑁 − 1)↑𝐾) · (if(𝑀 ∈ ℕ0, 𝑀, 1)↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑(if(𝑀 ∈ ℕ0,
𝑀, 1) + 𝐾))) · (!‘(𝑁 − 1))) ↔ (((𝑁 − 1)↑if(𝐾 ∈ ℕ0, 𝐾, 1)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑(𝑁 − 1))) ≤
(((2↑(if(𝐾 ∈
ℕ0, 𝐾,
1)↑2)) · (if(𝑀
∈ ℕ0, 𝑀, 1)↑(if(𝑀 ∈ ℕ0, 𝑀, 1) + if(𝐾 ∈ ℕ0, 𝐾, 1)))) · (!‘(𝑁 − 1))))) |
26 | | oveq1 7282 |
. . . . . 6
⊢ (𝐾 = if(𝐾 ∈ ℕ0, 𝐾, 1) → (𝐾 + 1) = (if(𝐾 ∈ ℕ0, 𝐾, 1) + 1)) |
27 | 26 | oveq2d 7291 |
. . . . 5
⊢ (𝐾 = if(𝐾 ∈ ℕ0, 𝐾, 1) → (𝑁↑(𝐾 + 1)) = (𝑁↑(if(𝐾 ∈ ℕ0, 𝐾, 1) + 1))) |
28 | 27 | oveq1d 7290 |
. . . 4
⊢ (𝐾 = if(𝐾 ∈ ℕ0, 𝐾, 1) → ((𝑁↑(𝐾 + 1)) · (if(𝑀 ∈ ℕ0, 𝑀, 1)↑𝑁)) = ((𝑁↑(if(𝐾 ∈ ℕ0, 𝐾, 1) + 1)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑𝑁))) |
29 | 26 | oveq1d 7290 |
. . . . . . 7
⊢ (𝐾 = if(𝐾 ∈ ℕ0, 𝐾, 1) → ((𝐾 + 1)↑2) = ((if(𝐾 ∈ ℕ0, 𝐾, 1) +
1)↑2)) |
30 | 29 | oveq2d 7291 |
. . . . . 6
⊢ (𝐾 = if(𝐾 ∈ ℕ0, 𝐾, 1) → (2↑((𝐾 + 1)↑2)) =
(2↑((if(𝐾 ∈
ℕ0, 𝐾, 1)
+ 1)↑2))) |
31 | 26 | oveq2d 7291 |
. . . . . . 7
⊢ (𝐾 = if(𝐾 ∈ ℕ0, 𝐾, 1) → (if(𝑀 ∈ ℕ0,
𝑀, 1) + (𝐾 + 1)) = (if(𝑀 ∈ ℕ0, 𝑀, 1) + (if(𝐾 ∈ ℕ0, 𝐾, 1) + 1))) |
32 | 31 | oveq2d 7291 |
. . . . . 6
⊢ (𝐾 = if(𝐾 ∈ ℕ0, 𝐾, 1) → (if(𝑀 ∈ ℕ0,
𝑀, 1)↑(if(𝑀 ∈ ℕ0,
𝑀, 1) + (𝐾 + 1))) = (if(𝑀 ∈ ℕ0, 𝑀, 1)↑(if(𝑀 ∈ ℕ0, 𝑀, 1) + (if(𝐾 ∈ ℕ0, 𝐾, 1) + 1)))) |
33 | 30, 32 | oveq12d 7293 |
. . . . 5
⊢ (𝐾 = if(𝐾 ∈ ℕ0, 𝐾, 1) → ((2↑((𝐾 + 1)↑2)) ·
(if(𝑀 ∈
ℕ0, 𝑀,
1)↑(if(𝑀 ∈
ℕ0, 𝑀, 1)
+ (𝐾 + 1)))) =
((2↑((if(𝐾 ∈
ℕ0, 𝐾, 1)
+ 1)↑2)) · (if(𝑀 ∈ ℕ0, 𝑀, 1)↑(if(𝑀 ∈ ℕ0, 𝑀, 1) + (if(𝐾 ∈ ℕ0, 𝐾, 1) + 1))))) |
34 | 33 | oveq1d 7290 |
. . . 4
⊢ (𝐾 = if(𝐾 ∈ ℕ0, 𝐾, 1) → (((2↑((𝐾 + 1)↑2)) ·
(if(𝑀 ∈
ℕ0, 𝑀,
1)↑(if(𝑀 ∈
ℕ0, 𝑀, 1)
+ (𝐾 + 1)))) ·
(!‘𝑁)) =
(((2↑((if(𝐾 ∈
ℕ0, 𝐾, 1)
+ 1)↑2)) · (if(𝑀 ∈ ℕ0, 𝑀, 1)↑(if(𝑀 ∈ ℕ0, 𝑀, 1) + (if(𝐾 ∈ ℕ0, 𝐾, 1) + 1)))) ·
(!‘𝑁))) |
35 | 28, 34 | breq12d 5087 |
. . 3
⊢ (𝐾 = if(𝐾 ∈ ℕ0, 𝐾, 1) → (((𝑁↑(𝐾 + 1)) · (if(𝑀 ∈ ℕ0, 𝑀, 1)↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑(if(𝑀 ∈ ℕ0,
𝑀, 1) + (𝐾 + 1)))) · (!‘𝑁)) ↔ ((𝑁↑(if(𝐾 ∈ ℕ0, 𝐾, 1) + 1)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑𝑁)) ≤ (((2↑((if(𝐾 ∈ ℕ0,
𝐾, 1) + 1)↑2))
· (if(𝑀 ∈
ℕ0, 𝑀,
1)↑(if(𝑀 ∈
ℕ0, 𝑀, 1)
+ (if(𝐾 ∈
ℕ0, 𝐾, 1)
+ 1)))) · (!‘𝑁)))) |
36 | 25, 35 | imbi12d 345 |
. 2
⊢ (𝐾 = if(𝐾 ∈ ℕ0, 𝐾, 1) → (((((𝑁 − 1)↑𝐾) · (if(𝑀 ∈ ℕ0, 𝑀, 1)↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑(if(𝑀 ∈ ℕ0,
𝑀, 1) + 𝐾))) · (!‘(𝑁 − 1))) → ((𝑁↑(𝐾 + 1)) · (if(𝑀 ∈ ℕ0, 𝑀, 1)↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑(if(𝑀 ∈ ℕ0,
𝑀, 1) + (𝐾 + 1)))) · (!‘𝑁))) ↔ ((((𝑁 − 1)↑if(𝐾 ∈ ℕ0, 𝐾, 1)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑(𝑁 − 1))) ≤
(((2↑(if(𝐾 ∈
ℕ0, 𝐾,
1)↑2)) · (if(𝑀
∈ ℕ0, 𝑀, 1)↑(if(𝑀 ∈ ℕ0, 𝑀, 1) + if(𝐾 ∈ ℕ0, 𝐾, 1)))) · (!‘(𝑁 − 1))) → ((𝑁↑(if(𝐾 ∈ ℕ0, 𝐾, 1) + 1)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑𝑁)) ≤ (((2↑((if(𝐾 ∈ ℕ0,
𝐾, 1) + 1)↑2))
· (if(𝑀 ∈
ℕ0, 𝑀,
1)↑(if(𝑀 ∈
ℕ0, 𝑀, 1)
+ (if(𝐾 ∈
ℕ0, 𝐾, 1)
+ 1)))) · (!‘𝑁))))) |
37 | | oveq1 7282 |
. . . . . 6
⊢ (𝑁 = if(𝑁 ∈ ℕ, 𝑁, 1) → (𝑁 − 1) = (if(𝑁 ∈ ℕ, 𝑁, 1) − 1)) |
38 | 37 | oveq1d 7290 |
. . . . 5
⊢ (𝑁 = if(𝑁 ∈ ℕ, 𝑁, 1) → ((𝑁 − 1)↑if(𝐾 ∈ ℕ0, 𝐾, 1)) = ((if(𝑁 ∈ ℕ, 𝑁, 1) − 1)↑if(𝐾 ∈ ℕ0, 𝐾, 1))) |
39 | 37 | oveq2d 7291 |
. . . . 5
⊢ (𝑁 = if(𝑁 ∈ ℕ, 𝑁, 1) → (if(𝑀 ∈ ℕ0, 𝑀, 1)↑(𝑁 − 1)) = (if(𝑀 ∈ ℕ0, 𝑀, 1)↑(if(𝑁 ∈ ℕ, 𝑁, 1) − 1))) |
40 | 38, 39 | oveq12d 7293 |
. . . 4
⊢ (𝑁 = if(𝑁 ∈ ℕ, 𝑁, 1) → (((𝑁 − 1)↑if(𝐾 ∈ ℕ0, 𝐾, 1)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑(𝑁 − 1))) = (((if(𝑁 ∈ ℕ, 𝑁, 1) − 1)↑if(𝐾 ∈ ℕ0,
𝐾, 1)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑(if(𝑁 ∈ ℕ, 𝑁, 1) −
1)))) |
41 | | fvoveq1 7298 |
. . . . 5
⊢ (𝑁 = if(𝑁 ∈ ℕ, 𝑁, 1) → (!‘(𝑁 − 1)) = (!‘(if(𝑁 ∈ ℕ, 𝑁, 1) −
1))) |
42 | 41 | oveq2d 7291 |
. . . 4
⊢ (𝑁 = if(𝑁 ∈ ℕ, 𝑁, 1) → (((2↑(if(𝐾 ∈ ℕ0, 𝐾, 1)↑2)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑(if(𝑀 ∈ ℕ0,
𝑀, 1) + if(𝐾 ∈ ℕ0,
𝐾, 1)))) ·
(!‘(𝑁 − 1))) =
(((2↑(if(𝐾 ∈
ℕ0, 𝐾,
1)↑2)) · (if(𝑀
∈ ℕ0, 𝑀, 1)↑(if(𝑀 ∈ ℕ0, 𝑀, 1) + if(𝐾 ∈ ℕ0, 𝐾, 1)))) ·
(!‘(if(𝑁 ∈
ℕ, 𝑁, 1) −
1)))) |
43 | 40, 42 | breq12d 5087 |
. . 3
⊢ (𝑁 = if(𝑁 ∈ ℕ, 𝑁, 1) → ((((𝑁 − 1)↑if(𝐾 ∈ ℕ0, 𝐾, 1)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑(𝑁 − 1))) ≤
(((2↑(if(𝐾 ∈
ℕ0, 𝐾,
1)↑2)) · (if(𝑀
∈ ℕ0, 𝑀, 1)↑(if(𝑀 ∈ ℕ0, 𝑀, 1) + if(𝐾 ∈ ℕ0, 𝐾, 1)))) · (!‘(𝑁 − 1))) ↔ (((if(𝑁 ∈ ℕ, 𝑁, 1) − 1)↑if(𝐾 ∈ ℕ0,
𝐾, 1)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑(if(𝑁 ∈ ℕ, 𝑁, 1) − 1))) ≤
(((2↑(if(𝐾 ∈
ℕ0, 𝐾,
1)↑2)) · (if(𝑀
∈ ℕ0, 𝑀, 1)↑(if(𝑀 ∈ ℕ0, 𝑀, 1) + if(𝐾 ∈ ℕ0, 𝐾, 1)))) ·
(!‘(if(𝑁 ∈
ℕ, 𝑁, 1) −
1))))) |
44 | | oveq1 7282 |
. . . . 5
⊢ (𝑁 = if(𝑁 ∈ ℕ, 𝑁, 1) → (𝑁↑(if(𝐾 ∈ ℕ0, 𝐾, 1) + 1)) = (if(𝑁 ∈ ℕ, 𝑁, 1)↑(if(𝐾 ∈ ℕ0, 𝐾, 1) + 1))) |
45 | | oveq2 7283 |
. . . . 5
⊢ (𝑁 = if(𝑁 ∈ ℕ, 𝑁, 1) → (if(𝑀 ∈ ℕ0, 𝑀, 1)↑𝑁) = (if(𝑀 ∈ ℕ0, 𝑀, 1)↑if(𝑁 ∈ ℕ, 𝑁, 1))) |
46 | 44, 45 | oveq12d 7293 |
. . . 4
⊢ (𝑁 = if(𝑁 ∈ ℕ, 𝑁, 1) → ((𝑁↑(if(𝐾 ∈ ℕ0, 𝐾, 1) + 1)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑𝑁)) = ((if(𝑁 ∈ ℕ, 𝑁, 1)↑(if(𝐾 ∈ ℕ0, 𝐾, 1) + 1)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑if(𝑁 ∈ ℕ, 𝑁, 1)))) |
47 | | fveq2 6774 |
. . . . 5
⊢ (𝑁 = if(𝑁 ∈ ℕ, 𝑁, 1) → (!‘𝑁) = (!‘if(𝑁 ∈ ℕ, 𝑁, 1))) |
48 | 47 | oveq2d 7291 |
. . . 4
⊢ (𝑁 = if(𝑁 ∈ ℕ, 𝑁, 1) → (((2↑((if(𝐾 ∈ ℕ0, 𝐾, 1) + 1)↑2)) ·
(if(𝑀 ∈
ℕ0, 𝑀,
1)↑(if(𝑀 ∈
ℕ0, 𝑀, 1)
+ (if(𝐾 ∈
ℕ0, 𝐾, 1)
+ 1)))) · (!‘𝑁)) = (((2↑((if(𝐾 ∈ ℕ0, 𝐾, 1) + 1)↑2)) ·
(if(𝑀 ∈
ℕ0, 𝑀,
1)↑(if(𝑀 ∈
ℕ0, 𝑀, 1)
+ (if(𝐾 ∈
ℕ0, 𝐾, 1)
+ 1)))) · (!‘if(𝑁 ∈ ℕ, 𝑁, 1)))) |
49 | 46, 48 | breq12d 5087 |
. . 3
⊢ (𝑁 = if(𝑁 ∈ ℕ, 𝑁, 1) → (((𝑁↑(if(𝐾 ∈ ℕ0, 𝐾, 1) + 1)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑𝑁)) ≤ (((2↑((if(𝐾 ∈ ℕ0,
𝐾, 1) + 1)↑2))
· (if(𝑀 ∈
ℕ0, 𝑀,
1)↑(if(𝑀 ∈
ℕ0, 𝑀, 1)
+ (if(𝐾 ∈
ℕ0, 𝐾, 1)
+ 1)))) · (!‘𝑁)) ↔ ((if(𝑁 ∈ ℕ, 𝑁, 1)↑(if(𝐾 ∈ ℕ0, 𝐾, 1) + 1)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑if(𝑁 ∈ ℕ, 𝑁, 1))) ≤ (((2↑((if(𝐾 ∈ ℕ0,
𝐾, 1) + 1)↑2))
· (if(𝑀 ∈
ℕ0, 𝑀,
1)↑(if(𝑀 ∈
ℕ0, 𝑀, 1)
+ (if(𝐾 ∈
ℕ0, 𝐾, 1)
+ 1)))) · (!‘if(𝑁 ∈ ℕ, 𝑁, 1))))) |
50 | 43, 49 | imbi12d 345 |
. 2
⊢ (𝑁 = if(𝑁 ∈ ℕ, 𝑁, 1) → (((((𝑁 − 1)↑if(𝐾 ∈ ℕ0, 𝐾, 1)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑(𝑁 − 1))) ≤
(((2↑(if(𝐾 ∈
ℕ0, 𝐾,
1)↑2)) · (if(𝑀
∈ ℕ0, 𝑀, 1)↑(if(𝑀 ∈ ℕ0, 𝑀, 1) + if(𝐾 ∈ ℕ0, 𝐾, 1)))) · (!‘(𝑁 − 1))) → ((𝑁↑(if(𝐾 ∈ ℕ0, 𝐾, 1) + 1)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑𝑁)) ≤ (((2↑((if(𝐾 ∈ ℕ0,
𝐾, 1) + 1)↑2))
· (if(𝑀 ∈
ℕ0, 𝑀,
1)↑(if(𝑀 ∈
ℕ0, 𝑀, 1)
+ (if(𝐾 ∈
ℕ0, 𝐾, 1)
+ 1)))) · (!‘𝑁))) ↔ ((((if(𝑁 ∈ ℕ, 𝑁, 1) − 1)↑if(𝐾 ∈ ℕ0, 𝐾, 1)) · (if(𝑀 ∈ ℕ0,
𝑀, 1)↑(if(𝑁 ∈ ℕ, 𝑁, 1) − 1))) ≤
(((2↑(if(𝐾 ∈
ℕ0, 𝐾,
1)↑2)) · (if(𝑀
∈ ℕ0, 𝑀, 1)↑(if(𝑀 ∈ ℕ0, 𝑀, 1) + if(𝐾 ∈ ℕ0, 𝐾, 1)))) ·
(!‘(if(𝑁 ∈
ℕ, 𝑁, 1) − 1)))
→ ((if(𝑁 ∈
ℕ, 𝑁,
1)↑(if(𝐾 ∈
ℕ0, 𝐾, 1)
+ 1)) · (if(𝑀 ∈
ℕ0, 𝑀,
1)↑if(𝑁 ∈
ℕ, 𝑁, 1))) ≤
(((2↑((if(𝐾 ∈
ℕ0, 𝐾, 1)
+ 1)↑2)) · (if(𝑀 ∈ ℕ0, 𝑀, 1)↑(if(𝑀 ∈ ℕ0, 𝑀, 1) + (if(𝐾 ∈ ℕ0, 𝐾, 1) + 1)))) ·
(!‘if(𝑁 ∈
ℕ, 𝑁,
1)))))) |
51 | | 1nn 11984 |
. . . 4
⊢ 1 ∈
ℕ |
52 | 51 | elimel 4528 |
. . 3
⊢ if(𝑁 ∈ ℕ, 𝑁, 1) ∈
ℕ |
53 | | 1nn0 12249 |
. . . 4
⊢ 1 ∈
ℕ0 |
54 | 53 | elimel 4528 |
. . 3
⊢ if(𝐾 ∈ ℕ0,
𝐾, 1) ∈
ℕ0 |
55 | 53 | elimel 4528 |
. . 3
⊢ if(𝑀 ∈ ℕ0,
𝑀, 1) ∈
ℕ0 |
56 | 52, 54, 55 | faclbnd4lem1 14007 |
. 2
⊢
((((if(𝑁 ∈
ℕ, 𝑁, 1) −
1)↑if(𝐾 ∈
ℕ0, 𝐾, 1))
· (if(𝑀 ∈
ℕ0, 𝑀,
1)↑(if(𝑁 ∈
ℕ, 𝑁, 1) − 1)))
≤ (((2↑(if(𝐾 ∈
ℕ0, 𝐾,
1)↑2)) · (if(𝑀
∈ ℕ0, 𝑀, 1)↑(if(𝑀 ∈ ℕ0, 𝑀, 1) + if(𝐾 ∈ ℕ0, 𝐾, 1)))) ·
(!‘(if(𝑁 ∈
ℕ, 𝑁, 1) − 1)))
→ ((if(𝑁 ∈
ℕ, 𝑁,
1)↑(if(𝐾 ∈
ℕ0, 𝐾, 1)
+ 1)) · (if(𝑀 ∈
ℕ0, 𝑀,
1)↑if(𝑁 ∈
ℕ, 𝑁, 1))) ≤
(((2↑((if(𝐾 ∈
ℕ0, 𝐾, 1)
+ 1)↑2)) · (if(𝑀 ∈ ℕ0, 𝑀, 1)↑(if(𝑀 ∈ ℕ0, 𝑀, 1) + (if(𝐾 ∈ ℕ0, 𝐾, 1) + 1)))) ·
(!‘if(𝑁 ∈
ℕ, 𝑁,
1)))) |
57 | 16, 36, 50, 56 | dedth3h 4519 |
1
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ) → ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)))) |