This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrrid 
 |-  ( ( 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