Proof of Theorem stoweidlem24
Step | Hyp | Ref
| Expression |
1 | | 1red 10834 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → 1 ∈ ℝ) |
2 | | stoweidlem24.8 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
3 | 2 | rpred 12628 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ ℝ) |
4 | 3 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → 𝐸 ∈ ℝ) |
5 | 1, 4 | resubcld 11260 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − 𝐸) ∈ ℝ) |
6 | | stoweidlem24.5 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
7 | 6 | nn0red 12151 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ ℝ) |
8 | 7 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → 𝐾 ∈ ℝ) |
9 | | stoweidlem24.3 |
. . . . . . . 8
⊢ (𝜑 → 𝑃:𝑇⟶ℝ) |
10 | 9 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → 𝑃:𝑇⟶ℝ) |
11 | | stoweidlem24.1 |
. . . . . . . . . 10
⊢ 𝑉 = {𝑡 ∈ 𝑇 ∣ (𝑃‘𝑡) < (𝐷 / 2)} |
12 | 11 | rabeq2i 3398 |
. . . . . . . . 9
⊢ (𝑡 ∈ 𝑉 ↔ (𝑡 ∈ 𝑇 ∧ (𝑃‘𝑡) < (𝐷 / 2))) |
13 | 12 | simplbi 501 |
. . . . . . . 8
⊢ (𝑡 ∈ 𝑉 → 𝑡 ∈ 𝑇) |
14 | 13 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → 𝑡 ∈ 𝑇) |
15 | 10, 14 | ffvelrnd 6905 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝑃‘𝑡) ∈ ℝ) |
16 | 8, 15 | remulcld 10863 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝐾 · (𝑃‘𝑡)) ∈ ℝ) |
17 | | stoweidlem24.4 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
18 | 17 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → 𝑁 ∈
ℕ0) |
19 | 16, 18 | reexpcld 13733 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → ((𝐾 · (𝑃‘𝑡))↑𝑁) ∈ ℝ) |
20 | 1, 19 | resubcld 11260 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − ((𝐾 · (𝑃‘𝑡))↑𝑁)) ∈ ℝ) |
21 | 15, 18 | reexpcld 13733 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → ((𝑃‘𝑡)↑𝑁) ∈ ℝ) |
22 | 1, 21 | resubcld 11260 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − ((𝑃‘𝑡)↑𝑁)) ∈ ℝ) |
23 | 6, 17 | jca 515 |
. . . . . 6
⊢ (𝜑 → (𝐾 ∈ ℕ0 ∧ 𝑁 ∈
ℕ0)) |
24 | 23 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝐾 ∈ ℕ0 ∧ 𝑁 ∈
ℕ0)) |
25 | | nn0expcl 13649 |
. . . . 5
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐾↑𝑁) ∈
ℕ0) |
26 | 24, 25 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝐾↑𝑁) ∈
ℕ0) |
27 | 22, 26 | reexpcld 13733 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → ((1 − ((𝑃‘𝑡)↑𝑁))↑(𝐾↑𝑁)) ∈ ℝ) |
28 | | 1red 10834 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) |
29 | | stoweidlem24.6 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈
ℝ+) |
30 | 29 | rpred 12628 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ ℝ) |
31 | 7, 30 | remulcld 10863 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 · 𝐷) ∈ ℝ) |
32 | 31 | rehalfcld 12077 |
. . . . . . 7
⊢ (𝜑 → ((𝐾 · 𝐷) / 2) ∈ ℝ) |
33 | 32, 17 | reexpcld 13733 |
. . . . . 6
⊢ (𝜑 → (((𝐾 · 𝐷) / 2)↑𝑁) ∈ ℝ) |
34 | 28, 33 | resubcld 11260 |
. . . . 5
⊢ (𝜑 → (1 − (((𝐾 · 𝐷) / 2)↑𝑁)) ∈ ℝ) |
35 | 34 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − (((𝐾 · 𝐷) / 2)↑𝑁)) ∈ ℝ) |
36 | | stoweidlem24.9 |
. . . . 5
⊢ (𝜑 → (1 − 𝐸) < (1 − (((𝐾 · 𝐷) / 2)↑𝑁))) |
37 | 36 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − 𝐸) < (1 − (((𝐾 · 𝐷) / 2)↑𝑁))) |
38 | 33 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (((𝐾 · 𝐷) / 2)↑𝑁) ∈ ℝ) |
39 | 32 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → ((𝐾 · 𝐷) / 2) ∈ ℝ) |
40 | 6 | nn0ge0d 12153 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ 𝐾) |
41 | 7, 40 | jca 515 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 ∈ ℝ ∧ 0 ≤ 𝐾)) |
42 | 41 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝐾 ∈ ℝ ∧ 0 ≤ 𝐾)) |
43 | | stoweidlem24.10 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑡 ∈ 𝑇 (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1)) |
44 | 43 | r19.21bi 3130 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1)) |
45 | 44 | simpld 498 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 0 ≤ (𝑃‘𝑡)) |
46 | 13, 45 | sylan2 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → 0 ≤ (𝑃‘𝑡)) |
47 | | mulge0 11350 |
. . . . . . 7
⊢ (((𝐾 ∈ ℝ ∧ 0 ≤
𝐾) ∧ ((𝑃‘𝑡) ∈ ℝ ∧ 0 ≤ (𝑃‘𝑡))) → 0 ≤ (𝐾 · (𝑃‘𝑡))) |
48 | 42, 15, 46, 47 | syl12anc 837 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → 0 ≤ (𝐾 · (𝑃‘𝑡))) |
49 | 30 | rehalfcld 12077 |
. . . . . . . . 9
⊢ (𝜑 → (𝐷 / 2) ∈ ℝ) |
50 | 49 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝐷 / 2) ∈ ℝ) |
51 | 12 | simprbi 500 |
. . . . . . . . . 10
⊢ (𝑡 ∈ 𝑉 → (𝑃‘𝑡) < (𝐷 / 2)) |
52 | 51 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝑃‘𝑡) < (𝐷 / 2)) |
53 | 15, 50, 52 | ltled 10980 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝑃‘𝑡) ≤ (𝐷 / 2)) |
54 | | lemul2a 11687 |
. . . . . . . 8
⊢ ((((𝑃‘𝑡) ∈ ℝ ∧ (𝐷 / 2) ∈ ℝ ∧ (𝐾 ∈ ℝ ∧ 0 ≤
𝐾)) ∧ (𝑃‘𝑡) ≤ (𝐷 / 2)) → (𝐾 · (𝑃‘𝑡)) ≤ (𝐾 · (𝐷 / 2))) |
55 | 15, 50, 42, 53, 54 | syl31anc 1375 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝐾 · (𝑃‘𝑡)) ≤ (𝐾 · (𝐷 / 2))) |
56 | 6 | nn0cnd 12152 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ ℂ) |
57 | 56 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → 𝐾 ∈ ℂ) |
58 | 29 | rpcnd 12630 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ ℂ) |
59 | 58 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → 𝐷 ∈ ℂ) |
60 | | 2cnne0 12040 |
. . . . . . . . 9
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
61 | 60 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (2 ∈ ℂ ∧ 2 ≠
0)) |
62 | | divass 11508 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0)) → ((𝐾 · 𝐷) / 2) = (𝐾 · (𝐷 / 2))) |
63 | 57, 59, 61, 62 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → ((𝐾 · 𝐷) / 2) = (𝐾 · (𝐷 / 2))) |
64 | 55, 63 | breqtrrd 5081 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝐾 · (𝑃‘𝑡)) ≤ ((𝐾 · 𝐷) / 2)) |
65 | | leexp1a 13745 |
. . . . . 6
⊢ ((((𝐾 · (𝑃‘𝑡)) ∈ ℝ ∧ ((𝐾 · 𝐷) / 2) ∈ ℝ ∧ 𝑁 ∈ ℕ0)
∧ (0 ≤ (𝐾 ·
(𝑃‘𝑡)) ∧ (𝐾 · (𝑃‘𝑡)) ≤ ((𝐾 · 𝐷) / 2))) → ((𝐾 · (𝑃‘𝑡))↑𝑁) ≤ (((𝐾 · 𝐷) / 2)↑𝑁)) |
66 | 16, 39, 18, 48, 64, 65 | syl32anc 1380 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → ((𝐾 · (𝑃‘𝑡))↑𝑁) ≤ (((𝐾 · 𝐷) / 2)↑𝑁)) |
67 | 19, 38, 1, 66 | lesub2dd 11449 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − (((𝐾 · 𝐷) / 2)↑𝑁)) ≤ (1 − ((𝐾 · (𝑃‘𝑡))↑𝑁))) |
68 | 5, 35, 20, 37, 67 | ltletrd 10992 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − 𝐸) < (1 − ((𝐾 · (𝑃‘𝑡))↑𝑁))) |
69 | 15 | recnd 10861 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝑃‘𝑡) ∈ ℂ) |
70 | 57, 69, 18 | mulexpd 13731 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → ((𝐾 · (𝑃‘𝑡))↑𝑁) = ((𝐾↑𝑁) · ((𝑃‘𝑡)↑𝑁))) |
71 | 70 | eqcomd 2743 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → ((𝐾↑𝑁) · ((𝑃‘𝑡)↑𝑁)) = ((𝐾 · (𝑃‘𝑡))↑𝑁)) |
72 | 71 | oveq2d 7229 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − ((𝐾↑𝑁) · ((𝑃‘𝑡)↑𝑁))) = (1 − ((𝐾 · (𝑃‘𝑡))↑𝑁))) |
73 | 13, 44 | sylan2 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1)) |
74 | 73 | simprd 499 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝑃‘𝑡) ≤ 1) |
75 | | exple1 13746 |
. . . . . 6
⊢ ((((𝑃‘𝑡) ∈ ℝ ∧ 0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1) ∧ 𝑁 ∈ ℕ0) → ((𝑃‘𝑡)↑𝑁) ≤ 1) |
76 | 15, 46, 74, 18, 75 | syl31anc 1375 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → ((𝑃‘𝑡)↑𝑁) ≤ 1) |
77 | | stoweidlem10 43226 |
. . . . 5
⊢ ((((𝑃‘𝑡)↑𝑁) ∈ ℝ ∧ (𝐾↑𝑁) ∈ ℕ0 ∧ ((𝑃‘𝑡)↑𝑁) ≤ 1) → (1 − ((𝐾↑𝑁) · ((𝑃‘𝑡)↑𝑁))) ≤ ((1 − ((𝑃‘𝑡)↑𝑁))↑(𝐾↑𝑁))) |
78 | 21, 26, 76, 77 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − ((𝐾↑𝑁) · ((𝑃‘𝑡)↑𝑁))) ≤ ((1 − ((𝑃‘𝑡)↑𝑁))↑(𝐾↑𝑁))) |
79 | 72, 78 | eqbrtrrd 5077 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − ((𝐾 · (𝑃‘𝑡))↑𝑁)) ≤ ((1 − ((𝑃‘𝑡)↑𝑁))↑(𝐾↑𝑁))) |
80 | 5, 20, 27, 68, 79 | ltletrd 10992 |
. 2
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − 𝐸) < ((1 − ((𝑃‘𝑡)↑𝑁))↑(𝐾↑𝑁))) |
81 | | stoweidlem24.2 |
. . . 4
⊢ 𝑄 = (𝑡 ∈ 𝑇 ↦ ((1 − ((𝑃‘𝑡)↑𝑁))↑(𝐾↑𝑁))) |
82 | 81, 9, 17, 6 | stoweidlem12 43228 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑄‘𝑡) = ((1 − ((𝑃‘𝑡)↑𝑁))↑(𝐾↑𝑁))) |
83 | 13, 82 | sylan2 596 |
. 2
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝑄‘𝑡) = ((1 − ((𝑃‘𝑡)↑𝑁))↑(𝐾↑𝑁))) |
84 | 80, 83 | breqtrrd 5081 |
1
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − 𝐸) < (𝑄‘𝑡)) |