# Metamath Proof Explorer

## Theorem expdiophlem1

Description: Lemma for expdioph . Fully expanded expression for exponential. (Contributed by Stefan O'Rear, 17-Oct-2014)

Ref Expression
Assertion expdiophlem1 ${⊢}{C}\in {ℕ}_{0}\to \left(\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\wedge {C}={{A}}^{{B}}\right)↔\exists {d}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\wedge \left(\left({A}\in {ℤ}_{\ge 2}\wedge {d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 2re ${⊢}2\in ℝ$
2 1 a1i ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\to 2\in ℝ$
3 nnre ${⊢}{B}\in ℕ\to {B}\in ℝ$
4 peano2re ${⊢}{B}\in ℝ\to {B}+1\in ℝ$
5 3 4 syl ${⊢}{B}\in ℕ\to {B}+1\in ℝ$
6 5 adantl ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\to {B}+1\in ℝ$
7 nnz ${⊢}{B}\in ℕ\to {B}\in ℤ$
8 7 peano2zd ${⊢}{B}\in ℕ\to {B}+1\in ℤ$
9 frmy ${⊢}{Y}_{\mathrm{rm}}:{ℤ}_{\ge 2}×ℤ⟶ℤ$
10 9 fovcl ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {B}+1\in ℤ\right)\to {A}{Y}_{\mathrm{rm}}\left({B}+1\right)\in ℤ$
11 8 10 sylan2 ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\to {A}{Y}_{\mathrm{rm}}\left({B}+1\right)\in ℤ$
12 11 zred ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\to {A}{Y}_{\mathrm{rm}}\left({B}+1\right)\in ℝ$
13 elnnuz ${⊢}{B}\in ℕ↔{B}\in {ℤ}_{\ge 1}$
14 eluzp1p1 ${⊢}{B}\in {ℤ}_{\ge 1}\to {B}+1\in {ℤ}_{\ge \left(1+1\right)}$
15 df-2 ${⊢}2=1+1$
16 15 fveq2i ${⊢}{ℤ}_{\ge 2}={ℤ}_{\ge \left(1+1\right)}$
17 14 16 eleqtrrdi ${⊢}{B}\in {ℤ}_{\ge 1}\to {B}+1\in {ℤ}_{\ge 2}$
18 13 17 sylbi ${⊢}{B}\in ℕ\to {B}+1\in {ℤ}_{\ge 2}$
19 eluzle ${⊢}{B}+1\in {ℤ}_{\ge 2}\to 2\le {B}+1$
20 18 19 syl ${⊢}{B}\in ℕ\to 2\le {B}+1$
21 20 adantl ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\to 2\le {B}+1$
22 nnnn0 ${⊢}{B}\in ℕ\to {B}\in {ℕ}_{0}$
23 peano2nn0 ${⊢}{B}\in {ℕ}_{0}\to {B}+1\in {ℕ}_{0}$
24 22 23 syl ${⊢}{B}\in ℕ\to {B}+1\in {ℕ}_{0}$
25 rmygeid ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {B}+1\in {ℕ}_{0}\right)\to {B}+1\le {A}{Y}_{\mathrm{rm}}\left({B}+1\right)$
26 24 25 sylan2 ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\to {B}+1\le {A}{Y}_{\mathrm{rm}}\left({B}+1\right)$
27 2 6 12 21 26 letrd ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\to 2\le {A}{Y}_{\mathrm{rm}}\left({B}+1\right)$
28 2z ${⊢}2\in ℤ$
29 eluz ${⊢}\left(2\in ℤ\wedge {A}{Y}_{\mathrm{rm}}\left({B}+1\right)\in ℤ\right)\to \left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\in {ℤ}_{\ge 2}↔2\le {A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)$
30 28 11 29 sylancr ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\to \left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\in {ℤ}_{\ge 2}↔2\le {A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)$
31 27 30 mpbird ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\to {A}{Y}_{\mathrm{rm}}\left({B}+1\right)\in {ℤ}_{\ge 2}$
32 31 adantl ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to {A}{Y}_{\mathrm{rm}}\left({B}+1\right)\in {ℤ}_{\ge 2}$
33 simprl ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to {A}\in {ℤ}_{\ge 2}$
34 simprr ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to {B}\in ℕ$
35 12 leidd ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\to {A}{Y}_{\mathrm{rm}}\left({B}+1\right)\le {A}{Y}_{\mathrm{rm}}\left({B}+1\right)$
36 35 adantl ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to {A}{Y}_{\mathrm{rm}}\left({B}+1\right)\le {A}{Y}_{\mathrm{rm}}\left({B}+1\right)$
37 jm3.1 ${⊢}\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\in {ℤ}_{\ge 2}\wedge {A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\wedge {A}{Y}_{\mathrm{rm}}\left({B}+1\right)\le {A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\to {{A}}^{{B}}=\left(\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\right)-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)\right)\mathrm{mod}\left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)$
38 32 33 34 36 37 syl31anc ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to {{A}}^{{B}}=\left(\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\right)-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)\right)\mathrm{mod}\left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)$
39 38 eqeq2d ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to \left({C}={{A}}^{{B}}↔{C}=\left(\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\right)-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)\right)\mathrm{mod}\left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\right)$
40 7 adantl ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\to {B}\in ℤ$
41 frmx ${⊢}{X}_{\mathrm{rm}}:{ℤ}_{\ge 2}×ℤ⟶{ℕ}_{0}$
42 41 fovcl ${⊢}\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\in {ℤ}_{\ge 2}\wedge {B}\in ℤ\right)\to \left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\in {ℕ}_{0}$
43 31 40 42 syl2anc ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\to \left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\in {ℕ}_{0}$
44 43 nn0zd ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\to \left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\in ℤ$
45 eluzelz ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}\in ℤ$
46 45 adantr ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\to {A}\in ℤ$
47 11 46 zsubcld ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\to \left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\in ℤ$
48 9 fovcl ${⊢}\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\in {ℤ}_{\ge 2}\wedge {B}\in ℤ\right)\to \left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\in ℤ$
49 31 40 48 syl2anc ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\to \left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\in ℤ$
50 47 49 zmulcld ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\to \left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)\in ℤ$
51 44 50 zsubcld ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\to \left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\right)-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)\in ℤ$
52 51 adantl ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to \left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\right)-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)\in ℤ$
53 32 33 34 36 jm3.1lem3 ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to 2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\in ℕ$
54 simpl ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to {C}\in {ℕ}_{0}$
55 divalgmodcl ${⊢}\left(\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\right)-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)\in ℤ\wedge 2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\in ℕ\wedge {C}\in {ℕ}_{0}\right)\to \left({C}=\left(\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\right)-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)\right)\mathrm{mod}\left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)↔\left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left(\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\right)-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)-{C}\right)\right)\right)$
56 52 53 54 55 syl3anc ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to \left({C}=\left(\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\right)-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)\right)\mathrm{mod}\left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)↔\left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left(\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\right)-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)-{C}\right)\right)\right)$
57 39 56 bitrd ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to \left({C}={{A}}^{{B}}↔\left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left(\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\right)-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)-{C}\right)\right)\right)$
58 rmynn0 ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {B}+1\in {ℕ}_{0}\right)\to {A}{Y}_{\mathrm{rm}}\left({B}+1\right)\in {ℕ}_{0}$
59 24 58 sylan2 ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\to {A}{Y}_{\mathrm{rm}}\left({B}+1\right)\in {ℕ}_{0}$
60 59 adantl ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to {A}{Y}_{\mathrm{rm}}\left({B}+1\right)\in {ℕ}_{0}$
61 oveq1 ${⊢}{d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\to {d}{Y}_{\mathrm{rm}}{B}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}$
62 61 eqeq2d ${⊢}{d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\to \left({e}={d}{Y}_{\mathrm{rm}}{B}↔{e}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)$
63 oveq1 ${⊢}{d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\to {d}{X}_{\mathrm{rm}}{B}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}$
64 63 eqeq2d ${⊢}{d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\to \left({f}={d}{X}_{\mathrm{rm}}{B}↔{f}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\right)$
65 oveq2 ${⊢}{d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\to 2{d}=2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)$
66 65 oveq1d ${⊢}{d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\to 2{d}{A}=2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}$
67 66 oveq1d ${⊢}{d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\to 2{d}{A}-{{A}}^{2}=2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}$
68 67 oveq1d ${⊢}{d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\to 2{d}{A}-{{A}}^{2}-1=2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1$
69 68 breq2d ${⊢}{d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\to \left({C}<2{d}{A}-{{A}}^{2}-1↔{C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)$
70 oveq1 ${⊢}{d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\to {d}-{A}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}$
71 70 oveq1d ${⊢}{d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\to \left({d}-{A}\right){e}=\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right){e}$
72 71 oveq2d ${⊢}{d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\to {f}-\left({d}-{A}\right){e}={f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right){e}$
73 72 oveq1d ${⊢}{d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\to {f}-\left({d}-{A}\right){e}-{C}={f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right){e}-{C}$
74 68 73 breq12d ${⊢}{d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\to \left(\left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)↔\left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left({f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right){e}-{C}\right)\right)$
75 69 74 anbi12d ${⊢}{d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\to \left(\left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)↔\left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left({f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right){e}-{C}\right)\right)\right)$
76 64 75 anbi12d ${⊢}{d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\to \left(\left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)↔\left({f}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\wedge \left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left({f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right){e}-{C}\right)\right)\right)\right)$
77 76 rexbidv ${⊢}{d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\to \left(\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)↔\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({f}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\wedge \left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left({f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right){e}-{C}\right)\right)\right)\right)$
78 62 77 anbi12d ${⊢}{d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\to \left(\left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)↔\left({e}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\wedge \exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({f}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\wedge \left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left({f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right){e}-{C}\right)\right)\right)\right)\right)$
79 78 rexbidv ${⊢}{d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\to \left(\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)↔\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({e}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\wedge \exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({f}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\wedge \left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left({f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right){e}-{C}\right)\right)\right)\right)\right)$
80 79 ceqsrexv ${⊢}{A}{Y}_{\mathrm{rm}}\left({B}+1\right)\in {ℕ}_{0}\to \left(\exists {d}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\wedge \exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)↔\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({e}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\wedge \exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({f}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\wedge \left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left({f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right){e}-{C}\right)\right)\right)\right)\right)$
81 60 80 syl ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to \left(\exists {d}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\wedge \exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)↔\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({e}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\wedge \exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({f}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\wedge \left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left({f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right){e}-{C}\right)\right)\right)\right)\right)$
82 22 ad2antll ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to {B}\in {ℕ}_{0}$
83 rmynn0 ${⊢}\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\in {ℤ}_{\ge 2}\wedge {B}\in {ℕ}_{0}\right)\to \left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\in {ℕ}_{0}$
84 32 82 83 syl2anc ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to \left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\in {ℕ}_{0}$
85 oveq2 ${⊢}{e}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\to \left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right){e}=\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)$
86 85 oveq2d ${⊢}{e}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\to {f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right){e}={f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)$
87 86 oveq1d ${⊢}{e}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\to {f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right){e}-{C}={f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)-{C}$
88 87 breq2d ${⊢}{e}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\to \left(\left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left({f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right){e}-{C}\right)↔\left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left({f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)-{C}\right)\right)$
89 88 anbi2d ${⊢}{e}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\to \left(\left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left({f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right){e}-{C}\right)\right)↔\left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left({f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)-{C}\right)\right)\right)$
90 89 anbi2d ${⊢}{e}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\to \left(\left({f}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\wedge \left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left({f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right){e}-{C}\right)\right)\right)↔\left({f}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\wedge \left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left({f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)-{C}\right)\right)\right)\right)$
91 90 rexbidv ${⊢}{e}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\to \left(\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({f}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\wedge \left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left({f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right){e}-{C}\right)\right)\right)↔\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({f}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\wedge \left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left({f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)-{C}\right)\right)\right)\right)$
92 91 ceqsrexv ${⊢}\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\in {ℕ}_{0}\to \left(\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({e}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\wedge \exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({f}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\wedge \left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left({f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right){e}-{C}\right)\right)\right)\right)↔\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({f}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\wedge \left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left({f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)-{C}\right)\right)\right)\right)$
93 84 92 syl ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to \left(\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({e}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\wedge \exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({f}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\wedge \left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left({f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right){e}-{C}\right)\right)\right)\right)↔\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({f}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\wedge \left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left({f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)-{C}\right)\right)\right)\right)$
94 7 ad2antll ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to {B}\in ℤ$
95 32 94 42 syl2anc ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to \left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\in {ℕ}_{0}$
96 oveq1 ${⊢}{f}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\to {f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)=\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\right)-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)$
97 96 oveq1d ${⊢}{f}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\to {f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)-{C}=\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\right)-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)-{C}$
98 97 breq2d ${⊢}{f}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\to \left(\left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left({f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)-{C}\right)↔\left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left(\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\right)-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)-{C}\right)\right)$
99 98 anbi2d ${⊢}{f}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\to \left(\left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left({f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)-{C}\right)\right)↔\left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left(\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\right)-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)-{C}\right)\right)\right)$
100 99 ceqsrexv ${⊢}\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\in {ℕ}_{0}\to \left(\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({f}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\wedge \left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left({f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)-{C}\right)\right)\right)↔\left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left(\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\right)-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)-{C}\right)\right)\right)$
101 95 100 syl ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to \left(\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({f}=\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\wedge \left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left({f}-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)-{C}\right)\right)\right)↔\left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left(\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\right)-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)-{C}\right)\right)\right)$
102 81 93 101 3bitrrd ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to \left(\left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left(\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\right)-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)-{C}\right)\right)↔\exists {d}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\wedge \exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)\right)$
103 r19.42v ${⊢}\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\wedge \left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)↔\left({d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\wedge \exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)$
104 r19.42v ${⊢}\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)↔\left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)$
105 104 anbi2i ${⊢}\left({d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\wedge \exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)↔\left({d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\wedge \left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)$
106 103 105 bitri ${⊢}\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\wedge \left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)↔\left({d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\wedge \left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)$
107 106 rexbii ${⊢}\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\wedge \left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)↔\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\wedge \left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)$
108 r19.42v ${⊢}\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\wedge \left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)↔\left({d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\wedge \exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)$
109 107 108 bitri ${⊢}\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\wedge \left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)↔\left({d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\wedge \exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)$
110 109 rexbii ${⊢}\exists {d}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\wedge \left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)↔\exists {d}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\wedge \exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)$
111 102 110 syl6bbr ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to \left(\left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left(\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\right)-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)-{C}\right)\right)↔\exists {d}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\wedge \left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)\right)$
112 eleq1 ${⊢}{d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\to \left({d}\in {ℤ}_{\ge 2}↔{A}{Y}_{\mathrm{rm}}\left({B}+1\right)\in {ℤ}_{\ge 2}\right)$
113 32 112 syl5ibrcom ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to \left({d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\to {d}\in {ℤ}_{\ge 2}\right)$
114 113 imp ${⊢}\left(\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\wedge {d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\to {d}\in {ℤ}_{\ge 2}$
115 ibar ${⊢}{d}\in {ℤ}_{\ge 2}\to \left({e}={d}{Y}_{\mathrm{rm}}{B}↔\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\right)$
116 ibar ${⊢}{d}\in {ℤ}_{\ge 2}\to \left({f}={d}{X}_{\mathrm{rm}}{B}↔\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\right)$
117 116 anbi1d ${⊢}{d}\in {ℤ}_{\ge 2}\to \left(\left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)↔\left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)$
118 115 117 anbi12d ${⊢}{d}\in {ℤ}_{\ge 2}\to \left(\left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)↔\left(\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)$
119 114 118 syl ${⊢}\left(\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\wedge {d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\to \left(\left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)↔\left(\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)$
120 119 pm5.32da ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to \left(\left({d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\wedge \left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)↔\left({d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)\right)$
121 ibar ${⊢}{A}\in {ℤ}_{\ge 2}\to \left({d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)↔\left({A}\in {ℤ}_{\ge 2}\wedge {d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\right)$
122 121 ad2antrl ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to \left({d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)↔\left({A}\in {ℤ}_{\ge 2}\wedge {d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\right)$
123 122 anbi1d ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to \left(\left({d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)↔\left(\left({A}\in {ℤ}_{\ge 2}\wedge {d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)\right)$
124 120 123 bitrd ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to \left(\left({d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\wedge \left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)↔\left(\left({A}\in {ℤ}_{\ge 2}\wedge {d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)\right)$
125 124 rexbidv ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to \left(\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\wedge \left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)↔\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)\right)$
126 125 2rexbidv ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to \left(\exists {d}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\wedge \left({e}={d}{Y}_{\mathrm{rm}}{B}\wedge \left({f}={d}{X}_{\mathrm{rm}}{B}\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)↔\exists {d}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)\right)$
127 111 126 bitrd ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to \left(\left({C}<2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\wedge \left(2\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){A}-{{A}}^{2}-1\right)\parallel \left(\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){X}_{\mathrm{rm}}{B}\right)-\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)-{A}\right)\left(\left({A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right){Y}_{\mathrm{rm}}{B}\right)-{C}\right)\right)↔\exists {d}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)\right)$
128 57 127 bitrd ${⊢}\left({C}\in {ℕ}_{0}\wedge \left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\right)\to \left({C}={{A}}^{{B}}↔\exists {d}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)\right)$
129 128 pm5.32da ${⊢}{C}\in {ℕ}_{0}\to \left(\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\wedge {C}={{A}}^{{B}}\right)↔\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\wedge \exists {d}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)\right)\right)$
130 r19.42v ${⊢}\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\wedge \left(\left({A}\in {ℤ}_{\ge 2}\wedge {d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)\right)↔\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\wedge \exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)\right)$
131 130 2rexbii ${⊢}\exists {d}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\wedge \left(\left({A}\in {ℤ}_{\ge 2}\wedge {d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)\right)↔\exists {d}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\wedge \exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)\right)$
132 r19.42v ${⊢}\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\wedge \exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)\right)↔\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\wedge \exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)\right)$
133 132 rexbii ${⊢}\exists {d}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\wedge \exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)\right)↔\exists {d}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\wedge \exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)\right)$
134 r19.42v ${⊢}\exists {d}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\wedge \exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)\right)↔\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\wedge \exists {d}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)\right)$
135 133 134 bitri ${⊢}\exists {d}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\wedge \exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)\right)↔\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\wedge \exists {d}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)\right)$
136 131 135 bitri ${⊢}\exists {d}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\wedge \left(\left({A}\in {ℤ}_{\ge 2}\wedge {d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)\right)↔\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\wedge \exists {d}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)\right)$
137 129 136 syl6bbr ${⊢}{C}\in {ℕ}_{0}\to \left(\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\wedge {C}={{A}}^{{B}}\right)↔\exists {d}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {e}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {f}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℕ\right)\wedge \left(\left({A}\in {ℤ}_{\ge 2}\wedge {d}={A}{Y}_{\mathrm{rm}}\left({B}+1\right)\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {e}={d}{Y}_{\mathrm{rm}}{B}\right)\wedge \left(\left({d}\in {ℤ}_{\ge 2}\wedge {f}={d}{X}_{\mathrm{rm}}{B}\right)\wedge \left({C}<2{d}{A}-{{A}}^{2}-1\wedge \left(2{d}{A}-{{A}}^{2}-1\right)\parallel \left({f}-\left({d}-{A}\right){e}-{C}\right)\right)\right)\right)\right)\right)\right)$