Metamath Proof Explorer

Theorem jm2.27c

Description: Lemma for jm2.27 . Forward direction with substitutions. (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Hypotheses jm2.27a1 ⊢ ( 𝜑 → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
jm2.27a2 ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
jm2.27a3 ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
jm2.27c4 ⊢ ( 𝜑 → 𝐶 = ( 𝐴 Yrm 𝐵 ) )
jm2.27c5 ⊢ 𝐷 = ( 𝐴 Xrm 𝐵 )
jm2.27c6 ⊢ 𝑄 = ( 𝐵 · ( 𝐴 Yrm 𝐵 ) )
jm2.27c7 ⊢ 𝐸 = ( 𝐴 Yrm ( 2 · 𝑄 ) )
jm2.27c8 ⊢ 𝐹 = ( 𝐴 Xrm ( 2 · 𝑄 ) )
jm2.27c9 ⊢ 𝐺 = ( 𝐴 + ( ( 𝐹 ↑ 2 ) · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) )
jm2.27c10 ⊢ 𝐻 = ( 𝐺 Yrm 𝐵 )
jm2.27c11 ⊢ 𝐼 = ( 𝐺 Xrm 𝐵 )
jm2.27c12 ⊢ 𝐽 = ( ( 𝐸 / ( 2 · ( 𝐶 ↑ 2 ) ) ) − 1 )
Assertion jm2.27c ( 𝜑 → ( ( ( 𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ∧ 𝐹 ∈ ℕ0 ) ∧ ( 𝐺 ∈ ℕ0 ∧ 𝐻 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ ( 𝐽 ∈ ℕ0 ∧ ( ( ( ( ( 𝐷 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐶 ↑ 2 ) ) ) = 1 ∧ ( ( 𝐹 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 ↑ 2 ) ) ) = 1 ∧ 𝐺 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( ( 𝐼 ↑ 2 ) − ( ( ( 𝐺 ↑ 2 ) − 1 ) · ( 𝐻 ↑ 2 ) ) ) = 1 ∧ 𝐸 = ( ( 𝐽 + 1 ) · ( 2 · ( 𝐶 ↑ 2 ) ) ) ∧ 𝐹 ∥ ( 𝐺 − 𝐴 ) ) ) ∧ ( ( ( 2 · 𝐶 ) ∥ ( 𝐺 − 1 ) ∧ 𝐹 ∥ ( 𝐻 − 𝐶 ) ) ∧ ( ( 2 · 𝐶 ) ∥ ( 𝐻 − 𝐵 ) ∧ 𝐵 ≤ 𝐶 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 jm2.27a1 ⊢ ( 𝜑 → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
2 jm2.27a2 ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3 jm2.27a3 ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
4 jm2.27c4 ⊢ ( 𝜑 → 𝐶 = ( 𝐴 Yrm 𝐵 ) )
5 jm2.27c5 ⊢ 𝐷 = ( 𝐴 Xrm 𝐵 )
6 jm2.27c6 ⊢ 𝑄 = ( 𝐵 · ( 𝐴 Yrm 𝐵 ) )
7 jm2.27c7 ⊢ 𝐸 = ( 𝐴 Yrm ( 2 · 𝑄 ) )
8 jm2.27c8 ⊢ 𝐹 = ( 𝐴 Xrm ( 2 · 𝑄 ) )
9 jm2.27c9 ⊢ 𝐺 = ( 𝐴 + ( ( 𝐹 ↑ 2 ) · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) )
10 jm2.27c10 ⊢ 𝐻 = ( 𝐺 Yrm 𝐵 )
11 jm2.27c11 ⊢ 𝐼 = ( 𝐺 Xrm 𝐵 )
12 jm2.27c12 ⊢ 𝐽 = ( ( 𝐸 / ( 2 · ( 𝐶 ↑ 2 ) ) ) − 1 )
13 2 nnzd ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
14 frmx ⊢ Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0
15 14 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℤ ) → ( 𝐴 Xrm 𝐵 ) ∈ ℕ0 )
16 1 13 15 syl2anc ⊢ ( 𝜑 → ( 𝐴 Xrm 𝐵 ) ∈ ℕ0 )
17 5 16 eqeltrid ⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
18 2z ⊢ 2 ∈ ℤ
19 3 nnzd ⊢ ( 𝜑 → 𝐶 ∈ ℤ )
20 4 19 eqeltrrd ⊢ ( 𝜑 → ( 𝐴 Yrm 𝐵 ) ∈ ℤ )
21 13 20 zmulcld ⊢ ( 𝜑 → ( 𝐵 · ( 𝐴 Yrm 𝐵 ) ) ∈ ℤ )
22 6 21 eqeltrid ⊢ ( 𝜑 → 𝑄 ∈ ℤ )
23 zmulcl ⊢ ( ( 2 ∈ ℤ ∧ 𝑄 ∈ ℤ ) → ( 2 · 𝑄 ) ∈ ℤ )
24 18 22 23 sylancr ⊢ ( 𝜑 → ( 2 · 𝑄 ) ∈ ℤ )
25 frmy ⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
26 25 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 2 · 𝑄 ) ∈ ℤ ) → ( 𝐴 Yrm ( 2 · 𝑄 ) ) ∈ ℤ )
27 1 24 26 syl2anc ⊢ ( 𝜑 → ( 𝐴 Yrm ( 2 · 𝑄 ) ) ∈ ℤ )
28 rmy0 ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm 0 ) = 0 )
29 1 28 syl ⊢ ( 𝜑 → ( 𝐴 Yrm 0 ) = 0 )
30 2nn ⊢ 2 ∈ ℕ
31 4 3 eqeltrrd ⊢ ( 𝜑 → ( 𝐴 Yrm 𝐵 ) ∈ ℕ )
32 2 31 nnmulcld ⊢ ( 𝜑 → ( 𝐵 · ( 𝐴 Yrm 𝐵 ) ) ∈ ℕ )
33 6 32 eqeltrid ⊢ ( 𝜑 → 𝑄 ∈ ℕ )
34 nnmulcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑄 ∈ ℕ ) → ( 2 · 𝑄 ) ∈ ℕ )
35 30 33 34 sylancr ⊢ ( 𝜑 → ( 2 · 𝑄 ) ∈ ℕ )
36 35 nnnn0d ⊢ ( 𝜑 → ( 2 · 𝑄 ) ∈ ℕ0 )
37 36 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( 2 · 𝑄 ) )
38 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
39 lermy ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 0 ∈ ℤ ∧ ( 2 · 𝑄 ) ∈ ℤ ) → ( 0 ≤ ( 2 · 𝑄 ) ↔ ( 𝐴 Yrm 0 ) ≤ ( 𝐴 Yrm ( 2 · 𝑄 ) ) ) )
40 1 38 24 39 syl3anc ⊢ ( 𝜑 → ( 0 ≤ ( 2 · 𝑄 ) ↔ ( 𝐴 Yrm 0 ) ≤ ( 𝐴 Yrm ( 2 · 𝑄 ) ) ) )
41 37 40 mpbid ⊢ ( 𝜑 → ( 𝐴 Yrm 0 ) ≤ ( 𝐴 Yrm ( 2 · 𝑄 ) ) )
42 29 41 eqbrtrrd ⊢ ( 𝜑 → 0 ≤ ( 𝐴 Yrm ( 2 · 𝑄 ) ) )
43 elnn0z ⊢ ( ( 𝐴 Yrm ( 2 · 𝑄 ) ) ∈ ℕ0 ↔ ( ( 𝐴 Yrm ( 2 · 𝑄 ) ) ∈ ℤ ∧ 0 ≤ ( 𝐴 Yrm ( 2 · 𝑄 ) ) ) )
44 27 42 43 sylanbrc ⊢ ( 𝜑 → ( 𝐴 Yrm ( 2 · 𝑄 ) ) ∈ ℕ0 )
45 7 44 eqeltrid ⊢ ( 𝜑 → 𝐸 ∈ ℕ0 )
46 14 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 2 · 𝑄 ) ∈ ℤ ) → ( 𝐴 Xrm ( 2 · 𝑄 ) ) ∈ ℕ0 )
47 1 24 46 syl2anc ⊢ ( 𝜑 → ( 𝐴 Xrm ( 2 · 𝑄 ) ) ∈ ℕ0 )
48 8 47 eqeltrid ⊢ ( 𝜑 → 𝐹 ∈ ℕ0 )
49 17 45 48 3jca ⊢ ( 𝜑 → ( 𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ∧ 𝐹 ∈ ℕ0 ) )
50 2nn0 ⊢ 2 ∈ ℕ0
51 48 nn0cnd ⊢ ( 𝜑 → 𝐹 ∈ ℂ )
52 51 sqvald ⊢ ( 𝜑 → ( 𝐹 ↑ 2 ) = ( 𝐹 · 𝐹 ) )
53 48 48 nn0mulcld ⊢ ( 𝜑 → ( 𝐹 · 𝐹 ) ∈ ℕ0 )
54 52 53 eqeltrd ⊢ ( 𝜑 → ( 𝐹 ↑ 2 ) ∈ ℕ0 )
55 eluz2nn ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℕ )
56 1 55 syl ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
57 56 nnnn0d ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
58 57 nn0red ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
59 48 nn0red ⊢ ( 𝜑 → 𝐹 ∈ ℝ )
60 59 59 remulcld ⊢ ( 𝜑 → ( 𝐹 · 𝐹 ) ∈ ℝ )
61 rmx1 ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Xrm 1 ) = 𝐴 )
62 1 61 syl ⊢ ( 𝜑 → ( 𝐴 Xrm 1 ) = 𝐴 )
63 35 nnge1d ⊢ ( 𝜑 → 1 ≤ ( 2 · 𝑄 ) )
64 1nn0 ⊢ 1 ∈ ℕ0
65 64 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
66 lermxnn0 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 1 ∈ ℕ0 ∧ ( 2 · 𝑄 ) ∈ ℕ0 ) → ( 1 ≤ ( 2 · 𝑄 ) ↔ ( 𝐴 Xrm 1 ) ≤ ( 𝐴 Xrm ( 2 · 𝑄 ) ) ) )
67 1 65 36 66 syl3anc ⊢ ( 𝜑 → ( 1 ≤ ( 2 · 𝑄 ) ↔ ( 𝐴 Xrm 1 ) ≤ ( 𝐴 Xrm ( 2 · 𝑄 ) ) ) )
68 63 67 mpbid ⊢ ( 𝜑 → ( 𝐴 Xrm 1 ) ≤ ( 𝐴 Xrm ( 2 · 𝑄 ) ) )
69 62 68 eqbrtrrd ⊢ ( 𝜑 → 𝐴 ≤ ( 𝐴 Xrm ( 2 · 𝑄 ) ) )
70 69 8 breqtrrdi ⊢ ( 𝜑 → 𝐴 ≤ 𝐹 )
71 48 nn0ge0d ⊢ ( 𝜑 → 0 ≤ 𝐹 )
72 rmxnn ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 2 · 𝑄 ) ∈ ℤ ) → ( 𝐴 Xrm ( 2 · 𝑄 ) ) ∈ ℕ )
73 1 24 72 syl2anc ⊢ ( 𝜑 → ( 𝐴 Xrm ( 2 · 𝑄 ) ) ∈ ℕ )
74 8 73 eqeltrid ⊢ ( 𝜑 → 𝐹 ∈ ℕ )
75 74 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝐹 )
76 59 59 71 75 lemulge12d ⊢ ( 𝜑 → 𝐹 ≤ ( 𝐹 · 𝐹 ) )
77 58 59 60 70 76 letrd ⊢ ( 𝜑 → 𝐴 ≤ ( 𝐹 · 𝐹 ) )
78 77 52 breqtrrd ⊢ ( 𝜑 → 𝐴 ≤ ( 𝐹 ↑ 2 ) )
79 nn0sub ⊢ ( ( 𝐴 ∈ ℕ0 ∧ ( 𝐹 ↑ 2 ) ∈ ℕ0 ) → ( 𝐴 ≤ ( 𝐹 ↑ 2 ) ↔ ( ( 𝐹 ↑ 2 ) − 𝐴 ) ∈ ℕ0 ) )
80 57 54 79 syl2anc ⊢ ( 𝜑 → ( 𝐴 ≤ ( 𝐹 ↑ 2 ) ↔ ( ( 𝐹 ↑ 2 ) − 𝐴 ) ∈ ℕ0 ) )
81 78 80 mpbid ⊢ ( 𝜑 → ( ( 𝐹 ↑ 2 ) − 𝐴 ) ∈ ℕ0 )
82 54 81 nn0mulcld ⊢ ( 𝜑 → ( ( 𝐹 ↑ 2 ) · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) ∈ ℕ0 )
83 uzaddcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( 𝐹 ↑ 2 ) · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) ∈ ℕ0 ) → ( 𝐴 + ( ( 𝐹 ↑ 2 ) · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) ) ∈ ( ℤ≥ ‘ 2 ) )
84 1 82 83 syl2anc ⊢ ( 𝜑 → ( 𝐴 + ( ( 𝐹 ↑ 2 ) · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) ) ∈ ( ℤ≥ ‘ 2 ) )
85 9 84 eqeltrid ⊢ ( 𝜑 → 𝐺 ∈ ( ℤ≥ ‘ 2 ) )
86 eluznn0 ⊢ ( ( 2 ∈ ℕ0 ∧ 𝐺 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐺 ∈ ℕ0 )
87 50 85 86 sylancr ⊢ ( 𝜑 → 𝐺 ∈ ℕ0 )
88 25 fovcl ⊢ ( ( 𝐺 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℤ ) → ( 𝐺 Yrm 𝐵 ) ∈ ℤ )
89 85 13 88 syl2anc ⊢ ( 𝜑 → ( 𝐺 Yrm 𝐵 ) ∈ ℤ )
90 rmy0 ⊢ ( 𝐺 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐺 Yrm 0 ) = 0 )
91 85 90 syl ⊢ ( 𝜑 → ( 𝐺 Yrm 0 ) = 0 )
92 2 nnnn0d ⊢ ( 𝜑 → 𝐵 ∈ ℕ0 )
93 92 nn0ge0d ⊢ ( 𝜑 → 0 ≤ 𝐵 )
94 lermy ⊢ ( ( 𝐺 ∈ ( ℤ≥ ‘ 2 ) ∧ 0 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 0 ≤ 𝐵 ↔ ( 𝐺 Yrm 0 ) ≤ ( 𝐺 Yrm 𝐵 ) ) )
95 85 38 13 94 syl3anc ⊢ ( 𝜑 → ( 0 ≤ 𝐵 ↔ ( 𝐺 Yrm 0 ) ≤ ( 𝐺 Yrm 𝐵 ) ) )
96 93 95 mpbid ⊢ ( 𝜑 → ( 𝐺 Yrm 0 ) ≤ ( 𝐺 Yrm 𝐵 ) )
97 91 96 eqbrtrrd ⊢ ( 𝜑 → 0 ≤ ( 𝐺 Yrm 𝐵 ) )
98 elnn0z ⊢ ( ( 𝐺 Yrm 𝐵 ) ∈ ℕ0 ↔ ( ( 𝐺 Yrm 𝐵 ) ∈ ℤ ∧ 0 ≤ ( 𝐺 Yrm 𝐵 ) ) )
99 89 97 98 sylanbrc ⊢ ( 𝜑 → ( 𝐺 Yrm 𝐵 ) ∈ ℕ0 )
100 10 99 eqeltrid ⊢ ( 𝜑 → 𝐻 ∈ ℕ0 )
101 14 fovcl ⊢ ( ( 𝐺 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℤ ) → ( 𝐺 Xrm 𝐵 ) ∈ ℕ0 )
102 85 13 101 syl2anc ⊢ ( 𝜑 → ( 𝐺 Xrm 𝐵 ) ∈ ℕ0 )
103 11 102 eqeltrid ⊢ ( 𝜑 → 𝐼 ∈ ℕ0 )
104 87 100 103 3jca ⊢ ( 𝜑 → ( 𝐺 ∈ ℕ0 ∧ 𝐻 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) )
105 zsqcl ⊢ ( ( 𝐴 Yrm 𝐵 ) ∈ ℤ → ( ( 𝐴 Yrm 𝐵 ) ↑ 2 ) ∈ ℤ )
106 20 105 syl ⊢ ( 𝜑 → ( ( 𝐴 Yrm 𝐵 ) ↑ 2 ) ∈ ℤ )
107 zmulcl ⊢ ( ( 2 ∈ ℤ ∧ ( ( 𝐴 Yrm 𝐵 ) ↑ 2 ) ∈ ℤ ) → ( 2 · ( ( 𝐴 Yrm 𝐵 ) ↑ 2 ) ) ∈ ℤ )
108 18 106 107 sylancr ⊢ ( 𝜑 → ( 2 · ( ( 𝐴 Yrm 𝐵 ) ↑ 2 ) ) ∈ ℤ )
109 25 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑄 ∈ ℤ ) → ( 𝐴 Yrm 𝑄 ) ∈ ℤ )
110 1 22 109 syl2anc ⊢ ( 𝜑 → ( 𝐴 Yrm 𝑄 ) ∈ ℤ )
111 zmulcl ⊢ ( ( 2 ∈ ℤ ∧ ( 𝐴 Yrm 𝑄 ) ∈ ℤ ) → ( 2 · ( 𝐴 Yrm 𝑄 ) ) ∈ ℤ )
112 18 110 111 sylancr ⊢ ( 𝜑 → ( 2 · ( 𝐴 Yrm 𝑄 ) ) ∈ ℤ )
113 iddvds ⊢ ( ( 𝐵 · ( 𝐴 Yrm 𝐵 ) ) ∈ ℤ → ( 𝐵 · ( 𝐴 Yrm 𝐵 ) ) ∥ ( 𝐵 · ( 𝐴 Yrm 𝐵 ) ) )
114 21 113 syl ⊢ ( 𝜑 → ( 𝐵 · ( 𝐴 Yrm 𝐵 ) ) ∥ ( 𝐵 · ( 𝐴 Yrm 𝐵 ) ) )
115 114 6 breqtrrdi ⊢ ( 𝜑 → ( 𝐵 · ( 𝐴 Yrm 𝐵 ) ) ∥ 𝑄 )
116 jm2.20nn ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑄 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( ( 𝐴 Yrm 𝐵 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑄 ) ↔ ( 𝐵 · ( 𝐴 Yrm 𝐵 ) ) ∥ 𝑄 ) )
117 1 33 2 116 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐴 Yrm 𝐵 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑄 ) ↔ ( 𝐵 · ( 𝐴 Yrm 𝐵 ) ) ∥ 𝑄 ) )
118 115 117 mpbird ⊢ ( 𝜑 → ( ( 𝐴 Yrm 𝐵 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑄 ) )
119 18 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
120 dvdscmul ⊢ ( ( ( ( 𝐴 Yrm 𝐵 ) ↑ 2 ) ∈ ℤ ∧ ( 𝐴 Yrm 𝑄 ) ∈ ℤ ∧ 2 ∈ ℤ ) → ( ( ( 𝐴 Yrm 𝐵 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑄 ) → ( 2 · ( ( 𝐴 Yrm 𝐵 ) ↑ 2 ) ) ∥ ( 2 · ( 𝐴 Yrm 𝑄 ) ) ) )
121 106 110 119 120 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐴 Yrm 𝐵 ) ↑ 2 ) ∥ ( 𝐴 Yrm 𝑄 ) → ( 2 · ( ( 𝐴 Yrm 𝐵 ) ↑ 2 ) ) ∥ ( 2 · ( 𝐴 Yrm 𝑄 ) ) ) )
122 118 121 mpd ⊢ ( 𝜑 → ( 2 · ( ( 𝐴 Yrm 𝐵 ) ↑ 2 ) ) ∥ ( 2 · ( 𝐴 Yrm 𝑄 ) ) )
123 14 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑄 ∈ ℤ ) → ( 𝐴 Xrm 𝑄 ) ∈ ℕ0 )
124 1 22 123 syl2anc ⊢ ( 𝜑 → ( 𝐴 Xrm 𝑄 ) ∈ ℕ0 )
125 124 nn0zd ⊢ ( 𝜑 → ( 𝐴 Xrm 𝑄 ) ∈ ℤ )
126 dvdsmul1 ⊢ ( ( ( 2 · ( 𝐴 Yrm 𝑄 ) ) ∈ ℤ ∧ ( 𝐴 Xrm 𝑄 ) ∈ ℤ ) → ( 2 · ( 𝐴 Yrm 𝑄 ) ) ∥ ( ( 2 · ( 𝐴 Yrm 𝑄 ) ) · ( 𝐴 Xrm 𝑄 ) ) )
127 112 125 126 syl2anc ⊢ ( 𝜑 → ( 2 · ( 𝐴 Yrm 𝑄 ) ) ∥ ( ( 2 · ( 𝐴 Yrm 𝑄 ) ) · ( 𝐴 Xrm 𝑄 ) ) )
128 rmydbl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑄 ∈ ℤ ) → ( 𝐴 Yrm ( 2 · 𝑄 ) ) = ( ( 2 · ( 𝐴 Xrm 𝑄 ) ) · ( 𝐴 Yrm 𝑄 ) ) )
129 1 22 128 syl2anc ⊢ ( 𝜑 → ( 𝐴 Yrm ( 2 · 𝑄 ) ) = ( ( 2 · ( 𝐴 Xrm 𝑄 ) ) · ( 𝐴 Yrm 𝑄 ) ) )
130 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
131 124 nn0cnd ⊢ ( 𝜑 → ( 𝐴 Xrm 𝑄 ) ∈ ℂ )
132 110 zcnd ⊢ ( 𝜑 → ( 𝐴 Yrm 𝑄 ) ∈ ℂ )
133 130 131 132 mul32d ⊢ ( 𝜑 → ( ( 2 · ( 𝐴 Xrm 𝑄 ) ) · ( 𝐴 Yrm 𝑄 ) ) = ( ( 2 · ( 𝐴 Yrm 𝑄 ) ) · ( 𝐴 Xrm 𝑄 ) ) )
134 129 133 eqtrd ⊢ ( 𝜑 → ( 𝐴 Yrm ( 2 · 𝑄 ) ) = ( ( 2 · ( 𝐴 Yrm 𝑄 ) ) · ( 𝐴 Xrm 𝑄 ) ) )
135 127 134 breqtrrd ⊢ ( 𝜑 → ( 2 · ( 𝐴 Yrm 𝑄 ) ) ∥ ( 𝐴 Yrm ( 2 · 𝑄 ) ) )
136 108 112 27 122 135 dvdstrd ⊢ ( 𝜑 → ( 2 · ( ( 𝐴 Yrm 𝐵 ) ↑ 2 ) ) ∥ ( 𝐴 Yrm ( 2 · 𝑄 ) ) )
137 4 oveq1d ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) = ( ( 𝐴 Yrm 𝐵 ) ↑ 2 ) )
138 137 oveq2d ⊢ ( 𝜑 → ( 2 · ( 𝐶 ↑ 2 ) ) = ( 2 · ( ( 𝐴 Yrm 𝐵 ) ↑ 2 ) ) )
139 7 a1i ⊢ ( 𝜑 → 𝐸 = ( 𝐴 Yrm ( 2 · 𝑄 ) ) )
140 136 138 139 3brtr4d ⊢ ( 𝜑 → ( 2 · ( 𝐶 ↑ 2 ) ) ∥ 𝐸 )
141 7 27 eqeltrid ⊢ ( 𝜑 → 𝐸 ∈ ℤ )
142 35 nngt0d ⊢ ( 𝜑 → 0 < ( 2 · 𝑄 ) )
143 ltrmy ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 0 ∈ ℤ ∧ ( 2 · 𝑄 ) ∈ ℤ ) → ( 0 < ( 2 · 𝑄 ) ↔ ( 𝐴 Yrm 0 ) < ( 𝐴 Yrm ( 2 · 𝑄 ) ) ) )
144 1 38 24 143 syl3anc ⊢ ( 𝜑 → ( 0 < ( 2 · 𝑄 ) ↔ ( 𝐴 Yrm 0 ) < ( 𝐴 Yrm ( 2 · 𝑄 ) ) ) )
145 142 144 mpbid ⊢ ( 𝜑 → ( 𝐴 Yrm 0 ) < ( 𝐴 Yrm ( 2 · 𝑄 ) ) )
146 29 eqcomd ⊢ ( 𝜑 → 0 = ( 𝐴 Yrm 0 ) )
147 145 146 139 3brtr4d ⊢ ( 𝜑 → 0 < 𝐸 )
148 elnnz ⊢ ( 𝐸 ∈ ℕ ↔ ( 𝐸 ∈ ℤ ∧ 0 < 𝐸 ) )
149 141 147 148 sylanbrc ⊢ ( 𝜑 → 𝐸 ∈ ℕ )
150 3 nnsqcld ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℕ )
151 nnmulcl ⊢ ( ( 2 ∈ ℕ ∧ ( 𝐶 ↑ 2 ) ∈ ℕ ) → ( 2 · ( 𝐶 ↑ 2 ) ) ∈ ℕ )
152 30 150 151 sylancr ⊢ ( 𝜑 → ( 2 · ( 𝐶 ↑ 2 ) ) ∈ ℕ )
153 nndivdvds ⊢ ( ( 𝐸 ∈ ℕ ∧ ( 2 · ( 𝐶 ↑ 2 ) ) ∈ ℕ ) → ( ( 2 · ( 𝐶 ↑ 2 ) ) ∥ 𝐸 ↔ ( 𝐸 / ( 2 · ( 𝐶 ↑ 2 ) ) ) ∈ ℕ ) )
154 149 152 153 syl2anc ⊢ ( 𝜑 → ( ( 2 · ( 𝐶 ↑ 2 ) ) ∥ 𝐸 ↔ ( 𝐸 / ( 2 · ( 𝐶 ↑ 2 ) ) ) ∈ ℕ ) )
155 140 154 mpbid ⊢ ( 𝜑 → ( 𝐸 / ( 2 · ( 𝐶 ↑ 2 ) ) ) ∈ ℕ )
156 nnm1nn0 ⊢ ( ( 𝐸 / ( 2 · ( 𝐶 ↑ 2 ) ) ) ∈ ℕ → ( ( 𝐸 / ( 2 · ( 𝐶 ↑ 2 ) ) ) − 1 ) ∈ ℕ0 )
157 155 156 syl ⊢ ( 𝜑 → ( ( 𝐸 / ( 2 · ( 𝐶 ↑ 2 ) ) ) − 1 ) ∈ ℕ0 )
158 12 157 eqeltrid ⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
159 5 oveq1i ⊢ ( 𝐷 ↑ 2 ) = ( ( 𝐴 Xrm 𝐵 ) ↑ 2 )
160 159 a1i ⊢ ( 𝜑 → ( 𝐷 ↑ 2 ) = ( ( 𝐴 Xrm 𝐵 ) ↑ 2 ) )
161 137 oveq2d ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐶 ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝐵 ) ↑ 2 ) ) )
162 160 161 oveq12d ⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐶 ↑ 2 ) ) ) = ( ( ( 𝐴 Xrm 𝐵 ) ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝐵 ) ↑ 2 ) ) ) )
163 rmxynorm ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℤ ) → ( ( ( 𝐴 Xrm 𝐵 ) ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝐵 ) ↑ 2 ) ) ) = 1 )
164 1 13 163 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐴 Xrm 𝐵 ) ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm 𝐵 ) ↑ 2 ) ) ) = 1 )
165 162 164 eqtrd ⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐶 ↑ 2 ) ) ) = 1 )
166 8 oveq1i ⊢ ( 𝐹 ↑ 2 ) = ( ( 𝐴 Xrm ( 2 · 𝑄 ) ) ↑ 2 )
167 7 oveq1i ⊢ ( 𝐸 ↑ 2 ) = ( ( 𝐴 Yrm ( 2 · 𝑄 ) ) ↑ 2 )
168 167 oveq2i ⊢ ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm ( 2 · 𝑄 ) ) ↑ 2 ) )
169 166 168 oveq12i ⊢ ( ( 𝐹 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 ↑ 2 ) ) ) = ( ( ( 𝐴 Xrm ( 2 · 𝑄 ) ) ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm ( 2 · 𝑄 ) ) ↑ 2 ) ) )
170 rmxynorm ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 2 · 𝑄 ) ∈ ℤ ) → ( ( ( 𝐴 Xrm ( 2 · 𝑄 ) ) ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm ( 2 · 𝑄 ) ) ↑ 2 ) ) ) = 1 )
171 1 24 170 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐴 Xrm ( 2 · 𝑄 ) ) ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( ( 𝐴 Yrm ( 2 · 𝑄 ) ) ↑ 2 ) ) ) = 1 )
172 169 171 syl5eq ⊢ ( 𝜑 → ( ( 𝐹 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 ↑ 2 ) ) ) = 1 )
173 165 172 85 3jca ⊢ ( 𝜑 → ( ( ( 𝐷 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐶 ↑ 2 ) ) ) = 1 ∧ ( ( 𝐹 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 ↑ 2 ) ) ) = 1 ∧ 𝐺 ∈ ( ℤ≥ ‘ 2 ) ) )
174 11 oveq1i ⊢ ( 𝐼 ↑ 2 ) = ( ( 𝐺 Xrm 𝐵 ) ↑ 2 )
175 10 oveq1i ⊢ ( 𝐻 ↑ 2 ) = ( ( 𝐺 Yrm 𝐵 ) ↑ 2 )
176 175 oveq2i ⊢ ( ( ( 𝐺 ↑ 2 ) − 1 ) · ( 𝐻 ↑ 2 ) ) = ( ( ( 𝐺 ↑ 2 ) − 1 ) · ( ( 𝐺 Yrm 𝐵 ) ↑ 2 ) )
177 174 176 oveq12i ⊢ ( ( 𝐼 ↑ 2 ) − ( ( ( 𝐺 ↑ 2 ) − 1 ) · ( 𝐻 ↑ 2 ) ) ) = ( ( ( 𝐺 Xrm 𝐵 ) ↑ 2 ) − ( ( ( 𝐺 ↑ 2 ) − 1 ) · ( ( 𝐺 Yrm 𝐵 ) ↑ 2 ) ) )
178 rmxynorm ⊢ ( ( 𝐺 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℤ ) → ( ( ( 𝐺 Xrm 𝐵 ) ↑ 2 ) − ( ( ( 𝐺 ↑ 2 ) − 1 ) · ( ( 𝐺 Yrm 𝐵 ) ↑ 2 ) ) ) = 1 )
179 85 13 178 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐺 Xrm 𝐵 ) ↑ 2 ) − ( ( ( 𝐺 ↑ 2 ) − 1 ) · ( ( 𝐺 Yrm 𝐵 ) ↑ 2 ) ) ) = 1 )
180 177 179 syl5eq ⊢ ( 𝜑 → ( ( 𝐼 ↑ 2 ) − ( ( ( 𝐺 ↑ 2 ) − 1 ) · ( 𝐻 ↑ 2 ) ) ) = 1 )
181 12 a1i ⊢ ( 𝜑 → 𝐽 = ( ( 𝐸 / ( 2 · ( 𝐶 ↑ 2 ) ) ) − 1 ) )
182 181 oveq1d ⊢ ( 𝜑 → ( 𝐽 + 1 ) = ( ( ( 𝐸 / ( 2 · ( 𝐶 ↑ 2 ) ) ) − 1 ) + 1 ) )
183 141 zcnd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
184 152 nncnd ⊢ ( 𝜑 → ( 2 · ( 𝐶 ↑ 2 ) ) ∈ ℂ )
185 152 nnne0d ⊢ ( 𝜑 → ( 2 · ( 𝐶 ↑ 2 ) ) ≠ 0 )
186 183 184 185 divcld ⊢ ( 𝜑 → ( 𝐸 / ( 2 · ( 𝐶 ↑ 2 ) ) ) ∈ ℂ )
187 ax-1cn ⊢ 1 ∈ ℂ
188 npcan ⊢ ( ( ( 𝐸 / ( 2 · ( 𝐶 ↑ 2 ) ) ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝐸 / ( 2 · ( 𝐶 ↑ 2 ) ) ) − 1 ) + 1 ) = ( 𝐸 / ( 2 · ( 𝐶 ↑ 2 ) ) ) )
189 186 187 188 sylancl ⊢ ( 𝜑 → ( ( ( 𝐸 / ( 2 · ( 𝐶 ↑ 2 ) ) ) − 1 ) + 1 ) = ( 𝐸 / ( 2 · ( 𝐶 ↑ 2 ) ) ) )
190 182 189 eqtrd ⊢ ( 𝜑 → ( 𝐽 + 1 ) = ( 𝐸 / ( 2 · ( 𝐶 ↑ 2 ) ) ) )
191 190 oveq1d ⊢ ( 𝜑 → ( ( 𝐽 + 1 ) · ( 2 · ( 𝐶 ↑ 2 ) ) ) = ( ( 𝐸 / ( 2 · ( 𝐶 ↑ 2 ) ) ) · ( 2 · ( 𝐶 ↑ 2 ) ) ) )
192 183 184 185 divcan1d ⊢ ( 𝜑 → ( ( 𝐸 / ( 2 · ( 𝐶 ↑ 2 ) ) ) · ( 2 · ( 𝐶 ↑ 2 ) ) ) = 𝐸 )
193 191 192 eqtr2d ⊢ ( 𝜑 → 𝐸 = ( ( 𝐽 + 1 ) · ( 2 · ( 𝐶 ↑ 2 ) ) ) )
194 48 nn0zd ⊢ ( 𝜑 → 𝐹 ∈ ℤ )
195 81 nn0zd ⊢ ( 𝜑 → ( ( 𝐹 ↑ 2 ) − 𝐴 ) ∈ ℤ )
196 194 195 zmulcld ⊢ ( 𝜑 → ( 𝐹 · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) ∈ ℤ )
197 dvdsmul1 ⊢ ( ( 𝐹 ∈ ℤ ∧ ( 𝐹 · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) ∈ ℤ ) → 𝐹 ∥ ( 𝐹 · ( 𝐹 · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) ) )
198 194 196 197 syl2anc ⊢ ( 𝜑 → 𝐹 ∥ ( 𝐹 · ( 𝐹 · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) ) )
199 9 oveq1i ⊢ ( 𝐺 − 𝐴 ) = ( ( 𝐴 + ( ( 𝐹 ↑ 2 ) · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) ) − 𝐴 )
200 57 nn0cnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
201 82 nn0cnd ⊢ ( 𝜑 → ( ( 𝐹 ↑ 2 ) · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) ∈ ℂ )
202 200 201 pncan2d ⊢ ( 𝜑 → ( ( 𝐴 + ( ( 𝐹 ↑ 2 ) · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) ) − 𝐴 ) = ( ( 𝐹 ↑ 2 ) · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) )
203 52 oveq1d ⊢ ( 𝜑 → ( ( 𝐹 ↑ 2 ) · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) = ( ( 𝐹 · 𝐹 ) · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) )
204 81 nn0cnd ⊢ ( 𝜑 → ( ( 𝐹 ↑ 2 ) − 𝐴 ) ∈ ℂ )
205 51 51 204 mulassd ⊢ ( 𝜑 → ( ( 𝐹 · 𝐹 ) · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) = ( 𝐹 · ( 𝐹 · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) ) )
206 202 203 205 3eqtrd ⊢ ( 𝜑 → ( ( 𝐴 + ( ( 𝐹 ↑ 2 ) · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) ) − 𝐴 ) = ( 𝐹 · ( 𝐹 · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) ) )
207 199 206 syl5eq ⊢ ( 𝜑 → ( 𝐺 − 𝐴 ) = ( 𝐹 · ( 𝐹 · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) ) )
208 198 207 breqtrrd ⊢ ( 𝜑 → 𝐹 ∥ ( 𝐺 − 𝐴 ) )
209 180 193 208 3jca ⊢ ( 𝜑 → ( ( ( 𝐼 ↑ 2 ) − ( ( ( 𝐺 ↑ 2 ) − 1 ) · ( 𝐻 ↑ 2 ) ) ) = 1 ∧ 𝐸 = ( ( 𝐽 + 1 ) · ( 2 · ( 𝐶 ↑ 2 ) ) ) ∧ 𝐹 ∥ ( 𝐺 − 𝐴 ) ) )
210 zmulcl ⊢ ( ( 2 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 2 · 𝐶 ) ∈ ℤ )
211 18 19 210 sylancr ⊢ ( 𝜑 → ( 2 · 𝐶 ) ∈ ℤ )
212 eluzelz ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℤ )
213 1 212 syl ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
214 82 nn0zd ⊢ ( 𝜑 → ( ( 𝐹 ↑ 2 ) · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) ∈ ℤ )
215 1z ⊢ 1 ∈ ℤ
216 zsubcl ⊢ ( ( 1 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 1 − 𝐴 ) ∈ ℤ )
217 215 213 216 sylancr ⊢ ( 𝜑 → ( 1 − 𝐴 ) ∈ ℤ )
218 zmulcl ⊢ ( ( 1 ∈ ℤ ∧ ( 1 − 𝐴 ) ∈ ℤ ) → ( 1 · ( 1 − 𝐴 ) ) ∈ ℤ )
219 215 217 218 sylancr ⊢ ( 𝜑 → ( 1 · ( 1 − 𝐴 ) ) ∈ ℤ )
220 congid ⊢ ( ( ( 2 · 𝐶 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 2 · 𝐶 ) ∥ ( 𝐴 − 𝐴 ) )
221 211 213 220 syl2anc ⊢ ( 𝜑 → ( 2 · 𝐶 ) ∥ ( 𝐴 − 𝐴 ) )
222 54 nn0zd ⊢ ( 𝜑 → ( 𝐹 ↑ 2 ) ∈ ℤ )
223 215 a1i ⊢ ( 𝜑 → 1 ∈ ℤ )
224 3 nncnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
225 130 224 224 mulassd ⊢ ( 𝜑 → ( ( 2 · 𝐶 ) · 𝐶 ) = ( 2 · ( 𝐶 · 𝐶 ) ) )
226 224 sqvald ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) = ( 𝐶 · 𝐶 ) )
227 226 oveq2d ⊢ ( 𝜑 → ( 2 · ( 𝐶 ↑ 2 ) ) = ( 2 · ( 𝐶 · 𝐶 ) ) )
228 225 227 eqtr4d ⊢ ( 𝜑 → ( ( 2 · 𝐶 ) · 𝐶 ) = ( 2 · ( 𝐶 ↑ 2 ) ) )
229 228 140 eqbrtrd ⊢ ( 𝜑 → ( ( 2 · 𝐶 ) · 𝐶 ) ∥ 𝐸 )
230 muldvds1 ⊢ ( ( ( 2 · 𝐶 ) ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝐸 ∈ ℤ ) → ( ( ( 2 · 𝐶 ) · 𝐶 ) ∥ 𝐸 → ( 2 · 𝐶 ) ∥ 𝐸 ) )
231 211 19 141 230 syl3anc ⊢ ( 𝜑 → ( ( ( 2 · 𝐶 ) · 𝐶 ) ∥ 𝐸 → ( 2 · 𝐶 ) ∥ 𝐸 ) )
232 229 231 mpd ⊢ ( 𝜑 → ( 2 · 𝐶 ) ∥ 𝐸 )
233 zsqcl ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ↑ 2 ) ∈ ℤ )
234 213 233 syl ⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℤ )
235 peano2zm ⊢ ( ( 𝐴 ↑ 2 ) ∈ ℤ → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℤ )
236 234 235 syl ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℤ )
237 236 141 zmulcld ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) − 1 ) · 𝐸 ) ∈ ℤ )
238 dvdsmultr2 ⊢ ( ( ( 2 · 𝐶 ) ∈ ℤ ∧ ( ( ( 𝐴 ↑ 2 ) − 1 ) · 𝐸 ) ∈ ℤ ∧ 𝐸 ∈ ℤ ) → ( ( 2 · 𝐶 ) ∥ 𝐸 → ( 2 · 𝐶 ) ∥ ( ( ( ( 𝐴 ↑ 2 ) − 1 ) · 𝐸 ) · 𝐸 ) ) )
239 211 237 141 238 syl3anc ⊢ ( 𝜑 → ( ( 2 · 𝐶 ) ∥ 𝐸 → ( 2 · 𝐶 ) ∥ ( ( ( ( 𝐴 ↑ 2 ) − 1 ) · 𝐸 ) · 𝐸 ) ) )
240 232 239 mpd ⊢ ( 𝜑 → ( 2 · 𝐶 ) ∥ ( ( ( ( 𝐴 ↑ 2 ) − 1 ) · 𝐸 ) · 𝐸 ) )
241 183 sqvald ⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) = ( 𝐸 · 𝐸 ) )
242 241 oveq2d ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 · 𝐸 ) ) )
243 200 sqcld ⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℂ )
244 subcl ⊢ ( ( ( 𝐴 ↑ 2 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℂ )
245 243 187 244 sylancl ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℂ )
246 245 183 183 mulassd ⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 2 ) − 1 ) · 𝐸 ) · 𝐸 ) = ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 · 𝐸 ) ) )
247 242 246 eqtr4d ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 ↑ 2 ) ) = ( ( ( ( 𝐴 ↑ 2 ) − 1 ) · 𝐸 ) · 𝐸 ) )
248 240 247 breqtrrd ⊢ ( 𝜑 → ( 2 · 𝐶 ) ∥ ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 ↑ 2 ) ) )
249 51 sqcld ⊢ ( 𝜑 → ( 𝐹 ↑ 2 ) ∈ ℂ )
250 183 sqcld ⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℂ )
251 245 250 mulcld ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 ↑ 2 ) ) ∈ ℂ )
252 187 a1i ⊢ ( 𝜑 → 1 ∈ ℂ )
253 subsub23 ⊢ ( ( ( 𝐹 ↑ 2 ) ∈ ℂ ∧ ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 ↑ 2 ) ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝐹 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 ↑ 2 ) ) ) = 1 ↔ ( ( 𝐹 ↑ 2 ) − 1 ) = ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 ↑ 2 ) ) ) )
254 249 251 252 253 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐹 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 ↑ 2 ) ) ) = 1 ↔ ( ( 𝐹 ↑ 2 ) − 1 ) = ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 ↑ 2 ) ) ) )
255 172 254 mpbid ⊢ ( 𝜑 → ( ( 𝐹 ↑ 2 ) − 1 ) = ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 ↑ 2 ) ) )
256 248 255 breqtrrd ⊢ ( 𝜑 → ( 2 · 𝐶 ) ∥ ( ( 𝐹 ↑ 2 ) − 1 ) )
257 congsub ⊢ ( ( ( ( 2 · 𝐶 ) ∈ ℤ ∧ ( 𝐹 ↑ 2 ) ∈ ℤ ∧ 1 ∈ ℤ ) ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ ( ( 2 · 𝐶 ) ∥ ( ( 𝐹 ↑ 2 ) − 1 ) ∧ ( 2 · 𝐶 ) ∥ ( 𝐴 − 𝐴 ) ) ) → ( 2 · 𝐶 ) ∥ ( ( ( 𝐹 ↑ 2 ) − 𝐴 ) − ( 1 − 𝐴 ) ) )
258 211 222 223 213 213 256 221 257 syl322anc ⊢ ( 𝜑 → ( 2 · 𝐶 ) ∥ ( ( ( 𝐹 ↑ 2 ) − 𝐴 ) − ( 1 − 𝐴 ) ) )
259 congmul ⊢ ( ( ( ( 2 · 𝐶 ) ∈ ℤ ∧ ( 𝐹 ↑ 2 ) ∈ ℤ ∧ 1 ∈ ℤ ) ∧ ( ( ( 𝐹 ↑ 2 ) − 𝐴 ) ∈ ℤ ∧ ( 1 − 𝐴 ) ∈ ℤ ) ∧ ( ( 2 · 𝐶 ) ∥ ( ( 𝐹 ↑ 2 ) − 1 ) ∧ ( 2 · 𝐶 ) ∥ ( ( ( 𝐹 ↑ 2 ) − 𝐴 ) − ( 1 − 𝐴 ) ) ) ) → ( 2 · 𝐶 ) ∥ ( ( ( 𝐹 ↑ 2 ) · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) − ( 1 · ( 1 − 𝐴 ) ) ) )
260 211 222 223 195 217 256 258 259 syl322anc ⊢ ( 𝜑 → ( 2 · 𝐶 ) ∥ ( ( ( 𝐹 ↑ 2 ) · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) − ( 1 · ( 1 − 𝐴 ) ) ) )
261 congadd ⊢ ( ( ( ( 2 · 𝐶 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ ( ( ( 𝐹 ↑ 2 ) · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) ∈ ℤ ∧ ( 1 · ( 1 − 𝐴 ) ) ∈ ℤ ) ∧ ( ( 2 · 𝐶 ) ∥ ( 𝐴 − 𝐴 ) ∧ ( 2 · 𝐶 ) ∥ ( ( ( 𝐹 ↑ 2 ) · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) − ( 1 · ( 1 − 𝐴 ) ) ) ) ) → ( 2 · 𝐶 ) ∥ ( ( 𝐴 + ( ( 𝐹 ↑ 2 ) · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) ) − ( 𝐴 + ( 1 · ( 1 − 𝐴 ) ) ) ) )
262 211 213 213 214 219 221 260 261 syl322anc ⊢ ( 𝜑 → ( 2 · 𝐶 ) ∥ ( ( 𝐴 + ( ( 𝐹 ↑ 2 ) · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) ) − ( 𝐴 + ( 1 · ( 1 − 𝐴 ) ) ) ) )
263 9 a1i ⊢ ( 𝜑 → 𝐺 = ( 𝐴 + ( ( 𝐹 ↑ 2 ) · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) ) )
264 217 zcnd ⊢ ( 𝜑 → ( 1 − 𝐴 ) ∈ ℂ )
265 264 mulid2d ⊢ ( 𝜑 → ( 1 · ( 1 − 𝐴 ) ) = ( 1 − 𝐴 ) )
266 265 oveq2d ⊢ ( 𝜑 → ( 𝐴 + ( 1 · ( 1 − 𝐴 ) ) ) = ( 𝐴 + ( 1 − 𝐴 ) ) )
267 pncan3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝐴 + ( 1 − 𝐴 ) ) = 1 )
268 200 187 267 sylancl ⊢ ( 𝜑 → ( 𝐴 + ( 1 − 𝐴 ) ) = 1 )
269 266 268 eqtr2d ⊢ ( 𝜑 → 1 = ( 𝐴 + ( 1 · ( 1 − 𝐴 ) ) ) )
270 263 269 oveq12d ⊢ ( 𝜑 → ( 𝐺 − 1 ) = ( ( 𝐴 + ( ( 𝐹 ↑ 2 ) · ( ( 𝐹 ↑ 2 ) − 𝐴 ) ) ) − ( 𝐴 + ( 1 · ( 1 − 𝐴 ) ) ) ) )
271 262 270 breqtrrd ⊢ ( 𝜑 → ( 2 · 𝐶 ) ∥ ( 𝐺 − 1 ) )
272 eluzelz ⊢ ( 𝐺 ∈ ( ℤ≥ ‘ 2 ) → 𝐺 ∈ ℤ )
273 85 272 syl ⊢ ( 𝜑 → 𝐺 ∈ ℤ )
274 273 213 zsubcld ⊢ ( 𝜑 → ( 𝐺 − 𝐴 ) ∈ ℤ )
275 10 89 eqeltrid ⊢ ( 𝜑 → 𝐻 ∈ ℤ )
276 275 19 zsubcld ⊢ ( 𝜑 → ( 𝐻 − 𝐶 ) ∈ ℤ )
277 jm2.15nn0 ⊢ ( ( 𝐺 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℕ0 ) → ( 𝐺 − 𝐴 ) ∥ ( ( 𝐺 Yrm 𝐵 ) − ( 𝐴 Yrm 𝐵 ) ) )
278 85 1 92 277 syl3anc ⊢ ( 𝜑 → ( 𝐺 − 𝐴 ) ∥ ( ( 𝐺 Yrm 𝐵 ) − ( 𝐴 Yrm 𝐵 ) ) )
279 10 a1i ⊢ ( 𝜑 → 𝐻 = ( 𝐺 Yrm 𝐵 ) )
280 279 4 oveq12d ⊢ ( 𝜑 → ( 𝐻 − 𝐶 ) = ( ( 𝐺 Yrm 𝐵 ) − ( 𝐴 Yrm 𝐵 ) ) )
281 278 280 breqtrrd ⊢ ( 𝜑 → ( 𝐺 − 𝐴 ) ∥ ( 𝐻 − 𝐶 ) )
282 194 274 276 208 281 dvdstrd ⊢ ( 𝜑 → 𝐹 ∥ ( 𝐻 − 𝐶 ) )
283 peano2zm ⊢ ( 𝐺 ∈ ℤ → ( 𝐺 − 1 ) ∈ ℤ )
284 273 283 syl ⊢ ( 𝜑 → ( 𝐺 − 1 ) ∈ ℤ )
285 275 13 zsubcld ⊢ ( 𝜑 → ( 𝐻 − 𝐵 ) ∈ ℤ )
286 jm2.16nn0 ⊢ ( ( 𝐺 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℕ0 ) → ( 𝐺 − 1 ) ∥ ( ( 𝐺 Yrm 𝐵 ) − 𝐵 ) )
287 85 92 286 syl2anc ⊢ ( 𝜑 → ( 𝐺 − 1 ) ∥ ( ( 𝐺 Yrm 𝐵 ) − 𝐵 ) )
288 10 oveq1i ⊢ ( 𝐻 − 𝐵 ) = ( ( 𝐺 Yrm 𝐵 ) − 𝐵 )
289 287 288 breqtrrdi ⊢ ( 𝜑 → ( 𝐺 − 1 ) ∥ ( 𝐻 − 𝐵 ) )
290 211 284 285 271 289 dvdstrd ⊢ ( 𝜑 → ( 2 · 𝐶 ) ∥ ( 𝐻 − 𝐵 ) )
291 rmygeid ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℕ0 ) → 𝐵 ≤ ( 𝐴 Yrm 𝐵 ) )
292 1 92 291 syl2anc ⊢ ( 𝜑 → 𝐵 ≤ ( 𝐴 Yrm 𝐵 ) )
293 292 4 breqtrrd ⊢ ( 𝜑 → 𝐵 ≤ 𝐶 )
294 290 293 jca ⊢ ( 𝜑 → ( ( 2 · 𝐶 ) ∥ ( 𝐻 − 𝐵 ) ∧ 𝐵 ≤ 𝐶 ) )
295 271 282 294 jca31 ⊢ ( 𝜑 → ( ( ( 2 · 𝐶 ) ∥ ( 𝐺 − 1 ) ∧ 𝐹 ∥ ( 𝐻 − 𝐶 ) ) ∧ ( ( 2 · 𝐶 ) ∥ ( 𝐻 − 𝐵 ) ∧ 𝐵 ≤ 𝐶 ) ) )
296 173 209 295 jca31 ⊢ ( 𝜑 → ( ( ( ( ( 𝐷 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐶 ↑ 2 ) ) ) = 1 ∧ ( ( 𝐹 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 ↑ 2 ) ) ) = 1 ∧ 𝐺 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( ( 𝐼 ↑ 2 ) − ( ( ( 𝐺 ↑ 2 ) − 1 ) · ( 𝐻 ↑ 2 ) ) ) = 1 ∧ 𝐸 = ( ( 𝐽 + 1 ) · ( 2 · ( 𝐶 ↑ 2 ) ) ) ∧ 𝐹 ∥ ( 𝐺 − 𝐴 ) ) ) ∧ ( ( ( 2 · 𝐶 ) ∥ ( 𝐺 − 1 ) ∧ 𝐹 ∥ ( 𝐻 − 𝐶 ) ) ∧ ( ( 2 · 𝐶 ) ∥ ( 𝐻 − 𝐵 ) ∧ 𝐵 ≤ 𝐶 ) ) ) )
297 158 296 jca ⊢ ( 𝜑 → ( 𝐽 ∈ ℕ0 ∧ ( ( ( ( ( 𝐷 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐶 ↑ 2 ) ) ) = 1 ∧ ( ( 𝐹 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 ↑ 2 ) ) ) = 1 ∧ 𝐺 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( ( 𝐼 ↑ 2 ) − ( ( ( 𝐺 ↑ 2 ) − 1 ) · ( 𝐻 ↑ 2 ) ) ) = 1 ∧ 𝐸 = ( ( 𝐽 + 1 ) · ( 2 · ( 𝐶 ↑ 2 ) ) ) ∧ 𝐹 ∥ ( 𝐺 − 𝐴 ) ) ) ∧ ( ( ( 2 · 𝐶 ) ∥ ( 𝐺 − 1 ) ∧ 𝐹 ∥ ( 𝐻 − 𝐶 ) ) ∧ ( ( 2 · 𝐶 ) ∥ ( 𝐻 − 𝐵 ) ∧ 𝐵 ≤ 𝐶 ) ) ) ) )
298 49 104 297 jca31 ⊢ ( 𝜑 → ( ( ( 𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ∧ 𝐹 ∈ ℕ0 ) ∧ ( 𝐺 ∈ ℕ0 ∧ 𝐻 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0 ) ) ∧ ( 𝐽 ∈ ℕ0 ∧ ( ( ( ( ( 𝐷 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐶 ↑ 2 ) ) ) = 1 ∧ ( ( 𝐹 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝐸 ↑ 2 ) ) ) = 1 ∧ 𝐺 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( ( 𝐼 ↑ 2 ) − ( ( ( 𝐺 ↑ 2 ) − 1 ) · ( 𝐻 ↑ 2 ) ) ) = 1 ∧ 𝐸 = ( ( 𝐽 + 1 ) · ( 2 · ( 𝐶 ↑ 2 ) ) ) ∧ 𝐹 ∥ ( 𝐺 − 𝐴 ) ) ) ∧ ( ( ( 2 · 𝐶 ) ∥ ( 𝐺 − 1 ) ∧ 𝐹 ∥ ( 𝐻 − 𝐶 ) ) ∧ ( ( 2 · 𝐶 ) ∥ ( 𝐻 − 𝐵 ) ∧ 𝐵 ≤ 𝐶 ) ) ) ) ) )