Step |
Hyp |
Ref |
Expression |
1 |
|
ixx.1 |
⊢ 𝑂 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } ) |
2 |
|
ixxub.2 |
⊢ ( ( 𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑤 < 𝐵 → 𝑤 𝑆 𝐵 ) ) |
3 |
|
ixxub.3 |
⊢ ( ( 𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑤 𝑆 𝐵 → 𝑤 ≤ 𝐵 ) ) |
4 |
|
ixxub.4 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝐴 < 𝑤 → 𝐴 𝑅 𝑤 ) ) |
5 |
|
ixxub.5 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝐴 𝑅 𝑤 → 𝐴 ≤ 𝑤 ) ) |
6 |
1
|
elixx1 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ↔ ( 𝑤 ∈ ℝ* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐵 ) ) ) |
7 |
6
|
3adant3 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ↔ ( 𝑤 ∈ ℝ* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐵 ) ) ) |
8 |
7
|
biimpa |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → ( 𝑤 ∈ ℝ* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐵 ) ) |
9 |
8
|
simp1d |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝑤 ∈ ℝ* ) |
10 |
9
|
ex |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) → 𝑤 ∈ ℝ* ) ) |
11 |
10
|
ssrdv |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ( 𝐴 𝑂 𝐵 ) ⊆ ℝ* ) |
12 |
|
infxrcl |
⊢ ( ( 𝐴 𝑂 𝐵 ) ⊆ ℝ* → inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ∈ ℝ* ) |
13 |
11 12
|
syl |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ∈ ℝ* ) |
14 |
|
simp1 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → 𝐴 ∈ ℝ* ) |
15 |
|
simprr |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) ) → 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) |
16 |
11
|
ad2antrr |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) ) → ( 𝐴 𝑂 𝐵 ) ⊆ ℝ* ) |
17 |
|
qre |
⊢ ( 𝑤 ∈ ℚ → 𝑤 ∈ ℝ ) |
18 |
17
|
rexrd |
⊢ ( 𝑤 ∈ ℚ → 𝑤 ∈ ℝ* ) |
19 |
18
|
ad2antlr |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) ) → 𝑤 ∈ ℝ* ) |
20 |
|
simprl |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) ) → 𝐴 < 𝑤 ) |
21 |
14
|
ad2antrr |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) ) → 𝐴 ∈ ℝ* ) |
22 |
21 19 4
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) ) → ( 𝐴 < 𝑤 → 𝐴 𝑅 𝑤 ) ) |
23 |
20 22
|
mpd |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) ) → 𝐴 𝑅 𝑤 ) |
24 |
13
|
ad2antrr |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) ) → inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ∈ ℝ* ) |
25 |
|
simpll2 |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) ) → 𝐵 ∈ ℝ* ) |
26 |
|
simp3 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) |
27 |
|
n0 |
⊢ ( ( 𝐴 𝑂 𝐵 ) ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) |
28 |
26 27
|
sylib |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ∃ 𝑤 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) |
29 |
13
|
adantr |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ∈ ℝ* ) |
30 |
|
simpl2 |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝐵 ∈ ℝ* ) |
31 |
|
infxrlb |
⊢ ( ( ( 𝐴 𝑂 𝐵 ) ⊆ ℝ* ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ≤ 𝑤 ) |
32 |
11 31
|
sylan |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ≤ 𝑤 ) |
33 |
8
|
simp3d |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝑤 𝑆 𝐵 ) |
34 |
9 30 3
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → ( 𝑤 𝑆 𝐵 → 𝑤 ≤ 𝐵 ) ) |
35 |
33 34
|
mpd |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝑤 ≤ 𝐵 ) |
36 |
29 9 30 32 35
|
xrletrd |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ≤ 𝐵 ) |
37 |
28 36
|
exlimddv |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ≤ 𝐵 ) |
38 |
37
|
ad2antrr |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) ) → inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ≤ 𝐵 ) |
39 |
19 24 25 15 38
|
xrltletrd |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) ) → 𝑤 < 𝐵 ) |
40 |
19 25 2
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) ) → ( 𝑤 < 𝐵 → 𝑤 𝑆 𝐵 ) ) |
41 |
39 40
|
mpd |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) ) → 𝑤 𝑆 𝐵 ) |
42 |
7
|
ad2antrr |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) ) → ( 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ↔ ( 𝑤 ∈ ℝ* ∧ 𝐴 𝑅 𝑤 ∧ 𝑤 𝑆 𝐵 ) ) ) |
43 |
19 23 41 42
|
mpbir3and |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) ) → 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) |
44 |
16 43 31
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) ) → inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ≤ 𝑤 ) |
45 |
24 19
|
xrlenltd |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) ) → ( inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ≤ 𝑤 ↔ ¬ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) ) |
46 |
44 45
|
mpbid |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) ∧ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) ) → ¬ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) |
47 |
15 46
|
pm2.65da |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ℚ ) → ¬ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) ) |
48 |
47
|
nrexdv |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ¬ ∃ 𝑤 ∈ ℚ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) ) |
49 |
|
qbtwnxr |
⊢ ( ( 𝐴 ∈ ℝ* ∧ inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ∈ ℝ* ∧ 𝐴 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) → ∃ 𝑤 ∈ ℚ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) ) |
50 |
49
|
3expia |
⊢ ( ( 𝐴 ∈ ℝ* ∧ inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ∈ ℝ* ) → ( 𝐴 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) → ∃ 𝑤 ∈ ℚ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) ) ) |
51 |
14 13 50
|
syl2anc |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ( 𝐴 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) → ∃ 𝑤 ∈ ℚ ( 𝐴 < 𝑤 ∧ 𝑤 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) ) ) |
52 |
48 51
|
mtod |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ¬ 𝐴 < inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) |
53 |
13 14 52
|
xrnltled |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ≤ 𝐴 ) |
54 |
8
|
simp2d |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝐴 𝑅 𝑤 ) |
55 |
14
|
adantr |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝐴 ∈ ℝ* ) |
56 |
55 9 5
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → ( 𝐴 𝑅 𝑤 → 𝐴 ≤ 𝑤 ) ) |
57 |
54 56
|
mpd |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) ∧ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) ) → 𝐴 ≤ 𝑤 ) |
58 |
57
|
ralrimiva |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ∀ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) 𝐴 ≤ 𝑤 ) |
59 |
|
infxrgelb |
⊢ ( ( ( 𝐴 𝑂 𝐵 ) ⊆ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( 𝐴 ≤ inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ↔ ∀ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) 𝐴 ≤ 𝑤 ) ) |
60 |
11 14 59
|
syl2anc |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → ( 𝐴 ≤ inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ↔ ∀ 𝑤 ∈ ( 𝐴 𝑂 𝐵 ) 𝐴 ≤ 𝑤 ) ) |
61 |
58 60
|
mpbird |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → 𝐴 ≤ inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) ) |
62 |
13 14 53 61
|
xrletrid |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 𝑂 𝐵 ) ≠ ∅ ) → inf ( ( 𝐴 𝑂 𝐵 ) , ℝ* , < ) = 𝐴 ) |