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

Theorem mullocprlem 6549
Description: Calculations for mullocpr 6550. (Contributed by Jim Kingdon, 10-Dec-2019.)
Hypotheses
Ref Expression
mullocprlem.ab (φ → (A P B P))
mullocprlem.uqedu (φ → (𝑈 ·Q 𝑄) <Q (𝐸 ·Q (𝐷 ·Q 𝑈)))
mullocprlem.edutdu (φ → (𝐸 ·Q (𝐷 ·Q 𝑈)) <Q (𝑇 ·Q (𝐷 ·Q 𝑈)))
mullocprlem.tdudr (φ → (𝑇 ·Q (𝐷 ·Q 𝑈)) <Q (𝐷 ·Q 𝑅))
mullocprlem.qr (φ → (𝑄 Q 𝑅 Q))
mullocprlem.duq (φ → (𝐷 Q 𝑈 Q))
mullocprlem.du (φ → (𝐷 (1stA) 𝑈 (2ndA)))
mullocprlem.et (φ → (𝐸 Q 𝑇 Q))
Assertion
Ref Expression
mullocprlem (φ → (𝑄 (1st ‘(A ·P B)) 𝑅 (2nd ‘(A ·P B))))

Proof of Theorem mullocprlem
Dummy variables x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mullocprlem.uqedu . . . . . . 7 (φ → (𝑈 ·Q 𝑄) <Q (𝐸 ·Q (𝐷 ·Q 𝑈)))
2 mullocprlem.et . . . . . . . . 9 (φ → (𝐸 Q 𝑇 Q))
32simpld 105 . . . . . . . 8 (φ𝐸 Q)
4 mullocprlem.duq . . . . . . . . 9 (φ → (𝐷 Q 𝑈 Q))
54simpld 105 . . . . . . . 8 (φ𝐷 Q)
64simprd 107 . . . . . . . 8 (φ𝑈 Q)
7 mulcomnqg 6367 . . . . . . . . 9 ((x Q y Q) → (x ·Q y) = (y ·Q x))
87adantl 262 . . . . . . . 8 ((φ (x Q y Q)) → (x ·Q y) = (y ·Q x))
9 mulassnqg 6368 . . . . . . . . 9 ((x Q y Q z Q) → ((x ·Q y) ·Q z) = (x ·Q (y ·Q z)))
109adantl 262 . . . . . . . 8 ((φ (x Q y Q z Q)) → ((x ·Q y) ·Q z) = (x ·Q (y ·Q z)))
113, 5, 6, 8, 10caov13d 5626 . . . . . . 7 (φ → (𝐸 ·Q (𝐷 ·Q 𝑈)) = (𝑈 ·Q (𝐷 ·Q 𝐸)))
121, 11breqtrd 3779 . . . . . 6 (φ → (𝑈 ·Q 𝑄) <Q (𝑈 ·Q (𝐷 ·Q 𝐸)))
13 mullocprlem.qr . . . . . . . 8 (φ → (𝑄 Q 𝑅 Q))
1413simpld 105 . . . . . . 7 (φ𝑄 Q)
15 mulclnq 6360 . . . . . . . 8 ((𝐷 Q 𝐸 Q) → (𝐷 ·Q 𝐸) Q)
165, 3, 15syl2anc 391 . . . . . . 7 (φ → (𝐷 ·Q 𝐸) Q)
17 ltmnqg 6385 . . . . . . 7 ((𝑄 Q (𝐷 ·Q 𝐸) Q 𝑈 Q) → (𝑄 <Q (𝐷 ·Q 𝐸) ↔ (𝑈 ·Q 𝑄) <Q (𝑈 ·Q (𝐷 ·Q 𝐸))))
1814, 16, 6, 17syl3anc 1134 . . . . . 6 (φ → (𝑄 <Q (𝐷 ·Q 𝐸) ↔ (𝑈 ·Q 𝑄) <Q (𝑈 ·Q (𝐷 ·Q 𝐸))))
1912, 18mpbird 156 . . . . 5 (φ𝑄 <Q (𝐷 ·Q 𝐸))
2019adantr 261 . . . 4 ((φ 𝐸 (1stB)) → 𝑄 <Q (𝐷 ·Q 𝐸))
21 mullocprlem.ab . . . . . . . 8 (φ → (A P B P))
2221simpld 105 . . . . . . 7 (φA P)
23 mullocprlem.du . . . . . . . 8 (φ → (𝐷 (1stA) 𝑈 (2ndA)))
2423simpld 105 . . . . . . 7 (φ𝐷 (1stA))
2522, 24jca 290 . . . . . 6 (φ → (A P 𝐷 (1stA)))
2625adantr 261 . . . . 5 ((φ 𝐸 (1stB)) → (A P 𝐷 (1stA)))
2721simprd 107 . . . . . 6 (φB P)
2827anim1i 323 . . . . 5 ((φ 𝐸 (1stB)) → (B P 𝐸 (1stB)))
2914adantr 261 . . . . 5 ((φ 𝐸 (1stB)) → 𝑄 Q)
30 mulnqprl 6547 . . . . 5 ((((A P 𝐷 (1stA)) (B P 𝐸 (1stB))) 𝑄 Q) → (𝑄 <Q (𝐷 ·Q 𝐸) → 𝑄 (1st ‘(A ·P B))))
3126, 28, 29, 30syl21anc 1133 . . . 4 ((φ 𝐸 (1stB)) → (𝑄 <Q (𝐷 ·Q 𝐸) → 𝑄 (1st ‘(A ·P B))))
3220, 31mpd 13 . . 3 ((φ 𝐸 (1stB)) → 𝑄 (1st ‘(A ·P B)))
3332orcd 651 . 2 ((φ 𝐸 (1stB)) → (𝑄 (1st ‘(A ·P B)) 𝑅 (2nd ‘(A ·P B))))
342simprd 107 . . . . . . 7 (φ𝑇 Q)
35 mulcomnqg 6367 . . . . . . 7 ((𝑇 Q 𝑈 Q) → (𝑇 ·Q 𝑈) = (𝑈 ·Q 𝑇))
3634, 6, 35syl2anc 391 . . . . . 6 (φ → (𝑇 ·Q 𝑈) = (𝑈 ·Q 𝑇))
37 mullocprlem.tdudr . . . . . . 7 (φ → (𝑇 ·Q (𝐷 ·Q 𝑈)) <Q (𝐷 ·Q 𝑅))
38 mulclnq 6360 . . . . . . . . . 10 ((𝑇 Q 𝑈 Q) → (𝑇 ·Q 𝑈) Q)
3934, 6, 38syl2anc 391 . . . . . . . . 9 (φ → (𝑇 ·Q 𝑈) Q)
4013simprd 107 . . . . . . . . 9 (φ𝑅 Q)
41 ltmnqg 6385 . . . . . . . . 9 (((𝑇 ·Q 𝑈) Q 𝑅 Q 𝐷 Q) → ((𝑇 ·Q 𝑈) <Q 𝑅 ↔ (𝐷 ·Q (𝑇 ·Q 𝑈)) <Q (𝐷 ·Q 𝑅)))
4239, 40, 5, 41syl3anc 1134 . . . . . . . 8 (φ → ((𝑇 ·Q 𝑈) <Q 𝑅 ↔ (𝐷 ·Q (𝑇 ·Q 𝑈)) <Q (𝐷 ·Q 𝑅)))
4334, 5, 6, 8, 10caov12d 5624 . . . . . . . . 9 (φ → (𝑇 ·Q (𝐷 ·Q 𝑈)) = (𝐷 ·Q (𝑇 ·Q 𝑈)))
4443breq1d 3765 . . . . . . . 8 (φ → ((𝑇 ·Q (𝐷 ·Q 𝑈)) <Q (𝐷 ·Q 𝑅) ↔ (𝐷 ·Q (𝑇 ·Q 𝑈)) <Q (𝐷 ·Q 𝑅)))
4542, 44bitr4d 180 . . . . . . 7 (φ → ((𝑇 ·Q 𝑈) <Q 𝑅 ↔ (𝑇 ·Q (𝐷 ·Q 𝑈)) <Q (𝐷 ·Q 𝑅)))
4637, 45mpbird 156 . . . . . 6 (φ → (𝑇 ·Q 𝑈) <Q 𝑅)
4736, 46eqbrtrrd 3777 . . . . 5 (φ → (𝑈 ·Q 𝑇) <Q 𝑅)
4847adantr 261 . . . 4 ((φ 𝑇 (2ndB)) → (𝑈 ·Q 𝑇) <Q 𝑅)
4923simprd 107 . . . . . . 7 (φ𝑈 (2ndA))
5022, 49jca 290 . . . . . 6 (φ → (A P 𝑈 (2ndA)))
5150adantr 261 . . . . 5 ((φ 𝑇 (2ndB)) → (A P 𝑈 (2ndA)))
5227anim1i 323 . . . . 5 ((φ 𝑇 (2ndB)) → (B P 𝑇 (2ndB)))
5340adantr 261 . . . . 5 ((φ 𝑇 (2ndB)) → 𝑅 Q)
54 mulnqpru 6548 . . . . 5 ((((A P 𝑈 (2ndA)) (B P 𝑇 (2ndB))) 𝑅 Q) → ((𝑈 ·Q 𝑇) <Q 𝑅𝑅 (2nd ‘(A ·P B))))
5551, 52, 53, 54syl21anc 1133 . . . 4 ((φ 𝑇 (2ndB)) → ((𝑈 ·Q 𝑇) <Q 𝑅𝑅 (2nd ‘(A ·P B))))
5648, 55mpd 13 . . 3 ((φ 𝑇 (2ndB)) → 𝑅 (2nd ‘(A ·P B)))
5756olcd 652 . 2 ((φ 𝑇 (2ndB)) → (𝑄 (1st ‘(A ·P B)) 𝑅 (2nd ‘(A ·P B))))
58 mullocprlem.edutdu . . . 4 (φ → (𝐸 ·Q (𝐷 ·Q 𝑈)) <Q (𝑇 ·Q (𝐷 ·Q 𝑈)))
59 mulclnq 6360 . . . . . . 7 ((𝐷 Q 𝑈 Q) → (𝐷 ·Q 𝑈) Q)
604, 59syl 14 . . . . . 6 (φ → (𝐷 ·Q 𝑈) Q)
61 ltmnqg 6385 . . . . . 6 ((𝐸 Q 𝑇 Q (𝐷 ·Q 𝑈) Q) → (𝐸 <Q 𝑇 ↔ ((𝐷 ·Q 𝑈) ·Q 𝐸) <Q ((𝐷 ·Q 𝑈) ·Q 𝑇)))
623, 34, 60, 61syl3anc 1134 . . . . 5 (φ → (𝐸 <Q 𝑇 ↔ ((𝐷 ·Q 𝑈) ·Q 𝐸) <Q ((𝐷 ·Q 𝑈) ·Q 𝑇)))
63 mulcomnqg 6367 . . . . . . 7 (((𝐷 ·Q 𝑈) Q 𝐸 Q) → ((𝐷 ·Q 𝑈) ·Q 𝐸) = (𝐸 ·Q (𝐷 ·Q 𝑈)))
6460, 3, 63syl2anc 391 . . . . . 6 (φ → ((𝐷 ·Q 𝑈) ·Q 𝐸) = (𝐸 ·Q (𝐷 ·Q 𝑈)))
65 mulcomnqg 6367 . . . . . . 7 (((𝐷 ·Q 𝑈) Q 𝑇 Q) → ((𝐷 ·Q 𝑈) ·Q 𝑇) = (𝑇 ·Q (𝐷 ·Q 𝑈)))
6660, 34, 65syl2anc 391 . . . . . 6 (φ → ((𝐷 ·Q 𝑈) ·Q 𝑇) = (𝑇 ·Q (𝐷 ·Q 𝑈)))
6764, 66breq12d 3768 . . . . 5 (φ → (((𝐷 ·Q 𝑈) ·Q 𝐸) <Q ((𝐷 ·Q 𝑈) ·Q 𝑇) ↔ (𝐸 ·Q (𝐷 ·Q 𝑈)) <Q (𝑇 ·Q (𝐷 ·Q 𝑈))))
6862, 67bitrd 177 . . . 4 (φ → (𝐸 <Q 𝑇 ↔ (𝐸 ·Q (𝐷 ·Q 𝑈)) <Q (𝑇 ·Q (𝐷 ·Q 𝑈))))
6958, 68mpbird 156 . . 3 (φ𝐸 <Q 𝑇)
70 prop 6457 . . . 4 (B P → ⟨(1stB), (2ndB)⟩ P)
71 prloc 6473 . . . 4 ((⟨(1stB), (2ndB)⟩ P 𝐸 <Q 𝑇) → (𝐸 (1stB) 𝑇 (2ndB)))
7270, 71sylan 267 . . 3 ((B P 𝐸 <Q 𝑇) → (𝐸 (1stB) 𝑇 (2ndB)))
7327, 69, 72syl2anc 391 . 2 (φ → (𝐸 (1stB) 𝑇 (2ndB)))
7433, 57, 73mpjaodan 710 1 (φ → (𝑄 (1st ‘(A ·P B)) 𝑅 (2nd ‘(A ·P B))))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   wo 628   w3a 884   = wceq 1242   wcel 1390  cop 3370   class class class wbr 3755  cfv 4845  (class class class)co 5455  1st c1st 5707  2nd c2nd 5708  Qcnq 6264   ·Q cmq 6267   <Q cltq 6269  Pcnp 6275   ·P cmp 6278
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-coll 3863  ax-sep 3866  ax-nul 3874  ax-pow 3918  ax-pr 3935  ax-un 4136  ax-setind 4220  ax-iinf 4254
This theorem depends on definitions:  df-bi 110  df-dc 742  df-3or 885  df-3an 886  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-ral 2305  df-rex 2306  df-reu 2307  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-int 3607  df-iun 3650  df-br 3756  df-opab 3810  df-mpt 3811  df-tr 3846  df-eprel 4017  df-id 4021  df-iord 4069  df-on 4071  df-suc 4074  df-iom 4257  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-fv 4853  df-ov 5458  df-oprab 5459  df-mpt2 5460  df-1st 5709  df-2nd 5710  df-recs 5861  df-irdg 5897  df-1o 5940  df-oadd 5944  df-omul 5945  df-er 6042  df-ec 6044  df-qs 6048  df-ni 6288  df-mi 6290  df-lti 6291  df-mpq 6329  df-enq 6331  df-nqqs 6332  df-mqqs 6334  df-1nqqs 6335  df-rq 6336  df-ltnqqs 6337  df-inp 6448  df-imp 6451
This theorem is referenced by:  mullocpr  6550
  Copyright terms: Public domain W3C validator