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 (((A \in ℤ_{\geq 2} \land B \in ℕ) \land C = A^{B}) \leftrightarrow \exists d \in ℕ_{0} \exists e \in ℕ_{0} \exists f \in ℕ_{0} ((A \in ℤ_{\geq 2} \land B \in ℕ) \land ((A \in ℤ_{\geq 2} \land d = A Y_{rm} (B + 1)) \land ((d \in ℤ_{\geq 2} \land e = d Y_{rm} B) \land ((d \in ℤ_{\geq 2} \land f = d X_{rm} B) \land (C < 2 d A - A^{2} - 1 \land (2 d A - A^{2} - 1) ∥ (f - (d - A) e - C)))))))$

Proof

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

Metamath Proof Explorer

Theorem expdiophlem1

Proof