difsqpwdvds

Description: If the difference of two squares is a power of a prime, the prime divides twice the second squared number. (Contributed by AV, 13-Aug-2021)

		Ref	Expression
	Assertion	difsqpwdvds	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \to (C^{D} = A^{2} - B^{2} \to C ∥ 2 B)$

Proof

Step	Hyp	Ref	Expression
1		nn0cn	$⊢ A \in ℕ_{0} \to A \in ℂ$
2		nn0cn	$⊢ B \in ℕ_{0} \to B \in ℂ$
3	1 2	anim12i	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (A \in ℂ \land B \in ℂ)$
4	3	3adant3	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \to (A \in ℂ \land B \in ℂ)$
5		subsq	$⊢ (A \in ℂ \land B \in ℂ) \to A^{2} - B^{2} = (A + B) (A - B)$
6	4 5	syl	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \to A^{2} - B^{2} = (A + B) (A - B)$
7	6	adantr	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \to A^{2} - B^{2} = (A + B) (A - B)$
8	7	eqeq2d	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \to (C^{D} = A^{2} - B^{2} \leftrightarrow C^{D} = (A + B) (A - B))$
9		simprl	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \to C \in ℙ$
10		nn0z	$⊢ A \in ℕ_{0} \to A \in ℤ$
11		nn0z	$⊢ B \in ℕ_{0} \to B \in ℤ$
12	10 11	anim12i	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (A \in ℤ \land B \in ℤ)$
13		zaddcl	$⊢ (A \in ℤ \land B \in ℤ) \to A + B \in ℤ$
14	12 13	syl	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to A + B \in ℤ$
15	14	3adant3	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \to A + B \in ℤ$
16		nn0re	$⊢ B \in ℕ_{0} \to B \in ℝ$
17	16	adantl	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to B \in ℝ$
18		1red	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to 1 \in ℝ$
19		nn0re	$⊢ A \in ℕ_{0} \to A \in ℝ$
20	19	adantr	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to A \in ℝ$
21	17 18 20	ltaddsub2d	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (B + 1 < A \leftrightarrow 1 < A - B)$
22		simpr	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to B \in ℕ_{0}$
23	20 22 18	3jca	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (A \in ℝ \land B \in ℕ_{0} \land 1 \in ℝ)$
24		difgtsumgt	$⊢ (A \in ℝ \land B \in ℕ_{0} \land 1 \in ℝ) \to (1 < A - B \to 1 < A + B)$
25	23 24	syl	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (1 < A - B \to 1 < A + B)$
26	21 25	sylbid	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (B + 1 < A \to 1 < A + B)$
27	26	3impia	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \to 1 < A + B$
28		eluz2b1	$⊢ A + B \in ℤ_{\geq 2} \leftrightarrow (A + B \in ℤ \land 1 < A + B)$
29	15 27 28	sylanbrc	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \to A + B \in ℤ_{\geq 2}$
30	29	adantr	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \to A + B \in ℤ_{\geq 2}$
31		simprr	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \to D \in ℕ_{0}$
32	9 30 31	3jca	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \to (C \in ℙ \land A + B \in ℤ_{\geq 2} \land D \in ℕ_{0})$
33	32	adantr	$⊢ (((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \land C^{D} = (A + B) (A - B)) \to (C \in ℙ \land A + B \in ℤ_{\geq 2} \land D \in ℕ_{0})$
34		zsubcl	$⊢ (A \in ℤ \land B \in ℤ) \to A - B \in ℤ$
35	13 34	jca	$⊢ (A \in ℤ \land B \in ℤ) \to (A + B \in ℤ \land A - B \in ℤ)$
36	12 35	syl	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (A + B \in ℤ \land A - B \in ℤ)$
37	36	3adant3	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \to (A + B \in ℤ \land A - B \in ℤ)$
38		dvdsmul1	$⊢ (A + B \in ℤ \land A - B \in ℤ) \to (A + B) ∥ (A + B) (A - B)$
39	37 38	syl	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \to (A + B) ∥ (A + B) (A - B)$
40	39	ad2antrr	$⊢ (((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \land C^{D} = (A + B) (A - B)) \to (A + B) ∥ (A + B) (A - B)$
41		breq2	$⊢ C^{D} = (A + B) (A - B) \to ((A + B) ∥ C^{D} \leftrightarrow (A + B) ∥ (A + B) (A - B))$
42	41	adantl	$⊢ (((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \land C^{D} = (A + B) (A - B)) \to ((A + B) ∥ C^{D} \leftrightarrow (A + B) ∥ (A + B) (A - B))$
43	40 42	mpbird	$⊢ (((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \land C^{D} = (A + B) (A - B)) \to (A + B) ∥ C^{D}$
44		dvdsprmpweqnn	$⊢ (C \in ℙ \land A + B \in ℤ_{\geq 2} \land D \in ℕ_{0}) \to ((A + B) ∥ C^{D} \to \exists m \in ℕ A + B = C^{m})$
45	33 43 44	sylc	$⊢ (((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \land C^{D} = (A + B) (A - B)) \to \exists m \in ℕ A + B = C^{m}$
46		prmz	$⊢ C \in ℙ \to C \in ℤ$
47		iddvdsexp	$⊢ (C \in ℤ \land m \in ℕ) \to C ∥ C^{m}$
48	46 47	sylan	$⊢ (C \in ℙ \land m \in ℕ) \to C ∥ C^{m}$
49		breq2	$⊢ A + B = C^{m} \to (C ∥ (A + B) \leftrightarrow C ∥ C^{m})$
50	48 49	syl5ibrcom	$⊢ (C \in ℙ \land m \in ℕ) \to (A + B = C^{m} \to C ∥ (A + B))$
51	50	rexlimdva	$⊢ C \in ℙ \to (\exists m \in ℕ A + B = C^{m} \to C ∥ (A + B))$
52	51	adantr	$⊢ (C \in ℙ \land D \in ℕ_{0}) \to (\exists m \in ℕ A + B = C^{m} \to C ∥ (A + B))$
53	52	adantl	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \to (\exists m \in ℕ A + B = C^{m} \to C ∥ (A + B))$
54	53	adantr	$⊢ (((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \land C^{D} = (A + B) (A - B)) \to (\exists m \in ℕ A + B = C^{m} \to C ∥ (A + B))$
55	12 34	syl	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to A - B \in ℤ$
56	55	3adant3	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \to A - B \in ℤ$
57	21	biimp3a	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \to 1 < A - B$
58		eluz2b1	$⊢ A - B \in ℤ_{\geq 2} \leftrightarrow (A - B \in ℤ \land 1 < A - B)$
59	56 57 58	sylanbrc	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \to A - B \in ℤ_{\geq 2}$
60	59	adantr	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \to A - B \in ℤ_{\geq 2}$
61	9 60 31	3jca	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \to (C \in ℙ \land A - B \in ℤ_{\geq 2} \land D \in ℕ_{0})$
62	61	adantr	$⊢ (((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \land C^{D} = (A + B) (A - B)) \to (C \in ℙ \land A - B \in ℤ_{\geq 2} \land D \in ℕ_{0})$
63		dvdsmul2	$⊢ (A + B \in ℤ \land A - B \in ℤ) \to (A - B) ∥ (A + B) (A - B)$
64	37 63	syl	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \to (A - B) ∥ (A + B) (A - B)$
65	64	ad2antrr	$⊢ (((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \land C^{D} = (A + B) (A - B)) \to (A - B) ∥ (A + B) (A - B)$
66		breq2	$⊢ C^{D} = (A + B) (A - B) \to ((A - B) ∥ C^{D} \leftrightarrow (A - B) ∥ (A + B) (A - B))$
67	66	adantl	$⊢ (((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \land C^{D} = (A + B) (A - B)) \to ((A - B) ∥ C^{D} \leftrightarrow (A - B) ∥ (A + B) (A - B))$
68	65 67	mpbird	$⊢ (((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \land C^{D} = (A + B) (A - B)) \to (A - B) ∥ C^{D}$
69		dvdsprmpweqnn	$⊢ (C \in ℙ \land A - B \in ℤ_{\geq 2} \land D \in ℕ_{0}) \to ((A - B) ∥ C^{D} \to \exists n \in ℕ A - B = C^{n})$
70	62 68 69	sylc	$⊢ (((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \land C^{D} = (A + B) (A - B)) \to \exists n \in ℕ A - B = C^{n}$
71		iddvdsexp	$⊢ (C \in ℤ \land n \in ℕ) \to C ∥ C^{n}$
72	46 71	sylan	$⊢ (C \in ℙ \land n \in ℕ) \to C ∥ C^{n}$
73		breq2	$⊢ A - B = C^{n} \to (C ∥ (A - B) \leftrightarrow C ∥ C^{n})$
74	72 73	syl5ibrcom	$⊢ (C \in ℙ \land n \in ℕ) \to (A - B = C^{n} \to C ∥ (A - B))$
75	74	rexlimdva	$⊢ C \in ℙ \to (\exists n \in ℕ A - B = C^{n} \to C ∥ (A - B))$
76	75	adantr	$⊢ (C \in ℙ \land D \in ℕ_{0}) \to (\exists n \in ℕ A - B = C^{n} \to C ∥ (A - B))$
77	76	adantl	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \to (\exists n \in ℕ A - B = C^{n} \to C ∥ (A - B))$
78	77	adantr	$⊢ (((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \land C^{D} = (A + B) (A - B)) \to (\exists n \in ℕ A - B = C^{n} \to C ∥ (A - B))$
79	46	adantr	$⊢ (C \in ℙ \land D \in ℕ_{0}) \to C \in ℤ$
80	37 79	anim12ci	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \to (C \in ℤ \land (A + B \in ℤ \land A - B \in ℤ))$
81		3anass	$⊢ (C \in ℤ \land A + B \in ℤ \land A - B \in ℤ) \leftrightarrow (C \in ℤ \land (A + B \in ℤ \land A - B \in ℤ))$
82	80 81	sylibr	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \to (C \in ℤ \land A + B \in ℤ \land A - B \in ℤ)$
83		dvds2sub	$⊢ (C \in ℤ \land A + B \in ℤ \land A - B \in ℤ) \to ((C ∥ (A + B) \land C ∥ (A - B)) \to C ∥ (A + B - (A - B)))$
84	82 83	syl	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \to ((C ∥ (A + B) \land C ∥ (A - B)) \to C ∥ (A + B - (A - B)))$
85	1	3ad2ant1	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \to A \in ℂ$
86	2	3ad2ant2	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \to B \in ℂ$
87	85 86 86	pnncand	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \to A + B - (A - B) = B + B$
88	2	2timesd	$⊢ B \in ℕ_{0} \to 2 B = B + B$
89	88	eqcomd	$⊢ B \in ℕ_{0} \to B + B = 2 B$
90	89	3ad2ant2	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \to B + B = 2 B$
91	87 90	eqtrd	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \to A + B - (A - B) = 2 B$
92	91	breq2d	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \to (C ∥ (A + B - (A - B)) \leftrightarrow C ∥ 2 B)$
93	92	biimpd	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \to (C ∥ (A + B - (A - B)) \to C ∥ 2 B)$
94	93	adantr	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \to (C ∥ (A + B - (A - B)) \to C ∥ 2 B)$
95	84 94	syld	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \to ((C ∥ (A + B) \land C ∥ (A - B)) \to C ∥ 2 B)$
96	95	expcomd	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \to (C ∥ (A - B) \to (C ∥ (A + B) \to C ∥ 2 B))$
97	96	adantr	$⊢ (((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \land C^{D} = (A + B) (A - B)) \to (C ∥ (A - B) \to (C ∥ (A + B) \to C ∥ 2 B))$
98	78 97	syld	$⊢ (((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \land C^{D} = (A + B) (A - B)) \to (\exists n \in ℕ A - B = C^{n} \to (C ∥ (A + B) \to C ∥ 2 B))$
99	70 98	mpd	$⊢ (((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \land C^{D} = (A + B) (A - B)) \to (C ∥ (A + B) \to C ∥ 2 B)$
100	54 99	syld	$⊢ (((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \land C^{D} = (A + B) (A - B)) \to (\exists m \in ℕ A + B = C^{m} \to C ∥ 2 B)$
101	45 100	mpd	$⊢ (((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \land C^{D} = (A + B) (A - B)) \to C ∥ 2 B$
102	101	ex	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \to (C^{D} = (A + B) (A - B) \to C ∥ 2 B)$
103	8 102	sylbid	$⊢ ((A \in ℕ_{0} \land B \in ℕ_{0} \land B + 1 < A) \land (C \in ℙ \land D \in ℕ_{0})) \to (C^{D} = A^{2} - B^{2} \to C ∥ 2 B)$

Metamath Proof Explorer

Theorem difsqpwdvds

Proof