Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  jm2.27c Structured version   Visualization version   GIF version

Theorem jm2.27c 38095
Description: Lemma for jm2.27 38096. Forward direction with substitutions. (Contributed by Stefan O'Rear, 4-Oct-2014.)
Hypotheses
Ref Expression
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
Ref Expression
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 of Theorem jm2.27c
StepHypRef Expression
1 jm2.27c5 . . . 4 𝐷 = (𝐴 Xrm 𝐵)
2 jm2.27a1 . . . . 5 (𝜑𝐴 ∈ (ℤ‘2))
3 jm2.27a2 . . . . . 6 (𝜑𝐵 ∈ ℕ)
43nnzd 11694 . . . . 5 (𝜑𝐵 ∈ ℤ)
5 frmx 37999 . . . . . 6 Xrm :((ℤ‘2) × ℤ)⟶ℕ0
65fovcl 6932 . . . . 5 ((𝐴 ∈ (ℤ‘2) ∧ 𝐵 ∈ ℤ) → (𝐴 Xrm 𝐵) ∈ ℕ0)
72, 4, 6syl2anc 696 . . . 4 (𝜑 → (𝐴 Xrm 𝐵) ∈ ℕ0)
81, 7syl5eqel 2844 . . 3 (𝜑𝐷 ∈ ℕ0)
9 jm2.27c7 . . . 4 𝐸 = (𝐴 Yrm (2 · 𝑄))
10 2z 11622 . . . . . . 7 2 ∈ ℤ
11 jm2.27c6 . . . . . . . 8 𝑄 = (𝐵 · (𝐴 Yrm 𝐵))
12 jm2.27c4 . . . . . . . . . 10 (𝜑𝐶 = (𝐴 Yrm 𝐵))
13 jm2.27a3 . . . . . . . . . . 11 (𝜑𝐶 ∈ ℕ)
1413nnzd 11694 . . . . . . . . . 10 (𝜑𝐶 ∈ ℤ)
1512, 14eqeltrrd 2841 . . . . . . . . 9 (𝜑 → (𝐴 Yrm 𝐵) ∈ ℤ)
164, 15zmulcld 11701 . . . . . . . 8 (𝜑 → (𝐵 · (𝐴 Yrm 𝐵)) ∈ ℤ)
1711, 16syl5eqel 2844 . . . . . . 7 (𝜑𝑄 ∈ ℤ)
18 zmulcl 11639 . . . . . . 7 ((2 ∈ ℤ ∧ 𝑄 ∈ ℤ) → (2 · 𝑄) ∈ ℤ)
1910, 17, 18sylancr 698 . . . . . 6 (𝜑 → (2 · 𝑄) ∈ ℤ)
20 frmy 38000 . . . . . . 7 Yrm :((ℤ‘2) × ℤ)⟶ℤ
2120fovcl 6932 . . . . . 6 ((𝐴 ∈ (ℤ‘2) ∧ (2 · 𝑄) ∈ ℤ) → (𝐴 Yrm (2 · 𝑄)) ∈ ℤ)
222, 19, 21syl2anc 696 . . . . 5 (𝜑 → (𝐴 Yrm (2 · 𝑄)) ∈ ℤ)
23 rmy0 38015 . . . . . . 7 (𝐴 ∈ (ℤ‘2) → (𝐴 Yrm 0) = 0)
242, 23syl 17 . . . . . 6 (𝜑 → (𝐴 Yrm 0) = 0)
25 2nn 11398 . . . . . . . . . 10 2 ∈ ℕ
2612, 13eqeltrrd 2841 . . . . . . . . . . . 12 (𝜑 → (𝐴 Yrm 𝐵) ∈ ℕ)
273, 26nnmulcld 11281 . . . . . . . . . . 11 (𝜑 → (𝐵 · (𝐴 Yrm 𝐵)) ∈ ℕ)
2811, 27syl5eqel 2844 . . . . . . . . . 10 (𝜑𝑄 ∈ ℕ)
29 nnmulcl 11256 . . . . . . . . . 10 ((2 ∈ ℕ ∧ 𝑄 ∈ ℕ) → (2 · 𝑄) ∈ ℕ)
3025, 28, 29sylancr 698 . . . . . . . . 9 (𝜑 → (2 · 𝑄) ∈ ℕ)
3130nnnn0d 11564 . . . . . . . 8 (𝜑 → (2 · 𝑄) ∈ ℕ0)
3231nn0ge0d 11567 . . . . . . 7 (𝜑 → 0 ≤ (2 · 𝑄))
33 0zd 11602 . . . . . . . 8 (𝜑 → 0 ∈ ℤ)
34 lermy 38043 . . . . . . . 8 ((𝐴 ∈ (ℤ‘2) ∧ 0 ∈ ℤ ∧ (2 · 𝑄) ∈ ℤ) → (0 ≤ (2 · 𝑄) ↔ (𝐴 Yrm 0) ≤ (𝐴 Yrm (2 · 𝑄))))
352, 33, 19, 34syl3anc 1477 . . . . . . 7 (𝜑 → (0 ≤ (2 · 𝑄) ↔ (𝐴 Yrm 0) ≤ (𝐴 Yrm (2 · 𝑄))))
3632, 35mpbid 222 . . . . . 6 (𝜑 → (𝐴 Yrm 0) ≤ (𝐴 Yrm (2 · 𝑄)))
3724, 36eqbrtrrd 4829 . . . . 5 (𝜑 → 0 ≤ (𝐴 Yrm (2 · 𝑄)))
38 elnn0z 11603 . . . . 5 ((𝐴 Yrm (2 · 𝑄)) ∈ ℕ0 ↔ ((𝐴 Yrm (2 · 𝑄)) ∈ ℤ ∧ 0 ≤ (𝐴 Yrm (2 · 𝑄))))
3922, 37, 38sylanbrc 701 . . . 4 (𝜑 → (𝐴 Yrm (2 · 𝑄)) ∈ ℕ0)
409, 39syl5eqel 2844 . . 3 (𝜑𝐸 ∈ ℕ0)
41 jm2.27c8 . . . 4 𝐹 = (𝐴 Xrm (2 · 𝑄))
425fovcl 6932 . . . . 5 ((𝐴 ∈ (ℤ‘2) ∧ (2 · 𝑄) ∈ ℤ) → (𝐴 Xrm (2 · 𝑄)) ∈ ℕ0)
432, 19, 42syl2anc 696 . . . 4 (𝜑 → (𝐴 Xrm (2 · 𝑄)) ∈ ℕ0)
4441, 43syl5eqel 2844 . . 3 (𝜑𝐹 ∈ ℕ0)
458, 40, 443jca 1123 . 2 (𝜑 → (𝐷 ∈ ℕ0𝐸 ∈ ℕ0𝐹 ∈ ℕ0))
46 2nn0 11522 . . . 4 2 ∈ ℕ0
47 jm2.27c9 . . . . 5 𝐺 = (𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴)))
4844nn0cnd 11566 . . . . . . . . 9 (𝜑𝐹 ∈ ℂ)
4948sqvald 13220 . . . . . . . 8 (𝜑 → (𝐹↑2) = (𝐹 · 𝐹))
5044, 44nn0mulcld 11569 . . . . . . . 8 (𝜑 → (𝐹 · 𝐹) ∈ ℕ0)
5149, 50eqeltrd 2840 . . . . . . 7 (𝜑 → (𝐹↑2) ∈ ℕ0)
52 eluz2nn 11940 . . . . . . . . . . . . 13 (𝐴 ∈ (ℤ‘2) → 𝐴 ∈ ℕ)
532, 52syl 17 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℕ)
5453nnnn0d 11564 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℕ0)
5554nn0red 11565 . . . . . . . . . 10 (𝜑𝐴 ∈ ℝ)
5644nn0red 11565 . . . . . . . . . 10 (𝜑𝐹 ∈ ℝ)
5756, 56remulcld 10283 . . . . . . . . . 10 (𝜑 → (𝐹 · 𝐹) ∈ ℝ)
58 rmx1 38012 . . . . . . . . . . . . 13 (𝐴 ∈ (ℤ‘2) → (𝐴 Xrm 1) = 𝐴)
592, 58syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐴 Xrm 1) = 𝐴)
6030nnge1d 11276 . . . . . . . . . . . . 13 (𝜑 → 1 ≤ (2 · 𝑄))
61 1nn0 11521 . . . . . . . . . . . . . . 15 1 ∈ ℕ0
6261a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ ℕ0)
63 lermxnn0 38038 . . . . . . . . . . . . . 14 ((𝐴 ∈ (ℤ‘2) ∧ 1 ∈ ℕ0 ∧ (2 · 𝑄) ∈ ℕ0) → (1 ≤ (2 · 𝑄) ↔ (𝐴 Xrm 1) ≤ (𝐴 Xrm (2 · 𝑄))))
642, 62, 31, 63syl3anc 1477 . . . . . . . . . . . . 13 (𝜑 → (1 ≤ (2 · 𝑄) ↔ (𝐴 Xrm 1) ≤ (𝐴 Xrm (2 · 𝑄))))
6560, 64mpbid 222 . . . . . . . . . . . 12 (𝜑 → (𝐴 Xrm 1) ≤ (𝐴 Xrm (2 · 𝑄)))
6659, 65eqbrtrrd 4829 . . . . . . . . . . 11 (𝜑𝐴 ≤ (𝐴 Xrm (2 · 𝑄)))
6766, 41syl6breqr 4847 . . . . . . . . . 10 (𝜑𝐴𝐹)
6844nn0ge0d 11567 . . . . . . . . . . 11 (𝜑 → 0 ≤ 𝐹)
69 rmxnn 38039 . . . . . . . . . . . . . 14 ((𝐴 ∈ (ℤ‘2) ∧ (2 · 𝑄) ∈ ℤ) → (𝐴 Xrm (2 · 𝑄)) ∈ ℕ)
702, 19, 69syl2anc 696 . . . . . . . . . . . . 13 (𝜑 → (𝐴 Xrm (2 · 𝑄)) ∈ ℕ)
7141, 70syl5eqel 2844 . . . . . . . . . . . 12 (𝜑𝐹 ∈ ℕ)
7271nnge1d 11276 . . . . . . . . . . 11 (𝜑 → 1 ≤ 𝐹)
7356, 56, 68, 72lemulge12d 11175 . . . . . . . . . 10 (𝜑𝐹 ≤ (𝐹 · 𝐹))
7455, 56, 57, 67, 73letrd 10407 . . . . . . . . 9 (𝜑𝐴 ≤ (𝐹 · 𝐹))
7574, 49breqtrrd 4833 . . . . . . . 8 (𝜑𝐴 ≤ (𝐹↑2))
76 nn0sub 11556 . . . . . . . . 9 ((𝐴 ∈ ℕ0 ∧ (𝐹↑2) ∈ ℕ0) → (𝐴 ≤ (𝐹↑2) ↔ ((𝐹↑2) − 𝐴) ∈ ℕ0))
7754, 51, 76syl2anc 696 . . . . . . . 8 (𝜑 → (𝐴 ≤ (𝐹↑2) ↔ ((𝐹↑2) − 𝐴) ∈ ℕ0))
7875, 77mpbid 222 . . . . . . 7 (𝜑 → ((𝐹↑2) − 𝐴) ∈ ℕ0)
7951, 78nn0mulcld 11569 . . . . . 6 (𝜑 → ((𝐹↑2) · ((𝐹↑2) − 𝐴)) ∈ ℕ0)
80 uzaddcl 11958 . . . . . 6 ((𝐴 ∈ (ℤ‘2) ∧ ((𝐹↑2) · ((𝐹↑2) − 𝐴)) ∈ ℕ0) → (𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) ∈ (ℤ‘2))
812, 79, 80syl2anc 696 . . . . 5 (𝜑 → (𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) ∈ (ℤ‘2))
8247, 81syl5eqel 2844 . . . 4 (𝜑𝐺 ∈ (ℤ‘2))
83 eluznn0 11971 . . . 4 ((2 ∈ ℕ0𝐺 ∈ (ℤ‘2)) → 𝐺 ∈ ℕ0)
8446, 82, 83sylancr 698 . . 3 (𝜑𝐺 ∈ ℕ0)
85 jm2.27c10 . . . 4 𝐻 = (𝐺 Yrm 𝐵)
8620fovcl 6932 . . . . . 6 ((𝐺 ∈ (ℤ‘2) ∧ 𝐵 ∈ ℤ) → (𝐺 Yrm 𝐵) ∈ ℤ)
8782, 4, 86syl2anc 696 . . . . 5 (𝜑 → (𝐺 Yrm 𝐵) ∈ ℤ)
88 rmy0 38015 . . . . . . 7 (𝐺 ∈ (ℤ‘2) → (𝐺 Yrm 0) = 0)
8982, 88syl 17 . . . . . 6 (𝜑 → (𝐺 Yrm 0) = 0)
903nnnn0d 11564 . . . . . . . 8 (𝜑𝐵 ∈ ℕ0)
9190nn0ge0d 11567 . . . . . . 7 (𝜑 → 0 ≤ 𝐵)
92 lermy 38043 . . . . . . . 8 ((𝐺 ∈ (ℤ‘2) ∧ 0 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (0 ≤ 𝐵 ↔ (𝐺 Yrm 0) ≤ (𝐺 Yrm 𝐵)))
9382, 33, 4, 92syl3anc 1477 . . . . . . 7 (𝜑 → (0 ≤ 𝐵 ↔ (𝐺 Yrm 0) ≤ (𝐺 Yrm 𝐵)))
9491, 93mpbid 222 . . . . . 6 (𝜑 → (𝐺 Yrm 0) ≤ (𝐺 Yrm 𝐵))
9589, 94eqbrtrrd 4829 . . . . 5 (𝜑 → 0 ≤ (𝐺 Yrm 𝐵))
96 elnn0z 11603 . . . . 5 ((𝐺 Yrm 𝐵) ∈ ℕ0 ↔ ((𝐺 Yrm 𝐵) ∈ ℤ ∧ 0 ≤ (𝐺 Yrm 𝐵)))
9787, 95, 96sylanbrc 701 . . . 4 (𝜑 → (𝐺 Yrm 𝐵) ∈ ℕ0)
9885, 97syl5eqel 2844 . . 3 (𝜑𝐻 ∈ ℕ0)
99 jm2.27c11 . . . 4 𝐼 = (𝐺 Xrm 𝐵)
1005fovcl 6932 . . . . 5 ((𝐺 ∈ (ℤ‘2) ∧ 𝐵 ∈ ℤ) → (𝐺 Xrm 𝐵) ∈ ℕ0)
10182, 4, 100syl2anc 696 . . . 4 (𝜑 → (𝐺 Xrm 𝐵) ∈ ℕ0)
10299, 101syl5eqel 2844 . . 3 (𝜑𝐼 ∈ ℕ0)
10384, 98, 1023jca 1123 . 2 (𝜑 → (𝐺 ∈ ℕ0𝐻 ∈ ℕ0𝐼 ∈ ℕ0))
104 jm2.27c12 . . . 4 𝐽 = ((𝐸 / (2 · (𝐶↑2))) − 1)
105 iddvds 15218 . . . . . . . . . . . 12 ((𝐵 · (𝐴 Yrm 𝐵)) ∈ ℤ → (𝐵 · (𝐴 Yrm 𝐵)) ∥ (𝐵 · (𝐴 Yrm 𝐵)))
10616, 105syl 17 . . . . . . . . . . 11 (𝜑 → (𝐵 · (𝐴 Yrm 𝐵)) ∥ (𝐵 · (𝐴 Yrm 𝐵)))
107106, 11syl6breqr 4847 . . . . . . . . . 10 (𝜑 → (𝐵 · (𝐴 Yrm 𝐵)) ∥ 𝑄)
108 jm2.20nn 38085 . . . . . . . . . . 11 ((𝐴 ∈ (ℤ‘2) ∧ 𝑄 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (((𝐴 Yrm 𝐵)↑2) ∥ (𝐴 Yrm 𝑄) ↔ (𝐵 · (𝐴 Yrm 𝐵)) ∥ 𝑄))
1092, 28, 3, 108syl3anc 1477 . . . . . . . . . 10 (𝜑 → (((𝐴 Yrm 𝐵)↑2) ∥ (𝐴 Yrm 𝑄) ↔ (𝐵 · (𝐴 Yrm 𝐵)) ∥ 𝑄))
110107, 109mpbird 247 . . . . . . . . 9 (𝜑 → ((𝐴 Yrm 𝐵)↑2) ∥ (𝐴 Yrm 𝑄))
111 zsqcl 13149 . . . . . . . . . . 11 ((𝐴 Yrm 𝐵) ∈ ℤ → ((𝐴 Yrm 𝐵)↑2) ∈ ℤ)
11215, 111syl 17 . . . . . . . . . 10 (𝜑 → ((𝐴 Yrm 𝐵)↑2) ∈ ℤ)
11320fovcl 6932 . . . . . . . . . . 11 ((𝐴 ∈ (ℤ‘2) ∧ 𝑄 ∈ ℤ) → (𝐴 Yrm 𝑄) ∈ ℤ)
1142, 17, 113syl2anc 696 . . . . . . . . . 10 (𝜑 → (𝐴 Yrm 𝑄) ∈ ℤ)
11510a1i 11 . . . . . . . . . 10 (𝜑 → 2 ∈ ℤ)
116 dvdscmul 15231 . . . . . . . . . 10 ((((𝐴 Yrm 𝐵)↑2) ∈ ℤ ∧ (𝐴 Yrm 𝑄) ∈ ℤ ∧ 2 ∈ ℤ) → (((𝐴 Yrm 𝐵)↑2) ∥ (𝐴 Yrm 𝑄) → (2 · ((𝐴 Yrm 𝐵)↑2)) ∥ (2 · (𝐴 Yrm 𝑄))))
117112, 114, 115, 116syl3anc 1477 . . . . . . . . 9 (𝜑 → (((𝐴 Yrm 𝐵)↑2) ∥ (𝐴 Yrm 𝑄) → (2 · ((𝐴 Yrm 𝐵)↑2)) ∥ (2 · (𝐴 Yrm 𝑄))))
118110, 117mpd 15 . . . . . . . 8 (𝜑 → (2 · ((𝐴 Yrm 𝐵)↑2)) ∥ (2 · (𝐴 Yrm 𝑄)))
119 zmulcl 11639 . . . . . . . . . . 11 ((2 ∈ ℤ ∧ (𝐴 Yrm 𝑄) ∈ ℤ) → (2 · (𝐴 Yrm 𝑄)) ∈ ℤ)
12010, 114, 119sylancr 698 . . . . . . . . . 10 (𝜑 → (2 · (𝐴 Yrm 𝑄)) ∈ ℤ)
1215fovcl 6932 . . . . . . . . . . . 12 ((𝐴 ∈ (ℤ‘2) ∧ 𝑄 ∈ ℤ) → (𝐴 Xrm 𝑄) ∈ ℕ0)
1222, 17, 121syl2anc 696 . . . . . . . . . . 11 (𝜑 → (𝐴 Xrm 𝑄) ∈ ℕ0)
123122nn0zd 11693 . . . . . . . . . 10 (𝜑 → (𝐴 Xrm 𝑄) ∈ ℤ)
124 dvdsmul1 15226 . . . . . . . . . 10 (((2 · (𝐴 Yrm 𝑄)) ∈ ℤ ∧ (𝐴 Xrm 𝑄) ∈ ℤ) → (2 · (𝐴 Yrm 𝑄)) ∥ ((2 · (𝐴 Yrm 𝑄)) · (𝐴 Xrm 𝑄)))
125120, 123, 124syl2anc 696 . . . . . . . . 9 (𝜑 → (2 · (𝐴 Yrm 𝑄)) ∥ ((2 · (𝐴 Yrm 𝑄)) · (𝐴 Xrm 𝑄)))
126 rmydbl 38026 . . . . . . . . . . 11 ((𝐴 ∈ (ℤ‘2) ∧ 𝑄 ∈ ℤ) → (𝐴 Yrm (2 · 𝑄)) = ((2 · (𝐴 Xrm 𝑄)) · (𝐴 Yrm 𝑄)))
1272, 17, 126syl2anc 696 . . . . . . . . . 10 (𝜑 → (𝐴 Yrm (2 · 𝑄)) = ((2 · (𝐴 Xrm 𝑄)) · (𝐴 Yrm 𝑄)))
128 2cnd 11306 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℂ)
129122nn0cnd 11566 . . . . . . . . . . 11 (𝜑 → (𝐴 Xrm 𝑄) ∈ ℂ)
130114zcnd 11696 . . . . . . . . . . 11 (𝜑 → (𝐴 Yrm 𝑄) ∈ ℂ)
131128, 129, 130mul32d 10459 . . . . . . . . . 10 (𝜑 → ((2 · (𝐴 Xrm 𝑄)) · (𝐴 Yrm 𝑄)) = ((2 · (𝐴 Yrm 𝑄)) · (𝐴 Xrm 𝑄)))
132127, 131eqtrd 2795 . . . . . . . . 9 (𝜑 → (𝐴 Yrm (2 · 𝑄)) = ((2 · (𝐴 Yrm 𝑄)) · (𝐴 Xrm 𝑄)))
133125, 132breqtrrd 4833 . . . . . . . 8 (𝜑 → (2 · (𝐴 Yrm 𝑄)) ∥ (𝐴 Yrm (2 · 𝑄)))
134 zmulcl 11639 . . . . . . . . . 10 ((2 ∈ ℤ ∧ ((𝐴 Yrm 𝐵)↑2) ∈ ℤ) → (2 · ((𝐴 Yrm 𝐵)↑2)) ∈ ℤ)
13510, 112, 134sylancr 698 . . . . . . . . 9 (𝜑 → (2 · ((𝐴 Yrm 𝐵)↑2)) ∈ ℤ)
136 dvdstr 15241 . . . . . . . . 9 (((2 · ((𝐴 Yrm 𝐵)↑2)) ∈ ℤ ∧ (2 · (𝐴 Yrm 𝑄)) ∈ ℤ ∧ (𝐴 Yrm (2 · 𝑄)) ∈ ℤ) → (((2 · ((𝐴 Yrm 𝐵)↑2)) ∥ (2 · (𝐴 Yrm 𝑄)) ∧ (2 · (𝐴 Yrm 𝑄)) ∥ (𝐴 Yrm (2 · 𝑄))) → (2 · ((𝐴 Yrm 𝐵)↑2)) ∥ (𝐴 Yrm (2 · 𝑄))))
137135, 120, 22, 136syl3anc 1477 . . . . . . . 8 (𝜑 → (((2 · ((𝐴 Yrm 𝐵)↑2)) ∥ (2 · (𝐴 Yrm 𝑄)) ∧ (2 · (𝐴 Yrm 𝑄)) ∥ (𝐴 Yrm (2 · 𝑄))) → (2 · ((𝐴 Yrm 𝐵)↑2)) ∥ (𝐴 Yrm (2 · 𝑄))))
138118, 133, 137mp2and 717 . . . . . . 7 (𝜑 → (2 · ((𝐴 Yrm 𝐵)↑2)) ∥ (𝐴 Yrm (2 · 𝑄)))
13912oveq1d 6830 . . . . . . . 8 (𝜑 → (𝐶↑2) = ((𝐴 Yrm 𝐵)↑2))
140139oveq2d 6831 . . . . . . 7 (𝜑 → (2 · (𝐶↑2)) = (2 · ((𝐴 Yrm 𝐵)↑2)))
1419a1i 11 . . . . . . 7 (𝜑𝐸 = (𝐴 Yrm (2 · 𝑄)))
142138, 140, 1413brtr4d 4837 . . . . . 6 (𝜑 → (2 · (𝐶↑2)) ∥ 𝐸)
1439, 22syl5eqel 2844 . . . . . . . 8 (𝜑𝐸 ∈ ℤ)
14430nngt0d 11277 . . . . . . . . . 10 (𝜑 → 0 < (2 · 𝑄))
145 ltrmy 38040 . . . . . . . . . . 11 ((𝐴 ∈ (ℤ‘2) ∧ 0 ∈ ℤ ∧ (2 · 𝑄) ∈ ℤ) → (0 < (2 · 𝑄) ↔ (𝐴 Yrm 0) < (𝐴 Yrm (2 · 𝑄))))
1462, 33, 19, 145syl3anc 1477 . . . . . . . . . 10 (𝜑 → (0 < (2 · 𝑄) ↔ (𝐴 Yrm 0) < (𝐴 Yrm (2 · 𝑄))))
147144, 146mpbid 222 . . . . . . . . 9 (𝜑 → (𝐴 Yrm 0) < (𝐴 Yrm (2 · 𝑄)))
14824eqcomd 2767 . . . . . . . . 9 (𝜑 → 0 = (𝐴 Yrm 0))
149147, 148, 1413brtr4d 4837 . . . . . . . 8 (𝜑 → 0 < 𝐸)
150 elnnz 11600 . . . . . . . 8 (𝐸 ∈ ℕ ↔ (𝐸 ∈ ℤ ∧ 0 < 𝐸))
151143, 149, 150sylanbrc 701 . . . . . . 7 (𝜑𝐸 ∈ ℕ)
15213nnsqcld 13244 . . . . . . . 8 (𝜑 → (𝐶↑2) ∈ ℕ)
153 nnmulcl 11256 . . . . . . . 8 ((2 ∈ ℕ ∧ (𝐶↑2) ∈ ℕ) → (2 · (𝐶↑2)) ∈ ℕ)
15425, 152, 153sylancr 698 . . . . . . 7 (𝜑 → (2 · (𝐶↑2)) ∈ ℕ)
155 nndivdvds 15212 . . . . . . 7 ((𝐸 ∈ ℕ ∧ (2 · (𝐶↑2)) ∈ ℕ) → ((2 · (𝐶↑2)) ∥ 𝐸 ↔ (𝐸 / (2 · (𝐶↑2))) ∈ ℕ))
156151, 154, 155syl2anc 696 . . . . . 6 (𝜑 → ((2 · (𝐶↑2)) ∥ 𝐸 ↔ (𝐸 / (2 · (𝐶↑2))) ∈ ℕ))
157142, 156mpbid 222 . . . . 5 (𝜑 → (𝐸 / (2 · (𝐶↑2))) ∈ ℕ)
158 nnm1nn0 11547 . . . . 5 ((𝐸 / (2 · (𝐶↑2))) ∈ ℕ → ((𝐸 / (2 · (𝐶↑2))) − 1) ∈ ℕ0)
159157, 158syl 17 . . . 4 (𝜑 → ((𝐸 / (2 · (𝐶↑2))) − 1) ∈ ℕ0)
160104, 159syl5eqel 2844 . . 3 (𝜑𝐽 ∈ ℕ0)
1611oveq1i 6825 . . . . . . . 8 (𝐷↑2) = ((𝐴 Xrm 𝐵)↑2)
162161a1i 11 . . . . . . 7 (𝜑 → (𝐷↑2) = ((𝐴 Xrm 𝐵)↑2))
163139oveq2d 6831 . . . . . . 7 (𝜑 → (((𝐴↑2) − 1) · (𝐶↑2)) = (((𝐴↑2) − 1) · ((𝐴 Yrm 𝐵)↑2)))
164162, 163oveq12d 6833 . . . . . 6 (𝜑 → ((𝐷↑2) − (((𝐴↑2) − 1) · (𝐶↑2))) = (((𝐴 Xrm 𝐵)↑2) − (((𝐴↑2) − 1) · ((𝐴 Yrm 𝐵)↑2))))
165 rmxynorm 38004 . . . . . . 7 ((𝐴 ∈ (ℤ‘2) ∧ 𝐵 ∈ ℤ) → (((𝐴 Xrm 𝐵)↑2) − (((𝐴↑2) − 1) · ((𝐴 Yrm 𝐵)↑2))) = 1)
1662, 4, 165syl2anc 696 . . . . . 6 (𝜑 → (((𝐴 Xrm 𝐵)↑2) − (((𝐴↑2) − 1) · ((𝐴 Yrm 𝐵)↑2))) = 1)
167164, 166eqtrd 2795 . . . . 5 (𝜑 → ((𝐷↑2) − (((𝐴↑2) − 1) · (𝐶↑2))) = 1)
16841oveq1i 6825 . . . . . . 7 (𝐹↑2) = ((𝐴 Xrm (2 · 𝑄))↑2)
1699oveq1i 6825 . . . . . . . 8 (𝐸↑2) = ((𝐴 Yrm (2 · 𝑄))↑2)
170169oveq2i 6826 . . . . . . 7 (((𝐴↑2) − 1) · (𝐸↑2)) = (((𝐴↑2) − 1) · ((𝐴 Yrm (2 · 𝑄))↑2))
171168, 170oveq12i 6827 . . . . . 6 ((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = (((𝐴 Xrm (2 · 𝑄))↑2) − (((𝐴↑2) − 1) · ((𝐴 Yrm (2 · 𝑄))↑2)))
172 rmxynorm 38004 . . . . . . 7 ((𝐴 ∈ (ℤ‘2) ∧ (2 · 𝑄) ∈ ℤ) → (((𝐴 Xrm (2 · 𝑄))↑2) − (((𝐴↑2) − 1) · ((𝐴 Yrm (2 · 𝑄))↑2))) = 1)
1732, 19, 172syl2anc 696 . . . . . 6 (𝜑 → (((𝐴 Xrm (2 · 𝑄))↑2) − (((𝐴↑2) − 1) · ((𝐴 Yrm (2 · 𝑄))↑2))) = 1)
174171, 173syl5eq 2807 . . . . 5 (𝜑 → ((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = 1)
175167, 174, 823jca 1123 . . . 4 (𝜑 → (((𝐷↑2) − (((𝐴↑2) − 1) · (𝐶↑2))) = 1 ∧ ((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = 1 ∧ 𝐺 ∈ (ℤ‘2)))
17699oveq1i 6825 . . . . . . 7 (𝐼↑2) = ((𝐺 Xrm 𝐵)↑2)
17785oveq1i 6825 . . . . . . . 8 (𝐻↑2) = ((𝐺 Yrm 𝐵)↑2)
178177oveq2i 6826 . . . . . . 7 (((𝐺↑2) − 1) · (𝐻↑2)) = (((𝐺↑2) − 1) · ((𝐺 Yrm 𝐵)↑2))
179176, 178oveq12i 6827 . . . . . 6 ((𝐼↑2) − (((𝐺↑2) − 1) · (𝐻↑2))) = (((𝐺 Xrm 𝐵)↑2) − (((𝐺↑2) − 1) · ((𝐺 Yrm 𝐵)↑2)))
180 rmxynorm 38004 . . . . . . 7 ((𝐺 ∈ (ℤ‘2) ∧ 𝐵 ∈ ℤ) → (((𝐺 Xrm 𝐵)↑2) − (((𝐺↑2) − 1) · ((𝐺 Yrm 𝐵)↑2))) = 1)
18182, 4, 180syl2anc 696 . . . . . 6 (𝜑 → (((𝐺 Xrm 𝐵)↑2) − (((𝐺↑2) − 1) · ((𝐺 Yrm 𝐵)↑2))) = 1)
182179, 181syl5eq 2807 . . . . 5 (𝜑 → ((𝐼↑2) − (((𝐺↑2) − 1) · (𝐻↑2))) = 1)
183104a1i 11 . . . . . . . . 9 (𝜑𝐽 = ((𝐸 / (2 · (𝐶↑2))) − 1))
184183oveq1d 6830 . . . . . . . 8 (𝜑 → (𝐽 + 1) = (((𝐸 / (2 · (𝐶↑2))) − 1) + 1))
185143zcnd 11696 . . . . . . . . . 10 (𝜑𝐸 ∈ ℂ)
186154nncnd 11249 . . . . . . . . . 10 (𝜑 → (2 · (𝐶↑2)) ∈ ℂ)
187154nnne0d 11278 . . . . . . . . . 10 (𝜑 → (2 · (𝐶↑2)) ≠ 0)
188185, 186, 187divcld 11014 . . . . . . . . 9 (𝜑 → (𝐸 / (2 · (𝐶↑2))) ∈ ℂ)
189 ax-1cn 10207 . . . . . . . . 9 1 ∈ ℂ
190 npcan 10503 . . . . . . . . 9 (((𝐸 / (2 · (𝐶↑2))) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐸 / (2 · (𝐶↑2))) − 1) + 1) = (𝐸 / (2 · (𝐶↑2))))
191188, 189, 190sylancl 697 . . . . . . . 8 (𝜑 → (((𝐸 / (2 · (𝐶↑2))) − 1) + 1) = (𝐸 / (2 · (𝐶↑2))))
192184, 191eqtrd 2795 . . . . . . 7 (𝜑 → (𝐽 + 1) = (𝐸 / (2 · (𝐶↑2))))
193192oveq1d 6830 . . . . . 6 (𝜑 → ((𝐽 + 1) · (2 · (𝐶↑2))) = ((𝐸 / (2 · (𝐶↑2))) · (2 · (𝐶↑2))))
194185, 186, 187divcan1d 11015 . . . . . 6 (𝜑 → ((𝐸 / (2 · (𝐶↑2))) · (2 · (𝐶↑2))) = 𝐸)
195193, 194eqtr2d 2796 . . . . 5 (𝜑𝐸 = ((𝐽 + 1) · (2 · (𝐶↑2))))
19644nn0zd 11693 . . . . . . 7 (𝜑𝐹 ∈ ℤ)
19778nn0zd 11693 . . . . . . . 8 (𝜑 → ((𝐹↑2) − 𝐴) ∈ ℤ)
198196, 197zmulcld 11701 . . . . . . 7 (𝜑 → (𝐹 · ((𝐹↑2) − 𝐴)) ∈ ℤ)
199 dvdsmul1 15226 . . . . . . 7 ((𝐹 ∈ ℤ ∧ (𝐹 · ((𝐹↑2) − 𝐴)) ∈ ℤ) → 𝐹 ∥ (𝐹 · (𝐹 · ((𝐹↑2) − 𝐴))))
200196, 198, 199syl2anc 696 . . . . . 6 (𝜑𝐹 ∥ (𝐹 · (𝐹 · ((𝐹↑2) − 𝐴))))
20147oveq1i 6825 . . . . . . 7 (𝐺𝐴) = ((𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) − 𝐴)
20254nn0cnd 11566 . . . . . . . . 9 (𝜑𝐴 ∈ ℂ)
20379nn0cnd 11566 . . . . . . . . 9 (𝜑 → ((𝐹↑2) · ((𝐹↑2) − 𝐴)) ∈ ℂ)
204202, 203pncan2d 10607 . . . . . . . 8 (𝜑 → ((𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) − 𝐴) = ((𝐹↑2) · ((𝐹↑2) − 𝐴)))
20549oveq1d 6830 . . . . . . . 8 (𝜑 → ((𝐹↑2) · ((𝐹↑2) − 𝐴)) = ((𝐹 · 𝐹) · ((𝐹↑2) − 𝐴)))
20678nn0cnd 11566 . . . . . . . . 9 (𝜑 → ((𝐹↑2) − 𝐴) ∈ ℂ)
20748, 48, 206mulassd 10276 . . . . . . . 8 (𝜑 → ((𝐹 · 𝐹) · ((𝐹↑2) − 𝐴)) = (𝐹 · (𝐹 · ((𝐹↑2) − 𝐴))))
208204, 205, 2073eqtrd 2799 . . . . . . 7 (𝜑 → ((𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) − 𝐴) = (𝐹 · (𝐹 · ((𝐹↑2) − 𝐴))))
209201, 208syl5eq 2807 . . . . . 6 (𝜑 → (𝐺𝐴) = (𝐹 · (𝐹 · ((𝐹↑2) − 𝐴))))
210200, 209breqtrrd 4833 . . . . 5 (𝜑𝐹 ∥ (𝐺𝐴))
211182, 195, 2103jca 1123 . . . 4 (𝜑 → (((𝐼↑2) − (((𝐺↑2) − 1) · (𝐻↑2))) = 1 ∧ 𝐸 = ((𝐽 + 1) · (2 · (𝐶↑2))) ∧ 𝐹 ∥ (𝐺𝐴)))
212 zmulcl 11639 . . . . . . . 8 ((2 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (2 · 𝐶) ∈ ℤ)
21310, 14, 212sylancr 698 . . . . . . 7 (𝜑 → (2 · 𝐶) ∈ ℤ)
214 eluzelz 11910 . . . . . . . 8 (𝐴 ∈ (ℤ‘2) → 𝐴 ∈ ℤ)
2152, 214syl 17 . . . . . . 7 (𝜑𝐴 ∈ ℤ)
21679nn0zd 11693 . . . . . . 7 (𝜑 → ((𝐹↑2) · ((𝐹↑2) − 𝐴)) ∈ ℤ)
217 1z 11620 . . . . . . . 8 1 ∈ ℤ
218 zsubcl 11632 . . . . . . . . 9 ((1 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (1 − 𝐴) ∈ ℤ)
219217, 215, 218sylancr 698 . . . . . . . 8 (𝜑 → (1 − 𝐴) ∈ ℤ)
220 zmulcl 11639 . . . . . . . 8 ((1 ∈ ℤ ∧ (1 − 𝐴) ∈ ℤ) → (1 · (1 − 𝐴)) ∈ ℤ)
221217, 219, 220sylancr 698 . . . . . . 7 (𝜑 → (1 · (1 − 𝐴)) ∈ ℤ)
222 congid 38059 . . . . . . . 8 (((2 · 𝐶) ∈ ℤ ∧ 𝐴 ∈ ℤ) → (2 · 𝐶) ∥ (𝐴𝐴))
223213, 215, 222syl2anc 696 . . . . . . 7 (𝜑 → (2 · 𝐶) ∥ (𝐴𝐴))
22451nn0zd 11693 . . . . . . . 8 (𝜑 → (𝐹↑2) ∈ ℤ)
225217a1i 11 . . . . . . . 8 (𝜑 → 1 ∈ ℤ)
22613nncnd 11249 . . . . . . . . . . . . . . 15 (𝜑𝐶 ∈ ℂ)
227128, 226, 226mulassd 10276 . . . . . . . . . . . . . 14 (𝜑 → ((2 · 𝐶) · 𝐶) = (2 · (𝐶 · 𝐶)))
228226sqvald 13220 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶↑2) = (𝐶 · 𝐶))
229228oveq2d 6831 . . . . . . . . . . . . . 14 (𝜑 → (2 · (𝐶↑2)) = (2 · (𝐶 · 𝐶)))
230227, 229eqtr4d 2798 . . . . . . . . . . . . 13 (𝜑 → ((2 · 𝐶) · 𝐶) = (2 · (𝐶↑2)))
231230, 142eqbrtrd 4827 . . . . . . . . . . . 12 (𝜑 → ((2 · 𝐶) · 𝐶) ∥ 𝐸)
232 muldvds1 15229 . . . . . . . . . . . . 13 (((2 · 𝐶) ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝐸 ∈ ℤ) → (((2 · 𝐶) · 𝐶) ∥ 𝐸 → (2 · 𝐶) ∥ 𝐸))
233213, 14, 143, 232syl3anc 1477 . . . . . . . . . . . 12 (𝜑 → (((2 · 𝐶) · 𝐶) ∥ 𝐸 → (2 · 𝐶) ∥ 𝐸))
234231, 233mpd 15 . . . . . . . . . . 11 (𝜑 → (2 · 𝐶) ∥ 𝐸)
235 zsqcl 13149 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ)
236215, 235syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝐴↑2) ∈ ℤ)
237 peano2zm 11633 . . . . . . . . . . . . . 14 ((𝐴↑2) ∈ ℤ → ((𝐴↑2) − 1) ∈ ℤ)
238236, 237syl 17 . . . . . . . . . . . . 13 (𝜑 → ((𝐴↑2) − 1) ∈ ℤ)
239238, 143zmulcld 11701 . . . . . . . . . . . 12 (𝜑 → (((𝐴↑2) − 1) · 𝐸) ∈ ℤ)
240 dvdsmultr2 15244 . . . . . . . . . . . 12 (((2 · 𝐶) ∈ ℤ ∧ (((𝐴↑2) − 1) · 𝐸) ∈ ℤ ∧ 𝐸 ∈ ℤ) → ((2 · 𝐶) ∥ 𝐸 → (2 · 𝐶) ∥ ((((𝐴↑2) − 1) · 𝐸) · 𝐸)))
241213, 239, 143, 240syl3anc 1477 . . . . . . . . . . 11 (𝜑 → ((2 · 𝐶) ∥ 𝐸 → (2 · 𝐶) ∥ ((((𝐴↑2) − 1) · 𝐸) · 𝐸)))
242234, 241mpd 15 . . . . . . . . . 10 (𝜑 → (2 · 𝐶) ∥ ((((𝐴↑2) − 1) · 𝐸) · 𝐸))
243185sqvald 13220 . . . . . . . . . . . 12 (𝜑 → (𝐸↑2) = (𝐸 · 𝐸))
244243oveq2d 6831 . . . . . . . . . . 11 (𝜑 → (((𝐴↑2) − 1) · (𝐸↑2)) = (((𝐴↑2) − 1) · (𝐸 · 𝐸)))
245202sqcld 13221 . . . . . . . . . . . . 13 (𝜑 → (𝐴↑2) ∈ ℂ)
246 subcl 10493 . . . . . . . . . . . . 13 (((𝐴↑2) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐴↑2) − 1) ∈ ℂ)
247245, 189, 246sylancl 697 . . . . . . . . . . . 12 (𝜑 → ((𝐴↑2) − 1) ∈ ℂ)
248247, 185, 185mulassd 10276 . . . . . . . . . . 11 (𝜑 → ((((𝐴↑2) − 1) · 𝐸) · 𝐸) = (((𝐴↑2) − 1) · (𝐸 · 𝐸)))
249244, 248eqtr4d 2798 . . . . . . . . . 10 (𝜑 → (((𝐴↑2) − 1) · (𝐸↑2)) = ((((𝐴↑2) − 1) · 𝐸) · 𝐸))
250242, 249breqtrrd 4833 . . . . . . . . 9 (𝜑 → (2 · 𝐶) ∥ (((𝐴↑2) − 1) · (𝐸↑2)))
25148sqcld 13221 . . . . . . . . . . 11 (𝜑 → (𝐹↑2) ∈ ℂ)
252185sqcld 13221 . . . . . . . . . . . 12 (𝜑 → (𝐸↑2) ∈ ℂ)
253247, 252mulcld 10273 . . . . . . . . . . 11 (𝜑 → (((𝐴↑2) − 1) · (𝐸↑2)) ∈ ℂ)
254189a1i 11 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℂ)
255 subsub23 10499 . . . . . . . . . . 11 (((𝐹↑2) ∈ ℂ ∧ (((𝐴↑2) − 1) · (𝐸↑2)) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = 1 ↔ ((𝐹↑2) − 1) = (((𝐴↑2) − 1) · (𝐸↑2))))
256251, 253, 254, 255syl3anc 1477 . . . . . . . . . 10 (𝜑 → (((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = 1 ↔ ((𝐹↑2) − 1) = (((𝐴↑2) − 1) · (𝐸↑2))))
257174, 256mpbid 222 . . . . . . . . 9 (𝜑 → ((𝐹↑2) − 1) = (((𝐴↑2) − 1) · (𝐸↑2)))
258250, 257breqtrrd 4833 . . . . . . . 8 (𝜑 → (2 · 𝐶) ∥ ((𝐹↑2) − 1))
259 congsub 38058 . . . . . . . . 9 ((((2 · 𝐶) ∈ ℤ ∧ (𝐹↑2) ∈ ℤ ∧ 1 ∈ ℤ) ∧ (𝐴 ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ ((2 · 𝐶) ∥ ((𝐹↑2) − 1) ∧ (2 · 𝐶) ∥ (𝐴𝐴))) → (2 · 𝐶) ∥ (((𝐹↑2) − 𝐴) − (1 − 𝐴)))
260213, 224, 225, 215, 215, 258, 223, 259syl322anc 1505 . . . . . . . 8 (𝜑 → (2 · 𝐶) ∥ (((𝐹↑2) − 𝐴) − (1 − 𝐴)))
261 congmul 38055 . . . . . . . 8 ((((2 · 𝐶) ∈ ℤ ∧ (𝐹↑2) ∈ ℤ ∧ 1 ∈ ℤ) ∧ (((𝐹↑2) − 𝐴) ∈ ℤ ∧ (1 − 𝐴) ∈ ℤ) ∧ ((2 · 𝐶) ∥ ((𝐹↑2) − 1) ∧ (2 · 𝐶) ∥ (((𝐹↑2) − 𝐴) − (1 − 𝐴)))) → (2 · 𝐶) ∥ (((𝐹↑2) · ((𝐹↑2) − 𝐴)) − (1 · (1 − 𝐴))))
262213, 224, 225, 197, 219, 258, 260, 261syl322anc 1505 . . . . . . 7 (𝜑 → (2 · 𝐶) ∥ (((𝐹↑2) · ((𝐹↑2) − 𝐴)) − (1 · (1 − 𝐴))))
263 congadd 38054 . . . . . . 7 ((((2 · 𝐶) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ (((𝐹↑2) · ((𝐹↑2) − 𝐴)) ∈ ℤ ∧ (1 · (1 − 𝐴)) ∈ ℤ) ∧ ((2 · 𝐶) ∥ (𝐴𝐴) ∧ (2 · 𝐶) ∥ (((𝐹↑2) · ((𝐹↑2) − 𝐴)) − (1 · (1 − 𝐴))))) → (2 · 𝐶) ∥ ((𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) − (𝐴 + (1 · (1 − 𝐴)))))
264213, 215, 215, 216, 221, 223, 262, 263syl322anc 1505 . . . . . 6 (𝜑 → (2 · 𝐶) ∥ ((𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) − (𝐴 + (1 · (1 − 𝐴)))))
26547a1i 11 . . . . . . 7 (𝜑𝐺 = (𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))))
266219zcnd 11696 . . . . . . . . . 10 (𝜑 → (1 − 𝐴) ∈ ℂ)
267266mulid2d 10271 . . . . . . . . 9 (𝜑 → (1 · (1 − 𝐴)) = (1 − 𝐴))
268267oveq2d 6831 . . . . . . . 8 (𝜑 → (𝐴 + (1 · (1 − 𝐴))) = (𝐴 + (1 − 𝐴)))
269 pncan3 10502 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + (1 − 𝐴)) = 1)
270202, 189, 269sylancl 697 . . . . . . . 8 (𝜑 → (𝐴 + (1 − 𝐴)) = 1)
271268, 270eqtr2d 2796 . . . . . . 7 (𝜑 → 1 = (𝐴 + (1 · (1 − 𝐴))))
272265, 271oveq12d 6833 . . . . . 6 (𝜑 → (𝐺 − 1) = ((𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) − (𝐴 + (1 · (1 − 𝐴)))))
273264, 272breqtrrd 4833 . . . . 5 (𝜑 → (2 · 𝐶) ∥ (𝐺 − 1))
274 jm2.15nn0 38091 . . . . . . . 8 ((𝐺 ∈ (ℤ‘2) ∧ 𝐴 ∈ (ℤ‘2) ∧ 𝐵 ∈ ℕ0) → (𝐺𝐴) ∥ ((𝐺 Yrm 𝐵) − (𝐴 Yrm 𝐵)))
27582, 2, 90, 274syl3anc 1477 . . . . . . 7 (𝜑 → (𝐺𝐴) ∥ ((𝐺 Yrm 𝐵) − (𝐴 Yrm 𝐵)))
27685a1i 11 . . . . . . . 8 (𝜑𝐻 = (𝐺 Yrm 𝐵))
277276, 12oveq12d 6833 . . . . . . 7 (𝜑 → (𝐻𝐶) = ((𝐺 Yrm 𝐵) − (𝐴 Yrm 𝐵)))
278275, 277breqtrrd 4833 . . . . . 6 (𝜑 → (𝐺𝐴) ∥ (𝐻𝐶))
279 eluzelz 11910 . . . . . . . . 9 (𝐺 ∈ (ℤ‘2) → 𝐺 ∈ ℤ)
28082, 279syl 17 . . . . . . . 8 (𝜑𝐺 ∈ ℤ)
281280, 215zsubcld 11700 . . . . . . 7 (𝜑 → (𝐺𝐴) ∈ ℤ)
28285, 87syl5eqel 2844 . . . . . . . 8 (𝜑𝐻 ∈ ℤ)
283282, 14zsubcld 11700 . . . . . . 7 (𝜑 → (𝐻𝐶) ∈ ℤ)
284 dvdstr 15241 . . . . . . 7 ((𝐹 ∈ ℤ ∧ (𝐺𝐴) ∈ ℤ ∧ (𝐻𝐶) ∈ ℤ) → ((𝐹 ∥ (𝐺𝐴) ∧ (𝐺𝐴) ∥ (𝐻𝐶)) → 𝐹 ∥ (𝐻𝐶)))
285196, 281, 283, 284syl3anc 1477 . . . . . 6 (𝜑 → ((𝐹 ∥ (𝐺𝐴) ∧ (𝐺𝐴) ∥ (𝐻𝐶)) → 𝐹 ∥ (𝐻𝐶)))
286210, 278, 285mp2and 717 . . . . 5 (𝜑𝐹 ∥ (𝐻𝐶))
287 jm2.16nn0 38092 . . . . . . . . 9 ((𝐺 ∈ (ℤ‘2) ∧ 𝐵 ∈ ℕ0) → (𝐺 − 1) ∥ ((𝐺 Yrm 𝐵) − 𝐵))
28882, 90, 287syl2anc 696 . . . . . . . 8 (𝜑 → (𝐺 − 1) ∥ ((𝐺 Yrm 𝐵) − 𝐵))
28985oveq1i 6825 . . . . . . . 8 (𝐻𝐵) = ((𝐺 Yrm 𝐵) − 𝐵)
290288, 289syl6breqr 4847 . . . . . . 7 (𝜑 → (𝐺 − 1) ∥ (𝐻𝐵))
291 peano2zm 11633 . . . . . . . . 9 (𝐺 ∈ ℤ → (𝐺 − 1) ∈ ℤ)
292280, 291syl 17 . . . . . . . 8 (𝜑 → (𝐺 − 1) ∈ ℤ)
293282, 4zsubcld 11700 . . . . . . . 8 (𝜑 → (𝐻𝐵) ∈ ℤ)
294 dvdstr 15241 . . . . . . . 8 (((2 · 𝐶) ∈ ℤ ∧ (𝐺 − 1) ∈ ℤ ∧ (𝐻𝐵) ∈ ℤ) → (((2 · 𝐶) ∥ (𝐺 − 1) ∧ (𝐺 − 1) ∥ (𝐻𝐵)) → (2 · 𝐶) ∥ (𝐻𝐵)))
295213, 292, 293, 294syl3anc 1477 . . . . . . 7 (𝜑 → (((2 · 𝐶) ∥ (𝐺 − 1) ∧ (𝐺 − 1) ∥ (𝐻𝐵)) → (2 · 𝐶) ∥ (𝐻𝐵)))
296273, 290, 295mp2and 717 . . . . . 6 (𝜑 → (2 · 𝐶) ∥ (𝐻𝐵))
297 rmygeid 38052 . . . . . . . 8 ((𝐴 ∈ (ℤ‘2) ∧ 𝐵 ∈ ℕ0) → 𝐵 ≤ (𝐴 Yrm 𝐵))
2982, 90, 297syl2anc 696 . . . . . . 7 (𝜑𝐵 ≤ (𝐴 Yrm 𝐵))
299298, 12breqtrrd 4833 . . . . . 6 (𝜑𝐵𝐶)
300296, 299jca 555 . . . . 5 (𝜑 → ((2 · 𝐶) ∥ (𝐻𝐵) ∧ 𝐵𝐶))
301273, 286, 300jca31 558 . . . 4 (𝜑 → (((2 · 𝐶) ∥ (𝐺 − 1) ∧ 𝐹 ∥ (𝐻𝐶)) ∧ ((2 · 𝐶) ∥ (𝐻𝐵) ∧ 𝐵𝐶)))
302175, 211, 301jca31 558 . . 3 (𝜑 → (((((𝐷↑2) − (((𝐴↑2) − 1) · (𝐶↑2))) = 1 ∧ ((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = 1 ∧ 𝐺 ∈ (ℤ‘2)) ∧ (((𝐼↑2) − (((𝐺↑2) − 1) · (𝐻↑2))) = 1 ∧ 𝐸 = ((𝐽 + 1) · (2 · (𝐶↑2))) ∧ 𝐹 ∥ (𝐺𝐴))) ∧ (((2 · 𝐶) ∥ (𝐺 − 1) ∧ 𝐹 ∥ (𝐻𝐶)) ∧ ((2 · 𝐶) ∥ (𝐻𝐵) ∧ 𝐵𝐶))))
303160, 302jca 555 . 2 (𝜑 → (𝐽 ∈ ℕ0 ∧ (((((𝐷↑2) − (((𝐴↑2) − 1) · (𝐶↑2))) = 1 ∧ ((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = 1 ∧ 𝐺 ∈ (ℤ‘2)) ∧ (((𝐼↑2) − (((𝐺↑2) − 1) · (𝐻↑2))) = 1 ∧ 𝐸 = ((𝐽 + 1) · (2 · (𝐶↑2))) ∧ 𝐹 ∥ (𝐺𝐴))) ∧ (((2 · 𝐶) ∥ (𝐺 − 1) ∧ 𝐹 ∥ (𝐻𝐶)) ∧ ((2 · 𝐶) ∥ (𝐻𝐵) ∧ 𝐵𝐶)))))
30445, 103, 303jca31 558 1 (𝜑 → (((𝐷 ∈ ℕ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 · 𝐶) ∥ (𝐻𝐵) ∧ 𝐵𝐶))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1632  wcel 2140   class class class wbr 4805  cfv 6050  (class class class)co 6815  cc 10147  0cc0 10149  1c1 10150   + caddc 10152   · cmul 10154   < clt 10287  cle 10288  cmin 10479   / cdiv 10897  cn 11233  2c2 11283  0cn0 11505  cz 11590  cuz 11900  cexp 13075  cdvds 15203   Xrm crmx 37985   Yrm crmy 37986
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2142  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-rep 4924  ax-sep 4934  ax-nul 4942  ax-pow 4993  ax-pr 5056  ax-un 7116  ax-inf2 8714  ax-cnex 10205  ax-resscn 10206  ax-1cn 10207  ax-icn 10208  ax-addcl 10209  ax-addrcl 10210  ax-mulcl 10211  ax-mulrcl 10212  ax-mulcom 10213  ax-addass 10214  ax-mulass 10215  ax-distr 10216  ax-i2m1 10217  ax-1ne0 10218  ax-1rid 10219  ax-rnegex 10220  ax-rrecex 10221  ax-cnre 10222  ax-pre-lttri 10223  ax-pre-lttrn 10224  ax-pre-ltadd 10225  ax-pre-mulgt0 10226  ax-pre-sup 10227  ax-addf 10228  ax-mulf 10229
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-nel 3037  df-ral 3056  df-rex 3057  df-reu 3058  df-rmo 3059  df-rab 3060  df-v 3343  df-sbc 3578  df-csb 3676  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-pss 3732  df-nul 4060  df-if 4232  df-pw 4305  df-sn 4323  df-pr 4325  df-tp 4327  df-op 4329  df-uni 4590  df-int 4629  df-iun 4675  df-iin 4676  df-br 4806  df-opab 4866  df-mpt 4883  df-tr 4906  df-id 5175  df-eprel 5180  df-po 5188  df-so 5189  df-fr 5226  df-se 5227  df-we 5228  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-pred 5842  df-ord 5888  df-on 5889  df-lim 5890  df-suc 5891  df-iota 6013  df-fun 6052  df-fn 6053  df-f 6054  df-f1 6055  df-fo 6056  df-f1o 6057  df-fv 6058  df-isom 6059  df-riota 6776  df-ov 6818  df-oprab 6819  df-mpt2 6820  df-of 7064  df-om 7233  df-1st 7335  df-2nd 7336  df-supp 7466  df-wrecs 7578  df-recs 7639  df-rdg 7677  df-1o 7731  df-2o 7732  df-oadd 7735  df-omul 7736  df-er 7914  df-map 8028  df-pm 8029  df-ixp 8078  df-en 8125  df-dom 8126  df-sdom 8127  df-fin 8128  df-fsupp 8444  df-fi 8485  df-sup 8516  df-inf 8517  df-oi 8583  df-card 8976  df-acn 8979  df-cda 9203  df-pnf 10289  df-mnf 10290  df-xr 10291  df-ltxr 10292  df-le 10293  df-sub 10481  df-neg 10482  df-div 10898  df-nn 11234  df-2 11292  df-3 11293  df-4 11294  df-5 11295  df-6 11296  df-7 11297  df-8 11298  df-9 11299  df-n0 11506  df-xnn0 11577  df-z 11591  df-dec 11707  df-uz 11901  df-q 12003  df-rp 12047  df-xneg 12160  df-xadd 12161  df-xmul 12162  df-ioo 12393  df-ioc 12394  df-ico 12395  df-icc 12396  df-fz 12541  df-fzo 12681  df-fl 12808  df-mod 12884  df-seq 13017  df-exp 13076  df-fac 13276  df-bc 13305  df-hash 13333  df-shft 14027  df-cj 14059  df-re 14060  df-im 14061  df-sqrt 14195  df-abs 14196  df-limsup 14422  df-clim 14439  df-rlim 14440  df-sum 14637  df-ef 15018  df-sin 15020  df-cos 15021  df-pi 15023  df-dvds 15204  df-gcd 15440  df-prm 15609  df-numer 15666  df-denom 15667  df-struct 16082  df-ndx 16083  df-slot 16084  df-base 16086  df-sets 16087  df-ress 16088  df-plusg 16177  df-mulr 16178  df-starv 16179  df-sca 16180  df-vsca 16181  df-ip 16182  df-tset 16183  df-ple 16184  df-ds 16187  df-unif 16188  df-hom 16189  df-cco 16190  df-rest 16306  df-topn 16307  df-0g 16325  df-gsum 16326  df-topgen 16327  df-pt 16328  df-prds 16331  df-xrs 16385  df-qtop 16390  df-imas 16391  df-xps 16393  df-mre 16469  df-mrc 16470  df-acs 16472  df-mgm 17464  df-sgrp 17506  df-mnd 17517  df-submnd 17558  df-mulg 17763  df-cntz 17971  df-cmn 18416  df-psmet 19961  df-xmet 19962  df-met 19963  df-bl 19964  df-mopn 19965  df-fbas 19966  df-fg 19967  df-cnfld 19970  df-top 20922  df-topon 20939  df-topsp 20960  df-bases 20973  df-cld 21046  df-ntr 21047  df-cls 21048  df-nei 21125  df-lp 21163  df-perf 21164  df-cn 21254  df-cnp 21255  df-haus 21342  df-tx 21588  df-hmeo 21781  df-fil 21872  df-fm 21964  df-flim 21965  df-flf 21966  df-xms 22347  df-ms 22348  df-tms 22349  df-cncf 22903  df-limc 23850  df-dv 23851  df-log 24524  df-squarenn 37926  df-pell1qr 37927  df-pell14qr 37928  df-pell1234qr 37929  df-pellfund 37930  df-rmx 37987  df-rmy 37988
This theorem is referenced by:  jm2.27  38096
  Copyright terms: Public domain W3C validator