Metamath Proof Explorer

Theorem expdiophlem1

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

Ref Expression
Assertion expdiophlem1 
|- ( C e. NN0 -> ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN ) /\ C = ( A ^ B ) ) <-> E. d e. NN0 E. e e. NN0 E. f e. NN0 ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN ) /\ ( ( A e. ( ZZ>= ` 2 ) /\ d = ( A rmY ( B + 1 ) ) ) /\ ( ( d e. ( ZZ>= ` 2 ) /\ e = ( d rmY B ) ) /\ ( ( d e. ( ZZ>= ` 2 ) /\ f = ( d rmX B ) ) /\ ( C < ( ( ( ( 2 x. d ) x. A ) - ( A ^ 2 ) ) - 1 ) /\ ( ( ( ( 2 x. d ) x. A ) - ( A ^ 2 ) ) - 1 ) || ( ( f - ( ( d - A ) x. e ) ) - C ) ) ) ) ) ) ) )

Proof

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