dvdssq

Description: Two numbers are divisible iff their squares are. (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	dvdssq	$⊢ (M \in ℤ \land N \in ℤ) \to (M ∥ N \leftrightarrow M^{2} ∥ N^{2})$

Proof

Step	Hyp	Ref	Expression
1		breq1	$⊢ M = 0 \to (M ∥ N \leftrightarrow 0 ∥ N)$
2		sq0i	$⊢ M = 0 \to M^{2} = 0$
3	2	breq1d	$⊢ M = 0 \to (M^{2} ∥ N^{2} \leftrightarrow 0 ∥ N^{2})$
4	1 3	bibi12d	$⊢ M = 0 \to ((M ∥ N \leftrightarrow M^{2} ∥ N^{2}) \leftrightarrow (0 ∥ N \leftrightarrow 0 ∥ N^{2}))$
5		nnabscl	$⊢ (M \in ℤ \land M \neq 0) \to \|M\| \in ℕ$
6		breq2	$⊢ N = 0 \to (\|M\| ∥ N \leftrightarrow \|M\| ∥ 0)$
7		sq0i	$⊢ N = 0 \to N^{2} = 0$
8	7	breq2d	$⊢ N = 0 \to ({\|M\|}^{2} ∥ N^{2} \leftrightarrow {\|M\|}^{2} ∥ 0)$
9	6 8	bibi12d	$⊢ N = 0 \to ((\|M\| ∥ N \leftrightarrow {\|M\|}^{2} ∥ N^{2}) \leftrightarrow (\|M\| ∥ 0 \leftrightarrow {\|M\|}^{2} ∥ 0))$
10		nnabscl	$⊢ (N \in ℤ \land N \neq 0) \to \|N\| \in ℕ$
11		dvdssqlem	$⊢ (\|M\| \in ℕ \land \|N\| \in ℕ) \to (\|M\| ∥ \|N\| \leftrightarrow {\|M\|}^{2} ∥ {\|N\|}^{2})$
12	10 11	sylan2	$⊢ (\|M\| \in ℕ \land (N \in ℤ \land N \neq 0)) \to (\|M\| ∥ \|N\| \leftrightarrow {\|M\|}^{2} ∥ {\|N\|}^{2})$
13		nnz	$⊢ \|M\| \in ℕ \to \|M\| \in ℤ$
14		simpl	$⊢ (N \in ℤ \land N \neq 0) \to N \in ℤ$
15		dvdsabsb	$⊢ (\|M\| \in ℤ \land N \in ℤ) \to (\|M\| ∥ N \leftrightarrow \|M\| ∥ \|N\|)$
16	13 14 15	syl2an	$⊢ (\|M\| \in ℕ \land (N \in ℤ \land N \neq 0)) \to (\|M\| ∥ N \leftrightarrow \|M\| ∥ \|N\|)$
17		nnsqcl	$⊢ \|M\| \in ℕ \to {\|M\|}^{2} \in ℕ$
18	17	nnzd	$⊢ \|M\| \in ℕ \to {\|M\|}^{2} \in ℤ$
19		zsqcl	$⊢ N \in ℤ \to N^{2} \in ℤ$
20	19	adantr	$⊢ (N \in ℤ \land N \neq 0) \to N^{2} \in ℤ$
21		dvdsabsb	$⊢ ({\|M\|}^{2} \in ℤ \land N^{2} \in ℤ) \to ({\|M\|}^{2} ∥ N^{2} \leftrightarrow {\|M\|}^{2} ∥ \|N^{2}\|)$
22	18 20 21	syl2an	$⊢ (\|M\| \in ℕ \land (N \in ℤ \land N \neq 0)) \to ({\|M\|}^{2} ∥ N^{2} \leftrightarrow {\|M\|}^{2} ∥ \|N^{2}\|)$
23		zcn	$⊢ N \in ℤ \to N \in ℂ$
24	23	adantr	$⊢ (N \in ℤ \land N \neq 0) \to N \in ℂ$
25		abssq	$⊢ N \in ℂ \to {\|N\|}^{2} = \|N^{2}\|$
26	24 25	syl	$⊢ (N \in ℤ \land N \neq 0) \to {\|N\|}^{2} = \|N^{2}\|$
27	26	breq2d	$⊢ (N \in ℤ \land N \neq 0) \to ({\|M\|}^{2} ∥ {\|N\|}^{2} \leftrightarrow {\|M\|}^{2} ∥ \|N^{2}\|)$
28	27	adantl	$⊢ (\|M\| \in ℕ \land (N \in ℤ \land N \neq 0)) \to ({\|M\|}^{2} ∥ {\|N\|}^{2} \leftrightarrow {\|M\|}^{2} ∥ \|N^{2}\|)$
29	22 28	bitr4d	$⊢ (\|M\| \in ℕ \land (N \in ℤ \land N \neq 0)) \to ({\|M\|}^{2} ∥ N^{2} \leftrightarrow {\|M\|}^{2} ∥ {\|N\|}^{2})$
30	12 16 29	3bitr4d	$⊢ (\|M\| \in ℕ \land (N \in ℤ \land N \neq 0)) \to (\|M\| ∥ N \leftrightarrow {\|M\|}^{2} ∥ N^{2})$
31	30	anassrs	$⊢ ((\|M\| \in ℕ \land N \in ℤ) \land N \neq 0) \to (\|M\| ∥ N \leftrightarrow {\|M\|}^{2} ∥ N^{2})$
32		dvds0	$⊢ \|M\| \in ℤ \to \|M\| ∥ 0$
33		zsqcl	$⊢ \|M\| \in ℤ \to {\|M\|}^{2} \in ℤ$
34		dvds0	$⊢ {\|M\|}^{2} \in ℤ \to {\|M\|}^{2} ∥ 0$
35	33 34	syl	$⊢ \|M\| \in ℤ \to {\|M\|}^{2} ∥ 0$
36	32 35	2thd	$⊢ \|M\| \in ℤ \to (\|M\| ∥ 0 \leftrightarrow {\|M\|}^{2} ∥ 0)$
37	13 36	syl	$⊢ \|M\| \in ℕ \to (\|M\| ∥ 0 \leftrightarrow {\|M\|}^{2} ∥ 0)$
38	37	adantr	$⊢ (\|M\| \in ℕ \land N \in ℤ) \to (\|M\| ∥ 0 \leftrightarrow {\|M\|}^{2} ∥ 0)$
39	9 31 38	pm2.61ne	$⊢ (\|M\| \in ℕ \land N \in ℤ) \to (\|M\| ∥ N \leftrightarrow {\|M\|}^{2} ∥ N^{2})$
40	5 39	sylan	$⊢ ((M \in ℤ \land M \neq 0) \land N \in ℤ) \to (\|M\| ∥ N \leftrightarrow {\|M\|}^{2} ∥ N^{2})$
41		absdvdsb	$⊢ (M \in ℤ \land N \in ℤ) \to (M ∥ N \leftrightarrow \|M\| ∥ N)$
42	41	adantlr	$⊢ ((M \in ℤ \land M \neq 0) \land N \in ℤ) \to (M ∥ N \leftrightarrow \|M\| ∥ N)$
43		zsqcl	$⊢ M \in ℤ \to M^{2} \in ℤ$
44	43	adantr	$⊢ (M \in ℤ \land M \neq 0) \to M^{2} \in ℤ$
45		absdvdsb	$⊢ (M^{2} \in ℤ \land N^{2} \in ℤ) \to (M^{2} ∥ N^{2} \leftrightarrow \|M^{2}\| ∥ N^{2})$
46	44 19 45	syl2an	$⊢ ((M \in ℤ \land M \neq 0) \land N \in ℤ) \to (M^{2} ∥ N^{2} \leftrightarrow \|M^{2}\| ∥ N^{2})$
47		zcn	$⊢ M \in ℤ \to M \in ℂ$
48		abssq	$⊢ M \in ℂ \to {\|M\|}^{2} = \|M^{2}\|$
49	47 48	syl	$⊢ M \in ℤ \to {\|M\|}^{2} = \|M^{2}\|$
50	49	eqcomd	$⊢ M \in ℤ \to \|M^{2}\| = {\|M\|}^{2}$
51	50	adantr	$⊢ (M \in ℤ \land M \neq 0) \to \|M^{2}\| = {\|M\|}^{2}$
52	51	breq1d	$⊢ (M \in ℤ \land M \neq 0) \to (\|M^{2}\| ∥ N^{2} \leftrightarrow {\|M\|}^{2} ∥ N^{2})$
53	52	adantr	$⊢ ((M \in ℤ \land M \neq 0) \land N \in ℤ) \to (\|M^{2}\| ∥ N^{2} \leftrightarrow {\|M\|}^{2} ∥ N^{2})$
54	46 53	bitrd	$⊢ ((M \in ℤ \land M \neq 0) \land N \in ℤ) \to (M^{2} ∥ N^{2} \leftrightarrow {\|M\|}^{2} ∥ N^{2})$
55	40 42 54	3bitr4d	$⊢ ((M \in ℤ \land M \neq 0) \land N \in ℤ) \to (M ∥ N \leftrightarrow M^{2} ∥ N^{2})$
56	55	an32s	$⊢ ((M \in ℤ \land N \in ℤ) \land M \neq 0) \to (M ∥ N \leftrightarrow M^{2} ∥ N^{2})$
57		0dvds	$⊢ N \in ℤ \to (0 ∥ N \leftrightarrow N = 0)$
58		sqeq0	$⊢ N \in ℂ \to (N^{2} = 0 \leftrightarrow N = 0)$
59	23 58	syl	$⊢ N \in ℤ \to (N^{2} = 0 \leftrightarrow N = 0)$
60	57 59	bitr4d	$⊢ N \in ℤ \to (0 ∥ N \leftrightarrow N^{2} = 0)$
61		0dvds	$⊢ N^{2} \in ℤ \to (0 ∥ N^{2} \leftrightarrow N^{2} = 0)$
62	19 61	syl	$⊢ N \in ℤ \to (0 ∥ N^{2} \leftrightarrow N^{2} = 0)$
63	60 62	bitr4d	$⊢ N \in ℤ \to (0 ∥ N \leftrightarrow 0 ∥ N^{2})$
64	63	adantl	$⊢ (M \in ℤ \land N \in ℤ) \to (0 ∥ N \leftrightarrow 0 ∥ N^{2})$
65	4 56 64	pm2.61ne	$⊢ (M \in ℤ \land N \in ℤ) \to (M ∥ N \leftrightarrow M^{2} ∥ N^{2})$

Metamath Proof Explorer

Theorem dvdssq

Proof