Theorem 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	⊢ ( ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ ( 𝐵 + 1 ) < 𝐴 ) ∧ ( 𝐶 ∈ ℙ ∧ 𝐷 ∈ ℕ0 ) ) → ( ( 𝐶 ↑ 𝐷 ) = ( ( 𝐴 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) → 𝐶 ∥ ( 2 · 𝐵 ) ) )

Proof

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