Metamath Proof Explorer

Theorem naddcom

Description: Natural addition commutes. (Contributed by Scott Fenton, 26-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 oveq1 Could not format ( a = c -> ( a +no b ) = ( c +no b ) ) : No typesetting found for |- ( a = c -> ( a +no b ) = ( c +no b ) ) with typecode |-
2 oveq2 Could not format ( a = c -> ( b +no a ) = ( b +no c ) ) : No typesetting found for |- ( a = c -> ( b +no a ) = ( b +no c ) ) with typecode |-
3 1 2 eqeq12d Could not format ( a = c -> ( ( a +no b ) = ( b +no a ) <-> ( c +no b ) = ( b +no c ) ) ) : No typesetting found for |- ( a = c -> ( ( a +no b ) = ( b +no a ) <-> ( c +no b ) = ( b +no c ) ) ) with typecode |-
4 oveq2 Could not format ( b = d -> ( c +no b ) = ( c +no d ) ) : No typesetting found for |- ( b = d -> ( c +no b ) = ( c +no d ) ) with typecode |-
5 oveq1 Could not format ( b = d -> ( b +no c ) = ( d +no c ) ) : No typesetting found for |- ( b = d -> ( b +no c ) = ( d +no c ) ) with typecode |-
6 4 5 eqeq12d Could not format ( b = d -> ( ( c +no b ) = ( b +no c ) <-> ( c +no d ) = ( d +no c ) ) ) : No typesetting found for |- ( b = d -> ( ( c +no b ) = ( b +no c ) <-> ( c +no d ) = ( d +no c ) ) ) with typecode |-
7 oveq1 Could not format ( a = c -> ( a +no d ) = ( c +no d ) ) : No typesetting found for |- ( a = c -> ( a +no d ) = ( c +no d ) ) with typecode |-
8 oveq2 Could not format ( a = c -> ( d +no a ) = ( d +no c ) ) : No typesetting found for |- ( a = c -> ( d +no a ) = ( d +no c ) ) with typecode |-
9 7 8 eqeq12d Could not format ( a = c -> ( ( a +no d ) = ( d +no a ) <-> ( c +no d ) = ( d +no c ) ) ) : No typesetting found for |- ( a = c -> ( ( a +no d ) = ( d +no a ) <-> ( c +no d ) = ( d +no c ) ) ) with typecode |-
10 oveq1 Could not format ( a = A -> ( a +no b ) = ( A +no b ) ) : No typesetting found for |- ( a = A -> ( a +no b ) = ( A +no b ) ) with typecode |-
11 oveq2 Could not format ( a = A -> ( b +no a ) = ( b +no A ) ) : No typesetting found for |- ( a = A -> ( b +no a ) = ( b +no A ) ) with typecode |-
12 10 11 eqeq12d Could not format ( a = A -> ( ( a +no b ) = ( b +no a ) <-> ( A +no b ) = ( b +no A ) ) ) : No typesetting found for |- ( a = A -> ( ( a +no b ) = ( b +no a ) <-> ( A +no b ) = ( b +no A ) ) ) with typecode |-
13 oveq2 Could not format ( b = B -> ( A +no b ) = ( A +no B ) ) : No typesetting found for |- ( b = B -> ( A +no b ) = ( A +no B ) ) with typecode |-
14 oveq1 Could not format ( b = B -> ( b +no A ) = ( B +no A ) ) : No typesetting found for |- ( b = B -> ( b +no A ) = ( B +no A ) ) with typecode |-
15 13 14 eqeq12d Could not format ( b = B -> ( ( A +no b ) = ( b +no A ) <-> ( A +no B ) = ( B +no A ) ) ) : No typesetting found for |- ( b = B -> ( ( A +no b ) = ( b +no A ) <-> ( A +no B ) = ( B +no A ) ) ) with typecode |-
16 eleq1 Could not format ( ( a +no d ) = ( d +no a ) -> ( ( a +no d ) e. x <-> ( d +no a ) e. x ) ) : No typesetting found for |- ( ( a +no d ) = ( d +no a ) -> ( ( a +no d ) e. x <-> ( d +no a ) e. x ) ) with typecode |-
17 16 ralimi Could not format ( A. d e. b ( a +no d ) = ( d +no a ) -> A. d e. b ( ( a +no d ) e. x <-> ( d +no a ) e. x ) ) : No typesetting found for |- ( A. d e. b ( a +no d ) = ( d +no a ) -> A. d e. b ( ( a +no d ) e. x <-> ( d +no a ) e. x ) ) with typecode |-
18 ralbi Could not format ( A. d e. b ( ( a +no d ) e. x <-> ( d +no a ) e. x ) -> ( A. d e. b ( a +no d ) e. x <-> A. d e. b ( d +no a ) e. x ) ) : No typesetting found for |- ( A. d e. b ( ( a +no d ) e. x <-> ( d +no a ) e. x ) -> ( A. d e. b ( a +no d ) e. x <-> A. d e. b ( d +no a ) e. x ) ) with typecode |-
19 17 18 syl Could not format ( A. d e. b ( a +no d ) = ( d +no a ) -> ( A. d e. b ( a +no d ) e. x <-> A. d e. b ( d +no a ) e. x ) ) : No typesetting found for |- ( A. d e. b ( a +no d ) = ( d +no a ) -> ( A. d e. b ( a +no d ) e. x <-> A. d e. b ( d +no a ) e. x ) ) with typecode |-
20 19 3ad2ant3 Could not format ( ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) -> ( A. d e. b ( a +no d ) e. x <-> A. d e. b ( d +no a ) e. x ) ) : No typesetting found for |- ( ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) -> ( A. d e. b ( a +no d ) e. x <-> A. d e. b ( d +no a ) e. x ) ) with typecode |-
21 20 adantl Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) ) -> ( A. d e. b ( a +no d ) e. x <-> A. d e. b ( d +no a ) e. x ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) ) -> ( A. d e. b ( a +no d ) e. x <-> A. d e. b ( d +no a ) e. x ) ) with typecode |-
22 eleq1 Could not format ( ( c +no b ) = ( b +no c ) -> ( ( c +no b ) e. x <-> ( b +no c ) e. x ) ) : No typesetting found for |- ( ( c +no b ) = ( b +no c ) -> ( ( c +no b ) e. x <-> ( b +no c ) e. x ) ) with typecode |-
23 22 ralimi Could not format ( A. c e. a ( c +no b ) = ( b +no c ) -> A. c e. a ( ( c +no b ) e. x <-> ( b +no c ) e. x ) ) : No typesetting found for |- ( A. c e. a ( c +no b ) = ( b +no c ) -> A. c e. a ( ( c +no b ) e. x <-> ( b +no c ) e. x ) ) with typecode |-
24 ralbi Could not format ( A. c e. a ( ( c +no b ) e. x <-> ( b +no c ) e. x ) -> ( A. c e. a ( c +no b ) e. x <-> A. c e. a ( b +no c ) e. x ) ) : No typesetting found for |- ( A. c e. a ( ( c +no b ) e. x <-> ( b +no c ) e. x ) -> ( A. c e. a ( c +no b ) e. x <-> A. c e. a ( b +no c ) e. x ) ) with typecode |-
25 23 24 syl Could not format ( A. c e. a ( c +no b ) = ( b +no c ) -> ( A. c e. a ( c +no b ) e. x <-> A. c e. a ( b +no c ) e. x ) ) : No typesetting found for |- ( A. c e. a ( c +no b ) = ( b +no c ) -> ( A. c e. a ( c +no b ) e. x <-> A. c e. a ( b +no c ) e. x ) ) with typecode |-
26 25 3ad2ant2 Could not format ( ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) -> ( A. c e. a ( c +no b ) e. x <-> A. c e. a ( b +no c ) e. x ) ) : No typesetting found for |- ( ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) -> ( A. c e. a ( c +no b ) e. x <-> A. c e. a ( b +no c ) e. x ) ) with typecode |-
27 26 adantl Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) ) -> ( A. c e. a ( c +no b ) e. x <-> A. c e. a ( b +no c ) e. x ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) ) -> ( A. c e. a ( c +no b ) e. x <-> A. c e. a ( b +no c ) e. x ) ) with typecode |-
28 21 27 anbi12d Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) ) -> ( ( A. d e. b ( a +no d ) e. x /\ A. c e. a ( c +no b ) e. x ) <-> ( A. d e. b ( d +no a ) e. x /\ A. c e. a ( b +no c ) e. x ) ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) ) -> ( ( A. d e. b ( a +no d ) e. x /\ A. c e. a ( c +no b ) e. x ) <-> ( A. d e. b ( d +no a ) e. x /\ A. c e. a ( b +no c ) e. x ) ) ) with typecode |-
29 28 biancomd Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) ) -> ( ( A. d e. b ( a +no d ) e. x /\ A. c e. a ( c +no b ) e. x ) <-> ( A. c e. a ( b +no c ) e. x /\ A. d e. b ( d +no a ) e. x ) ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) ) -> ( ( A. d e. b ( a +no d ) e. x /\ A. c e. a ( c +no b ) e. x ) <-> ( A. c e. a ( b +no c ) e. x /\ A. d e. b ( d +no a ) e. x ) ) ) with typecode |-
30 29 rabbidv Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) ) -> { x e. On | ( A. d e. b ( a +no d ) e. x /\ A. c e. a ( c +no b ) e. x ) } = { x e. On | ( A. c e. a ( b +no c ) e. x /\ A. d e. b ( d +no a ) e. x ) } ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) ) -> { x e. On | ( A. d e. b ( a +no d ) e. x /\ A. c e. a ( c +no b ) e. x ) } = { x e. On | ( A. c e. a ( b +no c ) e. x /\ A. d e. b ( d +no a ) e. x ) } ) with typecode |-
31 30 inteqd Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) ) -> |^| { x e. On | ( A. d e. b ( a +no d ) e. x /\ A. c e. a ( c +no b ) e. x ) } = |^| { x e. On | ( A. c e. a ( b +no c ) e. x /\ A. d e. b ( d +no a ) e. x ) } ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) ) -> |^| { x e. On | ( A. d e. b ( a +no d ) e. x /\ A. c e. a ( c +no b ) e. x ) } = |^| { x e. On | ( A. c e. a ( b +no c ) e. x /\ A. d e. b ( d +no a ) e. x ) } ) with typecode |-
32 naddov2 Could not format ( ( a e. On /\ b e. On ) -> ( a +no b ) = |^| { x e. On | ( A. d e. b ( a +no d ) e. x /\ A. c e. a ( c +no b ) e. x ) } ) : No typesetting found for |- ( ( a e. On /\ b e. On ) -> ( a +no b ) = |^| { x e. On | ( A. d e. b ( a +no d ) e. x /\ A. c e. a ( c +no b ) e. x ) } ) with typecode |-
33 32 adantr Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) ) -> ( a +no b ) = |^| { x e. On | ( A. d e. b ( a +no d ) e. x /\ A. c e. a ( c +no b ) e. x ) } ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) ) -> ( a +no b ) = |^| { x e. On | ( A. d e. b ( a +no d ) e. x /\ A. c e. a ( c +no b ) e. x ) } ) with typecode |-
34 naddov2 Could not format ( ( b e. On /\ a e. On ) -> ( b +no a ) = |^| { x e. On | ( A. c e. a ( b +no c ) e. x /\ A. d e. b ( d +no a ) e. x ) } ) : No typesetting found for |- ( ( b e. On /\ a e. On ) -> ( b +no a ) = |^| { x e. On | ( A. c e. a ( b +no c ) e. x /\ A. d e. b ( d +no a ) e. x ) } ) with typecode |-
35 34 ancoms Could not format ( ( a e. On /\ b e. On ) -> ( b +no a ) = |^| { x e. On | ( A. c e. a ( b +no c ) e. x /\ A. d e. b ( d +no a ) e. x ) } ) : No typesetting found for |- ( ( a e. On /\ b e. On ) -> ( b +no a ) = |^| { x e. On | ( A. c e. a ( b +no c ) e. x /\ A. d e. b ( d +no a ) e. x ) } ) with typecode |-
36 35 adantr Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) ) -> ( b +no a ) = |^| { x e. On | ( A. c e. a ( b +no c ) e. x /\ A. d e. b ( d +no a ) e. x ) } ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) ) -> ( b +no a ) = |^| { x e. On | ( A. c e. a ( b +no c ) e. x /\ A. d e. b ( d +no a ) e. x ) } ) with typecode |-
37 31 33 36 3eqtr4d Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) ) -> ( a +no b ) = ( b +no a ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) ) -> ( a +no b ) = ( b +no a ) ) with typecode |-
38 37 ex Could not format ( ( a e. On /\ b e. On ) -> ( ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) -> ( a +no b ) = ( b +no a ) ) ) : No typesetting found for |- ( ( a e. On /\ b e. On ) -> ( ( A. c e. a A. d e. b ( c +no d ) = ( d +no c ) /\ A. c e. a ( c +no b ) = ( b +no c ) /\ A. d e. b ( a +no d ) = ( d +no a ) ) -> ( a +no b ) = ( b +no a ) ) ) with typecode |-
39 3 6 9 12 15 38 on2ind Could not format ( ( A e. On /\ B e. On ) -> ( A +no B ) = ( B +no A ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A +no B ) = ( B +no A ) ) with typecode |-