Theorem smumul 15621

Description: For sequences that correspond to valid integers, the sequence multiplication function produces the sequence for the product. This is effectively a proof of the correctness of the multiplication process, implemented in terms of logic gates for df-sad 15579, whose correctness is verified in sadadd 15595.

Outside this range, the sequences cannot be representing integers, but the smul function still "works". This extended function is best interpreted in terms of the ring structure of the 2-adic integers. (Contributed by Mario Carneiro, 22-Sep-2016.)

Assertion

Ref	Expression
smumul	⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((bits‘𝐴) smul (bits‘𝐵)) = (bits‘(𝐴 · 𝐵)))

Proof of Theorem smumul

Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		bitsss 15554	. . . . . 6 ⊢ (bits‘𝐴) ⊆ ℕ0
2		bitsss 15554	. . . . . 6 ⊢ (bits‘𝐵) ⊆ ℕ0
3		smucl 15612	. . . . . 6 ⊢ (((bits‘𝐴) ⊆ ℕ0 ∧ (bits‘𝐵) ⊆ ℕ0) → ((bits‘𝐴) smul (bits‘𝐵)) ⊆ ℕ0)
4	1, 2, 3	mp2an 682	. . . . 5 ⊢ ((bits‘𝐴) smul (bits‘𝐵)) ⊆ ℕ0
5	4	sseli 3816	. . . 4 ⊢ (𝑘 ∈ ((bits‘𝐴) smul (bits‘𝐵)) → 𝑘 ∈ ℕ0)
6	5	a1i 11	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑘 ∈ ((bits‘𝐴) smul (bits‘𝐵)) → 𝑘 ∈ ℕ0))
7		bitsss 15554	. . . . 5 ⊢ (bits‘(𝐴 · 𝐵)) ⊆ ℕ0
8	7	sseli 3816	. . . 4 ⊢ (𝑘 ∈ (bits‘(𝐴 · 𝐵)) → 𝑘 ∈ ℕ0)
9	8	a1i 11	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑘 ∈ (bits‘(𝐴 · 𝐵)) → 𝑘 ∈ ℕ0))
10		simpll 757	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ ℤ)
11		simplr 759	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℤ)
12		simpr 479	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
13		1nn0 11660	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℕ0
14	13	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → 1 ∈ ℕ0)
15	12, 14	nn0addcld 11706	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈ ℕ0)
16	10, 11, 15	smumullem 15620	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → (((bits‘𝐴) ∩ (0..^(𝑘 + 1))) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑(𝑘 + 1))) · 𝐵)))
17	16	ineq1d 4035	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → ((((bits‘𝐴) ∩ (0..^(𝑘 + 1))) smul (bits‘𝐵)) ∩ (0..^(𝑘 + 1))) = ((bits‘((𝐴 mod (2↑(𝑘 + 1))) · 𝐵)) ∩ (0..^(𝑘 + 1))))
18		2nn 11448	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℕ
19	18	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → 2 ∈ ℕ)
20	19, 15	nnexpcld 13351	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℕ)
21	10, 20	zmodcld 13010	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → (𝐴 mod (2↑(𝑘 + 1))) ∈ ℕ0)
22	21	nn0zd 11832	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → (𝐴 mod (2↑(𝑘 + 1))) ∈ ℤ)
23	22, 11	zmulcld 11840	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → ((𝐴 mod (2↑(𝑘 + 1))) · 𝐵) ∈ ℤ)
24		bitsmod 15564	. . . . . . . . . . 11 ⊢ ((((𝐴 mod (2↑(𝑘 + 1))) · 𝐵) ∈ ℤ ∧ (𝑘 + 1) ∈ ℕ0) → (bits‘(((𝐴 mod (2↑(𝑘 + 1))) · 𝐵) mod (2↑(𝑘 + 1)))) = ((bits‘((𝐴 mod (2↑(𝑘 + 1))) · 𝐵)) ∩ (0..^(𝑘 + 1))))
25	23, 15, 24	syl2anc 579	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → (bits‘(((𝐴 mod (2↑(𝑘 + 1))) · 𝐵) mod (2↑(𝑘 + 1)))) = ((bits‘((𝐴 mod (2↑(𝑘 + 1))) · 𝐵)) ∩ (0..^(𝑘 + 1))))
26	17, 25	eqtr4d 2816	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → ((((bits‘𝐴) ∩ (0..^(𝑘 + 1))) smul (bits‘𝐵)) ∩ (0..^(𝑘 + 1))) = (bits‘(((𝐴 mod (2↑(𝑘 + 1))) · 𝐵) mod (2↑(𝑘 + 1)))))
27		inass 4043	. . . . . . . . . . . . 13 ⊢ (((bits‘𝐴) ∩ (0..^(𝑘 + 1))) ∩ (0..^(𝑘 + 1))) = ((bits‘𝐴) ∩ ((0..^(𝑘 + 1)) ∩ (0..^(𝑘 + 1))))
28		inidm 4042	. . . . . . . . . . . . . 14 ⊢ ((0..^(𝑘 + 1)) ∩ (0..^(𝑘 + 1))) = (0..^(𝑘 + 1))
29	28	ineq2i 4033	. . . . . . . . . . . . 13 ⊢ ((bits‘𝐴) ∩ ((0..^(𝑘 + 1)) ∩ (0..^(𝑘 + 1)))) = ((bits‘𝐴) ∩ (0..^(𝑘 + 1)))
30	27, 29	eqtri 2801	. . . . . . . . . . . 12 ⊢ (((bits‘𝐴) ∩ (0..^(𝑘 + 1))) ∩ (0..^(𝑘 + 1))) = ((bits‘𝐴) ∩ (0..^(𝑘 + 1)))
31	30	oveq1i 6932	. . . . . . . . . . 11 ⊢ ((((bits‘𝐴) ∩ (0..^(𝑘 + 1))) ∩ (0..^(𝑘 + 1))) smul ((bits‘𝐵) ∩ (0..^(𝑘 + 1)))) = (((bits‘𝐴) ∩ (0..^(𝑘 + 1))) smul ((bits‘𝐵) ∩ (0..^(𝑘 + 1))))
32	31	ineq1i 4032	. . . . . . . . . 10 ⊢ (((((bits‘𝐴) ∩ (0..^(𝑘 + 1))) ∩ (0..^(𝑘 + 1))) smul ((bits‘𝐵) ∩ (0..^(𝑘 + 1)))) ∩ (0..^(𝑘 + 1))) = ((((bits‘𝐴) ∩ (0..^(𝑘 + 1))) smul ((bits‘𝐵) ∩ (0..^(𝑘 + 1)))) ∩ (0..^(𝑘 + 1)))
33		inss1 4052	. . . . . . . . . . . 12 ⊢ ((bits‘𝐴) ∩ (0..^(𝑘 + 1))) ⊆ (bits‘𝐴)
34	1	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → (bits‘𝐴) ⊆ ℕ0)
35	33, 34	syl5ss 3831	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → ((bits‘𝐴) ∩ (0..^(𝑘 + 1))) ⊆ ℕ0)
36	2	a1i 11	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → (bits‘𝐵) ⊆ ℕ0)
37	35, 36, 15	smueq 15619	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → ((((bits‘𝐴) ∩ (0..^(𝑘 + 1))) smul (bits‘𝐵)) ∩ (0..^(𝑘 + 1))) = (((((bits‘𝐴) ∩ (0..^(𝑘 + 1))) ∩ (0..^(𝑘 + 1))) smul ((bits‘𝐵) ∩ (0..^(𝑘 + 1)))) ∩ (0..^(𝑘 + 1))))
38	34, 36, 15	smueq 15619	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → (((bits‘𝐴) smul (bits‘𝐵)) ∩ (0..^(𝑘 + 1))) = ((((bits‘𝐴) ∩ (0..^(𝑘 + 1))) smul ((bits‘𝐵) ∩ (0..^(𝑘 + 1)))) ∩ (0..^(𝑘 + 1))))
39	32, 37, 38	3eqtr4a 2839	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → ((((bits‘𝐴) ∩ (0..^(𝑘 + 1))) smul (bits‘𝐵)) ∩ (0..^(𝑘 + 1))) = (((bits‘𝐴) smul (bits‘𝐵)) ∩ (0..^(𝑘 + 1))))
40	20	nnrpd 12179	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℝ+)
41	10	zred 11834	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ ℝ)
42		modabs2 13023	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ (2↑(𝑘 + 1)) ∈ ℝ+) → ((𝐴 mod (2↑(𝑘 + 1))) mod (2↑(𝑘 + 1))) = (𝐴 mod (2↑(𝑘 + 1))))
43	41, 40, 42	syl2anc 579	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → ((𝐴 mod (2↑(𝑘 + 1))) mod (2↑(𝑘 + 1))) = (𝐴 mod (2↑(𝑘 + 1))))
44		eqidd 2778	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → (𝐵 mod (2↑(𝑘 + 1))) = (𝐵 mod (2↑(𝑘 + 1))))
45	22, 10, 11, 11, 40, 43, 44	modmul12d 13043	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → (((𝐴 mod (2↑(𝑘 + 1))) · 𝐵) mod (2↑(𝑘 + 1))) = ((𝐴 · 𝐵) mod (2↑(𝑘 + 1))))
46	45	fveq2d 6450	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → (bits‘(((𝐴 mod (2↑(𝑘 + 1))) · 𝐵) mod (2↑(𝑘 + 1)))) = (bits‘((𝐴 · 𝐵) mod (2↑(𝑘 + 1)))))
47	26, 39, 46	3eqtr3d 2821	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → (((bits‘𝐴) smul (bits‘𝐵)) ∩ (0..^(𝑘 + 1))) = (bits‘((𝐴 · 𝐵) mod (2↑(𝑘 + 1)))))
48	10, 11	zmulcld 11840	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → (𝐴 · 𝐵) ∈ ℤ)
49		bitsmod 15564	. . . . . . . . 9 ⊢ (((𝐴 · 𝐵) ∈ ℤ ∧ (𝑘 + 1) ∈ ℕ0) → (bits‘((𝐴 · 𝐵) mod (2↑(𝑘 + 1)))) = ((bits‘(𝐴 · 𝐵)) ∩ (0..^(𝑘 + 1))))
50	48, 15, 49	syl2anc 579	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → (bits‘((𝐴 · 𝐵) mod (2↑(𝑘 + 1)))) = ((bits‘(𝐴 · 𝐵)) ∩ (0..^(𝑘 + 1))))
51	47, 50	eqtrd 2813	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → (((bits‘𝐴) smul (bits‘𝐵)) ∩ (0..^(𝑘 + 1))) = ((bits‘(𝐴 · 𝐵)) ∩ (0..^(𝑘 + 1))))
52	51	eleq2d 2844	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ (((bits‘𝐴) smul (bits‘𝐵)) ∩ (0..^(𝑘 + 1))) ↔ 𝑘 ∈ ((bits‘(𝐴 · 𝐵)) ∩ (0..^(𝑘 + 1)))))
53		elin 4018	. . . . . 6 ⊢ (𝑘 ∈ (((bits‘𝐴) smul (bits‘𝐵)) ∩ (0..^(𝑘 + 1))) ↔ (𝑘 ∈ ((bits‘𝐴) smul (bits‘𝐵)) ∧ 𝑘 ∈ (0..^(𝑘 + 1))))
54		elin 4018	. . . . . 6 ⊢ (𝑘 ∈ ((bits‘(𝐴 · 𝐵)) ∩ (0..^(𝑘 + 1))) ↔ (𝑘 ∈ (bits‘(𝐴 · 𝐵)) ∧ 𝑘 ∈ (0..^(𝑘 + 1))))
55	52, 53, 54	3bitr3g 305	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → ((𝑘 ∈ ((bits‘𝐴) smul (bits‘𝐵)) ∧ 𝑘 ∈ (0..^(𝑘 + 1))) ↔ (𝑘 ∈ (bits‘(𝐴 · 𝐵)) ∧ 𝑘 ∈ (0..^(𝑘 + 1)))))
56		nn0uz 12028	. . . . . . . . 9 ⊢ ℕ0 = (ℤ≥‘0)
57	12, 56	syl6eleq 2868	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ (ℤ≥‘0))
58		eluzfz2b 12667	. . . . . . . 8 ⊢ (𝑘 ∈ (ℤ≥‘0) ↔ 𝑘 ∈ (0...𝑘))
59	57, 58	sylib 210	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ (0...𝑘))
60	12	nn0zd 11832	. . . . . . . 8 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℤ)
61		fzval3 12856	. . . . . . . 8 ⊢ (𝑘 ∈ ℤ → (0...𝑘) = (0..^(𝑘 + 1)))
62	60, 61	syl 17	. . . . . . 7 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → (0...𝑘) = (0..^(𝑘 + 1)))
63	59, 62	eleqtrd 2860	. . . . . 6 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ (0..^(𝑘 + 1)))
64	63	biantrud 527	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ ((bits‘𝐴) smul (bits‘𝐵)) ↔ (𝑘 ∈ ((bits‘𝐴) smul (bits‘𝐵)) ∧ 𝑘 ∈ (0..^(𝑘 + 1)))))
65	63	biantrud 527	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ (bits‘(𝐴 · 𝐵)) ↔ (𝑘 ∈ (bits‘(𝐴 · 𝐵)) ∧ 𝑘 ∈ (0..^(𝑘 + 1)))))
66	55, 64, 65	3bitr4d 303	. . . 4 ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ ((bits‘𝐴) smul (bits‘𝐵)) ↔ 𝑘 ∈ (bits‘(𝐴 · 𝐵))))
67	66	ex 403	. . 3 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑘 ∈ ℕ0 → (𝑘 ∈ ((bits‘𝐴) smul (bits‘𝐵)) ↔ 𝑘 ∈ (bits‘(𝐴 · 𝐵)))))
68	6, 9, 67	pm5.21ndd 371	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑘 ∈ ((bits‘𝐴) smul (bits‘𝐵)) ↔ 𝑘 ∈ (bits‘(𝐴 · 𝐵))))
69	68	eqrdv 2775	1 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((bits‘𝐴) smul (bits‘𝐵)) = (bits‘(𝐴 · 𝐵)))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1601   ∈ wcel 2106   ∩ cin 3790   ⊆ wss 3791  ‘cfv 6135  (class class class)co 6922  ℝcr 10271  0cc0 10272  1c1 10273   + caddc 10275   · cmul 10277  ℕcn 11374  2c2 11430  ℕ₀cn0 11642  ℤcz 11728  ℤ_≥cuz 11992  ℝ⁺crp 12137  ...cfz 12643  ..^cfzo 12784   mod cmo 12987  ↑cexp 13178  bitscbits 15547   smul csmu 15549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-inf2 8835  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349  ax-pre-sup 10350

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-xor 1583  df-tru 1605  df-fal 1615  df-had 1652  df-cad 1665  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rmo 3097  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-pss 3807  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4672  df-int 4711  df-iun 4755  df-disj 4855  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-se 5315  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-isom 6144  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-1st 7445  df-2nd 7446  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-2o 7844  df-oadd 7847  df-er 8026  df-map 8142  df-pm 8143  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-sup 8636  df-inf 8637  df-oi 8704  df-card 9098  df-cda 9325  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-nn 11375  df-2 11438  df-3 11439  df-n0 11643  df-xnn0 11715  df-z 11729  df-uz 11993  df-rp 12138  df-fz 12644  df-fzo 12785  df-fl 12912  df-mod 12988  df-seq 13120  df-exp 13179  df-hash 13436  df-cj 14246  df-re 14247  df-im 14248  df-sqrt 14382  df-abs 14383  df-clim 14627  df-sum 14825  df-dvds 15388  df-bits 15550  df-sad 15579  df-smu 15604

This theorem is referenced by: (None)