Metamath Proof Explorer

Theorem jm2.27a

Description: Lemma for jm2.27 . Reverse direction after existential quantifiers are expanded. (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Hypotheses jm2.27a1 ⊢ ( 𝜑 → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
jm2.27a2 ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
jm2.27a3 ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
jm2.27a4 ⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
jm2.27a5 ⊢ ( 𝜑 → 𝐸 ∈ ℕ0 )
jm2.27a6 ⊢ ( 𝜑 → 𝐹 ∈ ℕ0 )
jm2.27a7 ⊢ ( 𝜑 → 𝐺 ∈ ℕ0 )
jm2.27a8 ⊢ ( 𝜑 → 𝐻 ∈ ℕ0 )
jm2.27a9 ⊢ ( 𝜑 → 𝐼 ∈ ℕ0 )
jm2.27a10 ⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
jm2.27a11 ⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐶 ↑ 2 ) ) ) = 1 )
jm2.27a12 ⊢ ( 𝜑 → ( ( 𝐹 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 ↑ 2 ) ) ) = 1 )
jm2.27a13 ⊢ ( 𝜑 → 𝐺 ∈ ( ℤ≥ ‘ 2 ) )
jm2.27a14 ⊢ ( 𝜑 → ( ( 𝐼 ↑ 2 ) − ( ( ( 𝐺 ↑ 2 ) − 1 ) · ( 𝐻 ↑ 2 ) ) ) = 1 )
jm2.27a15 ⊢ ( 𝜑 → 𝐸 = ( ( 𝐽 + 1 ) · ( 2 · ( 𝐶 ↑ 2 ) ) ) )
jm2.27a16 ⊢ ( 𝜑 → 𝐹 ∥ ( 𝐺 − 𝐴 ) )
jm2.27a17 ⊢ ( 𝜑 → ( 2 · 𝐶 ) ∥ ( 𝐺 − 1 ) )
jm2.27a18 ⊢ ( 𝜑 → 𝐹 ∥ ( 𝐻 − 𝐶 ) )
jm2.27a19 ⊢ ( 𝜑 → ( 2 · 𝐶 ) ∥ ( 𝐻 − 𝐵 ) )
jm2.27a20 ⊢ ( 𝜑 → 𝐵 ≤ 𝐶 )
jm2.27a21 ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
jm2.27a22 ⊢ ( 𝜑 → 𝐷 = ( 𝐴 Xrm 𝑃 ) )
jm2.27a23 ⊢ ( 𝜑 → 𝐶 = ( 𝐴 Yrm 𝑃 ) )
jm2.27a24 ⊢ ( 𝜑 → 𝑄 ∈ ℤ )
jm2.27a25 ⊢ ( 𝜑 → 𝐹 = ( 𝐴 Xrm 𝑄 ) )
jm2.27a26 ⊢ ( 𝜑 → 𝐸 = ( 𝐴 Yrm 𝑄 ) )
jm2.27a27 ⊢ ( 𝜑 → 𝑅 ∈ ℤ )
jm2.27a28 ⊢ ( 𝜑 → 𝐼 = ( 𝐺 Xrm 𝑅 ) )
jm2.27a29 ⊢ ( 𝜑 → 𝐻 = ( 𝐺 Yrm 𝑅 ) )
Assertion jm2.27a ( 𝜑 → 𝐶 = ( 𝐴 Yrm 𝐵 ) )

Proof

