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 38525
Description: Lemma for jm2.27 38526. 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 11833 . . . . 5 (𝜑𝐵 ∈ ℤ)
5 frmx 38429 . . . . . 6 Xrm :((ℤ‘2) × ℤ)⟶ℕ0
65fovcl 7042 . . . . 5 ((𝐴 ∈ (ℤ‘2) ∧ 𝐵 ∈ ℤ) → (𝐴 Xrm 𝐵) ∈ ℕ0)
72, 4, 6syl2anc 579 . . . 4 (𝜑 → (𝐴 Xrm 𝐵) ∈ ℕ0)
81, 7syl5eqel 2862 . . 3 (𝜑𝐷 ∈ ℕ0)
9 jm2.27c7 . . . 4 𝐸 = (𝐴 Yrm (2 · 𝑄))
10 2z 11761 . . . . . . 7 2 ∈ ℤ
11 jm2.27c6 . . . . . . . 8 𝑄 = (𝐵 · (𝐴 Yrm 𝐵))
12 jm2.27c4 . . . . . . . . . 10 (𝜑𝐶 = (𝐴 Yrm 𝐵))
13 jm2.27a3 . . . . . . . . . . 11 (𝜑𝐶 ∈ ℕ)
1413nnzd 11833 . . . . . . . . . 10 (𝜑𝐶 ∈ ℤ)
1512, 14eqeltrrd 2859 . . . . . . . . 9 (𝜑 → (𝐴 Yrm 𝐵) ∈ ℤ)
164, 15zmulcld 11840 . . . . . . . 8 (𝜑 → (𝐵 · (𝐴 Yrm 𝐵)) ∈ ℤ)
1711, 16syl5eqel 2862 . . . . . . 7 (𝜑𝑄 ∈ ℤ)
18 zmulcl 11778 . . . . . . 7 ((2 ∈ ℤ ∧ 𝑄 ∈ ℤ) → (2 · 𝑄) ∈ ℤ)
1910, 17, 18sylancr 581 . . . . . 6 (𝜑 → (2 · 𝑄) ∈ ℤ)
20 frmy 38430 . . . . . . 7 Yrm :((ℤ‘2) × ℤ)⟶ℤ
2120fovcl 7042 . . . . . 6 ((𝐴 ∈ (ℤ‘2) ∧ (2 · 𝑄) ∈ ℤ) → (𝐴 Yrm (2 · 𝑄)) ∈ ℤ)
222, 19, 21syl2anc 579 . . . . 5 (𝜑 → (𝐴 Yrm (2 · 𝑄)) ∈ ℤ)
23 rmy0 38445 . . . . . . 7 (𝐴 ∈ (ℤ‘2) → (𝐴 Yrm 0) = 0)
242, 23syl 17 . . . . . 6 (𝜑 → (𝐴 Yrm 0) = 0)
25 2nn 11448 . . . . . . . . . 10 2 ∈ ℕ
2612, 13eqeltrrd 2859 . . . . . . . . . . . 12 (𝜑 → (𝐴 Yrm 𝐵) ∈ ℕ)
273, 26nnmulcld 11428 . . . . . . . . . . 11 (𝜑 → (𝐵 · (𝐴 Yrm 𝐵)) ∈ ℕ)
2811, 27syl5eqel 2862 . . . . . . . . . 10 (𝜑𝑄 ∈ ℕ)
29 nnmulcl 11399 . . . . . . . . . 10 ((2 ∈ ℕ ∧ 𝑄 ∈ ℕ) → (2 · 𝑄) ∈ ℕ)
3025, 28, 29sylancr 581 . . . . . . . . 9 (𝜑 → (2 · 𝑄) ∈ ℕ)
3130nnnn0d 11702 . . . . . . . 8 (𝜑 → (2 · 𝑄) ∈ ℕ0)
3231nn0ge0d 11705 . . . . . . 7 (𝜑 → 0 ≤ (2 · 𝑄))
33 0zd 11740 . . . . . . . 8 (𝜑 → 0 ∈ ℤ)
34 lermy 38473 . . . . . . . 8 ((𝐴 ∈ (ℤ‘2) ∧ 0 ∈ ℤ ∧ (2 · 𝑄) ∈ ℤ) → (0 ≤ (2 · 𝑄) ↔ (𝐴 Yrm 0) ≤ (𝐴 Yrm (2 · 𝑄))))
352, 33, 19, 34syl3anc 1439 . . . . . . 7 (𝜑 → (0 ≤ (2 · 𝑄) ↔ (𝐴 Yrm 0) ≤ (𝐴 Yrm (2 · 𝑄))))
3632, 35mpbid 224 . . . . . 6 (𝜑 → (𝐴 Yrm 0) ≤ (𝐴 Yrm (2 · 𝑄)))
3724, 36eqbrtrrd 4910 . . . . 5 (𝜑 → 0 ≤ (𝐴 Yrm (2 · 𝑄)))
38 elnn0z 11741 . . . . 5 ((𝐴 Yrm (2 · 𝑄)) ∈ ℕ0 ↔ ((𝐴 Yrm (2 · 𝑄)) ∈ ℤ ∧ 0 ≤ (𝐴 Yrm (2 · 𝑄))))
3922, 37, 38sylanbrc 578 . . . 4 (𝜑 → (𝐴 Yrm (2 · 𝑄)) ∈ ℕ0)
409, 39syl5eqel 2862 . . 3 (𝜑𝐸 ∈ ℕ0)
41 jm2.27c8 . . . 4 𝐹 = (𝐴 Xrm (2 · 𝑄))
425fovcl 7042 . . . . 5 ((𝐴 ∈ (ℤ‘2) ∧ (2 · 𝑄) ∈ ℤ) → (𝐴 Xrm (2 · 𝑄)) ∈ ℕ0)
432, 19, 42syl2anc 579 . . . 4 (𝜑 → (𝐴 Xrm (2 · 𝑄)) ∈ ℕ0)
4441, 43syl5eqel 2862 . . 3 (𝜑𝐹 ∈ ℕ0)
458, 40, 443jca 1119 . 2 (𝜑 → (𝐷 ∈ ℕ0𝐸 ∈ ℕ0𝐹 ∈ ℕ0))
46 2nn0 11661 . . . 4 2 ∈ ℕ0
47 jm2.27c9 . . . . 5 𝐺 = (𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴)))
4844nn0cnd 11704 . . . . . . . . 9 (𝜑𝐹 ∈ ℂ)
4948sqvald 13324 . . . . . . . 8 (𝜑 → (𝐹↑2) = (𝐹 · 𝐹))
5044, 44nn0mulcld 11707 . . . . . . . 8 (𝜑 → (𝐹 · 𝐹) ∈ ℕ0)
5149, 50eqeltrd 2858 . . . . . . 7 (𝜑 → (𝐹↑2) ∈ ℕ0)
52 eluz2nn 12032 . . . . . . . . . . . . 13 (𝐴 ∈ (ℤ‘2) → 𝐴 ∈ ℕ)
532, 52syl 17 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℕ)
5453nnnn0d 11702 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℕ0)
5554nn0red 11703 . . . . . . . . . 10 (𝜑𝐴 ∈ ℝ)
5644nn0red 11703 . . . . . . . . . 10 (𝜑𝐹 ∈ ℝ)
5756, 56remulcld 10407 . . . . . . . . . 10 (𝜑 → (𝐹 · 𝐹) ∈ ℝ)
58 rmx1 38442 . . . . . . . . . . . . 13 (𝐴 ∈ (ℤ‘2) → (𝐴 Xrm 1) = 𝐴)
592, 58syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐴 Xrm 1) = 𝐴)
6030nnge1d 11423 . . . . . . . . . . . . 13 (𝜑 → 1 ≤ (2 · 𝑄))
61 1nn0 11660 . . . . . . . . . . . . . . 15 1 ∈ ℕ0
6261a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ ℕ0)
63 lermxnn0 38468 . . . . . . . . . . . . . 14 ((𝐴 ∈ (ℤ‘2) ∧ 1 ∈ ℕ0 ∧ (2 · 𝑄) ∈ ℕ0) → (1 ≤ (2 · 𝑄) ↔ (𝐴 Xrm 1) ≤ (𝐴 Xrm (2 · 𝑄))))
642, 62, 31, 63syl3anc 1439 . . . . . . . . . . . . 13 (𝜑 → (1 ≤ (2 · 𝑄) ↔ (𝐴 Xrm 1) ≤ (𝐴 Xrm (2 · 𝑄))))
6560, 64mpbid 224 . . . . . . . . . . . 12 (𝜑 → (𝐴 Xrm 1) ≤ (𝐴 Xrm (2 · 𝑄)))
6659, 65eqbrtrrd 4910 . . . . . . . . . . 11 (𝜑𝐴 ≤ (𝐴 Xrm (2 · 𝑄)))
6766, 41syl6breqr 4928 . . . . . . . . . 10 (𝜑𝐴𝐹)
6844nn0ge0d 11705 . . . . . . . . . . 11 (𝜑 → 0 ≤ 𝐹)
69 rmxnn 38469 . . . . . . . . . . . . . 14 ((𝐴 ∈ (ℤ‘2) ∧ (2 · 𝑄) ∈ ℤ) → (𝐴 Xrm (2 · 𝑄)) ∈ ℕ)
702, 19, 69syl2anc 579 . . . . . . . . . . . . 13 (𝜑 → (𝐴 Xrm (2 · 𝑄)) ∈ ℕ)
7141, 70syl5eqel 2862 . . . . . . . . . . . 12 (𝜑𝐹 ∈ ℕ)
7271nnge1d 11423 . . . . . . . . . . 11 (𝜑 → 1 ≤ 𝐹)
7356, 56, 68, 72lemulge12d 11316 . . . . . . . . . 10 (𝜑𝐹 ≤ (𝐹 · 𝐹))
7455, 56, 57, 67, 73letrd 10533 . . . . . . . . 9 (𝜑𝐴 ≤ (𝐹 · 𝐹))
7574, 49breqtrrd 4914 . . . . . . . 8 (𝜑𝐴 ≤ (𝐹↑2))
76 nn0sub 11694 . . . . . . . . 9 ((𝐴 ∈ ℕ0 ∧ (𝐹↑2) ∈ ℕ0) → (𝐴 ≤ (𝐹↑2) ↔ ((𝐹↑2) − 𝐴) ∈ ℕ0))
7754, 51, 76syl2anc 579 . . . . . . . 8 (𝜑 → (𝐴 ≤ (𝐹↑2) ↔ ((𝐹↑2) − 𝐴) ∈ ℕ0))
7875, 77mpbid 224 . . . . . . 7 (𝜑 → ((𝐹↑2) − 𝐴) ∈ ℕ0)
7951, 78nn0mulcld 11707 . . . . . 6 (𝜑 → ((𝐹↑2) · ((𝐹↑2) − 𝐴)) ∈ ℕ0)
80 uzaddcl 12050 . . . . . 6 ((𝐴 ∈ (ℤ‘2) ∧ ((𝐹↑2) · ((𝐹↑2) − 𝐴)) ∈ ℕ0) → (𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) ∈ (ℤ‘2))
812, 79, 80syl2anc 579 . . . . 5 (𝜑 → (𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) ∈ (ℤ‘2))
8247, 81syl5eqel 2862 . . . 4 (𝜑𝐺 ∈ (ℤ‘2))
83 eluznn0 12064 . . . 4 ((2 ∈ ℕ0𝐺 ∈ (ℤ‘2)) → 𝐺 ∈ ℕ0)
8446, 82, 83sylancr 581 . . 3 (𝜑𝐺 ∈ ℕ0)
85 jm2.27c10 . . . 4 𝐻 = (𝐺 Yrm 𝐵)
8620fovcl 7042 . . . . . 6 ((𝐺 ∈ (ℤ‘2) ∧ 𝐵 ∈ ℤ) → (𝐺 Yrm 𝐵) ∈ ℤ)
8782, 4, 86syl2anc 579 . . . . 5 (𝜑 → (𝐺 Yrm 𝐵) ∈ ℤ)
88 rmy0 38445 . . . . . . 7 (𝐺 ∈ (ℤ‘2) → (𝐺 Yrm 0) = 0)
8982, 88syl 17 . . . . . 6 (𝜑 → (𝐺 Yrm 0) = 0)
903nnnn0d 11702 . . . . . . . 8 (𝜑𝐵 ∈ ℕ0)
9190nn0ge0d 11705 . . . . . . 7 (𝜑 → 0 ≤ 𝐵)
92 lermy 38473 . . . . . . . 8 ((𝐺 ∈ (ℤ‘2) ∧ 0 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (0 ≤ 𝐵 ↔ (𝐺 Yrm 0) ≤ (𝐺 Yrm 𝐵)))
9382, 33, 4, 92syl3anc 1439 . . . . . . 7 (𝜑 → (0 ≤ 𝐵 ↔ (𝐺 Yrm 0) ≤ (𝐺 Yrm 𝐵)))
9491, 93mpbid 224 . . . . . 6 (𝜑 → (𝐺 Yrm 0) ≤ (𝐺 Yrm 𝐵))
9589, 94eqbrtrrd 4910 . . . . 5 (𝜑 → 0 ≤ (𝐺 Yrm 𝐵))
96 elnn0z 11741 . . . . 5 ((𝐺 Yrm 𝐵) ∈ ℕ0 ↔ ((𝐺 Yrm 𝐵) ∈ ℤ ∧ 0 ≤ (𝐺 Yrm 𝐵)))
9787, 95, 96sylanbrc 578 . . . 4 (𝜑 → (𝐺 Yrm 𝐵) ∈ ℕ0)
9885, 97syl5eqel 2862 . . 3 (𝜑𝐻 ∈ ℕ0)
99 jm2.27c11 . . . 4 𝐼 = (𝐺 Xrm 𝐵)
1005fovcl 7042 . . . . 5 ((𝐺 ∈ (ℤ‘2) ∧ 𝐵 ∈ ℤ) → (𝐺 Xrm 𝐵) ∈ ℕ0)
10182, 4, 100syl2anc 579 . . . 4 (𝜑 → (𝐺 Xrm 𝐵) ∈ ℕ0)
10299, 101syl5eqel 2862 . . 3 (𝜑𝐼 ∈ ℕ0)
10384, 98, 1023jca 1119 . 2 (𝜑 → (𝐺 ∈ ℕ0𝐻 ∈ ℕ0𝐼 ∈ ℕ0))
104 jm2.27c12 . . . 4 𝐽 = ((𝐸 / (2 · (𝐶↑2))) − 1)
105 iddvds 15402 . . . . . . . . . . . 12 ((𝐵 · (𝐴 Yrm 𝐵)) ∈ ℤ → (𝐵 · (𝐴 Yrm 𝐵)) ∥ (𝐵 · (𝐴 Yrm 𝐵)))
10616, 105syl 17 . . . . . . . . . . 11 (𝜑 → (𝐵 · (𝐴 Yrm 𝐵)) ∥ (𝐵 · (𝐴 Yrm 𝐵)))
107106, 11syl6breqr 4928 . . . . . . . . . 10 (𝜑 → (𝐵 · (𝐴 Yrm 𝐵)) ∥ 𝑄)
108 jm2.20nn 38515 . . . . . . . . . . 11 ((𝐴 ∈ (ℤ‘2) ∧ 𝑄 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (((𝐴 Yrm 𝐵)↑2) ∥ (𝐴 Yrm 𝑄) ↔ (𝐵 · (𝐴 Yrm 𝐵)) ∥ 𝑄))
1092, 28, 3, 108syl3anc 1439 . . . . . . . . . 10 (𝜑 → (((𝐴 Yrm 𝐵)↑2) ∥ (𝐴 Yrm 𝑄) ↔ (𝐵 · (𝐴 Yrm 𝐵)) ∥ 𝑄))
110107, 109mpbird 249 . . . . . . . . 9 (𝜑 → ((𝐴 Yrm 𝐵)↑2) ∥ (𝐴 Yrm 𝑄))
111 zsqcl 13253 . . . . . . . . . . 11 ((𝐴 Yrm 𝐵) ∈ ℤ → ((𝐴 Yrm 𝐵)↑2) ∈ ℤ)
11215, 111syl 17 . . . . . . . . . 10 (𝜑 → ((𝐴 Yrm 𝐵)↑2) ∈ ℤ)
11320fovcl 7042 . . . . . . . . . . 11 ((𝐴 ∈ (ℤ‘2) ∧ 𝑄 ∈ ℤ) → (𝐴 Yrm 𝑄) ∈ ℤ)
1142, 17, 113syl2anc 579 . . . . . . . . . 10 (𝜑 → (𝐴 Yrm 𝑄) ∈ ℤ)
11510a1i 11 . . . . . . . . . 10 (𝜑 → 2 ∈ ℤ)
116 dvdscmul 15415 . . . . . . . . . 10 ((((𝐴 Yrm 𝐵)↑2) ∈ ℤ ∧ (𝐴 Yrm 𝑄) ∈ ℤ ∧ 2 ∈ ℤ) → (((𝐴 Yrm 𝐵)↑2) ∥ (𝐴 Yrm 𝑄) → (2 · ((𝐴 Yrm 𝐵)↑2)) ∥ (2 · (𝐴 Yrm 𝑄))))
117112, 114, 115, 116syl3anc 1439 . . . . . . . . 9 (𝜑 → (((𝐴 Yrm 𝐵)↑2) ∥ (𝐴 Yrm 𝑄) → (2 · ((𝐴 Yrm 𝐵)↑2)) ∥ (2 · (𝐴 Yrm 𝑄))))
118110, 117mpd 15 . . . . . . . 8 (𝜑 → (2 · ((𝐴 Yrm 𝐵)↑2)) ∥ (2 · (𝐴 Yrm 𝑄)))
119 zmulcl 11778 . . . . . . . . . . 11 ((2 ∈ ℤ ∧ (𝐴 Yrm 𝑄) ∈ ℤ) → (2 · (𝐴 Yrm 𝑄)) ∈ ℤ)
12010, 114, 119sylancr 581 . . . . . . . . . 10 (𝜑 → (2 · (𝐴 Yrm 𝑄)) ∈ ℤ)
1215fovcl 7042 . . . . . . . . . . . 12 ((𝐴 ∈ (ℤ‘2) ∧ 𝑄 ∈ ℤ) → (𝐴 Xrm 𝑄) ∈ ℕ0)
1222, 17, 121syl2anc 579 . . . . . . . . . . 11 (𝜑 → (𝐴 Xrm 𝑄) ∈ ℕ0)
123122nn0zd 11832 . . . . . . . . . 10 (𝜑 → (𝐴 Xrm 𝑄) ∈ ℤ)
124 dvdsmul1 15410 . . . . . . . . . 10 (((2 · (𝐴 Yrm 𝑄)) ∈ ℤ ∧ (𝐴 Xrm 𝑄) ∈ ℤ) → (2 · (𝐴 Yrm 𝑄)) ∥ ((2 · (𝐴 Yrm 𝑄)) · (𝐴 Xrm 𝑄)))
125120, 123, 124syl2anc 579 . . . . . . . . 9 (𝜑 → (2 · (𝐴 Yrm 𝑄)) ∥ ((2 · (𝐴 Yrm 𝑄)) · (𝐴 Xrm 𝑄)))
126 rmydbl 38456 . . . . . . . . . . 11 ((𝐴 ∈ (ℤ‘2) ∧ 𝑄 ∈ ℤ) → (𝐴 Yrm (2 · 𝑄)) = ((2 · (𝐴 Xrm 𝑄)) · (𝐴 Yrm 𝑄)))
1272, 17, 126syl2anc 579 . . . . . . . . . 10 (𝜑 → (𝐴 Yrm (2 · 𝑄)) = ((2 · (𝐴 Xrm 𝑄)) · (𝐴 Yrm 𝑄)))
128 2cnd 11453 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℂ)
129122nn0cnd 11704 . . . . . . . . . . 11 (𝜑 → (𝐴 Xrm 𝑄) ∈ ℂ)
130114zcnd 11835 . . . . . . . . . . 11 (𝜑 → (𝐴 Yrm 𝑄) ∈ ℂ)
131128, 129, 130mul32d 10586 . . . . . . . . . 10 (𝜑 → ((2 · (𝐴 Xrm 𝑄)) · (𝐴 Yrm 𝑄)) = ((2 · (𝐴 Yrm 𝑄)) · (𝐴 Xrm 𝑄)))
132127, 131eqtrd 2813 . . . . . . . . 9 (𝜑 → (𝐴 Yrm (2 · 𝑄)) = ((2 · (𝐴 Yrm 𝑄)) · (𝐴 Xrm 𝑄)))
133125, 132breqtrrd 4914 . . . . . . . 8 (𝜑 → (2 · (𝐴 Yrm 𝑄)) ∥ (𝐴 Yrm (2 · 𝑄)))
134 zmulcl 11778 . . . . . . . . . 10 ((2 ∈ ℤ ∧ ((𝐴 Yrm 𝐵)↑2) ∈ ℤ) → (2 · ((𝐴 Yrm 𝐵)↑2)) ∈ ℤ)
13510, 112, 134sylancr 581 . . . . . . . . 9 (𝜑 → (2 · ((𝐴 Yrm 𝐵)↑2)) ∈ ℤ)
136 dvdstr 15425 . . . . . . . . 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 1439 . . . . . . . 8 (𝜑 → (((2 · ((𝐴 Yrm 𝐵)↑2)) ∥ (2 · (𝐴 Yrm 𝑄)) ∧ (2 · (𝐴 Yrm 𝑄)) ∥ (𝐴 Yrm (2 · 𝑄))) → (2 · ((𝐴 Yrm 𝐵)↑2)) ∥ (𝐴 Yrm (2 · 𝑄))))
138118, 133, 137mp2and 689 . . . . . . 7 (𝜑 → (2 · ((𝐴 Yrm 𝐵)↑2)) ∥ (𝐴 Yrm (2 · 𝑄)))
13912oveq1d 6937 . . . . . . . 8 (𝜑 → (𝐶↑2) = ((𝐴 Yrm 𝐵)↑2))
140139oveq2d 6938 . . . . . . 7 (𝜑 → (2 · (𝐶↑2)) = (2 · ((𝐴 Yrm 𝐵)↑2)))
1419a1i 11 . . . . . . 7 (𝜑𝐸 = (𝐴 Yrm (2 · 𝑄)))
142138, 140, 1413brtr4d 4918 . . . . . 6 (𝜑 → (2 · (𝐶↑2)) ∥ 𝐸)
1439, 22syl5eqel 2862 . . . . . . . 8 (𝜑𝐸 ∈ ℤ)
14430nngt0d 11424 . . . . . . . . . 10 (𝜑 → 0 < (2 · 𝑄))
145 ltrmy 38470 . . . . . . . . . . 11 ((𝐴 ∈ (ℤ‘2) ∧ 0 ∈ ℤ ∧ (2 · 𝑄) ∈ ℤ) → (0 < (2 · 𝑄) ↔ (𝐴 Yrm 0) < (𝐴 Yrm (2 · 𝑄))))
1462, 33, 19, 145syl3anc 1439 . . . . . . . . . 10 (𝜑 → (0 < (2 · 𝑄) ↔ (𝐴 Yrm 0) < (𝐴 Yrm (2 · 𝑄))))
147144, 146mpbid 224 . . . . . . . . 9 (𝜑 → (𝐴 Yrm 0) < (𝐴 Yrm (2 · 𝑄)))
14824eqcomd 2783 . . . . . . . . 9 (𝜑 → 0 = (𝐴 Yrm 0))
149147, 148, 1413brtr4d 4918 . . . . . . . 8 (𝜑 → 0 < 𝐸)
150 elnnz 11738 . . . . . . . 8 (𝐸 ∈ ℕ ↔ (𝐸 ∈ ℤ ∧ 0 < 𝐸))
151143, 149, 150sylanbrc 578 . . . . . . 7 (𝜑𝐸 ∈ ℕ)
15213nnsqcld 13350 . . . . . . . 8 (𝜑 → (𝐶↑2) ∈ ℕ)
153 nnmulcl 11399 . . . . . . . 8 ((2 ∈ ℕ ∧ (𝐶↑2) ∈ ℕ) → (2 · (𝐶↑2)) ∈ ℕ)
15425, 152, 153sylancr 581 . . . . . . 7 (𝜑 → (2 · (𝐶↑2)) ∈ ℕ)
155 nndivdvds 15396 . . . . . . 7 ((𝐸 ∈ ℕ ∧ (2 · (𝐶↑2)) ∈ ℕ) → ((2 · (𝐶↑2)) ∥ 𝐸 ↔ (𝐸 / (2 · (𝐶↑2))) ∈ ℕ))
156151, 154, 155syl2anc 579 . . . . . 6 (𝜑 → ((2 · (𝐶↑2)) ∥ 𝐸 ↔ (𝐸 / (2 · (𝐶↑2))) ∈ ℕ))
157142, 156mpbid 224 . . . . 5 (𝜑 → (𝐸 / (2 · (𝐶↑2))) ∈ ℕ)
158 nnm1nn0 11685 . . . . 5 ((𝐸 / (2 · (𝐶↑2))) ∈ ℕ → ((𝐸 / (2 · (𝐶↑2))) − 1) ∈ ℕ0)
159157, 158syl 17 . . . 4 (𝜑 → ((𝐸 / (2 · (𝐶↑2))) − 1) ∈ ℕ0)
160104, 159syl5eqel 2862 . . 3 (𝜑𝐽 ∈ ℕ0)
1611oveq1i 6932 . . . . . . . 8 (𝐷↑2) = ((𝐴 Xrm 𝐵)↑2)
162161a1i 11 . . . . . . 7 (𝜑 → (𝐷↑2) = ((𝐴 Xrm 𝐵)↑2))
163139oveq2d 6938 . . . . . . 7 (𝜑 → (((𝐴↑2) − 1) · (𝐶↑2)) = (((𝐴↑2) − 1) · ((𝐴 Yrm 𝐵)↑2)))
164162, 163oveq12d 6940 . . . . . 6 (𝜑 → ((𝐷↑2) − (((𝐴↑2) − 1) · (𝐶↑2))) = (((𝐴 Xrm 𝐵)↑2) − (((𝐴↑2) − 1) · ((𝐴 Yrm 𝐵)↑2))))
165 rmxynorm 38434 . . . . . . 7 ((𝐴 ∈ (ℤ‘2) ∧ 𝐵 ∈ ℤ) → (((𝐴 Xrm 𝐵)↑2) − (((𝐴↑2) − 1) · ((𝐴 Yrm 𝐵)↑2))) = 1)
1662, 4, 165syl2anc 579 . . . . . 6 (𝜑 → (((𝐴 Xrm 𝐵)↑2) − (((𝐴↑2) − 1) · ((𝐴 Yrm 𝐵)↑2))) = 1)
167164, 166eqtrd 2813 . . . . 5 (𝜑 → ((𝐷↑2) − (((𝐴↑2) − 1) · (𝐶↑2))) = 1)
16841oveq1i 6932 . . . . . . 7 (𝐹↑2) = ((𝐴 Xrm (2 · 𝑄))↑2)
1699oveq1i 6932 . . . . . . . 8 (𝐸↑2) = ((𝐴 Yrm (2 · 𝑄))↑2)
170169oveq2i 6933 . . . . . . 7 (((𝐴↑2) − 1) · (𝐸↑2)) = (((𝐴↑2) − 1) · ((𝐴 Yrm (2 · 𝑄))↑2))
171168, 170oveq12i 6934 . . . . . 6 ((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = (((𝐴 Xrm (2 · 𝑄))↑2) − (((𝐴↑2) − 1) · ((𝐴 Yrm (2 · 𝑄))↑2)))
172 rmxynorm 38434 . . . . . . 7 ((𝐴 ∈ (ℤ‘2) ∧ (2 · 𝑄) ∈ ℤ) → (((𝐴 Xrm (2 · 𝑄))↑2) − (((𝐴↑2) − 1) · ((𝐴 Yrm (2 · 𝑄))↑2))) = 1)
1732, 19, 172syl2anc 579 . . . . . 6 (𝜑 → (((𝐴 Xrm (2 · 𝑄))↑2) − (((𝐴↑2) − 1) · ((𝐴 Yrm (2 · 𝑄))↑2))) = 1)
174171, 173syl5eq 2825 . . . . 5 (𝜑 → ((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = 1)
175167, 174, 823jca 1119 . . . 4 (𝜑 → (((𝐷↑2) − (((𝐴↑2) − 1) · (𝐶↑2))) = 1 ∧ ((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = 1 ∧ 𝐺 ∈ (ℤ‘2)))
17699oveq1i 6932 . . . . . . 7 (𝐼↑2) = ((𝐺 Xrm 𝐵)↑2)
17785oveq1i 6932 . . . . . . . 8 (𝐻↑2) = ((𝐺 Yrm 𝐵)↑2)
178177oveq2i 6933 . . . . . . 7 (((𝐺↑2) − 1) · (𝐻↑2)) = (((𝐺↑2) − 1) · ((𝐺 Yrm 𝐵)↑2))
179176, 178oveq12i 6934 . . . . . 6 ((𝐼↑2) − (((𝐺↑2) − 1) · (𝐻↑2))) = (((𝐺 Xrm 𝐵)↑2) − (((𝐺↑2) − 1) · ((𝐺 Yrm 𝐵)↑2)))
180 rmxynorm 38434 . . . . . . 7 ((𝐺 ∈ (ℤ‘2) ∧ 𝐵 ∈ ℤ) → (((𝐺 Xrm 𝐵)↑2) − (((𝐺↑2) − 1) · ((𝐺 Yrm 𝐵)↑2))) = 1)
18182, 4, 180syl2anc 579 . . . . . 6 (𝜑 → (((𝐺 Xrm 𝐵)↑2) − (((𝐺↑2) − 1) · ((𝐺 Yrm 𝐵)↑2))) = 1)
182179, 181syl5eq 2825 . . . . 5 (𝜑 → ((𝐼↑2) − (((𝐺↑2) − 1) · (𝐻↑2))) = 1)
183104a1i 11 . . . . . . . . 9 (𝜑𝐽 = ((𝐸 / (2 · (𝐶↑2))) − 1))
184183oveq1d 6937 . . . . . . . 8 (𝜑 → (𝐽 + 1) = (((𝐸 / (2 · (𝐶↑2))) − 1) + 1))
185143zcnd 11835 . . . . . . . . . 10 (𝜑𝐸 ∈ ℂ)
186154nncnd 11392 . . . . . . . . . 10 (𝜑 → (2 · (𝐶↑2)) ∈ ℂ)
187154nnne0d 11425 . . . . . . . . . 10 (𝜑 → (2 · (𝐶↑2)) ≠ 0)
188185, 186, 187divcld 11151 . . . . . . . . 9 (𝜑 → (𝐸 / (2 · (𝐶↑2))) ∈ ℂ)
189 ax-1cn 10330 . . . . . . . . 9 1 ∈ ℂ
190 npcan 10632 . . . . . . . . 9 (((𝐸 / (2 · (𝐶↑2))) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐸 / (2 · (𝐶↑2))) − 1) + 1) = (𝐸 / (2 · (𝐶↑2))))
191188, 189, 190sylancl 580 . . . . . . . 8 (𝜑 → (((𝐸 / (2 · (𝐶↑2))) − 1) + 1) = (𝐸 / (2 · (𝐶↑2))))
192184, 191eqtrd 2813 . . . . . . 7 (𝜑 → (𝐽 + 1) = (𝐸 / (2 · (𝐶↑2))))
193192oveq1d 6937 . . . . . 6 (𝜑 → ((𝐽 + 1) · (2 · (𝐶↑2))) = ((𝐸 / (2 · (𝐶↑2))) · (2 · (𝐶↑2))))
194185, 186, 187divcan1d 11152 . . . . . 6 (𝜑 → ((𝐸 / (2 · (𝐶↑2))) · (2 · (𝐶↑2))) = 𝐸)
195193, 194eqtr2d 2814 . . . . 5 (𝜑𝐸 = ((𝐽 + 1) · (2 · (𝐶↑2))))
19644nn0zd 11832 . . . . . . 7 (𝜑𝐹 ∈ ℤ)
19778nn0zd 11832 . . . . . . . 8 (𝜑 → ((𝐹↑2) − 𝐴) ∈ ℤ)
198196, 197zmulcld 11840 . . . . . . 7 (𝜑 → (𝐹 · ((𝐹↑2) − 𝐴)) ∈ ℤ)
199 dvdsmul1 15410 . . . . . . 7 ((𝐹 ∈ ℤ ∧ (𝐹 · ((𝐹↑2) − 𝐴)) ∈ ℤ) → 𝐹 ∥ (𝐹 · (𝐹 · ((𝐹↑2) − 𝐴))))
200196, 198, 199syl2anc 579 . . . . . 6 (𝜑𝐹 ∥ (𝐹 · (𝐹 · ((𝐹↑2) − 𝐴))))
20147oveq1i 6932 . . . . . . 7 (𝐺𝐴) = ((𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) − 𝐴)
20254nn0cnd 11704 . . . . . . . . 9 (𝜑𝐴 ∈ ℂ)
20379nn0cnd 11704 . . . . . . . . 9 (𝜑 → ((𝐹↑2) · ((𝐹↑2) − 𝐴)) ∈ ℂ)
204202, 203pncan2d 10736 . . . . . . . 8 (𝜑 → ((𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) − 𝐴) = ((𝐹↑2) · ((𝐹↑2) − 𝐴)))
20549oveq1d 6937 . . . . . . . 8 (𝜑 → ((𝐹↑2) · ((𝐹↑2) − 𝐴)) = ((𝐹 · 𝐹) · ((𝐹↑2) − 𝐴)))
20678nn0cnd 11704 . . . . . . . . 9 (𝜑 → ((𝐹↑2) − 𝐴) ∈ ℂ)
20748, 48, 206mulassd 10400 . . . . . . . 8 (𝜑 → ((𝐹 · 𝐹) · ((𝐹↑2) − 𝐴)) = (𝐹 · (𝐹 · ((𝐹↑2) − 𝐴))))
208204, 205, 2073eqtrd 2817 . . . . . . 7 (𝜑 → ((𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) − 𝐴) = (𝐹 · (𝐹 · ((𝐹↑2) − 𝐴))))
209201, 208syl5eq 2825 . . . . . 6 (𝜑 → (𝐺𝐴) = (𝐹 · (𝐹 · ((𝐹↑2) − 𝐴))))
210200, 209breqtrrd 4914 . . . . 5 (𝜑𝐹 ∥ (𝐺𝐴))
211182, 195, 2103jca 1119 . . . 4 (𝜑 → (((𝐼↑2) − (((𝐺↑2) − 1) · (𝐻↑2))) = 1 ∧ 𝐸 = ((𝐽 + 1) · (2 · (𝐶↑2))) ∧ 𝐹 ∥ (𝐺𝐴)))
212 zmulcl 11778 . . . . . . . 8 ((2 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (2 · 𝐶) ∈ ℤ)
21310, 14, 212sylancr 581 . . . . . . 7 (𝜑 → (2 · 𝐶) ∈ ℤ)
214 eluzelz 12002 . . . . . . . 8 (𝐴 ∈ (ℤ‘2) → 𝐴 ∈ ℤ)
2152, 214syl 17 . . . . . . 7 (𝜑𝐴 ∈ ℤ)
21679nn0zd 11832 . . . . . . 7 (𝜑 → ((𝐹↑2) · ((𝐹↑2) − 𝐴)) ∈ ℤ)
217 1z 11759 . . . . . . . 8 1 ∈ ℤ
218 zsubcl 11771 . . . . . . . . 9 ((1 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (1 − 𝐴) ∈ ℤ)
219217, 215, 218sylancr 581 . . . . . . . 8 (𝜑 → (1 − 𝐴) ∈ ℤ)
220 zmulcl 11778 . . . . . . . 8 ((1 ∈ ℤ ∧ (1 − 𝐴) ∈ ℤ) → (1 · (1 − 𝐴)) ∈ ℤ)
221217, 219, 220sylancr 581 . . . . . . 7 (𝜑 → (1 · (1 − 𝐴)) ∈ ℤ)
222 congid 38489 . . . . . . . 8 (((2 · 𝐶) ∈ ℤ ∧ 𝐴 ∈ ℤ) → (2 · 𝐶) ∥ (𝐴𝐴))
223213, 215, 222syl2anc 579 . . . . . . 7 (𝜑 → (2 · 𝐶) ∥ (𝐴𝐴))
22451nn0zd 11832 . . . . . . . 8 (𝜑 → (𝐹↑2) ∈ ℤ)
225217a1i 11 . . . . . . . 8 (𝜑 → 1 ∈ ℤ)
22613nncnd 11392 . . . . . . . . . . . . . . 15 (𝜑𝐶 ∈ ℂ)
227128, 226, 226mulassd 10400 . . . . . . . . . . . . . 14 (𝜑 → ((2 · 𝐶) · 𝐶) = (2 · (𝐶 · 𝐶)))
228226sqvald 13324 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶↑2) = (𝐶 · 𝐶))
229228oveq2d 6938 . . . . . . . . . . . . . 14 (𝜑 → (2 · (𝐶↑2)) = (2 · (𝐶 · 𝐶)))
230227, 229eqtr4d 2816 . . . . . . . . . . . . 13 (𝜑 → ((2 · 𝐶) · 𝐶) = (2 · (𝐶↑2)))
231230, 142eqbrtrd 4908 . . . . . . . . . . . 12 (𝜑 → ((2 · 𝐶) · 𝐶) ∥ 𝐸)
232 muldvds1 15413 . . . . . . . . . . . . 13 (((2 · 𝐶) ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝐸 ∈ ℤ) → (((2 · 𝐶) · 𝐶) ∥ 𝐸 → (2 · 𝐶) ∥ 𝐸))
233213, 14, 143, 232syl3anc 1439 . . . . . . . . . . . 12 (𝜑 → (((2 · 𝐶) · 𝐶) ∥ 𝐸 → (2 · 𝐶) ∥ 𝐸))
234231, 233mpd 15 . . . . . . . . . . 11 (𝜑 → (2 · 𝐶) ∥ 𝐸)
235 zsqcl 13253 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ)
236215, 235syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝐴↑2) ∈ ℤ)
237 peano2zm 11772 . . . . . . . . . . . . . 14 ((𝐴↑2) ∈ ℤ → ((𝐴↑2) − 1) ∈ ℤ)
238236, 237syl 17 . . . . . . . . . . . . 13 (𝜑 → ((𝐴↑2) − 1) ∈ ℤ)
239238, 143zmulcld 11840 . . . . . . . . . . . 12 (𝜑 → (((𝐴↑2) − 1) · 𝐸) ∈ ℤ)
240 dvdsmultr2 15428 . . . . . . . . . . . 12 (((2 · 𝐶) ∈ ℤ ∧ (((𝐴↑2) − 1) · 𝐸) ∈ ℤ ∧ 𝐸 ∈ ℤ) → ((2 · 𝐶) ∥ 𝐸 → (2 · 𝐶) ∥ ((((𝐴↑2) − 1) · 𝐸) · 𝐸)))
241213, 239, 143, 240syl3anc 1439 . . . . . . . . . . 11 (𝜑 → ((2 · 𝐶) ∥ 𝐸 → (2 · 𝐶) ∥ ((((𝐴↑2) − 1) · 𝐸) · 𝐸)))
242234, 241mpd 15 . . . . . . . . . 10 (𝜑 → (2 · 𝐶) ∥ ((((𝐴↑2) − 1) · 𝐸) · 𝐸))
243185sqvald 13324 . . . . . . . . . . . 12 (𝜑 → (𝐸↑2) = (𝐸 · 𝐸))
244243oveq2d 6938 . . . . . . . . . . 11 (𝜑 → (((𝐴↑2) − 1) · (𝐸↑2)) = (((𝐴↑2) − 1) · (𝐸 · 𝐸)))
245202sqcld 13325 . . . . . . . . . . . . 13 (𝜑 → (𝐴↑2) ∈ ℂ)
246 subcl 10621 . . . . . . . . . . . . 13 (((𝐴↑2) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐴↑2) − 1) ∈ ℂ)
247245, 189, 246sylancl 580 . . . . . . . . . . . 12 (𝜑 → ((𝐴↑2) − 1) ∈ ℂ)
248247, 185, 185mulassd 10400 . . . . . . . . . . 11 (𝜑 → ((((𝐴↑2) − 1) · 𝐸) · 𝐸) = (((𝐴↑2) − 1) · (𝐸 · 𝐸)))
249244, 248eqtr4d 2816 . . . . . . . . . 10 (𝜑 → (((𝐴↑2) − 1) · (𝐸↑2)) = ((((𝐴↑2) − 1) · 𝐸) · 𝐸))
250242, 249breqtrrd 4914 . . . . . . . . 9 (𝜑 → (2 · 𝐶) ∥ (((𝐴↑2) − 1) · (𝐸↑2)))
25148sqcld 13325 . . . . . . . . . . 11 (𝜑 → (𝐹↑2) ∈ ℂ)
252185sqcld 13325 . . . . . . . . . . . 12 (𝜑 → (𝐸↑2) ∈ ℂ)
253247, 252mulcld 10397 . . . . . . . . . . 11 (𝜑 → (((𝐴↑2) − 1) · (𝐸↑2)) ∈ ℂ)
254189a1i 11 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℂ)
255 subsub23 10627 . . . . . . . . . . 11 (((𝐹↑2) ∈ ℂ ∧ (((𝐴↑2) − 1) · (𝐸↑2)) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = 1 ↔ ((𝐹↑2) − 1) = (((𝐴↑2) − 1) · (𝐸↑2))))
256251, 253, 254, 255syl3anc 1439 . . . . . . . . . 10 (𝜑 → (((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = 1 ↔ ((𝐹↑2) − 1) = (((𝐴↑2) − 1) · (𝐸↑2))))
257174, 256mpbid 224 . . . . . . . . 9 (𝜑 → ((𝐹↑2) − 1) = (((𝐴↑2) − 1) · (𝐸↑2)))
258250, 257breqtrrd 4914 . . . . . . . 8 (𝜑 → (2 · 𝐶) ∥ ((𝐹↑2) − 1))
259 congsub 38488 . . . . . . . . 9 ((((2 · 𝐶) ∈ ℤ ∧ (𝐹↑2) ∈ ℤ ∧ 1 ∈ ℤ) ∧ (𝐴 ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ ((2 · 𝐶) ∥ ((𝐹↑2) − 1) ∧ (2 · 𝐶) ∥ (𝐴𝐴))) → (2 · 𝐶) ∥ (((𝐹↑2) − 𝐴) − (1 − 𝐴)))
260213, 224, 225, 215, 215, 258, 223, 259syl322anc 1466 . . . . . . . 8 (𝜑 → (2 · 𝐶) ∥ (((𝐹↑2) − 𝐴) − (1 − 𝐴)))
261 congmul 38485 . . . . . . . 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 1466 . . . . . . 7 (𝜑 → (2 · 𝐶) ∥ (((𝐹↑2) · ((𝐹↑2) − 𝐴)) − (1 · (1 − 𝐴))))
263 congadd 38484 . . . . . . 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 1466 . . . . . 6 (𝜑 → (2 · 𝐶) ∥ ((𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) − (𝐴 + (1 · (1 − 𝐴)))))
26547a1i 11 . . . . . . 7 (𝜑𝐺 = (𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))))
266219zcnd 11835 . . . . . . . . . 10 (𝜑 → (1 − 𝐴) ∈ ℂ)
267266mulid2d 10395 . . . . . . . . 9 (𝜑 → (1 · (1 − 𝐴)) = (1 − 𝐴))
268267oveq2d 6938 . . . . . . . 8 (𝜑 → (𝐴 + (1 · (1 − 𝐴))) = (𝐴 + (1 − 𝐴)))
269 pncan3 10630 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + (1 − 𝐴)) = 1)
270202, 189, 269sylancl 580 . . . . . . . 8 (𝜑 → (𝐴 + (1 − 𝐴)) = 1)
271268, 270eqtr2d 2814 . . . . . . 7 (𝜑 → 1 = (𝐴 + (1 · (1 − 𝐴))))
272265, 271oveq12d 6940 . . . . . 6 (𝜑 → (𝐺 − 1) = ((𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) − (𝐴 + (1 · (1 − 𝐴)))))
273264, 272breqtrrd 4914 . . . . 5 (𝜑 → (2 · 𝐶) ∥ (𝐺 − 1))
274 jm2.15nn0 38521 . . . . . . . 8 ((𝐺 ∈ (ℤ‘2) ∧ 𝐴 ∈ (ℤ‘2) ∧ 𝐵 ∈ ℕ0) → (𝐺𝐴) ∥ ((𝐺 Yrm 𝐵) − (𝐴 Yrm 𝐵)))
27582, 2, 90, 274syl3anc 1439 . . . . . . 7 (𝜑 → (𝐺𝐴) ∥ ((𝐺 Yrm 𝐵) − (𝐴 Yrm 𝐵)))
27685a1i 11 . . . . . . . 8 (𝜑𝐻 = (𝐺 Yrm 𝐵))
277276, 12oveq12d 6940 . . . . . . 7 (𝜑 → (𝐻𝐶) = ((𝐺 Yrm 𝐵) − (𝐴 Yrm 𝐵)))
278275, 277breqtrrd 4914 . . . . . 6 (𝜑 → (𝐺𝐴) ∥ (𝐻𝐶))
279 eluzelz 12002 . . . . . . . . 9 (𝐺 ∈ (ℤ‘2) → 𝐺 ∈ ℤ)
28082, 279syl 17 . . . . . . . 8 (𝜑𝐺 ∈ ℤ)
281280, 215zsubcld 11839 . . . . . . 7 (𝜑 → (𝐺𝐴) ∈ ℤ)
28285, 87syl5eqel 2862 . . . . . . . 8 (𝜑𝐻 ∈ ℤ)
283282, 14zsubcld 11839 . . . . . . 7 (𝜑 → (𝐻𝐶) ∈ ℤ)
284 dvdstr 15425 . . . . . . 7 ((𝐹 ∈ ℤ ∧ (𝐺𝐴) ∈ ℤ ∧ (𝐻𝐶) ∈ ℤ) → ((𝐹 ∥ (𝐺𝐴) ∧ (𝐺𝐴) ∥ (𝐻𝐶)) → 𝐹 ∥ (𝐻𝐶)))
285196, 281, 283, 284syl3anc 1439 . . . . . 6 (𝜑 → ((𝐹 ∥ (𝐺𝐴) ∧ (𝐺𝐴) ∥ (𝐻𝐶)) → 𝐹 ∥ (𝐻𝐶)))
286210, 278, 285mp2and 689 . . . . 5 (𝜑𝐹 ∥ (𝐻𝐶))
287 jm2.16nn0 38522 . . . . . . . . 9 ((𝐺 ∈ (ℤ‘2) ∧ 𝐵 ∈ ℕ0) → (𝐺 − 1) ∥ ((𝐺 Yrm 𝐵) − 𝐵))
28882, 90, 287syl2anc 579 . . . . . . . 8 (𝜑 → (𝐺 − 1) ∥ ((𝐺 Yrm 𝐵) − 𝐵))
28985oveq1i 6932 . . . . . . . 8 (𝐻𝐵) = ((𝐺 Yrm 𝐵) − 𝐵)
290288, 289syl6breqr 4928 . . . . . . 7 (𝜑 → (𝐺 − 1) ∥ (𝐻𝐵))
291 peano2zm 11772 . . . . . . . . 9 (𝐺 ∈ ℤ → (𝐺 − 1) ∈ ℤ)
292280, 291syl 17 . . . . . . . 8 (𝜑 → (𝐺 − 1) ∈ ℤ)
293282, 4zsubcld 11839 . . . . . . . 8 (𝜑 → (𝐻𝐵) ∈ ℤ)
294 dvdstr 15425 . . . . . . . 8 (((2 · 𝐶) ∈ ℤ ∧ (𝐺 − 1) ∈ ℤ ∧ (𝐻𝐵) ∈ ℤ) → (((2 · 𝐶) ∥ (𝐺 − 1) ∧ (𝐺 − 1) ∥ (𝐻𝐵)) → (2 · 𝐶) ∥ (𝐻𝐵)))
295213, 292, 293, 294syl3anc 1439 . . . . . . 7 (𝜑 → (((2 · 𝐶) ∥ (𝐺 − 1) ∧ (𝐺 − 1) ∥ (𝐻𝐵)) → (2 · 𝐶) ∥ (𝐻𝐵)))
296273, 290, 295mp2and 689 . . . . . 6 (𝜑 → (2 · 𝐶) ∥ (𝐻𝐵))
297 rmygeid 38482 . . . . . . . 8 ((𝐴 ∈ (ℤ‘2) ∧ 𝐵 ∈ ℕ0) → 𝐵 ≤ (𝐴 Yrm 𝐵))
2982, 90, 297syl2anc 579 . . . . . . 7 (𝜑𝐵 ≤ (𝐴 Yrm 𝐵))
299298, 12breqtrrd 4914 . . . . . 6 (𝜑𝐵𝐶)
300296, 299jca 507 . . . . 5 (𝜑 → ((2 · 𝐶) ∥ (𝐻𝐵) ∧ 𝐵𝐶))
301273, 286, 300jca31 510 . . . 4 (𝜑 → (((2 · 𝐶) ∥ (𝐺 − 1) ∧ 𝐹 ∥ (𝐻𝐶)) ∧ ((2 · 𝐶) ∥ (𝐻𝐵) ∧ 𝐵𝐶)))
302175, 211, 301jca31 510 . . 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 507 . 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 510 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 198  wa 386  w3a 1071   = wceq 1601  wcel 2106   class class class wbr 4886  cfv 6135  (class class class)co 6922  cc 10270  0cc0 10272  1c1 10273   + caddc 10275   · cmul 10277   < clt 10411  cle 10412  cmin 10606   / cdiv 11032  cn 11374  2c2 11430  0cn0 11642  cz 11728  cuz 11992  cexp 13178  cdvds 15387   Xrm crmx 38416   Yrm crmy 38417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-inf2 8835  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349  ax-pre-sup 10350  ax-addf 10351  ax-mulf 10352
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-fal 1615  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rmo 3097  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-pss 3807  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4672  df-int 4711  df-iun 4755  df-iin 4756  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-se 5315  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-isom 6144  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-of 7174  df-om 7344  df-1st 7445  df-2nd 7446  df-supp 7577  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-2o 7844  df-oadd 7847  df-omul 7848  df-er 8026  df-map 8142  df-pm 8143  df-ixp 8195  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-fsupp 8564  df-fi 8605  df-sup 8636  df-inf 8637  df-oi 8704  df-card 9098  df-acn 9101  df-cda 9325  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-nn 11375  df-2 11438  df-3 11439  df-4 11440  df-5 11441  df-6 11442  df-7 11443  df-8 11444  df-9 11445  df-n0 11643  df-xnn0 11715  df-z 11729  df-dec 11846  df-uz 11993  df-q 12096  df-rp 12138  df-xneg 12257  df-xadd 12258  df-xmul 12259  df-ioo 12491  df-ioc 12492  df-ico 12493  df-icc 12494  df-fz 12644  df-fzo 12785  df-fl 12912  df-mod 12988  df-seq 13120  df-exp 13179  df-fac 13379  df-bc 13408  df-hash 13436  df-shft 14214  df-cj 14246  df-re 14247  df-im 14248  df-sqrt 14382  df-abs 14383  df-limsup 14610  df-clim 14627  df-rlim 14628  df-sum 14825  df-ef 15200  df-sin 15202  df-cos 15203  df-pi 15205  df-dvds 15388  df-gcd 15623  df-prm 15791  df-numer 15847  df-denom 15848  df-struct 16257  df-ndx 16258  df-slot 16259  df-base 16261  df-sets 16262  df-ress 16263  df-plusg 16351  df-mulr 16352  df-starv 16353  df-sca 16354  df-vsca 16355  df-ip 16356  df-tset 16357  df-ple 16358  df-ds 16360  df-unif 16361  df-hom 16362  df-cco 16363  df-rest 16469  df-topn 16470  df-0g 16488  df-gsum 16489  df-topgen 16490  df-pt 16491  df-prds 16494  df-xrs 16548  df-qtop 16553  df-imas 16554  df-xps 16556  df-mre 16632  df-mrc 16633  df-acs 16635  df-mgm 17628  df-sgrp 17670  df-mnd 17681  df-submnd 17722  df-mulg 17928  df-cntz 18133  df-cmn 18581  df-psmet 20134  df-xmet 20135  df-met 20136  df-bl 20137  df-mopn 20138  df-fbas 20139  df-fg 20140  df-cnfld 20143  df-top 21106  df-topon 21123  df-topsp 21145  df-bases 21158  df-cld 21231  df-ntr 21232  df-cls 21233  df-nei 21310  df-lp 21348  df-perf 21349  df-cn 21439  df-cnp 21440  df-haus 21527  df-tx 21774  df-hmeo 21967  df-fil 22058  df-fm 22150  df-flim 22151  df-flf 22152  df-xms 22533  df-ms 22534  df-tms 22535  df-cncf 23089  df-limc 24067  df-dv 24068  df-log 24740  df-squarenn 38357  df-pell1qr 38358  df-pell14qr 38359  df-pell1234qr 38360  df-pellfund 38361  df-rmx 38418  df-rmy 38419
This theorem is referenced by:  jm2.27  38526
  Copyright terms: Public domain W3C validator