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

Theorem expcnv 9274
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 8030 . . 3 |- NN = (ZZ>=` 1)
2 1z 7906 . . . 4 |- 1 e. ZZ
32a1i 10 . . 3 |- ((ph /\ A = 0) -> 1 e. ZZ)
4 nn0ex 7840 . . . . 5 |- NN0 e. _V
54mptex 5093 . . . 4 |- (n e. NN0 |-> (A^n)) e. _V
65a1i 10 . . 3 |- ((ph /\ A = 0) -> (n e. NN0 |-> (A^n)) e. _V)
7 0cn 7062 . . . 4 |- 0 e. CC
87a1i 10 . . 3 |- ((ph /\ A = 0) -> 0 e. CC)
9 nnnn0 7841 . . . . . 6 |- (k e. NN -> k e. NN0)
10 oveq2 4934 . . . . . . 7 |- (n = k -> (A^n) = (A^k))
11 eqid 1960 . . . . . . 7 |- (n e. NN0 |-> (A^n)) = (n e. NN0 |-> (A^n))
12 ovex 4950 . . . . . . 7 |- (A^k) e. _V
1310, 11, 12fvmpt 5109 . . . . . 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 469 . . . . . 6 |- ((ph /\ A = 0) -> A = 0)
1615oveq1d 4940 . . . . 5 |- ((ph /\ A = 0) -> (A^k) = (0^k))
1714, 16sylan9eqr 2014 . . . 4 |- (((ph /\ A = 0) /\ k e. NN) -> ((n e. NN0 |-> (A^n))` k) = (0^k))
18 0exp 8608 . . . . 5 |- (k e. NN -> (0^k) = 0)
1918adantl 475 . . . 4 |- (((ph /\ A = 0) /\ k e. NN) -> (0^k) = 0)
2017, 19eqtrd 1992 . . 3 |- (((ph /\ A = 0) /\ k e. NN) -> ((n e. NN0 |-> (A^n))` k) = 0)
211, 3, 6, 8, 20climconst 9070 . 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 474 . . . . . . . . . 10 |- ((ph /\ A =/= 0) -> (abs` A) < 1)
26 expcnv.1 . . . . . . . . . . . 12 |- (ph -> A e. CC)
27 absrpcl 8984 . . . . . . . . . . . 12 |- ((A e. CC /\ A =/= 0) -> (abs`
A) e. RR+)
2826, 27sylan 480 . . . . . . . . . . 11 |- ((ph /\ A =/= 0) -> (abs` A) e. RR+)
29 elrp 8204 . . . . . . . . . . . 12 |- ((abs` A) e. RR+ <-> ((abs` A) e. RR /\ 0 < (abs` A)))
30 reclt1 7610 . . . . . . . . . . . 12 |- (((abs` A) e. RR /\ 0 < (abs` A)) -> ((abs` A) < 1 <-> 1 < (1 / (abs` A))))
3129, 30sylbi 200 . . . . . . . . . . 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 219 . . . . . . . . 9 |- ((ph /\ A =/= 0) -> 1 < (1 / (abs` A)))
34 1re 7070 . . . . . . . . . 10 |- 1 e. RR
35 rpreccl 8223 . . . . . . . . . . . 12 |- ((abs` A) e. RR+ -> (1 / (abs`
A)) e. RR+)
3628, 35syl 14 . . . . . . . . . . 11 |- ((ph /\ A =/= 0) -> (1 / (abs` A)) e. RR+)
37 rpre 8207 . . . . . . . . . . 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 8231 . . . . . . . . . 10 |- ((1 e. RR /\ (1 / (abs` A)) e. RR) -> (1 < (1 / (abs` A)) <-> ((1 / (abs`
A)) - 1) e. RR+))
4034, 38, 39sylancr 670 . . . . . . . . 9 |- ((ph /\ A =/= 0) -> (1 < (1 / (abs`
A)) <-> ((1 / (abs` A)) - 1) e. RR+))
4133, 40mpbid 219 . . . . . . . 8 |- ((ph /\ A =/= 0) -> ((1 / (abs` A)) - 1) e. RR+)
42 rpreccl 8223 . . . . . . . 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 8207 . . . . . . 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 7052 . . . . 5 |- ((ph /\ A =/= 0) -> (1 / ((1 / (abs` A)) - 1)) e. CC)
47 divcnv 9269 . . . . 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 7666 . . . . . 6 |- NN e. _V
5049mptex 5093 . . . . 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 4934 . . . . . . 7 |- (n = k -> ((1 / ((1 / (abs` A)) - 1)) / n) = ((1 / ((1 / (abs`
A)) - 1)) / k))
53 eqid 1960 . . . . . . 7 |- (n e. NN |-> ((1 / ((1 / (abs` A)) - 1)) / n)) = (n e. NN |-> ((1 / ((1 / (abs` A)) - 1)) / n))
54 ovex 4950 . . . . . . 7 |- ((1 / ((1 / (abs` A)) - 1)) / k) e. _V
5552, 53, 54fvmpt 5109 . . . . . 6 |- (k e. NN -> ((n e. NN |-> ((1 / ((1 / (abs`
A)) - 1)) / n))` k) = ((1 / ((1 / (abs` A)) - 1)) / k))
5655adantl 475 . . . . 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 7695 . . . . . 6 |- (((1 / ((1 / (abs` A)) - 1)) e. RR /\ k e. NN) -> ((1 / ((1 / (abs`
A)) - 1)) / k) e. RR)
5845, 57sylan 480 . . . . 5 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((1 / ((1 / (abs`
A)) - 1)) / k) e. RR)
5956, 58eqeltrd 2033 . . . 4 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((n e. NN |-> ((1 / ((1 / (abs` A)) - 1)) / n))` k) e. RR)
60 oveq2 4934 . . . . . . . 8 |- (n = k -> ((abs` A)^n) = ((abs` A)^k))
61 eqid 1960 . . . . . . . 8 |- (n e. NN |-> ((abs` A)^n)) = (n e. NN |-> ((abs` A)^n))
62 ovex 4950 . . . . . . . 8 |- ((abs` A)^k) e. _V
6360, 61, 62fvmpt 5109 . . . . . . 7 |- (k e. NN -> ((n e. NN |-> ((abs` A)^n))` k) = ((abs` A)^k))
6463adantl 475 . . . . . 6 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((n e. NN |-> ((abs` A)^n))` k) = ((abs` A)^k))
65 nnz 7898 . . . . . . 7 |- (k e. NN -> k e. ZZ)
66 rpexpcl 8597 . . . . . . 7 |- (((abs` A) e. RR+ /\ k e. ZZ) -> ((abs` A)^k) e. RR+)
6728, 65, 66syl2an 486 . . . . . 6 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((abs` A)^k) e. RR+)
6864, 67eqeltrd 2033 . . . . 5 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((n e. NN |-> ((abs` A)^n))` k) e. RR+)
69 rpre 8207 . . . . 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 8209 . . . . . . . . . . 11 |- (k e. NN -> k e. RR+)
72 rpmulcl 8221 . . . . . . . . . . 11 |- ((((1 / (abs` A)) - 1) e. RR+ /\ k e. RR+) -> (((1 / (abs` A)) - 1) x. k) e. RR+)
7341, 71, 72syl2an 486 . . . . . . . . . 10 |- (((ph /\ A =/= 0) /\ k e. NN) -> (((1 / (abs` A)) - 1) x. k) e. RR+)
74 rpre 8207 . . . . . . . . . 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 7164 . . . . . . . . . 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 8597 . . . . . . . . . . 11 |- (((1 / (abs` A)) e. RR+ /\ k e. ZZ) -> ((1 / (abs`
A))^k) e. RR+)
7936, 65, 78syl2an 486 . . . . . . . . . 10 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((1 / (abs`
A))^k) e. RR+)
80 rpre 8207 . . . . . . . . . 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 7532 . . . . . . . . . 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 474 . . . . . . . . . 10 |- (((ph /\ A =/= 0) /\ k e. NN) -> (1 / (abs` A)) e. RR)
859adantl 475 . . . . . . . . . 10 |- (((ph /\ A =/= 0) /\ k e. NN) -> k e. NN0)
86 rpge0 8212 . . . . . . . . . . . 12 |- ((1 / (abs` A)) e. RR+ -> 0 <_ (1 / (abs` A)))
8736, 86syl 14 . . . . . . . . . . 11 |- ((ph /\ A =/= 0) -> 0 <_ (1 / (abs` A)))
8887adantr 474 . . . . . . . . . 10 |- (((ph /\ A =/= 0) /\ k e. NN) -> 0 <_ (1 / (abs` A)))
89 bernneq2 8692 . . . . . . . . . 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 1187 . . . . . . . . 9 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((((1 / (abs` A)) - 1) x. k) + 1) <_ ((1 / (abs` A))^k))
9175, 77, 81, 83, 90letrd 7117 . . . . . . . 8 |- (((ph /\ A =/= 0) /\ k e. NN) -> (((1 / (abs` A)) - 1) x. k) <_ ((1 / (abs` A))^k))
92 rpcnne0 8217 . . . . . . . . . 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 8614 . . . . . . . . . 10 |- (((abs` A) e. CC /\ (abs` A) =/= 0 /\ k e. ZZ) -> ((1 / (abs`
A))^k) = (1 / ((abs` A)^k)))
95943expa 1157 . . . . . . . . 9 |- ((((abs`
A) e. CC /\ (abs`
A) =/= 0) /\ k e. ZZ) -> ((1 / (abs` A))^k) = (1 / ((abs` A)^k)))
9693, 65, 95syl2an 486 . . . . . . . 8 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((1 / (abs`
A))^k) = (1 / ((abs` A)^k)))
9791, 96breqtrd 3402 . . . . . . 7 |- (((ph /\ A =/= 0) /\ k e. NN) -> (((1 / (abs` A)) - 1) x. k) <_ (1 / ((abs` A)^k)))
98 elrp 8204 . . . . . . . . 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 8204 . . . . . . . . 9 |- (((abs` A)^k) e. RR+ <-> (((abs` A)^k) e. RR /\ 0 < ((abs` A)^k)))
100 lerec2 7601 . . . . . . . . 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 488 . . . . . . . 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 668 . . . . . . 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 219 . . . . . 6 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((abs` A)^k) <_ (1 / (((1 / (abs` A)) - 1) x. k)))
104 rpcnne0 8217 . . . . . . . 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 7671 . . . . . . . 8 |- (k e. NN -> k e. CC)
107 nnne0 7692 . . . . . . . 8 |- (k e. NN -> k =/= 0)
108106, 107jca 541 . . . . . . 7 |- (k e. NN -> (k e. CC /\ k =/= 0))
109 recdiv2 7515 . . . . . . 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 486 . . . . . 6 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((1 / ((1 / (abs`
A)) - 1)) / k) = (1 / (((1 / (abs` A)) - 1) x. k)))
111103, 110breqtrrd 3404 . . . . 5 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((abs` A)^k) <_ ((1 / ((1 / (abs` A)) - 1)) / k))
112111, 64, 563brtr4d 3408 . . . 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 8212 . . . . 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, 114climsqueeze2 9105 . . 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 475 . . . . . . 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 8596 . . . . . . 7 |- ((A e. CC /\ k e. NN0) -> (A^k) e. CC)
12226, 9, 121syl2an 486 . . . . . 6 |- ((ph /\ k e. NN) -> (A^k) e. CC)
123120, 122eqeltrd 2033 . . . . 5 |- ((ph /\ k e. NN) -> ((n e. NN0 |-> (A^n))` k) e. CC)
124 absexp 8998 . . . . . . 7 |- ((A e. CC /\ k e. NN0) -> (abs` (A^k)) = ((abs` A)^k))
12526, 9, 124syl2an 486 . . . . . 6 |- ((ph /\ k e. NN) -> (abs` (A^k)) = ((abs` A)^k))
126120fveq2d 4682 . . . . . 6 |- ((ph /\ k e. NN) -> (abs` ((n e. NN0 |-> (A^n))` k)) = (abs` (A^k)))
12763adantl 475 . . . . . 6 |- ((ph /\ k e. NN) -> ((n e. NN |-> ((abs` A)^n))` k) = ((abs` A)^k))
128125, 126, 1273eqtr4rd 2003 . . . . 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 9089 . . . 4 |- (ph -> ((n e. NN0 |-> (A^n)) ~~> 0 <-> (n e. NN |-> ((abs` A)^n)) ~~> 0))
130129biimpar 494 . . 3 |- ((ph /\ (n e. NN |-> ((abs` A)^n)) ~~> 0) -> (n e. NN0 |-> (A^n)) ~~> 0)
131115, 130syldan 479 . 2 |- ((ph /\ A =/= 0) -> (n e. NN0 |-> (A^n)) ~~> 0)
13221, 131pm2.61dane 2152 1 |- (ph -> (n e. NN0 |-> (A^n)) ~~> 0)
Colors of variables: wff set class
Syntax hints:   -> wi 4   <-> wb 189   /\ wa 382   = wceq 1457   e. wcel 1459   =/= wne 2078  _Vcvv 2365   class class class wbr 3378  ` cfv 4014  (class class class)co 4928   e. cmpt 5063  CCcc 6962  RRcr 6963  0cc0 6964  1c1 6965   + caddc 6967   x. cmul 6969   <_ cle 7072   < clt 7076   - cmin 7186   / cdiv 7188  NNcn 7189  NN0cn0 7190  ZZcz 7191  RR+crp 7193  ^cexp 8579  abscabs 8906   ~~> cli 9058
This theorem is referenced by:  explecnv 9275  geolim 9277  geo2lim 9281  geomcau 16682
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1376  ax-6 1377  ax-7 1378  ax-gen 1379  ax-8 1461  ax-10 1462  ax-11 1463  ax-12 1464  ax-13 1465  ax-14 1466  ax-17 1473  ax-9 1488  ax-4 1494  ax-16 1671  ax-ext 1942  ax-rep 3464  ax-sep 3474  ax-nul 3483  ax-pow 3519  ax-pr 3543  ax-un 3813  ax-inf2 6037  ax-resscn 7018  ax-1cn 7019  ax-icn 7020  ax-addcl 7021  ax-addrcl 7022  ax-mulcl 7023  ax-mulrcl 7024  ax-mulcom 7025  ax-addass 7026  ax-mulass 7027  ax-distr 7028  ax-i2m1 7029  ax-1ne0 7030  ax-1rid 7031  ax-rnegex 7032  ax-rrecex 7033  ax-cnre 7034  ax-pre-lttri 7035  ax-pre-lttrn 7036  ax-pre-ltadd 7037  ax-pre-mulgt0 7038  ax-pre-sup 7039
This theorem depends on definitions:  df-bi 190  df-or 383  df-an 384  df-3or 947  df-3an 948  df-tru 1354  df-ex 1381  df-sb 1633  df-eu 1860  df-mo 1861  df-clab 1948  df-cleq 1953  df-clel 1956  df-ne 2080  df-nel 2081  df-ral 2173  df-rex 2174  df-reu 2175  df-rab 2176  df-v 2367  df-sbc 2532  df-csb 2606  df-dif 2665  df-un 2667  df-in 2669  df-ss 2671  df-pss 2673  df-nul 2927  df-if 3028  df-pw 3086  df-sn 3101  df-pr 3102  df-tp 3104  df-op 3105  df-uni 3234  df-iun 3306  df-br 3379  df-opab 3433  df-tr 3448  df-eprel 3626  df-id 3629  df-po 3634  df-so 3648  df-fr 3667  df-we 3683  df-ord 3699  df-on 3700  df-lim 3701  df-suc 3702  df-om 3969  df-xp 4016  df-rel 4017  df-cnv 4018  df-co 4019  df-dm 4020  df-rn 4021  df-res 4022  df-ima 4023  df-fun 4024  df-fn 4025  df-f 4026  df-f1 4027  df-fo 4028  df-f1o 4029  df-fv 4030  df-ov 4930  df-oprab 4931  df-mpt 5065  df-mpt2 5066  df-1st 5134  df-2nd 5135  df-iota 5238  df-rdg 5324  df-er 5498  df-en 5643  df-dom 5644  df-sdom 5645  df-riota 5786  df-sup 5959  df-pnf 7077  df-mnf 7078  df-xr 7079  df-ltxr 7080  df-le 7081  df-sub 7205  df-neg 7207  df-div 7431  df-n 7665  df-2 7711  df-3 7712  df-n0 7835  df-z 7879  df-uz 7999  df-rp 8203  df-seq 8528  df-exp 8580  df-cj 8816  df-re 8817  df-im 8818  df-sqr 8907  df-abs 8908  df-clim 9059
Copyright terms: Public domain