Theorem jm2.19 43150

Description: Lemma 2.19 of [JonesMatijasevic] p. 696. Transfer divisibility constraints between Y-values and their indices. (Contributed by Stefan O'Rear, 24-Sep-2014.)

Assertion

Ref	Expression
jm2.19	⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁)))

Proof of Theorem jm2.19

Step	Hyp	Ref	Expression
1		rmyeq0 43110	. . . . . 6 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝑁 = 0 ↔ (𝐴 Yrm 𝑁) = 0))
2	1	3adant2 1131	. . . . 5 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 = 0 ↔ (𝐴 Yrm 𝑁) = 0))
3		0dvds 16194	. . . . . 6 ⊢ (𝑁 ∈ ℤ → (0 ∥ 𝑁 ↔ 𝑁 = 0))
4	3	3ad2ant3 1135	. . . . 5 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0 ∥ 𝑁 ↔ 𝑁 = 0))
5		frmy 43071	. . . . . . . 8 ⊢ Yrm :((ℤ≥‘2) × ℤ)⟶ℤ
6	5	fovcl 7483	. . . . . . 7 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) ∈ ℤ)
7	6	3adant2 1131	. . . . . 6 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) ∈ ℤ)
8		0dvds 16194	. . . . . 6 ⊢ ((𝐴 Yrm 𝑁) ∈ ℤ → (0 ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑁) = 0))
9	7, 8	syl 17	. . . . 5 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0 ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑁) = 0))
10	2, 4, 9	3bitr4d 311	. . . 4 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0 ∥ 𝑁 ↔ 0 ∥ (𝐴 Yrm 𝑁)))
11	10	adantr 480	. . 3 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → (0 ∥ 𝑁 ↔ 0 ∥ (𝐴 Yrm 𝑁)))
12		simpr 484	. . . 4 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → 𝑀 = 0)
13	12	breq1d 5105	. . 3 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → (𝑀 ∥ 𝑁 ↔ 0 ∥ 𝑁))
14	12	oveq2d 7371	. . . . 5 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → (𝐴 Yrm 𝑀) = (𝐴 Yrm 0))
15		simpl1 1192	. . . . . 6 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → 𝐴 ∈ (ℤ≥‘2))
16		rmy0 43086	. . . . . 6 ⊢ (𝐴 ∈ (ℤ≥‘2) → (𝐴 Yrm 0) = 0)
17	15, 16	syl 17	. . . . 5 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → (𝐴 Yrm 0) = 0)
18	14, 17	eqtrd 2768	. . . 4 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → (𝐴 Yrm 𝑀) = 0)
19	18	breq1d 5105	. . 3 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁) ↔ 0 ∥ (𝐴 Yrm 𝑁)))
20	11, 13, 19	3bitr4d 311	. 2 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 = 0) → (𝑀 ∥ 𝑁 ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁)))
21	5	fovcl 7483	. . . . . . . . 9 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ) → (𝐴 Yrm 𝑀) ∈ ℤ)
22	21	3adant3 1132	. . . . . . . 8 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑀) ∈ ℤ)
23		dvds0 16189	. . . . . . . 8 ⊢ ((𝐴 Yrm 𝑀) ∈ ℤ → (𝐴 Yrm 𝑀) ∥ 0)
24	22, 23	syl 17	. . . . . . 7 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑀) ∥ 0)
25	16	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 0) = 0)
26	24, 25	breqtrrd 5123	. . . . . 6 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 0))
27		oveq2 7363	. . . . . . 7 ⊢ ((𝑁 mod (abs‘𝑀)) = 0 → (𝐴 Yrm (𝑁 mod (abs‘𝑀))) = (𝐴 Yrm 0))
28	27	breq2d 5107	. . . . . 6 ⊢ ((𝑁 mod (abs‘𝑀)) = 0 → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 mod (abs‘𝑀))) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 0)))
29	26, 28	syl5ibrcom 247	. . . . 5 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑁 mod (abs‘𝑀)) = 0 → (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 mod (abs‘𝑀)))))
30	29	adantr 480	. . . 4 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → ((𝑁 mod (abs‘𝑀)) = 0 → (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 mod (abs‘𝑀)))))
31		zre 12483	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
32	31	3ad2ant3 1135	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℝ)
33	32	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → 𝑁 ∈ ℝ)
34		zcn 12484	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℂ)
35	34	3ad2ant2 1134	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℂ)
36	35	ad2antrr 726	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → 𝑀 ∈ ℂ)
37		simplr 768	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → 𝑀 ≠ 0)
38	36, 37	absrpcld 15365	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (abs‘𝑀) ∈ ℝ+)
39		modlt 13791	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ ∧ (abs‘𝑀) ∈ ℝ+) → (𝑁 mod (abs‘𝑀)) < (abs‘𝑀))
40	33, 38, 39	syl2anc 584	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (𝑁 mod (abs‘𝑀)) < (abs‘𝑀))
41		simpll1 1213	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → 𝐴 ∈ (ℤ≥‘2))
42		simpll3 1215	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → 𝑁 ∈ ℤ)
43		simpll2 1214	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → 𝑀 ∈ ℤ)
44		nnabscl 15240	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) → (abs‘𝑀) ∈ ℕ)
45	43, 37, 44	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (abs‘𝑀) ∈ ℕ)
46	42, 45	zmodcld 13803	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (𝑁 mod (abs‘𝑀)) ∈ ℕ0)
47		nn0abscl 15226	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℤ → (abs‘𝑀) ∈ ℕ0)
48	47	3ad2ant2 1134	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (abs‘𝑀) ∈ ℕ0)
49	48	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (abs‘𝑀) ∈ ℕ0)
50		ltrmynn0 43105	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ (𝑁 mod (abs‘𝑀)) ∈ ℕ0 ∧ (abs‘𝑀) ∈ ℕ0) → ((𝑁 mod (abs‘𝑀)) < (abs‘𝑀) ↔ (𝐴 Yrm (𝑁 mod (abs‘𝑀))) < (𝐴 Yrm (abs‘𝑀))))
51	41, 46, 49, 50	syl3anc 1373	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → ((𝑁 mod (abs‘𝑀)) < (abs‘𝑀) ↔ (𝐴 Yrm (𝑁 mod (abs‘𝑀))) < (𝐴 Yrm (abs‘𝑀))))
52	40, 51	mpbid 232	. . . . . . . . 9 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (𝐴 Yrm (𝑁 mod (abs‘𝑀))) < (𝐴 Yrm (abs‘𝑀)))
53	46	nn0zd 12504	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (𝑁 mod (abs‘𝑀)) ∈ ℤ)
54		rmyabs 43115	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ (𝑁 mod (abs‘𝑀)) ∈ ℤ) → (abs‘(𝐴 Yrm (𝑁 mod (abs‘𝑀)))) = (𝐴 Yrm (abs‘(𝑁 mod (abs‘𝑀)))))
55	41, 53, 54	syl2anc 584	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (abs‘(𝐴 Yrm (𝑁 mod (abs‘𝑀)))) = (𝐴 Yrm (abs‘(𝑁 mod (abs‘𝑀)))))
56	33, 38	modcld 13786	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (𝑁 mod (abs‘𝑀)) ∈ ℝ)
57		modge0 13790	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℝ ∧ (abs‘𝑀) ∈ ℝ+) → 0 ≤ (𝑁 mod (abs‘𝑀)))
58	33, 38, 57	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → 0 ≤ (𝑁 mod (abs‘𝑀)))
59	56, 58	absidd 15337	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (abs‘(𝑁 mod (abs‘𝑀))) = (𝑁 mod (abs‘𝑀)))
60	59	oveq2d 7371	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (𝐴 Yrm (abs‘(𝑁 mod (abs‘𝑀)))) = (𝐴 Yrm (𝑁 mod (abs‘𝑀))))
61	55, 60	eqtrd 2768	. . . . . . . . 9 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (abs‘(𝐴 Yrm (𝑁 mod (abs‘𝑀)))) = (𝐴 Yrm (𝑁 mod (abs‘𝑀))))
62		rmyabs 43115	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ) → (abs‘(𝐴 Yrm 𝑀)) = (𝐴 Yrm (abs‘𝑀)))
63	41, 43, 62	syl2anc 584	. . . . . . . . 9 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (abs‘(𝐴 Yrm 𝑀)) = (𝐴 Yrm (abs‘𝑀)))
64	52, 61, 63	3brtr4d 5127	. . . . . . . 8 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (abs‘(𝐴 Yrm (𝑁 mod (abs‘𝑀)))) < (abs‘(𝐴 Yrm 𝑀)))
65	5	fovcl 7483	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ (𝑁 mod (abs‘𝑀)) ∈ ℤ) → (𝐴 Yrm (𝑁 mod (abs‘𝑀))) ∈ ℤ)
66	41, 53, 65	syl2anc 584	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (𝐴 Yrm (𝑁 mod (abs‘𝑀))) ∈ ℤ)
67		nn0abscl 15226	. . . . . . . . . . 11 ⊢ ((𝐴 Yrm (𝑁 mod (abs‘𝑀))) ∈ ℤ → (abs‘(𝐴 Yrm (𝑁 mod (abs‘𝑀)))) ∈ ℕ0)
68	66, 67	syl 17	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (abs‘(𝐴 Yrm (𝑁 mod (abs‘𝑀)))) ∈ ℕ0)
69	68	nn0red 12454	. . . . . . . . 9 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (abs‘(𝐴 Yrm (𝑁 mod (abs‘𝑀)))) ∈ ℝ)
70	22	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (𝐴 Yrm 𝑀) ∈ ℤ)
71		nn0abscl 15226	. . . . . . . . . . 11 ⊢ ((𝐴 Yrm 𝑀) ∈ ℤ → (abs‘(𝐴 Yrm 𝑀)) ∈ ℕ0)
72	70, 71	syl 17	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (abs‘(𝐴 Yrm 𝑀)) ∈ ℕ0)
73	72	nn0red 12454	. . . . . . . . 9 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (abs‘(𝐴 Yrm 𝑀)) ∈ ℝ)
74	69, 73	ltnled 11271	. . . . . . . 8 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → ((abs‘(𝐴 Yrm (𝑁 mod (abs‘𝑀)))) < (abs‘(𝐴 Yrm 𝑀)) ↔ ¬ (abs‘(𝐴 Yrm 𝑀)) ≤ (abs‘(𝐴 Yrm (𝑁 mod (abs‘𝑀))))))
75	64, 74	mpbid 232	. . . . . . 7 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → ¬ (abs‘(𝐴 Yrm 𝑀)) ≤ (abs‘(𝐴 Yrm (𝑁 mod (abs‘𝑀)))))
76		simpr 484	. . . . . . . . 9 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (𝑁 mod (abs‘𝑀)) ≠ 0)
77		rmyeq0 43110	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ (𝑁 mod (abs‘𝑀)) ∈ ℤ) → ((𝑁 mod (abs‘𝑀)) = 0 ↔ (𝐴 Yrm (𝑁 mod (abs‘𝑀))) = 0))
78	41, 53, 77	syl2anc 584	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → ((𝑁 mod (abs‘𝑀)) = 0 ↔ (𝐴 Yrm (𝑁 mod (abs‘𝑀))) = 0))
79	78	necon3bid 2973	. . . . . . . . 9 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → ((𝑁 mod (abs‘𝑀)) ≠ 0 ↔ (𝐴 Yrm (𝑁 mod (abs‘𝑀))) ≠ 0))
80	76, 79	mpbid 232	. . . . . . . 8 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → (𝐴 Yrm (𝑁 mod (abs‘𝑀))) ≠ 0)
81		dvdsleabs2 16230	. . . . . . . 8 ⊢ (((𝐴 Yrm 𝑀) ∈ ℤ ∧ (𝐴 Yrm (𝑁 mod (abs‘𝑀))) ∈ ℤ ∧ (𝐴 Yrm (𝑁 mod (abs‘𝑀))) ≠ 0) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 mod (abs‘𝑀))) → (abs‘(𝐴 Yrm 𝑀)) ≤ (abs‘(𝐴 Yrm (𝑁 mod (abs‘𝑀))))))
82	70, 66, 80, 81	syl3anc 1373	. . . . . . 7 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 mod (abs‘𝑀))) → (abs‘(𝐴 Yrm 𝑀)) ≤ (abs‘(𝐴 Yrm (𝑁 mod (abs‘𝑀))))))
83	75, 82	mtod 198	. . . . . 6 ⊢ ((((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) ∧ (𝑁 mod (abs‘𝑀)) ≠ 0) → ¬ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 mod (abs‘𝑀))))
84	83	ex 412	. . . . 5 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → ((𝑁 mod (abs‘𝑀)) ≠ 0 → ¬ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 mod (abs‘𝑀)))))
85	84	necon4ad 2948	. . . 4 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 mod (abs‘𝑀))) → (𝑁 mod (abs‘𝑀)) = 0))
86	30, 85	impbid 212	. . 3 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → ((𝑁 mod (abs‘𝑀)) = 0 ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 mod (abs‘𝑀)))))
87		simpl2 1193	. . . 4 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → 𝑀 ∈ ℤ)
88		simpl3 1194	. . . 4 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → 𝑁 ∈ ℤ)
89		simpr 484	. . . 4 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → 𝑀 ≠ 0)
90		dvdsabsmod0 43144	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≠ 0) → (𝑀 ∥ 𝑁 ↔ (𝑁 mod (abs‘𝑀)) = 0))
91	87, 88, 89, 90	syl3anc 1373	. . 3 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (𝑀 ∥ 𝑁 ↔ (𝑁 mod (abs‘𝑀)) = 0))
92		simpl1 1192	. . . . 5 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → 𝐴 ∈ (ℤ≥‘2))
93	32	adantr 480	. . . . . . 7 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → 𝑁 ∈ ℝ)
94		zre 12483	. . . . . . . . 9 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
95	94	3ad2ant2 1134	. . . . . . . 8 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℝ)
96	95	adantr 480	. . . . . . 7 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → 𝑀 ∈ ℝ)
97		modabsdifz 43143	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑀 ≠ 0) → ((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) ∈ ℤ)
98	93, 96, 89, 97	syl3anc 1373	. . . . . 6 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → ((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) ∈ ℤ)
99	98	znegcld 12589	. . . . 5 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → -((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) ∈ ℤ)
100		jm2.19lem4 43149	. . . . 5 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ -((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) ∈ ℤ) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + (-((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀)))))
101	92, 87, 88, 99, 100	syl121anc 1377	. . . 4 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + (-((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀)))))
102	32	recnd 11151	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℂ)
103	102	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → 𝑁 ∈ ℂ)
104	35	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → 𝑀 ∈ ℂ)
105	104, 89	absrpcld 15365	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (abs‘𝑀) ∈ ℝ+)
106	93, 105	modcld 13786	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (𝑁 mod (abs‘𝑀)) ∈ ℝ)
107	106	recnd 11151	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (𝑁 mod (abs‘𝑀)) ∈ ℂ)
108	103, 107	subcld 11483	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (𝑁 − (𝑁 mod (abs‘𝑀))) ∈ ℂ)
109	108, 104, 89	divcld 11908	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → ((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) ∈ ℂ)
110	109, 104	mulneg1d 11581	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (-((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀) = -(((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀))
111	110	oveq2d 7371	. . . . . . 7 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (𝑁 + (-((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀)) = (𝑁 + -(((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀)))
112	109, 104	mulcld 11143	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀) ∈ ℂ)
113	103, 112	negsubd 11489	. . . . . . 7 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (𝑁 + -(((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀)) = (𝑁 − (((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀)))
114	108, 104, 89	divcan1d 11909	. . . . . . . . 9 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀) = (𝑁 − (𝑁 mod (abs‘𝑀))))
115	114	oveq2d 7371	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (𝑁 − (((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀)) = (𝑁 − (𝑁 − (𝑁 mod (abs‘𝑀)))))
116	103, 107	nncand 11488	. . . . . . . 8 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (𝑁 − (𝑁 − (𝑁 mod (abs‘𝑀)))) = (𝑁 mod (abs‘𝑀)))
117	115, 116	eqtrd 2768	. . . . . . 7 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (𝑁 − (((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀)) = (𝑁 mod (abs‘𝑀)))
118	111, 113, 117	3eqtrrd 2773	. . . . . 6 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (𝑁 mod (abs‘𝑀)) = (𝑁 + (-((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀)))
119	118	oveq2d 7371	. . . . 5 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (𝐴 Yrm (𝑁 mod (abs‘𝑀))) = (𝐴 Yrm (𝑁 + (-((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀))))
120	119	breq2d 5107	. . . 4 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 mod (abs‘𝑀))) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + (-((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) · 𝑀)))))
121	101, 120	bitr4d 282	. . 3 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 mod (abs‘𝑀)))))
122	86, 91, 121	3bitr4d 311	. 2 ⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → (𝑀 ∥ 𝑁 ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁)))
123	20, 122	pm2.61dane 3016	1 ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113   ≠ wne 2929   class class class wbr 5095  ‘cfv 6489  (class class class)co 7355  ℂcc 11015  ℝcr 11016  0cc0 11017   + caddc 11020   · cmul 11022   < clt 11157   ≤ cle 11158   − cmin 11355  -cneg 11356   / cdiv 11785  ℕcn 12136  2c2 12191  ℕ₀cn0 12392  ℤcz 12479  ℤ_≥cuz 12742  ℝ⁺crp 12896   mod cmo 13780  abscabs 15148   ∥ cdvds 16170   Y_rm crmy 43058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-inf2 9542  ax-cnex 11073  ax-resscn 11074  ax-1cn 11075  ax-icn 11076  ax-addcl 11077  ax-addrcl 11078  ax-mulcl 11079  ax-mulrcl 11080  ax-mulcom 11081  ax-addass 11082  ax-mulass 11083  ax-distr 11084  ax-i2m1 11085  ax-1ne0 11086  ax-1rid 11087  ax-rnegex 11088  ax-rrecex 11089  ax-cnre 11090  ax-pre-lttri 11091  ax-pre-lttrn 11092  ax-pre-ltadd 11093  ax-pre-mulgt0 11094  ax-pre-sup 11095  ax-addf 11096

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rmo 3347  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-tp 4582  df-op 4584  df-uni 4861  df-int 4900  df-iun 4945  df-iin 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-se 5575  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-isom 6498  df-riota 7312  df-ov 7358  df-oprab 7359  df-mpo 7360  df-of 7619  df-om 7806  df-1st 7930  df-2nd 7931  df-supp 8100  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-1o 8394  df-2o 8395  df-oadd 8398  df-omul 8399  df-er 8631  df-map 8761  df-pm 8762  df-ixp 8832  df-en 8880  df-dom 8881  df-sdom 8882  df-fin 8883  df-fsupp 9257  df-fi 9306  df-sup 9337  df-inf 9338  df-oi 9407  df-card 9843  df-acn 9846  df-pnf 11159  df-mnf 11160  df-xr 11161  df-ltxr 11162  df-le 11163  df-sub 11357  df-neg 11358  df-div 11786  df-nn 12137  df-2 12199  df-3 12200  df-4 12201  df-5 12202  df-6 12203  df-7 12204  df-8 12205  df-9 12206  df-n0 12393  df-xnn0 12466  df-z 12480  df-dec 12599  df-uz 12743  df-q 12853  df-rp 12897  df-xneg 13017  df-xadd 13018  df-xmul 13019  df-ioo 13256  df-ioc 13257  df-ico 13258  df-icc 13259  df-fz 13415  df-fzo 13562  df-fl 13703  df-mod 13781  df-seq 13916  df-exp 13976  df-fac 14188  df-bc 14217  df-hash 14245  df-shft 14981  df-cj 15013  df-re 15014  df-im 15015  df-sqrt 15149  df-abs 15150  df-limsup 15385  df-clim 15402  df-rlim 15403  df-sum 15601  df-ef 15981  df-sin 15983  df-cos 15984  df-pi 15986  df-dvds 16171  df-gcd 16413  df-numer 16653  df-denom 16654  df-struct 17065  df-sets 17082  df-slot 17100  df-ndx 17112  df-base 17128  df-ress 17149  df-plusg 17181  df-mulr 17182  df-starv 17183  df-sca 17184  df-vsca 17185  df-ip 17186  df-tset 17187  df-ple 17188  df-ds 17190  df-unif 17191  df-hom 17192  df-cco 17193  df-rest 17333  df-topn 17334  df-0g 17352  df-gsum 17353  df-topgen 17354  df-pt 17355  df-prds 17358  df-xrs 17414  df-qtop 17419  df-imas 17420  df-xps 17422  df-mre 17496  df-mrc 17497  df-acs 17499  df-mgm 18556  df-sgrp 18635  df-mnd 18651  df-submnd 18700  df-mulg 18989  df-cntz 19237  df-cmn 19702  df-psmet 21292  df-xmet 21293  df-met 21294  df-bl 21295  df-mopn 21296  df-fbas 21297  df-fg 21298  df-cnfld 21301  df-top 22829  df-topon 22846  df-topsp 22868  df-bases 22881  df-cld 22954  df-ntr 22955  df-cls 22956  df-nei 23033  df-lp 23071  df-perf 23072  df-cn 23162  df-cnp 23163  df-haus 23250  df-tx 23497  df-hmeo 23690  df-fil 23781  df-fm 23873  df-flim 23874  df-flf 23875  df-xms 24255  df-ms 24256  df-tms 24257  df-cncf 24818  df-limc 25814  df-dv 25815  df-log 26512  df-squarenn 42998  df-pell1qr 42999  df-pell14qr 43000  df-pell1234qr 43001  df-pellfund 43002  df-rmx 43059  df-rmy 43060

This theorem is referenced by:  jm2.20nn  43154