Metamath Proof Explorer

Theorem axpre-ltadd

Description: Ordering property of addition on reals. Axiom 20 of 22 for real and complex numbers, derived from ZF set theory. Note: The more general version for extended reals is axltadd . This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltadd . (Contributed by NM, 11-May-1996) (New usage is discouraged.)

Ref Expression
Assertion axpre-ltadd 
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A  ( C + A )

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 elreal 
 |-  ( C e. RR <-> E. z e. R. <. z , 0R >. = C )
4 breq1 
 |-  ( <. x , 0R >. = A -> ( <. x , 0R >. . <-> A . ) )
5 oveq2 
 |-  ( <. x , 0R >. = A -> ( <. z , 0R >. + <. x , 0R >. ) = ( <. z , 0R >. + A ) )
6 5 breq1d 
 |-  ( <. x , 0R >. = A -> ( ( <. z , 0R >. + <. x , 0R >. ) . + <. y , 0R >. ) <-> ( <. z , 0R >. + A ) . + <. y , 0R >. ) ) )
7 4 6 bibi12d 
 |-  ( <. x , 0R >. = A -> ( ( <. x , 0R >. . <-> ( <. z , 0R >. + <. x , 0R >. ) . + <. y , 0R >. ) ) <-> ( A . <-> ( <. z , 0R >. + A ) . + <. y , 0R >. ) ) ) )
8 breq2 
 |-  ( <. y , 0R >. = B -> ( A . <-> A
9 oveq2 
 |-  ( <. y , 0R >. = B -> ( <. z , 0R >. + <. y , 0R >. ) = ( <. z , 0R >. + B ) )
10 9 breq2d 
 |-  ( <. y , 0R >. = B -> ( ( <. z , 0R >. + A ) . + <. y , 0R >. ) <-> ( <. z , 0R >. + A ) . + B ) ) )
11 8 10 bibi12d 
 |-  ( <. y , 0R >. = B -> ( ( A . <-> ( <. z , 0R >. + A ) . + <. y , 0R >. ) ) <-> ( A  ( <. z , 0R >. + A ) . + B ) ) ) )
12 oveq1 
 |-  ( <. z , 0R >. = C -> ( <. z , 0R >. + A ) = ( C + A ) )
13 oveq1 
 |-  ( <. z , 0R >. = C -> ( <. z , 0R >. + B ) = ( C + B ) )
14 12 13 breq12d 
 |-  ( <. z , 0R >. = C -> ( ( <. z , 0R >. + A ) . + B ) <-> ( C + A )
15 14 bibi2d 
 |-  ( <. z , 0R >. = C -> ( ( A  ( <. z , 0R >. + A ) . + B ) ) <-> ( A  ( C + A )
16 ltasr 
 |-  ( z e. R. -> ( x  ( z +R x )
17 16 adantr 
 |-  ( ( z e. R. /\ ( x e. R. /\ y e. R. ) ) -> ( x  ( z +R x )
18 ltresr 
 |-  ( <. x , 0R >. . <-> x
19 18 a1i 
 |-  ( ( z e. R. /\ ( x e. R. /\ y e. R. ) ) -> ( <. x , 0R >. . <-> x
20 addresr 
 |-  ( ( z e. R. /\ x e. R. ) -> ( <. z , 0R >. + <. x , 0R >. ) = <. ( z +R x ) , 0R >. )
21 addresr 
 |-  ( ( z e. R. /\ y e. R. ) -> ( <. z , 0R >. + <. y , 0R >. ) = <. ( z +R y ) , 0R >. )
22 20 21 breqan12d 
 |-  ( ( ( z e. R. /\ x e. R. ) /\ ( z e. R. /\ y e. R. ) ) -> ( ( <. z , 0R >. + <. x , 0R >. ) . + <. y , 0R >. ) <-> <. ( z +R x ) , 0R >. . ) )
23 22 anandis 
 |-  ( ( z e. R. /\ ( x e. R. /\ y e. R. ) ) -> ( ( <. z , 0R >. + <. x , 0R >. ) . + <. y , 0R >. ) <-> <. ( z +R x ) , 0R >. . ) )
24 ltresr 
 |-  ( <. ( z +R x ) , 0R >. . <-> ( z +R x )
25 23 24 bitrdi 
 |-  ( ( z e. R. /\ ( x e. R. /\ y e. R. ) ) -> ( ( <. z , 0R >. + <. x , 0R >. ) . + <. y , 0R >. ) <-> ( z +R x )
26 17 19 25 3bitr4d 
 |-  ( ( z e. R. /\ ( x e. R. /\ y e. R. ) ) -> ( <. x , 0R >. . <-> ( <. z , 0R >. + <. x , 0R >. ) . + <. y , 0R >. ) ) )
27 26 ancoms 
 |-  ( ( ( x e. R. /\ y e. R. ) /\ z e. R. ) -> ( <. x , 0R >. . <-> ( <. z , 0R >. + <. x , 0R >. ) . + <. y , 0R >. ) ) )
28 27 3impa 
 |-  ( ( x e. R. /\ y e. R. /\ z e. R. ) -> ( <. x , 0R >. . <-> ( <. z , 0R >. + <. x , 0R >. ) . + <. y , 0R >. ) ) )
29 1 2 3 7 11 15 28 3gencl 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A  ( C + A )
30 29 biimpd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A  ( C + A )