Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isarchi2 Structured version   Visualization version   Unicode version

Theorem isarchi2 28502
 Description: Alternative way to express the predicate " is Archimedean ", for Tosets. (Contributed by Thierry Arnoux, 30-Jan-2018.)
Hypotheses
Ref Expression
isarchi2.b
isarchi2.0
isarchi2.x .g
isarchi2.l
isarchi2.t
Assertion
Ref Expression
isarchi2 Toset Archi
Distinct variable groups:   ,,,   ,,,
Allowed substitution hints:   (,,)   (,,)   (,,)   (,,)

Proof of Theorem isarchi2
StepHypRef Expression
1 isarchi2.b . . . 4
2 isarchi2.0 . . . 4
3 eqid 2451 . . . 4 <<< <<<
41, 2, 3isarchi 28499 . . 3 Toset Archi <<<
54adantr 467 . 2 Toset Archi <<<
6 simpl1l 1059 . . . . . . . 8 Toset Toset
7 simpl1r 1060 . . . . . . . . 9 Toset
8 simpr 463 . . . . . . . . . 10 Toset
98nnnn0d 10925 . . . . . . . . 9 Toset
10 simpl2 1012 . . . . . . . . 9 Toset
11 isarchi2.x . . . . . . . . . 10 .g
121, 11mulgnn0cl 16774 . . . . . . . . 9
137, 9, 10, 12syl3anc 1268 . . . . . . . 8 Toset
14 simpl3 1013 . . . . . . . 8 Toset
15 isarchi2.l . . . . . . . . . 10
16 isarchi2.t . . . . . . . . . 10
171, 15, 16tltnle 28423 . . . . . . . . 9 Toset
1817con2bid 331 . . . . . . . 8 Toset
196, 13, 14, 18syl3anc 1268 . . . . . . 7 Toset
2019rexbidva 2898 . . . . . 6 Toset
2120imbi2d 318 . . . . 5 Toset
221, 2, 11, 16isinftm 28498 . . . . . . . 8 Toset <<<
2322notbid 296 . . . . . . 7 Toset <<<
24 rexnal 2836 . . . . . . . . 9
2524imbi2i 314 . . . . . . . 8
26 imnan 424 . . . . . . . 8
2725, 26bitr2i 254 . . . . . . 7
2823, 27syl6bb 265 . . . . . 6 Toset <<<
29283adant1r 1261 . . . . 5 Toset <<<
3021, 29bitr4d 260 . . . 4 Toset <<<
31303expb 1209 . . 3 Toset <<<
32312ralbidva 2830 . 2 Toset <<<
335, 32bitr4d 260 1 Toset Archi
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 188   wa 371   w3a 985   wceq 1444   wcel 1887  wral 2737  wrex 2738   class class class wbr 4402  cfv 5582  (class class class)co 6290  cn 10609  cn0 10869  cbs 15121  cple 15197  c0g 15338  cplt 16186  Tosetctos 16279  cmnd 16535  .gcmg 16672  <<
 Copyright terms: Public domain W3C validator