Metamath Proof Explorer

Theorem nmuladdel

Description: Ordering relationship for natural ordinal operations. (Contributed by Scott Fenton, 15-Jul-2026)

Ref Expression
Assertion nmuladdel Could not format assertion : No typesetting found for |- ( ( ( A e. On /\ B e. On ) /\ ( C e. A /\ D e. B ) ) -> ( ( C .no B ) +no ( A .no D ) ) e. ( ( A .no B ) +no ( C .no D ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 oveq1 Could not format ( x = ( A .no B ) -> ( x +no ( c .no d ) ) = ( ( A .no B ) +no ( c .no d ) ) ) : No typesetting found for |- ( x = ( A .no B ) -> ( x +no ( c .no d ) ) = ( ( A .no B ) +no ( c .no d ) ) ) with typecode |-
2 1 eleq2d Could not format ( x = ( A .no B ) -> ( ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) <-> ( ( c .no B ) +no ( A .no d ) ) e. ( ( A .no B ) +no ( c .no d ) ) ) ) : No typesetting found for |- ( x = ( A .no B ) -> ( ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) <-> ( ( c .no B ) +no ( A .no d ) ) e. ( ( A .no B ) +no ( c .no d ) ) ) ) with typecode |-
3 2 2ralbidv Could not format ( x = ( A .no B ) -> ( A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) <-> A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( ( A .no B ) +no ( c .no d ) ) ) ) : No typesetting found for |- ( x = ( A .no B ) -> ( A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) <-> A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( ( A .no B ) +no ( c .no d ) ) ) ) with typecode |-
4 nmulval Could not format ( ( A e. On /\ B e. On ) -> ( A .no B ) = |^| { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A .no B ) = |^| { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } ) with typecode |-
5 ssrab2 Could not format { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } C_ On : No typesetting found for |- { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } C_ On with typecode |-
6 nmulcl Could not format ( ( A e. On /\ B e. On ) -> ( A .no B ) e. On ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A .no B ) e. On ) with typecode |-
7 4 6 eqeltrrd Could not format ( ( A e. On /\ B e. On ) -> |^| { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } e. On ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> |^| { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } e. On ) with typecode |-
8 rabn0 Could not format ( { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } =/= (/) <-> E. x e. On A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) ) : No typesetting found for |- ( { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } =/= (/) <-> E. x e. On A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) ) with typecode |-
9 onintrab2 Could not format ( E. x e. On A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) <-> |^| { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } e. On ) : No typesetting found for |- ( E. x e. On A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) <-> |^| { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } e. On ) with typecode |-
10 8 9 bitri Could not format ( { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } =/= (/) <-> |^| { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } e. On ) : No typesetting found for |- ( { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } =/= (/) <-> |^| { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } e. On ) with typecode |-
11 7 10 sylibr Could not format ( ( A e. On /\ B e. On ) -> { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } =/= (/) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } =/= (/) ) with typecode |-
12 onint Could not format ( ( { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } C_ On /\ { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } =/= (/) ) -> |^| { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } e. { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } ) : No typesetting found for |- ( ( { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } C_ On /\ { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } =/= (/) ) -> |^| { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } e. { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } ) with typecode |-
13 5 11 12 sylancr Could not format ( ( A e. On /\ B e. On ) -> |^| { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } e. { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> |^| { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } e. { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } ) with typecode |-
14 4 13 eqeltrd Could not format ( ( A e. On /\ B e. On ) -> ( A .no B ) e. { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A .no B ) e. { x e. On | A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( x +no ( c .no d ) ) } ) with typecode |-
15 3 14 elrabrd Could not format ( ( A e. On /\ B e. On ) -> A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( ( A .no B ) +no ( c .no d ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( ( A .no B ) +no ( c .no d ) ) ) with typecode |-
16 oveq1 Could not format ( c = C -> ( c .no B ) = ( C .no B ) ) : No typesetting found for |- ( c = C -> ( c .no B ) = ( C .no B ) ) with typecode |-
17 16 oveq1d Could not format ( c = C -> ( ( c .no B ) +no ( A .no d ) ) = ( ( C .no B ) +no ( A .no d ) ) ) : No typesetting found for |- ( c = C -> ( ( c .no B ) +no ( A .no d ) ) = ( ( C .no B ) +no ( A .no d ) ) ) with typecode |-
18 oveq1 Could not format ( c = C -> ( c .no d ) = ( C .no d ) ) : No typesetting found for |- ( c = C -> ( c .no d ) = ( C .no d ) ) with typecode |-
19 18 oveq2d Could not format ( c = C -> ( ( A .no B ) +no ( c .no d ) ) = ( ( A .no B ) +no ( C .no d ) ) ) : No typesetting found for |- ( c = C -> ( ( A .no B ) +no ( c .no d ) ) = ( ( A .no B ) +no ( C .no d ) ) ) with typecode |-
20 17 19 eleq12d Could not format ( c = C -> ( ( ( c .no B ) +no ( A .no d ) ) e. ( ( A .no B ) +no ( c .no d ) ) <-> ( ( C .no B ) +no ( A .no d ) ) e. ( ( A .no B ) +no ( C .no d ) ) ) ) : No typesetting found for |- ( c = C -> ( ( ( c .no B ) +no ( A .no d ) ) e. ( ( A .no B ) +no ( c .no d ) ) <-> ( ( C .no B ) +no ( A .no d ) ) e. ( ( A .no B ) +no ( C .no d ) ) ) ) with typecode |-
21 oveq2 Could not format ( d = D -> ( A .no d ) = ( A .no D ) ) : No typesetting found for |- ( d = D -> ( A .no d ) = ( A .no D ) ) with typecode |-
22 21 oveq2d Could not format ( d = D -> ( ( C .no B ) +no ( A .no d ) ) = ( ( C .no B ) +no ( A .no D ) ) ) : No typesetting found for |- ( d = D -> ( ( C .no B ) +no ( A .no d ) ) = ( ( C .no B ) +no ( A .no D ) ) ) with typecode |-
23 oveq2 Could not format ( d = D -> ( C .no d ) = ( C .no D ) ) : No typesetting found for |- ( d = D -> ( C .no d ) = ( C .no D ) ) with typecode |-
24 23 oveq2d Could not format ( d = D -> ( ( A .no B ) +no ( C .no d ) ) = ( ( A .no B ) +no ( C .no D ) ) ) : No typesetting found for |- ( d = D -> ( ( A .no B ) +no ( C .no d ) ) = ( ( A .no B ) +no ( C .no D ) ) ) with typecode |-
25 22 24 eleq12d Could not format ( d = D -> ( ( ( C .no B ) +no ( A .no d ) ) e. ( ( A .no B ) +no ( C .no d ) ) <-> ( ( C .no B ) +no ( A .no D ) ) e. ( ( A .no B ) +no ( C .no D ) ) ) ) : No typesetting found for |- ( d = D -> ( ( ( C .no B ) +no ( A .no d ) ) e. ( ( A .no B ) +no ( C .no d ) ) <-> ( ( C .no B ) +no ( A .no D ) ) e. ( ( A .no B ) +no ( C .no D ) ) ) ) with typecode |-
26 20 25 rspc2va Could not format ( ( ( C e. A /\ D e. B ) /\ A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( ( A .no B ) +no ( c .no d ) ) ) -> ( ( C .no B ) +no ( A .no D ) ) e. ( ( A .no B ) +no ( C .no D ) ) ) : No typesetting found for |- ( ( ( C e. A /\ D e. B ) /\ A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( ( A .no B ) +no ( c .no d ) ) ) -> ( ( C .no B ) +no ( A .no D ) ) e. ( ( A .no B ) +no ( C .no D ) ) ) with typecode |-
27 26 ancoms Could not format ( ( A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( ( A .no B ) +no ( c .no d ) ) /\ ( C e. A /\ D e. B ) ) -> ( ( C .no B ) +no ( A .no D ) ) e. ( ( A .no B ) +no ( C .no D ) ) ) : No typesetting found for |- ( ( A. c e. A A. d e. B ( ( c .no B ) +no ( A .no d ) ) e. ( ( A .no B ) +no ( c .no d ) ) /\ ( C e. A /\ D e. B ) ) -> ( ( C .no B ) +no ( A .no D ) ) e. ( ( A .no B ) +no ( C .no D ) ) ) with typecode |-
28 15 27 sylan Could not format ( ( ( A e. On /\ B e. On ) /\ ( C e. A /\ D e. B ) ) -> ( ( C .no B ) +no ( A .no D ) ) e. ( ( A .no B ) +no ( C .no D ) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On ) /\ ( C e. A /\ D e. B ) ) -> ( ( C .no B ) +no ( A .no D ) ) e. ( ( A .no B ) +no ( C .no D ) ) ) with typecode |-