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