Theorem 3dvds 12341

Description: A rule for divisibility by 3 of a number written in base 10. This is Metamath 100 proof #85. (Contributed by Mario Carneiro, 14-Jul-2014.) (Revised by Mario Carneiro, 17-Jan-2015.) (Revised by AV, 8-Sep-2021.)

Assertion

Ref	Expression
3dvds	⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) → (3 ∥ Σ𝑘 ∈ (0...𝑁)((𝐹‘𝑘) · (;10↑𝑘)) ↔ 3 ∥ Σ𝑘 ∈ (0...𝑁)(𝐹‘𝑘)))

Distinct variable groups:   𝑘,𝐹   𝑘,𝑁

Proof of Theorem 3dvds

Dummy variable 𝑗 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		3z 9443	. . 3 ⊢ 3 ∈ ℤ
2	1	a1i 9	. 2 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) → 3 ∈ ℤ)
3		0zd 9426	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) → 0 ∈ ℤ)
4		nn0z 9434	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)
5	4	adantr 276	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) → 𝑁 ∈ ℤ)
6	3, 5	fzfigd 10620	. . 3 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) → (0...𝑁) ∈ Fin)
7		ffvelcdm 5741	. . . . 5 ⊢ ((𝐹:(0...𝑁)⟶ℤ ∧ 𝑘 ∈ (0...𝑁)) → (𝐹‘𝑘) ∈ ℤ)
8	7	adantll 476	. . . 4 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → (𝐹‘𝑘) ∈ ℤ)
9		10nn 9561	. . . . . 6 ⊢ ;10 ∈ ℕ
10	9	nnzi 9435	. . . . 5 ⊢ ;10 ∈ ℤ
11		elfznn0 10278	. . . . . 6 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
12	11	adantl 277	. . . . 5 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
13		zexpcl 10743	. . . . 5 ⊢ ((;10 ∈ ℤ ∧ 𝑘 ∈ ℕ0) → (;10↑𝑘) ∈ ℤ)
14	10, 12, 13	sylancr 414	. . . 4 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → (;10↑𝑘) ∈ ℤ)
15	8, 14	zmulcld 9543	. . 3 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐹‘𝑘) · (;10↑𝑘)) ∈ ℤ)
16	6, 15	fsumzcl 11879	. 2 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) → Σ𝑘 ∈ (0...𝑁)((𝐹‘𝑘) · (;10↑𝑘)) ∈ ℤ)
17	6, 8	fsumzcl 11879	. 2 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) → Σ𝑘 ∈ (0...𝑁)(𝐹‘𝑘) ∈ ℤ)
18	15, 8	zsubcld 9542	. . . 4 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → (((𝐹‘𝑘) · (;10↑𝑘)) − (𝐹‘𝑘)) ∈ ℤ)
19		ax-1cn 8060	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
20	9	nncni 9088	. . . . . . . . . . . 12 ⊢ ;10 ∈ ℂ
21	19, 20	negsubdi2i 8400	. . . . . . . . . . 11 ⊢ -(1 − ;10) = (;10 − 1)
22		9p1e10 9548	. . . . . . . . . . . . 13 ⊢ (9 + 1) = ;10
23	22	eqcomi 2213	. . . . . . . . . . . 12 ⊢ ;10 = (9 + 1)
24	23	oveq1i 5984	. . . . . . . . . . 11 ⊢ (;10 − 1) = ((9 + 1) − 1)
25		9cn 9166	. . . . . . . . . . . 12 ⊢ 9 ∈ ℂ
26	25, 19	pncan3oi 8330	. . . . . . . . . . 11 ⊢ ((9 + 1) − 1) = 9
27	21, 24, 26	3eqtri 2234	. . . . . . . . . 10 ⊢ -(1 − ;10) = 9
28		3t3e9 9236	. . . . . . . . . 10 ⊢ (3 · 3) = 9
29	27, 28	eqtr4i 2233	. . . . . . . . 9 ⊢ -(1 − ;10) = (3 · 3)
30	20	a1i 9	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ0 → ;10 ∈ ℂ)
31		1re 8113	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ
32		10re 9564	. . . . . . . . . . . . . . . . 17 ⊢ ;10 ∈ ℝ
33		1lt10 9684	. . . . . . . . . . . . . . . . 17 ⊢ 1 < ;10
34	31, 32, 33	gtapii 8749	. . . . . . . . . . . . . . . 16 ⊢ ;10 # 1
35	34	a1i 9	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ0 → ;10 # 1)
36		id 19	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ0 → 𝑘 ∈ ℕ0)
37	30, 35, 36	geoserap 11984	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ0 → Σ𝑗 ∈ (0...(𝑘 − 1))(;10↑𝑗) = ((1 − (;10↑𝑘)) / (1 − ;10)))
38		0zd 9426	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ0 → 0 ∈ ℤ)
39		nn0z 9434	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ0 → 𝑘 ∈ ℤ)
40		peano2zm 9452	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℤ → (𝑘 − 1) ∈ ℤ)
41	39, 40	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ0 → (𝑘 − 1) ∈ ℤ)
42	38, 41	fzfigd 10620	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ0 → (0...(𝑘 − 1)) ∈ Fin)
43		elfznn0 10278	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...(𝑘 − 1)) → 𝑗 ∈ ℕ0)
44	43	adantl 277	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑗 ∈ (0...(𝑘 − 1))) → 𝑗 ∈ ℕ0)
45		zexpcl 10743	. . . . . . . . . . . . . . . 16 ⊢ ((;10 ∈ ℤ ∧ 𝑗 ∈ ℕ0) → (;10↑𝑗) ∈ ℤ)
46	10, 44, 45	sylancr 414	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ0 ∧ 𝑗 ∈ (0...(𝑘 − 1))) → (;10↑𝑗) ∈ ℤ)
47	42, 46	fsumzcl 11879	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ0 → Σ𝑗 ∈ (0...(𝑘 − 1))(;10↑𝑗) ∈ ℤ)
48	37, 47	eqeltrrd 2287	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ0 → ((1 − (;10↑𝑘)) / (1 − ;10)) ∈ ℤ)
49		1z 9440	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℤ
50		zsubcl 9455	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℤ ∧ ;10 ∈ ℤ) → (1 − ;10) ∈ ℤ)
51	49, 10, 50	mp2an 426	. . . . . . . . . . . . . 14 ⊢ (1 − ;10) ∈ ℤ
52	31, 33	ltneii 8211	. . . . . . . . . . . . . . 15 ⊢ 1 ≠ ;10
53	19, 20	subeq0i 8394	. . . . . . . . . . . . . . . 16 ⊢ ((1 − ;10) = 0 ↔ 1 = ;10)
54	53	necon3bii 2418	. . . . . . . . . . . . . . 15 ⊢ ((1 − ;10) ≠ 0 ↔ 1 ≠ ;10)
55	52, 54	mpbir 146	. . . . . . . . . . . . . 14 ⊢ (1 − ;10) ≠ 0
56	10, 36, 13	sylancr 414	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ0 → (;10↑𝑘) ∈ ℤ)
57		zsubcl 9455	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℤ ∧ (;10↑𝑘) ∈ ℤ) → (1 − (;10↑𝑘)) ∈ ℤ)
58	49, 56, 57	sylancr 414	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ0 → (1 − (;10↑𝑘)) ∈ ℤ)
59		dvdsval2 12267	. . . . . . . . . . . . . 14 ⊢ (((1 − ;10) ∈ ℤ ∧ (1 − ;10) ≠ 0 ∧ (1 − (;10↑𝑘)) ∈ ℤ) → ((1 − ;10) ∥ (1 − (;10↑𝑘)) ↔ ((1 − (;10↑𝑘)) / (1 − ;10)) ∈ ℤ))
60	51, 55, 58, 59	mp3an12i 1356	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ0 → ((1 − ;10) ∥ (1 − (;10↑𝑘)) ↔ ((1 − (;10↑𝑘)) / (1 − ;10)) ∈ ℤ))
61	48, 60	mpbird 167	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 → (1 − ;10) ∥ (1 − (;10↑𝑘)))
62	56	zcnd 9538	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ0 → (;10↑𝑘) ∈ ℂ)
63		negsubdi2 8373	. . . . . . . . . . . . 13 ⊢ (((;10↑𝑘) ∈ ℂ ∧ 1 ∈ ℂ) → -((;10↑𝑘) − 1) = (1 − (;10↑𝑘)))
64	62, 19, 63	sylancl 413	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 → -((;10↑𝑘) − 1) = (1 − (;10↑𝑘)))
65	61, 64	breqtrrd 4090	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 → (1 − ;10) ∥ -((;10↑𝑘) − 1))
66		peano2zm 9452	. . . . . . . . . . . . 13 ⊢ ((;10↑𝑘) ∈ ℤ → ((;10↑𝑘) − 1) ∈ ℤ)
67	56, 66	syl 14	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ0 → ((;10↑𝑘) − 1) ∈ ℤ)
68		dvdsnegb 12285	. . . . . . . . . . . 12 ⊢ (((1 − ;10) ∈ ℤ ∧ ((;10↑𝑘) − 1) ∈ ℤ) → ((1 − ;10) ∥ ((;10↑𝑘) − 1) ↔ (1 − ;10) ∥ -((;10↑𝑘) − 1)))
69	51, 67, 68	sylancr 414	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 → ((1 − ;10) ∥ ((;10↑𝑘) − 1) ↔ (1 − ;10) ∥ -((;10↑𝑘) − 1)))
70	65, 69	mpbird 167	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → (1 − ;10) ∥ ((;10↑𝑘) − 1))
71		negdvdsb 12284	. . . . . . . . . . 11 ⊢ (((1 − ;10) ∈ ℤ ∧ ((;10↑𝑘) − 1) ∈ ℤ) → ((1 − ;10) ∥ ((;10↑𝑘) − 1) ↔ -(1 − ;10) ∥ ((;10↑𝑘) − 1)))
72	51, 67, 71	sylancr 414	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 → ((1 − ;10) ∥ ((;10↑𝑘) − 1) ↔ -(1 − ;10) ∥ ((;10↑𝑘) − 1)))
73	70, 72	mpbid 147	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ0 → -(1 − ;10) ∥ ((;10↑𝑘) − 1))
74	29, 73	eqbrtrrid 4098	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → (3 · 3) ∥ ((;10↑𝑘) − 1))
75		muldvds1 12293	. . . . . . . . 9 ⊢ ((3 ∈ ℤ ∧ 3 ∈ ℤ ∧ ((;10↑𝑘) − 1) ∈ ℤ) → ((3 · 3) ∥ ((;10↑𝑘) − 1) → 3 ∥ ((;10↑𝑘) − 1)))
76	1, 1, 67, 75	mp3an12i 1356	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → ((3 · 3) ∥ ((;10↑𝑘) − 1) → 3 ∥ ((;10↑𝑘) − 1)))
77	74, 76	mpd 13	. . . . . . 7 ⊢ (𝑘 ∈ ℕ0 → 3 ∥ ((;10↑𝑘) − 1))
78	12, 77	syl 14	. . . . . 6 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → 3 ∥ ((;10↑𝑘) − 1))
79	14, 66	syl 14	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → ((;10↑𝑘) − 1) ∈ ℤ)
80		dvdsmultr2 12310	. . . . . . 7 ⊢ ((3 ∈ ℤ ∧ (𝐹‘𝑘) ∈ ℤ ∧ ((;10↑𝑘) − 1) ∈ ℤ) → (3 ∥ ((;10↑𝑘) − 1) → 3 ∥ ((𝐹‘𝑘) · ((;10↑𝑘) − 1))))
81	1, 8, 79, 80	mp3an2i 1357	. . . . . 6 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → (3 ∥ ((;10↑𝑘) − 1) → 3 ∥ ((𝐹‘𝑘) · ((;10↑𝑘) − 1))))
82	78, 81	mpd 13	. . . . 5 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → 3 ∥ ((𝐹‘𝑘) · ((;10↑𝑘) − 1)))
83	8	zcnd 9538	. . . . . 6 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → (𝐹‘𝑘) ∈ ℂ)
84	14	zcnd 9538	. . . . . 6 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → (;10↑𝑘) ∈ ℂ)
85	83, 84	muls1d 8532	. . . . 5 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐹‘𝑘) · ((;10↑𝑘) − 1)) = (((𝐹‘𝑘) · (;10↑𝑘)) − (𝐹‘𝑘)))
86	82, 85	breqtrd 4088	. . . 4 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → 3 ∥ (((𝐹‘𝑘) · (;10↑𝑘)) − (𝐹‘𝑘)))
87	6, 2, 18, 86	fsumdvds 12319	. . 3 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) → 3 ∥ Σ𝑘 ∈ (0...𝑁)(((𝐹‘𝑘) · (;10↑𝑘)) − (𝐹‘𝑘)))
88	15	zcnd 9538	. . . 4 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐹‘𝑘) · (;10↑𝑘)) ∈ ℂ)
89	6, 88, 83	fsumsub 11929	. . 3 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) → Σ𝑘 ∈ (0...𝑁)(((𝐹‘𝑘) · (;10↑𝑘)) − (𝐹‘𝑘)) = (Σ𝑘 ∈ (0...𝑁)((𝐹‘𝑘) · (;10↑𝑘)) − Σ𝑘 ∈ (0...𝑁)(𝐹‘𝑘)))
90	87, 89	breqtrd 4088	. 2 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) → 3 ∥ (Σ𝑘 ∈ (0...𝑁)((𝐹‘𝑘) · (;10↑𝑘)) − Σ𝑘 ∈ (0...𝑁)(𝐹‘𝑘)))
91		dvdssub2 12312	. 2 ⊢ (((3 ∈ ℤ ∧ Σ𝑘 ∈ (0...𝑁)((𝐹‘𝑘) · (;10↑𝑘)) ∈ ℤ ∧ Σ𝑘 ∈ (0...𝑁)(𝐹‘𝑘) ∈ ℤ) ∧ 3 ∥ (Σ𝑘 ∈ (0...𝑁)((𝐹‘𝑘) · (;10↑𝑘)) − Σ𝑘 ∈ (0...𝑁)(𝐹‘𝑘))) → (3 ∥ Σ𝑘 ∈ (0...𝑁)((𝐹‘𝑘) · (;10↑𝑘)) ↔ 3 ∥ Σ𝑘 ∈ (0...𝑁)(𝐹‘𝑘)))
92	2, 16, 17, 90, 91	syl31anc 1255	1 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) → (3 ∥ Σ𝑘 ∈ (0...𝑁)((𝐹‘𝑘) · (;10↑𝑘)) ↔ 3 ∥ Σ𝑘 ∈ (0...𝑁)(𝐹‘𝑘)))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1375   ∈ wcel 2180   ≠ wne 2380   class class class wbr 4062  ⟶wf 5290  ‘cfv 5294  (class class class)co 5974  ℂcc 7965  0cc0 7967  1c1 7968   + caddc 7970   · cmul 7972   − cmin 8285  -cneg 8286   # cap 8696   / cdiv 8787  3c3 9130  9c9 9136  ℕ₀cn0 9337  ℤcz 9414  ;cdc 9546  ...cfz 10172  ↑cexp 10727  Σcsu 11830   ∥ cdvds 12264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-13 2182  ax-14 2183  ax-ext 2191  ax-coll 4178  ax-sep 4181  ax-nul 4189  ax-pow 4237  ax-pr 4272  ax-un 4501  ax-setind 4606  ax-iinf 4657  ax-cnex 8058  ax-resscn 8059  ax-1cn 8060  ax-1re 8061  ax-icn 8062  ax-addcl 8063  ax-addrcl 8064  ax-mulcl 8065  ax-mulrcl 8066  ax-addcom 8067  ax-mulcom 8068  ax-addass 8069  ax-mulass 8070  ax-distr 8071  ax-i2m1 8072  ax-0lt1 8073  ax-1rid 8074  ax-0id 8075  ax-rnegex 8076  ax-precex 8077  ax-cnre 8078  ax-pre-ltirr 8079  ax-pre-ltwlin 8080  ax-pre-lttrn 8081  ax-pre-apti 8082  ax-pre-ltadd 8083  ax-pre-mulgt0 8084  ax-pre-mulext 8085  ax-arch 8086  ax-caucvg 8087

