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

Theorem mullocprlem 6400
Description: Calculations for mullocpr 6401. (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 6228 . . . . . . . . 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 6229 . . . . . . . . 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 5595 . . . . . . 7 (φ → (𝐸 ·Q (𝐷 ·Q 𝑈)) = (𝑈 ·Q (𝐷 ·Q 𝐸)))
121, 11breqtrd 3751 . . . . . 6 (φ → (𝑈 ·Q 𝑄) <Q (𝑈 ·Q (𝐷 ·Q 𝐸)))
13 mullocprlem.qr . . . . . . . 8 (φ → (𝑄 Q 𝑅 Q))
1413simpld 105 . . . . . . 7 (φ𝑄 Q)
15 mulclnq 6221 . . . . . . . 8 ((𝐷 Q 𝐸 Q) → (𝐷 ·Q 𝐸) Q)
165, 3, 15syl2anc 391 . . . . . . 7 (φ → (𝐷 ·Q 𝐸) Q)
17 ltmnqg 6246 . . . . . . 7 ((𝑄 Q (𝐷 ·Q 𝐸) Q 𝑈 Q) → (𝑄 <Q (𝐷 ·Q 𝐸) ↔ (𝑈 ·Q 𝑄) <Q (𝑈 ·Q (𝐷 ·Q 𝐸))))
1814, 16, 6, 17syl3anc 1116 . . . . . 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 6398 . . . . 5 ((((A P 𝐷 (1stA)) (B P 𝐸 (1stB))) 𝑄 Q) → (𝑄 <Q (𝐷 ·Q 𝐸) → 𝑄 (1st ‘(A ·P B))))
3126, 28, 29, 30syl21anc 1115 . . . 4 ((φ 𝐸 (1stB)) → (𝑄 <Q (𝐷 ·Q 𝐸) → 𝑄 (1st ‘(A ·P B))))
3220, 31mpd 13 . . 3 ((φ 𝐸 (1stB)) → 𝑄 (1st ‘(A ·P B)))
3332orcd 636 . 2 ((φ 𝐸 (1stB)) → (𝑄 (1st ‘(A ·P B)) 𝑅 (2nd ‘(A ·P B))))
342simprd 107 . . . . . . 7 (φ𝑇 Q)
35 mulcomnqg 6228 . . . . . . 7 ((𝑇 Q 𝑈 Q) → (𝑇 ·Q 𝑈) = (𝑈 ·Q 𝑇))
3634, 6, 35syl2anc 391 . . . . . 6 (φ → (𝑇 ·Q 𝑈) = (𝑈 ·Q 𝑇))
37 mullocprlem.tdudr . . . . . . 7 (φ → (𝑇 ·Q (𝐷 ·Q 𝑈)) <Q (𝐷 ·Q 𝑅))
38 mulclnq 6221 . . . . . . . . . 10 ((𝑇 Q 𝑈 Q) → (𝑇 ·Q 𝑈) Q)
3934, 6, 38syl2anc 391 . . . . . . . . 9 (φ → (𝑇 ·Q 𝑈) Q)
4013simprd 107 . . . . . . . . 9 (φ𝑅 Q)
41 ltmnqg 6246 . . . . . . . . 9 (((𝑇 ·Q 𝑈) Q 𝑅 Q 𝐷 Q) → ((𝑇 ·Q 𝑈) <Q 𝑅 ↔ (𝐷 ·Q (𝑇 ·Q 𝑈)) <Q (𝐷 ·Q 𝑅)))
4239, 40, 5, 41syl3anc 1116 . . . . . . . 8 (φ → ((𝑇 ·Q 𝑈) <Q 𝑅 ↔ (𝐷 ·Q (𝑇 ·Q 𝑈)) <Q (𝐷 ·Q 𝑅)))
4334, 5, 6, 8, 10caov12d 5593 . . . . . . . . 9 (φ → (𝑇 ·Q (𝐷 ·Q 𝑈)) = (𝐷 ·Q (𝑇 ·Q 𝑈)))
4443breq1d 3737 . . . . . . . 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 3749 . . . . 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 6399 . . . . 5 ((((A P 𝑈 (2ndA)) (B P 𝑇 (2ndB))) 𝑅 Q) → ((𝑈 ·Q 𝑇) <Q 𝑅𝑅 (2nd ‘(A ·P B))))
5551, 52, 53, 54syl21anc 1115 . . . 4 ((φ 𝑇 (2ndB)) → ((𝑈 ·Q 𝑇) <Q 𝑅𝑅 (2nd ‘(A ·P B))))
5648, 55mpd 13 . . 3 ((φ 𝑇 (2ndB)) → 𝑅 (2nd ‘(A ·P B)))
5756olcd 637 . 2 ((φ 𝑇 (2ndB)) → (𝑄 (1st ‘(A ·P B)) 𝑅 (2nd ‘(A ·P B))))
58 mullocprlem.edutdu . . . 4 (φ → (𝐸 ·Q (𝐷 ·Q 𝑈)) <Q (𝑇 ·Q (𝐷 ·Q 𝑈)))
59 mulclnq 6221 . . . . . . 7 ((𝐷 Q 𝑈 Q) → (𝐷 ·Q 𝑈) Q)
604, 59syl 14 . . . . . 6 (φ → (𝐷 ·Q 𝑈) Q)
61 ltmnqg 6246 . . . . . 6 ((𝐸 Q 𝑇 Q (𝐷 ·Q 𝑈) Q) → (𝐸 <Q 𝑇 ↔ ((𝐷 ·Q 𝑈) ·Q 𝐸) <Q ((𝐷 ·Q 𝑈) ·Q 𝑇)))
623, 34, 60, 61syl3anc 1116 . . . . 5 (φ → (𝐸 <Q 𝑇 ↔ ((𝐷 ·Q 𝑈) ·Q 𝐸) <Q ((𝐷 ·Q 𝑈) ·Q 𝑇)))
63 mulcomnqg 6228 . . . . . . 7 (((𝐷 ·Q 𝑈) Q 𝐸 Q) → ((𝐷 ·Q 𝑈) ·Q 𝐸) = (𝐸 ·Q (𝐷 ·Q 𝑈)))
6460, 3, 63syl2anc 391 . . . . . 6 (φ → ((𝐷 ·Q 𝑈) ·Q 𝐸) = (𝐸 ·Q (𝐷 ·Q 𝑈)))
65 mulcomnqg 6228 . . . . . . 7 (((𝐷 ·Q 𝑈) Q 𝑇 Q) → ((𝐷 ·Q 𝑈) ·Q 𝑇) = (𝑇 ·Q (𝐷 ·Q 𝑈)))
6660, 34, 65syl2anc 391 . . . . . 6 (φ → ((𝐷 ·Q 𝑈) ·Q 𝑇) = (𝑇 ·Q (𝐷 ·Q 𝑈)))
6764, 66breq12d 3740 . . . . 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 6315 . . . 4 (B P → ⟨(1stB), (2ndB)⟩ P)
71 prloc 6331 . . . 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 695 1 (φ → (𝑄 (1st ‘(A ·P B)) 𝑅 (2nd ‘(A ·P B))))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   wo 613   w3a 867   = wceq 1223   wcel 1366  cop 3342   class class class wbr 3727  cfv 4817  (class class class)co 5424  1st c1st 5676  2nd c2nd 5677  Qcnq 6126   ·Q cmq 6129   <Q cltq 6131  Pcnp 6137   ·P cmp 6140
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 529  ax-in2 530  ax-io 614  ax-5 1309  ax-7 1310  ax-gen 1311  ax-ie1 1355  ax-ie2 1356  ax-8 1368  ax-10 1369  ax-11 1370  ax-i12 1371  ax-bnd 1372  ax-4 1373  ax-13 1377  ax-14 1378  ax-17 1392  ax-i9 1396  ax-ial 1400  ax-i5r 1401  ax-ext 1995  ax-coll 3835  ax-sep 3838  ax-nul 3846  ax-pow 3890  ax-pr 3907  ax-un 4108  ax-setind 4192  ax-iinf 4226
This theorem depends on definitions:  df-bi 110  df-dc 727  df-3or 868  df-3an 869  df-tru 1226  df-fal 1229  df-nf 1323  df-sb 1619  df-eu 1876  df-mo 1877  df-clab 2000  df-cleq 2006  df-clel 2009  df-nfc 2140  df-ne 2179  df-ral 2280  df-rex 2281  df-reu 2282  df-rab 2284  df-v 2528  df-sbc 2733  df-csb 2821  df-dif 2888  df-un 2890  df-in 2892  df-ss 2899  df-nul 3193  df-pw 3325  df-sn 3345  df-pr 3346  df-op 3348  df-uni 3544  df-int 3579  df-iun 3622  df-br 3728  df-opab 3782  df-mpt 3783  df-tr 3818  df-eprel 3989  df-id 3993  df-iord 4041  df-on 4043  df-suc 4046  df-iom 4229  df-xp 4266  df-rel 4267  df-cnv 4268  df-co 4269  df-dm 4270  df-rn 4271  df-res 4272  df-ima 4273  df-iota 4782  df-fun 4819  df-fn 4820  df-f 4821  df-f1 4822  df-fo 4823  df-f1o 4824  df-fv 4825  df-ov 5427  df-oprab 5428  df-mpt2 5429  df-1st 5678  df-2nd 5679  df-recs 5830  df-irdg 5866  df-1o 5904  df-oadd 5908  df-omul 5909  df-er 6005  df-ec 6007  df-qs 6011  df-ni 6150  df-mi 6152  df-lti 6153  df-mpq 6190  df-enq 6192  df-nqqs 6193  df-mqqs 6195  df-1nqqs 6196  df-rq 6197  df-ltnqqs 6198  df-inp 6306  df-imp 6309
This theorem is referenced by:  mullocpr  6401
  Copyright terms: Public domain W3C validator