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