HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem zaddclt 4590
Description: Closure of addition of integers.
Assertion
Ref Expression
zaddclt |- ((A e. ZZ /\ B e. ZZ) -> (A + B) e. ZZ)
Proof of Theorem zaddclt
StepHypRef Expression
1 axaddrcl 4067 . . . . . . . 8 |- ((A e. RR /\ B e. RR) -> (A + B) e. RR)
21a1d 14 . . . . . . 7 |- ((A e. RR /\ B e. RR) -> ((A e. NN0 /\ B e. NN0) -> (A + B) e. RR))
3 nn0addclt 4551 . . . . . . . . 9 |- ((A e. NN0 /\ B e. NN0) -> (A + B) e. NN0)
4 orc 225 . . . . . . . . 9 |- ((A + B) e. NN0 -> ((A + B) e. NN0 \/ -u(A + B) e. NN0))
53, 4syl 12 . . . . . . . 8 |- ((A e. NN0 /\ B e. NN0) -> ((A + B) e. NN0 \/ -u(A + B) e. NN0))
65a1i 7 . . . . . . 7 |- ((A e. RR /\ B e. RR) -> ((A e. NN0 /\ B e. NN0) -> ((A + B) e. NN0 \/ -u(A + B) e. NN0)))
72, 6jcad 455 . . . . . 6 |- ((A e. RR /\ B e. RR) -> ((A e. NN0 /\ B e. NN0) -> ((A + B) e. RR /\ ((A + B) e. NN0 \/ -u(A + B) e. NN0))))
81a1d 14 . . . . . . 7 |- ((A e. RR /\ B e. RR) -> ((-uA e. NN0 /\ B e. NN0) -> (A + B) e. RR))
9 letrit 4347 . . . . . . . . . . 11 |- ((-uA e. RR /\ B e. RR) -> (-uA <_ B \/ B <_ -uA))
10 renegclt 4172 . . . . . . . . . . 11 |- (A e. RR -> -uA e. RR)
119, 10sylan 343 . . . . . . . . . 10 |- ((A e. RR /\ B e. RR) -> (-uA <_ B \/ B <_ -uA))
1211adantr 306 . . . . . . . . 9 |- (((A e. RR /\ B e. RR) /\ (-uA e. NN0 /\ B e. NN0)) -> (-uA <_ B \/ B <_ -uA))
13 nn0subt 4587 . . . . . . . . . . 11 |- ((-uA e. NN0 /\ B e. NN0) -> (-uA <_ B <-> (B - -uA) e. NN0))
14 subneg2t 4158 . . . . . . . . . . . . . . 15 |- ((B e. CC /\ A e. CC) -> (B - -uA) = (B + A))
1514ancoms 334 . . . . . . . . . . . . . 14 |- ((A e. CC /\ B e. CC) -> (B - -uA) = (B + A))
16 axaddcom 4070 . . . . . . . . . . . . . 14 |- ((A e. CC /\ B e. CC) -> (A + B) = (B + A))
1715, 16eqtr4d 1131 . . . . . . . . . . . . 13 |- ((A e. CC /\ B e. CC) -> (B - -uA) = (A + B))
18 recnt 4097 . . . . . . . . . . . . 13 |- (A e. RR -> A e. CC)
19 recnt 4097 . . . . . . . . . . . . 13 |- (B e. RR -> B e. CC)
2017, 18, 19syl2an 349 . . . . . . . . . . . 12 |- ((A e. RR /\ B e. RR) -> (B - -uA) = (A + B))
2120eleq1d 1155 . . . . . . . . . . 11 |- ((A e. RR /\ B e. RR) -> ((B - -uA) e. NN0 <-> (A + B) e. NN0))
2213, 21sylan9bbr 419 . . . . . . . . . 10 |- (((A e. RR /\ B e. RR) /\ (-uA e. NN0 /\ B e. NN0)) -> (-uA <_ B <-> (A + B) e. NN0))
23 nn0subt 4587 . . . . . . . . . . . 12 |- ((B e. NN0 /\ -uA e. NN0) -> (B <_ -uA <-> (-uA - B) e. NN0))
2423ancoms 334 . . . . . . . . . . 11 |- ((-uA e. NN0 /\ B e. NN0) -> (B <_ -uA <-> (-uA - B) e. NN0))
25 subnegt 4149 . . . . . . . . . . . . . . 15 |- ((-uA e. CC /\ B e. CC) -> (-uA - B) = (-uA + -uB))
26 negclt 4141 . . . . . . . . . . . . . . 15 |- (A e. CC -> -uA e. CC)
2725, 26sylan 343 . . . . . . . . . . . . . 14 |- ((A e. CC /\ B e. CC) -> (-uA - B) = (-uA + -uB))
28 negdit 4200 . . . . . . . . . . . . . 14 |- ((A e. CC /\ B e. CC) -> -u(A + B) = (-uA + -uB))
2927, 28eqtr4d 1131 . . . . . . . . . . . . 13 |- ((A e. CC /\ B e. CC) -> (-uA - B) = -u(A + B))
3029, 18, 19syl2an 349 . . . . . . . . . . . 12 |- ((A e. RR /\ B e. RR) -> (-uA - B) = -u(A + B))
3130eleq1d 1155 . . . . . . . . . . 11 |- ((A e. RR /\ B e. RR) -> ((-uA - B) e. NN0 <-> -u(A + B) e. NN0))
3224, 31sylan9bbr 419 . . . . . . . . . 10 |- (((A e. RR /\ B e. RR) /\ (-uA e. NN0 /\ B e. NN0)) -> (B <_ -uA <-> -u(A + B) e. NN0))
3322, 32orbi12d 475 . . . . . . . . 9 |- (((A e. RR /\ B e. RR) /\ (-uA e. NN0 /\ B e. NN0)) -> ((-uA <_ B \/ B <_ -uA) <-> ((A + B) e. NN0 \/ -u(A + B) e. NN0)))
3412, 33mpbid 170 . . . . . . . 8 |- (((A e. RR /\ B e. RR) /\ (-uA e. NN0 /\ B e. NN0)) -> ((A + B) e. NN0 \/ -u(A + B) e. NN0))
3534exp 291 . . . . . . 7 |- ((A e. RR /\ B e. RR) -> ((-uA e. NN0 /\ B e. NN0) -> ((A + B) e. NN0 \/ -u(A + B) e. NN0)))
368, 35jcad 455 . . . . . 6 |- ((A e. RR /\ B e. RR) -> ((-uA e. NN0 /\ B e. NN0) -> ((A + B) e. RR /\ ((A + B) e. NN0 \/ -u(A + B) e. NN0))))
371a1d 14 . . . . . . 7 |- ((A e. RR /\ B e. RR) -> ((A e. NN0 /\ -uB e. NN0) -> (A + B) e. RR))
38 letrit 4347 . . . . . . . . . . . 12 |- ((-uB e. RR /\ A e. RR) -> (-uB <_ A \/ A <_ -uB))
39 renegclt 4172 . . . . . . . . . . . 12 |- (B e. RR -> -uB e. RR)
4038, 39sylan 343 . . . . . . . . . . 11 |- ((B e. RR /\ A e. RR) -> (-uB <_ A \/ A <_ -uB))
4140ancoms 334 . . . . . . . . . 10 |- ((A e. RR /\ B e. RR) -> (-uB <_ A \/ A <_ -uB))
4241adantr 306 . . . . . . . . 9 |- (((A e. RR /\ B e. RR) /\ (A e. NN0 /\ -uB e. NN0)) -> (-uB <_ A \/ A <_ -uB))
43 nn0subt 4587 . . . . . . . . . . . 12 |- ((-uB e. NN0 /\ A e. NN0) -> (-uB <_ A <-> (A - -uB) e. NN0))
4443ancoms 334 . . . . . . . . . . 11 |- ((A e. NN0 /\ -uB e. NN0) -> (-uB <_ A <-> (A - -uB) e. NN0))
45 subneg2t 4158 . . . . . . . . . . . . 13 |- ((A e. CC /\ B e. CC) -> (A - -uB) = (A + B))
4645, 18, 19syl2an 349 . . . . . . . . . . . 12 |- ((A e. RR /\ B e. RR) -> (A - -uB) = (A + B))
4746eleq1d 1155 . . . . . . . . . . 11 |- ((A e. RR /\ B e. RR) -> ((A - -uB) e. NN0 <-> (A + B) e. NN0))
4844, 47sylan9bbr 419 . . . . . . . . . 10 |- (((A e. RR /\ B e. RR) /\ (A e. NN0 /\ -uB e. NN0)) -> (-uB <_ A <-> (A + B) e. NN0))
49 nn0subt 4587 . . . . . . . . . . 11 |- ((A e. NN0 /\ -uB e. NN0) -> (A <_ -uB <-> (-uB - A) e. NN0))
50 subnegt 4149 . . . . . . . . . . . . . . . . 17 |- ((-uB e. CC /\ A e. CC) -> (-uB - A) = (-uB + -uA))
5150ancoms 334 . . . . . . . . . . . . . . . 16 |- ((A e. CC /\ -uB e. CC) -> (-uB - A) = (-uB + -uA))
52 axaddcom 4070 . . . . . . . . . . . . . . . . 17 |- ((-uA e. CC /\ -uB e. CC) -> (-uA + -uB) = (-uB + -uA))
5352, 26sylan 343 . . . . . . . . . . . . . . . 16 |- ((A e. CC /\ -uB e. CC) -> (-uA + -uB) = (-uB + -uA))
5451, 53eqtr4d 1131 . . . . . . . . . . . . . . 15 |- ((A e. CC /\ -uB e. CC) -> (-uB - A) = (-uA + -uB))
55 negclt 4141 . . . . . . . . . . . . . . 15 |- (B e. CC -> -uB e. CC)
5654, 55sylan2 346 . . . . . . . . . . . . . 14 |- ((A e. CC /\ B e. CC) -> (-uB - A) = (-uA + -uB))
5756, 28eqtr4d 1131 . . . . . . . . . . . . 13 |- ((A e. CC /\ B e. CC) -> (-uB - A) = -u(A + B))
5857, 18, 19syl2an 349 . . . . . . . . . . . 12 |- ((A e. RR /\ B e. RR) -> (-uB - A) = -u(A + B))
5958eleq1d 1155 . . . . . . . . . . 11 |- ((A e. RR /\ B e. RR) -> ((-uB - A) e. NN0 <-> -u(A + B) e. NN0))
6049, 59sylan9bbr 419 . . . . . . . . . 10 |- (((A e. RR /\ B e. RR) /\ (A e. NN0 /\ -uB e. NN0)) -> (A <_ -uB <-> -u(A + B) e. NN0))
6148, 60orbi12d 475 . . . . . . . . 9 |- (((A e. RR /\ B e. RR) /\ (A e. NN0 /\ -uB e. NN0)) -> ((-uB <_ A \/ A <_ -uB) <-> ((A + B) e. NN0 \/ -u(A + B) e. NN0)))
6242, 61mpbid 170 . . . . . . . 8 |- (((A e. RR /\ B e. RR) /\ (A e. NN0 /\ -uB e. NN0)) -> ((A + B) e. NN0 \/ -u(A + B) e. NN0))
6362exp 291 . . . . . . 7 |- ((A e. RR /\ B e. RR) -> ((A e. NN0 /\ -uB e. NN0) -> ((A + B) e. NN0 \/ -u(A + B) e. NN0)))
6437, 63jcad 455 . . . . . 6 |- ((A e. RR /\ B e. RR) -> ((A e. NN0 /\ -uB e. NN0) -> ((A + B) e. RR /\ ((A + B) e. NN0 \/ -u(A + B) e. NN0))))
651a1d 14 . . . . . . 7 |- ((A e. RR /\ B e. RR) -> ((-uA e. NN0 /\ -uB e. NN0) -> (A + B) e. RR))
6628, 18, 19syl2an 349 . . . . . . . . . 10 |- ((A e. RR /\ B e. RR) -> -u(A + B) = (-uA