Metamath Proof Explorer

Theorem nmulr0

Description: Natural multiplication by zero. (Contributed by Scott Fenton, 10-Jun-2026)

Ref Expression
Assertion nmulr0 Could not format assertion : No typesetting found for |- ( A e. On -> ( A .no (/) ) = (/) ) with typecode |-

Proof

Step Hyp Ref Expression
1 0elon ⊢ ∅ ∈ On
2 nmulval Could not format ( ( A e. On /\ (/) e. On ) -> ( A .no (/) ) = |^| { x e. On | A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) : No typesetting found for |- ( ( A e. On /\ (/) e. On ) -> ( A .no (/) ) = |^| { x e. On | A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) with typecode |-
3 1 2 mpan2 Could not format ( A e. On -> ( A .no (/) ) = |^| { x e. On | A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) : No typesetting found for |- ( A e. On -> ( A .no (/) ) = |^| { x e. On | A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) with typecode |-
4 ral0 Could not format A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( (/) +no ( a .no b ) ) : No typesetting found for |- A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( (/) +no ( a .no b ) ) with typecode |-
5 4 rgenw Could not format A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( (/) +no ( a .no b ) ) : No typesetting found for |- A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( (/) +no ( a .no b ) ) with typecode |-
6 oveq1 Could not format ( x = (/) -> ( x +no ( a .no b ) ) = ( (/) +no ( a .no b ) ) ) : No typesetting found for |- ( x = (/) -> ( x +no ( a .no b ) ) = ( (/) +no ( a .no b ) ) ) with typecode |-
7 6 eleq2d Could not format ( x = (/) -> ( ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) <-> ( ( a .no (/) ) +no ( A .no b ) ) e. ( (/) +no ( a .no b ) ) ) ) : No typesetting found for |- ( x = (/) -> ( ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) <-> ( ( a .no (/) ) +no ( A .no b ) ) e. ( (/) +no ( a .no b ) ) ) ) with typecode |-
8 7 2ralbidv Could not format ( x = (/) -> ( A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) <-> A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( (/) +no ( a .no b ) ) ) ) : No typesetting found for |- ( x = (/) -> ( A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) <-> A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( (/) +no ( a .no b ) ) ) ) with typecode |-
9 8 elrab3 Could not format ( (/) e. On -> ( (/) e. { x e. On | A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } <-> A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( (/) +no ( a .no b ) ) ) ) : No typesetting found for |- ( (/) e. On -> ( (/) e. { x e. On | A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } <-> A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( (/) +no ( a .no b ) ) ) ) with typecode |-
10 1 9 ax-mp Could not format ( (/) e. { x e. On | A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } <-> A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( (/) +no ( a .no b ) ) ) : No typesetting found for |- ( (/) e. { x e. On | A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } <-> A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( (/) +no ( a .no b ) ) ) with typecode |-
11 5 10 mpbir Could not format (/) e. { x e. On | A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } : No typesetting found for |- (/) e. { x e. On | A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } with typecode |-
12 int0el Could not format ( (/) e. { x e. On | A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } -> |^| { x e. On | A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } = (/) ) : No typesetting found for |- ( (/) e. { x e. On | A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } -> |^| { x e. On | A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } = (/) ) with typecode |-
13 11 12 ax-mp Could not format |^| { x e. On | A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } = (/) : No typesetting found for |- |^| { x e. On | A. a e. A A. b e. (/) ( ( a .no (/) ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } = (/) with typecode |-
14 3 13 eqtrdi Could not format ( A e. On -> ( A .no (/) ) = (/) ) : No typesetting found for |- ( A e. On -> ( A .no (/) ) = (/) ) with typecode |-