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

Theorem expcnv 9338
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 8071 . . 3 |- NN = (ZZ>=` 1)
2 1z 7947 . . . 4 |- 1 e. ZZ
32a1i 10 . . 3 |- ((ph /\ A = 0) -> 1 e. ZZ)
4 nn0ex 7881 . . . . 5 |- NN0 e. _V
54mptex 5097 . . . 4 |- (n e. NN0 |-> (A^n)) e. _V
65a1i 10 . . 3 |- ((ph /\ A = 0) -> (n e. NN0 |-> (A^n)) e. _V)
7 0cn 7098 . . . 4 |- 0 e. CC
87a1i 10 . . 3 |- ((ph /\ A = 0) -> 0 e. CC)
9 nnnn0 7882 . . . . . 6 |- (k e. NN -> k e. NN0)
10 oveq2 4937 . . . . . . 7 |- (n = k -> (A^n) = (A^k))
11 eqid 1953 . . . . . . 7 |- (n e. NN0 |-> (A^n)) = (n e. NN0 |-> (A^n))
12 ovex 4953 . . . . . . 7 |- (A^k) e. _V
1310, 11, 12fvmpt 5113 . . . . . 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 463 . . . . . 6 |- ((ph /\ A = 0) -> A = 0)
1615oveq1d 4943 . . . . 5 |- ((ph /\ A = 0) -> (A^k) = (0^k))
1714, 16sylan9eqr 2007 . . . 4 |- (((ph /\ A = 0) /\ k e. NN) -> ((n e. NN0 |-> (A^n))` k) = (0^k))
18 0exp 8656 . . . . 5 |- (k e. NN -> (0^k) = 0)
1918adantl 469 . . . 4 |- (((ph /\ A = 0) /\ k e. NN) -> (0^k) = 0)
2017, 19eqtrd 1985 . . 3 |- (((ph /\ A = 0) /\ k e. NN) -> ((n e. NN0 |-> (A^n))` k) = 0)
211, 3, 6, 8, 20climconst 9133 . 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 468 . . . . . . . . . 10 |- ((ph /\ A =/= 0) -> (abs` A) < 1)
26 expcnv.1 . . . . . . . . . . . 12 |- (ph -> A e. CC)
27 absrpcl 9031 . . . . . . . . . . . 12 |- ((A e. CC /\ A =/= 0) -> (abs`
A) e. RR+)
2826, 27sylan 474 . . . . . . . . . . 11 |- ((ph /\ A =/= 0) -> (abs` A) e. RR+)
29 elrp 8248 . . . . . . . . . . . 12 |- ((abs` A) e. RR+ <-> ((abs` A) e. RR /\ 0 < (abs` A)))
30 reclt1 7648 . . . . . . . . . . . 12 |- (((abs` A) e. RR /\ 0 < (abs` A)) -> ((abs` A) < 1 <-> 1 < (1 / (abs` A))))
3129, 30sylbi 195 . . . . . . . . . . 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 214 . . . . . . . . 9 |- ((ph /\ A =/= 0) -> 1 < (1 / (abs` A)))
34 1re 7106 . . . . . . . . . 10 |- 1 e. RR
35 rpreccl 8267 . . . . . . . . . . . 12 |- ((abs` A) e. RR+ -> (1 / (abs`
A)) e. RR+)
3628, 35syl 14 . . . . . . . . . . 11 |- ((ph /\ A =/= 0) -> (1 / (abs` A)) e. RR+)
37 rpre 8251 . . . . . . . . . . 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 8275 . . . . . . . . . 10 |- ((1 e. RR /\ (1 / (abs` A)) e. RR) -> (1 < (1 / (abs` A)) <-> ((1 / (abs`
A)) - 1) e. RR+))
4034, 38, 39sylancr 661 . . . . . . . . 9 |- ((ph /\ A =/= 0) -> (1 < (1 / (abs`
A)) <-> ((1 / (abs` A)) - 1) e. RR+))
4133, 40mpbid 214 . . . . . . . 8 |- ((ph /\ A =/= 0) -> ((1 / (abs` A)) - 1) e. RR+)
42 rpreccl 8267 . . . . . . . 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 8251 . . . . . . 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 7088 . . . . 5 |- ((ph /\ A =/= 0) -> (1 / ((1 / (abs` A)) - 1)) e. CC)
47 divcnv 9332 . . . . 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 7707 . . . . . 6 |- NN e. _V
5049mptex 5097 . . . . 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 4937 . . . . . . 7 |- (n = k -> ((1 / ((1 / (abs` A)) - 1)) / n) = ((1 / ((1 / (abs`
A)) - 1)) / k))
53 eqid 1953 . . . . . . 7 |- (n e. NN |-> ((1 / ((1 / (abs` A)) - 1)) / n)) = (n e. NN |-> ((1 / ((1 / (abs` A)) - 1)) / n))
54 ovex 4953 . . . . . . 7 |- ((1 / ((1 / (abs` A)) - 1)) / k) e. _V
5552, 53, 54fvmpt 5113 . . . . . 6 |- (k e. NN -> ((n e. NN |-> ((1 / ((1 / (abs`
A)) - 1)) / n))` k) = ((1 / ((1 / (abs` A)) - 1)) / k))
5655adantl 469 . . . . 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 7736 . . . . . 6 |- (((1 / ((1 / (abs` A)) - 1)) e. RR /\ k e. NN) -> ((1 / ((1 / (abs`
A)) - 1)) / k) e. RR)
5845, 57sylan 474 . . . . 5 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((1 / ((1 / (abs`
A)) - 1)) / k) e. RR)
5956, 58eqeltrd 2026 . . . 4 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((n e. NN |-> ((1 / ((1 / (abs` A)) - 1)) / n))` k) e. RR)
60 oveq2 4937 . . . . . . . 8 |- (n = k -> ((abs` A)^n) = ((abs` A)^k))
61 eqid 1953 . . . . . . . 8 |- (n e. NN |-> ((abs` A)^n)) = (n e. NN |-> ((abs` A)^n))
62 ovex 4953 . . . . . . . 8 |- ((abs` A)^k) e. _V
6360, 61, 62fvmpt 5113 . . . . . . 7 |- (k e. NN -> ((n e. NN |-> ((abs` A)^n))` k) = ((abs` A)^k))
6463adantl 469 . . . . . 6 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((n e. NN |-> ((abs` A)^n))` k) = ((abs` A)^k))
65 nnz 7939 . . . . . . 7 |- (k e. NN -> k e. ZZ)
66 rpexpcl 8644 . . . . . . 7 |- (((abs` A) e. RR+ /\ k e. ZZ) -> ((abs` A)^k) e. RR+)
6728, 65, 66syl2an 480 . . . . . 6 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((abs` A)^k) e. RR+)
6864, 67eqeltrd 2026 . . . . 5 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((n e. NN |-> ((abs` A)^n))` k) e. RR+)
69 rpre 8251 . . . . 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 8253 . . . . . . . . . . 11 |- (k e. NN -> k e. RR+)
72 rpmulcl 8265 . . . . . . . . . . 11 |- ((((1 / (abs` A)) - 1) e. RR+ /\ k e. RR+) -> (((1 / (abs` A)) - 1) x. k) e. RR+)
7341, 71, 72syl2an 480 . . . . . . . . . 10 |- (((ph /\ A =/= 0) /\ k e. NN) -> (((1 / (abs` A)) - 1) x. k) e. RR+)
74 rpre 8251 . . . . . . . . . 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 7201 . . . . . . . . . 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 8644 . . . . . . . . . . 11 |- (((1 / (abs` A)) e. RR+ /\ k e. ZZ) -> ((1 / (abs`
A))^k) e. RR+)
7936, 65, 78syl2an 480 . . . . . . . . . 10 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((1 / (abs`
A))^k) e. RR+)
80 rpre 8251 . . . . . . . . . 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 7570 . . . . . . . . . 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 468 . . . . . . . . . 10 |- (((ph /\ A =/= 0) /\ k e. NN) -> (1 / (abs` A)) e. RR)
859adantl 469 . . . . . . . . . 10 |- (((ph /\ A =/= 0) /\ k e. NN) -> k e. NN0)
86 rpge0 8256 . . . . . . . . . . . 12 |- ((1 / (abs` A)) e. RR+ -> 0 <_ (1 / (abs` A)))
8736, 86syl 14 . . . . . . . . . . 11 |- ((ph /\ A =/= 0) -> 0 <_ (1 / (abs` A)))
8887adantr 468 . . . . . . . . . 10 |- (((ph /\ A =/= 0) /\ k e. NN) -> 0 <_ (1 / (abs` A)))
89 bernneq2 8740 . . . . . . . . . 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 1178 . . . . . . . . 9 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((((1 / (abs` A)) - 1) x. k) + 1) <_ ((1 / (abs` A))^k))
9175, 77, 81, 83, 90letrd 7153 . . . . . . . 8 |- (((ph /\ A =/= 0) /\ k e. NN) -> (((1 / (abs` A)) - 1) x. k) <_ ((1 / (abs` A))^k))
92 rpcnne0 8261 . . . . . . . . . 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 8662 . . . . . . . . . 10 |- (((abs` A) e. CC /\ (abs` A) =/= 0 /\ k e. ZZ) -> ((1 / (abs`
A))^k) = (1 / ((abs` A)^k)))
95943expa 1148 . . . . . . . . 9 |- ((((abs`
A) e. CC /\ (abs`
A) =/= 0) /\ k e. ZZ) -> ((1 / (abs` A))^k) = (1 / ((abs` A)^k)))
9693, 65, 95syl2an 480 . . . . . . . 8 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((1 / (abs`
A))^k) = (1 / ((abs` A)^k)))
9791, 96breqtrd 3397 . . . . . . 7 |- (((ph /\ A =/= 0) /\ k e. NN) -> (((1 / (abs` A)) - 1) x. k) <_ (1 / ((abs` A)^k)))
98 elrp 8248 . . . . . . . . 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 8248 . . . . . . . . 9 |- (((abs` A)^k) e. RR+ <-> (((abs` A)^k) e. RR /\ 0 < ((abs` A)^k)))
100 lerec2 7639 . . . . . . . . 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 482 . . . . . . . 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 659 . . . . . . 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 214 . . . . . 6 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((abs` A)^k) <_ (1 / (((1 / (abs` A)) - 1) x. k)))
104 rpcnne0 8261 . . . . . . . 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 7712 . . . . . . . 8 |- (k e. NN -> k e. CC)
107 nnne0 7733 . . . . . . . 8 |- (k e. NN -> k =/= 0)
108106, 107jca 535 . . . . . . 7 |- (k e. NN -> (k e. CC /\ k =/= 0))
109 recdiv2 7553 . . . . . . 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 480 . . . . . 6 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((1 / ((1 / (abs`
A)) - 1)) / k) = (1 / (((1 / (abs` A)) - 1) x. k)))
111103, 110breqtrrd 3399 . . . . 5 |- (((ph /\ A =/= 0) /\ k e. NN) -> ((abs` A)^k) <_ ((1 / ((1 / (abs` A)) - 1)) / k))
112111, 64, 563brtr4d 3403 . . . 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 8256 . . . . 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 9168 . . 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 469 . . . . . . 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 8643 . . . . . . 7 |- ((A e. CC /\ k e. NN0) -> (A^k) e. CC)
12226, 9, 121syl2an 480 . . . . . 6 |- ((ph /\ k e. NN) -> (A^k) e. CC)
123120, 122eqeltrd 2026 . . . . 5 |- ((ph /\ k e. NN) -> ((n e. NN0 |-> (A^n))` k) e. CC)
124 absexp 9045 . . . . . . 7 |- ((A e. CC /\ k e. NN0) -> (abs` (A^k)) = ((abs` A)^k))
12526, 9, 124syl2an 480 . . . . . 6 |- ((ph /\ k e. NN) -> (abs` (A^k)) = ((abs` A)^k))
126120fveq2d 4685 . . . . . 6 |- ((ph /\ k e. NN) -> (abs` ((n e. NN0 |-> (A^n))` k)) = (abs` (A^k)))
12763adantl 469 . . . . . 6 |- ((ph /\ k e. NN) -> ((n e. NN |-> ((abs` A)^n))` k) = ((abs` A)^k))
128125, 126, 1273eqtr4rd 1996 . . . . 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 9152 . . . 4 |- (ph -> ((n e. NN0 |-> (A^n)) ~~> 0 <-> (n e. NN |-> ((abs` A)^n)) ~~> 0))
130129biimpar 488 . . 3 |- ((ph /\ (n e. NN |-> ((abs` A)^n)) ~~> 0) -> (n e. NN0 |-> (A^n)) ~~> 0)
131115, 130syldan 473 . 2 |- ((ph /\ A =/= 0) -> (n e. NN0 |-> (A^n)) ~~> 0)
13221, 131pm2.61dane 2145 1 |- (ph -> (n e. NN0 |-> (A^n)) ~~> 0)
Colors of variables: wff set class
Syntax hints:   -> wi 4   <-> wb 184   /\ wa 377   = wceq 1449   e. wcel 1451   =/= wne 2071  _Vcvv 2358   class class class wbr 3373  ` cfv 4016  (class class class)co 4931   e. cmpt 5066  CCcc 6998  RRcr 6999  0cc0 7000  1c1 7001   + caddc 7003   x. cmul 7005   <_ cle 7108   < clt 7112   - cmin 7223   / cdiv 7225  NNcn 7226  NN0cn0 7227  ZZcz 7228  RR+crp 7230  ^cexp 8626  abscabs 8954   ~~> cli 9121
This theorem is referenced by:  explecnv 9339  geolim 9341  geo2lim 9345  mbfi1fseqlem6 12239  geomcau 17095
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1367  ax-6 1368  ax-7 1369  ax-gen 1370  ax-8 1453  ax-10 1454  ax-11 1455  ax-12 1456  ax-13 1457  ax-14 1458  ax-17 1465  ax-9 1480  ax-4 1486  ax-16 1664  ax-ext 1935  ax-rep 3459  ax-sep 3469  ax-nul 3478  ax-pow 3514  ax-pr 3538  ax-un 3808  ax-inf2 6071  ax-resscn 7054  ax-1cn 7055  ax-icn 7056  ax-addcl 7057  ax-addrcl 7058  ax-mulcl 7059  ax-mulrcl 7060  ax-mulcom 7061  ax-addass 7062  ax-mulass 7063  ax-distr 7064  ax-i2m1 7065  ax-1ne0 7066  ax-1rid 7067  ax-rnegex 7068  ax-rrecex 7069  ax-cnre 7070  ax-pre-lttri 7071  ax-pre-lttrn 7072  ax-pre-ltadd 7073  ax-pre-mulgt0 7074  ax-pre-sup 7075
This theorem depends on definitions:  df-bi 185  df-or 378  df-an 379  df-3or 938  df-3an 939  df-tru 1345  df-ex 1372  df-sb 1626  df-eu 1853  df-mo 1854  df-clab 1941  df-cleq 1946  df-clel 1949  df-ne 2073  df-nel 2074  df-ral 2166  df-rex 2167  df-reu 2168  df-rab 2169  df-v 2360  df-sbc 2525  df-csb 2600  df-dif 2660  df-un 2662  df-in 2664  df-ss 2666  df-pss 2668  df-nul 2922  df-if 3023  df-pw 3081  df-sn 3096  df-pr 3097  df-tp 3099  df-op 3100  df-uni 3229  df-iun 3301  df-br 3374  df-opab 3428  df-tr 3443  df-eprel 3621  df-id 3624  df-po 3629  df-so 3643  df-fr 3662  df-we 3678  df-ord 3694  df-on 3695  df-lim 3696  df-suc 3697  df-om 3971  df-xp 4018  df-rel 4019  df-cnv 4020  df-co 4021  df-dm 4022  df-rn 4023  df-res 4024  df-ima 4025  df-fun 4026  df-fn 4027  df-f 4028  df-f1 4029  df-fo 4030  df-f1o 4031  df-fv 4032  df-ov 4933  df-oprab 4934  df-mpt 5068  df-mpt2 5069  df-1st 5166  df-2nd 5167  df-iota 5270  df-rdg 5356  df-er 5530  df-en 5675  df-dom 5676  df-sdom 5677  df-riota 5818  df-sup 5992  df-pnf 7113  df-mnf 7114  df-xr 7115  df-ltxr 7116  df-le 7117  df-sub 7242  df-neg 7244  df-div 7468  df-n 7706  df-2 7752  df-3 7753  df-n0 7876  df-z 7920  df-uz 8040  df-rp 8247  df-seq 8575  df-exp 8627  df-cj 8861  df-re 8862  df-im 8863  df-sqr 8955  df-abs 8956  df-clim 9122
Copyright terms: Public domain