Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for metakunt
Miscellaneous results for AKS formalisation
0nonelalab
Next ⟩
dvrelogpow2b
Metamath Proof Explorer
Ascii
Unicode
Theorem
0nonelalab
Description:
Technical lemma for open interval.
(Contributed by
metakunt
, 12-Aug-2024)
Ref
Expression
Hypotheses
0nonelaleb.1
⊢
φ
→
A
∈
ℝ
0nonelaleb.2
⊢
φ
→
B
∈
ℝ
0nonelaleb.3
⊢
φ
→
0
<
A
0nonelaleb.4
⊢
φ
→
A
≤
B
0nonelalab.5
⊢
φ
→
C
∈
A
B
Assertion
0nonelalab
⊢
φ
→
0
≠
C
Proof
Step
Hyp
Ref
Expression
1
0nonelaleb.1
⊢
φ
→
A
∈
ℝ
2
0nonelaleb.2
⊢
φ
→
B
∈
ℝ
3
0nonelaleb.3
⊢
φ
→
0
<
A
4
0nonelaleb.4
⊢
φ
→
A
≤
B
5
0nonelalab.5
⊢
φ
→
C
∈
A
B
6
0red
⊢
φ
→
0
∈
ℝ
7
elioore
⊢
C
∈
A
B
→
C
∈
ℝ
8
5
7
syl
⊢
φ
→
C
∈
ℝ
9
1
rexrd
⊢
φ
→
A
∈
ℝ
*
10
2
rexrd
⊢
φ
→
B
∈
ℝ
*
11
elioo2
⊢
A
∈
ℝ
*
∧
B
∈
ℝ
*
→
C
∈
A
B
↔
C
∈
ℝ
∧
A
<
C
∧
C
<
B
12
9
10
11
syl2anc
⊢
φ
→
C
∈
A
B
↔
C
∈
ℝ
∧
A
<
C
∧
C
<
B
13
5
12
mpbid
⊢
φ
→
C
∈
ℝ
∧
A
<
C
∧
C
<
B
14
13
simp2d
⊢
φ
→
A
<
C
15
6
1
8
3
14
lttrd
⊢
φ
→
0
<
C
16
6
15
ltned
⊢
φ
→
0
≠
C