Theorem nmulval

Description: Show the value of natural multiplication. (Contributed by Scott Fenton, 10-Jun-2026)

	Ref	Expression
Assertion	nmulval	Could not format assertion : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A .no B ) = |^| { x e. On | A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		nmulprop	Could not format ( ( A e. On /\ B e. On ) -> ( ( A .no B ) e. On /\ ( A .no B ) = |^| { x e. On | A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( ( A .no B ) e. On /\ ( A .no B ) = |^| { x e. On | A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) ) with typecode |-
2	1	simprd	Could not format ( ( A e. On /\ B e. On ) -> ( A .no B ) = |^| { x e. On | A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A .no B ) = |^| { x e. On | A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) with typecode |-