Metamath Proof Explorer


Theorem axpre-mulgt0

Description: The product of two positive reals is positive. Axiom 21 of 22 for real and complex numbers, derived from ZF set theory. Note: The more general version for extended reals is axmulgt0 . This construction-dependent theorem should not be referenced directly; instead, use ax-pre-mulgt0 . (Contributed by NM, 13-May-1996) (New usage is discouraged.)

Ref Expression
Assertion axpre-mulgt0
|- ( ( A e. RR /\ B e. RR ) -> ( ( 0  0 

Proof

Step Hyp Ref Expression
1 elreal
 |-  ( A e. RR <-> E. x e. R. <. x , 0R >. = A )
2 elreal
 |-  ( B e. RR <-> E. y e. R. <. y , 0R >. = B )
3 breq2
 |-  ( <. x , 0R >. = A -> ( 0 . <-> 0 
4 3 anbi1d
 |-  ( <. x , 0R >. = A -> ( ( 0 . /\ 0 . ) <-> ( 0 . ) ) )
5 oveq1
 |-  ( <. x , 0R >. = A -> ( <. x , 0R >. x. <. y , 0R >. ) = ( A x. <. y , 0R >. ) )
6 5 breq2d
 |-  ( <. x , 0R >. = A -> ( 0 . x. <. y , 0R >. ) <-> 0 . ) ) )
7 4 6 imbi12d
 |-  ( <. x , 0R >. = A -> ( ( ( 0 . /\ 0 . ) -> 0 . x. <. y , 0R >. ) ) <-> ( ( 0 . ) -> 0 . ) ) ) )
8 breq2
 |-  ( <. y , 0R >. = B -> ( 0 . <-> 0 
9 8 anbi2d
 |-  ( <. y , 0R >. = B -> ( ( 0 . ) <-> ( 0 
10 oveq2
 |-  ( <. y , 0R >. = B -> ( A x. <. y , 0R >. ) = ( A x. B ) )
11 10 breq2d
 |-  ( <. y , 0R >. = B -> ( 0 . ) <-> 0 
12 9 11 imbi12d
 |-  ( <. y , 0R >. = B -> ( ( ( 0 . ) -> 0 . ) ) <-> ( ( 0  0 
13 df-0
 |-  0 = <. 0R , 0R >.
14 13 breq1i
 |-  ( 0 . <-> <. 0R , 0R >. . )
15 ltresr
 |-  ( <. 0R , 0R >. . <-> 0R 
16 14 15 bitri
 |-  ( 0 . <-> 0R 
17 13 breq1i
 |-  ( 0 . <-> <. 0R , 0R >. . )
18 ltresr
 |-  ( <. 0R , 0R >. . <-> 0R 
19 17 18 bitri
 |-  ( 0 . <-> 0R 
20 mulgt0sr
 |-  ( ( 0R  0R 
21 16 19 20 syl2anb
 |-  ( ( 0 . /\ 0 . ) -> 0R 
22 13 a1i
 |-  ( ( x e. R. /\ y e. R. ) -> 0 = <. 0R , 0R >. )
23 mulresr
 |-  ( ( x e. R. /\ y e. R. ) -> ( <. x , 0R >. x. <. y , 0R >. ) = <. ( x .R y ) , 0R >. )
24 22 23 breq12d
 |-  ( ( x e. R. /\ y e. R. ) -> ( 0 . x. <. y , 0R >. ) <-> <. 0R , 0R >. . ) )
25 ltresr
 |-  ( <. 0R , 0R >. . <-> 0R 
26 24 25 bitrdi
 |-  ( ( x e. R. /\ y e. R. ) -> ( 0 . x. <. y , 0R >. ) <-> 0R 
27 21 26 syl5ibr
 |-  ( ( x e. R. /\ y e. R. ) -> ( ( 0 . /\ 0 . ) -> 0 . x. <. y , 0R >. ) ) )
28 1 2 7 12 27 2gencl
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0  0