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 ) ∥ ( ( 𝑓 − ( ( 𝑑 − 𝐴 ) · 𝑒 ) ) − 𝐶 ) ) ) ) ) ) ) )