Theorem lgsdilem2 27313

Description: Lemma for lgsdi 27314. (Contributed by Mario Carneiro, 4-Feb-2015.)

Hypotheses

Ref	Expression
lgsdilem2.1	⊢ (𝜑 → 𝐴 ∈ ℤ)
lgsdilem2.2	⊢ (𝜑 → 𝑀 ∈ ℤ)
lgsdilem2.3	⊢ (𝜑 → 𝑁 ∈ ℤ)
lgsdilem2.4	⊢ (𝜑 → 𝑀 ≠ 0)
lgsdilem2.5	⊢ (𝜑 → 𝑁 ≠ 0)
lgsdilem2.6	⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1))

Assertion

Ref	Expression
lgsdilem2	⊢ (𝜑 → (seq1( · , 𝐹)‘(abs‘𝑀)) = (seq1( · , 𝐹)‘(abs‘(𝑀 · 𝑁))))

Distinct variable groups:   𝑛,𝑀   𝐴,𝑛   𝑛,𝑁

Allowed substitution hints:   𝜑(𝑛)   𝐹(𝑛)

Proof of Theorem lgsdilem2

Dummy variables 𝑘 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mulrid 11136	. . 3 ⊢ (𝑘 ∈ ℂ → (𝑘 · 1) = 𝑘)
2	1	adantl 481	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ ℂ) → (𝑘 · 1) = 𝑘)
3		lgsdilem2.2	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℤ)
4		lgsdilem2.4	. . . 4 ⊢ (𝜑 → 𝑀 ≠ 0)
5		nnabscl 15282	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) → (abs‘𝑀) ∈ ℕ)
6	3, 4, 5	syl2anc 585	. . 3 ⊢ (𝜑 → (abs‘𝑀) ∈ ℕ)
7		nnuz 12821	. . 3 ⊢ ℕ = (ℤ≥‘1)
8	6, 7	eleqtrdi 2847	. 2 ⊢ (𝜑 → (abs‘𝑀) ∈ (ℤ≥‘1))
9	6	nnzd 12544	. . 3 ⊢ (𝜑 → (abs‘𝑀) ∈ ℤ)
10		lgsdilem2.3	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℤ)
11	3, 10	zmulcld 12633	. . . . 5 ⊢ (𝜑 → (𝑀 · 𝑁) ∈ ℤ)
12	3	zcnd 12628	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℂ)
13	10	zcnd 12628	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℂ)
14		lgsdilem2.5	. . . . . 6 ⊢ (𝜑 → 𝑁 ≠ 0)
15	12, 13, 4, 14	mulne0d 11796	. . . . 5 ⊢ (𝜑 → (𝑀 · 𝑁) ≠ 0)
16		nnabscl 15282	. . . . 5 ⊢ (((𝑀 · 𝑁) ∈ ℤ ∧ (𝑀 · 𝑁) ≠ 0) → (abs‘(𝑀 · 𝑁)) ∈ ℕ)
17	11, 15, 16	syl2anc 585	. . . 4 ⊢ (𝜑 → (abs‘(𝑀 · 𝑁)) ∈ ℕ)
18	17	nnzd 12544	. . 3 ⊢ (𝜑 → (abs‘(𝑀 · 𝑁)) ∈ ℤ)
19	12	abscld 15395	. . . . 5 ⊢ (𝜑 → (abs‘𝑀) ∈ ℝ)
20	13	abscld 15395	. . . . 5 ⊢ (𝜑 → (abs‘𝑁) ∈ ℝ)
21	12	absge0d 15403	. . . . 5 ⊢ (𝜑 → 0 ≤ (abs‘𝑀))
22		nnabscl 15282	. . . . . . 7 ⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ)
23	10, 14, 22	syl2anc 585	. . . . . 6 ⊢ (𝜑 → (abs‘𝑁) ∈ ℕ)
24	23	nnge1d 12219	. . . . 5 ⊢ (𝜑 → 1 ≤ (abs‘𝑁))
25	19, 20, 21, 24	lemulge11d 12087	. . . 4 ⊢ (𝜑 → (abs‘𝑀) ≤ ((abs‘𝑀) · (abs‘𝑁)))
26	12, 13	absmuld 15413	. . . 4 ⊢ (𝜑 → (abs‘(𝑀 · 𝑁)) = ((abs‘𝑀) · (abs‘𝑁)))
27	25, 26	breqtrrd 5114	. . 3 ⊢ (𝜑 → (abs‘𝑀) ≤ (abs‘(𝑀 · 𝑁)))
28		eluz2 12788	. . 3 ⊢ ((abs‘(𝑀 · 𝑁)) ∈ (ℤ≥‘(abs‘𝑀)) ↔ ((abs‘𝑀) ∈ ℤ ∧ (abs‘(𝑀 · 𝑁)) ∈ ℤ ∧ (abs‘𝑀) ≤ (abs‘(𝑀 · 𝑁))))
29	9, 18, 27, 28	syl3anbrc 1345	. 2 ⊢ (𝜑 → (abs‘(𝑀 · 𝑁)) ∈ (ℤ≥‘(abs‘𝑀)))
30		lgsdilem2.1	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ ℤ)
31		lgsdilem2.6	. . . . . . 7 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1))
32	31	lgsfcl3 27298	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) → 𝐹:ℕ⟶ℤ)
33	30, 3, 4, 32	syl3anc 1374	. . . . 5 ⊢ (𝜑 → 𝐹:ℕ⟶ℤ)
34		elfznn 13501	. . . . 5 ⊢ (𝑘 ∈ (1...(abs‘𝑀)) → 𝑘 ∈ ℕ)
35		ffvelcdm 7028	. . . . 5 ⊢ ((𝐹:ℕ⟶ℤ ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℤ)
36	33, 34, 35	syl2an 597	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(abs‘𝑀))) → (𝐹‘𝑘) ∈ ℤ)
37	36	zcnd 12628	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(abs‘𝑀))) → (𝐹‘𝑘) ∈ ℂ)
38		mulcl 11116	. . . 4 ⊢ ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑘 · 𝑥) ∈ ℂ)
39	38	adantl 481	. . 3 ⊢ ((𝜑 ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ)
40	8, 37, 39	seqcl 13978	. 2 ⊢ (𝜑 → (seq1( · , 𝐹)‘(abs‘𝑀)) ∈ ℂ)
41	6	peano2nnd 12185	. . . . 5 ⊢ (𝜑 → ((abs‘𝑀) + 1) ∈ ℕ)
42		elfzuz 13468	. . . . 5 ⊢ (𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁))) → 𝑘 ∈ (ℤ≥‘((abs‘𝑀) + 1)))
43		eluznn 12862	. . . . 5 ⊢ ((((abs‘𝑀) + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘((abs‘𝑀) + 1))) → 𝑘 ∈ ℕ)
44	41, 42, 43	syl2an 597	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → 𝑘 ∈ ℕ)
45		eleq1w 2820	. . . . . 6 ⊢ (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ))
46		oveq2 7369	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (𝐴 /L 𝑛) = (𝐴 /L 𝑘))
47		oveq1 7368	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (𝑛 pCnt 𝑀) = (𝑘 pCnt 𝑀))
48	46, 47	oveq12d 7379	. . . . . 6 ⊢ (𝑛 = 𝑘 → ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)) = ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)))
49	45, 48	ifbieq1d 4492	. . . . 5 ⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, ((𝐴 /L 𝑛)↑(𝑛 pCnt 𝑀)), 1) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1))
50		ovex 7394	. . . . . 6 ⊢ ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)) ∈ V
51		1ex 11134	. . . . . 6 ⊢ 1 ∈ V
52	50, 51	ifex 4518	. . . . 5 ⊢ if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1) ∈ V
53	49, 31, 52	fvmpt 6942	. . . 4 ⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1))
54	44, 53	syl 17	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → (𝐹‘𝑘) = if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1))
55		simpr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℙ)
56	3	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝑀 ∈ ℤ)
57		zq 12898	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℚ)
58	56, 57	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝑀 ∈ ℚ)
59		pcabs 16840	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℙ ∧ 𝑀 ∈ ℚ) → (𝑘 pCnt (abs‘𝑀)) = (𝑘 pCnt 𝑀))
60	55, 58, 59	syl2anc 585	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt (abs‘𝑀)) = (𝑘 pCnt 𝑀))
61		elfzle1 13475	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁))) → ((abs‘𝑀) + 1) ≤ 𝑘)
62	61	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → ((abs‘𝑀) + 1) ≤ 𝑘)
63		elfzelz 13472	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁))) → 𝑘 ∈ ℤ)
64		zltp1le 12571	. . . . . . . . . . . . . 14 ⊢ (((abs‘𝑀) ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((abs‘𝑀) < 𝑘 ↔ ((abs‘𝑀) + 1) ≤ 𝑘))
65	9, 63, 64	syl2an 597	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → ((abs‘𝑀) < 𝑘 ↔ ((abs‘𝑀) + 1) ≤ 𝑘))
66	62, 65	mpbird 257	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → (abs‘𝑀) < 𝑘)
67	19	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → (abs‘𝑀) ∈ ℝ)
68	63	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → 𝑘 ∈ ℤ)
69	68	zred 12627	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → 𝑘 ∈ ℝ)
70	67, 69	ltnled 11287	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → ((abs‘𝑀) < 𝑘 ↔ ¬ 𝑘 ≤ (abs‘𝑀)))
71	66, 70	mpbid 232	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → ¬ 𝑘 ≤ (abs‘𝑀))
72	71	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → ¬ 𝑘 ≤ (abs‘𝑀))
73		prmz 16638	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℙ → 𝑘 ∈ ℤ)
74	73	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝑘 ∈ ℤ)
75	4	ad2antrr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝑀 ≠ 0)
76	56, 75, 5	syl2anc 585	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → (abs‘𝑀) ∈ ℕ)
77		dvdsle 16273	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℤ ∧ (abs‘𝑀) ∈ ℕ) → (𝑘 ∥ (abs‘𝑀) → 𝑘 ≤ (abs‘𝑀)))
78	74, 76, 77	syl2anc 585	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝑘 ∥ (abs‘𝑀) → 𝑘 ≤ (abs‘𝑀)))
79	72, 78	mtod 198	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → ¬ 𝑘 ∥ (abs‘𝑀))
80		pceq0 16836	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℙ ∧ (abs‘𝑀) ∈ ℕ) → ((𝑘 pCnt (abs‘𝑀)) = 0 ↔ ¬ 𝑘 ∥ (abs‘𝑀)))
81	55, 76, 80	syl2anc 585	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → ((𝑘 pCnt (abs‘𝑀)) = 0 ↔ ¬ 𝑘 ∥ (abs‘𝑀)))
82	79, 81	mpbird 257	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt (abs‘𝑀)) = 0)
83	60, 82	eqtr3d 2774	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝑘 pCnt 𝑀) = 0)
84	83	oveq2d 7377	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)) = ((𝐴 /L 𝑘)↑0))
85	30	ad2antrr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → 𝐴 ∈ ℤ)
86		lgscl 27291	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝐴 /L 𝑘) ∈ ℤ)
87	85, 74, 86	syl2anc 585	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝐴 /L 𝑘) ∈ ℤ)
88	87	zcnd 12628	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → (𝐴 /L 𝑘) ∈ ℂ)
89	88	exp0d 14096	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → ((𝐴 /L 𝑘)↑0) = 1)
90	84, 89	eqtrd 2772	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) ∧ 𝑘 ∈ ℙ) → ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)) = 1)
91	90	ifeq1da 4499	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1) = if(𝑘 ∈ ℙ, 1, 1))
92		ifid 4508	. . . 4 ⊢ if(𝑘 ∈ ℙ, 1, 1) = 1
93	91, 92	eqtrdi 2788	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → if(𝑘 ∈ ℙ, ((𝐴 /L 𝑘)↑(𝑘 pCnt 𝑀)), 1) = 1)
94	54, 93	eqtrd 2772	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ (((abs‘𝑀) + 1)...(abs‘(𝑀 · 𝑁)))) → (𝐹‘𝑘) = 1)
95	2, 8, 29, 40, 94	seqid2 14004	1 ⊢ (𝜑 → (seq1( · , 𝐹)‘(abs‘𝑀)) = (seq1( · , 𝐹)‘(abs‘(𝑀 · 𝑁))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ifcif 4467   class class class wbr 5086   ↦ cmpt 5167  ⟶wf 6489  ‘cfv 6493  (class class class)co 7361  ℂcc 11030  ℝcr 11031  0cc0 11032  1c1 11033   + caddc 11035   · cmul 11037   < clt 11173   ≤ cle 11174  ℕcn 12168  ℤcz 12518  ℤ_≥cuz 12782  ℚcq 12892  ...cfz 13455  seqcseq 13957  ↑cexp 14017  abscabs 15190   ∥ cdvds 16215  ℙcprime 16634   pCnt cpc 16801   /_L clgs 27274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-cnex 11088  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108  ax-pre-mulgt0 11109  ax-pre-sup 11110

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7812  df-1st 7936  df-2nd 7937  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-1o 8399  df-2o 8400  df-oadd 8403  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-fin 8891  df-sup 9349  df-inf 9350  df-dju 9819  df-card 9857  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179  df-sub 11373  df-neg 11374  df-div 11802  df-nn 12169  df-2 12238  df-3 12239  df-n0 12432  df-xnn0 12505  df-z 12519  df-uz 12783  df-q 12893  df-rp 12937  df-fz 13456  df-fzo 13603  df-fl 13745  df-mod 13823  df-seq 13958  df-exp 14018  df-hash 14287  df-cj 15055  df-re 15056  df-im 15057  df-sqrt 15191  df-abs 15192  df-dvds 16216  df-gcd 16458  df-prm 16635  df-phi 16730  df-pc 16802  df-lgs 27275

This theorem is referenced by:  lgsdi  27314