Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nnmass Structured version   Visualization version   GIF version

Theorem nnmass 7749
 Description: Multiplication of natural numbers is associative. Theorem 4K(4) of [Enderton] p. 81. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
Assertion
Ref Expression
nnmass ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 ·𝑜 𝐵) ·𝑜 𝐶) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝐶)))

Proof of Theorem nnmass
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 6698 . . . . . 6 (𝑥 = 𝐶 → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = ((𝐴 ·𝑜 𝐵) ·𝑜 𝐶))
2 oveq2 6698 . . . . . . 7 (𝑥 = 𝐶 → (𝐵 ·𝑜 𝑥) = (𝐵 ·𝑜 𝐶))
32oveq2d 6706 . . . . . 6 (𝑥 = 𝐶 → (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝐶)))
41, 3eqeq12d 2666 . . . . 5 (𝑥 = 𝐶 → (((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)) ↔ ((𝐴 ·𝑜 𝐵) ·𝑜 𝐶) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝐶))))
54imbi2d 329 . . . 4 (𝑥 = 𝐶 → (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥))) ↔ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 ·𝑜 𝐵) ·𝑜 𝐶) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝐶)))))
6 oveq2 6698 . . . . . 6 (𝑥 = ∅ → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = ((𝐴 ·𝑜 𝐵) ·𝑜 ∅))
7 oveq2 6698 . . . . . . 7 (𝑥 = ∅ → (𝐵 ·𝑜 𝑥) = (𝐵 ·𝑜 ∅))
87oveq2d 6706 . . . . . 6 (𝑥 = ∅ → (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)) = (𝐴 ·𝑜 (𝐵 ·𝑜 ∅)))
96, 8eqeq12d 2666 . . . . 5 (𝑥 = ∅ → (((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)) ↔ ((𝐴 ·𝑜 𝐵) ·𝑜 ∅) = (𝐴 ·𝑜 (𝐵 ·𝑜 ∅))))
10 oveq2 6698 . . . . . 6 (𝑥 = 𝑦 → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = ((𝐴 ·𝑜 𝐵) ·𝑜 𝑦))
11 oveq2 6698 . . . . . . 7 (𝑥 = 𝑦 → (𝐵 ·𝑜 𝑥) = (𝐵 ·𝑜 𝑦))
1211oveq2d 6706 . . . . . 6 (𝑥 = 𝑦 → (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)))
1310, 12eqeq12d 2666 . . . . 5 (𝑥 = 𝑦 → (((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)) ↔ ((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦))))
14 oveq2 6698 . . . . . 6 (𝑥 = suc 𝑦 → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = ((𝐴 ·𝑜 𝐵) ·𝑜 suc 𝑦))
15 oveq2 6698 . . . . . . 7 (𝑥 = suc 𝑦 → (𝐵 ·𝑜 𝑥) = (𝐵 ·𝑜 suc 𝑦))
1615oveq2d 6706 . . . . . 6 (𝑥 = suc 𝑦 → (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)) = (𝐴 ·𝑜 (𝐵 ·𝑜 suc 𝑦)))
1714, 16eqeq12d 2666 . . . . 5 (𝑥 = suc 𝑦 → (((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥)) ↔ ((𝐴 ·𝑜 𝐵) ·𝑜 suc 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 suc 𝑦))))
18 nnmcl 7737 . . . . . . 7 ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ·𝑜 𝐵) ∈ ω)
19 nnm0 7730 . . . . . . 7 ((𝐴 ·𝑜 𝐵) ∈ ω → ((𝐴 ·𝑜 𝐵) ·𝑜 ∅) = ∅)
2018, 19syl 17 . . . . . 6 ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 ·𝑜 𝐵) ·𝑜 ∅) = ∅)
21 nnm0 7730 . . . . . . . 8 (𝐵 ∈ ω → (𝐵 ·𝑜 ∅) = ∅)
2221oveq2d 6706 . . . . . . 7 (𝐵 ∈ ω → (𝐴 ·𝑜 (𝐵 ·𝑜 ∅)) = (𝐴 ·𝑜 ∅))
23 nnm0 7730 . . . . . . 7 (𝐴 ∈ ω → (𝐴 ·𝑜 ∅) = ∅)
2422, 23sylan9eqr 2707 . . . . . 6 ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ·𝑜 (𝐵 ·𝑜 ∅)) = ∅)
2520, 24eqtr4d 2688 . . . . 5 ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 ·𝑜 𝐵) ·𝑜 ∅) = (𝐴 ·𝑜 (𝐵 ·𝑜 ∅)))
26 oveq1 6697 . . . . . . . . 9 (((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) → (((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) +𝑜 (𝐴 ·𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) +𝑜 (𝐴 ·𝑜 𝐵)))
27 nnmsuc 7732 . . . . . . . . . . 11 (((𝐴 ·𝑜 𝐵) ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ·𝑜 𝐵) ·𝑜 suc 𝑦) = (((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) +𝑜 (𝐴 ·𝑜 𝐵)))
2818, 27stoic3 1741 . . . . . . . . . 10 ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ·𝑜 𝐵) ·𝑜 suc 𝑦) = (((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) +𝑜 (𝐴 ·𝑜 𝐵)))
29 nnmsuc 7732 . . . . . . . . . . . . 13 ((𝐵 ∈ ω ∧ 𝑦 ∈ ω) → (𝐵 ·𝑜 suc 𝑦) = ((𝐵 ·𝑜 𝑦) +𝑜 𝐵))
30293adant1 1099 . . . . . . . . . . . 12 ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝑦 ∈ ω) → (𝐵 ·𝑜 suc 𝑦) = ((𝐵 ·𝑜 𝑦) +𝑜 𝐵))
3130oveq2d 6706 . . . . . . . . . . 11 ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 ·𝑜 (𝐵 ·𝑜 suc 𝑦)) = (𝐴 ·𝑜 ((𝐵 ·𝑜 𝑦) +𝑜 𝐵)))
32 nnmcl 7737 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ ω ∧ 𝑦 ∈ ω) → (𝐵 ·𝑜 𝑦) ∈ ω)
33 nndi 7748 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ω ∧ (𝐵 ·𝑜 𝑦) ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ·𝑜 ((𝐵 ·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) +𝑜 (𝐴 ·𝑜 𝐵)))
3432, 33syl3an2 1400 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ω ∧ (𝐵 ∈ ω ∧ 𝑦 ∈ ω) ∧ 𝐵 ∈ ω) → (𝐴 ·𝑜 ((𝐵 ·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) +𝑜 (𝐴 ·𝑜 𝐵)))
35343exp 1283 . . . . . . . . . . . . . . 15 (𝐴 ∈ ω → ((𝐵 ∈ ω ∧ 𝑦 ∈ ω) → (𝐵 ∈ ω → (𝐴 ·𝑜 ((𝐵 ·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) +𝑜 (𝐴 ·𝑜 𝐵)))))
3635expd 451 . . . . . . . . . . . . . 14 (𝐴 ∈ ω → (𝐵 ∈ ω → (𝑦 ∈ ω → (𝐵 ∈ ω → (𝐴 ·𝑜 ((𝐵 ·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) +𝑜 (𝐴 ·𝑜 𝐵))))))
3736com34 91 . . . . . . . . . . . . 13 (𝐴 ∈ ω → (𝐵 ∈ ω → (𝐵 ∈ ω → (𝑦 ∈ ω → (𝐴 ·𝑜 ((𝐵 ·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) +𝑜 (𝐴 ·𝑜 𝐵))))))
3837pm2.43d 53 . . . . . . . . . . . 12 (𝐴 ∈ ω → (𝐵 ∈ ω → (𝑦 ∈ ω → (𝐴 ·𝑜 ((𝐵 ·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) +𝑜 (𝐴 ·𝑜 𝐵)))))
39383imp 1275 . . . . . . . . . . 11 ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 ·𝑜 ((𝐵 ·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) +𝑜 (𝐴 ·𝑜 𝐵)))
4031, 39eqtrd 2685 . . . . . . . . . 10 ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 ·𝑜 (𝐵 ·𝑜 suc 𝑦)) = ((𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) +𝑜 (𝐴 ·𝑜 𝐵)))
4128, 40eqeq12d 2666 . . . . . . . . 9 ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝑦 ∈ ω) → (((𝐴 ·𝑜 𝐵) ·𝑜 suc 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 suc 𝑦)) ↔ (((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) +𝑜 (𝐴 ·𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) +𝑜 (𝐴 ·𝑜 𝐵))))
4226, 41syl5ibr 236 . . . . . . . 8 ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝑦 ∈ ω) → (((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) → ((𝐴 ·𝑜 𝐵) ·𝑜 suc 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 suc 𝑦))))
43423exp 1283 . . . . . . 7 (𝐴 ∈ ω → (𝐵 ∈ ω → (𝑦 ∈ ω → (((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) → ((𝐴 ·𝑜 𝐵) ·𝑜 suc 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 suc 𝑦))))))
4443com3r 87 . . . . . 6 (𝑦 ∈ ω → (𝐴 ∈ ω → (𝐵 ∈ ω → (((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) → ((𝐴 ·𝑜 𝐵) ·𝑜 suc 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 suc 𝑦))))))
4544impd 446 . . . . 5 (𝑦 ∈ ω → ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (((𝐴 ·𝑜 𝐵) ·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑦)) → ((𝐴 ·𝑜 𝐵) ·𝑜 suc 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜 suc 𝑦)))))
469, 13, 17, 25, 45finds2 7136 . . . 4 (𝑥 ∈ ω → ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 ·𝑜 𝐵) ·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝑥))))
475, 46vtoclga 3303 . . 3 (𝐶 ∈ ω → ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 ·𝑜 𝐵) ·𝑜 𝐶) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝐶))))
4847expdcom 454 . 2 (𝐴 ∈ ω → (𝐵 ∈ ω → (𝐶 ∈ ω → ((𝐴 ·𝑜 𝐵) ·𝑜 𝐶) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝐶)))))
49483imp 1275 1 ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 ·𝑜 𝐵) ·𝑜 𝐶) = (𝐴 ·𝑜 (𝐵 ·𝑜 𝐶)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030  ∅c0 3948  suc csuc 5763  (class class class)co 6690  ωcom 7107   +𝑜 coa 7602   ·𝑜 comu 7603 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-oadd 7609  df-omul 7610 This theorem is referenced by:  mulasspi  9757
 Copyright terms: Public domain W3C validator