Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  om00 Structured version   Unicode version

Theorem om00 7223
 Description: The product of two ordinal numbers is zero iff at least one of them is zero. Proposition 8.22 of [TakeutiZaring] p. 64. (Contributed by NM, 21-Dec-2004.)
Assertion
Ref Expression
om00

Proof of Theorem om00
StepHypRef Expression
1 neanior 2766 . . . . 5
2 eloni 4875 . . . . . . . . . 10
3 ordge1n0 7147 . . . . . . . . . 10
42, 3syl 16 . . . . . . . . 9
54biimprd 223 . . . . . . . 8
65adantr 465 . . . . . . 7
7 on0eln0 4920 . . . . . . . . 9
87adantl 466 . . . . . . . 8
9 omword1 7221 . . . . . . . . 9
109ex 434 . . . . . . . 8
118, 10sylbird 235 . . . . . . 7
126, 11anim12d 563 . . . . . 6
13 sstr 3495 . . . . . 6
1412, 13syl6 33 . . . . 5
151, 14syl5bir 218 . . . 4
16 omcl 7185 . . . . 5
17 eloni 4875 . . . . 5
18 ordge1n0 7147 . . . . 5
1916, 17, 183syl 20 . . . 4
2015, 19sylibd 214 . . 3
2120necon4bd 2663 . 2
22 oveq1 6285 . . . . . 6
23 om0r 7188 . . . . . 6
2422, 23sylan9eqr 2504 . . . . 5
2524ex 434 . . . 4