HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem zaddclt 6122
Description: Closure of addition of integers.
Assertion
Ref Expression
zaddclt |- ((M e. ZZ /\ N e. ZZ) -> (M + N) e. ZZ)
Proof of Theorem zaddclt
StepHypRef Expression
1 nn0addclt 6077 . . . . . . . . 9 |- ((M e. NN0 /\ N e. NN0) -> (M + N) e. NN0)
21orcd 272 . . . . . . . 8 |- ((M e. NN0 /\ N e. NN0) -> ((M + N) e. NN0 \/ -u(M + N) e. NN0))
32a1i 8 . . . . . . 7 |- ((M e. RR /\ N e. RR) -> ((M e. NN0 /\ N e. NN0) -> ((M + N) e. NN0 \/ -u(M + N) e. NN0)))
4 axaddrcl 5255 . . . . . . 7 |- ((M e. RR /\ N e. RR) -> (M + N) e. RR)
53, 4jctild 600 . . . . . 6 |- ((M e. RR /\ N e. RR) -> ((M e. NN0 /\ N e. NN0) -> ((M + N) e. RR /\ ((M + N) e. NN0 \/ -u(M + N) e. NN0))))
6 letrit 5604 . . . . . . . . . . 11 |- ((-uM e. RR /\ N e. RR) -> (-uM <_ N \/ N <_ -uM))
7 renegclt 5420 . . . . . . . . . . 11 |- (M e. RR -> -uM e. RR)
86, 7sylan 448 . . . . . . . . . 10 |- ((M e. RR /\ N e. RR) -> (-uM <_ N \/ N <_ -uM))
98adantr 389 . . . . . . . . 9 |- (((M e. RR /\ N e. RR) /\ (-uM e. NN0 /\ N e. NN0)) -> (-uM <_ N \/ N <_ -uM))
10 nn0subt 6118 . . . . . . . . . . 11 |- ((-uM e. NN0 /\ N e. NN0) -> (-uM <_ N <-> (N - -uM) e. NN0))
11 subnegt 5377 . . . . . . . . . . . . . . 15 |- ((N e. CC /\ M e. CC) -> (N - -uM) = (N + M))
1211ancoms 436 . . . . . . . . . . . . . 14 |- ((M e. CC /\ N e. CC) -> (N - -uM) = (N + M))
13 axaddcom 5258 . . . . . . . . . . . . . 14 |- ((M e. CC /\ N e. CC) -> (M + N) = (N + M))
1412, 13eqtr4d 1508 . . . . . . . . . . . . 13 |- ((M e. CC /\ N e. CC) -> (N - -uM) = (M + N))
15 recnt 5296 . . . . . . . . . . . . 13 |- (M e. RR -> M e. CC)
16 recnt 5296 . . . . . . . . . . . . 13 |- (N e. RR -> N e. CC)
1714, 15, 16syl2an 454 . . . . . . . . . . . 12 |- ((M e. RR /\ N e. RR) -> (N - -uM) = (M + N))
1817eleq1d 1538 . . . . . . . . . . 11 |- ((M e. RR /\ N e. RR) -> ((N - -uM) e. NN0 <-> (M + N) e. NN0))
1910, 18sylan9bbr 540 . . . . . . . . . 10 |- (((M e. RR /\ N e. RR) /\ (-uM e. NN0 /\ N e. NN0)) -> (-uM <_ N <-> (M + N) e. NN0))
20 nn0subt 6118 . . . . . . . . . . . 12 |- ((N e. NN0 /\ -uM e. NN0) -> (N <_ -uM <-> (-uM - N) e. NN0))
2120ancoms 436 . . . . . . . . . . 11 |- ((-uM e. NN0 /\ N e. NN0) -> (N <_ -uM <-> (-uM - N) e. NN0))
22 negdit 5438 . . . . . . . . . . . . . 14 |- ((M e. CC /\ N e. CC) -> -u(M + N) = (-uM + -uN))
23 negsubt 5365 . . . . . . . . . . . . . . 15 |- ((-uM e. CC /\ N e. CC) -> (-uM + -uN) = (-uM - N))
24 negclt 5351 . . . . . . . . . . . . . . 15 |- (M e. CC -> -uM e. CC)
2523, 24sylan 448 . . . . . . . . . . . . . 14 |- ((M e. CC /\ N e. CC) -> (-uM + -uN) = (-uM - N))
2622, 25eqtr2d 1506 . . . . . . . . . . . . 13 |- ((M e. CC /\ N e. CC) -> (-uM - N) = -u(M + N))
2726, 15, 16syl2an 454 . . . . . . . . . . . 12 |- ((M e. RR /\ N e. RR) -> (-uM - N) = -u(M + N))
2827eleq1d 1538 . . . . . . . . . . 11 |- ((M e. RR /\ N e. RR) -> ((-uM - N) e. NN0 <-> -u(M + N) e. NN0))
2921, 28sylan9bbr 540 . . . . . . . . . 10 |- (((M e. RR /\ N e. RR) /\ (-uM e. NN0 /\ N e. NN0)) -> (N <_ -uM <-> -u(M + N) e. NN0))
3019, 29orbi12d 626 . . . . . . . . 9 |- (((M e. RR /\ N e. RR) /\ (-uM e. NN0 /\ N e. NN0)) -> ((-uM <_ N \/ N <_ -uM) <-> ((M + N) e. NN0 \/ -u(M + N) e. NN0)))
319, 30mpbid 195 . . . . . . . 8 |- (((M e. RR /\ N e. RR) /\ (-uM e. NN0 /\ N e. NN0)) -> ((M + N) e. NN0 \/ -u(M + N) e. NN0))
3231ex 373 . . . . . . 7 |- ((M e. RR /\ N e. RR) -> ((-uM e. NN0 /\ N e. NN0) -> ((M + N) e. NN0 \/ -u(M + N) e. NN0)))
3332, 4jctild 600 . . . . . 6 |- ((M e. RR /\ N e. RR) -> ((-uM e. NN0 /\ N e. NN0) -> ((M + N) e. RR /\ ((M + N) e. NN0 \/ -u(M + N) e. NN0))))
34 letrit 5604 . . . . . . . . . . . 12 |- ((-uN e. RR /\ M e. RR) -> (-uN <_ M \/ M <_ -uN))
35 renegclt 5420 . . . . . . . . . . . 12 |- (N e. RR -> -uN e. RR)
3634, 35sylan 448 . . . . . . . . . . 11 |- ((N e. RR /\ M e. RR) -> (-uN <_ M \/ M <_ -uN))
3736ancoms 436 . . . . . . . . . 10 |- ((M e. RR /\ N e. RR) -> (-uN <_ M \/ M <_ -uN))
3837adantr 389 . . . . . . . . 9 |- (((M e. RR /\ N e. RR) /\ (M e. NN0 /\ -uN e. NN0)) -> (-uN <_ M \/ M <_ -uN))
39 nn0subt 6118 . . . . . . . . . . . 12 |- ((-uN e. NN0 /\ M e. NN0) -> (-uN <_ M <-> (M - -uN) e. NN0))
4039ancoms 436 . . . . . . . . . . 11 |- ((M e. NN0 /\ -uN e. NN0) -> (-uN <_ M <-> (M - -uN) e. NN0))
41 subnegt 5377 . . . . . . . . . . . . 13 |- ((M e. CC /\ N e. CC) -> (M - -uN) = (M + N))
4241, 15, 16syl2an 454 . . . . . . . . . . . 12 |- ((M e. RR /\ N e. RR) -> (M - -uN) = (M + N))
4342eleq1d 1538 . . . . . . . . . . 11 |- ((M e. RR /\ N e. RR) -> ((M - -uN) e. NN0 <-> (M + N) e. NN0))
4440, 43sylan9bbr 540 . . . . . . . . . 10 |- (((M e. RR /\ N e. RR) /\ (M e. NN0 /\ -uN e. NN0)) -> (-uN <_ M <-> (M + N) e. NN0))
45 nn0subt 6118 . . . . . . . . . . 11 |- ((M e. NN0 /\ -uN e. NN0) -> (M <_ -uN <-> (-uN - M) e. NN0))
46 axaddcom 5258 . . . . . . . . . . . . . . . . 17 |- ((-uM e. CC /\ -uN e. CC) -> (-uM + -uN) = (-uN + -uM))
4746, 24sylan 448 . . . . . . . . . . . . . . . 16 |- ((M e. CC /\ -uN e. CC) -> (-uM + -uN) = (-uN + -uM))
48 negsubt 5365 . . . . . . . . . . . . . . . . 17 |- ((-uN e. CC /\ M e. CC) -> (-uN + -uM) = (-uN - M))
4948ancoms 436 . . . . . . . . . . . . . . . 16 |- ((M e. CC /\ -uN e. CC) -> (-uN + -uM) = (-uN - M))
5047, 49eqtr2d 1506 . . . . . . . . . . . . . . 15 |- ((M e. CC /\ -uN e. CC) -> (-uN - M) = (-uM + -uN))
51 negclt 5351 . . . . . . . . . . . . . . 15 |- (N e. CC -> -uN e. CC)
5250, 51sylan2 451 . . . . . . . . . . . . . 14 |- ((M e. CC /\ N e. CC) -> (-uN - M) = (-uM + -uN))
5352, 22eqtr4d 1508 . . . . . . . . . . . . 13 |- ((M e. CC /\ N e. CC) -> (-uN - M) = -u(M + N))
5453, 15, 16syl2an 454 . . . . . . . . . . . 12 |- ((M e. RR /\ N e. RR) -> (-uN - M) = -u(M + N))
5554eleq1d 1538 . . . . . . . . . . 11 |- ((M e. RR /\ N e. RR) -> ((-uN - M) e. NN0 <-> -u(M + N) e. NN0))
5645, 55sylan9bbr 540 . . . . . . . . . 10 |- (((M e. RR /\ N e. RR) /\ (M e. NN0 /\ -uN e. NN0)) -> (M <_ -uN <-> -u(M + N) e. NN0))
5744, 56orbi12d 626 . . . . . . . . 9 |- (((M e. RR /\ N e. RR) /\ (M e. NN0 /\ -uN e. NN0)) -> ((-uN <_ M \/ M <_ -uN) <-> ((M + N) e. NN0 \/ -u(M + N) e. NN0)))
5838, 57mpbid 195 . . . . . . . 8 |- (((M e. RR /\ N e. RR) /\ (M e. NN0 /\ -uN e. NN0)) -> ((M + N) e. NN0 \/ -u(M + N) e. NN0))
5958ex 373 . . . . . . 7 |- ((M e. RR /\ N e. RR) -> ((M e. NN0 /\ -uN e. NN0) -> ((M + N) e. NN0 \/ -u(M + N) e. NN0)))
6059, 4jctild 600 . . . . . 6 |- ((M e. RR /\ N e. RR) -> ((M e. NN0 /\ -uN e. NN0) -> ((M + N) e. RR /\ ((M + N) e. NN0 \/ -u(M + N) e. NN0))))
6122, 15, 16syl2an 454 . . . . . . . . . 10 |- ((M e. RR /\ N e. RR) -> -u(M + N) = (-uM + -uN))
6261eleq1d 1538 . . . . . . . . 9 |- ((M e. RR /\ N e. RR) -> (-u(M + N) e. NN0 <-> (-uM + -uN) e. NN0))
63 nn0addclt 6077 . . . . . . . . 9 |- ((-uM e. NN0 /\ -uN e. NN0) -> (-uM + -uN) e. NN0)
6462, 63syl5bir 210 . . . . . . . 8 |- ((M e. RR /\ N e. RR) -> ((-uM e. NN0 /\ -uN e. NN0) -> -u(M + N) e. NN0