Metamath Proof Explorer

Theorem qaddcl

Description: Closure of addition of rationals. (Contributed by NM, 1-Aug-2004)

Ref Expression
Assertion qaddcl 
|- ( ( A e. QQ /\ B e. QQ ) -> ( A + B ) e. QQ )

Proof

Step Hyp Ref Expression
1 elq 
 |-  ( A e. QQ <-> E. x e. ZZ E. y e. NN A = ( x / y ) )
2 elq 
 |-  ( B e. QQ <-> E. z e. ZZ E. w e. NN B = ( z / w ) )
3 nnz 
 |-  ( w e. NN -> w e. ZZ )
4 zmulcl 
 |-  ( ( x e. ZZ /\ w e. ZZ ) -> ( x x. w ) e. ZZ )
5 3 4 sylan2 
 |-  ( ( x e. ZZ /\ w e. NN ) -> ( x x. w ) e. ZZ )
6 5 ad2ant2rl 
 |-  ( ( ( x e. ZZ /\ y e. NN ) /\ ( z e. ZZ /\ w e. NN ) ) -> ( x x. w ) e. ZZ )
7 simpl 
 |-  ( ( z e. ZZ /\ w e. NN ) -> z e. ZZ )
8 nnz 
 |-  ( y e. NN -> y e. ZZ )
9 8 adantl 
 |-  ( ( x e. ZZ /\ y e. NN ) -> y e. ZZ )
10 zmulcl 
 |-  ( ( z e. ZZ /\ y e. ZZ ) -> ( z x. y ) e. ZZ )
11 7 9 10 syl2anr 
 |-  ( ( ( x e. ZZ /\ y e. NN ) /\ ( z e. ZZ /\ w e. NN ) ) -> ( z x. y ) e. ZZ )
12 6 11 zaddcld 
 |-  ( ( ( x e. ZZ /\ y e. NN ) /\ ( z e. ZZ /\ w e. NN ) ) -> ( ( x x. w ) + ( z x. y ) ) e. ZZ )
13 12 adantr 
 |-  ( ( ( ( x e. ZZ /\ y e. NN ) /\ ( z e. ZZ /\ w e. NN ) ) /\ ( A = ( x / y ) /\ B = ( z / w ) ) ) -> ( ( x x. w ) + ( z x. y ) ) e. ZZ )
14 nnmulcl 
 |-  ( ( y e. NN /\ w e. NN ) -> ( y x. w ) e. NN )
15 14 ad2ant2l 
 |-  ( ( ( x e. ZZ /\ y e. NN ) /\ ( z e. ZZ /\ w e. NN ) ) -> ( y x. w ) e. NN )
16 15 adantr 
 |-  ( ( ( ( x e. ZZ /\ y e. NN ) /\ ( z e. ZZ /\ w e. NN ) ) /\ ( A = ( x / y ) /\ B = ( z / w ) ) ) -> ( y x. w ) e. NN )
17 oveq12 
 |-  ( ( A = ( x / y ) /\ B = ( z / w ) ) -> ( A + B ) = ( ( x / y ) + ( z / w ) ) )
18 zcn 
 |-  ( x e. ZZ -> x e. CC )
19 zcn 
 |-  ( z e. ZZ -> z e. CC )
20 18 19 anim12i 
 |-  ( ( x e. ZZ /\ z e. ZZ ) -> ( x e. CC /\ z e. CC ) )
21 nncn 
 |-  ( y e. NN -> y e. CC )
22 nnne0 
 |-  ( y e. NN -> y =/= 0 )
23 21 22 jca 
 |-  ( y e. NN -> ( y e. CC /\ y =/= 0 ) )
24 nncn 
 |-  ( w e. NN -> w e. CC )
25 nnne0 
 |-  ( w e. NN -> w =/= 0 )
26 24 25 jca 
 |-  ( w e. NN -> ( w e. CC /\ w =/= 0 ) )
