HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem expcnv 9385
Description: A sequence of powers of a complex number A with absolute value smaller than 1 converges to zero. (The proof was shortened by Mario Carneiro, 26-Apr-2014.)
Hypotheses
Ref Expression
expcnv.1 |- (ph -> A e. CC)
expcnv.2 |- (ph -> (abs` A) < 1)
Assertion
Ref Expression
expcnv |- (ph -> (n e. NN0 |-> (A^n)) ~~> 0)
Distinct variable group:   A,n
Allowed substitution hint:   ph(n)

Proof of Theorem expcnv
StepHypRef Expression
1 nnuz 8064 . . 3 |- NN = (ZZ>=` 1)
2 1z 7940 . . . 4 |- 1 e. ZZ
32a1i 10 . . 3 |- ((ph /\ A = 0) -> 1 e. ZZ)
4 nn0ex 7874 . . . . 5 |- NN0 e. _V
54mptex 5088 . . . 4 |- (n e. NN0 |-> (A^n)) e. _V
65a1i 10 . . 3 |- ((ph /\ A = 0) -> (n e. NN0 |-> (A^n)) e. _V)
7 0cn 7090 . . . 4 |- 0 e. CC
87a1i 10 . . 3 |- ((ph /\ A = 0) -> 0 e. CC)
9 nnnn0 7875 . . . . . 6 |- (k e. NN -> k e. NN0)
10 oveq2 4928 . . . . . . 7 |- (n = k -> (A^n) = (A^k))
11 eqid 1938 . . . . . . 7 |- (n e. NN0 |-> (A^n)) = (n e. NN0 |-> (A^n))
12 ovex 4944 . . . . . . 7 |- (A^k) e. _V
1310, 11, 12fvmpt 5104 . . . . . 6 |- (k e. NN0 -> ((n e. NN0 |-> (A^n))` k) = (A^k))
149, 13syl 14 . . . . 5 |- (k e. NN -> ((n e. NN0 |-> (A^n))` k) = (A^k))
15 simpr 447 . . . . . 6 |- ((ph /\ A = 0) -> A = 0)
1615oveq1d 4934 . . . . 5 |- ((ph /\ A = 0) -> (A^k) = (0^k))
1714, 16sylan9eqr 1992 . . . 4 |- (((ph /\ A = 0) /\ k e. NN) -> ((n e. NN0 |-> (A^n))` k) = (0^k))
18 0exp 8651 . . . . 5 |- (k e. NN -> (0^k) = 0)
1918adantl 453 . . . 4 |- (((ph /\ A = 0) /\ k e. NN) -> (0^k) = 0)
2017, 19eqtrd 1970 . . 3 |- (((ph /\ A = 0) /\ k e. NN) -> ((n e. NN0 |-> (A^n))` k) = 0)
211, 3, 6, 8, 20climconst 9153 . 2 |- ((ph /\ A = 0) -> (n e. NN0 |-> (A^n)) ~~> 0)
222a1i 10 . . . 4 |- ((ph /\ A =/= 0) -> 1 e. ZZ)
237a1i 10 . . . 4 |- ((ph /\ A =/= 0) -> 0 e. CC)
24 expcnv.2 . . . . . . . . . . 11 |- (ph -> (abs` A) < 1)
2524adantr 452 . . . . . . . . . 10 |- ((ph /\ A =/= 0) -> (abs` A) < 1)
26 expcnv.1 . . . . . . . . . . . 12 |- (ph -> A e. CC)
27 absrpcl 9026 . . . . . . . . . . . 12 |- ((A e. CC /\ A =/= 0) -> (abs`
A) e. RR+)
2826, 27sylan 458 . . . . . . . . . . 11 |- ((ph /\ A =/= 0) -> (abs` A) e. RR+)
29 elrp 8241 . . . . . . . . . . . 12 |- ((abs` A) e. RR+ <-> ((abs` A) e. RR /\ 0 < (abs` A)))
30 reclt1 7641 . . . . . . . . . . . 12 |- (((abs` A) e. RR /\ 0 < (abs` A)) -> ((abs` A) < 1 <-> 1 < (1 / (abs` A))))
3129, 30sylbi 185 . . . . . . . . . . 11 |- ((abs` A) e. RR+ -> ((abs` A) < 1 <-> 1 < (1 / (abs` A))))
3228, 31syl 14 . . . . . . . . . 10 |- ((ph /\ A =/= 0) -> ((abs` A) < 1 <-> 1 < (1 / (abs` A))))
3325, 32mpbid 199 . . . . . . . . 9 |- ((ph /\ A =/= 0) -> 1 < (1 / (abs` A)))
34 1re 7098 . . . . . . . . . 10 |- 1 e. RR
35 rpreccl 8260 . . . . . . . . . . . 12 |- ((abs` A) e. RR+ -> (1 / (abs`
A)) e. RR+)
3628, 35syl 14 . . . . . . . . . . 11 |- ((ph /\ A =/= 0) -> (1 / (abs` A)) e. RR+)
37 rpre 8244 . . . . . . . . . . 11 |- ((1 / (abs` A)) e. RR+ -> (1 / (abs`
A)) e. RR)
3836, 37syl 14 . . . . . . . . . 10 |- ((ph /\ A =/= 0) -> (1 / (abs` A)) e. RR)
39 difrp 8268 . . . . . . . . . 10 |- ((1 e. RR /\ (1 / (abs` A)) e. RR) -> (1 < (1 / (abs` A)) <-> ((1 / (abs`
A)) - 1) e. RR+))
4034, 38, 39sylancr 647 . . . . . . . . 9 |- ((ph /\ A =/= 0) -> (1 < (1 / (abs`
A)) <-> ((1 / (abs` A)) - 1) e. RR+))
4133, 40mpbid 199 . . . . . . . 8 |- ((ph /\ A =/= 0) -> ((1 / (abs` A)) - 1) e. RR+)
42 rpreccl 8260 . . . . . . . 8 |- (((1 / (abs` A)) - 1) e. RR+ -> (1 / ((1 / (abs` A)) - 1)) e. RR+)
4341, 42syl 14 . . . . . . 7 |- ((ph /\ A =/= 0) -> (1 / ((1 / (abs` A)) - 1)) e. RR+)
44 rpre 8244 . . . . . . 7 |- ((1 / ((1 / (abs` A)) - 1)) e. RR+ -> (1 / ((1 / (abs`
A)) - 1)) e. RR)
4543, 44syl 14 . . . . . 6 |- ((ph /\ A =/= 0) -> (1 / ((1 / (abs` A)) - 1)) e. RR)
4645recnd 7080 . . . . 5 |- ((ph /\ A =/= 0) -> (1 / ((1 / (abs` A)) - 1)) e. CC)
47 divcnv 9379 . . . . 5 |- ((1 / ((1 / (abs` A)) - 1)) e. CC -> (n e. NN |-> ((1 / ((1 / (abs` A)) - 1)) / n)) ~~> 0)
4846, 47syl 14 . . . 4 |- ((ph /\ A =/= 0) -> (n e. NN |-> ((1 / ((1 / (abs` A)) - 1)) / n)) ~~> 0)
49 nnex 7700 . . . . . 6 |- NN e. _V
5049mptex 5088 . . . . 5 |- (n e. NN |-> ((abs` A)^n)) e. _V
5150a1i 10 . . . 4 |- ((ph /\ A =/= 0) -> (n e. NN |-> ((abs` A)^n)) e. _V)
52 oveq2 4928 . . . . . . 7 |- (n = k -> ((1 / ((1 / (abs` A)) - 1)) / n) = ((1 / ((1 / (abs`
A)) - 1)) / k))
53 eqid 1938 . . . . . . 7 |- (n e. NN |-> ((1 / ((1 / (abs` A)) - 1)) / n)) = (n e. NN |-> ((1 / ((1 / (abs` A)) - 1)) / n))
54 ovex 4944 . . . . . . 7 |- ((1 / ((1 / (abs` A)) - 1)) / k) e. _V
5552, 53, 54fvmpt 5104 . . . . . 6 |- (k e. NN -> ((n e. NN |-> ((1 / ((1 / (abs`
A)) - 1)) / n))` k) = ((1 / ((1 / (abs` A)) - 1)) / k))
5655adantl 453 . . . . 5 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((n e. NN |-> ((1 / ((1 / (abs` A)) - 1)) / n))` k) = ((1 / ((1 / (abs`
A)) - 1)) / k))
57 nndivre 7729 . . . . . 6 |- (((1 / ((1 / (abs` A)) - 1)) e. RR /\ k e. NN) -> ((1 / ((1 / (abs`
A)) - 1)) / k) e. RR)
5845, 57sylan 458 . . . . 5 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((1 / ((1 / (abs`
A)) - 1)) / k) e. RR)
5956, 58eqeltrd 2011 . . . 4 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((n e. NN |-> ((1 / ((1 / (abs` A)) - 1)) / n))` k) e. RR)
60 oveq2 4928 . . . . . . . 8 |- (n = k -> ((abs` A)^n) = ((abs` A)^k))
61 eqid 1938 . . . . . . . 8 |- (n e. NN |-> ((abs` A)^n)) = (n e. NN |-> ((abs` A)^n))
62 ovex 4944 . . . . . . . 8 |- ((abs` A)^k) e. _V
6360, 61, 62fvmpt 5104 . . . . . . 7 |- (k e. NN -> ((n e. NN |-> ((abs` A)^n))` k) = ((abs` A)^k))
6463adantl 453 . . . . . 6 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((n e. NN |-> ((abs` A)^n))` k) = ((abs` A)^k))
65 nnz 7932 . . . . . . 7 |- (k e. NN -> k e. ZZ)
66 rpexpcl 8639 . . . . . . 7 |- (((abs` A) e. RR+ /\ k e. ZZ) -> ((abs` A)^k) e. RR+)
6728, 65, 66syl2an 464 . . . . . 6 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((abs` A)^k) e. RR+)
6864, 67eqeltrd 2011 . . . . 5 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((n e. NN |-> ((abs` A)^n))` k) e. RR+)
69 rpre 8244 . . . . 5 |- (((n e. NN |-> ((abs` A)^n))` k) e. RR+ -> ((n e. NN |-> ((abs` A)^n))` k) e. RR)
7068, 69syl 14 . . . 4 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((n e. NN |-> ((abs` A)^n))` k) e. RR)
71 nnrp 8246 . . . . . . . . . . 11 |- (k e. NN -> k e. RR+)
72 rpmulcl 8258 . . . . . . . . . . 11 |- ((((1 / (abs` A)) - 1) e. RR+ /\ k e. RR+) -> (((1 / (abs` A)) - 1) x. k) e. RR+)
7341, 71, 72syl2an 464 . . . . . . . . . 10 |- (((ph /\ A =/= 0) /\ k e. NN) -> (((1 / (abs` A)) - 1) x. k) e. RR+)
74 rpre 8244 . . . . . . . . . 10 |- ((((1 / (abs` A)) - 1) x. k) e. RR+ -> (((1 / (abs` A)) - 1) x. k) e. RR)
7573, 74syl 14 . . . . . . . . 9 |- (((ph /\ A =/= 0) /\ k e. NN) -> (((1 / (abs` A)) - 1) x. k) e. RR)
76 peano2re 7193 . . . . . . . . . 10 |- ((((1 / (abs` A)) - 1) x. k) e. RR -> ((((1 / (abs`
A)) - 1) x. k) + 1) e. RR)
7775, 76syl 14 . . . . . . . . 9 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((((1 / (abs` A)) - 1) x. k) + 1) e. RR)
78 rpexpcl 8639 . . . . . . . . . . 11 |- (((1 / (abs` A)) e. RR+ /\ k e. ZZ) -> ((1 / (abs`
A))^k) e. RR+)
7936, 65, 78syl2an 464 . . . . . . . . . 10 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((1 / (abs`
A))^k) e. RR+)
80 rpre 8244 . . . . . . . . . 10 |- (((1 / (abs` A))^k) e. RR+ -> ((1 / (abs` A))^k) e. RR)
8179, 80syl 14 . . . . . . . . 9 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((1 / (abs`
A))^k) e. RR)
82 lep1 7563 . . . . . . . . . 10 |- ((((1 / (abs` A)) - 1) x. k) e. RR -> (((1 / (abs` A)) - 1) x. k) <_ ((((1 / (abs` A)) - 1) x. k) + 1))
8375, 82syl 14 . . . . . . . . 9 |- (((ph /\ A =/= 0) /\ k e. NN) -> (((1 / (abs` A)) - 1) x. k) <_ ((((1 / (abs` A)) - 1) x. k) + 1))
8438adantr 452 . . . . . . . . . 10 |- (((ph /\ A =/= 0) /\ k e. NN) -> (1 / (abs` A)) e. RR)
859adantl 453 . . . . . . . . . 10 |- (((ph /\ A =/= 0) /\ k e. NN) -> k e. NN0)
86 rpge0 8249 . . . . . . . . . . . 12 |- ((1 / (abs` A)) e. RR+ -> 0 <_ (1 / (abs` A)))
8736, 86syl 14 . . . . . . . . . . 11 |- ((ph /\ A =/= 0) -> 0 <_ (1 / (abs` A)))
8887adantr 452 . . . . . . . . . 10 |- (((ph /\ A =/= 0) /\ k e. NN) -> 0 <_ (1 / (abs` A)))
89 bernneq2 8735 . . . . . . . . . 10 |- (((1 / (abs` A)) e. RR /\ k e. NN0 /\ 0 <_ (1 / (abs`
A))) -> ((((1 / (abs` A)) - 1) x. k) + 1) <_ ((1 / (abs` A))^k))
9084, 85, 88, 89syl3anc 1162 . . . . . . . . 9 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((((1 / (abs` A)) - 1) x. k) + 1) <_ ((1 / (abs` A))^k))
9175, 77, 81, 83, 90letrd 7145 . . . . . . . 8 |- (((ph /\ A =/= 0) /\ k e. NN) -> (((1 / (abs` A)) - 1) x. k) <_ ((1 / (abs` A))^k))
92 rpcnne0 8254 . . . . . . . . . 10 |- ((abs` A) e. RR+ -> ((abs` A) e. CC /\ (abs` A) =/= 0))
9328, 92syl 14 . . . . . . . . 9 |- ((ph /\ A =/= 0) -> ((abs` A) e. CC /\ (abs` A) =/= 0))
94 exprec 8657 . . . . . . . . . 10 |- (((abs` A) e. CC /\ (abs` A) =/= 0 /\ k e. ZZ) -> ((1 / (abs`
A))^k) = (1 / ((abs` A)^k)))
95943expa 1132 . . . . . . . . 9 |- ((((abs`
A) e. CC /\ (abs`
A) =/= 0) /\ k e. ZZ) -> ((1 / (abs` A))^k) = (1 / ((abs` A)^k)))
9693, 65, 95syl2an 464 . . . . . . . 8 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((1 / (abs`
A))^k) = (1 / ((abs` A)^k)))
9791, 96breqtrd 3386 . . . . . . 7 |- (((ph /\ A =/= 0) /\ k e. NN) -> (((1 / (abs` A)) - 1) x. k) <_ (1 / ((abs` A)^k)))
98 elrp 8241 . . . . . . . . 9 |- ((((1 / (abs` A)) - 1) x. k) e. RR+ <-> ((((1 / (abs` A)) - 1) x. k) e. RR /\ 0 < (((1 / (abs`
A)) - 1) x. k)))
99 elrp 8241 . . . . . . . . 9 |- (((abs` A)^k) e. RR+ <-> (((abs` A)^k) e. RR /\ 0 < ((abs` A)^k)))
100 lerec2 7632 . . . . . . . . 9 |- ((((((1 / (abs` A)) - 1) x. k) e. RR /\ 0 < (((1 / (abs` A)) - 1) x. k)) /\ (((abs` A)^k) e. RR /\ 0 < ((abs` A)^k))) -> ((((1 / (abs`
A)) - 1) x. k) <_ (1 / ((abs` A)^k)) <-> ((abs` A)^k) <_ (1 / (((1 / (abs`
A)) - 1) x. k))))
10198, 99, 100syl2anb 466 . . . . . . . 8 |- (((((1 / (abs`
A)) - 1) x. k) e. RR+ /\ ((abs`
A)^k) e. RR+) -> ((((1 / (abs` A)) - 1) x. k) <_ (1 / ((abs` A)^k)) <-> ((abs` A)^k) <_ (1 / (((1 / (abs` A)) - 1) x. k))))
10273, 67, 101syl2anc 645 . . . . . . 7 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((((1 / (abs` A)) - 1) x. k) <_ (1 / ((abs` A)^k)) <-> ((abs` A)^k) <_ (1 / (((1 / (abs` A)) - 1) x. k))))
10397, 102mpbid 199 . . . . . 6 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((abs` A)^k) <_ (1 / (((1 / (abs` A)) - 1) x. k)))
104 rpcnne0 8254 . . . . . . . 8 |- (((1 / (abs` A)) - 1) e. RR+ -> (((1 / (abs` A)) - 1) e. CC /\ ((1 / (abs` A)) - 1) =/= 0))
10541, 104syl 14 . . . . . . 7 |- ((ph /\ A =/= 0) -> (((1 / (abs` A)) - 1) e. CC /\ ((1 / (abs` A)) - 1) =/= 0))
106 nncn 7705 . . . . . . . 8 |- (k e. NN -> k e. CC)
107 nnne0 7726 . . . . . . . 8 |- (k e. NN -> k =/= 0)
108106, 107jca 521 . . . . . . 7 |- (k e. NN -> (k e. CC /\ k =/= 0))
109 recdiv2 7545 . . . . . . 7 |- (((((1 / (abs`
A)) - 1) e. CC /\ ((1 / (abs`
A)) - 1) =/= 0) /\ (k e. CC /\ k =/= 0)) -> ((1 / ((1 / (abs`
A)) - 1)) / k) = (1 / (((1 / (abs` A)) - 1) x. k)))
110105, 108, 109syl2an 464 . . . . . 6 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((1 / ((1 / (abs`
A)) - 1)) / k) = (1 / (((1 / (abs` A)) - 1) x. k)))
111103, 110breqtrrd 3388 . . . . 5 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((abs` A)^k) <_ ((1 / ((1 / (abs` A)) - 1)) / k))
112111, 64, 563brtr4d 3392 . . . 4 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((n e. NN |-> ((abs` A)^n))` k) <_ ((n e. NN |-> ((1 / ((1 / (abs` A)) - 1)) / n))` k))
113 rpge0 8249 . . . . 5 |- (((n e. NN |-> ((abs` A)^n))` k) e. RR+ -> 0 <_ ((n e. NN |-> ((abs` A)^n))` k))
11468, 113syl 14 . . . 4 |- (((ph /\ A =/= 0) /\ k e. NN) -> 0 <_ ((n e. NN |-> ((abs` A)^n))` k))
1151, 22, 23, 48, 51, 59, 70, 112, 114climsqz2 9207 . . 3 |- ((ph /\ A =/= 0) -> (n e. NN |-> ((abs` A)^n)) ~~> 0)
1162a1i 10 . . . . 5 |- (ph -> 1 e. ZZ)
1175a1i 10 . . . . 5 |- (ph -> (n e. NN0 |-> (A^n)) e. _V)
11850a1i 10 . . . . 5 |- (ph -> (n e. NN |-> ((abs` A)^n)) e. _V)
1199adantl 453 . . . . . . 7 |- ((ph /\ k e. NN) -> k e. NN0)
120119, 13syl 14 . . . . . 6 |- ((ph /\ k e. NN) -> ((n e. NN0 |-> (A^n))` k) = (A^k))
121 expcl 8638 . . . . . . 7 |- ((A e. CC /\ k e. NN0) -> (A^k) e. CC)
12226, 9, 121syl2an 464 . . . . . 6 |- ((ph /\ k e. NN) -> (A^k) e. CC)
123120, 122eqeltrd 2011 . . . . 5 |- ((ph /\ k e. NN) -> ((n e. NN0 |-> (A^n))` k) e. CC)
124 absexp 9040 . . . . . . 7 |- ((A e. CC /\ k e. NN0) -> (abs` (A^k)) = ((abs` A)^k))
12526, 9, 124syl2an 464 . . . . . 6 |- ((ph /\ k e. NN) -> (abs` (A^k)) = ((abs` A)^k))
126120fveq2d 4676 . . . . . 6 |- ((ph /\ k e. NN) -> (abs` ((n e. NN0 |-> (A^n))` k)) = (abs` (A^k)))
12763adantl 453 . . . . . 6 |- ((ph /\ k e. NN) -> ((n e. NN |-> ((abs` A)^n))` k) = ((abs` A)^k))
128125, 126, 1273eqtr4rd 1981 . . . . 5 |- ((ph /\ k e. NN) -> ((n e. NN |-> ((abs` A)^n))` k) = (abs`
((n e. NN0 |-> (A^n))` k)))
1291, 116, 117, 118, 123, 128climabs0 9182 . . . 4 |- (ph -> ((n e. NN0 |-> (A^n)) ~~> 0 <-> (n e. NN |-> ((abs` A)^n)) ~~> 0))
130129biimpar 472 . . 3 |- ((ph /\ (n e. NN |-> ((abs` A)^n)) ~~> 0) -> (n e. NN0 |-> (A^n)) ~~> 0)
131115, 130syldan 457 . 2 |- ((ph /\ A =/= 0) -> (n e. NN0 |-> (A^n)) ~~> 0)
13221, 131pm2.61dane 2130 1 |- (ph -> (n e. NN0 |-> (A^n)) ~~> 0)
Colors of variables: wff set class
Syntax hints:   -> wi 4   <-> wb 174   /\ wa 361   = wceq 1434   e. wcel 1436   =/= wne 2056  _Vcvv 2343   class class class wbr 3362  ` cfv 4007  (class class class)co 4922   e. cmpt 5057  CCcc 6990  RRcr 6991  0cc0 6992  1c1 6993   + caddc 6995   x. cmul 6997   <_ cle 7100   < clt 7104   - cmin 7215   / cdiv 7217  NNcn 7218  NN0cn0 7219  ZZcz 7220  RR+crp 7222  ^cexp 8621  abscabs 8949   ~~> cli 9116
This theorem is referenced by:  explecnv 9386  geolim 9388  geo2lim 9392  mbfi1fseqlem6 12290  geomcau 17235
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1351  ax-6 1352  ax-7 1353  ax-gen 1354  ax-8 1438  ax-10 1439  ax-11 1440  ax-12 1441  ax-13 1442  ax-14 1443  ax-17 1450  ax-9 1465  ax-4 1471  ax-16 1649  ax-ext 1920  ax-rep 3448  ax-sep 3458  ax-nul 3467  ax-pow 3503  ax-pr 3527  ax-un 3799  ax-inf2 6064  ax-resscn 7046  ax-1cn 7047  ax-icn 7048  ax-addcl 7049  ax-addrcl 7050  ax-mulcl 7051  ax-mulrcl 7052  ax-mulcom 7053  ax-addass 7054  ax-mulass 7055  ax-distr 7056  ax-i2m1 7057  ax-1ne0 7058  ax-1rid 7059  ax-rnegex 7060  ax-rrecex 7061  ax-cnre 7062  ax-pre-lttri 7063  ax-pre-lttrn 7064  ax-pre-ltadd 7065  ax-pre-mulgt0 7066  ax-pre-sup 7067
This theorem depends on definitions:  df-bi 175  df-or 362  df-an 363  df-3or 922  df-3an 923  df-tru 1329  df-ex 1356  df-sb 1611  df-eu 1838  df-mo 1839  df-clab 1926  df-cleq 1931  df-clel 1934  df-ne 2058  df-nel 2059  df-ral 2151  df-rex 2152  df-reu 2153  df-rab 2154  df-v 2345  df-sbc 2510  df-csb 2585  df-dif 2645  df-un 2647  df-in 2649  df-ss 2651  df-pss 2653  df-nul 2907  df-if 3009  df-pw 3067  df-sn 3084  df-pr 3085  df-tp 3086  df-op 3087  df-uni 3218  df-iun 3290  df-br 3363  df-opab 3417  df-tr 3432  df-eprel 3612  df-id 3615  df-po 3620  df-so 3634  df-fr 3653  df-we 3669  df-ord 3685  df-on 3686  df-lim 3687  df-suc 3688  df-om 3962  df-xp 4009  df-rel 4010  df-cnv 4011  df-co 4012  df-dm 4013  df-rn 4014  df-res 4015  df-ima 4016  df-fun 4017  df-fn 4018  df-f 4019  df-f1 4020  df-fo 4021  df-f1o 4022  df-fv 4023  df-ov 4924  df-oprab 4925  df-mpt 5059  df-mpt2 5060  df-1st 5158  df-2nd 5159  df-iota 5263  df-rdg 5349  df-er 5523  df-map 5611  df-pm 5612  df-en 5668  df-dom 5669  df-sdom 5670  df-riota 5811  df-sup 5985  df-pnf 7105  df-mnf 7106  df-xr 7107  df-ltxr 7108  df-le 7109  df-sub 7234  df-neg 7236  df-div 7460  df-n 7699  df-2 7745  df-3 7746  df-n0 7869  df-z 7913  df-uz 8033  df-q 8115  df-rp 8240  df-fl 8478  df-seq 8570  df-exp 8622  df-cj 8856  df-re 8857  df-im 8858  df-sqr 8950  df-abs 8951  df-clim 9119  df-rlim 9120
Copyright terms: Public domain