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

 Description: Lemma for addlocpr 7245. The result, in deduction form. (Contributed by Jim Kingdon, 6-Dec-2019.)
Hypotheses
Ref Expression
addlocprlem.qppr (𝜑 → (𝑄 +Q (𝑃 +Q 𝑃)) = 𝑅)
addlocprlem.du (𝜑𝑈 <Q (𝐷 +Q 𝑃))
addlocprlem.et (𝜑𝑇 <Q (𝐸 +Q 𝑃))
Assertion
Ref Expression
addlocprlem (𝜑 → (𝑄 ∈ (1st ‘(𝐴 +P 𝐵)) ∨ 𝑅 ∈ (2nd ‘(𝐴 +P 𝐵))))

StepHypRef Expression
1 addlocprlem.qr . . . 4 (𝜑𝑄 <Q 𝑅)
2 ltrelnq 7074 . . . . . 6 <Q ⊆ (Q × Q)
32brel 4529 . . . . 5 (𝑄 <Q 𝑅 → (𝑄Q𝑅Q))
43simpld 111 . . . 4 (𝑄 <Q 𝑅𝑄Q)
51, 4syl 14 . . 3 (𝜑𝑄Q)
6 addlocprlem.a . . . . . 6 (𝜑𝐴P)
7 prop 7184 . . . . . 6 (𝐴P → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
86, 7syl 14 . . . . 5 (𝜑 → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
9 addlocprlem.dlo . . . . 5 (𝜑𝐷 ∈ (1st𝐴))
10 elprnql 7190 . . . . 5 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝐷 ∈ (1st𝐴)) → 𝐷Q)
118, 9, 10syl2anc 406 . . . 4 (𝜑𝐷Q)
12 addlocprlem.b . . . . . 6 (𝜑𝐵P)
13 prop 7184 . . . . . 6 (𝐵P → ⟨(1st𝐵), (2nd𝐵)⟩ ∈ P)
1412, 13syl 14 . . . . 5 (𝜑 → ⟨(1st𝐵), (2nd𝐵)⟩ ∈ P)
15 addlocprlem.elo . . . . 5 (𝜑𝐸 ∈ (1st𝐵))
16 elprnql 7190 . . . . 5 ((⟨(1st𝐵), (2nd𝐵)⟩ ∈ P𝐸 ∈ (1st𝐵)) → 𝐸Q)
1714, 15, 16syl2anc 406 . . . 4 (𝜑𝐸Q)
18 addclnq 7084 . . . 4 ((𝐷Q𝐸Q) → (𝐷 +Q 𝐸) ∈ Q)
1911, 17, 18syl2anc 406 . . 3 (𝜑 → (𝐷 +Q 𝐸) ∈ Q)
20 nqtri3or 7105 . . 3 ((𝑄Q ∧ (𝐷 +Q 𝐸) ∈ Q) → (𝑄 <Q (𝐷 +Q 𝐸) ∨ 𝑄 = (𝐷 +Q 𝐸) ∨ (𝐷 +Q 𝐸) <Q 𝑄))
215, 19, 20syl2anc 406 . 2 (𝜑 → (𝑄 <Q (𝐷 +Q 𝐸) ∨ 𝑄 = (𝐷 +Q 𝐸) ∨ (𝐷 +Q 𝐸) <Q 𝑄))
22 addlocprlem.p . . . . 5 (𝜑𝑃Q)
23 addlocprlem.qppr . . . . 5 (𝜑 → (𝑄 +Q (𝑃 +Q 𝑃)) = 𝑅)
24 addlocprlem.uup . . . . 5 (𝜑𝑈 ∈ (2nd𝐴))
25 addlocprlem.du . . . . 5 (𝜑𝑈 <Q (𝐷 +Q 𝑃))
26 addlocprlem.tup . . . . 5 (𝜑𝑇 ∈ (2nd𝐵))
27 addlocprlem.et . . . . 5 (𝜑𝑇 <Q (𝐸 +Q 𝑃))
286, 12, 1, 22, 23, 9, 24, 25, 15, 26, 27addlocprlemlt 7240 . . . 4 (𝜑 → (𝑄 <Q (𝐷 +Q 𝐸) → 𝑄 ∈ (1st ‘(𝐴 +P 𝐵))))
29 orc 674 . . . 4 (𝑄 ∈ (1st ‘(𝐴 +P 𝐵)) → (𝑄 ∈ (1st ‘(𝐴 +P 𝐵)) ∨ 𝑅 ∈ (2nd ‘(𝐴 +P 𝐵))))
3028, 29syl6 33 . . 3 (𝜑 → (𝑄 <Q (𝐷 +Q 𝐸) → (𝑄 ∈ (1st ‘(𝐴 +P 𝐵)) ∨ 𝑅 ∈ (2nd ‘(𝐴 +P 𝐵)))))
316, 12, 1, 22, 23, 9, 24, 25, 15, 26, 27addlocprlemeq 7242 . . . 4 (𝜑 → (𝑄 = (𝐷 +Q 𝐸) → 𝑅 ∈ (2nd ‘(𝐴 +P 𝐵))))
32 olc 673 . . . 4 (𝑅 ∈ (2nd ‘(𝐴 +P 𝐵)) → (𝑄 ∈ (1st ‘(𝐴 +P 𝐵)) ∨ 𝑅 ∈ (2nd ‘(𝐴 +P 𝐵))))
3331, 32syl6 33 . . 3 (𝜑 → (𝑄 = (𝐷 +Q 𝐸) → (𝑄 ∈ (1st ‘(𝐴 +P 𝐵)) ∨ 𝑅 ∈ (2nd ‘(𝐴 +P 𝐵)))))
346, 12, 1, 22, 23, 9, 24, 25, 15, 26, 27addlocprlemgt 7243 . . . 4 (𝜑 → ((𝐷 +Q 𝐸) <Q 𝑄𝑅 ∈ (2nd ‘(𝐴 +P 𝐵))))
3534, 32syl6 33 . . 3 (𝜑 → ((𝐷 +Q 𝐸) <Q 𝑄 → (𝑄 ∈ (1st ‘(𝐴 +P 𝐵)) ∨ 𝑅 ∈ (2nd ‘(𝐴 +P 𝐵)))))
3630, 33, 353jaod 1250 . 2 (𝜑 → ((𝑄 <Q (𝐷 +Q 𝐸) ∨ 𝑄 = (𝐷 +Q 𝐸) ∨ (𝐷 +Q 𝐸) <Q 𝑄) → (𝑄 ∈ (1st ‘(𝐴 +P 𝐵)) ∨ 𝑅 ∈ (2nd ‘(𝐴 +P 𝐵)))))
3721, 36mpd 13 1 (𝜑 → (𝑄 ∈ (1st ‘(𝐴 +P 𝐵)) ∨ 𝑅 ∈ (2nd ‘(𝐴 +P 𝐵))))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∨ wo 670   ∨ w3o 929   = wceq 1299   ∈ wcel 1448  ⟨cop 3477   class class class wbr 3875  ‘cfv 5059  (class class class)co 5706  1st c1st 5967  2nd c2nd 5968  Qcnq 6989   +Q cplq 6991
 Copyright terms: Public domain W3C validator