27 23 26 anim12i 
 |-  ( ( y e. NN /\ w e. NN ) -> ( ( y e. CC /\ y =/= 0 ) /\ ( w e. CC /\ w =/= 0 ) ) )
28 divadddiv 
 |-  ( ( ( x e. CC /\ z e. CC ) /\ ( ( y e. CC /\ y =/= 0 ) /\ ( w e. CC /\ w =/= 0 ) ) ) -> ( ( x / y ) + ( z / w ) ) = ( ( ( x x. w ) + ( z x. y ) ) / ( y x. w ) ) )
29 20 27 28 syl2an 
 |-  ( ( ( x e. ZZ /\ z e. ZZ ) /\ ( y e. NN /\ w e. NN ) ) -> ( ( x / y ) + ( z / w ) ) = ( ( ( x x. w ) + ( z x. y ) ) / ( y x. w ) ) )
30 29 an4s 
 |-  ( ( ( x e. ZZ /\ y e. NN ) /\ ( z e. ZZ /\ w e. NN ) ) -> ( ( x / y ) + ( z / w ) ) = ( ( ( x x. w ) + ( z x. y ) ) / ( y x. w ) ) )
31 17 30 sylan9eqr 
 |-  ( ( ( ( x e. ZZ /\ y e. NN ) /\ ( z e. ZZ /\ w e. NN ) ) /\ ( A = ( x / y ) /\ B = ( z / w ) ) ) -> ( A + B ) = ( ( ( x x. w ) + ( z x. y ) ) / ( y x. w ) ) )
32 rspceov 
 |-  ( ( ( ( x x. w ) + ( z x. y ) ) e. ZZ /\ ( y x. w ) e. NN /\ ( A + B ) = ( ( ( x x. w ) + ( z x. y ) ) / ( y x. w ) ) ) -> E. u e. ZZ E. v e. NN ( A + B ) = ( u / v ) )
33 elq 
 |-  ( ( A + B ) e. QQ <-> E. u e. ZZ E. v e. NN ( A + B ) = ( u / v ) )
34 32 33 sylibr 
 |-  ( ( ( ( x x. w ) + ( z x. y ) ) e. ZZ /\ ( y x. w ) e. NN /\ ( A + B ) = ( ( ( x x. w ) + ( z x. y ) ) / ( y x. w ) ) ) -> ( A + B ) e. QQ )
35 13 16 31 34 syl3anc 
 |-  ( ( ( ( x e. ZZ /\ y e. NN ) /\ ( z e. ZZ /\ w e. NN ) ) /\ ( A = ( x / y ) /\ B = ( z / w ) ) ) -> ( A + B ) e. QQ )
36 35 an4s 
 |-  ( ( ( ( x e. ZZ /\ y e. NN ) /\ A = ( x / y ) ) /\ ( ( z e. ZZ /\ w e. NN ) /\ B = ( z / w ) ) ) -> ( A + B ) e. QQ )
37 36 exp43 
 |-  ( ( x e. ZZ /\ y e. NN ) -> ( A = ( x / y ) -> ( ( z e. ZZ /\ w e. NN ) -> ( B = ( z / w ) -> ( A + B ) e. QQ ) ) ) )
38 37 rexlimivv 
 |-  ( E. x e. ZZ E. y e. NN A = ( x / y ) -> ( ( z e. ZZ /\ w e. NN ) -> ( B = ( z / w ) -> ( A + B ) e. QQ ) ) )
39 38 rexlimdvv 
 |-  ( E. x e. ZZ E. y e. NN A = ( x / y ) -> ( E. z e. ZZ E. w e. NN B = ( z / w ) -> ( A + B ) e. QQ ) )
40 39 imp 
 |-  ( ( E. x e. ZZ E. y e. NN A = ( x / y ) /\ E. z e. ZZ E. w e. NN B = ( z / w ) ) -> ( A + B ) e. QQ )
41 1 2 40 syl2anb 
 |-  ( ( A e. QQ /\ B e. QQ ) -> ( A + B ) e. QQ )