Nearby theorems
|
|
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > ILE Home > Th. List > dfgcd2 | Unicode version | ||
Description: Alternate definition of
the  operator,
see definition in
[ApostolNT] p. 15. (Contributed by
AV, 8-Aug-2021.) |
| Ref | Expression |
|---|---|
| dfgcd2 |
     ![/\](wedge.gif "/\"){kind=small} 
       
  |
, , ,
are mutually distinct and
distinct from all other variables.| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | gcdcl 11385 |
. . . . . 6
 | |
| 2 | 1 | nn0ge0d 8827 |
. . . . 5
|
| 3 | gcddvds 11382 |
. . . . 5
| |
| 4 | 3anass 931 |
. . . . . . . 8
| |
| 5 | ancom 263 |
. . . . . . . 8
| |
| 6 | 4, 5 | bitri 183 |
. . . . . . 7
|
| 7 | dvdsgcd 11428 |
. . . . . . 7
| |
| 8 | 6, 7 | sylbir 134 |
. . . . . 6
|
| 9 | 8 | ralrimiva 2458 |
. . . . 5
|
| 10 | 2, 3, 9 | 3jca 1126 |
. . . 4
|
| 11 | 10 | adantr 271 |
. . 3
|
| 12 | breq2 3871 |
. . . . 5
| |
| 13 | breq1 3870 |
. . . . . 6
| |
| 14 | breq1 3870 |
. . . . . 6
| |
| 15 | 13, 14 | anbi12d 458 |
. . . . 5
|
| 16 | breq2 3871 |
. . . . . . 7
| |
| 17 | 16 | imbi2d 229 |
. . . . . 6
|
| 18 | 17 | ralbidv 2391 |
. . . . 5
|
| 19 | 12, 15, 18 | 3anbi123d 1255 |
. . . 4
|
| 20 | 19 | adantl 272 |
. . 3
|
| 21 | 11, 20 | mpbird 166 |
. 2
|
| 22 | gcdval 11378 |
. . . 4
      
 | |
| 23 | 22 | adantr 271 |
. . 3
|
| 24 | iftrue 3418 |
. . . . . . 7
| |
| 25 | 24 | adantr 271 |
. . . . . 6
|
| 26 | breq2 3871 |
. . . . . . . . . . 11
| |
| 27 | breq2 3871 |
. . . . . . . . . . 11
| |
| 28 | 26, 27 | bi2anan9 574 |
. . . . . . . . . 10
|
| 29 | breq2 3871 |
. . . . . . . . . . . . 13
| |
| 30 | breq2 3871 |
. . . . . . . . . . . . 13
| |
| 31 | 29, 30 | bi2anan9 574 |
. . . . . . . . . . . 12
|
| 32 | 31 | imbi1d 230 |
. . . . . . . . . . 11
|
| 33 | 32 | ralbidv 2391 |
. . . . . . . . . 10
|
| 34 | 28, 33 | 3anbi23d 1258 |
. . . . . . . . 9
|
| 35 | dvdszrcl 11228 |
. . . . . . . . . . . . 13
| |
| 36 | dvds0 11238 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 37 | 36, 36 | jca 301 |
. . . . . . . . . . . . . . . . . . 19
|
| 38 | 37 | adantl 272 |
. . . . . . . . . . . . . . . . . 18
|
| 39 | pm5.5 241 |
. . . . . . . . . . . . . . . . . 18
| |
| 40 | 38, 39 | syl 14 |
. . . . . . . . . . . . . . . . 17
|
| 41 | 40 | ralbidva 2387 |
. . . . . . . . . . . . . . . 16
|
| 42 | 0z 8859 |
. . . . . . . . . . . . . . . . . . 19
| |
| 43 | breq1 3870 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 44 | 43 | rspcv 2732 |
. . . . . . . . . . . . . . . . . . 19
|
| 45 | 42, 44 | ax-mp 7 |
. . . . . . . . . . . . . . . . . 18
|
| 46 | 0dvds 11243 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 47 | 46 | biimpd 143 |
. . . . . . . . . . . . . . . . . . 19
|
| 48 | eqcom 2097 |
. . . . . . . . . . . . . . . . . . 19
| |
| 49 | 47, 48 | syl6ibr 161 |
. . . . . . . . . . . . . . . . . 18
|
| 50 | 45, 49 | syl5 32 |
. . . . . . . . . . . . . . . . 17
|
| 51 | 50 | adantr 271 |
. . . . . . . . . . . . . . . 16
|
| 52 | 41, 51 | sylbid 149 |
. . . . . . . . . . . . . . 15
|
| 53 | 52 | ex 114 |
. . . . . . . . . . . . . 14
|
| 54 | 53 | adantr 271 |
. . . . . . . . . . . . 13
|
| 55 | 35, 54 | syl 14 |
. . . . . . . . . . . 12
|
| 56 | 55 | adantr 271 |
. . . . . . . . . . 11
|
| 57 | 56 | com12 30 |
. . . . . . . . . 10
|
| 58 | 57 | 3imp 1140 |
. . . . . . . . 9
|
| 59 | 34, 58 | syl6bi 162 |
. . . . . . . 8
|
| 60 | 59 | adantld 273 |
. . . . . . 7
|
| 61 | 60 | imp 123 |
. . . . . 6
|
| 62 | 25, 61 | eqtrd 2127 |
. . . . 5
|
| 63 | 62 | ancoms 265 |
. . . 4
|
| 64 | iffalse 3421 |
. . . . . . 7
| |
| 65 | 64 | adantr 271 |
. . . . . 6
|
| 66 | lttri3 7662 |
. . . . . . . 8
| |
| 67 | 66 | adantl 272 |
. . . . . . 7
|
| 68 | dvdszrcl 11228 |
. . . . . . . . . . . 12
| |
| 69 | 68 | simpld 111 |
. . . . . . . . . . 11
|
| 70 | 69 | zred 8967 |
. . . . . . . . . 10
|
| 71 | 70 | adantr 271 |
. . . . . . . . 9
|
| 72 | 71 | 3ad2ant2 968 |
. . . . . . . 8
|
| 73 | 72 | ad2antll 476 |
. . . . . . 7
|
| 74 | breq1 3870 |
. . . . . . . . . . 11
| |
| 75 | breq1 3870 |
. . . . . . . . . . 11
| |
| 76 | 74, 75 | anbi12d 458 |
. . . . . . . . . 10
|
| 77 | 76 | elrab 2785 |
. . . . . . . . 9
|
| 78 | breq1 3870 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 79 | breq1 3870 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 80 | 78, 79 | anbi12d 458 |
. . . . . . . . . . . . . . . . . . . 20
|
| 81 | breq1 3870 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 82 | 80, 81 | imbi12d 233 |
. . . . . . . . . . . . . . . . . . 19
|
| 83 | 82 | rspcv 2732 |
. . . . . . . . . . . . . . . . . 18
|
| 84 | 83 | com23 78 |
. . . . . . . . . . . . . . . . 17
|
| 85 | 84 | imp 123 |
. . . . . . . . . . . . . . . 16
|
| 86 | 85 | ad2antrr 473 |
. . . . . . . . . . . . . . 15
|
| 87 | elnn0z 8861 |
. . . . . . . . . . . . . . . . . . . . . 22
| |
| 88 | 87 | simplbi2 378 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 89 | 88 | adantr 271 |
. . . . . . . . . . . . . . . . . . . 20
|
| 90 | 68, 89 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
|
| 91 | 90 | adantr 271 |
. . . . . . . . . . . . . . . . . 18
|
| 92 | 91 | impcom 124 |
. . . . . . . . . . . . . . . . 17
|
| 93 | zre 8852 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 94 | 93 | ad2antrr 473 |
. . . . . . . . . . . . . . . . . . . 20
|
| 95 | 94 | ad2antrl 475 |
. . . . . . . . . . . . . . . . . . 19
|
| 96 | 71 | ad3antlr 478 |
. . . . . . . . . . . . . . . . . . 19
|
| 97 | simp-5l 511 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
| |
| 98 | elnn0 8773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  | |
| 99 | 2a1 25 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 100 | breq1 3870 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
| |
| 101 | breq1 3870 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
| |
| 102 | 100, 101 | anbi12d 458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
| 103 | 102 | anbi2d 453 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
| 104 | 103 | adantr 271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 105 | simplr 498 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
| |
| 106 | zdceq 8920 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
DECID | |
| 107 | 42, 106 | mpan2 417 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
DECID
|
| 108 | ianordc 840 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
DECID
| |
| 109 | 107, 108 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
| 110 | 109 | ad2antrl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
| 111 | 105, 110 | mpbid 146 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
| 112 | dvdszrcl 11228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
| |
| 113 | 0dvds 11243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
| |
| 114 | pm2.24 589 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
| |
| 115 | 113, 114 | syl6bi 162 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
| 116 | 115 | adantl 272 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
| 117 | 112, 116 | mpcom 36 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
| 118 | 117 | adantr 271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
| 119 | 118 | com12 30 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
| 120 | dvdszrcl 11228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
| |
| 121 | 0dvds 11243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
| |
| 122 | pm2.24 589 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
| |
| 123 | 121, 122 | syl6bi 162 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
| 124 | 123 | adantl 272 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
| 125 | 120, 124 | mpcom 36 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
| 126 | 125 | adantl 272 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
| 127 | 126 | com12 30 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
| 128 | 119, 127 | jaoi 674 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
| 129 | 111, 128 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
| 130 | 129 | adantld 273 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
| 131 | 130 | adantl 272 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 132 | 104, 131 | sylbid 149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
| 133 | 132 | ex 114 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
| 134 | 99, 133 | jaoi 674 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 135 | 98, 134 | sylbi 120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 136 | 135 | impcom 124 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 137 | 136 | imp 123 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 138 | dvdsle 11272 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
| |
| 139 | 97, 137, 138 | syl2anc 404 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 140 | 139 | exp31 357 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 141 | 140 | com14 88 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 142 | 141 | imp 123 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 143 | 142 | impcom 124 |
. . . . . . . . . . . . . . . . . . . 20
|
| 144 | 143 | imp 123 |
. . . . . . . . . . . . . . . . . . 19
|
| 145 | 95, 96, 144 | lensymd 7702 |
. . . . . . . . . . . . . . . . . 18
|
| 146 | 145 | exp31 357 |
. . . . . . . . . . . . . . . . 17
|
| 147 | 92, 146 | mpan2d 420 |
. . . . . . . . . . . . . . . 16
|
| 148 | 147 | com13 80 |
. . . . . . . . . . . . . . 15
|
| 149 | 86, 148 | syld 45 |
. . . . . . . . . . . . . 14
|
| 150 | 149 | com13 80 |
. . . . . . . . . . . . 13
|
| 151 | 150 | 3impia 1143 |
. . . . . . . . . . . 12
|
| 152 | 151 | com12 30 |
. . . . . . . . . . 11
|
| 153 | 152 | expimpd 356 |
. . . . . . . . . 10
|
| 154 | 153 | expimpd 356 |
. . . . . . . . 9
|
| 155 | 77, 154 | sylbi 120 |
. . . . . . . 8
|
| 156 | 155 | impcom 124 |
. . . . . . 7
|
| 157 | 69 | adantr 271 |
. . . . . . . . . . . . 13
|
| 158 | 157 | ancri 318 |
. . . . . . . . . . . 12
|
| 159 | 158 | 3ad2ant2 968 |
. . . . . . . . . . 11
|
| 160 | 159 | ad2antll 476 |
. . . . . . . . . 10
|
| 161 | 160 | adantr 271 |
. . . . . . . . 9
|
| 162 | breq1 3870 |
. . . . . . . . . . 11
| |
| 163 | breq1 3870 |
. . . . . . . . . . 11
| |
| 164 | 162, 163 | anbi12d 458 |
. . . . . . . . . 10
|
| 165 | 164 | elrab 2785 |
. . . . . . . . 9
|
| 166 | 161, 165 | sylibr 133 |
. . . . . . . 8
|
| 167 | breq2 3871 |
. . . . . . . . 9
| |
| 168 | 167 | adantl 272 |
. . . . . . . 8
|
| 169 | simprr 500 |
. . . . . . . 8
| |
| 170 | 166, 168, 169 | rspcedvd 2742 |
. . . . . . 7
|
| 171 | 67, 73, 156, 170 | eqsuptid 6772 |
. . . . . 6
|
| 172 | 65, 171 | eqtrd 2127 |
. . . . 5
|
| 173 | 172 | ancoms 265 |
. . . 4
|
| 174 | gcdmndc 11367 |
. . . . . 6
DECID | |
| 175 | 174 | adantr 271 |
. . . . 5
DECID |
| 176 | exmiddc 785 |
. . . . 5
DECID
| |
| 177 | 175, 176 | syl 14 |
. . . 4
|
| 178 | 63, 173, 177 | mpjaodan 750 |
. . 3
|
| 179 | 23, 178 | eqtr2d 2128 |
. 2
|
| 180 | 21, 179 | impbida 564 |
1
|
| Colors of variables: wff set class |
| Syntax hints: wn 3
wi 4
wa 103
wb 104 wo 667 DECID wdc 783
w3a 927
wceq 1296
wcel 1445
wral 2370
crab 2374
cif 3413
class class class wbr 3867 (class class class)co 5690
csup 6757
cr 7446
cc0 7447
clt 7619
cle 7620
cn 8520
cn0 8771
cz 8848
cdvds 11223 cgcd 11365 |
| 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-coll 3975 ax-sep 3978 ax-nul 3986 ax-pow 4030 ax-pr 4060 ax-un 4284 ax-setind 4381 ax-iinf 4431 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-ltwlin 7555 ax-pre-lttrn 7556 ax-pre-apti 7557 ax-pre-ltadd 7558 ax-pre-mulgt0 7559 ax-pre-mulext 7560 ax-arch 7561 ax-caucvg 7562 |
| This theorem depends on definitions: df-bi 116 df-dc 784 df-3or 928 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-rmo 2378 df-rab 2379 df-v 2635 df-sbc 2855 df-csb 2948 df-dif 3015 df-un 3017 df-in 3019 df-ss 3026 df-nul 3303 df-if 3414 df-pw 3451 df-sn 3472 df-pr 3473 df-op 3475 df-uni 3676 df-int 3711 df-iun 3754 df-br 3868 df-opab 3922 df-mpt 3923 df-tr 3959 df-id 4144 df-po 4147 df-iso 4148 df-iord 4217 df-on 4219 df-ilim 4220 df-suc 4222 df-iom 4434 df-xp 4473 df-rel 4474 df-cnv 4475 df-co 4476 df-dm 4477 df-rn 4478 df-res 4479 df-ima 4480 df-iota 5014 df-fun 5051 df-fn 5052 df-f 5053 df-f1 5054 df-fo 5055 df-f1o 5056 df-fv 5057 df-riota 5646 df-ov 5693 df-oprab 5694 df-mpt2 5695 df-1st 5949 df-2nd 5950 df-recs 6108 df-frec 6194 df-sup 6759 df-pnf 7621 df-mnf 7622 df-xr 7623 df-ltxr 7624 df-le 7625 df-sub 7752 df-neg 7753 df-reap 8149 df-ap 8156 df-div 8237 df-inn 8521 df-2 8579 df-3 8580 df-4 8581 df-n0 8772 df-z 8849 df-uz 9119 df-q 9204 df-rp 9234 df-fz 9574 df-fzo 9703 df-fl 9826 df-mod 9879 df-seqfrec 10001 df-exp 10070 df-cj 10391 df-re 10392 df-im 10393 df-rsqrt 10546 df-abs 10547 df-dvds 11224 df-gcd 11366 |
| This theorem is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |