Nearby theorems
|
|
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > ILE Home > Th. List > apadd1 | Unicode version | ||
| Description: Addition respects apartness. Analogue of addcan 7759 for apartness. (Contributed by Jim Kingdon, 13-Feb-2020.) |
| Ref | Expression |
|---|---|
| apadd1 |
     ![/\](wedge.gif "/\"){kind=small} 
   #
  #
|
are mutually distinct and distinct from all other
variables.| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cnre 7581 |
. . 3
     | |
| 2 | 1 | 3ad2ant3 969 |
. 2
|
| 3 | cnre 7581 |
. . . . . . 7
| |
| 4 | 3 | 3ad2ant2 968 |
. . . . . 6
|
| 5 | 4 | ad2antrr 473 |
. . . . 5
|
| 6 | cnre 7581 |
. . . . . . . . . . 11
| |
| 7 | 6 | 3ad2ant1 967 |
. . . . . . . . . 10
|
| 8 | 7 | ad2antrr 473 |
. . . . . . . . 9
|
| 9 | 8 | ad2antrr 473 |
. . . . . . . 8
|
| 10 | simplrl 503 |
. . . . . . . . . . . 12
| |
| 11 | simplrr 504 |
. . . . . . . . . . . 12
| |
| 12 | simprl 499 |
. . . . . . . . . . . . 13
| |
| 13 | 12 | ad3antrrr 477 |
. . . . . . . . . . . 12
|
| 14 | simprr 500 |
. . . . . . . . . . . . 13
| |
| 15 | 14 | ad3antrrr 477 |
. . . . . . . . . . . 12
|
| 16 | apreim 8177 |
. . . . . . . . . . . 12
#
# 
# | |
| 17 | 10, 11, 13, 15, 16 | syl22anc 1182 |
. . . . . . . . . . 11
#
#
# |
| 18 | simpr 109 |
. . . . . . . . . . . 12
| |
| 19 | simpllr 502 |
. . . . . . . . . . . 12
| |
| 20 | 18, 19 | breq12d 3880 |
. . . . . . . . . . 11
#
# |
| 21 | simprl 499 |
. . . . . . . . . . . . . . . 16
| |
| 22 | 21 | ad2antrr 473 |
. . . . . . . . . . . . . . 15
|
| 23 | 22 | ad3antrrr 477 |
. . . . . . . . . . . . . 14
|
| 24 | 10, 23 | readdcld 7614 |
. . . . . . . . . . . . 13
|
| 25 | simprr 500 |
. . . . . . . . . . . . . . . 16
| |
| 26 | 25 | ad2antrr 473 |
. . . . . . . . . . . . . . 15
|
| 27 | 26 | ad3antrrr 477 |
. . . . . . . . . . . . . 14
|
| 28 | 11, 27 | readdcld 7614 |
. . . . . . . . . . . . 13
|
| 29 | 13, 23 | readdcld 7614 |
. . . . . . . . . . . . 13
|
| 30 | 15, 27 | readdcld 7614 |
. . . . . . . . . . . . 13
|
| 31 | apreim 8177 |
. . . . . . . . . . . . 13
#
# # | |
| 32 | 24, 28, 29, 30, 31 | syl22anc 1182 |
. . . . . . . . . . . 12
#
# # |
| 33 | 10 | recnd 7613 |
. . . . . . . . . . . . . . 15
|
| 34 | ax-icn 7537 |
. . . . . . . . . . . . . . . . 17
| |
| 35 | 34 | a1i 9 |
. . . . . . . . . . . . . . . 16
|
| 36 | 11 | recnd 7613 |
. . . . . . . . . . . . . . . 16
|
| 37 | 35, 36 | mulcld 7605 |
. . . . . . . . . . . . . . 15
|
| 38 | 23 | recnd 7613 |
. . . . . . . . . . . . . . 15
|
| 39 | 27 | recnd 7613 |
. . . . . . . . . . . . . . . 16
|
| 40 | 35, 39 | mulcld 7605 |
. . . . . . . . . . . . . . 15
|
| 41 | 33, 37, 38, 40 | add4d 7748 |
. . . . . . . . . . . . . 14
|
| 42 | simplr 498 |
. . . . . . . . . . . . . . . 16
| |
| 43 | 42 | ad3antrrr 477 |
. . . . . . . . . . . . . . 15
|
| 44 | 18, 43 | oveq12d 5708 |
. . . . . . . . . . . . . 14
|
| 45 | 35, 36, 39 | adddid 7609 |
. . . . . . . . . . . . . . 15
|
| 46 | 45 | oveq2d 5706 |
. . . . . . . . . . . . . 14
|
| 47 | 41, 44, 46 | 3eqtr4d 2137 |
. . . . . . . . . . . . 13
|
| 48 | 13 | recnd 7613 |
. . . . . . . . . . . . . . 15
|
| 49 | 15 | recnd 7613 |
. . . . . . . . . . . . . . . 16
|
| 50 | 35, 49 | mulcld 7605 |
. . . . . . . . . . . . . . 15
|
| 51 | 48, 50, 38, 40 | add4d 7748 |
. . . . . . . . . . . . . 14
|
| 52 | 19, 43 | oveq12d 5708 |
. . . . . . . . . . . . . 14
|
| 53 | 35, 49, 39 | adddid 7609 |
. . . . . . . . . . . . . . 15
|
| 54 | 53 | oveq2d 5706 |
. . . . . . . . . . . . . 14
|
| 55 | 51, 52, 54 | 3eqtr4d 2137 |
. . . . . . . . . . . . 13
|
| 56 | 47, 55 | breq12d 3880 |
. . . . . . . . . . . 12
#
# |
| 57 | reapadd1 8170 |
. . . . . . . . . . . . . 14
#
# | |
| 58 | 10, 13, 23, 57 | syl3anc 1181 |
. . . . . . . . . . . . 13
#
# |
| 59 | reapadd1 8170 |
. . . . . . . . . . . . . 14
#
# | |
| 60 | 11, 15, 27, 59 | syl3anc 1181 |
. . . . . . . . . . . . 13
#
# |
| 61 | 58, 60 | orbi12d 745 |
. . . . . . . . . . . 12
# #
# # |
| 62 | 32, 56, 61 | 3bitr4d 219 |
. . . . . . . . . . 11
#
#
# |
| 63 | 17, 20, 62 | 3bitr4d 219 |
. . . . . . . . . 10
#
#
|
| 64 | 63 | ex 114 |
. . . . . . . . 9
#
#
|
| 65 | 64 | rexlimdvva 2510 |
. . . . . . . 8
#
#
|
| 66 | 9, 65 | mpd 13 |
. . . . . . 7
#
#
|
| 67 | 66 | ex 114 |
. . . . . 6
#
#
|
| 68 | 67 | rexlimdvva 2510 |
. . . . 5
#
#
|
| 69 | 5, 68 | mpd 13 |
. . . 4
#
#
|
| 70 | 69 | ex 114 |
. . 3
#
#
|
| 71 | 70 | rexlimdvva 2510 |
. 2
#
#
|
| 72 | 2, 71 | mpd 13 |
1
#
#
|
| Colors of variables: wff set class |
| Syntax hints: wi 4
wa 103
wb 104 wo 667 w3a 927 wceq 1296 wcel 1445 wrex 2371 class class class wbr 3867
(class class class)co 5690 cc 7445 cr 7446 ci 7449 caddc 7450 cmul 7452 # cap 8155 |
| This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 582 ax-in2 583 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-13 1456 ax-14 1457 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 ax-sep 3978 ax-pow 4030 ax-pr 4060 ax-un 4284 ax-setind 4381 ax-cnex 7533 ax-resscn 7534 ax-1cn 7535 ax-1re 7536 ax-icn 7537 ax-addcl 7538 ax-addrcl 7539 ax-mulcl 7540 ax-mulrcl 7541 ax-addcom 7542 ax-mulcom 7543 ax-addass 7544 ax-mulass 7545 ax-distr 7546 ax-i2m1 7547 ax-0lt1 7548 ax-1rid 7549 ax-0id 7550 ax-rnegex 7551 ax-precex 7552 ax-cnre 7553 ax-pre-ltirr 7554 ax-pre-lttrn 7556 ax-pre-apti 7557 ax-pre-ltadd 7558 ax-pre-mulgt0 7559 |
| This theorem depends on definitions: df-bi 116 df-3an 929 df-tru 1299 df-fal 1302 df-nf 1402 df-sb 1700 df-eu 1958 df-mo 1959 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-ne 2263 df-nel 2358 df-ral 2375 df-rex 2376 df-reu 2377 df-rab 2379 df-v 2635 df-sbc 2855 df-dif 3015 df-un 3017 df-in 3019 df-ss 3026 df-pw 3451 df-sn 3472 df-pr 3473 df-op 3475 df-uni 3676 df-br 3868 df-opab 3922 df-id 4144 df-xp 4473 df-rel 4474 df-cnv 4475 df-co 4476 df-dm 4477 df-iota 5014 df-fun 5051 df-fv 5057 df-riota 5646 df-ov 5693 df-oprab 5694 df-mpt2 5695 df-pnf 7621 df-mnf 7622 df-ltxr 7624 df-sub 7752 df-neg 7753 df-reap 8149 df-ap 8156 |
| This theorem is referenced by: apadd2 8183 addext 8184 apsub1 8214 subap0 8215 subap0d 8216 |
| Copyright terms: Public domain | W3C validator |