Metamath Proof Explorer

Theorem om00

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)

Ref Expression
Assertion om00 
|- ( ( A e. On /\ B e. On ) -> ( ( A .o B ) = (/) <-> ( A = (/) \/ B = (/) ) ) )

Proof

Step Hyp Ref Expression
1 neanior 
 |-  ( ( A =/= (/) /\ B =/= (/) ) <-> -. ( A = (/) \/ B = (/) ) )
2 eloni 
 |-  ( A e. On -> Ord A )
3 ordge1n0 
 |-  ( Ord A -> ( 1o C_ A <-> A =/= (/) ) )
4 2 3 syl 
 |-  ( A e. On -> ( 1o C_ A <-> A =/= (/) ) )
5 4 biimprd 
 |-  ( A e. On -> ( A =/= (/) -> 1o C_ A ) )
6 5 adantr 
 |-  ( ( A e. On /\ B e. On ) -> ( A =/= (/) -> 1o C_ A ) )
7 on0eln0 
 |-  ( B e. On -> ( (/) e. B <-> B =/= (/) ) )
8 7 adantl 
 |-  ( ( A e. On /\ B e. On ) -> ( (/) e. B <-> B =/= (/) ) )
9 omword1 
 |-  ( ( ( A e. On /\ B e. On ) /\ (/) e. B ) -> A C_ ( A .o B ) )
10 9 ex 
 |-  ( ( A e. On /\ B e. On ) -> ( (/) e. B -> A C_ ( A .o B ) ) )
11 8 10 sylbird 
 |-  ( ( A e. On /\ B e. On ) -> ( B =/= (/) -> A C_ ( A .o B ) ) )
12 6 11 anim12d 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A =/= (/) /\ B =/= (/) ) -> ( 1o C_ A /\ A C_ ( A .o B ) ) ) )
13 sstr 
 |-  ( ( 1o C_ A /\ A C_ ( A .o B ) ) -> 1o C_ ( A .o B ) )
14 12 13 syl6 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A =/= (/) /\ B =/= (/) ) -> 1o C_ ( A .o B ) ) )
15 1 14 syl5bir 
 |-  ( ( A e. On /\ B e. On ) -> ( -. ( A = (/) \/ B = (/) ) -> 1o C_ ( A .o B ) ) )
16 omcl 
 |-  ( ( A e. On /\ B e. On ) -> ( A .o B ) e. On )
17 eloni 
 |-  ( ( A .o B ) e. On -> Ord ( A .o B ) )
18 ordge1n0 
 |-  ( Ord ( A .o B ) -> ( 1o C_ ( A .o B ) <-> ( A .o B ) =/= (/) ) )
19 16 17 18 3syl 
 |-  ( ( A e. On /\ B e. On ) -> ( 1o C_ ( A .o B ) <-> ( A .o B ) =/= (/) ) )
20 15 19 sylibd 
 |-  ( ( A e. On /\ B e. On ) -> ( -. ( A = (/) \/ B = (/) ) -> ( A .o B ) =/= (/) ) )
21 20 necon4bd 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A .o B ) = (/) -> ( A = (/) \/ B = (/) ) ) )
22 oveq1 
 |-  ( A = (/) -> ( A .o B ) = ( (/) .o B ) )
23 om0r 
 |-  ( B e. On -> ( (/) .o B ) = (/) )
24 22 23 sylan9eqr 
 |-  ( ( B e. On /\ A = (/) ) -> ( A .o B ) = (/) )
25 24 ex 
 |-  ( B e. On -> ( A = (/) -> ( A .o B ) = (/) ) )
26 25 adantl 
 |-  ( ( A e. On /\ B e. On ) -> ( A = (/) -> ( A .o B ) = (/) ) )
27 oveq2 
 |-  ( B = (/) -> ( A .o B ) = ( A .o (/) ) )
28 om0 
 |-  ( A e. On -> ( A .o (/) ) = (/) )
29 27 28 sylan9eqr 
 |-  ( ( A e. On /\ B = (/) ) -> ( A .o B ) = (/) )
30 29 ex 
 |-  ( A e. On -> ( B = (/) -> ( A .o B ) = (/) ) )
31 30 adantr 
 |-  ( ( A e. On /\ B e. On ) -> ( B = (/) -> ( A .o B ) = (/) ) )
32 26 31 jaod 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A = (/) \/ B = (/) ) -> ( A .o B ) = (/) ) )
33 21 32 impbid 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A .o B ) = (/) <-> ( A = (/) \/ B = (/) ) ) )