This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qextltlem

Description: Lemma for qextlt and qextle . (Contributed by Mario Carneiro, 3-Oct-2014)

Ref Expression
Assertion qextltlem ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → ∃ 𝑥 ∈ ℚ ( ¬ ( 𝑥 < 𝐴 ↔ 𝑥 < 𝐵 ) ∧ ¬ ( 𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 qbtwnxr ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) )
2 1 3expia ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
3 simprl ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ℚ ) ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → 𝐴 < 𝑥 )
4 simplll ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ℚ ) ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → 𝐴 ∈ ℝ* )
5 qre ⊢ ( 𝑥 ∈ ℚ → 𝑥 ∈ ℝ )
6 5 rexrd ⊢ ( 𝑥 ∈ ℚ → 𝑥 ∈ ℝ* )
7 6 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ℚ ) ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → 𝑥 ∈ ℝ* )
8 xrltnle ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( 𝐴 < 𝑥 ↔ ¬ 𝑥 ≤ 𝐴 ) )
9 4 7 8 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ℚ ) ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → ( 𝐴 < 𝑥 ↔ ¬ 𝑥 ≤ 𝐴 ) )
10 3 9 mpbid ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ℚ ) ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → ¬ 𝑥 ≤ 𝐴 )
11 xrltle ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( 𝑥 < 𝐴 → 𝑥 ≤ 𝐴 ) )
12 7 4 11 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ℚ ) ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → ( 𝑥 < 𝐴 → 𝑥 ≤ 𝐴 ) )
13 10 12 mtod ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ℚ ) ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → ¬ 𝑥 < 𝐴 )
14 simprr ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ℚ ) ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → 𝑥 < 𝐵 )
15 13 14 2thd ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ℚ ) ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → ( ¬ 𝑥 < 𝐴 ↔ 𝑥 < 𝐵 ) )
16 nbbn ⊢ ( ( ¬ 𝑥 < 𝐴 ↔ 𝑥 < 𝐵 ) ↔ ¬ ( 𝑥 < 𝐴 ↔ 𝑥 < 𝐵 ) )
17 15 16 sylib ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ℚ ) ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → ¬ ( 𝑥 < 𝐴 ↔ 𝑥 < 𝐵 ) )
18 simpllr ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ℚ ) ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → 𝐵 ∈ ℝ* )
19 7 18 14 xrltled ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ℚ ) ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → 𝑥 ≤ 𝐵 )
20 10 19 2thd ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ℚ ) ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → ( ¬ 𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵 ) )
21 nbbn ⊢ ( ( ¬ 𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵 ) ↔ ¬ ( 𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵 ) )
22 20 21 sylib ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ℚ ) ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → ¬ ( 𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵 ) )
23 17 22 jca ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ℚ ) ∧ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) ) → ( ¬ ( 𝑥 < 𝐴 ↔ 𝑥 < 𝐵 ) ∧ ¬ ( 𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵 ) ) )
24 23 ex ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑥 ∈ ℚ ) → ( ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) → ( ¬ ( 𝑥 < 𝐴 ↔ 𝑥 < 𝐵 ) ∧ ¬ ( 𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵 ) ) ) )
25 24 reximdva ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ∃ 𝑥 ∈ ℚ ( 𝐴 < 𝑥 ∧ 𝑥 < 𝐵 ) → ∃ 𝑥 ∈ ℚ ( ¬ ( 𝑥 < 𝐴 ↔ 𝑥 < 𝐵 ) ∧ ¬ ( 𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵 ) ) ) )
26 2 25 syld ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → ∃ 𝑥 ∈ ℚ ( ¬ ( 𝑥 < 𝐴 ↔ 𝑥 < 𝐵 ) ∧ ¬ ( 𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵 ) ) ) )