Step |
Hyp |
Ref |
Expression |
1 |
|
avglt2 |
⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐵 < 𝐴 ↔ ( ( 𝐵 + 𝐴 ) / 2 ) < 𝐴 ) ) |
2 |
1
|
ancoms |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 < 𝐴 ↔ ( ( 𝐵 + 𝐴 ) / 2 ) < 𝐴 ) ) |
3 |
|
recn |
⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ ) |
4 |
|
recn |
⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ ) |
5 |
|
addcom |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) ) |
6 |
3 4 5
|
syl2an |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) ) |
7 |
6
|
oveq1d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) / 2 ) = ( ( 𝐵 + 𝐴 ) / 2 ) ) |
8 |
7
|
breq1d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 + 𝐵 ) / 2 ) < 𝐴 ↔ ( ( 𝐵 + 𝐴 ) / 2 ) < 𝐴 ) ) |
9 |
2 8
|
bitr4d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 < 𝐴 ↔ ( ( 𝐴 + 𝐵 ) / 2 ) < 𝐴 ) ) |
10 |
9
|
notbid |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ¬ 𝐵 < 𝐴 ↔ ¬ ( ( 𝐴 + 𝐵 ) / 2 ) < 𝐴 ) ) |
11 |
|
lenlt |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴 ) ) |
12 |
|
readdcl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ ) |
13 |
|
rehalfcl |
⊢ ( ( 𝐴 + 𝐵 ) ∈ ℝ → ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℝ ) |
14 |
12 13
|
syl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℝ ) |
15 |
|
lenlt |
⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℝ ) → ( 𝐴 ≤ ( ( 𝐴 + 𝐵 ) / 2 ) ↔ ¬ ( ( 𝐴 + 𝐵 ) / 2 ) < 𝐴 ) ) |
16 |
14 15
|
syldan |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ ( ( 𝐴 + 𝐵 ) / 2 ) ↔ ¬ ( ( 𝐴 + 𝐵 ) / 2 ) < 𝐴 ) ) |
17 |
10 11 16
|
3bitr4d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ 𝐴 ≤ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) |