This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 · 𝐵 ) ) )