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

Theorem ltmul1 8398
 Description: Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 13-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.)
Assertion
Ref Expression
ltmul1

Proof of Theorem ltmul1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ltmul1a 8397 . . 3
21ex 114 . 2
3 recexgt0 8386 . . . 4
5 simpl1 985 . . . . . . . . . 10
6 simpl3l 1037 . . . . . . . . . 10
75, 6remulcld 7840 . . . . . . . . 9
8 simpl2 986 . . . . . . . . . 10
98, 6remulcld 7840 . . . . . . . . 9
10 simprl 521 . . . . . . . . . 10
11 simprrl 529 . . . . . . . . . 10
1210, 11jca 304 . . . . . . . . 9
137, 9, 123jca 1162 . . . . . . . 8
14 ltmul1a 8397 . . . . . . . 8
1513, 14sylan 281 . . . . . . 7
165recnd 7838 . . . . . . . . 9
1716adantr 274 . . . . . . . 8
186recnd 7838 . . . . . . . . 9
1918adantr 274 . . . . . . . 8
2010recnd 7838 . . . . . . . . 9
2120adantr 274 . . . . . . . 8
2217, 19, 21mulassd 7833 . . . . . . 7
238recnd 7838 . . . . . . . . 9
2423adantr 274 . . . . . . . 8
2524, 19, 21mulassd 7833 . . . . . . 7
2615, 22, 253brtr3d 3968 . . . . . 6
27 simprrr 530 . . . . . . . 8
2827adantr 274 . . . . . . 7
2928oveq2d 5799 . . . . . 6
3028oveq2d 5799 . . . . . 6
3126, 29, 303brtr3d 3968 . . . . 5
3217mulid1d 7827 . . . . 5
3324mulid1d 7827 . . . . 5
3431, 32, 333brtr3d 3968 . . . 4
3534ex 114 . . 3
364, 35rexlimddv 2558 . 2
372, 36impbid 128 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104   w3a 963   wceq 1332   wcel 1481  wrex 2418   class class class wbr 3938  (class class class)co 5783  cc 7662  cr 7663  cc0 7664  c1 7665   cmul 7669   clt 7844 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4055  ax-pow 4107  ax-pr 4140  ax-un 4364  ax-setind 4461  ax-cnex 7755  ax-resscn 7756  ax-1cn 7757  ax-1re 7758  ax-icn 7759  ax-addcl 7760  ax-addrcl 7761  ax-mulcl 7762  ax-mulrcl 7763  ax-addcom 7764  ax-mulcom 7765  ax-addass 7766  ax-mulass 7767  ax-distr 7768  ax-i2m1 7769  ax-1rid 7771  ax-0id 7772  ax-rnegex 7773  ax-precex 7774  ax-cnre 7775  ax-pre-ltadd 7780  ax-pre-mulgt0 7781 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2692  df-sbc 2915  df-dif 3079  df-un 3081  df-in 3083  df-ss 3090  df-pw 3518  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-br 3939  df-opab 3999  df-id 4224  df-xp 4554  df-rel 4555  df-cnv 4556  df-co 4557  df-dm 4558  df-iota 5097  df-fun 5134  df-fv 5140  df-riota 5739  df-ov 5786  df-oprab 5787  df-mpo 5788  df-pnf 7846  df-mnf 7847  df-ltxr 7849  df-sub 7979  df-neg 7980 This theorem is referenced by:  lemul1  8399  reapmul1lem  8400  ltmul2  8658  ltdiv1  8670  ltdiv23  8694  recp1lt1  8701  ltmul1i  8722  ltmul1d  9575  mertenslemi1  11356  flodddiv4t2lthalf  11690  qnumgt0  11932  tangtx  12987
 Copyright terms: Public domain W3C validator