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

 Description: Strong extensionality of addition (ordering version). This is similar to addext 7601 but for positive reals and based on less-than rather than apartness. (Contributed by Jim Kingdon, 17-Feb-2020.)
Assertion
Ref Expression
addextpr (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → ((𝐴 +P 𝐵)<P (𝐶 +P 𝐷) → (𝐴<P 𝐶𝐵<P 𝐷)))

Dummy variables 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 addclpr 6635 . . . 4 ((𝐴P𝐵P) → (𝐴 +P 𝐵) ∈ P)
21adantr 261 . . 3 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → (𝐴 +P 𝐵) ∈ P)
3 addclpr 6635 . . . 4 ((𝐶P𝐷P) → (𝐶 +P 𝐷) ∈ P)
43adantl 262 . . 3 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → (𝐶 +P 𝐷) ∈ P)
5 simprl 483 . . . 4 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → 𝐶P)
6 simplr 482 . . . 4 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → 𝐵P)
7 addclpr 6635 . . . 4 ((𝐶P𝐵P) → (𝐶 +P 𝐵) ∈ P)
85, 6, 7syl2anc 391 . . 3 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → (𝐶 +P 𝐵) ∈ P)
9 ltsopr 6694 . . . 4 <P Or P
10 sowlin 4057 . . . 4 ((<P Or P ∧ ((𝐴 +P 𝐵) ∈ P ∧ (𝐶 +P 𝐷) ∈ P ∧ (𝐶 +P 𝐵) ∈ P)) → ((𝐴 +P 𝐵)<P (𝐶 +P 𝐷) → ((𝐴 +P 𝐵)<P (𝐶 +P 𝐵) ∨ (𝐶 +P 𝐵)<P (𝐶 +P 𝐷))))
119, 10mpan 400 . . 3 (((𝐴 +P 𝐵) ∈ P ∧ (𝐶 +P 𝐷) ∈ P ∧ (𝐶 +P 𝐵) ∈ P) → ((𝐴 +P 𝐵)<P (𝐶 +P 𝐷) → ((𝐴 +P 𝐵)<P (𝐶 +P 𝐵) ∨ (𝐶 +P 𝐵)<P (𝐶 +P 𝐷))))
122, 4, 8, 11syl3anc 1135 . 2 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → ((𝐴 +P 𝐵)<P (𝐶 +P 𝐷) → ((𝐴 +P 𝐵)<P (𝐶 +P 𝐵) ∨ (𝐶 +P 𝐵)<P (𝐶 +P 𝐷))))
13 simpll 481 . . . . 5 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → 𝐴P)
14 ltaprg 6717 . . . . 5 ((𝐴P𝐶P𝐵P) → (𝐴<P 𝐶 ↔ (𝐵 +P 𝐴)<P (𝐵 +P 𝐶)))
1513, 5, 6, 14syl3anc 1135 . . . 4 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → (𝐴<P 𝐶 ↔ (𝐵 +P 𝐴)<P (𝐵 +P 𝐶)))
16 addcomprg 6676 . . . . . . 7 ((𝑓P𝑔P) → (𝑓 +P 𝑔) = (𝑔 +P 𝑓))
1716adantl 262 . . . . . 6 ((((𝐴P𝐵P) ∧ (𝐶P𝐷P)) ∧ (𝑓P𝑔P)) → (𝑓 +P 𝑔) = (𝑔 +P 𝑓))
1817, 13, 6caovcomd 5657 . . . . 5 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → (𝐴 +P 𝐵) = (𝐵 +P 𝐴))
1917, 5, 6caovcomd 5657 . . . . 5 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → (𝐶 +P 𝐵) = (𝐵 +P 𝐶))
2018, 19breq12d 3777 . . . 4 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → ((𝐴 +P 𝐵)<P (𝐶 +P 𝐵) ↔ (𝐵 +P 𝐴)<P (𝐵 +P 𝐶)))
2115, 20bitr4d 180 . . 3 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → (𝐴<P 𝐶 ↔ (𝐴 +P 𝐵)<P (𝐶 +P 𝐵)))
22 simprr 484 . . . 4 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → 𝐷P)
23 ltaprg 6717 . . . 4 ((𝐵P𝐷P𝐶P) → (𝐵<P 𝐷 ↔ (𝐶 +P 𝐵)<P (𝐶 +P 𝐷)))
246, 22, 5, 23syl3anc 1135 . . 3 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → (𝐵<P 𝐷 ↔ (𝐶 +P 𝐵)<P (𝐶 +P 𝐷)))
2521, 24orbi12d 707 . 2 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → ((𝐴<P 𝐶𝐵<P 𝐷) ↔ ((𝐴 +P 𝐵)<P (𝐶 +P 𝐵) ∨ (𝐶 +P 𝐵)<P (𝐶 +P 𝐷))))
2612, 25sylibrd 158 1 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → ((𝐴 +P 𝐵)<P (𝐶 +P 𝐷) → (𝐴<P 𝐶𝐵<P 𝐷)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 629   ∧ w3a 885   = wceq 1243   ∈ wcel 1393   class class class wbr 3764   Or wor 4032  (class class class)co 5512  Pcnp 6389   +P cpp 6391
 Copyright terms: Public domain W3C validator