Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  aptipr GIF version

Theorem aptipr 6963
 Description: Apartness of positive reals is tight. (Contributed by Jim Kingdon, 28-Jan-2020.)
Assertion
Ref Expression
aptipr ((𝐴P𝐵P ∧ ¬ (𝐴<P 𝐵𝐵<P 𝐴)) → 𝐴 = 𝐵)

Proof of Theorem aptipr
StepHypRef Expression
1 simp1 939 . . . 4 ((𝐴P𝐵P ∧ ¬ (𝐴<P 𝐵𝐵<P 𝐴)) → 𝐴P)
2 simp2 940 . . . 4 ((𝐴P𝐵P ∧ ¬ (𝐴<P 𝐵𝐵<P 𝐴)) → 𝐵P)
3 ioran 702 . . . . . . 7 (¬ (𝐴<P 𝐵𝐵<P 𝐴) ↔ (¬ 𝐴<P 𝐵 ∧ ¬ 𝐵<P 𝐴))
43biimpi 118 . . . . . 6 (¬ (𝐴<P 𝐵𝐵<P 𝐴) → (¬ 𝐴<P 𝐵 ∧ ¬ 𝐵<P 𝐴))
543ad2ant3 962 . . . . 5 ((𝐴P𝐵P ∧ ¬ (𝐴<P 𝐵𝐵<P 𝐴)) → (¬ 𝐴<P 𝐵 ∧ ¬ 𝐵<P 𝐴))
65simprd 112 . . . 4 ((𝐴P𝐵P ∧ ¬ (𝐴<P 𝐵𝐵<P 𝐴)) → ¬ 𝐵<P 𝐴)
7 aptiprleml 6961 . . . 4 ((𝐴P𝐵P ∧ ¬ 𝐵<P 𝐴) → (1st𝐴) ⊆ (1st𝐵))
81, 2, 6, 7syl3anc 1170 . . 3 ((𝐴P𝐵P ∧ ¬ (𝐴<P 𝐵𝐵<P 𝐴)) → (1st𝐴) ⊆ (1st𝐵))
95simpld 110 . . . 4 ((𝐴P𝐵P ∧ ¬ (𝐴<P 𝐵𝐵<P 𝐴)) → ¬ 𝐴<P 𝐵)
10 aptiprleml 6961 . . . 4 ((𝐵P𝐴P ∧ ¬ 𝐴<P 𝐵) → (1st𝐵) ⊆ (1st𝐴))
112, 1, 9, 10syl3anc 1170 . . 3 ((𝐴P𝐵P ∧ ¬ (𝐴<P 𝐵𝐵<P 𝐴)) → (1st𝐵) ⊆ (1st𝐴))
128, 11eqssd 3025 . 2 ((𝐴P𝐵P ∧ ¬ (𝐴<P 𝐵𝐵<P 𝐴)) → (1st𝐴) = (1st𝐵))
13 aptiprlemu 6962 . . . 4 ((𝐵P𝐴P ∧ ¬ 𝐴<P 𝐵) → (2nd𝐴) ⊆ (2nd𝐵))
142, 1, 9, 13syl3anc 1170 . . 3 ((𝐴P𝐵P ∧ ¬ (𝐴<P 𝐵𝐵<P 𝐴)) → (2nd𝐴) ⊆ (2nd𝐵))
15 aptiprlemu 6962 . . . 4 ((𝐴P𝐵P ∧ ¬ 𝐵<P 𝐴) → (2nd𝐵) ⊆ (2nd𝐴))
161, 2, 6, 15syl3anc 1170 . . 3 ((𝐴P𝐵P ∧ ¬ (𝐴<P 𝐵𝐵<P 𝐴)) → (2nd𝐵) ⊆ (2nd𝐴))
1714, 16eqssd 3025 . 2 ((𝐴P𝐵P ∧ ¬ (𝐴<P 𝐵𝐵<P 𝐴)) → (2nd𝐴) = (2nd𝐵))
18 preqlu 6794 . . 3 ((𝐴P𝐵P) → (𝐴 = 𝐵 ↔ ((1st𝐴) = (1st𝐵) ∧ (2nd𝐴) = (2nd𝐵))))
19183adant3 959 . 2 ((𝐴P𝐵P ∧ ¬ (𝐴<P 𝐵𝐵<P 𝐴)) → (𝐴 = 𝐵 ↔ ((1st𝐴) = (1st𝐵) ∧ (2nd𝐴) = (2nd𝐵))))
2012, 17, 19mpbir2and 886 1 ((𝐴P𝐵P ∧ ¬ (𝐴<P 𝐵𝐵<P 𝐴)) → 𝐴 = 𝐵)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 102   ↔ wb 103   ∨ wo 662   ∧ w3a 920   = wceq 1285   ∈ wcel 1434   ⊆ wss 2982   class class class wbr 3805  ‘cfv 4952  1st c1st 5817  2nd c2nd 5818  Pcnp 6613
 Copyright terms: Public domain W3C validator