Step Hyp Ref Expression
1 jm2.27a1 ⊢ ( 𝜑 → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
2 jm2.27a2 ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3 jm2.27a3 ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
4 jm2.27a4 ⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
5 jm2.27a5 ⊢ ( 𝜑 → 𝐸 ∈ ℕ0 )
6 jm2.27a6 ⊢ ( 𝜑 → 𝐹 ∈ ℕ0 )
7 jm2.27a7 ⊢ ( 𝜑 → 𝐺 ∈ ℕ0 )
8 jm2.27a8 ⊢ ( 𝜑 → 𝐻 ∈ ℕ0 )
9 jm2.27a9 ⊢ ( 𝜑 → 𝐼 ∈ ℕ0 )
10 jm2.27a10 ⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
11 jm2.27a11 ⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐶 ↑ 2 ) ) ) = 1 )
12 jm2.27a12 ⊢ ( 𝜑 → ( ( 𝐹 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 ↑ 2 ) ) ) = 1 )
13 jm2.27a13 ⊢ ( 𝜑 → 𝐺 ∈ ( ℤ≥ ‘ 2 ) )
14 jm2.27a14 ⊢ ( 𝜑 → ( ( 𝐼 ↑ 2 ) − ( ( ( 𝐺 ↑ 2 ) − 1 ) · ( 𝐻 ↑ 2 ) ) ) = 1 )
15 jm2.27a15 ⊢ ( 𝜑 → 𝐸 = ( ( 𝐽 + 1 ) · ( 2 · ( 𝐶 ↑ 2 ) ) ) )
16 jm2.27a16 ⊢ ( 𝜑 → 𝐹 ∥ ( 𝐺 − 𝐴 ) )
17 jm2.27a17 ⊢ ( 𝜑 → ( 2 · 𝐶 ) ∥ ( 𝐺 − 1 ) )
18 jm2.27a18 ⊢ ( 𝜑 → 𝐹 ∥ ( 𝐻 − 𝐶 ) )
19 jm2.27a19 ⊢ ( 𝜑 → ( 2 · 𝐶 ) ∥ ( 𝐻 − 𝐵 ) )
20 jm2.27a20 ⊢ ( 𝜑 → 𝐵 ≤ 𝐶 )
21 jm2.27a21 ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
22 jm2.27a22 ⊢ ( 𝜑 → 𝐷 = ( 𝐴 Xrm 𝑃 ) )
23 jm2.27a23 ⊢ ( 𝜑 → 𝐶 = ( 𝐴 Yrm 𝑃 ) )
24 jm2.27a24 ⊢ ( 𝜑 → 𝑄 ∈ ℤ )
25 jm2.27a25 ⊢ ( 𝜑 → 𝐹 = ( 𝐴 Xrm 𝑄 ) )
26 jm2.27a26 ⊢ ( 𝜑 → 𝐸 = ( 𝐴 Yrm 𝑄 ) )
27 jm2.27a27 ⊢ ( 𝜑 → 𝑅 ∈ ℤ )
28 jm2.27a28 ⊢ ( 𝜑 → 𝐼 = ( 𝐺 Xrm 𝑅 ) )
29 jm2.27a29 ⊢ ( 𝜑 → 𝐻 = ( 𝐺 Yrm 𝑅 ) )
30 2z ⊢ 2 ∈ ℤ
31 3 nnzd ⊢ ( 𝜑 → 𝐶 ∈ ℤ )
32 zmulcl ⊢ ( ( 2 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 2 · 𝐶 ) ∈ ℤ )
33 30 31 32 sylancr ⊢ ( 𝜑 → ( 2 · 𝐶 ) ∈ ℤ )
34 2 nnzd ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
35 8 nn0zd ⊢ ( 𝜑 → 𝐻 ∈ ℤ )
36 congsym ⊢ ( ( ( ( 2 · 𝐶 ) ∈ ℤ ∧ 𝐻 ∈ ℤ ) ∧ ( 𝐵 ∈ ℤ ∧ ( 2 · 𝐶 ) ∥ ( 𝐻 − 𝐵 ) ) ) → ( 2 · 𝐶 ) ∥ ( 𝐵 − 𝐻 ) )
37 33 35 34 19 36 syl22anc ⊢ ( 𝜑 → ( 2 · 𝐶 ) ∥ ( 𝐵 − 𝐻 ) )
38 7 nn0zd ⊢ ( 𝜑 → 𝐺 ∈ ℤ )
39 peano2zm ⊢ ( 𝐺 ∈ ℤ → ( 𝐺 − 1 ) ∈ ℤ )
40 38 39 syl ⊢ ( 𝜑 → ( 𝐺 − 1 ) ∈ ℤ )
41 35 27 zsubcld ⊢ ( 𝜑 → ( 𝐻 − 𝑅 ) ∈ ℤ )
42 8 nn0ge0d ⊢ ( 𝜑 → 0 ≤ 𝐻 )
43 rmy0 ⊢ ( 𝐺 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐺 Yrm 0 ) = 0 )
44 13 43 syl ⊢ ( 𝜑 → ( 𝐺 Yrm 0 ) = 0 )
45 29 eqcomd ⊢ ( 𝜑 → ( 𝐺 Yrm 𝑅 ) = 𝐻 )
46 42 44 45 3brtr4d ⊢ ( 𝜑 → ( 𝐺 Yrm 0 ) ≤ ( 𝐺 Yrm 𝑅 ) )
47 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
48 lermy ⊢ ( ( 𝐺 ∈ ( ℤ≥ ‘ 2 ) ∧ 0 ∈ ℤ ∧ 𝑅 ∈ ℤ ) → ( 0 ≤ 𝑅 ↔ ( 𝐺 Yrm 0 ) ≤ ( 𝐺 Yrm 𝑅 ) ) )
49 13 47 27 48 syl3anc ⊢ ( 𝜑 → ( 0 ≤ 𝑅 ↔ ( 𝐺 Yrm 0 ) ≤ ( 𝐺 Yrm 𝑅 ) ) )
50 46 49 mpbird ⊢ ( 𝜑 → 0 ≤ 𝑅 )
51 elnn0z ⊢ ( 𝑅 ∈ ℕ0 ↔ ( 𝑅 ∈ ℤ ∧ 0 ≤ 𝑅 ) )
52 27 50 51 sylanbrc ⊢ ( 𝜑 → 𝑅 ∈ ℕ0 )
53 jm2.16nn0 ⊢ ( ( 𝐺 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ ℕ0 ) → ( 𝐺 − 1 ) ∥ ( ( 𝐺 Yrm 𝑅 ) − 𝑅 ) )
54 13 52 53 syl2anc ⊢ ( 𝜑 → ( 𝐺 − 1 ) ∥ ( ( 𝐺 Yrm 𝑅 ) − 𝑅 ) )
55 29 oveq1d ⊢ ( 𝜑 → ( 𝐻 − 𝑅 ) = ( ( 𝐺 Yrm 𝑅 ) − 𝑅 ) )
56 54 55 breqtrrd ⊢ ( 𝜑 → ( 𝐺 − 1 ) ∥ ( 𝐻 − 𝑅 ) )
57 33 40 41 17 56 dvdstrd ⊢ ( 𝜑 → ( 2 · 𝐶 ) ∥ ( 𝐻 − 𝑅 ) )
58 congtr ⊢ ( ( ( ( 2 · 𝐶 ) ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐻 ∈ ℤ ∧ 𝑅 ∈ ℤ ) ∧ ( ( 2 · 𝐶 ) ∥ ( 𝐵 − 𝐻 ) ∧ ( 2 · 𝐶 ) ∥ ( 𝐻 − 𝑅 ) ) ) → ( 2 · 𝐶 ) ∥ ( 𝐵 − 𝑅 ) )
59 33 34 35 27 37 57 58 syl222anc ⊢ ( 𝜑 → ( 2 · 𝐶 ) ∥ ( 𝐵 − 𝑅 ) )
60 59 orcd ⊢ ( 𝜑 → ( ( 2 · 𝐶 ) ∥ ( 𝐵 − 𝑅 ) ∨ ( 2 · 𝐶 ) ∥ ( 𝐵 − - 𝑅 ) ) )
61 zmulcl ⊢ ( ( 2 ∈ ℤ ∧ 𝑄 ∈ ℤ ) → ( 2 · 𝑄 ) ∈ ℤ )
62 30 24 61 sylancr ⊢ ( 𝜑 → ( 2 · 𝑄 ) ∈ ℤ )
63 zsqcl ⊢ ( 𝐶 ∈ ℤ → ( 𝐶 ↑ 2 ) ∈ ℤ )
64 31 63 syl ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℤ )
65 dvdsmul2 ⊢ ( ( 2 ∈ ℤ ∧ ( 𝐶 ↑ 2 ) ∈ ℤ ) → ( 𝐶 ↑ 2 ) ∥ ( 2 · ( 𝐶 ↑ 2 ) ) )
66 30 64 65 sylancr ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∥ ( 2 · ( 𝐶 ↑ 2 ) ) )
67 10 nn0zd ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
68 67 peano2zd ⊢ ( 𝜑 → ( 𝐽 + 1 ) ∈ ℤ )
69 zmulcl ⊢ ( ( 2 ∈ ℤ ∧ ( 𝐶 ↑ 2 ) ∈ ℤ ) → ( 2 · ( 𝐶 ↑ 2 ) ) ∈ ℤ )
70 30 64 69 sylancr ⊢ ( 𝜑 → ( 2 · ( 𝐶 ↑ 2 ) ) ∈ ℤ )
71 dvdsmultr2 ⊢ ( ( ( 𝐶 ↑ 2 ) ∈ ℤ ∧ ( 𝐽 + 1 ) ∈ ℤ ∧ ( 2 · ( 𝐶 ↑ 2 ) ) ∈ ℤ ) → ( ( 𝐶 ↑ 2 ) ∥ ( 2 · ( 𝐶 ↑ 2 ) ) → ( 𝐶 ↑ 2 ) ∥ ( ( 𝐽 + 1 ) · ( 2 · ( 𝐶 ↑ 2 ) ) ) ) )
72 64 68 70 71 syl3anc ⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) ∥ ( 2 · ( 𝐶 ↑ 2 ) ) → ( 𝐶 ↑ 2 ) ∥ ( ( 𝐽 + 1 ) · ( 2 · ( 𝐶 ↑ 2 ) ) ) ) )
73 66 72 mpd ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∥ ( ( 𝐽 + 1 ) · ( 2 · ( 𝐶 ↑ 2 ) ) ) )
74 23 oveq1d ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) = ( ( 𝐴 Yrm 𝑃 ) ↑ 2 ) )
75 15 26 eqtr3d ⊢ ( 𝜑 → ( ( 𝐽 + 1 ) · ( 2 · ( 𝐶 ↑ 2 ) ) ) = ( 𝐴 Yrm 𝑄 ) )
76 73 74 75 3brtr3d ⊢ ( 𝜑 → ( ( 𝐴 Yrm 𝑃 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑄 ) )
77 68 zred ⊢ ( 𝜑 → ( 𝐽 + 1 ) ∈ ℝ )
78 70 zred ⊢ ( 𝜑 → ( 2 · ( 𝐶 ↑ 2 ) ) ∈ ℝ )
79 nn0p1nn ⊢ ( 𝐽 ∈ ℕ0 → ( 𝐽 + 1 ) ∈ ℕ )
80 10 79 syl ⊢ ( 𝜑 → ( 𝐽 + 1 ) ∈ ℕ )
81 80 nngt0d ⊢ ( 𝜑 → 0 < ( 𝐽 + 1 ) )
82 2nn ⊢ 2 ∈ ℕ
83 3 nnsqcld ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℕ )
84 nnmulcl ⊢ ( ( 2 ∈ ℕ ∧ ( 𝐶 ↑ 2 ) ∈ ℕ ) → ( 2 · ( 𝐶 ↑ 2 ) ) ∈ ℕ )
85 82 83 84 sylancr ⊢ ( 𝜑 → ( 2 · ( 𝐶 ↑ 2 ) ) ∈ ℕ )
86 85 nngt0d ⊢ ( 𝜑 → 0 < ( 2 · ( 𝐶 ↑ 2 ) ) )
87 77 78 81 86 mulgt0d ⊢ ( 𝜑 → 0 < ( ( 𝐽 + 1 ) · ( 2 · ( 𝐶 ↑ 2 ) ) ) )
88 87 15 breqtrrd ⊢ ( 𝜑 → 0 < 𝐸 )
89 rmy0 ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm 0 ) = 0 )
90 1 89 syl ⊢ ( 𝜑 → ( 𝐴 Yrm 0 ) = 0 )
91 26 eqcomd ⊢ ( 𝜑 → ( 𝐴 Yrm 𝑄 ) = 𝐸 )
92 88 90 91 3brtr4d ⊢ ( 𝜑 → ( 𝐴 Yrm 0 ) < ( 𝐴 Yrm 𝑄 ) )
93 ltrmy ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 0 ∈ ℤ ∧ 𝑄 ∈ ℤ ) → ( 0 < 𝑄 ↔ ( 𝐴 Yrm 0 ) < ( 𝐴 Yrm 𝑄 ) ) )
94 1 47 24 93 syl3anc ⊢ ( 𝜑 → ( 0 < 𝑄 ↔ ( 𝐴 Yrm 0 ) < ( 𝐴 Yrm 𝑄 ) ) )
95 92 94 mpbird ⊢ ( 𝜑 → 0 < 𝑄 )
96 elnnz ⊢ ( 𝑄 ∈ ℕ ↔ ( 𝑄 ∈ ℤ ∧ 0 < 𝑄 ) )
97 24 95 96 sylanbrc ⊢ ( 𝜑 → 𝑄 ∈ ℕ )
98 3 nngt0d ⊢ ( 𝜑 → 0 < 𝐶 )
99 23 eqcomd ⊢ ( 𝜑 → ( 𝐴 Yrm 𝑃 ) = 𝐶 )
100 98 90 99 3brtr4d ⊢ ( 𝜑 → ( 𝐴 Yrm 0 ) < ( 𝐴 Yrm 𝑃 ) )
101 ltrmy ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 0 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 0 < 𝑃 ↔ ( 𝐴 Yrm 0 ) < ( 𝐴 Yrm 𝑃 ) ) )
102 1 47 21 101 syl3anc ⊢ ( 𝜑 → ( 0 < 𝑃 ↔ ( 𝐴 Yrm 0 ) < ( 𝐴 Yrm 𝑃 ) ) )
103 100 102 mpbird ⊢ ( 𝜑 → 0 < 𝑃 )
104 elnnz ⊢ ( 𝑃 ∈ ℕ ↔ ( 𝑃 ∈ ℤ ∧ 0 < 𝑃 ) )
105 21 103 104 sylanbrc ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
106 jm2.20nn ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑄 ∈ ℕ ∧ 𝑃 ∈ ℕ ) → ( ( ( 𝐴 Yrm 𝑃 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑄 ) ↔ ( 𝑃 · ( 𝐴 Yrm 𝑃 ) ) ∥ 𝑄 ) )
107 1 97 105 106 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐴 Yrm 𝑃 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑄 ) ↔ ( 𝑃 · ( 𝐴 Yrm 𝑃 ) ) ∥ 𝑄 ) )
108 76 107 mpbid ⊢ ( 𝜑 → ( 𝑃 · ( 𝐴 Yrm 𝑃 ) ) ∥ 𝑄 )
109 23 31 eqeltrrd ⊢ ( 𝜑 → ( 𝐴 Yrm 𝑃 ) ∈ ℤ )
110 muldvds2 ⊢ ( ( 𝑃 ∈ ℤ ∧ ( 𝐴 Yrm 𝑃 ) ∈ ℤ ∧ 𝑄 ∈ ℤ ) → ( ( 𝑃 · ( 𝐴 Yrm 𝑃 ) ) ∥ 𝑄 → ( 𝐴 Yrm 𝑃 ) ∥ 𝑄 ) )
111 21 109 24 110 syl3anc ⊢ ( 𝜑 → ( ( 𝑃 · ( 𝐴 Yrm 𝑃 ) ) ∥ 𝑄 → ( 𝐴 Yrm 𝑃 ) ∥ 𝑄 ) )
112 108 111 mpd ⊢ ( 𝜑 → ( 𝐴 Yrm 𝑃 ) ∥ 𝑄 )
113 23 112 eqbrtrd ⊢ ( 𝜑 → 𝐶 ∥ 𝑄 )
114 30 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
115 dvdscmul ⊢ ( ( 𝐶 ∈ ℤ ∧ 𝑄 ∈ ℤ ∧ 2 ∈ ℤ ) → ( 𝐶 ∥ 𝑄 → ( 2 · 𝐶 ) ∥ ( 2 · 𝑄 ) ) )
116 31 24 114 115 syl3anc ⊢ ( 𝜑 → ( 𝐶 ∥ 𝑄 → ( 2 · 𝐶 ) ∥ ( 2 · 𝑄 ) ) )
117 113 116 mpd ⊢ ( 𝜑 → ( 2 · 𝐶 ) ∥ ( 2 · 𝑄 ) )
118 6 nn0zd ⊢ ( 𝜑 → 𝐹 ∈ ℤ )
119 25 118 eqeltrrd ⊢ ( 𝜑 → ( 𝐴 Xrm 𝑄 ) ∈ ℤ )
120 frmy ⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
121 120 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ ℤ ) → ( 𝐴 Yrm 𝑅 ) ∈ ℤ )
122 1 27 121 syl2anc ⊢ ( 𝜑 → ( 𝐴 Yrm 𝑅 ) ∈ ℤ )
123 29 35 eqeltrrd ⊢ ( 𝜑 → ( 𝐺 Yrm 𝑅 ) ∈ ℤ )
124 eluzelz ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℤ )
125 1 124 syl ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
126 125 38 zsubcld ⊢ ( 𝜑 → ( 𝐴 − 𝐺 ) ∈ ℤ )
127 122 123 zsubcld ⊢ ( 𝜑 → ( ( 𝐴 Yrm 𝑅 ) − ( 𝐺 Yrm 𝑅 ) ) ∈ ℤ )
128 congsym ⊢ ( ( ( 𝐹 ∈ ℤ ∧ 𝐺 ∈ ℤ ) ∧ ( 𝐴 ∈ ℤ ∧ 𝐹 ∥ ( 𝐺 − 𝐴 ) ) ) → 𝐹 ∥ ( 𝐴 − 𝐺 ) )
129 118 38 125 16 128 syl22anc ⊢ ( 𝜑 → 𝐹 ∥ ( 𝐴 − 𝐺 ) )
130 25 129 eqbrtrrd ⊢ ( 𝜑 → ( 𝐴 Xrm 𝑄 ) ∥ ( 𝐴 − 𝐺 ) )
131 jm2.15nn0 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐺 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ ℕ0 ) → ( 𝐴 − 𝐺 ) ∥ ( ( 𝐴 Yrm 𝑅 ) − ( 𝐺 Yrm 𝑅 ) ) )
132 1 13 52 131 syl3anc ⊢ ( 𝜑 → ( 𝐴 − 𝐺 ) ∥ ( ( 𝐴 Yrm 𝑅 ) − ( 𝐺 Yrm 𝑅 ) ) )
133 119 126 127 130 132 dvdstrd ⊢ ( 𝜑 → ( 𝐴 Xrm 𝑄 ) ∥ ( ( 𝐴 Yrm 𝑅 ) − ( 𝐺 Yrm 𝑅 ) ) )
134 29 23 oveq12d ⊢ ( 𝜑 → ( 𝐻 − 𝐶 ) = ( ( 𝐺 Yrm 𝑅 ) − ( 𝐴 Yrm 𝑃 ) ) )
135 18 25 134 3brtr3d ⊢ ( 𝜑 → ( 𝐴 Xrm 𝑄 ) ∥ ( ( 𝐺 Yrm 𝑅 ) − ( 𝐴 Yrm 𝑃 ) ) )
136 congtr ⊢ ( ( ( ( 𝐴 Xrm 𝑄 ) ∈ ℤ ∧ ( 𝐴 Yrm 𝑅 ) ∈ ℤ ) ∧ ( ( 𝐺 Yrm 𝑅 ) ∈ ℤ ∧ ( 𝐴 Yrm 𝑃 ) ∈ ℤ ) ∧ ( ( 𝐴 Xrm 𝑄 ) ∥ ( ( 𝐴 Yrm 𝑅 ) − ( 𝐺 Yrm 𝑅 ) ) ∧ ( 𝐴 Xrm 𝑄 ) ∥ ( ( 𝐺 Yrm 𝑅 ) − ( 𝐴 Yrm 𝑃 ) ) ) ) → ( 𝐴 Xrm 𝑄 ) ∥ ( ( 𝐴 Yrm 𝑅 ) − ( 𝐴 Yrm 𝑃 ) ) )
137 119 122 123 109 133 135 136 syl222anc ⊢ ( 𝜑 → ( 𝐴 Xrm 𝑄 ) ∥ ( ( 𝐴 Yrm 𝑅 ) − ( 𝐴 Yrm 𝑃 ) ) )
138 137 orcd ⊢ ( 𝜑 → ( ( 𝐴 Xrm 𝑄 ) ∥ ( ( 𝐴 Yrm 𝑅 ) − ( 𝐴 Yrm 𝑃 ) ) ∨ ( 𝐴 Xrm 𝑄 ) ∥ ( ( 𝐴 Yrm 𝑅 ) − - ( 𝐴 Yrm 𝑃 ) ) ) )
139 jm2.26 ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑄 ∈ ℕ ) ∧ ( 𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ) → ( ( ( 𝐴 Xrm 𝑄 ) ∥ ( ( 𝐴 Yrm 𝑅 ) − ( 𝐴 Yrm 𝑃 ) ) ∨ ( 𝐴 Xrm 𝑄 ) ∥ ( ( 𝐴 Yrm 𝑅 ) − - ( 𝐴 Yrm 𝑃 ) ) ) ↔ ( ( 2 · 𝑄 ) ∥ ( 𝑅 − 𝑃 ) ∨ ( 2 · 𝑄 ) ∥ ( 𝑅 − - 𝑃 ) ) ) )
140 1 97 27 21 139 syl22anc ⊢ ( 𝜑 → ( ( ( 𝐴 Xrm 𝑄 ) ∥ ( ( 𝐴 Yrm 𝑅 ) − ( 𝐴 Yrm 𝑃 ) ) ∨ ( 𝐴 Xrm 𝑄 ) ∥ ( ( 𝐴 Yrm 𝑅 ) − - ( 𝐴 Yrm 𝑃 ) ) ) ↔ ( ( 2 · 𝑄 ) ∥ ( 𝑅 − 𝑃 ) ∨ ( 2 · 𝑄 ) ∥ ( 𝑅 − - 𝑃 ) ) ) )
141 138 140 mpbid ⊢ ( 𝜑 → ( ( 2 · 𝑄 ) ∥ ( 𝑅 − 𝑃 ) ∨ ( 2 · 𝑄 ) ∥ ( 𝑅 − - 𝑃 ) ) )
142 dvdsacongtr ⊢ ( ( ( ( 2 · 𝑄 ) ∈ ℤ ∧ 𝑅 ∈ ℤ ) ∧ ( 𝑃 ∈ ℤ ∧ ( 2 · 𝐶 ) ∈ ℤ ) ∧ ( ( 2 · 𝐶 ) ∥ ( 2 · 𝑄 ) ∧ ( ( 2 · 𝑄 ) ∥ ( 𝑅 − 𝑃 ) ∨ ( 2 · 𝑄 ) ∥ ( 𝑅 − - 𝑃 ) ) ) ) → ( ( 2 · 𝐶 ) ∥ ( 𝑅 − 𝑃 ) ∨ ( 2 · 𝐶 ) ∥ ( 𝑅 − - 𝑃 ) ) )
143 62 27 21 33 117 141 142 syl222anc ⊢ ( 𝜑 → ( ( 2 · 𝐶 ) ∥ ( 𝑅 − 𝑃 ) ∨ ( 2 · 𝐶 ) ∥ ( 𝑅 − - 𝑃 ) ) )
144 acongtr ⊢ ( ( ( ( 2 · 𝐶 ) ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ ( ( ( 2 · 𝐶 ) ∥ ( 𝐵 − 𝑅 ) ∨ ( 2 · 𝐶 ) ∥ ( 𝐵 − - 𝑅 ) ) ∧ ( ( 2 · 𝐶 ) ∥ ( 𝑅 − 𝑃 ) ∨ ( 2 · 𝐶 ) ∥ ( 𝑅 − - 𝑃 ) ) ) ) → ( ( 2 · 𝐶 ) ∥ ( 𝐵 − 𝑃 ) ∨ ( 2 · 𝐶 ) ∥ ( 𝐵 − - 𝑃 ) ) )
145 33 34 27 21 60 143 144 syl222anc ⊢ ( 𝜑 → ( ( 2 · 𝐶 ) ∥ ( 𝐵 − 𝑃 ) ∨ ( 2 · 𝐶 ) ∥ ( 𝐵 − - 𝑃 ) ) )
146 2 nnnn0d ⊢ ( 𝜑 → 𝐵 ∈ ℕ0 )
147 3 nnnn0d ⊢ ( 𝜑 → 𝐶 ∈ ℕ0 )
148 elfz2nn0 ⊢ ( 𝐵 ∈ ( 0 ... 𝐶 ) ↔ ( 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ∧ 𝐵 ≤ 𝐶 ) )
149 146 147 20 148 syl3anbrc ⊢ ( 𝜑 → 𝐵 ∈ ( 0 ... 𝐶 ) )
150 105 nnnn0d ⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
151 rmygeid ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℕ0 ) → 𝑃 ≤ ( 𝐴 Yrm 𝑃 ) )
152 1 150 151 syl2anc ⊢ ( 𝜑 → 𝑃 ≤ ( 𝐴 Yrm 𝑃 ) )
153 152 23 breqtrrd ⊢ ( 𝜑 → 𝑃 ≤ 𝐶 )
154 elfz2nn0 ⊢ ( 𝑃 ∈ ( 0 ... 𝐶 ) ↔ ( 𝑃 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ∧ 𝑃 ≤ 𝐶 ) )
155 150 147 153 154 syl3anbrc ⊢ ( 𝜑 → 𝑃 ∈ ( 0 ... 𝐶 ) )
156 acongeq ⊢ ( ( 𝐶 ∈ ℕ ∧ 𝐵 ∈ ( 0 ... 𝐶 ) ∧ 𝑃 ∈ ( 0 ... 𝐶 ) ) → ( 𝐵 = 𝑃 ↔ ( ( 2 · 𝐶 ) ∥ ( 𝐵 − 𝑃 ) ∨ ( 2 · 𝐶 ) ∥ ( 𝐵 − - 𝑃 ) ) ) )
157 3 149 155 156 syl3anc ⊢ ( 𝜑 → ( 𝐵 = 𝑃 ↔ ( ( 2 · 𝐶 ) ∥ ( 𝐵 − 𝑃 ) ∨ ( 2 · 𝐶 ) ∥ ( 𝐵 − - 𝑃 ) ) ) )
158 145 157 mpbird ⊢ ( 𝜑 → 𝐵 = 𝑃 )
159 158 oveq2d ⊢ ( 𝜑 → ( 𝐴 Yrm 𝐵 ) = ( 𝐴 Yrm 𝑃 ) )
160 23 159 eqtr4d ⊢ ( 𝜑 → 𝐶 = ( 𝐴 Yrm 𝐵 ) )