Theorem ltmul1i 6005

Description: Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20.

Hypotheses

Ref	Expression
ltmul1.1	|- A e. RR
ltmul1.2	|- B e. RR
ltmul1.3	|- C e. RR

Assertion

Ref	Expression
ltmul1i	|- (0 < C -> (A < B <-> (A x. C) < (B x. C)))

Proof of Theorem ltmul1i

Step	Hyp	Ref	Expression
1		opreq2 4070	. . . 4 |- (C = if(0 < C, C, 1) -> (A x. C) = (A x. if(0 < C, C, 1)))
2		opreq2 4070	. . . 4 |- (C = if(0 < C, C, 1) -> (B x. C) = (B x. if(0 < C, C, 1)))
3	1, 2	breq12d 2744	. . 3 |- (C = if(0 < C, C, 1) -> ((A x. C) < (B x. C) <-> (A x. if(0 < C, C, 1)) < (B x. if(0 < C, C, 1))))
4	3	bibi2d 641	. 2 |- (C = if(0 < C, C, 1) -> ((A < B <-> (A x. C) < (B x. C)) <-> (A < B <-> (A x. if(0 < C, C, 1)) < (B x. if(0 < C, C, 1)))))
5		ltmul1.1	. . 3 |- A e. RR
6		ltmul1.2	. . 3 |- B e. RR
7		ltmul1.3	. . . 4 |- C e. RR
8		1re 5632	. . . 4 |- 1 e. RR
9	7, 8	keepel 2493	. . 3 |- if(0 < C, C, 1) e. RR
10		elimgt0 5992	. . 3 |- 0 < if(0 < C, C, 1)
11	5, 6, 9, 10	ltmul1ii 6004	. 2 |- (A < B <-> (A x. if(0 < C, C, 1)) < (B x. if(0 < C, C, 1)))
12	4, 11	dedth 2474	1 |- (0 < C -> (A < B <-> (A x. C) < (B x. C)))

Syntax hints:   -> wi 3   <-> wb 152   = wceq 1018   e. wcel 1020  ifcif 2452   class class class wbr 2732  (class class class)co 4064  RRcr 5430  0cc0 5431  1c1 5432   x. cmul 5436   < clt 5683

This theorem is referenced by:  ltmul1 6013  lt2msqi 6069

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1024  ax-gen 1025  ax-8 1026  ax-9 1027  ax-10 1028  ax-11 1029  ax-12 1030  ax-13 1031  ax-14 1032  ax-17 1033  ax-4 1035  ax-5o 1037  ax-6o 1040  ax-9o 1185  ax-10o 1203  ax-16 1273  ax-11o 1281  ax-ext 1528  ax-rep 2807  ax-sep 2817  ax-nul 2824  ax-pow 2858  ax-pr 2895  ax-un 3129  ax-inf2 4813

This theorem depends on definitions:  df-bi 153  df-or 230  df-an 231  df-3or 802  df-3an 803  df-ex 1043  df-sb 1235  df-eu 1449  df-mo 1450  df-clab 1534  df-cleq 1539  df-clel 1542  df-ne 1661  df-nel 1662  df-ral 1726  df-rex 1727  df-reu 1728  df-rab 1729  df-v 1890  df-sbc 2019  df-csb 2084  df-dif 2134  df-un 2136  df-in 2138  df-ss 2140  df-pss 2142  df-nul 2368  df-if 2453  df-pw 2497  df-sn 2509  df-pr 2510  df-tp 2512  df-op 2513  df-uni 2609  df-int 2640  df-iun 2675  df-br 2733  df-opab 2781  df-tr 2795  df-eprel 2950  df-id 2953  df-po 2958  df-so 2969  df-fr 2987  df-we 3002  df-ord 3018  df-on 3019  df-lim 3020  df-suc 3021  df-om 3259  df-xp 3305  df-rel 3306  df-cnv 3307  df-co 3308  df-dm 3309  df-rn 3310  df-res 3311  df-ima 3312  df-fun 3313  df-fn 3314  df-f 3315  df-f1 3316  df-fo 3317  df-f1o 3318  df-fv 3319  df-opr 4066  df-oprab 4067  df-1st 4183  df-2nd 4184  df-rdg 4276  df-1o 4312  df-oadd 4314  df-omul 4315  df-er 4444  df-ec 4446  df-qs 4449  df-en 4552  df-dom 4553  df-sdom 4554  df-ni 5197  df-pli 5198  df-mi 5199  df-lti 5200  df-plpq 5232  df-mpq 5233  df-enq 5234  df-nq 5235  df-plq 5236  df-mq 5237  df-rq 5238  df-ltq 5239  df-1q 5240  df-np 5283  df-1p 5284  df-plp 5285  df-mp 5286  df-ltp 5287  df-plpr 5361  df-mpr 5362  df-enr 5363  df-nr 5364  df-plr 5365  df-mr 5366  df-ltr 5367  df-0r 5368  df-1r 5369  df-m1r 5370  df-c 5437  df-0 5438  df-1 5439  df-i 5440  df-r 5441  df-plus 5442  df-mul 5443  df-lt 5444  df-sub 5553  df-neg 5555  df-pnf 5684  df-mnf 5685  df-xr 5686  df-ltxr 5687  df-le 5688

Copyright terms: Public domain