Step |
Hyp |
Ref |
Expression |
1 |
|
bi2.04 |
|- ( ( x =/= 1 -> ( ( A / x ) e. NN -> x = A ) ) <-> ( ( A / x ) e. NN -> ( x =/= 1 -> x = A ) ) ) |
2 |
|
impexp |
|- ( ( ( x =/= 1 /\ ( A / x ) e. NN ) -> x = A ) <-> ( x =/= 1 -> ( ( A / x ) e. NN -> x = A ) ) ) |
3 |
|
neor |
|- ( ( x = 1 \/ x = A ) <-> ( x =/= 1 -> x = A ) ) |
4 |
3
|
imbi2i |
|- ( ( ( A / x ) e. NN -> ( x = 1 \/ x = A ) ) <-> ( ( A / x ) e. NN -> ( x =/= 1 -> x = A ) ) ) |
5 |
1 2 4
|
3bitr4ri |
|- ( ( ( A / x ) e. NN -> ( x = 1 \/ x = A ) ) <-> ( ( x =/= 1 /\ ( A / x ) e. NN ) -> x = A ) ) |
6 |
|
nngt1ne1 |
|- ( x e. NN -> ( 1 < x <-> x =/= 1 ) ) |
7 |
6
|
adantl |
|- ( ( A e. NN /\ x e. NN ) -> ( 1 < x <-> x =/= 1 ) ) |
8 |
7
|
anbi1d |
|- ( ( A e. NN /\ x e. NN ) -> ( ( 1 < x /\ ( A / x ) e. NN ) <-> ( x =/= 1 /\ ( A / x ) e. NN ) ) ) |
9 |
|
nnz |
|- ( ( A / x ) e. NN -> ( A / x ) e. ZZ ) |
10 |
|
nnre |
|- ( x e. NN -> x e. RR ) |
11 |
|
gtndiv |
|- ( ( x e. RR /\ A e. NN /\ A < x ) -> -. ( A / x ) e. ZZ ) |
12 |
11
|
3expia |
|- ( ( x e. RR /\ A e. NN ) -> ( A < x -> -. ( A / x ) e. ZZ ) ) |
13 |
10 12
|
sylan |
|- ( ( x e. NN /\ A e. NN ) -> ( A < x -> -. ( A / x ) e. ZZ ) ) |
14 |
13
|
con2d |
|- ( ( x e. NN /\ A e. NN ) -> ( ( A / x ) e. ZZ -> -. A < x ) ) |
15 |
|
nnre |
|- ( A e. NN -> A e. RR ) |
16 |
|
lenlt |
|- ( ( x e. RR /\ A e. RR ) -> ( x <_ A <-> -. A < x ) ) |
17 |
10 15 16
|
syl2an |
|- ( ( x e. NN /\ A e. NN ) -> ( x <_ A <-> -. A < x ) ) |
18 |
14 17
|
sylibrd |
|- ( ( x e. NN /\ A e. NN ) -> ( ( A / x ) e. ZZ -> x <_ A ) ) |
19 |
18
|
ancoms |
|- ( ( A e. NN /\ x e. NN ) -> ( ( A / x ) e. ZZ -> x <_ A ) ) |
20 |
9 19
|
syl5 |
|- ( ( A e. NN /\ x e. NN ) -> ( ( A / x ) e. NN -> x <_ A ) ) |
21 |
20
|
pm4.71rd |
|- ( ( A e. NN /\ x e. NN ) -> ( ( A / x ) e. NN <-> ( x <_ A /\ ( A / x ) e. NN ) ) ) |
22 |
21
|
anbi2d |
|- ( ( A e. NN /\ x e. NN ) -> ( ( 1 < x /\ ( A / x ) e. NN ) <-> ( 1 < x /\ ( x <_ A /\ ( A / x ) e. NN ) ) ) ) |
23 |
|
3anass |
|- ( ( 1 < x /\ x <_ A /\ ( A / x ) e. NN ) <-> ( 1 < x /\ ( x <_ A /\ ( A / x ) e. NN ) ) ) |
24 |
22 23
|
bitr4di |
|- ( ( A e. NN /\ x e. NN ) -> ( ( 1 < x /\ ( A / x ) e. NN ) <-> ( 1 < x /\ x <_ A /\ ( A / x ) e. NN ) ) ) |
25 |
8 24
|
bitr3d |
|- ( ( A e. NN /\ x e. NN ) -> ( ( x =/= 1 /\ ( A / x ) e. NN ) <-> ( 1 < x /\ x <_ A /\ ( A / x ) e. NN ) ) ) |
26 |
25
|
imbi1d |
|- ( ( A e. NN /\ x e. NN ) -> ( ( ( x =/= 1 /\ ( A / x ) e. NN ) -> x = A ) <-> ( ( 1 < x /\ x <_ A /\ ( A / x ) e. NN ) -> x = A ) ) ) |
27 |
5 26
|
syl5bb |
|- ( ( A e. NN /\ x e. NN ) -> ( ( ( A / x ) e. NN -> ( x = 1 \/ x = A ) ) <-> ( ( 1 < x /\ x <_ A /\ ( A / x ) e. NN ) -> x = A ) ) ) |
28 |
27
|
ralbidva |
|- ( A e. NN -> ( A. x e. NN ( ( A / x ) e. NN -> ( x = 1 \/ x = A ) ) <-> A. x e. NN ( ( 1 < x /\ x <_ A /\ ( A / x ) e. NN ) -> x = A ) ) ) |