Proof of Theorem stoweidlem24
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 1red 11262 | . . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → 1 ∈ ℝ) | 
| 2 |  | stoweidlem24.8 | . . . . . 6
⊢ (𝜑 → 𝐸 ∈
ℝ+) | 
| 3 | 2 | rpred 13077 | . . . . 5
⊢ (𝜑 → 𝐸 ∈ ℝ) | 
| 4 | 3 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → 𝐸 ∈ ℝ) | 
| 5 | 1, 4 | resubcld 11691 | . . 3
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − 𝐸) ∈ ℝ) | 
| 6 |  | stoweidlem24.5 | . . . . . . . 8
⊢ (𝜑 → 𝐾 ∈
ℕ0) | 
| 7 | 6 | nn0red 12588 | . . . . . . 7
⊢ (𝜑 → 𝐾 ∈ ℝ) | 
| 8 | 7 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → 𝐾 ∈ ℝ) | 
| 9 |  | stoweidlem24.3 | . . . . . . . 8
⊢ (𝜑 → 𝑃:𝑇⟶ℝ) | 
| 10 | 9 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → 𝑃:𝑇⟶ℝ) | 
| 11 |  | stoweidlem24.1 | . . . . . . . . . 10
⊢ 𝑉 = {𝑡 ∈ 𝑇 ∣ (𝑃‘𝑡) < (𝐷 / 2)} | 
| 12 | 11 | reqabi 3460 | . . . . . . . . 9
⊢ (𝑡 ∈ 𝑉 ↔ (𝑡 ∈ 𝑇 ∧ (𝑃‘𝑡) < (𝐷 / 2))) | 
| 13 | 12 | simplbi 497 | . . . . . . . 8
⊢ (𝑡 ∈ 𝑉 → 𝑡 ∈ 𝑇) | 
| 14 | 13 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → 𝑡 ∈ 𝑇) | 
| 15 | 10, 14 | ffvelcdmd 7105 | . . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝑃‘𝑡) ∈ ℝ) | 
| 16 | 8, 15 | remulcld 11291 | . . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝐾 · (𝑃‘𝑡)) ∈ ℝ) | 
| 17 |  | stoweidlem24.4 | . . . . . 6
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 18 | 17 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → 𝑁 ∈
ℕ0) | 
| 19 | 16, 18 | reexpcld 14203 | . . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → ((𝐾 · (𝑃‘𝑡))↑𝑁) ∈ ℝ) | 
| 20 | 1, 19 | resubcld 11691 | . . 3
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − ((𝐾 · (𝑃‘𝑡))↑𝑁)) ∈ ℝ) | 
| 21 | 15, 18 | reexpcld 14203 | . . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → ((𝑃‘𝑡)↑𝑁) ∈ ℝ) | 
| 22 | 1, 21 | resubcld 11691 | . . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − ((𝑃‘𝑡)↑𝑁)) ∈ ℝ) | 
| 23 | 6, 17 | jca 511 | . . . . . 6
⊢ (𝜑 → (𝐾 ∈ ℕ0 ∧ 𝑁 ∈
ℕ0)) | 
| 24 | 23 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝐾 ∈ ℕ0 ∧ 𝑁 ∈
ℕ0)) | 
| 25 |  | nn0expcl 14116 | . . . . 5
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐾↑𝑁) ∈
ℕ0) | 
| 26 | 24, 25 | syl 17 | . . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝐾↑𝑁) ∈
ℕ0) | 
| 27 | 22, 26 | reexpcld 14203 | . . 3
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → ((1 − ((𝑃‘𝑡)↑𝑁))↑(𝐾↑𝑁)) ∈ ℝ) | 
| 28 |  | 1red 11262 | . . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) | 
| 29 |  | stoweidlem24.6 | . . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈
ℝ+) | 
| 30 | 29 | rpred 13077 | . . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ ℝ) | 
| 31 | 7, 30 | remulcld 11291 | . . . . . . . 8
⊢ (𝜑 → (𝐾 · 𝐷) ∈ ℝ) | 
| 32 | 31 | rehalfcld 12513 | . . . . . . 7
⊢ (𝜑 → ((𝐾 · 𝐷) / 2) ∈ ℝ) | 
| 33 | 32, 17 | reexpcld 14203 | . . . . . 6
⊢ (𝜑 → (((𝐾 · 𝐷) / 2)↑𝑁) ∈ ℝ) | 
| 34 | 28, 33 | resubcld 11691 | . . . . 5
⊢ (𝜑 → (1 − (((𝐾 · 𝐷) / 2)↑𝑁)) ∈ ℝ) | 
| 35 | 34 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − (((𝐾 · 𝐷) / 2)↑𝑁)) ∈ ℝ) | 
| 36 |  | stoweidlem24.9 | . . . . 5
⊢ (𝜑 → (1 − 𝐸) < (1 − (((𝐾 · 𝐷) / 2)↑𝑁))) | 
| 37 | 36 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − 𝐸) < (1 − (((𝐾 · 𝐷) / 2)↑𝑁))) | 
| 38 | 33 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (((𝐾 · 𝐷) / 2)↑𝑁) ∈ ℝ) | 
| 39 | 32 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → ((𝐾 · 𝐷) / 2) ∈ ℝ) | 
| 40 | 6 | nn0ge0d 12590 | . . . . . . . . 9
⊢ (𝜑 → 0 ≤ 𝐾) | 
| 41 | 7, 40 | jca 511 | . . . . . . . 8
⊢ (𝜑 → (𝐾 ∈ ℝ ∧ 0 ≤ 𝐾)) | 
| 42 | 41 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝐾 ∈ ℝ ∧ 0 ≤ 𝐾)) | 
| 43 |  | stoweidlem24.10 | . . . . . . . . . 10
⊢ (𝜑 → ∀𝑡 ∈ 𝑇 (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1)) | 
| 44 | 43 | r19.21bi 3251 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1)) | 
| 45 | 44 | simpld 494 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 0 ≤ (𝑃‘𝑡)) | 
| 46 | 13, 45 | sylan2 593 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → 0 ≤ (𝑃‘𝑡)) | 
| 47 |  | mulge0 11781 | . . . . . . 7
⊢ (((𝐾 ∈ ℝ ∧ 0 ≤
𝐾) ∧ ((𝑃‘𝑡) ∈ ℝ ∧ 0 ≤ (𝑃‘𝑡))) → 0 ≤ (𝐾 · (𝑃‘𝑡))) | 
| 48 | 42, 15, 46, 47 | syl12anc 837 | . . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → 0 ≤ (𝐾 · (𝑃‘𝑡))) | 
| 49 | 30 | rehalfcld 12513 | . . . . . . . . 9
⊢ (𝜑 → (𝐷 / 2) ∈ ℝ) | 
| 50 | 49 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝐷 / 2) ∈ ℝ) | 
| 51 | 12 | simprbi 496 | . . . . . . . . . 10
⊢ (𝑡 ∈ 𝑉 → (𝑃‘𝑡) < (𝐷 / 2)) | 
| 52 | 51 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝑃‘𝑡) < (𝐷 / 2)) | 
| 53 | 15, 50, 52 | ltled 11409 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝑃‘𝑡) ≤ (𝐷 / 2)) | 
| 54 |  | lemul2a 12122 | . . . . . . . 8
⊢ ((((𝑃‘𝑡) ∈ ℝ ∧ (𝐷 / 2) ∈ ℝ ∧ (𝐾 ∈ ℝ ∧ 0 ≤
𝐾)) ∧ (𝑃‘𝑡) ≤ (𝐷 / 2)) → (𝐾 · (𝑃‘𝑡)) ≤ (𝐾 · (𝐷 / 2))) | 
| 55 | 15, 50, 42, 53, 54 | syl31anc 1375 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝐾 · (𝑃‘𝑡)) ≤ (𝐾 · (𝐷 / 2))) | 
| 56 | 6 | nn0cnd 12589 | . . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ ℂ) | 
| 57 | 56 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → 𝐾 ∈ ℂ) | 
| 58 | 29 | rpcnd 13079 | . . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ ℂ) | 
| 59 | 58 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → 𝐷 ∈ ℂ) | 
| 60 |  | 2cnne0 12476 | . . . . . . . . 9
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) | 
| 61 | 60 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (2 ∈ ℂ ∧ 2 ≠
0)) | 
| 62 |  | divass 11940 | . . . . . . . 8
⊢ ((𝐾 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0)) → ((𝐾 · 𝐷) / 2) = (𝐾 · (𝐷 / 2))) | 
| 63 | 57, 59, 61, 62 | syl3anc 1373 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → ((𝐾 · 𝐷) / 2) = (𝐾 · (𝐷 / 2))) | 
| 64 | 55, 63 | breqtrrd 5171 | . . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝐾 · (𝑃‘𝑡)) ≤ ((𝐾 · 𝐷) / 2)) | 
| 65 |  | leexp1a 14215 | . . . . . 6
⊢ ((((𝐾 · (𝑃‘𝑡)) ∈ ℝ ∧ ((𝐾 · 𝐷) / 2) ∈ ℝ ∧ 𝑁 ∈ ℕ0)
∧ (0 ≤ (𝐾 ·
(𝑃‘𝑡)) ∧ (𝐾 · (𝑃‘𝑡)) ≤ ((𝐾 · 𝐷) / 2))) → ((𝐾 · (𝑃‘𝑡))↑𝑁) ≤ (((𝐾 · 𝐷) / 2)↑𝑁)) | 
| 66 | 16, 39, 18, 48, 64, 65 | syl32anc 1380 | . . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → ((𝐾 · (𝑃‘𝑡))↑𝑁) ≤ (((𝐾 · 𝐷) / 2)↑𝑁)) | 
| 67 | 19, 38, 1, 66 | lesub2dd 11880 | . . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − (((𝐾 · 𝐷) / 2)↑𝑁)) ≤ (1 − ((𝐾 · (𝑃‘𝑡))↑𝑁))) | 
| 68 | 5, 35, 20, 37, 67 | ltletrd 11421 | . . 3
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − 𝐸) < (1 − ((𝐾 · (𝑃‘𝑡))↑𝑁))) | 
| 69 | 15 | recnd 11289 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝑃‘𝑡) ∈ ℂ) | 
| 70 | 57, 69, 18 | mulexpd 14201 | . . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → ((𝐾 · (𝑃‘𝑡))↑𝑁) = ((𝐾↑𝑁) · ((𝑃‘𝑡)↑𝑁))) | 
| 71 | 70 | eqcomd 2743 | . . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → ((𝐾↑𝑁) · ((𝑃‘𝑡)↑𝑁)) = ((𝐾 · (𝑃‘𝑡))↑𝑁)) | 
| 72 | 71 | oveq2d 7447 | . . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − ((𝐾↑𝑁) · ((𝑃‘𝑡)↑𝑁))) = (1 − ((𝐾 · (𝑃‘𝑡))↑𝑁))) | 
| 73 | 13, 44 | sylan2 593 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1)) | 
| 74 | 73 | simprd 495 | . . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝑃‘𝑡) ≤ 1) | 
| 75 |  | exple1 14216 | . . . . . 6
⊢ ((((𝑃‘𝑡) ∈ ℝ ∧ 0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1) ∧ 𝑁 ∈ ℕ0) → ((𝑃‘𝑡)↑𝑁) ≤ 1) | 
| 76 | 15, 46, 74, 18, 75 | syl31anc 1375 | . . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → ((𝑃‘𝑡)↑𝑁) ≤ 1) | 
| 77 |  | stoweidlem10 46025 | . . . . 5
⊢ ((((𝑃‘𝑡)↑𝑁) ∈ ℝ ∧ (𝐾↑𝑁) ∈ ℕ0 ∧ ((𝑃‘𝑡)↑𝑁) ≤ 1) → (1 − ((𝐾↑𝑁) · ((𝑃‘𝑡)↑𝑁))) ≤ ((1 − ((𝑃‘𝑡)↑𝑁))↑(𝐾↑𝑁))) | 
| 78 | 21, 26, 76, 77 | syl3anc 1373 | . . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − ((𝐾↑𝑁) · ((𝑃‘𝑡)↑𝑁))) ≤ ((1 − ((𝑃‘𝑡)↑𝑁))↑(𝐾↑𝑁))) | 
| 79 | 72, 78 | eqbrtrrd 5167 | . . 3
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − ((𝐾 · (𝑃‘𝑡))↑𝑁)) ≤ ((1 − ((𝑃‘𝑡)↑𝑁))↑(𝐾↑𝑁))) | 
| 80 | 5, 20, 27, 68, 79 | ltletrd 11421 | . 2
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − 𝐸) < ((1 − ((𝑃‘𝑡)↑𝑁))↑(𝐾↑𝑁))) | 
| 81 |  | stoweidlem24.2 | . . . 4
⊢ 𝑄 = (𝑡 ∈ 𝑇 ↦ ((1 − ((𝑃‘𝑡)↑𝑁))↑(𝐾↑𝑁))) | 
| 82 | 81, 9, 17, 6 | stoweidlem12 46027 | . . 3
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑄‘𝑡) = ((1 − ((𝑃‘𝑡)↑𝑁))↑(𝐾↑𝑁))) | 
| 83 | 13, 82 | sylan2 593 | . 2
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝑄‘𝑡) = ((1 − ((𝑃‘𝑡)↑𝑁))↑(𝐾↑𝑁))) | 
| 84 | 80, 83 | breqtrrd 5171 | 1
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − 𝐸) < (𝑄‘𝑡)) |