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 ( 𝐶 ∈ ℕ0 → ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℕ ) ∧ 𝐶 = ( 𝐴 ↑ 𝐵 ) ) ↔ ∃ 𝑑 ∈ ℕ0 ∃ 𝑒 ∈ ℕ0 ∃ 𝑓 ∈ ℕ0 ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℕ ) ∧ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑑 = ( 𝐴 Yrm ( 𝐵 + 1 ) ) ) ∧ ( ( 𝑑 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑒 = ( 𝑑 Yrm 𝐵 ) ) ∧ ( ( 𝑑 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑓 = ( 𝑑 Xrm 𝐵 ) ) ∧ ( 𝐶 < ( ( ( ( 2 · 𝑑 ) · 𝐴 ) − ( 𝐴 ↑ 2 ) ) − 1 ) ∧ ( ( ( ( 2 · 𝑑 ) · 𝐴 ) − ( 𝐴 ↑ 2 ) ) − 1 ) ∥ ( ( 𝑓 − ( ( 𝑑 − 𝐴 ) · 𝑒 ) ) − 𝐶 ) ) ) ) ) ) ) )

Proof

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