Step | Hyp | Ref
| Expression |
1 | | df-pi 14642 |
. . . 4
⊢ π =
inf((ℝ+ ∩ (◡sin
“ {0})), ℝ, < ) |
2 | | inss1 3795 |
. . . . . . 7
⊢
(ℝ+ ∩ (◡sin
“ {0})) ⊆ ℝ+ |
3 | | rpssre 11719 |
. . . . . . 7
⊢
ℝ+ ⊆ ℝ |
4 | 2, 3 | sstri 3577 |
. . . . . 6
⊢
(ℝ+ ∩ (◡sin
“ {0})) ⊆ ℝ |
5 | 4 | a1i 11 |
. . . . 5
⊢ (𝜑 → (ℝ+ ∩
(◡sin “ {0})) ⊆
ℝ) |
6 | | 0re 9919 |
. . . . . . 7
⊢ 0 ∈
ℝ |
7 | 2 | sseli 3564 |
. . . . . . . . 9
⊢ (𝑦 ∈ (ℝ+
∩ (◡sin “ {0})) → 𝑦 ∈
ℝ+) |
8 | 7 | rpge0d 11752 |
. . . . . . . 8
⊢ (𝑦 ∈ (ℝ+
∩ (◡sin “ {0})) → 0 ≤
𝑦) |
9 | 8 | rgen 2906 |
. . . . . . 7
⊢
∀𝑦 ∈
(ℝ+ ∩ (◡sin
“ {0}))0 ≤ 𝑦 |
10 | | breq1 4586 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝑥 ≤ 𝑦 ↔ 0 ≤ 𝑦)) |
11 | 10 | ralbidv 2969 |
. . . . . . . 8
⊢ (𝑥 = 0 → (∀𝑦 ∈ (ℝ+
∩ (◡sin “ {0}))𝑥 ≤ 𝑦 ↔ ∀𝑦 ∈ (ℝ+ ∩ (◡sin “ {0}))0 ≤ 𝑦)) |
12 | 11 | rspcev 3282 |
. . . . . . 7
⊢ ((0
∈ ℝ ∧ ∀𝑦 ∈ (ℝ+ ∩ (◡sin “ {0}))0 ≤ 𝑦) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (ℝ+ ∩ (◡sin “ {0}))𝑥 ≤ 𝑦) |
13 | 6, 9, 12 | mp2an 704 |
. . . . . 6
⊢
∃𝑥 ∈
ℝ ∀𝑦 ∈
(ℝ+ ∩ (◡sin
“ {0}))𝑥 ≤ 𝑦 |
14 | 13 | a1i 11 |
. . . . 5
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (ℝ+ ∩ (◡sin “ {0}))𝑥 ≤ 𝑦) |
15 | | 2re 10967 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
16 | | pilem.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
17 | 16 | rpred 11748 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ℝ) |
18 | | remulcl 9900 |
. . . . . . . . 9
⊢ ((2
∈ ℝ ∧ 𝐵
∈ ℝ) → (2 · 𝐵) ∈ ℝ) |
19 | 15, 17, 18 | sylancr 694 |
. . . . . . . 8
⊢ (𝜑 → (2 · 𝐵) ∈
ℝ) |
20 | | pilem.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ (2(,)4)) |
21 | | elioore 12076 |
. . . . . . . . 9
⊢ (𝐴 ∈ (2(,)4) → 𝐴 ∈
ℝ) |
22 | 20, 21 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℝ) |
23 | 19, 22 | resubcld 10337 |
. . . . . . 7
⊢ (𝜑 → ((2 · 𝐵) − 𝐴) ∈ ℝ) |
24 | | 4re 10974 |
. . . . . . . . . 10
⊢ 4 ∈
ℝ |
25 | 24 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 4 ∈
ℝ) |
26 | | eliooord 12104 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (2(,)4) → (2 <
𝐴 ∧ 𝐴 < 4)) |
27 | 20, 26 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (2 < 𝐴 ∧ 𝐴 < 4)) |
28 | 27 | simprd 478 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 < 4) |
29 | | 2t2e4 11054 |
. . . . . . . . . 10
⊢ (2
· 2) = 4 |
30 | 15 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ∈
ℝ) |
31 | | 0red 9920 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 0 ∈
ℝ) |
32 | | 2pos 10989 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 <
2 |
33 | 32 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 0 < 2) |
34 | 27 | simpld 474 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 2 < 𝐴) |
35 | 31, 30, 22, 33, 34 | lttrd 10077 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 < 𝐴) |
36 | 22, 35 | elrpd 11745 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
37 | | pilem.3 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (sin‘𝐴) = 0) |
38 | | pilem1 24009 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (ℝ+
∩ (◡sin “ {0})) ↔ (𝐴 ∈ ℝ+
∧ (sin‘𝐴) =
0)) |
39 | 36, 37, 38 | sylanbrc 695 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈ (ℝ+ ∩ (◡sin “ {0}))) |
40 | | ne0i 3880 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (ℝ+
∩ (◡sin “ {0})) →
(ℝ+ ∩ (◡sin
“ {0})) ≠ ∅) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℝ+ ∩
(◡sin “ {0})) ≠
∅) |
42 | | infrecl 10882 |
. . . . . . . . . . . . . 14
⊢
(((ℝ+ ∩ (◡sin “ {0})) ⊆ ℝ ∧
(ℝ+ ∩ (◡sin
“ {0})) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (ℝ+ ∩ (◡sin “ {0}))𝑥 ≤ 𝑦) → inf((ℝ+ ∩
(◡sin “ {0})), ℝ, < )
∈ ℝ) |
43 | 4, 13, 42 | mp3an13 1407 |
. . . . . . . . . . . . 13
⊢
((ℝ+ ∩ (◡sin “ {0})) ≠ ∅ →
inf((ℝ+ ∩ (◡sin
“ {0})), ℝ, < ) ∈ ℝ) |
44 | 41, 43 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → inf((ℝ+
∩ (◡sin “ {0})), ℝ,
< ) ∈ ℝ) |
45 | | pilem1 24009 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (ℝ+
∩ (◡sin “ {0})) ↔ (𝑥 ∈ ℝ+
∧ (sin‘𝑥) =
0)) |
46 | | rpre 11715 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
47 | 46 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ) |
48 | | letric 10016 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
∈ ℝ ∧ 𝑥
∈ ℝ) → (2 ≤ 𝑥 ∨ 𝑥 ≤ 2)) |
49 | 15, 47, 48 | sylancr 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (2 ≤
𝑥 ∨ 𝑥 ≤ 2)) |
50 | 49 | ord 391 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (¬ 2
≤ 𝑥 → 𝑥 ≤ 2)) |
51 | 46 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑥 ≤ 2) → 𝑥 ∈
ℝ) |
52 | | rpgt0 11720 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℝ+
→ 0 < 𝑥) |
53 | 52 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑥 ≤ 2) → 0 < 𝑥) |
54 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑥 ≤ 2) → 𝑥 ≤ 2) |
55 | | 0xr 9965 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ∈
ℝ* |
56 | | elioc2 12107 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((0
∈ ℝ* ∧ 2 ∈ ℝ) → (𝑥 ∈ (0(,]2) ↔ (𝑥 ∈ ℝ ∧ 0 < 𝑥 ∧ 𝑥 ≤ 2))) |
57 | 55, 15, 56 | mp2an 704 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (0(,]2) ↔ (𝑥 ∈ ℝ ∧ 0 <
𝑥 ∧ 𝑥 ≤ 2)) |
58 | 51, 53, 54, 57 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑥 ≤ 2) → 𝑥 ∈
(0(,]2)) |
59 | | sin02gt0 14761 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (0(,]2) → 0 <
(sin‘𝑥)) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑥 ≤ 2) → 0 <
(sin‘𝑥)) |
61 | 60 | gt0ne0d 10471 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑥 ≤ 2) → (sin‘𝑥) ≠ 0) |
62 | 61 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ≤ 2 → (sin‘𝑥) ≠ 0)) |
63 | 50, 62 | syld 46 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (¬ 2
≤ 𝑥 →
(sin‘𝑥) ≠
0)) |
64 | 63 | necon4bd 2802 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((sin‘𝑥) = 0 → 2
≤ 𝑥)) |
65 | 64 | expimpd 627 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑥 ∈ ℝ+ ∧
(sin‘𝑥) = 0) → 2
≤ 𝑥)) |
66 | 45, 65 | syl5bi 231 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ (ℝ+ ∩ (◡sin “ {0})) → 2 ≤ 𝑥)) |
67 | 66 | ralrimiv 2948 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑥 ∈ (ℝ+ ∩ (◡sin “ {0}))2 ≤ 𝑥) |
68 | | infregelb 10884 |
. . . . . . . . . . . . . 14
⊢
((((ℝ+ ∩ (◡sin “ {0})) ⊆ ℝ ∧
(ℝ+ ∩ (◡sin
“ {0})) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (ℝ+ ∩ (◡sin “ {0}))𝑥 ≤ 𝑦) ∧ 2 ∈ ℝ) → (2 ≤
inf((ℝ+ ∩ (◡sin
“ {0})), ℝ, < ) ↔ ∀𝑥 ∈ (ℝ+ ∩ (◡sin “ {0}))2 ≤ 𝑥)) |
69 | 5, 41, 14, 30, 68 | syl31anc 1321 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 ≤
inf((ℝ+ ∩ (◡sin
“ {0})), ℝ, < ) ↔ ∀𝑥 ∈ (ℝ+ ∩ (◡sin “ {0}))2 ≤ 𝑥)) |
70 | 67, 69 | mpbird 246 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ≤
inf((ℝ+ ∩ (◡sin
“ {0})), ℝ, < )) |
71 | | pilem.4 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (sin‘𝐵) = 0) |
72 | | pilem1 24009 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ (ℝ+
∩ (◡sin “ {0})) ↔ (𝐵 ∈ ℝ+
∧ (sin‘𝐵) =
0)) |
73 | 16, 71, 72 | sylanbrc 695 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ (ℝ+ ∩ (◡sin “ {0}))) |
74 | | infrelb 10885 |
. . . . . . . . . . . . 13
⊢
(((ℝ+ ∩ (◡sin “ {0})) ⊆ ℝ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈
(ℝ+ ∩ (◡sin
“ {0}))𝑥 ≤ 𝑦 ∧ 𝐵 ∈ (ℝ+ ∩ (◡sin “ {0}))) →
inf((ℝ+ ∩ (◡sin
“ {0})), ℝ, < ) ≤ 𝐵) |
75 | 5, 14, 73, 74 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (𝜑 → inf((ℝ+
∩ (◡sin “ {0})), ℝ,
< ) ≤ 𝐵) |
76 | 30, 44, 17, 70, 75 | letrd 10073 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ≤ 𝐵) |
77 | 15, 32 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢ (2 ∈
ℝ ∧ 0 < 2) |
78 | 77 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2 ∈ ℝ ∧ 0
< 2)) |
79 | | lemul2 10755 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℝ ∧ 𝐵
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (2 ≤ 𝐵 ↔ (2 · 2) ≤ (2
· 𝐵))) |
80 | 30, 17, 78, 79 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 ≤ 𝐵 ↔ (2 · 2) ≤ (2 ·
𝐵))) |
81 | 76, 80 | mpbid 221 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · 2) ≤ (2
· 𝐵)) |
82 | 29, 81 | syl5eqbrr 4619 |
. . . . . . . . 9
⊢ (𝜑 → 4 ≤ (2 · 𝐵)) |
83 | 22, 25, 19, 28, 82 | ltletrd 10076 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 < (2 · 𝐵)) |
84 | 22, 19 | posdifd 10493 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 < (2 · 𝐵) ↔ 0 < ((2 · 𝐵) − 𝐴))) |
85 | 83, 84 | mpbid 221 |
. . . . . . 7
⊢ (𝜑 → 0 < ((2 · 𝐵) − 𝐴)) |
86 | 23, 85 | elrpd 11745 |
. . . . . 6
⊢ (𝜑 → ((2 · 𝐵) − 𝐴) ∈
ℝ+) |
87 | 19 | recnd 9947 |
. . . . . . . 8
⊢ (𝜑 → (2 · 𝐵) ∈
ℂ) |
88 | 22 | recnd 9947 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) |
89 | | sinsub 14737 |
. . . . . . . 8
⊢ (((2
· 𝐵) ∈ ℂ
∧ 𝐴 ∈ ℂ)
→ (sin‘((2 · 𝐵) − 𝐴)) = (((sin‘(2 · 𝐵)) · (cos‘𝐴)) − ((cos‘(2
· 𝐵)) ·
(sin‘𝐴)))) |
90 | 87, 88, 89 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (sin‘((2 ·
𝐵) − 𝐴)) = (((sin‘(2 ·
𝐵)) ·
(cos‘𝐴)) −
((cos‘(2 · 𝐵))
· (sin‘𝐴)))) |
91 | 17 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ ℂ) |
92 | | sin2t 14746 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℂ →
(sin‘(2 · 𝐵))
= (2 · ((sin‘𝐵) · (cos‘𝐵)))) |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (sin‘(2 ·
𝐵)) = (2 ·
((sin‘𝐵) ·
(cos‘𝐵)))) |
94 | 71 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((sin‘𝐵) · (cos‘𝐵)) = (0 ·
(cos‘𝐵))) |
95 | 91 | coscld 14700 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (cos‘𝐵) ∈
ℂ) |
96 | 95 | mul02d 10113 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (0 ·
(cos‘𝐵)) =
0) |
97 | 94, 96 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((sin‘𝐵) · (cos‘𝐵)) = 0) |
98 | 97 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 ·
((sin‘𝐵) ·
(cos‘𝐵))) = (2
· 0)) |
99 | | 2t0e0 11060 |
. . . . . . . . . . . . 13
⊢ (2
· 0) = 0 |
100 | 98, 99 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2 ·
((sin‘𝐵) ·
(cos‘𝐵))) =
0) |
101 | 93, 100 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (𝜑 → (sin‘(2 ·
𝐵)) = 0) |
102 | 101 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝜑 → ((sin‘(2 ·
𝐵)) ·
(cos‘𝐴)) = (0
· (cos‘𝐴))) |
103 | 88 | coscld 14700 |
. . . . . . . . . . 11
⊢ (𝜑 → (cos‘𝐴) ∈
ℂ) |
104 | 103 | mul02d 10113 |
. . . . . . . . . 10
⊢ (𝜑 → (0 ·
(cos‘𝐴)) =
0) |
105 | 102, 104 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝜑 → ((sin‘(2 ·
𝐵)) ·
(cos‘𝐴)) =
0) |
106 | 37 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝜑 → ((cos‘(2 ·
𝐵)) ·
(sin‘𝐴)) =
((cos‘(2 · 𝐵))
· 0)) |
107 | 87 | coscld 14700 |
. . . . . . . . . . 11
⊢ (𝜑 → (cos‘(2 ·
𝐵)) ∈
ℂ) |
108 | 107 | mul01d 10114 |
. . . . . . . . . 10
⊢ (𝜑 → ((cos‘(2 ·
𝐵)) · 0) =
0) |
109 | 106, 108 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝜑 → ((cos‘(2 ·
𝐵)) ·
(sin‘𝐴)) =
0) |
110 | 105, 109 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝜑 → (((sin‘(2 ·
𝐵)) ·
(cos‘𝐴)) −
((cos‘(2 · 𝐵))
· (sin‘𝐴))) =
(0 − 0)) |
111 | | 0m0e0 11007 |
. . . . . . . 8
⊢ (0
− 0) = 0 |
112 | 110, 111 | syl6eq 2660 |
. . . . . . 7
⊢ (𝜑 → (((sin‘(2 ·
𝐵)) ·
(cos‘𝐴)) −
((cos‘(2 · 𝐵))
· (sin‘𝐴))) =
0) |
113 | 90, 112 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → (sin‘((2 ·
𝐵) − 𝐴)) = 0) |
114 | | pilem1 24009 |
. . . . . 6
⊢ (((2
· 𝐵) − 𝐴) ∈ (ℝ+
∩ (◡sin “ {0})) ↔ (((2
· 𝐵) − 𝐴) ∈ ℝ+
∧ (sin‘((2 · 𝐵) − 𝐴)) = 0)) |
115 | 86, 113, 114 | sylanbrc 695 |
. . . . 5
⊢ (𝜑 → ((2 · 𝐵) − 𝐴) ∈ (ℝ+ ∩ (◡sin “ {0}))) |
116 | | infrelb 10885 |
. . . . 5
⊢
(((ℝ+ ∩ (◡sin “ {0})) ⊆ ℝ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈
(ℝ+ ∩ (◡sin
“ {0}))𝑥 ≤ 𝑦 ∧ ((2 · 𝐵) − 𝐴) ∈ (ℝ+ ∩ (◡sin “ {0}))) →
inf((ℝ+ ∩ (◡sin
“ {0})), ℝ, < ) ≤ ((2 · 𝐵) − 𝐴)) |
117 | 5, 14, 115, 116 | syl3anc 1318 |
. . . 4
⊢ (𝜑 → inf((ℝ+
∩ (◡sin “ {0})), ℝ,
< ) ≤ ((2 · 𝐵)
− 𝐴)) |
118 | 1, 117 | syl5eqbr 4618 |
. . 3
⊢ (𝜑 → π ≤ ((2 ·
𝐵) − 𝐴)) |
119 | 1, 44 | syl5eqel 2692 |
. . . 4
⊢ (𝜑 → π ∈
ℝ) |
120 | | leaddsub 10383 |
. . . 4
⊢ ((π
∈ ℝ ∧ 𝐴
∈ ℝ ∧ (2 · 𝐵) ∈ ℝ) → ((π + 𝐴) ≤ (2 · 𝐵) ↔ π ≤ ((2 ·
𝐵) − 𝐴))) |
121 | 119, 22, 19, 120 | syl3anc 1318 |
. . 3
⊢ (𝜑 → ((π + 𝐴) ≤ (2 · 𝐵) ↔ π ≤ ((2 · 𝐵) − 𝐴))) |
122 | 118, 121 | mpbird 246 |
. 2
⊢ (𝜑 → (π + 𝐴) ≤ (2 · 𝐵)) |
123 | 119, 22 | readdcld 9948 |
. . 3
⊢ (𝜑 → (π + 𝐴) ∈ ℝ) |
124 | | ledivmul 10778 |
. . 3
⊢ (((π +
𝐴) ∈ ℝ ∧
𝐵 ∈ ℝ ∧ (2
∈ ℝ ∧ 0 < 2)) → (((π + 𝐴) / 2) ≤ 𝐵 ↔ (π + 𝐴) ≤ (2 · 𝐵))) |
125 | 123, 17, 78, 124 | syl3anc 1318 |
. 2
⊢ (𝜑 → (((π + 𝐴) / 2) ≤ 𝐵 ↔ (π + 𝐴) ≤ (2 · 𝐵))) |
126 | 122, 125 | mpbird 246 |
1
⊢ (𝜑 → ((π + 𝐴) / 2) ≤ 𝐵) |