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 8425 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 𝐷)))

Proof of Theorem addextpr
Dummy variables 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 addclpr 7398 . . . 4 ((𝐴P𝐵P) → (𝐴 +P 𝐵) ∈ P)
21adantr 274 . . 3 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → (𝐴 +P 𝐵) ∈ P)
3 addclpr 7398 . . . 4 ((𝐶P𝐷P) → (𝐶 +P 𝐷) ∈ P)
43adantl 275 . . 3 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → (𝐶 +P 𝐷) ∈ P)
5 simprl 521 . . . 4 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → 𝐶P)
6 simplr 520 . . . 4 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → 𝐵P)
7 addclpr 7398 . . . 4 ((𝐶P𝐵P) → (𝐶 +P 𝐵) ∈ P)
85, 6, 7syl2anc 409 . . 3 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → (𝐶 +P 𝐵) ∈ P)
9 ltsopr 7457 . . . 4 <P Or P
10 sowlin 4253 . . . 4 ((<P Or P ∧ ((𝐴 +P 𝐵) ∈ P ∧ (𝐶 +P 𝐷) ∈ P ∧ (𝐶 +P 𝐵) ∈ P)) → ((𝐴 +P 𝐵)<P (𝐶 +P 𝐷) → ((𝐴 +P 𝐵)<P (𝐶 +P 𝐵) ∨ (𝐶 +P 𝐵)<P (𝐶 +P 𝐷))))
119, 10mpan 421 . . 3 (((𝐴 +P 𝐵) ∈ P ∧ (𝐶 +P 𝐷) ∈ P ∧ (𝐶 +P 𝐵) ∈ P) → ((𝐴 +P 𝐵)<P (𝐶 +P 𝐷) → ((𝐴 +P 𝐵)<P (𝐶 +P 𝐵) ∨ (𝐶 +P 𝐵)<P (𝐶 +P 𝐷))))
122, 4, 8, 11syl3anc 1217 . 2 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → ((𝐴 +P 𝐵)<P (𝐶 +P 𝐷) → ((𝐴 +P 𝐵)<P (𝐶 +P 𝐵) ∨ (𝐶 +P 𝐵)<P (𝐶 +P 𝐷))))
13 simpll 519 . . . . 5 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → 𝐴P)
14 ltaprg 7480 . . . . 5 ((𝐴P𝐶P𝐵P) → (𝐴<P 𝐶 ↔ (𝐵 +P 𝐴)<P (𝐵 +P 𝐶)))
1513, 5, 6, 14syl3anc 1217 . . . 4 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → (𝐴<P 𝐶 ↔ (𝐵 +P 𝐴)<P (𝐵 +P 𝐶)))
16 addcomprg 7439 . . . . . . 7 ((𝑓P𝑔P) → (𝑓 +P 𝑔) = (𝑔 +P 𝑓))
1716adantl 275 . . . . . 6 ((((𝐴P𝐵P) ∧ (𝐶P𝐷P)) ∧ (𝑓P𝑔P)) → (𝑓 +P 𝑔) = (𝑔 +P 𝑓))
1817, 13, 6caovcomd 5939 . . . . 5 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → (𝐴 +P 𝐵) = (𝐵 +P 𝐴))
1917, 5, 6caovcomd 5939 . . . . 5 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → (𝐶 +P 𝐵) = (𝐵 +P 𝐶))
2018, 19breq12d 3952 . . . 4 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → ((𝐴 +P 𝐵)<P (𝐶 +P 𝐵) ↔ (𝐵 +P 𝐴)<P (𝐵 +P 𝐶)))
2115, 20bitr4d 190 . . 3 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → (𝐴<P 𝐶 ↔ (𝐴 +P 𝐵)<P (𝐶 +P 𝐵)))
22 simprr 522 . . . 4 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → 𝐷P)
23 ltaprg 7480 . . . 4 ((𝐵P𝐷P𝐶P) → (𝐵<P 𝐷 ↔ (𝐶 +P 𝐵)<P (𝐶 +P 𝐷)))
246, 22, 5, 23syl3anc 1217 . . 3 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → (𝐵<P 𝐷 ↔ (𝐶 +P 𝐵)<P (𝐶 +P 𝐷)))
2521, 24orbi12d 783 . 2 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → ((𝐴<P 𝐶𝐵<P 𝐷) ↔ ((𝐴 +P 𝐵)<P (𝐶 +P 𝐵) ∨ (𝐶 +P 𝐵)<P (𝐶 +P 𝐷))))
2612, 25sylibrd 168 1 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → ((𝐴 +P 𝐵)<P (𝐶 +P 𝐷) → (𝐴<P 𝐶𝐵<P 𝐷)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698   ∧ w3a 963   = wceq 1332   ∈ wcel 1481   class class class wbr 3939   Or wor 4228  (class class class)co 5786  Pcnp 7152   +P cpp 7154
 Copyright terms: Public domain W3C validator