This theorem depends on definitions:  df-bi 117  df-dc 839  df-3or 984  df-3an 985  df-tru 1378  df-fal 1381  df-nf 1487  df-sb 1789  df-eu 2060  df-mo 2061  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ne 2381  df-nel 2476  df-ral 2493  df-rex 2494  df-reu 2495  df-rmo 2496  df-rab 2497  df-v 2781  df-sbc 3009  df-csb 3105  df-dif 3179  df-un 3181  df-in 3183  df-ss 3190  df-nul 3472  df-if 3583  df-pw 3631  df-sn 3652  df-pr 3653  df-op 3655  df-uni 3868  df-int 3903  df-iun 3946  df-br 4063  df-opab 4125  df-mpt 4126  df-tr 4162  df-id 4361  df-po 4364  df-iso 4365  df-iord 4434  df-on 4436  df-ilim 4437  df-suc 4439  df-iom 4660  df-xp 4702  df-rel 4703  df-cnv 4704  df-co 4705  df-dm 4706  df-rn 4707  df-res 4708  df-ima 4709  df-iota 5254  df-fun 5296  df-fn 5297  df-f 5298  df-f1 5299  df-fo 5300  df-f1o 5301  df-fv 5302  df-isom 5303  df-riota 5927  df-ov 5977  df-oprab 5978  df-mpo 5979  df-1st 6256  df-2nd 6257  df-recs 6421  df-irdg 6486  df-frec 6507  df-1o 6532  df-oadd 6536  df-er 6650  df-en 6858  df-dom 6859  df-fin 6860  df-pnf 8151  df-mnf 8152  df-xr 8153  df-ltxr 8154  df-le 8155  df-sub 8287  df-neg 8288  df-reap 8690  df-ap 8697  df-div 8788  df-inn 9079  df-2 9137  df-3 9138  df-4 9139  df-5 9140  df-6 9141  df-7 9142  df-8 9143  df-9 9144  df-n0 9338  df-z 9415  df-dec 9547  df-uz 9691  df-q 9783  df-rp 9818  df-fz 10173  df-fzo 10307  df-seqfrec 10637  df-exp 10728  df-ihash 10965  df-cj 11319  df-re 11320  df-im 11321  df-rsqrt 11475  df-abs 11476  df-clim 11756  df-sumdc 11831  df-dvds 12265

This theorem is referenced by: (None)