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

Theorem lttrsr 6847
 Description: Signed real 'less than' is a transitive relation. (Contributed by Jim Kingdon, 4-Jan-2019.)
Assertion
Ref Expression
lttrsr ((𝑓R𝑔RR) → ((𝑓 <R 𝑔𝑔 <R ) → 𝑓 <R ))
Distinct variable group:   𝑓,𝑔,

Proof of Theorem lttrsr
Dummy variables 𝑟 𝑠 𝑡 𝑥 𝑦 𝑧 𝑤 𝑣 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-nr 6812 . 2 R = ((P × P) / ~R )
2 breq1 3767 . . . 4 ([⟨𝑥, 𝑦⟩] ~R = 𝑓 → ([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑧, 𝑤⟩] ~R𝑓 <R [⟨𝑧, 𝑤⟩] ~R ))
32anbi1d 438 . . 3 ([⟨𝑥, 𝑦⟩] ~R = 𝑓 → (([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑧, 𝑤⟩] ~R ∧ [⟨𝑧, 𝑤⟩] ~R <R [⟨𝑣, 𝑢⟩] ~R ) ↔ (𝑓 <R [⟨𝑧, 𝑤⟩] ~R ∧ [⟨𝑧, 𝑤⟩] ~R <R [⟨𝑣, 𝑢⟩] ~R )))
4 breq1 3767 . . 3 ([⟨𝑥, 𝑦⟩] ~R = 𝑓 → ([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑣, 𝑢⟩] ~R𝑓 <R [⟨𝑣, 𝑢⟩] ~R ))
53, 4imbi12d 223 . 2 ([⟨𝑥, 𝑦⟩] ~R = 𝑓 → ((([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑧, 𝑤⟩] ~R ∧ [⟨𝑧, 𝑤⟩] ~R <R [⟨𝑣, 𝑢⟩] ~R ) → [⟨𝑥, 𝑦⟩] ~R <R [⟨𝑣, 𝑢⟩] ~R ) ↔ ((𝑓 <R [⟨𝑧, 𝑤⟩] ~R ∧ [⟨𝑧, 𝑤⟩] ~R <R [⟨𝑣, 𝑢⟩] ~R ) → 𝑓 <R [⟨𝑣, 𝑢⟩] ~R )))
6 breq2 3768 . . . 4 ([⟨𝑧, 𝑤⟩] ~R = 𝑔 → (𝑓 <R [⟨𝑧, 𝑤⟩] ~R𝑓 <R 𝑔))
7 breq1 3767 . . . 4 ([⟨𝑧, 𝑤⟩] ~R = 𝑔 → ([⟨𝑧, 𝑤⟩] ~R <R [⟨𝑣, 𝑢⟩] ~R𝑔 <R [⟨𝑣, 𝑢⟩] ~R ))
86, 7anbi12d 442 . . 3 ([⟨𝑧, 𝑤⟩] ~R = 𝑔 → ((𝑓 <R [⟨𝑧, 𝑤⟩] ~R ∧ [⟨𝑧, 𝑤⟩] ~R <R [⟨𝑣, 𝑢⟩] ~R ) ↔ (𝑓 <R 𝑔𝑔 <R [⟨𝑣, 𝑢⟩] ~R )))
98imbi1d 220 . 2 ([⟨𝑧, 𝑤⟩] ~R = 𝑔 → (((𝑓 <R [⟨𝑧, 𝑤⟩] ~R ∧ [⟨𝑧, 𝑤⟩] ~R <R [⟨𝑣, 𝑢⟩] ~R ) → 𝑓 <R [⟨𝑣, 𝑢⟩] ~R ) ↔ ((𝑓 <R 𝑔𝑔 <R [⟨𝑣, 𝑢⟩] ~R ) → 𝑓 <R [⟨𝑣, 𝑢⟩] ~R )))
10 breq2 3768 . . . 4 ([⟨𝑣, 𝑢⟩] ~R = → (𝑔 <R [⟨𝑣, 𝑢⟩] ~R𝑔 <R ))
1110anbi2d 437 . . 3 ([⟨𝑣, 𝑢⟩] ~R = → ((𝑓 <R 𝑔𝑔 <R [⟨𝑣, 𝑢⟩] ~R ) ↔ (𝑓 <R 𝑔𝑔 <R )))
12 breq2 3768 . . 3 ([⟨𝑣, 𝑢⟩] ~R = → (𝑓 <R [⟨𝑣, 𝑢⟩] ~R𝑓 <R ))
1311, 12imbi12d 223 . 2 ([⟨𝑣, 𝑢⟩] ~R = → (((𝑓 <R 𝑔𝑔 <R [⟨𝑣, 𝑢⟩] ~R ) → 𝑓 <R [⟨𝑣, 𝑢⟩] ~R ) ↔ ((𝑓 <R 𝑔𝑔 <R ) → 𝑓 <R )))
14 ltsrprg 6832 . . . . . 6 (((𝑥P𝑦P) ∧ (𝑧P𝑤P)) → ([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑧, 𝑤⟩] ~R ↔ (𝑥 +P 𝑤)<P (𝑦 +P 𝑧)))
15143adant3 924 . . . . 5 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → ([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑧, 𝑤⟩] ~R ↔ (𝑥 +P 𝑤)<P (𝑦 +P 𝑧)))
16 ltaprg 6717 . . . . . . . 8 ((𝑟P𝑠P𝑡P) → (𝑟<P 𝑠 ↔ (𝑡 +P 𝑟)<P (𝑡 +P 𝑠)))
1716adantl 262 . . . . . . 7 ((((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) ∧ (𝑟P𝑠P𝑡P)) → (𝑟<P 𝑠 ↔ (𝑡 +P 𝑟)<P (𝑡 +P 𝑠)))
18 simp1l 928 . . . . . . . 8 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → 𝑥P)
19 simp2r 931 . . . . . . . 8 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → 𝑤P)
20 addclpr 6635 . . . . . . . 8 ((𝑥P𝑤P) → (𝑥 +P 𝑤) ∈ P)
2118, 19, 20syl2anc 391 . . . . . . 7 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → (𝑥 +P 𝑤) ∈ P)
22 simp1r 929 . . . . . . . 8 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → 𝑦P)
23 simp2l 930 . . . . . . . 8 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → 𝑧P)
24 addclpr 6635 . . . . . . . 8 ((𝑦P𝑧P) → (𝑦 +P 𝑧) ∈ P)
2522, 23, 24syl2anc 391 . . . . . . 7 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → (𝑦 +P 𝑧) ∈ P)
26 simp3r 933 . . . . . . 7 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → 𝑢P)
27 addcomprg 6676 . . . . . . . 8 ((𝑟P𝑠P) → (𝑟 +P 𝑠) = (𝑠 +P 𝑟))
2827adantl 262 . . . . . . 7 ((((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) ∧ (𝑟P𝑠P)) → (𝑟 +P 𝑠) = (𝑠 +P 𝑟))
2917, 21, 25, 26, 28caovord2d 5670 . . . . . 6 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → ((𝑥 +P 𝑤)<P (𝑦 +P 𝑧) ↔ ((𝑥 +P 𝑤) +P 𝑢)<P ((𝑦 +P 𝑧) +P 𝑢)))
30 addassprg 6677 . . . . . . . 8 ((𝑥P𝑤P𝑢P) → ((𝑥 +P 𝑤) +P 𝑢) = (𝑥 +P (𝑤 +P 𝑢)))
3118, 19, 26, 30syl3anc 1135 . . . . . . 7 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → ((𝑥 +P 𝑤) +P 𝑢) = (𝑥 +P (𝑤 +P 𝑢)))
32 addassprg 6677 . . . . . . . 8 ((𝑦P𝑧P𝑢P) → ((𝑦 +P 𝑧) +P 𝑢) = (𝑦 +P (𝑧 +P 𝑢)))
3322, 23, 26, 32syl3anc 1135 . . . . . . 7 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → ((𝑦 +P 𝑧) +P 𝑢) = (𝑦 +P (𝑧 +P 𝑢)))
3431, 33breq12d 3777 . . . . . 6 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → (((𝑥 +P 𝑤) +P 𝑢)<P ((𝑦 +P 𝑧) +P 𝑢) ↔ (𝑥 +P (𝑤 +P 𝑢))<P (𝑦 +P (𝑧 +P 𝑢))))
3529, 34bitrd 177 . . . . 5 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → ((𝑥 +P 𝑤)<P (𝑦 +P 𝑧) ↔ (𝑥 +P (𝑤 +P 𝑢))<P (𝑦 +P (𝑧 +P 𝑢))))
3615, 35bitrd 177 . . . 4 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → ([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑧, 𝑤⟩] ~R ↔ (𝑥 +P (𝑤 +P 𝑢))<P (𝑦 +P (𝑧 +P 𝑢))))
37 ltsrprg 6832 . . . . . 6 (((𝑧P𝑤P) ∧ (𝑣P𝑢P)) → ([⟨𝑧, 𝑤⟩] ~R <R [⟨𝑣, 𝑢⟩] ~R ↔ (𝑧 +P 𝑢)<P (𝑤 +P 𝑣)))
38373adant1 922 . . . . 5 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → ([⟨𝑧, 𝑤⟩] ~R <R [⟨𝑣, 𝑢⟩] ~R ↔ (𝑧 +P 𝑢)<P (𝑤 +P 𝑣)))
39 addclpr 6635 . . . . . . 7 ((𝑧P𝑢P) → (𝑧 +P 𝑢) ∈ P)
4023, 26, 39syl2anc 391 . . . . . 6 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → (𝑧 +P 𝑢) ∈ P)
41 simp3l 932 . . . . . . 7 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → 𝑣P)
42 addclpr 6635 . . . . . . 7 ((𝑤P𝑣P) → (𝑤 +P 𝑣) ∈ P)
4319, 41, 42syl2anc 391 . . . . . 6 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → (𝑤 +P 𝑣) ∈ P)
44 ltaprg 6717 . . . . . 6 (((𝑧 +P 𝑢) ∈ P ∧ (𝑤 +P 𝑣) ∈ P𝑦P) → ((𝑧 +P 𝑢)<P (𝑤 +P 𝑣) ↔ (𝑦 +P (𝑧 +P 𝑢))<P (𝑦 +P (𝑤 +P 𝑣))))
4540, 43, 22, 44syl3anc 1135 . . . . 5 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → ((𝑧 +P 𝑢)<P (𝑤 +P 𝑣) ↔ (𝑦 +P (𝑧 +P 𝑢))<P (𝑦 +P (𝑤 +P 𝑣))))
4638, 45bitrd 177 . . . 4 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → ([⟨𝑧, 𝑤⟩] ~R <R [⟨𝑣, 𝑢⟩] ~R ↔ (𝑦 +P (𝑧 +P 𝑢))<P (𝑦 +P (𝑤 +P 𝑣))))
4736, 46anbi12d 442 . . 3 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → (([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑧, 𝑤⟩] ~R ∧ [⟨𝑧, 𝑤⟩] ~R <R [⟨𝑣, 𝑢⟩] ~R ) ↔ ((𝑥 +P (𝑤 +P 𝑢))<P (𝑦 +P (𝑧 +P 𝑢)) ∧ (𝑦 +P (𝑧 +P 𝑢))<P (𝑦 +P (𝑤 +P 𝑣)))))
48 ltsopr 6694 . . . . 5 <P Or P
49 ltrelpr 6603 . . . . 5 <P ⊆ (P × P)
5048, 49sotri 4720 . . . 4 (((𝑥 +P (𝑤 +P 𝑢))<P (𝑦 +P (𝑧 +P 𝑢)) ∧ (𝑦 +P (𝑧 +P 𝑢))<P (𝑦 +P (𝑤 +P 𝑣))) → (𝑥 +P (𝑤 +P 𝑢))<P (𝑦 +P (𝑤 +P 𝑣)))
51 addclpr 6635 . . . . . . . 8 ((𝑥P𝑢P) → (𝑥 +P 𝑢) ∈ P)
5218, 26, 51syl2anc 391 . . . . . . 7 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → (𝑥 +P 𝑢) ∈ P)
53 addclpr 6635 . . . . . . . 8 ((𝑦P𝑣P) → (𝑦 +P 𝑣) ∈ P)
5422, 41, 53syl2anc 391 . . . . . . 7 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → (𝑦 +P 𝑣) ∈ P)
55 ltaprg 6717 . . . . . . 7 (((𝑥 +P 𝑢) ∈ P ∧ (𝑦 +P 𝑣) ∈ P𝑤P) → ((𝑥 +P 𝑢)<P (𝑦 +P 𝑣) ↔ (𝑤 +P (𝑥 +P 𝑢))<P (𝑤 +P (𝑦 +P 𝑣))))
5652, 54, 19, 55syl3anc 1135 . . . . . 6 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → ((𝑥 +P 𝑢)<P (𝑦 +P 𝑣) ↔ (𝑤 +P (𝑥 +P 𝑢))<P (𝑤 +P (𝑦 +P 𝑣))))
5756biimprd 147 . . . . 5 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → ((𝑤 +P (𝑥 +P 𝑢))<P (𝑤 +P (𝑦 +P 𝑣)) → (𝑥 +P 𝑢)<P (𝑦 +P 𝑣)))
58 addassprg 6677 . . . . . . . 8 ((𝑟P𝑠P𝑡P) → ((𝑟 +P 𝑠) +P 𝑡) = (𝑟 +P (𝑠 +P 𝑡)))
5958adantl 262 . . . . . . 7 ((((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) ∧ (𝑟P𝑠P𝑡P)) → ((𝑟 +P 𝑠) +P 𝑡) = (𝑟 +P (𝑠 +P 𝑡)))
6018, 19, 26, 28, 59caov12d 5682 . . . . . 6 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → (𝑥 +P (𝑤 +P 𝑢)) = (𝑤 +P (𝑥 +P 𝑢)))
6122, 19, 41, 28, 59caov12d 5682 . . . . . 6 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → (𝑦 +P (𝑤 +P 𝑣)) = (𝑤 +P (𝑦 +P 𝑣)))
6260, 61breq12d 3777 . . . . 5 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → ((𝑥 +P (𝑤 +P 𝑢))<P (𝑦 +P (𝑤 +P 𝑣)) ↔ (𝑤 +P (𝑥 +P 𝑢))<P (𝑤 +P (𝑦 +P 𝑣))))
63 ltsrprg 6832 . . . . . 6 (((𝑥P𝑦P) ∧ (𝑣P𝑢P)) → ([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑣, 𝑢⟩] ~R ↔ (𝑥 +P 𝑢)<P (𝑦 +P 𝑣)))
64633adant2 923 . . . . 5 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → ([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑣, 𝑢⟩] ~R ↔ (𝑥 +P 𝑢)<P (𝑦 +P 𝑣)))
6557, 62, 643imtr4d 192 . . . 4 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → ((𝑥 +P (𝑤 +P 𝑢))<P (𝑦 +P (𝑤 +P 𝑣)) → [⟨𝑥, 𝑦⟩] ~R <R [⟨𝑣, 𝑢⟩] ~R ))
6650, 65syl5 28 . . 3 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → (((𝑥 +P (𝑤 +P 𝑢))<P (𝑦 +P (𝑧 +P 𝑢)) ∧ (𝑦 +P (𝑧 +P 𝑢))<P (𝑦 +P (𝑤 +P 𝑣))) → [⟨𝑥, 𝑦⟩] ~R <R [⟨𝑣, 𝑢⟩] ~R ))
6747, 66sylbid 139 . 2 (((𝑥P𝑦P) ∧ (𝑧P𝑤P) ∧ (𝑣P𝑢P)) → (([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑧, 𝑤⟩] ~R ∧ [⟨𝑧, 𝑤⟩] ~R <R [⟨𝑣, 𝑢⟩] ~R ) → [⟨𝑥, 𝑦⟩] ~R <R [⟨𝑣, 𝑢⟩] ~R ))
681, 5, 9, 13, 673ecoptocl 6195 1 ((𝑓R𝑔RR) → ((𝑓 <R 𝑔𝑔 <R ) → 𝑓 <R ))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∧ w3a 885   = wceq 1243   ∈ wcel 1393  ⟨cop 3378   class class class wbr 3764  (class class class)co 5512  [cec 6104  Pcnp 6389   +P cpp 6391
 Copyright terms: Public domain W3C validator