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 39869
Description: Lemma for jm2.27 39870. 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 12083 . . . . 5 (𝜑𝐵 ∈ ℤ)
5 frmx 39775 . . . . . 6 Xrm :((ℤ‘2) × ℤ)⟶ℕ0
65fovcl 7272 . . . . 5 ((𝐴 ∈ (ℤ‘2) ∧ 𝐵 ∈ ℤ) → (𝐴 Xrm 𝐵) ∈ ℕ0)
72, 4, 6syl2anc 587 . . . 4 (𝜑 → (𝐴 Xrm 𝐵) ∈ ℕ0)
81, 7eqeltrid 2920 . . 3 (𝜑𝐷 ∈ ℕ0)
9 jm2.27c7 . . . 4 𝐸 = (𝐴 Yrm (2 · 𝑄))
10 2z 12011 . . . . . . 7 2 ∈ ℤ
11 jm2.27c6 . . . . . . . 8 𝑄 = (𝐵 · (𝐴 Yrm 𝐵))
12 jm2.27c4 . . . . . . . . . 10 (𝜑𝐶 = (𝐴 Yrm 𝐵))
13 jm2.27a3 . . . . . . . . . . 11 (𝜑𝐶 ∈ ℕ)
1413nnzd 12083 . . . . . . . . . 10 (𝜑𝐶 ∈ ℤ)
1512, 14eqeltrrd 2917 . . . . . . . . 9 (𝜑 → (𝐴 Yrm 𝐵) ∈ ℤ)
164, 15zmulcld 12090 . . . . . . . 8 (𝜑 → (𝐵 · (𝐴 Yrm 𝐵)) ∈ ℤ)
1711, 16eqeltrid 2920 . . . . . . 7 (𝜑𝑄 ∈ ℤ)
18 zmulcl 12028 . . . . . . 7 ((2 ∈ ℤ ∧ 𝑄 ∈ ℤ) → (2 · 𝑄) ∈ ℤ)
1910, 17, 18sylancr 590 . . . . . 6 (𝜑 → (2 · 𝑄) ∈ ℤ)
20 frmy 39776 . . . . . . 7 Yrm :((ℤ‘2) × ℤ)⟶ℤ
2120fovcl 7272 . . . . . 6 ((𝐴 ∈ (ℤ‘2) ∧ (2 · 𝑄) ∈ ℤ) → (𝐴 Yrm (2 · 𝑄)) ∈ ℤ)
222, 19, 21syl2anc 587 . . . . 5 (𝜑 → (𝐴 Yrm (2 · 𝑄)) ∈ ℤ)
23 rmy0 39791 . . . . . . 7 (𝐴 ∈ (ℤ‘2) → (𝐴 Yrm 0) = 0)
242, 23syl 17 . . . . . 6 (𝜑 → (𝐴 Yrm 0) = 0)
25 2nn 11707 . . . . . . . . . 10 2 ∈ ℕ
2612, 13eqeltrrd 2917 . . . . . . . . . . . 12 (𝜑 → (𝐴 Yrm 𝐵) ∈ ℕ)
273, 26nnmulcld 11687 . . . . . . . . . . 11 (𝜑 → (𝐵 · (𝐴 Yrm 𝐵)) ∈ ℕ)
2811, 27eqeltrid 2920 . . . . . . . . . 10 (𝜑𝑄 ∈ ℕ)
29 nnmulcl 11658 . . . . . . . . . 10 ((2 ∈ ℕ ∧ 𝑄 ∈ ℕ) → (2 · 𝑄) ∈ ℕ)
3025, 28, 29sylancr 590 . . . . . . . . 9 (𝜑 → (2 · 𝑄) ∈ ℕ)
3130nnnn0d 11952 . . . . . . . 8 (𝜑 → (2 · 𝑄) ∈ ℕ0)
3231nn0ge0d 11955 . . . . . . 7 (𝜑 → 0 ≤ (2 · 𝑄))
33 0zd 11990 . . . . . . . 8 (𝜑 → 0 ∈ ℤ)
34 lermy 39817 . . . . . . . 8 ((𝐴 ∈ (ℤ‘2) ∧ 0 ∈ ℤ ∧ (2 · 𝑄) ∈ ℤ) → (0 ≤ (2 · 𝑄) ↔ (𝐴 Yrm 0) ≤ (𝐴 Yrm (2 · 𝑄))))
352, 33, 19, 34syl3anc 1368 . . . . . . 7 (𝜑 → (0 ≤ (2 · 𝑄) ↔ (𝐴 Yrm 0) ≤ (𝐴 Yrm (2 · 𝑄))))
3632, 35mpbid 235 . . . . . 6 (𝜑 → (𝐴 Yrm 0) ≤ (𝐴 Yrm (2 · 𝑄)))
3724, 36eqbrtrrd 5076 . . . . 5 (𝜑 → 0 ≤ (𝐴 Yrm (2 · 𝑄)))
38 elnn0z 11991 . . . . 5 ((𝐴 Yrm (2 · 𝑄)) ∈ ℕ0 ↔ ((𝐴 Yrm (2 · 𝑄)) ∈ ℤ ∧ 0 ≤ (𝐴 Yrm (2 · 𝑄))))
3922, 37, 38sylanbrc 586 . . . 4 (𝜑 → (𝐴 Yrm (2 · 𝑄)) ∈ ℕ0)
409, 39eqeltrid 2920 . . 3 (𝜑𝐸 ∈ ℕ0)
41 jm2.27c8 . . . 4 𝐹 = (𝐴 Xrm (2 · 𝑄))
425fovcl 7272 . . . . 5 ((𝐴 ∈ (ℤ‘2) ∧ (2 · 𝑄) ∈ ℤ) → (𝐴 Xrm (2 · 𝑄)) ∈ ℕ0)
432, 19, 42syl2anc 587 . . . 4 (𝜑 → (𝐴 Xrm (2 · 𝑄)) ∈ ℕ0)
4441, 43eqeltrid 2920 . . 3 (𝜑𝐹 ∈ ℕ0)
458, 40, 443jca 1125 . 2 (𝜑 → (𝐷 ∈ ℕ0𝐸 ∈ ℕ0𝐹 ∈ ℕ0))
46 2nn0 11911 . . . 4 2 ∈ ℕ0
47 jm2.27c9 . . . . 5 𝐺 = (𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴)))
4844nn0cnd 11954 . . . . . . . . 9 (𝜑𝐹 ∈ ℂ)
4948sqvald 13512 . . . . . . . 8 (𝜑 → (𝐹↑2) = (𝐹 · 𝐹))
5044, 44nn0mulcld 11957 . . . . . . . 8 (𝜑 → (𝐹 · 𝐹) ∈ ℕ0)
5149, 50eqeltrd 2916 . . . . . . 7 (𝜑 → (𝐹↑2) ∈ ℕ0)
52 eluz2nn 12281 . . . . . . . . . . . . 13 (𝐴 ∈ (ℤ‘2) → 𝐴 ∈ ℕ)
532, 52syl 17 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℕ)
5453nnnn0d 11952 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℕ0)
5554nn0red 11953 . . . . . . . . . 10 (𝜑𝐴 ∈ ℝ)
5644nn0red 11953 . . . . . . . . . 10 (𝜑𝐹 ∈ ℝ)
5756, 56remulcld 10669 . . . . . . . . . 10 (𝜑 → (𝐹 · 𝐹) ∈ ℝ)
58 rmx1 39788 . . . . . . . . . . . . 13 (𝐴 ∈ (ℤ‘2) → (𝐴 Xrm 1) = 𝐴)
592, 58syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐴 Xrm 1) = 𝐴)
6030nnge1d 11682 . . . . . . . . . . . . 13 (𝜑 → 1 ≤ (2 · 𝑄))
61 1nn0 11910 . . . . . . . . . . . . . . 15 1 ∈ ℕ0
6261a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ ℕ0)
63 lermxnn0 39812 . . . . . . . . . . . . . 14 ((𝐴 ∈ (ℤ‘2) ∧ 1 ∈ ℕ0 ∧ (2 · 𝑄) ∈ ℕ0) → (1 ≤ (2 · 𝑄) ↔ (𝐴 Xrm 1) ≤ (𝐴 Xrm (2 · 𝑄))))
642, 62, 31, 63syl3anc 1368 . . . . . . . . . . . . 13 (𝜑 → (1 ≤ (2 · 𝑄) ↔ (𝐴 Xrm 1) ≤ (𝐴 Xrm (2 · 𝑄))))
6560, 64mpbid 235 . . . . . . . . . . . 12 (𝜑 → (𝐴 Xrm 1) ≤ (𝐴 Xrm (2 · 𝑄)))
6659, 65eqbrtrrd 5076 . . . . . . . . . . 11 (𝜑𝐴 ≤ (𝐴 Xrm (2 · 𝑄)))
6766, 41breqtrrdi 5094 . . . . . . . . . 10 (𝜑𝐴𝐹)
6844nn0ge0d 11955 . . . . . . . . . . 11 (𝜑 → 0 ≤ 𝐹)
69 rmxnn 39813 . . . . . . . . . . . . . 14 ((𝐴 ∈ (ℤ‘2) ∧ (2 · 𝑄) ∈ ℤ) → (𝐴 Xrm (2 · 𝑄)) ∈ ℕ)
702, 19, 69syl2anc 587 . . . . . . . . . . . . 13 (𝜑 → (𝐴 Xrm (2 · 𝑄)) ∈ ℕ)
7141, 70eqeltrid 2920 . . . . . . . . . . . 12 (𝜑𝐹 ∈ ℕ)
7271nnge1d 11682 . . . . . . . . . . 11 (𝜑 → 1 ≤ 𝐹)
7356, 56, 68, 72lemulge12d 11576 . . . . . . . . . 10 (𝜑𝐹 ≤ (𝐹 · 𝐹))
7455, 56, 57, 67, 73letrd 10795 . . . . . . . . 9 (𝜑𝐴 ≤ (𝐹 · 𝐹))
7574, 49breqtrrd 5080 . . . . . . . 8 (𝜑𝐴 ≤ (𝐹↑2))
76 nn0sub 11944 . . . . . . . . 9 ((𝐴 ∈ ℕ0 ∧ (𝐹↑2) ∈ ℕ0) → (𝐴 ≤ (𝐹↑2) ↔ ((𝐹↑2) − 𝐴) ∈ ℕ0))
7754, 51, 76syl2anc 587 . . . . . . . 8 (𝜑 → (𝐴 ≤ (𝐹↑2) ↔ ((𝐹↑2) − 𝐴) ∈ ℕ0))
7875, 77mpbid 235 . . . . . . 7 (𝜑 → ((𝐹↑2) − 𝐴) ∈ ℕ0)
7951, 78nn0mulcld 11957 . . . . . 6 (𝜑 → ((𝐹↑2) · ((𝐹↑2) − 𝐴)) ∈ ℕ0)
80 uzaddcl 12301 . . . . . 6 ((𝐴 ∈ (ℤ‘2) ∧ ((𝐹↑2) · ((𝐹↑2) − 𝐴)) ∈ ℕ0) → (𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) ∈ (ℤ‘2))
812, 79, 80syl2anc 587 . . . . 5 (𝜑 → (𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) ∈ (ℤ‘2))
8247, 81eqeltrid 2920 . . . 4 (𝜑𝐺 ∈ (ℤ‘2))
83 eluznn0 12314 . . . 4 ((2 ∈ ℕ0𝐺 ∈ (ℤ‘2)) → 𝐺 ∈ ℕ0)
8446, 82, 83sylancr 590 . . 3 (𝜑𝐺 ∈ ℕ0)
85 jm2.27c10 . . . 4 𝐻 = (𝐺 Yrm 𝐵)
8620fovcl 7272 . . . . . 6 ((𝐺 ∈ (ℤ‘2) ∧ 𝐵 ∈ ℤ) → (𝐺 Yrm 𝐵) ∈ ℤ)
8782, 4, 86syl2anc 587 . . . . 5 (𝜑 → (𝐺 Yrm 𝐵) ∈ ℤ)
88 rmy0 39791 . . . . . . 7 (𝐺 ∈ (ℤ‘2) → (𝐺 Yrm 0) = 0)
8982, 88syl 17 . . . . . 6 (𝜑 → (𝐺 Yrm 0) = 0)
903nnnn0d 11952 . . . . . . . 8 (𝜑𝐵 ∈ ℕ0)
9190nn0ge0d 11955 . . . . . . 7 (𝜑 → 0 ≤ 𝐵)
92 lermy 39817 . . . . . . . 8 ((𝐺 ∈ (ℤ‘2) ∧ 0 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (0 ≤ 𝐵 ↔ (𝐺 Yrm 0) ≤ (𝐺 Yrm 𝐵)))
9382, 33, 4, 92syl3anc 1368 . . . . . . 7 (𝜑 → (0 ≤ 𝐵 ↔ (𝐺 Yrm 0) ≤ (𝐺 Yrm 𝐵)))
9491, 93mpbid 235 . . . . . 6 (𝜑 → (𝐺 Yrm 0) ≤ (𝐺 Yrm 𝐵))
9589, 94eqbrtrrd 5076 . . . . 5 (𝜑 → 0 ≤ (𝐺 Yrm 𝐵))
96 elnn0z 11991 . . . . 5 ((𝐺 Yrm 𝐵) ∈ ℕ0 ↔ ((𝐺 Yrm 𝐵) ∈ ℤ ∧ 0 ≤ (𝐺 Yrm 𝐵)))
9787, 95, 96sylanbrc 586 . . . 4 (𝜑 → (𝐺 Yrm 𝐵) ∈ ℕ0)
9885, 97eqeltrid 2920 . . 3 (𝜑𝐻 ∈ ℕ0)
99 jm2.27c11 . . . 4 𝐼 = (𝐺 Xrm 𝐵)
1005fovcl 7272 . . . . 5 ((𝐺 ∈ (ℤ‘2) ∧ 𝐵 ∈ ℤ) → (𝐺 Xrm 𝐵) ∈ ℕ0)
10182, 4, 100syl2anc 587 . . . 4 (𝜑 → (𝐺 Xrm 𝐵) ∈ ℕ0)
10299, 101eqeltrid 2920 . . 3 (𝜑𝐼 ∈ ℕ0)
10384, 98, 1023jca 1125 . 2 (𝜑 → (𝐺 ∈ ℕ0𝐻 ∈ ℕ0𝐼 ∈ ℕ0))
104 jm2.27c12 . . . 4 𝐽 = ((𝐸 / (2 · (𝐶↑2))) − 1)
105 iddvds 15623 . . . . . . . . . . . 12 ((𝐵 · (𝐴 Yrm 𝐵)) ∈ ℤ → (𝐵 · (𝐴 Yrm 𝐵)) ∥ (𝐵 · (𝐴 Yrm 𝐵)))
10616, 105syl 17 . . . . . . . . . . 11 (𝜑 → (𝐵 · (𝐴 Yrm 𝐵)) ∥ (𝐵 · (𝐴 Yrm 𝐵)))
107106, 11breqtrrdi 5094 . . . . . . . . . 10 (𝜑 → (𝐵 · (𝐴 Yrm 𝐵)) ∥ 𝑄)
108 jm2.20nn 39859 . . . . . . . . . . 11 ((𝐴 ∈ (ℤ‘2) ∧ 𝑄 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (((𝐴 Yrm 𝐵)↑2) ∥ (𝐴 Yrm 𝑄) ↔ (𝐵 · (𝐴 Yrm 𝐵)) ∥ 𝑄))
1092, 28, 3, 108syl3anc 1368 . . . . . . . . . 10 (𝜑 → (((𝐴 Yrm 𝐵)↑2) ∥ (𝐴 Yrm 𝑄) ↔ (𝐵 · (𝐴 Yrm 𝐵)) ∥ 𝑄))
110107, 109mpbird 260 . . . . . . . . 9 (𝜑 → ((𝐴 Yrm 𝐵)↑2) ∥ (𝐴 Yrm 𝑄))
111 zsqcl 13499 . . . . . . . . . . 11 ((𝐴 Yrm 𝐵) ∈ ℤ → ((𝐴 Yrm 𝐵)↑2) ∈ ℤ)
11215, 111syl 17 . . . . . . . . . 10 (𝜑 → ((𝐴 Yrm 𝐵)↑2) ∈ ℤ)
11320fovcl 7272 . . . . . . . . . . 11 ((𝐴 ∈ (ℤ‘2) ∧ 𝑄 ∈ ℤ) → (𝐴 Yrm 𝑄) ∈ ℤ)
1142, 17, 113syl2anc 587 . . . . . . . . . 10 (𝜑 → (𝐴 Yrm 𝑄) ∈ ℤ)
11510a1i 11 . . . . . . . . . 10 (𝜑 → 2 ∈ ℤ)
116 dvdscmul 15636 . . . . . . . . . 10 ((((𝐴 Yrm 𝐵)↑2) ∈ ℤ ∧ (𝐴 Yrm 𝑄) ∈ ℤ ∧ 2 ∈ ℤ) → (((𝐴 Yrm 𝐵)↑2) ∥ (𝐴 Yrm 𝑄) → (2 · ((𝐴 Yrm 𝐵)↑2)) ∥ (2 · (𝐴 Yrm 𝑄))))
117112, 114, 115, 116syl3anc 1368 . . . . . . . . 9 (𝜑 → (((𝐴 Yrm 𝐵)↑2) ∥ (𝐴 Yrm 𝑄) → (2 · ((𝐴 Yrm 𝐵)↑2)) ∥ (2 · (𝐴 Yrm 𝑄))))
118110, 117mpd 15 . . . . . . . 8 (𝜑 → (2 · ((𝐴 Yrm 𝐵)↑2)) ∥ (2 · (𝐴 Yrm 𝑄)))
119 zmulcl 12028 . . . . . . . . . . 11 ((2 ∈ ℤ ∧ (𝐴 Yrm 𝑄) ∈ ℤ) → (2 · (𝐴 Yrm 𝑄)) ∈ ℤ)
12010, 114, 119sylancr 590 . . . . . . . . . 10 (𝜑 → (2 · (𝐴 Yrm 𝑄)) ∈ ℤ)
1215fovcl 7272 . . . . . . . . . . . 12 ((𝐴 ∈ (ℤ‘2) ∧ 𝑄 ∈ ℤ) → (𝐴 Xrm 𝑄) ∈ ℕ0)
1222, 17, 121syl2anc 587 . . . . . . . . . . 11 (𝜑 → (𝐴 Xrm 𝑄) ∈ ℕ0)
123122nn0zd 12082 . . . . . . . . . 10 (𝜑 → (𝐴 Xrm 𝑄) ∈ ℤ)
124 dvdsmul1 15631 . . . . . . . . . 10 (((2 · (𝐴 Yrm 𝑄)) ∈ ℤ ∧ (𝐴 Xrm 𝑄) ∈ ℤ) → (2 · (𝐴 Yrm 𝑄)) ∥ ((2 · (𝐴 Yrm 𝑄)) · (𝐴 Xrm 𝑄)))
125120, 123, 124syl2anc 587 . . . . . . . . 9 (𝜑 → (2 · (𝐴 Yrm 𝑄)) ∥ ((2 · (𝐴 Yrm 𝑄)) · (𝐴 Xrm 𝑄)))
126 rmydbl 39802 . . . . . . . . . . 11 ((𝐴 ∈ (ℤ‘2) ∧ 𝑄 ∈ ℤ) → (𝐴 Yrm (2 · 𝑄)) = ((2 · (𝐴 Xrm 𝑄)) · (𝐴 Yrm 𝑄)))
1272, 17, 126syl2anc 587 . . . . . . . . . 10 (𝜑 → (𝐴 Yrm (2 · 𝑄)) = ((2 · (𝐴 Xrm 𝑄)) · (𝐴 Yrm 𝑄)))
128 2cnd 11712 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℂ)
129122nn0cnd 11954 . . . . . . . . . . 11 (𝜑 → (𝐴 Xrm 𝑄) ∈ ℂ)
130114zcnd 12085 . . . . . . . . . . 11 (𝜑 → (𝐴 Yrm 𝑄) ∈ ℂ)
131128, 129, 130mul32d 10848 . . . . . . . . . 10 (𝜑 → ((2 · (𝐴 Xrm 𝑄)) · (𝐴 Yrm 𝑄)) = ((2 · (𝐴 Yrm 𝑄)) · (𝐴 Xrm 𝑄)))
132127, 131eqtrd 2859 . . . . . . . . 9 (𝜑 → (𝐴 Yrm (2 · 𝑄)) = ((2 · (𝐴 Yrm 𝑄)) · (𝐴 Xrm 𝑄)))
133125, 132breqtrrd 5080 . . . . . . . 8 (𝜑 → (2 · (𝐴 Yrm 𝑄)) ∥ (𝐴 Yrm (2 · 𝑄)))
134 zmulcl 12028 . . . . . . . . . 10 ((2 ∈ ℤ ∧ ((𝐴 Yrm 𝐵)↑2) ∈ ℤ) → (2 · ((𝐴 Yrm 𝐵)↑2)) ∈ ℤ)
13510, 112, 134sylancr 590 . . . . . . . . 9 (𝜑 → (2 · ((𝐴 Yrm 𝐵)↑2)) ∈ ℤ)
136 dvdstr 15646 . . . . . . . . 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 1368 . . . . . . . 8 (𝜑 → (((2 · ((𝐴 Yrm 𝐵)↑2)) ∥ (2 · (𝐴 Yrm 𝑄)) ∧ (2 · (𝐴 Yrm 𝑄)) ∥ (𝐴 Yrm (2 · 𝑄))) → (2 · ((𝐴 Yrm 𝐵)↑2)) ∥ (𝐴 Yrm (2 · 𝑄))))
138118, 133, 137mp2and 698 . . . . . . 7 (𝜑 → (2 · ((𝐴 Yrm 𝐵)↑2)) ∥ (𝐴 Yrm (2 · 𝑄)))
13912oveq1d 7164 . . . . . . . 8 (𝜑 → (𝐶↑2) = ((𝐴 Yrm 𝐵)↑2))
140139oveq2d 7165 . . . . . . 7 (𝜑 → (2 · (𝐶↑2)) = (2 · ((𝐴 Yrm 𝐵)↑2)))
1419a1i 11 . . . . . . 7 (𝜑𝐸 = (𝐴 Yrm (2 · 𝑄)))
142138, 140, 1413brtr4d 5084 . . . . . 6 (𝜑 → (2 · (𝐶↑2)) ∥ 𝐸)
1439, 22eqeltrid 2920 . . . . . . . 8 (𝜑𝐸 ∈ ℤ)
14430nngt0d 11683 . . . . . . . . . 10 (𝜑 → 0 < (2 · 𝑄))
145 ltrmy 39814 . . . . . . . . . . 11 ((𝐴 ∈ (ℤ‘2) ∧ 0 ∈ ℤ ∧ (2 · 𝑄) ∈ ℤ) → (0 < (2 · 𝑄) ↔ (𝐴 Yrm 0) < (𝐴 Yrm (2 · 𝑄))))
1462, 33, 19, 145syl3anc 1368 . . . . . . . . . 10 (𝜑 → (0 < (2 · 𝑄) ↔ (𝐴 Yrm 0) < (𝐴 Yrm (2 · 𝑄))))
147144, 146mpbid 235 . . . . . . . . 9 (𝜑 → (𝐴 Yrm 0) < (𝐴 Yrm (2 · 𝑄)))
14824eqcomd 2830 . . . . . . . . 9 (𝜑 → 0 = (𝐴 Yrm 0))
149147, 148, 1413brtr4d 5084 . . . . . . . 8 (𝜑 → 0 < 𝐸)
150 elnnz 11988 . . . . . . . 8 (𝐸 ∈ ℕ ↔ (𝐸 ∈ ℤ ∧ 0 < 𝐸))
151143, 149, 150sylanbrc 586 . . . . . . 7 (𝜑𝐸 ∈ ℕ)
15213nnsqcld 13610 . . . . . . . 8 (𝜑 → (𝐶↑2) ∈ ℕ)
153 nnmulcl 11658 . . . . . . . 8 ((2 ∈ ℕ ∧ (𝐶↑2) ∈ ℕ) → (2 · (𝐶↑2)) ∈ ℕ)
15425, 152, 153sylancr 590 . . . . . . 7 (𝜑 → (2 · (𝐶↑2)) ∈ ℕ)
155 nndivdvds 15616 . . . . . . 7 ((𝐸 ∈ ℕ ∧ (2 · (𝐶↑2)) ∈ ℕ) → ((2 · (𝐶↑2)) ∥ 𝐸 ↔ (𝐸 / (2 · (𝐶↑2))) ∈ ℕ))
156151, 154, 155syl2anc 587 . . . . . 6 (𝜑 → ((2 · (𝐶↑2)) ∥ 𝐸 ↔ (𝐸 / (2 · (𝐶↑2))) ∈ ℕ))
157142, 156mpbid 235 . . . . 5 (𝜑 → (𝐸 / (2 · (𝐶↑2))) ∈ ℕ)
158 nnm1nn0 11935 . . . . 5 ((𝐸 / (2 · (𝐶↑2))) ∈ ℕ → ((𝐸 / (2 · (𝐶↑2))) − 1) ∈ ℕ0)
159157, 158syl 17 . . . 4 (𝜑 → ((𝐸 / (2 · (𝐶↑2))) − 1) ∈ ℕ0)
160104, 159eqeltrid 2920 . . 3 (𝜑𝐽 ∈ ℕ0)
1611oveq1i 7159 . . . . . . . 8 (𝐷↑2) = ((𝐴 Xrm 𝐵)↑2)
162161a1i 11 . . . . . . 7 (𝜑 → (𝐷↑2) = ((𝐴 Xrm 𝐵)↑2))
163139oveq2d 7165 . . . . . . 7 (𝜑 → (((𝐴↑2) − 1) · (𝐶↑2)) = (((𝐴↑2) − 1) · ((𝐴 Yrm 𝐵)↑2)))
164162, 163oveq12d 7167 . . . . . 6 (𝜑 → ((𝐷↑2) − (((𝐴↑2) − 1) · (𝐶↑2))) = (((𝐴 Xrm 𝐵)↑2) − (((𝐴↑2) − 1) · ((𝐴 Yrm 𝐵)↑2))))
165 rmxynorm 39780 . . . . . . 7 ((𝐴 ∈ (ℤ‘2) ∧ 𝐵 ∈ ℤ) → (((𝐴 Xrm 𝐵)↑2) − (((𝐴↑2) − 1) · ((𝐴 Yrm 𝐵)↑2))) = 1)
1662, 4, 165syl2anc 587 . . . . . 6 (𝜑 → (((𝐴 Xrm 𝐵)↑2) − (((𝐴↑2) − 1) · ((𝐴 Yrm 𝐵)↑2))) = 1)
167164, 166eqtrd 2859 . . . . 5 (𝜑 → ((𝐷↑2) − (((𝐴↑2) − 1) · (𝐶↑2))) = 1)
16841oveq1i 7159 . . . . . . 7 (𝐹↑2) = ((𝐴 Xrm (2 · 𝑄))↑2)
1699oveq1i 7159 . . . . . . . 8 (𝐸↑2) = ((𝐴 Yrm (2 · 𝑄))↑2)
170169oveq2i 7160 . . . . . . 7 (((𝐴↑2) − 1) · (𝐸↑2)) = (((𝐴↑2) − 1) · ((𝐴 Yrm (2 · 𝑄))↑2))
171168, 170oveq12i 7161 . . . . . 6 ((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = (((𝐴 Xrm (2 · 𝑄))↑2) − (((𝐴↑2) − 1) · ((𝐴 Yrm (2 · 𝑄))↑2)))
172 rmxynorm 39780 . . . . . . 7 ((𝐴 ∈ (ℤ‘2) ∧ (2 · 𝑄) ∈ ℤ) → (((𝐴 Xrm (2 · 𝑄))↑2) − (((𝐴↑2) − 1) · ((𝐴 Yrm (2 · 𝑄))↑2))) = 1)
1732, 19, 172syl2anc 587 . . . . . 6 (𝜑 → (((𝐴 Xrm (2 · 𝑄))↑2) − (((𝐴↑2) − 1) · ((𝐴 Yrm (2 · 𝑄))↑2))) = 1)
174171, 173syl5eq 2871 . . . . 5 (𝜑 → ((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = 1)
175167, 174, 823jca 1125 . . . 4 (𝜑 → (((𝐷↑2) − (((𝐴↑2) − 1) · (𝐶↑2))) = 1 ∧ ((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = 1 ∧ 𝐺 ∈ (ℤ‘2)))
17699oveq1i 7159 . . . . . . 7 (𝐼↑2) = ((𝐺 Xrm 𝐵)↑2)
17785oveq1i 7159 . . . . . . . 8 (𝐻↑2) = ((𝐺 Yrm 𝐵)↑2)
178177oveq2i 7160 . . . . . . 7 (((𝐺↑2) − 1) · (𝐻↑2)) = (((𝐺↑2) − 1) · ((𝐺 Yrm 𝐵)↑2))
179176, 178oveq12i 7161 . . . . . 6 ((𝐼↑2) − (((𝐺↑2) − 1) · (𝐻↑2))) = (((𝐺 Xrm 𝐵)↑2) − (((𝐺↑2) − 1) · ((𝐺 Yrm 𝐵)↑2)))
180 rmxynorm 39780 . . . . . . 7 ((𝐺 ∈ (ℤ‘2) ∧ 𝐵 ∈ ℤ) → (((𝐺 Xrm 𝐵)↑2) − (((𝐺↑2) − 1) · ((𝐺 Yrm 𝐵)↑2))) = 1)
18182, 4, 180syl2anc 587 . . . . . 6 (𝜑 → (((𝐺 Xrm 𝐵)↑2) − (((𝐺↑2) − 1) · ((𝐺 Yrm 𝐵)↑2))) = 1)
182179, 181syl5eq 2871 . . . . 5 (𝜑 → ((𝐼↑2) − (((𝐺↑2) − 1) · (𝐻↑2))) = 1)
183104a1i 11 . . . . . . . . 9 (𝜑𝐽 = ((𝐸 / (2 · (𝐶↑2))) − 1))
184183oveq1d 7164 . . . . . . . 8 (𝜑 → (𝐽 + 1) = (((𝐸 / (2 · (𝐶↑2))) − 1) + 1))
185143zcnd 12085 . . . . . . . . . 10 (𝜑𝐸 ∈ ℂ)
186154nncnd 11650 . . . . . . . . . 10 (𝜑 → (2 · (𝐶↑2)) ∈ ℂ)
187154nnne0d 11684 . . . . . . . . . 10 (𝜑 → (2 · (𝐶↑2)) ≠ 0)
188185, 186, 187divcld 11414 . . . . . . . . 9 (𝜑 → (𝐸 / (2 · (𝐶↑2))) ∈ ℂ)
189 ax-1cn 10593 . . . . . . . . 9 1 ∈ ℂ
190 npcan 10893 . . . . . . . . 9 (((𝐸 / (2 · (𝐶↑2))) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐸 / (2 · (𝐶↑2))) − 1) + 1) = (𝐸 / (2 · (𝐶↑2))))
191188, 189, 190sylancl 589 . . . . . . . 8 (𝜑 → (((𝐸 / (2 · (𝐶↑2))) − 1) + 1) = (𝐸 / (2 · (𝐶↑2))))
192184, 191eqtrd 2859 . . . . . . 7 (𝜑 → (𝐽 + 1) = (𝐸 / (2 · (𝐶↑2))))
193192oveq1d 7164 . . . . . 6 (𝜑 → ((𝐽 + 1) · (2 · (𝐶↑2))) = ((𝐸 / (2 · (𝐶↑2))) · (2 · (𝐶↑2))))
194185, 186, 187divcan1d 11415 . . . . . 6 (𝜑 → ((𝐸 / (2 · (𝐶↑2))) · (2 · (𝐶↑2))) = 𝐸)
195193, 194eqtr2d 2860 . . . . 5 (𝜑𝐸 = ((𝐽 + 1) · (2 · (𝐶↑2))))
19644nn0zd 12082 . . . . . . 7 (𝜑𝐹 ∈ ℤ)
19778nn0zd 12082 . . . . . . . 8 (𝜑 → ((𝐹↑2) − 𝐴) ∈ ℤ)
198196, 197zmulcld 12090 . . . . . . 7 (𝜑 → (𝐹 · ((𝐹↑2) − 𝐴)) ∈ ℤ)
199 dvdsmul1 15631 . . . . . . 7 ((𝐹 ∈ ℤ ∧ (𝐹 · ((𝐹↑2) − 𝐴)) ∈ ℤ) → 𝐹 ∥ (𝐹 · (𝐹 · ((𝐹↑2) − 𝐴))))
200196, 198, 199syl2anc 587 . . . . . 6 (𝜑𝐹 ∥ (𝐹 · (𝐹 · ((𝐹↑2) − 𝐴))))
20147oveq1i 7159 . . . . . . 7 (𝐺𝐴) = ((𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) − 𝐴)
20254nn0cnd 11954 . . . . . . . . 9 (𝜑𝐴 ∈ ℂ)
20379nn0cnd 11954 . . . . . . . . 9 (𝜑 → ((𝐹↑2) · ((𝐹↑2) − 𝐴)) ∈ ℂ)
204202, 203pncan2d 10997 . . . . . . . 8 (𝜑 → ((𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) − 𝐴) = ((𝐹↑2) · ((𝐹↑2) − 𝐴)))
20549oveq1d 7164 . . . . . . . 8 (𝜑 → ((𝐹↑2) · ((𝐹↑2) − 𝐴)) = ((𝐹 · 𝐹) · ((𝐹↑2) − 𝐴)))
20678nn0cnd 11954 . . . . . . . . 9 (𝜑 → ((𝐹↑2) − 𝐴) ∈ ℂ)
20748, 48, 206mulassd 10662 . . . . . . . 8 (𝜑 → ((𝐹 · 𝐹) · ((𝐹↑2) − 𝐴)) = (𝐹 · (𝐹 · ((𝐹↑2) − 𝐴))))
208204, 205, 2073eqtrd 2863 . . . . . . 7 (𝜑 → ((𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) − 𝐴) = (𝐹 · (𝐹 · ((𝐹↑2) − 𝐴))))
209201, 208syl5eq 2871 . . . . . 6 (𝜑 → (𝐺𝐴) = (𝐹 · (𝐹 · ((𝐹↑2) − 𝐴))))
210200, 209breqtrrd 5080 . . . . 5 (𝜑𝐹 ∥ (𝐺𝐴))
211182, 195, 2103jca 1125 . . . 4 (𝜑 → (((𝐼↑2) − (((𝐺↑2) − 1) · (𝐻↑2))) = 1 ∧ 𝐸 = ((𝐽 + 1) · (2 · (𝐶↑2))) ∧ 𝐹 ∥ (𝐺𝐴)))
212 zmulcl 12028 . . . . . . . 8 ((2 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (2 · 𝐶) ∈ ℤ)
21310, 14, 212sylancr 590 . . . . . . 7 (𝜑 → (2 · 𝐶) ∈ ℤ)
214 eluzelz 12250 . . . . . . . 8 (𝐴 ∈ (ℤ‘2) → 𝐴 ∈ ℤ)
2152, 214syl 17 . . . . . . 7 (𝜑𝐴 ∈ ℤ)
21679nn0zd 12082 . . . . . . 7 (𝜑 → ((𝐹↑2) · ((𝐹↑2) − 𝐴)) ∈ ℤ)
217 1z 12009 . . . . . . . 8 1 ∈ ℤ
218 zsubcl 12021 . . . . . . . . 9 ((1 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (1 − 𝐴) ∈ ℤ)
219217, 215, 218sylancr 590 . . . . . . . 8 (𝜑 → (1 − 𝐴) ∈ ℤ)
220 zmulcl 12028 . . . . . . . 8 ((1 ∈ ℤ ∧ (1 − 𝐴) ∈ ℤ) → (1 · (1 − 𝐴)) ∈ ℤ)
221217, 219, 220sylancr 590 . . . . . . 7 (𝜑 → (1 · (1 − 𝐴)) ∈ ℤ)
222 congid 39833 . . . . . . . 8 (((2 · 𝐶) ∈ ℤ ∧ 𝐴 ∈ ℤ) → (2 · 𝐶) ∥ (𝐴𝐴))
223213, 215, 222syl2anc 587 . . . . . . 7 (𝜑 → (2 · 𝐶) ∥ (𝐴𝐴))
22451nn0zd 12082 . . . . . . . 8 (𝜑 → (𝐹↑2) ∈ ℤ)
225217a1i 11 . . . . . . . 8 (𝜑 → 1 ∈ ℤ)
22613nncnd 11650 . . . . . . . . . . . . . . 15 (𝜑𝐶 ∈ ℂ)
227128, 226, 226mulassd 10662 . . . . . . . . . . . . . 14 (𝜑 → ((2 · 𝐶) · 𝐶) = (2 · (𝐶 · 𝐶)))
228226sqvald 13512 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶↑2) = (𝐶 · 𝐶))
229228oveq2d 7165 . . . . . . . . . . . . . 14 (𝜑 → (2 · (𝐶↑2)) = (2 · (𝐶 · 𝐶)))
230227, 229eqtr4d 2862 . . . . . . . . . . . . 13 (𝜑 → ((2 · 𝐶) · 𝐶) = (2 · (𝐶↑2)))
231230, 142eqbrtrd 5074 . . . . . . . . . . . 12 (𝜑 → ((2 · 𝐶) · 𝐶) ∥ 𝐸)
232 muldvds1 15634 . . . . . . . . . . . . 13 (((2 · 𝐶) ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝐸 ∈ ℤ) → (((2 · 𝐶) · 𝐶) ∥ 𝐸 → (2 · 𝐶) ∥ 𝐸))
233213, 14, 143, 232syl3anc 1368 . . . . . . . . . . . 12 (𝜑 → (((2 · 𝐶) · 𝐶) ∥ 𝐸 → (2 · 𝐶) ∥ 𝐸))
234231, 233mpd 15 . . . . . . . . . . 11 (𝜑 → (2 · 𝐶) ∥ 𝐸)
235 zsqcl 13499 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ)
236215, 235syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝐴↑2) ∈ ℤ)
237 peano2zm 12022 . . . . . . . . . . . . . 14 ((𝐴↑2) ∈ ℤ → ((𝐴↑2) − 1) ∈ ℤ)
238236, 237syl 17 . . . . . . . . . . . . 13 (𝜑 → ((𝐴↑2) − 1) ∈ ℤ)
239238, 143zmulcld 12090 . . . . . . . . . . . 12 (𝜑 → (((𝐴↑2) − 1) · 𝐸) ∈ ℤ)
240 dvdsmultr2 15649 . . . . . . . . . . . 12 (((2 · 𝐶) ∈ ℤ ∧ (((𝐴↑2) − 1) · 𝐸) ∈ ℤ ∧ 𝐸 ∈ ℤ) → ((2 · 𝐶) ∥ 𝐸 → (2 · 𝐶) ∥ ((((𝐴↑2) − 1) · 𝐸) · 𝐸)))
241213, 239, 143, 240syl3anc 1368 . . . . . . . . . . 11 (𝜑 → ((2 · 𝐶) ∥ 𝐸 → (2 · 𝐶) ∥ ((((𝐴↑2) − 1) · 𝐸) · 𝐸)))
242234, 241mpd 15 . . . . . . . . . 10 (𝜑 → (2 · 𝐶) ∥ ((((𝐴↑2) − 1) · 𝐸) · 𝐸))
243185sqvald 13512 . . . . . . . . . . . 12 (𝜑 → (𝐸↑2) = (𝐸 · 𝐸))
244243oveq2d 7165 . . . . . . . . . . 11 (𝜑 → (((𝐴↑2) − 1) · (𝐸↑2)) = (((𝐴↑2) − 1) · (𝐸 · 𝐸)))
245202sqcld 13513 . . . . . . . . . . . . 13 (𝜑 → (𝐴↑2) ∈ ℂ)
246 subcl 10883 . . . . . . . . . . . . 13 (((𝐴↑2) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐴↑2) − 1) ∈ ℂ)
247245, 189, 246sylancl 589 . . . . . . . . . . . 12 (𝜑 → ((𝐴↑2) − 1) ∈ ℂ)
248247, 185, 185mulassd 10662 . . . . . . . . . . 11 (𝜑 → ((((𝐴↑2) − 1) · 𝐸) · 𝐸) = (((𝐴↑2) − 1) · (𝐸 · 𝐸)))
249244, 248eqtr4d 2862 . . . . . . . . . 10 (𝜑 → (((𝐴↑2) − 1) · (𝐸↑2)) = ((((𝐴↑2) − 1) · 𝐸) · 𝐸))
250242, 249breqtrrd 5080 . . . . . . . . 9 (𝜑 → (2 · 𝐶) ∥ (((𝐴↑2) − 1) · (𝐸↑2)))
25148sqcld 13513 . . . . . . . . . . 11 (𝜑 → (𝐹↑2) ∈ ℂ)
252185sqcld 13513 . . . . . . . . . . . 12 (𝜑 → (𝐸↑2) ∈ ℂ)
253247, 252mulcld 10659 . . . . . . . . . . 11 (𝜑 → (((𝐴↑2) − 1) · (𝐸↑2)) ∈ ℂ)
254189a1i 11 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℂ)
255 subsub23 10889 . . . . . . . . . . 11 (((𝐹↑2) ∈ ℂ ∧ (((𝐴↑2) − 1) · (𝐸↑2)) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = 1 ↔ ((𝐹↑2) − 1) = (((𝐴↑2) − 1) · (𝐸↑2))))
256251, 253, 254, 255syl3anc 1368 . . . . . . . . . 10 (𝜑 → (((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = 1 ↔ ((𝐹↑2) − 1) = (((𝐴↑2) − 1) · (𝐸↑2))))
257174, 256mpbid 235 . . . . . . . . 9 (𝜑 → ((𝐹↑2) − 1) = (((𝐴↑2) − 1) · (𝐸↑2)))
258250, 257breqtrrd 5080 . . . . . . . 8 (𝜑 → (2 · 𝐶) ∥ ((𝐹↑2) − 1))
259 congsub 39832 . . . . . . . . 9 ((((2 · 𝐶) ∈ ℤ ∧ (𝐹↑2) ∈ ℤ ∧ 1 ∈ ℤ) ∧ (𝐴 ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ ((2 · 𝐶) ∥ ((𝐹↑2) − 1) ∧ (2 · 𝐶) ∥ (𝐴𝐴))) → (2 · 𝐶) ∥ (((𝐹↑2) − 𝐴) − (1 − 𝐴)))
260213, 224, 225, 215, 215, 258, 223, 259syl322anc 1395 . . . . . . . 8 (𝜑 → (2 · 𝐶) ∥ (((𝐹↑2) − 𝐴) − (1 − 𝐴)))
261 congmul 39829 . . . . . . . 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 1395 . . . . . . 7 (𝜑 → (2 · 𝐶) ∥ (((𝐹↑2) · ((𝐹↑2) − 𝐴)) − (1 · (1 − 𝐴))))
263 congadd 39828 . . . . . . 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 1395 . . . . . 6 (𝜑 → (2 · 𝐶) ∥ ((𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) − (𝐴 + (1 · (1 − 𝐴)))))
26547a1i 11 . . . . . . 7 (𝜑𝐺 = (𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))))
266219zcnd 12085 . . . . . . . . . 10 (𝜑 → (1 − 𝐴) ∈ ℂ)
267266mulid2d 10657 . . . . . . . . 9 (𝜑 → (1 · (1 − 𝐴)) = (1 − 𝐴))
268267oveq2d 7165 . . . . . . . 8 (𝜑 → (𝐴 + (1 · (1 − 𝐴))) = (𝐴 + (1 − 𝐴)))
269 pncan3 10892 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + (1 − 𝐴)) = 1)
270202, 189, 269sylancl 589 . . . . . . . 8 (𝜑 → (𝐴 + (1 − 𝐴)) = 1)
271268, 270eqtr2d 2860 . . . . . . 7 (𝜑 → 1 = (𝐴 + (1 · (1 − 𝐴))))
272265, 271oveq12d 7167 . . . . . 6 (𝜑 → (𝐺 − 1) = ((𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) − (𝐴 + (1 · (1 − 𝐴)))))
273264, 272breqtrrd 5080 . . . . 5 (𝜑 → (2 · 𝐶) ∥ (𝐺 − 1))
274 jm2.15nn0 39865 . . . . . . . 8 ((𝐺 ∈ (ℤ‘2) ∧ 𝐴 ∈ (ℤ‘2) ∧ 𝐵 ∈ ℕ0) → (𝐺𝐴) ∥ ((𝐺 Yrm 𝐵) − (𝐴 Yrm 𝐵)))
27582, 2, 90, 274syl3anc 1368 . . . . . . 7 (𝜑 → (𝐺𝐴) ∥ ((𝐺 Yrm 𝐵) − (𝐴 Yrm 𝐵)))
27685a1i 11 . . . . . . . 8 (𝜑𝐻 = (𝐺 Yrm 𝐵))
277276, 12oveq12d 7167 . . . . . . 7 (𝜑 → (𝐻𝐶) = ((𝐺 Yrm 𝐵) − (𝐴 Yrm 𝐵)))
278275, 277breqtrrd 5080 . . . . . 6 (𝜑 → (𝐺𝐴) ∥ (𝐻𝐶))
279 eluzelz 12250 . . . . . . . . 9 (𝐺 ∈ (ℤ‘2) → 𝐺 ∈ ℤ)
28082, 279syl 17 . . . . . . . 8 (𝜑𝐺 ∈ ℤ)
281280, 215zsubcld 12089 . . . . . . 7 (𝜑 → (𝐺𝐴) ∈ ℤ)
28285, 87eqeltrid 2920 . . . . . . . 8 (𝜑𝐻 ∈ ℤ)
283282, 14zsubcld 12089 . . . . . . 7 (𝜑 → (𝐻𝐶) ∈ ℤ)
284 dvdstr 15646 . . . . . . 7 ((𝐹 ∈ ℤ ∧ (𝐺𝐴) ∈ ℤ ∧ (𝐻𝐶) ∈ ℤ) → ((𝐹 ∥ (𝐺𝐴) ∧ (𝐺𝐴) ∥ (𝐻𝐶)) → 𝐹 ∥ (𝐻𝐶)))
285196, 281, 283, 284syl3anc 1368 . . . . . 6 (𝜑 → ((𝐹 ∥ (𝐺𝐴) ∧ (𝐺𝐴) ∥ (𝐻𝐶)) → 𝐹 ∥ (𝐻𝐶)))
286210, 278, 285mp2and 698 . . . . 5 (𝜑𝐹 ∥ (𝐻𝐶))
287 jm2.16nn0 39866 . . . . . . . . 9 ((𝐺 ∈ (ℤ‘2) ∧ 𝐵 ∈ ℕ0) → (𝐺 − 1) ∥ ((𝐺 Yrm 𝐵) − 𝐵))
28882, 90, 287syl2anc 587 . . . . . . . 8 (𝜑 → (𝐺 − 1) ∥ ((𝐺 Yrm 𝐵) − 𝐵))
28985oveq1i 7159 . . . . . . . 8 (𝐻𝐵) = ((𝐺 Yrm 𝐵) − 𝐵)
290288, 289breqtrrdi 5094 . . . . . . 7 (𝜑 → (𝐺 − 1) ∥ (𝐻𝐵))
291 peano2zm 12022 . . . . . . . . 9 (𝐺 ∈ ℤ → (𝐺 − 1) ∈ ℤ)
292280, 291syl 17 . . . . . . . 8 (𝜑 → (𝐺 − 1) ∈ ℤ)
293282, 4zsubcld 12089 . . . . . . . 8 (𝜑 → (𝐻𝐵) ∈ ℤ)
294 dvdstr 15646 . . . . . . . 8 (((2 · 𝐶) ∈ ℤ ∧ (𝐺 − 1) ∈ ℤ ∧ (𝐻𝐵) ∈ ℤ) → (((2 · 𝐶) ∥ (𝐺 − 1) ∧ (𝐺 − 1) ∥ (𝐻𝐵)) → (2 · 𝐶) ∥ (𝐻𝐵)))
295213, 292, 293, 294syl3anc 1368 . . . . . . 7 (𝜑 → (((2 · 𝐶) ∥ (𝐺 − 1) ∧ (𝐺 − 1) ∥ (𝐻𝐵)) → (2 · 𝐶) ∥ (𝐻𝐵)))
296273, 290, 295mp2and 698 . . . . . 6 (𝜑 → (2 · 𝐶) ∥ (𝐻𝐵))
297 rmygeid 39826 . . . . . . . 8 ((𝐴 ∈ (ℤ‘2) ∧ 𝐵 ∈ ℕ0) → 𝐵 ≤ (𝐴 Yrm 𝐵))
2982, 90, 297syl2anc 587 . . . . . . 7 (𝜑𝐵 ≤ (𝐴 Yrm 𝐵))
299298, 12breqtrrd 5080 . . . . . 6 (𝜑𝐵𝐶)
300296, 299jca 515 . . . . 5 (𝜑 → ((2 · 𝐶) ∥ (𝐻𝐵) ∧ 𝐵𝐶))
301273, 286, 300jca31 518 . . . 4 (𝜑 → (((2 · 𝐶) ∥ (𝐺 − 1) ∧ 𝐹 ∥ (𝐻𝐶)) ∧ ((2 · 𝐶) ∥ (𝐻𝐵) ∧ 𝐵𝐶)))
302175, 211, 301jca31 518 . . 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 515 . 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 518 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 209  wa 399  w3a 1084   = wceq 1538  wcel 2115   class class class wbr 5052  cfv 6343  (class class class)co 7149  cc 10533  0cc0 10535  1c1 10536   + caddc 10538   · cmul 10540   < clt 10673  cle 10674  cmin 10868   / cdiv 11295  cn 11634  2c2 11689  0cn0 11894  cz 11978  cuz 12240  cexp 13434  cdvds 15607   Xrm crmx 39762   Yrm crmy 39763
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455  ax-inf2 9101  ax-cnex 10591  ax-resscn 10592  ax-1cn 10593  ax-icn 10594  ax-addcl 10595  ax-addrcl 10596  ax-mulcl 10597  ax-mulrcl 10598  ax-mulcom 10599  ax-addass 10600  ax-mulass 10601  ax-distr 10602  ax-i2m1 10603  ax-1ne0 10604  ax-1rid 10605  ax-rnegex 10606  ax-rrecex 10607  ax-cnre 10608  ax-pre-lttri 10609  ax-pre-lttrn 10610  ax-pre-ltadd 10611  ax-pre-mulgt0 10612  ax-pre-sup 10613  ax-addf 10614  ax-mulf 10615
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-iin 4908  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-se 5502  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-isom 6352  df-riota 7107  df-ov 7152  df-oprab 7153  df-mpo 7154  df-of 7403  df-om 7575  df-1st 7684  df-2nd 7685  df-supp 7827  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-2o 8099  df-oadd 8102  df-omul 8103  df-er 8285  df-map 8404  df-pm 8405  df-ixp 8458  df-en 8506  df-dom 8507  df-sdom 8508  df-fin 8509  df-fsupp 8831  df-fi 8872  df-sup 8903  df-inf 8904  df-oi 8971  df-card 9365  df-acn 9368  df-pnf 10675  df-mnf 10676  df-xr 10677  df-ltxr 10678  df-le 10679  df-sub 10870  df-neg 10871  df-div 11296  df-nn 11635  df-2 11697  df-3 11698  df-4 11699  df-5 11700  df-6 11701  df-7 11702  df-8 11703  df-9 11704  df-n0 11895  df-xnn0 11965  df-z 11979  df-dec 12096  df-uz 12241  df-q 12346  df-rp 12387  df-xneg 12504  df-xadd 12505  df-xmul 12506  df-ioo 12739  df-ioc 12740  df-ico 12741  df-icc 12742  df-fz 12895  df-fzo 13038  df-fl 13166  df-mod 13242  df-seq 13374  df-exp 13435  df-fac 13639  df-bc 13668  df-hash 13696  df-shft 14426  df-cj 14458  df-re 14459  df-im 14460  df-sqrt 14594  df-abs 14595  df-limsup 14828  df-clim 14845  df-rlim 14846  df-sum 15043  df-ef 15421  df-sin 15423  df-cos 15424  df-pi 15426  df-dvds 15608  df-gcd 15842  df-prm 16014  df-numer 16073  df-denom 16074  df-struct 16485  df-ndx 16486  df-slot 16487  df-base 16489  df-sets 16490  df-ress 16491  df-plusg 16578  df-mulr 16579  df-starv 16580  df-sca 16581  df-vsca 16582  df-ip 16583  df-tset 16584  df-ple 16585  df-ds 16587  df-unif 16588  df-hom 16589  df-cco 16590  df-rest 16696  df-topn 16697  df-0g 16715  df-gsum 16716  df-topgen 16717  df-pt 16718  df-prds 16721  df-xrs 16775  df-qtop 16780  df-imas 16781  df-xps 16783  df-mre 16857  df-mrc 16858  df-acs 16860  df-mgm 17852  df-sgrp 17901  df-mnd 17912  df-submnd 17957  df-mulg 18225  df-cntz 18447  df-cmn 18908  df-psmet 20090  df-xmet 20091  df-met 20092  df-bl 20093  df-mopn 20094  df-fbas 20095  df-fg 20096  df-cnfld 20099  df-top 21506  df-topon 21523  df-topsp 21545  df-bases 21558  df-cld 21631  df-ntr 21632  df-cls 21633  df-nei 21710  df-lp 21748  df-perf 21749  df-cn 21839  df-cnp 21840  df-haus 21927  df-tx 22174  df-hmeo 22367  df-fil 22458  df-fm 22550  df-flim 22551  df-flf 22552  df-xms 22934  df-ms 22935  df-tms 22936  df-cncf 23490  df-limc 24476  df-dv 24477  df-log 25155  df-squarenn 39703  df-pell1qr 39704  df-pell14qr 39705  df-pell1234qr 39706  df-pellfund 39707  df-rmx 39764  df-rmy 39765
This theorem is referenced by:  jm2.27  39870
  Copyright terms: Public domain W3C validator