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

 Description: Lemma for addlocpr 6691. The (𝐷 +Q 𝐸)
Hypotheses
Ref Expression
addlocprlem.qppr (𝜑 → (𝑄 +Q (𝑃 +Q 𝑃)) = 𝑅)
addlocprlem.du (𝜑𝑈 <Q (𝐷 +Q 𝑃))
addlocprlem.et (𝜑𝑇 <Q (𝐸 +Q 𝑃))
Assertion
Ref Expression
addlocprlemgt (𝜑 → ((𝐷 +Q 𝐸) <Q 𝑄𝑅 ∈ (2nd ‘(𝐴 +P 𝐵))))

StepHypRef Expression
1 addlocprlem.a . . . . . . 7 (𝜑𝐴P)
2 addlocprlem.b . . . . . . 7 (𝜑𝐵P)
3 addlocprlem.qr . . . . . . 7 (𝜑𝑄 <Q 𝑅)
4 addlocprlem.p . . . . . . 7 (𝜑𝑃Q)
5 addlocprlem.qppr . . . . . . 7 (𝜑 → (𝑄 +Q (𝑃 +Q 𝑃)) = 𝑅)
6 addlocprlem.dlo . . . . . . 7 (𝜑𝐷 ∈ (1st𝐴))
7 addlocprlem.uup . . . . . . 7 (𝜑𝑈 ∈ (2nd𝐴))
8 addlocprlem.du . . . . . . 7 (𝜑𝑈 <Q (𝐷 +Q 𝑃))
9 addlocprlem.elo . . . . . . 7 (𝜑𝐸 ∈ (1st𝐵))
10 addlocprlem.tup . . . . . . 7 (𝜑𝑇 ∈ (2nd𝐵))
11 addlocprlem.et . . . . . . 7 (𝜑𝑇 <Q (𝐸 +Q 𝑃))
121, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11addlocprlemeqgt 6687 . . . . . 6 (𝜑 → (𝑈 +Q 𝑇) <Q ((𝐷 +Q 𝐸) +Q (𝑃 +Q 𝑃)))
1312adantr 265 . . . . 5 ((𝜑 ∧ (𝐷 +Q 𝐸) <Q 𝑄) → (𝑈 +Q 𝑇) <Q ((𝐷 +Q 𝐸) +Q (𝑃 +Q 𝑃)))
14 prop 6630 . . . . . . . . . . . 12 (𝐴P → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
151, 14syl 14 . . . . . . . . . . 11 (𝜑 → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
16 elprnql 6636 . . . . . . . . . . 11 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝐷 ∈ (1st𝐴)) → 𝐷Q)
1715, 6, 16syl2anc 397 . . . . . . . . . 10 (𝜑𝐷Q)
18 prop 6630 . . . . . . . . . . . 12 (𝐵P → ⟨(1st𝐵), (2nd𝐵)⟩ ∈ P)
192, 18syl 14 . . . . . . . . . . 11 (𝜑 → ⟨(1st𝐵), (2nd𝐵)⟩ ∈ P)
20 elprnql 6636 . . . . . . . . . . 11 ((⟨(1st𝐵), (2nd𝐵)⟩ ∈ P𝐸 ∈ (1st𝐵)) → 𝐸Q)
2119, 9, 20syl2anc 397 . . . . . . . . . 10 (𝜑𝐸Q)
22 addclnq 6530 . . . . . . . . . 10 ((𝐷Q𝐸Q) → (𝐷 +Q 𝐸) ∈ Q)
2317, 21, 22syl2anc 397 . . . . . . . . 9 (𝜑 → (𝐷 +Q 𝐸) ∈ Q)
24 ltrelnq 6520 . . . . . . . . . . . 12 <Q ⊆ (Q × Q)
2524brel 4419 . . . . . . . . . . 11 (𝑄 <Q 𝑅 → (𝑄Q𝑅Q))
263, 25syl 14 . . . . . . . . . 10 (𝜑 → (𝑄Q𝑅Q))
2726simpld 109 . . . . . . . . 9 (𝜑𝑄Q)
28 addclnq 6530 . . . . . . . . . 10 ((𝑃Q𝑃Q) → (𝑃 +Q 𝑃) ∈ Q)
294, 4, 28syl2anc 397 . . . . . . . . 9 (𝜑 → (𝑃 +Q 𝑃) ∈ Q)
30 ltanqg 6555 . . . . . . . . 9 (((𝐷 +Q 𝐸) ∈ Q𝑄Q ∧ (𝑃 +Q 𝑃) ∈ Q) → ((𝐷 +Q 𝐸) <Q 𝑄 ↔ ((𝑃 +Q 𝑃) +Q (𝐷 +Q 𝐸)) <Q ((𝑃 +Q 𝑃) +Q 𝑄)))
3123, 27, 29, 30syl3anc 1146 . . . . . . . 8 (𝜑 → ((𝐷 +Q 𝐸) <Q 𝑄 ↔ ((𝑃 +Q 𝑃) +Q (𝐷 +Q 𝐸)) <Q ((𝑃 +Q 𝑃) +Q 𝑄)))
32 addcomnqg 6536 . . . . . . . . . 10 (((𝑃 +Q 𝑃) ∈ Q ∧ (𝐷 +Q 𝐸) ∈ Q) → ((𝑃 +Q 𝑃) +Q (𝐷 +Q 𝐸)) = ((𝐷 +Q 𝐸) +Q (𝑃 +Q 𝑃)))
3329, 23, 32syl2anc 397 . . . . . . . . 9 (𝜑 → ((𝑃 +Q 𝑃) +Q (𝐷 +Q 𝐸)) = ((𝐷 +Q 𝐸) +Q (𝑃 +Q 𝑃)))
34 addcomnqg 6536 . . . . . . . . . 10 (((𝑃 +Q 𝑃) ∈ Q𝑄Q) → ((𝑃 +Q 𝑃) +Q 𝑄) = (𝑄 +Q (𝑃 +Q 𝑃)))
3529, 27, 34syl2anc 397 . . . . . . . . 9 (𝜑 → ((𝑃 +Q 𝑃) +Q 𝑄) = (𝑄 +Q (𝑃 +Q 𝑃)))
3633, 35breq12d 3804 . . . . . . . 8 (𝜑 → (((𝑃 +Q 𝑃) +Q (𝐷 +Q 𝐸)) <Q ((𝑃 +Q 𝑃) +Q 𝑄) ↔ ((𝐷 +Q 𝐸) +Q (𝑃 +Q 𝑃)) <Q (𝑄 +Q (𝑃 +Q 𝑃))))
3731, 36bitrd 181 . . . . . . 7 (𝜑 → ((𝐷 +Q 𝐸) <Q 𝑄 ↔ ((𝐷 +Q 𝐸) +Q (𝑃 +Q 𝑃)) <Q (𝑄 +Q (𝑃 +Q 𝑃))))
3837biimpa 284 . . . . . 6 ((𝜑 ∧ (𝐷 +Q 𝐸) <Q 𝑄) → ((𝐷 +Q 𝐸) +Q (𝑃 +Q 𝑃)) <Q (𝑄 +Q (𝑃 +Q 𝑃)))
395breq2d 3803 . . . . . . 7 (𝜑 → (((𝐷 +Q 𝐸) +Q (𝑃 +Q 𝑃)) <Q (𝑄 +Q (𝑃 +Q 𝑃)) ↔ ((𝐷 +Q 𝐸) +Q (𝑃 +Q 𝑃)) <Q 𝑅))
4039adantr 265 . . . . . 6 ((𝜑 ∧ (𝐷 +Q 𝐸) <Q 𝑄) → (((𝐷 +Q 𝐸) +Q (𝑃 +Q 𝑃)) <Q (𝑄 +Q (𝑃 +Q 𝑃)) ↔ ((𝐷 +Q 𝐸) +Q (𝑃 +Q 𝑃)) <Q 𝑅))
4138, 40mpbid 139 . . . . 5 ((𝜑 ∧ (𝐷 +Q 𝐸) <Q 𝑄) → ((𝐷 +Q 𝐸) +Q (𝑃 +Q 𝑃)) <Q 𝑅)
4213, 41jca 294 . . . 4 ((𝜑 ∧ (𝐷 +Q 𝐸) <Q 𝑄) → ((𝑈 +Q 𝑇) <Q ((𝐷 +Q 𝐸) +Q (𝑃 +Q 𝑃)) ∧ ((𝐷 +Q 𝐸) +Q (𝑃 +Q 𝑃)) <Q 𝑅))
43 ltsonq 6553 . . . . 5 <Q Or Q
4443, 24sotri 4747 . . . 4 (((𝑈 +Q 𝑇) <Q ((𝐷 +Q 𝐸) +Q (𝑃 +Q 𝑃)) ∧ ((𝐷 +Q 𝐸) +Q (𝑃 +Q 𝑃)) <Q 𝑅) → (𝑈 +Q 𝑇) <Q 𝑅)
4542, 44syl 14 . . 3 ((𝜑 ∧ (𝐷 +Q 𝐸) <Q 𝑄) → (𝑈 +Q 𝑇) <Q 𝑅)
461, 7jca 294 . . . . 5 (𝜑 → (𝐴P𝑈 ∈ (2nd𝐴)))
472, 10jca 294 . . . . 5 (𝜑 → (𝐵P𝑇 ∈ (2nd𝐵)))
4826simprd 111 . . . . 5 (𝜑𝑅Q)
49 addnqpru 6685 . . . . 5 ((((𝐴P𝑈 ∈ (2nd𝐴)) ∧ (𝐵P𝑇 ∈ (2nd𝐵))) ∧ 𝑅Q) → ((𝑈 +Q 𝑇) <Q 𝑅𝑅 ∈ (2nd ‘(𝐴 +P 𝐵))))
5046, 47, 48, 49syl21anc 1145 . . . 4 (𝜑 → ((𝑈 +Q 𝑇) <Q 𝑅𝑅 ∈ (2nd ‘(𝐴 +P 𝐵))))
5150adantr 265 . . 3 ((𝜑 ∧ (𝐷 +Q 𝐸) <Q 𝑄) → ((𝑈 +Q 𝑇) <Q 𝑅𝑅 ∈ (2nd ‘(𝐴 +P 𝐵))))
5245, 51mpd 13 . 2 ((𝜑 ∧ (𝐷 +Q 𝐸) <Q 𝑄) → 𝑅 ∈ (2nd ‘(𝐴 +P 𝐵)))
5352ex 112 1 (𝜑 → ((𝐷 +Q 𝐸) <Q 𝑄𝑅 ∈ (2nd ‘(𝐴 +P 𝐵))))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ↔ wb 102   = wceq 1259   ∈ wcel 1409  ⟨cop 3405   class class class wbr 3791  ‘cfv 4929  (class class class)co 5539  1st c1st 5792  2nd c2nd 5793  Qcnq 6435   +Q cplq 6437
 Copyright terms: Public domain W3C validator