| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq1 7438 | . . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → (𝑛↑𝑗) = (𝑚↑𝑗)) | 
| 2 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → (𝑀↑𝑛) = (𝑀↑𝑚)) | 
| 3 | 1, 2 | oveq12d 7449 | . . . . . . . . . 10
⊢ (𝑛 = 𝑚 → ((𝑛↑𝑗) · (𝑀↑𝑛)) = ((𝑚↑𝑗) · (𝑀↑𝑚))) | 
| 4 |  | fveq2 6906 | . . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → (!‘𝑛) = (!‘𝑚)) | 
| 5 | 4 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘𝑛)) = (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘𝑚))) | 
| 6 | 3, 5 | breq12d 5156 | . . . . . . . . 9
⊢ (𝑛 = 𝑚 → (((𝑛↑𝑗) · (𝑀↑𝑛)) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘𝑛)) ↔ ((𝑚↑𝑗) · (𝑀↑𝑚)) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘𝑚)))) | 
| 7 | 6 | cbvralvw 3237 | . . . . . . . 8
⊢
(∀𝑛 ∈
ℕ ((𝑛↑𝑗) · (𝑀↑𝑛)) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘𝑛)) ↔ ∀𝑚 ∈ ℕ ((𝑚↑𝑗) · (𝑀↑𝑚)) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘𝑚))) | 
| 8 |  | nnre 12273 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ) | 
| 9 |  | 1re 11261 | . . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ | 
| 10 |  | lelttric 11368 | . . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℝ ∧ 1 ∈
ℝ) → (𝑛 ≤ 1
∨ 1 < 𝑛)) | 
| 11 | 8, 9, 10 | sylancl 586 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (𝑛 ≤ 1 ∨ 1 < 𝑛)) | 
| 12 | 11 | ancli 548 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (𝑛 ∈ ℕ ∧ (𝑛 ≤ 1 ∨ 1 < 𝑛))) | 
| 13 |  | andi 1010 | . . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ ∧ (𝑛 ≤ 1 ∨ 1 < 𝑛)) ↔ ((𝑛 ∈ ℕ ∧ 𝑛 ≤ 1) ∨ (𝑛 ∈ ℕ ∧ 1 < 𝑛))) | 
| 14 | 12, 13 | sylib 218 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → ((𝑛 ∈ ℕ ∧ 𝑛 ≤ 1) ∨ (𝑛 ∈ ℕ ∧ 1 <
𝑛))) | 
| 15 |  | nnge1 12294 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → 1 ≤
𝑛) | 
| 16 |  | letri3 11346 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ ℝ ∧ 1 ∈
ℝ) → (𝑛 = 1
↔ (𝑛 ≤ 1 ∧ 1
≤ 𝑛))) | 
| 17 | 8, 9, 16 | sylancl 586 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → (𝑛 = 1 ↔ (𝑛 ≤ 1 ∧ 1 ≤ 𝑛))) | 
| 18 | 17 | biimpar 477 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℕ ∧ (𝑛 ≤ 1 ∧ 1 ≤ 𝑛)) → 𝑛 = 1) | 
| 19 | 18 | anassrs 467 | . . . . . . . . . . . . . . . 16
⊢ (((𝑛 ∈ ℕ ∧ 𝑛 ≤ 1) ∧ 1 ≤ 𝑛) → 𝑛 = 1) | 
| 20 | 15, 19 | mpidan 689 | . . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℕ ∧ 𝑛 ≤ 1) → 𝑛 = 1) | 
| 21 |  | oveq1 7438 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 = 1 → (𝑛 − 1) = (1 − 1)) | 
| 22 |  | 1m1e0 12338 | . . . . . . . . . . . . . . . 16
⊢ (1
− 1) = 0 | 
| 23 | 21, 22 | eqtrdi 2793 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = 1 → (𝑛 − 1) = 0) | 
| 24 | 20, 23 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ∧ 𝑛 ≤ 1) → (𝑛 − 1) =
0) | 
| 25 |  | faclbnd4lem3 14334 | . . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ0
∧ 𝑗 ∈
ℕ0) ∧ (𝑛 − 1) = 0) → (((𝑛 − 1)↑𝑗) · (𝑀↑(𝑛 − 1))) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘(𝑛 − 1)))) | 
| 26 | 24, 25 | sylan2 593 | . . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ0
∧ 𝑗 ∈
ℕ0) ∧ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 1)) → (((𝑛 − 1)↑𝑗) · (𝑀↑(𝑛 − 1))) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘(𝑛 − 1)))) | 
| 27 | 26 | a1d 25 | . . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ0
∧ 𝑗 ∈
ℕ0) ∧ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 1)) → (∀𝑚 ∈ ℕ ((𝑚↑𝑗) · (𝑀↑𝑚)) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘𝑚)) → (((𝑛 − 1)↑𝑗) · (𝑀↑(𝑛 − 1))) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘(𝑛 − 1))))) | 
| 28 |  | 1nn 12277 | . . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℕ | 
| 29 |  | nnsub 12310 | . . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℕ ∧ 𝑛
∈ ℕ) → (1 < 𝑛 ↔ (𝑛 − 1) ∈ ℕ)) | 
| 30 | 28, 29 | mpan 690 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (1 <
𝑛 ↔ (𝑛 − 1) ∈
ℕ)) | 
| 31 | 30 | biimpa 476 | . . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ∧ 1 <
𝑛) → (𝑛 − 1) ∈
ℕ) | 
| 32 |  | oveq1 7438 | . . . . . . . . . . . . . . . . 17
⊢ (𝑚 = (𝑛 − 1) → (𝑚↑𝑗) = ((𝑛 − 1)↑𝑗)) | 
| 33 |  | oveq2 7439 | . . . . . . . . . . . . . . . . 17
⊢ (𝑚 = (𝑛 − 1) → (𝑀↑𝑚) = (𝑀↑(𝑛 − 1))) | 
| 34 | 32, 33 | oveq12d 7449 | . . . . . . . . . . . . . . . 16
⊢ (𝑚 = (𝑛 − 1) → ((𝑚↑𝑗) · (𝑀↑𝑚)) = (((𝑛 − 1)↑𝑗) · (𝑀↑(𝑛 − 1)))) | 
| 35 |  | fveq2 6906 | . . . . . . . . . . . . . . . . 17
⊢ (𝑚 = (𝑛 − 1) → (!‘𝑚) = (!‘(𝑛 − 1))) | 
| 36 | 35 | oveq2d 7447 | . . . . . . . . . . . . . . . 16
⊢ (𝑚 = (𝑛 − 1) → (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘𝑚)) = (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘(𝑛 − 1)))) | 
| 37 | 34, 36 | breq12d 5156 | . . . . . . . . . . . . . . 15
⊢ (𝑚 = (𝑛 − 1) → (((𝑚↑𝑗) · (𝑀↑𝑚)) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘𝑚)) ↔ (((𝑛 − 1)↑𝑗) · (𝑀↑(𝑛 − 1))) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘(𝑛 − 1))))) | 
| 38 | 37 | rspcv 3618 | . . . . . . . . . . . . . 14
⊢ ((𝑛 − 1) ∈ ℕ
→ (∀𝑚 ∈
ℕ ((𝑚↑𝑗) · (𝑀↑𝑚)) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘𝑚)) → (((𝑛 − 1)↑𝑗) · (𝑀↑(𝑛 − 1))) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘(𝑛 − 1))))) | 
| 39 | 31, 38 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ 1 <
𝑛) → (∀𝑚 ∈ ℕ ((𝑚↑𝑗) · (𝑀↑𝑚)) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘𝑚)) → (((𝑛 − 1)↑𝑗) · (𝑀↑(𝑛 − 1))) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘(𝑛 − 1))))) | 
| 40 | 39 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ0
∧ 𝑗 ∈
ℕ0) ∧ (𝑛 ∈ ℕ ∧ 1 < 𝑛)) → (∀𝑚 ∈ ℕ ((𝑚↑𝑗) · (𝑀↑𝑚)) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘𝑚)) → (((𝑛 − 1)↑𝑗) · (𝑀↑(𝑛 − 1))) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘(𝑛 − 1))))) | 
| 41 | 27, 40 | jaodan 960 | . . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ0
∧ 𝑗 ∈
ℕ0) ∧ ((𝑛 ∈ ℕ ∧ 𝑛 ≤ 1) ∨ (𝑛 ∈ ℕ ∧ 1 < 𝑛))) → (∀𝑚 ∈ ℕ ((𝑚↑𝑗) · (𝑀↑𝑚)) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘𝑚)) → (((𝑛 − 1)↑𝑗) · (𝑀↑(𝑛 − 1))) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘(𝑛 − 1))))) | 
| 42 | 14, 41 | sylan2 593 | . . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ0
∧ 𝑗 ∈
ℕ0) ∧ 𝑛 ∈ ℕ) → (∀𝑚 ∈ ℕ ((𝑚↑𝑗) · (𝑀↑𝑚)) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘𝑚)) → (((𝑛 − 1)↑𝑗) · (𝑀↑(𝑛 − 1))) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘(𝑛 − 1))))) | 
| 43 |  | faclbnd4lem2 14333 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ 𝑗 ∈
ℕ0 ∧ 𝑛
∈ ℕ) → ((((𝑛 − 1)↑𝑗) · (𝑀↑(𝑛 − 1))) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘(𝑛 − 1))) → ((𝑛↑(𝑗 + 1)) · (𝑀↑𝑛)) ≤ (((2↑((𝑗 + 1)↑2)) · (𝑀↑(𝑀 + (𝑗 + 1)))) · (!‘𝑛)))) | 
| 44 | 43 | 3expa 1119 | . . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ0
∧ 𝑗 ∈
ℕ0) ∧ 𝑛 ∈ ℕ) → ((((𝑛 − 1)↑𝑗) · (𝑀↑(𝑛 − 1))) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘(𝑛 − 1))) → ((𝑛↑(𝑗 + 1)) · (𝑀↑𝑛)) ≤ (((2↑((𝑗 + 1)↑2)) · (𝑀↑(𝑀 + (𝑗 + 1)))) · (!‘𝑛)))) | 
| 45 | 42, 44 | syld 47 | . . . . . . . . 9
⊢ (((𝑀 ∈ ℕ0
∧ 𝑗 ∈
ℕ0) ∧ 𝑛 ∈ ℕ) → (∀𝑚 ∈ ℕ ((𝑚↑𝑗) · (𝑀↑𝑚)) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘𝑚)) → ((𝑛↑(𝑗 + 1)) · (𝑀↑𝑛)) ≤ (((2↑((𝑗 + 1)↑2)) · (𝑀↑(𝑀 + (𝑗 + 1)))) · (!‘𝑛)))) | 
| 46 | 45 | ralrimdva 3154 | . . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝑗 ∈
ℕ0) → (∀𝑚 ∈ ℕ ((𝑚↑𝑗) · (𝑀↑𝑚)) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘𝑚)) → ∀𝑛 ∈ ℕ ((𝑛↑(𝑗 + 1)) · (𝑀↑𝑛)) ≤ (((2↑((𝑗 + 1)↑2)) · (𝑀↑(𝑀 + (𝑗 + 1)))) · (!‘𝑛)))) | 
| 47 | 7, 46 | biimtrid 242 | . . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑗 ∈
ℕ0) → (∀𝑛 ∈ ℕ ((𝑛↑𝑗) · (𝑀↑𝑛)) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘𝑛)) → ∀𝑛 ∈ ℕ ((𝑛↑(𝑗 + 1)) · (𝑀↑𝑛)) ≤ (((2↑((𝑗 + 1)↑2)) · (𝑀↑(𝑀 + (𝑗 + 1)))) · (!‘𝑛)))) | 
| 48 | 47 | expcom 413 | . . . . . 6
⊢ (𝑗 ∈ ℕ0
→ (𝑀 ∈
ℕ0 → (∀𝑛 ∈ ℕ ((𝑛↑𝑗) · (𝑀↑𝑛)) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘𝑛)) → ∀𝑛 ∈ ℕ ((𝑛↑(𝑗 + 1)) · (𝑀↑𝑛)) ≤ (((2↑((𝑗 + 1)↑2)) · (𝑀↑(𝑀 + (𝑗 + 1)))) · (!‘𝑛))))) | 
| 49 | 48 | a2d 29 | . . . . 5
⊢ (𝑗 ∈ ℕ0
→ ((𝑀 ∈
ℕ0 → ∀𝑛 ∈ ℕ ((𝑛↑𝑗) · (𝑀↑𝑛)) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘𝑛))) → (𝑀 ∈ ℕ0 →
∀𝑛 ∈ ℕ
((𝑛↑(𝑗 + 1)) · (𝑀↑𝑛)) ≤ (((2↑((𝑗 + 1)↑2)) · (𝑀↑(𝑀 + (𝑗 + 1)))) · (!‘𝑛))))) | 
| 50 |  | nnnn0 12533 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) | 
| 51 |  | faclbnd3 14331 | . . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → (𝑀↑𝑛) ≤ ((𝑀↑𝑀) · (!‘𝑛))) | 
| 52 | 50, 51 | sylan2 593 | . . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ (𝑀↑𝑛) ≤ ((𝑀↑𝑀) · (!‘𝑛))) | 
| 53 |  | nncn 12274 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) | 
| 54 | 53 | exp0d 14180 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (𝑛↑0) = 1) | 
| 55 | 54 | oveq1d 7446 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ → ((𝑛↑0) · (𝑀↑𝑛)) = (1 · (𝑀↑𝑛))) | 
| 56 | 55 | adantl 481 | . . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ ((𝑛↑0) ·
(𝑀↑𝑛)) = (1 · (𝑀↑𝑛))) | 
| 57 |  | nn0cn 12536 | . . . . . . . . . 10
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℂ) | 
| 58 |  | expcl 14120 | . . . . . . . . . 10
⊢ ((𝑀 ∈ ℂ ∧ 𝑛 ∈ ℕ0)
→ (𝑀↑𝑛) ∈
ℂ) | 
| 59 | 57, 50, 58 | syl2an 596 | . . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ (𝑀↑𝑛) ∈
ℂ) | 
| 60 | 59 | mullidd 11279 | . . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ (1 · (𝑀↑𝑛)) = (𝑀↑𝑛)) | 
| 61 | 56, 60 | eqtrd 2777 | . . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ ((𝑛↑0) ·
(𝑀↑𝑛)) = (𝑀↑𝑛)) | 
| 62 |  | sq0 14231 | . . . . . . . . . . . . . 14
⊢
(0↑2) = 0 | 
| 63 | 62 | oveq2i 7442 | . . . . . . . . . . . . 13
⊢
(2↑(0↑2)) = (2↑0) | 
| 64 |  | 2cn 12341 | . . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ | 
| 65 |  | exp0 14106 | . . . . . . . . . . . . . 14
⊢ (2 ∈
ℂ → (2↑0) = 1) | 
| 66 | 64, 65 | ax-mp 5 | . . . . . . . . . . . . 13
⊢
(2↑0) = 1 | 
| 67 | 63, 66 | eqtri 2765 | . . . . . . . . . . . 12
⊢
(2↑(0↑2)) = 1 | 
| 68 | 67 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ0
→ (2↑(0↑2)) = 1) | 
| 69 | 57 | addridd 11461 | . . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ0
→ (𝑀 + 0) = 𝑀) | 
| 70 | 69 | oveq2d 7447 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ0
→ (𝑀↑(𝑀 + 0)) = (𝑀↑𝑀)) | 
| 71 | 68, 70 | oveq12d 7449 | . . . . . . . . . 10
⊢ (𝑀 ∈ ℕ0
→ ((2↑(0↑2)) · (𝑀↑(𝑀 + 0))) = (1 · (𝑀↑𝑀))) | 
| 72 |  | expcl 14120 | . . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℂ ∧ 𝑀 ∈ ℕ0)
→ (𝑀↑𝑀) ∈
ℂ) | 
| 73 | 57, 72 | mpancom 688 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ0
→ (𝑀↑𝑀) ∈
ℂ) | 
| 74 | 73 | mullidd 11279 | . . . . . . . . . 10
⊢ (𝑀 ∈ ℕ0
→ (1 · (𝑀↑𝑀)) = (𝑀↑𝑀)) | 
| 75 | 71, 74 | eqtrd 2777 | . . . . . . . . 9
⊢ (𝑀 ∈ ℕ0
→ ((2↑(0↑2)) · (𝑀↑(𝑀 + 0))) = (𝑀↑𝑀)) | 
| 76 | 75 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑀 ∈ ℕ0
→ (((2↑(0↑2)) · (𝑀↑(𝑀 + 0))) · (!‘𝑛)) = ((𝑀↑𝑀) · (!‘𝑛))) | 
| 77 | 76 | adantr 480 | . . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ (((2↑(0↑2)) · (𝑀↑(𝑀 + 0))) · (!‘𝑛)) = ((𝑀↑𝑀) · (!‘𝑛))) | 
| 78 | 52, 61, 77 | 3brtr4d 5175 | . . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑛 ∈ ℕ)
→ ((𝑛↑0) ·
(𝑀↑𝑛)) ≤ (((2↑(0↑2)) · (𝑀↑(𝑀 + 0))) · (!‘𝑛))) | 
| 79 | 78 | ralrimiva 3146 | . . . . 5
⊢ (𝑀 ∈ ℕ0
→ ∀𝑛 ∈
ℕ ((𝑛↑0)
· (𝑀↑𝑛)) ≤ (((2↑(0↑2))
· (𝑀↑(𝑀 + 0))) · (!‘𝑛))) | 
| 80 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑚 = 0 → (𝑛↑𝑚) = (𝑛↑0)) | 
| 81 | 80 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑚 = 0 → ((𝑛↑𝑚) · (𝑀↑𝑛)) = ((𝑛↑0) · (𝑀↑𝑛))) | 
| 82 |  | oveq1 7438 | . . . . . . . . . . 11
⊢ (𝑚 = 0 → (𝑚↑2) = (0↑2)) | 
| 83 | 82 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑚 = 0 → (2↑(𝑚↑2)) =
(2↑(0↑2))) | 
| 84 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ (𝑚 = 0 → (𝑀 + 𝑚) = (𝑀 + 0)) | 
| 85 | 84 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑚 = 0 → (𝑀↑(𝑀 + 𝑚)) = (𝑀↑(𝑀 + 0))) | 
| 86 | 83, 85 | oveq12d 7449 | . . . . . . . . 9
⊢ (𝑚 = 0 → ((2↑(𝑚↑2)) · (𝑀↑(𝑀 + 𝑚))) = ((2↑(0↑2)) · (𝑀↑(𝑀 + 0)))) | 
| 87 | 86 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑚 = 0 → (((2↑(𝑚↑2)) · (𝑀↑(𝑀 + 𝑚))) · (!‘𝑛)) = (((2↑(0↑2)) · (𝑀↑(𝑀 + 0))) · (!‘𝑛))) | 
| 88 | 81, 87 | breq12d 5156 | . . . . . . 7
⊢ (𝑚 = 0 → (((𝑛↑𝑚) · (𝑀↑𝑛)) ≤ (((2↑(𝑚↑2)) · (𝑀↑(𝑀 + 𝑚))) · (!‘𝑛)) ↔ ((𝑛↑0) · (𝑀↑𝑛)) ≤ (((2↑(0↑2)) · (𝑀↑(𝑀 + 0))) · (!‘𝑛)))) | 
| 89 | 88 | ralbidv 3178 | . . . . . 6
⊢ (𝑚 = 0 → (∀𝑛 ∈ ℕ ((𝑛↑𝑚) · (𝑀↑𝑛)) ≤ (((2↑(𝑚↑2)) · (𝑀↑(𝑀 + 𝑚))) · (!‘𝑛)) ↔ ∀𝑛 ∈ ℕ ((𝑛↑0) · (𝑀↑𝑛)) ≤ (((2↑(0↑2)) · (𝑀↑(𝑀 + 0))) · (!‘𝑛)))) | 
| 90 | 89 | imbi2d 340 | . . . . 5
⊢ (𝑚 = 0 → ((𝑀 ∈ ℕ0 →
∀𝑛 ∈ ℕ
((𝑛↑𝑚) · (𝑀↑𝑛)) ≤ (((2↑(𝑚↑2)) · (𝑀↑(𝑀 + 𝑚))) · (!‘𝑛))) ↔ (𝑀 ∈ ℕ0 →
∀𝑛 ∈ ℕ
((𝑛↑0) · (𝑀↑𝑛)) ≤ (((2↑(0↑2)) · (𝑀↑(𝑀 + 0))) · (!‘𝑛))))) | 
| 91 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑚 = 𝑗 → (𝑛↑𝑚) = (𝑛↑𝑗)) | 
| 92 | 91 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑚 = 𝑗 → ((𝑛↑𝑚) · (𝑀↑𝑛)) = ((𝑛↑𝑗) · (𝑀↑𝑛))) | 
| 93 |  | oveq1 7438 | . . . . . . . . . . 11
⊢ (𝑚 = 𝑗 → (𝑚↑2) = (𝑗↑2)) | 
| 94 | 93 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑚 = 𝑗 → (2↑(𝑚↑2)) = (2↑(𝑗↑2))) | 
| 95 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ (𝑚 = 𝑗 → (𝑀 + 𝑚) = (𝑀 + 𝑗)) | 
| 96 | 95 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑚 = 𝑗 → (𝑀↑(𝑀 + 𝑚)) = (𝑀↑(𝑀 + 𝑗))) | 
| 97 | 94, 96 | oveq12d 7449 | . . . . . . . . 9
⊢ (𝑚 = 𝑗 → ((2↑(𝑚↑2)) · (𝑀↑(𝑀 + 𝑚))) = ((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗)))) | 
| 98 | 97 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑚 = 𝑗 → (((2↑(𝑚↑2)) · (𝑀↑(𝑀 + 𝑚))) · (!‘𝑛)) = (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘𝑛))) | 
| 99 | 92, 98 | breq12d 5156 | . . . . . . 7
⊢ (𝑚 = 𝑗 → (((𝑛↑𝑚) · (𝑀↑𝑛)) ≤ (((2↑(𝑚↑2)) · (𝑀↑(𝑀 + 𝑚))) · (!‘𝑛)) ↔ ((𝑛↑𝑗) · (𝑀↑𝑛)) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘𝑛)))) | 
| 100 | 99 | ralbidv 3178 | . . . . . 6
⊢ (𝑚 = 𝑗 → (∀𝑛 ∈ ℕ ((𝑛↑𝑚) · (𝑀↑𝑛)) ≤ (((2↑(𝑚↑2)) · (𝑀↑(𝑀 + 𝑚))) · (!‘𝑛)) ↔ ∀𝑛 ∈ ℕ ((𝑛↑𝑗) · (𝑀↑𝑛)) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘𝑛)))) | 
| 101 | 100 | imbi2d 340 | . . . . 5
⊢ (𝑚 = 𝑗 → ((𝑀 ∈ ℕ0 →
∀𝑛 ∈ ℕ
((𝑛↑𝑚) · (𝑀↑𝑛)) ≤ (((2↑(𝑚↑2)) · (𝑀↑(𝑀 + 𝑚))) · (!‘𝑛))) ↔ (𝑀 ∈ ℕ0 →
∀𝑛 ∈ ℕ
((𝑛↑𝑗) · (𝑀↑𝑛)) ≤ (((2↑(𝑗↑2)) · (𝑀↑(𝑀 + 𝑗))) · (!‘𝑛))))) | 
| 102 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑚 = (𝑗 + 1) → (𝑛↑𝑚) = (𝑛↑(𝑗 + 1))) | 
| 103 | 102 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑚 = (𝑗 + 1) → ((𝑛↑𝑚) · (𝑀↑𝑛)) = ((𝑛↑(𝑗 + 1)) · (𝑀↑𝑛))) | 
| 104 |  | oveq1 7438 | . . . . . . . . . . 11
⊢ (𝑚 = (𝑗 + 1) → (𝑚↑2) = ((𝑗 + 1)↑2)) | 
| 105 | 104 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑚 = (𝑗 + 1) → (2↑(𝑚↑2)) = (2↑((𝑗 + 1)↑2))) | 
| 106 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ (𝑚 = (𝑗 + 1) → (𝑀 + 𝑚) = (𝑀 + (𝑗 + 1))) | 
| 107 | 106 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑚 = (𝑗 + 1) → (𝑀↑(𝑀 + 𝑚)) = (𝑀↑(𝑀 + (𝑗 + 1)))) | 
| 108 | 105, 107 | oveq12d 7449 | . . . . . . . . 9
⊢ (𝑚 = (𝑗 + 1) → ((2↑(𝑚↑2)) · (𝑀↑(𝑀 + 𝑚))) = ((2↑((𝑗 + 1)↑2)) · (𝑀↑(𝑀 + (𝑗 + 1))))) | 
| 109 | 108 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑚 = (𝑗 + 1) → (((2↑(𝑚↑2)) · (𝑀↑(𝑀 + 𝑚))) · (!‘𝑛)) = (((2↑((𝑗 + 1)↑2)) · (𝑀↑(𝑀 + (𝑗 + 1)))) · (!‘𝑛))) | 
| 110 | 103, 109 | breq12d 5156 | . . . . . . 7
⊢ (𝑚 = (𝑗 + 1) → (((𝑛↑𝑚) · (𝑀↑𝑛)) ≤ (((2↑(𝑚↑2)) · (𝑀↑(𝑀 + 𝑚))) · (!‘𝑛)) ↔ ((𝑛↑(𝑗 + 1)) · (𝑀↑𝑛)) ≤ (((2↑((𝑗 + 1)↑2)) · (𝑀↑(𝑀 + (𝑗 + 1)))) · (!‘𝑛)))) | 
| 111 | 110 | ralbidv 3178 | . . . . . 6
⊢ (𝑚 = (𝑗 + 1) → (∀𝑛 ∈ ℕ ((𝑛↑𝑚) · (𝑀↑𝑛)) ≤ (((2↑(𝑚↑2)) · (𝑀↑(𝑀 + 𝑚))) · (!‘𝑛)) ↔ ∀𝑛 ∈ ℕ ((𝑛↑(𝑗 + 1)) · (𝑀↑𝑛)) ≤ (((2↑((𝑗 + 1)↑2)) · (𝑀↑(𝑀 + (𝑗 + 1)))) · (!‘𝑛)))) | 
| 112 | 111 | imbi2d 340 | . . . . 5
⊢ (𝑚 = (𝑗 + 1) → ((𝑀 ∈ ℕ0 →
∀𝑛 ∈ ℕ
((𝑛↑𝑚) · (𝑀↑𝑛)) ≤ (((2↑(𝑚↑2)) · (𝑀↑(𝑀 + 𝑚))) · (!‘𝑛))) ↔ (𝑀 ∈ ℕ0 →
∀𝑛 ∈ ℕ
((𝑛↑(𝑗 + 1)) · (𝑀↑𝑛)) ≤ (((2↑((𝑗 + 1)↑2)) · (𝑀↑(𝑀 + (𝑗 + 1)))) · (!‘𝑛))))) | 
| 113 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑚 = 𝐾 → (𝑛↑𝑚) = (𝑛↑𝐾)) | 
| 114 | 113 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑚 = 𝐾 → ((𝑛↑𝑚) · (𝑀↑𝑛)) = ((𝑛↑𝐾) · (𝑀↑𝑛))) | 
| 115 |  | oveq1 7438 | . . . . . . . . . . 11
⊢ (𝑚 = 𝐾 → (𝑚↑2) = (𝐾↑2)) | 
| 116 | 115 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑚 = 𝐾 → (2↑(𝑚↑2)) = (2↑(𝐾↑2))) | 
| 117 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ (𝑚 = 𝐾 → (𝑀 + 𝑚) = (𝑀 + 𝐾)) | 
| 118 | 117 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑚 = 𝐾 → (𝑀↑(𝑀 + 𝑚)) = (𝑀↑(𝑀 + 𝐾))) | 
| 119 | 116, 118 | oveq12d 7449 | . . . . . . . . 9
⊢ (𝑚 = 𝐾 → ((2↑(𝑚↑2)) · (𝑀↑(𝑀 + 𝑚))) = ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾)))) | 
| 120 | 119 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑚 = 𝐾 → (((2↑(𝑚↑2)) · (𝑀↑(𝑀 + 𝑚))) · (!‘𝑛)) = (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑛))) | 
| 121 | 114, 120 | breq12d 5156 | . . . . . . 7
⊢ (𝑚 = 𝐾 → (((𝑛↑𝑚) · (𝑀↑𝑛)) ≤ (((2↑(𝑚↑2)) · (𝑀↑(𝑀 + 𝑚))) · (!‘𝑛)) ↔ ((𝑛↑𝐾) · (𝑀↑𝑛)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑛)))) | 
| 122 | 121 | ralbidv 3178 | . . . . . 6
⊢ (𝑚 = 𝐾 → (∀𝑛 ∈ ℕ ((𝑛↑𝑚) · (𝑀↑𝑛)) ≤ (((2↑(𝑚↑2)) · (𝑀↑(𝑀 + 𝑚))) · (!‘𝑛)) ↔ ∀𝑛 ∈ ℕ ((𝑛↑𝐾) · (𝑀↑𝑛)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑛)))) | 
| 123 | 122 | imbi2d 340 | . . . . 5
⊢ (𝑚 = 𝐾 → ((𝑀 ∈ ℕ0 →
∀𝑛 ∈ ℕ
((𝑛↑𝑚) · (𝑀↑𝑛)) ≤ (((2↑(𝑚↑2)) · (𝑀↑(𝑀 + 𝑚))) · (!‘𝑛))) ↔ (𝑀 ∈ ℕ0 →
∀𝑛 ∈ ℕ
((𝑛↑𝐾) · (𝑀↑𝑛)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑛))))) | 
| 124 | 49, 79, 90, 101, 112, 123 | nn0indALT 12714 | . . . 4
⊢ (𝐾 ∈ ℕ0
→ (𝑀 ∈
ℕ0 → ∀𝑛 ∈ ℕ ((𝑛↑𝐾) · (𝑀↑𝑛)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑛)))) | 
| 125 | 124 | imp 406 | . . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → ∀𝑛 ∈ ℕ ((𝑛↑𝐾) · (𝑀↑𝑛)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑛))) | 
| 126 |  | oveq1 7438 | . . . . . 6
⊢ (𝑛 = 𝑁 → (𝑛↑𝐾) = (𝑁↑𝐾)) | 
| 127 |  | oveq2 7439 | . . . . . 6
⊢ (𝑛 = 𝑁 → (𝑀↑𝑛) = (𝑀↑𝑁)) | 
| 128 | 126, 127 | oveq12d 7449 | . . . . 5
⊢ (𝑛 = 𝑁 → ((𝑛↑𝐾) · (𝑀↑𝑛)) = ((𝑁↑𝐾) · (𝑀↑𝑁))) | 
| 129 |  | fveq2 6906 | . . . . . 6
⊢ (𝑛 = 𝑁 → (!‘𝑛) = (!‘𝑁)) | 
| 130 | 129 | oveq2d 7447 | . . . . 5
⊢ (𝑛 = 𝑁 → (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑛)) = (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) | 
| 131 | 128, 130 | breq12d 5156 | . . . 4
⊢ (𝑛 = 𝑁 → (((𝑛↑𝐾) · (𝑀↑𝑛)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑛)) ↔ ((𝑁↑𝐾) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁)))) | 
| 132 | 131 | rspcva 3620 | . . 3
⊢ ((𝑁 ∈ ℕ ∧
∀𝑛 ∈ ℕ
((𝑛↑𝐾) · (𝑀↑𝑛)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑛))) → ((𝑁↑𝐾) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) | 
| 133 | 125, 132 | sylan2 593 | . 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0)) → ((𝑁↑𝐾) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) | 
| 134 | 133 | 3impb 1115 | 1
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → ((𝑁↑𝐾) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) |