Metamath Proof Explorer

Theorem rpnnen3lem

Description: Lemma for rpnnen3 . (Contributed by Stefan O'Rear, 18-Jan-2015)

Ref Expression
Assertion rpnnen3lem ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ a < b → c ∈ ℚ | c < a ≠ c ∈ ℚ | c < b

Proof

Step Hyp Ref Expression
1 qbtwnre ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ a < b → ∃ d ∈ ℚ a < d ∧ d < b
2 simp2 ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ a < b ∧ d ∈ ℚ ∧ a < d ∧ d < b → d ∈ ℚ
3 simp3r ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ a < b ∧ d ∈ ℚ ∧ a < d ∧ d < b → d < b
4 breq1 ⊢ c = d → c < b ↔ d < b
5 4 elrab ⊢ d ∈ c ∈ ℚ | c < b ↔ d ∈ ℚ ∧ d < b
6 2 3 5 sylanbrc ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ a < b ∧ d ∈ ℚ ∧ a < d ∧ d < b → d ∈ c ∈ ℚ | c < b
7 simp11 ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ a < b ∧ d ∈ ℚ ∧ a < d ∧ d < b → a ∈ ℝ
8 qre ⊢ d ∈ ℚ → d ∈ ℝ
9 8 3ad2ant2 ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ a < b ∧ d ∈ ℚ ∧ a < d ∧ d < b → d ∈ ℝ
10 simp3l ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ a < b ∧ d ∈ ℚ ∧ a < d ∧ d < b → a < d
11 7 9 10 ltnsymd ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ a < b ∧ d ∈ ℚ ∧ a < d ∧ d < b → ¬ d < a
12 11 intnand ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ a < b ∧ d ∈ ℚ ∧ a < d ∧ d < b → ¬ d ∈ ℚ ∧ d < a
13 breq1 ⊢ c = d → c < a ↔ d < a
14 13 elrab ⊢ d ∈ c ∈ ℚ | c < a ↔ d ∈ ℚ ∧ d < a
15 12 14 sylnibr ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ a < b ∧ d ∈ ℚ ∧ a < d ∧ d < b → ¬ d ∈ c ∈ ℚ | c < a
16 nelne1 ⊢ d ∈ c ∈ ℚ | c < b ∧ ¬ d ∈ c ∈ ℚ | c < a → c ∈ ℚ | c < b ≠ c ∈ ℚ | c < a
17 6 15 16 syl2anc ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ a < b ∧ d ∈ ℚ ∧ a < d ∧ d < b → c ∈ ℚ | c < b ≠ c ∈ ℚ | c < a
18 17 necomd ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ a < b ∧ d ∈ ℚ ∧ a < d ∧ d < b → c ∈ ℚ | c < a ≠ c ∈ ℚ | c < b
19 18 rexlimdv3a ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ a < b → ∃ d ∈ ℚ a < d ∧ d < b → c ∈ ℚ | c < a ≠ c ∈ ℚ | c < b
20 1 19 mpd ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ a < b → c ∈ ℚ | c < a ≠ c ∈ ℚ | c < b
21 20 3expa ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ a < b → c ∈ ℚ | c < a ≠ c ∈ ℚ | c < b