Proof of Theorem faclbnd5
| Step | Hyp | Ref
| Expression |
| 1 | | nn0re 12535 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
| 2 | | reexpcl 14119 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 𝐾 ∈ ℕ0)
→ (𝑁↑𝐾) ∈
ℝ) |
| 3 | 1, 2 | sylan 580 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → (𝑁↑𝐾) ∈ ℝ) |
| 4 | 3 | ancoms 458 |
. . . . . . 7
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑁↑𝐾) ∈ ℝ) |
| 5 | | nnre 12273 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) |
| 6 | | reexpcl 14119 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℕ0)
→ (𝑀↑𝑁) ∈
ℝ) |
| 7 | 5, 6 | sylan 580 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝑀↑𝑁) ∈
ℝ) |
| 8 | | remulcl 11240 |
. . . . . . 7
⊢ (((𝑁↑𝐾) ∈ ℝ ∧ (𝑀↑𝑁) ∈ ℝ) → ((𝑁↑𝐾) · (𝑀↑𝑁)) ∈ ℝ) |
| 9 | 4, 7, 8 | syl2an 596 |
. . . . . 6
⊢ (((𝐾 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0)) → ((𝑁↑𝐾) · (𝑀↑𝑁)) ∈ ℝ) |
| 10 | 9 | anandirs 679 |
. . . . 5
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈ ℕ)
∧ 𝑁 ∈
ℕ0) → ((𝑁↑𝐾) · (𝑀↑𝑁)) ∈ ℝ) |
| 11 | | 2nn 12339 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
| 12 | | nn0sqcl 14130 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ (𝐾↑2) ∈
ℕ0) |
| 13 | | nnexpcl 14115 |
. . . . . . . . 9
⊢ ((2
∈ ℕ ∧ (𝐾↑2) ∈ ℕ0) →
(2↑(𝐾↑2)) ∈
ℕ) |
| 14 | 11, 12, 13 | sylancr 587 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ0
→ (2↑(𝐾↑2))
∈ ℕ) |
| 15 | | nnnn0 12533 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) |
| 16 | | nn0addcl 12561 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → (𝑀 + 𝐾) ∈
ℕ0) |
| 17 | 16 | ancoms 458 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝑀 + 𝐾) ∈
ℕ0) |
| 18 | 15, 17 | sylan2 593 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈ ℕ)
→ (𝑀 + 𝐾) ∈
ℕ0) |
| 19 | | nnexpcl 14115 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ (𝑀 + 𝐾) ∈ ℕ0) → (𝑀↑(𝑀 + 𝐾)) ∈ ℕ) |
| 20 | 18, 19 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ (𝐾 ∈ ℕ0
∧ 𝑀 ∈ ℕ))
→ (𝑀↑(𝑀 + 𝐾)) ∈ ℕ) |
| 21 | 20 | anabss7 673 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈ ℕ)
→ (𝑀↑(𝑀 + 𝐾)) ∈ ℕ) |
| 22 | | nnmulcl 12290 |
. . . . . . . 8
⊢
(((2↑(𝐾↑2)) ∈ ℕ ∧ (𝑀↑(𝑀 + 𝐾)) ∈ ℕ) → ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) ∈ ℕ) |
| 23 | 14, 21, 22 | syl2an2r 685 |
. . . . . . 7
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈ ℕ)
→ ((2↑(𝐾↑2))
· (𝑀↑(𝑀 + 𝐾))) ∈ ℕ) |
| 24 | 23 | nnred 12281 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈ ℕ)
→ ((2↑(𝐾↑2))
· (𝑀↑(𝑀 + 𝐾))) ∈ ℝ) |
| 25 | | faccl 14322 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ) |
| 26 | 25 | nnred 12281 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℝ) |
| 27 | | remulcl 11240 |
. . . . . 6
⊢
((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) ∈ ℝ ∧ (!‘𝑁) ∈ ℝ) →
(((2↑(𝐾↑2))
· (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁)) ∈ ℝ) |
| 28 | 24, 26, 27 | syl2an 596 |
. . . . 5
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈ ℕ)
∧ 𝑁 ∈
ℕ0) → (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁)) ∈ ℝ) |
| 29 | | 2re 12340 |
. . . . . 6
⊢ 2 ∈
ℝ |
| 30 | | remulcl 11240 |
. . . . . 6
⊢ ((2
∈ ℝ ∧ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁)) ∈ ℝ) → (2 ·
(((2↑(𝐾↑2))
· (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) ∈ ℝ) |
| 31 | 29, 28, 30 | sylancr 587 |
. . . . 5
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈ ℕ)
∧ 𝑁 ∈
ℕ0) → (2 · (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) ∈ ℝ) |
| 32 | | faclbnd4 14336 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑀
∈ ℕ0) → ((𝑁↑𝐾) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) |
| 33 | 15, 32 | syl3an3 1166 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑀
∈ ℕ) → ((𝑁↑𝐾) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) |
| 34 | 33 | 3coml 1128 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈
ℕ0) → ((𝑁↑𝐾) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) |
| 35 | 34 | 3expa 1119 |
. . . . 5
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈ ℕ)
∧ 𝑁 ∈
ℕ0) → ((𝑁↑𝐾) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) |
| 36 | | 1lt2 12437 |
. . . . . 6
⊢ 1 <
2 |
| 37 | | nnmulcl 12290 |
. . . . . . . . 9
⊢
((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) ∈ ℕ ∧ (!‘𝑁) ∈ ℕ) →
(((2↑(𝐾↑2))
· (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁)) ∈ ℕ) |
| 38 | 23, 25, 37 | syl2an 596 |
. . . . . . . 8
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈ ℕ)
∧ 𝑁 ∈
ℕ0) → (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁)) ∈ ℕ) |
| 39 | 38 | nngt0d 12315 |
. . . . . . 7
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈ ℕ)
∧ 𝑁 ∈
ℕ0) → 0 < (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) |
| 40 | | ltmulgt12 12128 |
. . . . . . . 8
⊢
(((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁)) ∈ ℝ ∧ 2 ∈ ℝ
∧ 0 < (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) → (1 < 2 ↔ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁)) < (2 · (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))))) |
| 41 | 29, 40 | mp3an2 1451 |
. . . . . . 7
⊢
(((((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁)) ∈ ℝ ∧ 0 <
(((2↑(𝐾↑2))
· (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) → (1 < 2 ↔ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁)) < (2 · (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))))) |
| 42 | 28, 39, 41 | syl2anc 584 |
. . . . . 6
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈ ℕ)
∧ 𝑁 ∈
ℕ0) → (1 < 2 ↔ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁)) < (2 · (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))))) |
| 43 | 36, 42 | mpbii 233 |
. . . . 5
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈ ℕ)
∧ 𝑁 ∈
ℕ0) → (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁)) < (2 · (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁)))) |
| 44 | 10, 28, 31, 35, 43 | lelttrd 11419 |
. . . 4
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈ ℕ)
∧ 𝑁 ∈
ℕ0) → ((𝑁↑𝐾) · (𝑀↑𝑁)) < (2 · (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁)))) |
| 45 | | 2cn 12341 |
. . . . 5
⊢ 2 ∈
ℂ |
| 46 | 23 | nncnd 12282 |
. . . . 5
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈ ℕ)
→ ((2↑(𝐾↑2))
· (𝑀↑(𝑀 + 𝐾))) ∈ ℂ) |
| 47 | 25 | nncnd 12282 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℂ) |
| 48 | | mulass 11243 |
. . . . 5
⊢ ((2
∈ ℂ ∧ ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) ∈ ℂ ∧ (!‘𝑁) ∈ ℂ) → ((2
· ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾)))) · (!‘𝑁)) = (2 · (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁)))) |
| 49 | 45, 46, 47, 48 | mp3an3an 1469 |
. . . 4
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈ ℕ)
∧ 𝑁 ∈
ℕ0) → ((2 · ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾)))) · (!‘𝑁)) = (2 · (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁)))) |
| 50 | 44, 49 | breqtrrd 5171 |
. . 3
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈ ℕ)
∧ 𝑁 ∈
ℕ0) → ((𝑁↑𝐾) · (𝑀↑𝑁)) < ((2 · ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾)))) · (!‘𝑁))) |
| 51 | 50 | 3impa 1110 |
. 2
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈
ℕ0) → ((𝑁↑𝐾) · (𝑀↑𝑁)) < ((2 · ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾)))) · (!‘𝑁))) |
| 52 | 51 | 3comr 1126 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈
ℕ0 ∧ 𝑀
∈ ℕ) → ((𝑁↑𝐾) · (𝑀↑𝑁)) < ((2 · ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾)))) · (!‘𝑁))) |