ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  lgsfcl2 GIF version

Theorem lgsfcl2 14377
Description: The function ๐น is closed in integers with absolute value less than 1 (namely {-1, 0, 1}, see zabsle1 14370). (Contributed by Mario Carneiro, 4-Feb-2015.)
Hypotheses
Ref Expression
lgsval.1 ๐น = (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โˆˆ โ„™, (if(๐‘› = 2, if(2 โˆฅ ๐ด, 0, if((๐ด mod 8) โˆˆ {1, 7}, 1, -1)), ((((๐ดโ†‘((๐‘› โˆ’ 1) / 2)) + 1) mod ๐‘›) โˆ’ 1))โ†‘(๐‘› pCnt ๐‘)), 1))
lgsfcl2.z ๐‘ = {๐‘ฅ โˆˆ โ„ค โˆฃ (absโ€˜๐‘ฅ) โ‰ค 1}
Assertion
Ref Expression
lgsfcl2 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ ๐น:โ„•โŸถ๐‘)
Distinct variable groups:   ๐ด,๐‘›,๐‘ฅ   ๐‘ฅ,๐น   ๐‘›,๐‘,๐‘ฅ   ๐‘›,๐‘
Allowed substitution hints:   ๐น(๐‘›)   ๐‘(๐‘ฅ)

Proof of Theorem lgsfcl2
Dummy variables ๐‘Ž ๐‘ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0z 9263 . . . . . . . . 9 0 โˆˆ โ„ค
2 0le1 8437 . . . . . . . . 9 0 โ‰ค 1
3 fveq2 5515 . . . . . . . . . . . 12 (๐‘ฅ = 0 โ†’ (absโ€˜๐‘ฅ) = (absโ€˜0))
4 abs0 11066 . . . . . . . . . . . 12 (absโ€˜0) = 0
53, 4eqtrdi 2226 . . . . . . . . . . 11 (๐‘ฅ = 0 โ†’ (absโ€˜๐‘ฅ) = 0)
65breq1d 4013 . . . . . . . . . 10 (๐‘ฅ = 0 โ†’ ((absโ€˜๐‘ฅ) โ‰ค 1 โ†” 0 โ‰ค 1))
7 lgsfcl2.z . . . . . . . . . 10 ๐‘ = {๐‘ฅ โˆˆ โ„ค โˆฃ (absโ€˜๐‘ฅ) โ‰ค 1}
86, 7elrab2 2896 . . . . . . . . 9 (0 โˆˆ ๐‘ โ†” (0 โˆˆ โ„ค โˆง 0 โ‰ค 1))
91, 2, 8mpbir2an 942 . . . . . . . 8 0 โˆˆ ๐‘
109a1i 9 . . . . . . 7 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ 0 โˆˆ ๐‘)
11 1z 9278 . . . . . . . . . 10 1 โˆˆ โ„ค
12 1le1 8528 . . . . . . . . . 10 1 โ‰ค 1
13 fveq2 5515 . . . . . . . . . . . . 13 (๐‘ฅ = 1 โ†’ (absโ€˜๐‘ฅ) = (absโ€˜1))
14 abs1 11080 . . . . . . . . . . . . 13 (absโ€˜1) = 1
1513, 14eqtrdi 2226 . . . . . . . . . . . 12 (๐‘ฅ = 1 โ†’ (absโ€˜๐‘ฅ) = 1)
1615breq1d 4013 . . . . . . . . . . 11 (๐‘ฅ = 1 โ†’ ((absโ€˜๐‘ฅ) โ‰ค 1 โ†” 1 โ‰ค 1))
1716, 7elrab2 2896 . . . . . . . . . 10 (1 โˆˆ ๐‘ โ†” (1 โˆˆ โ„ค โˆง 1 โ‰ค 1))
1811, 12, 17mpbir2an 942 . . . . . . . . 9 1 โˆˆ ๐‘
1918a1i 9 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ 1 โˆˆ ๐‘)
20 neg1z 9284 . . . . . . . . . 10 -1 โˆˆ โ„ค
21 fveq2 5515 . . . . . . . . . . . . 13 (๐‘ฅ = -1 โ†’ (absโ€˜๐‘ฅ) = (absโ€˜-1))
22 ax-1cn 7903 . . . . . . . . . . . . . . 15 1 โˆˆ โ„‚
2322absnegi 11155 . . . . . . . . . . . . . 14 (absโ€˜-1) = (absโ€˜1)
2423, 14eqtri 2198 . . . . . . . . . . . . 13 (absโ€˜-1) = 1
2521, 24eqtrdi 2226 . . . . . . . . . . . 12 (๐‘ฅ = -1 โ†’ (absโ€˜๐‘ฅ) = 1)
2625breq1d 4013 . . . . . . . . . . 11 (๐‘ฅ = -1 โ†’ ((absโ€˜๐‘ฅ) โ‰ค 1 โ†” 1 โ‰ค 1))
2726, 7elrab2 2896 . . . . . . . . . 10 (-1 โˆˆ ๐‘ โ†” (-1 โˆˆ โ„ค โˆง 1 โ‰ค 1))
2820, 12, 27mpbir2an 942 . . . . . . . . 9 -1 โˆˆ ๐‘
2928a1i 9 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ -1 โˆˆ ๐‘)
30 simp1 997 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ ๐ด โˆˆ โ„ค)
31 8nn 9085 . . . . . . . . . . . . . 14 8 โˆˆ โ„•
3231a1i 9 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ 8 โˆˆ โ„•)
3330, 32zmodcld 10344 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ (๐ด mod 8) โˆˆ โ„•0)
3433nn0zd 9372 . . . . . . . . . . 11 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ (๐ด mod 8) โˆˆ โ„ค)
35 zdceq 9327 . . . . . . . . . . 11 (((๐ด mod 8) โˆˆ โ„ค โˆง 1 โˆˆ โ„ค) โ†’ DECID (๐ด mod 8) = 1)
3634, 11, 35sylancl 413 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ DECID (๐ด mod 8) = 1)
37 7nn 9084 . . . . . . . . . . . 12 7 โˆˆ โ„•
3837nnzi 9273 . . . . . . . . . . 11 7 โˆˆ โ„ค
39 zdceq 9327 . . . . . . . . . . 11 (((๐ด mod 8) โˆˆ โ„ค โˆง 7 โˆˆ โ„ค) โ†’ DECID (๐ด mod 8) = 7)
4034, 38, 39sylancl 413 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ DECID (๐ด mod 8) = 7)
41 dcor 935 . . . . . . . . . 10 (DECID (๐ด mod 8) = 1 โ†’ (DECID (๐ด mod 8) = 7 โ†’ DECID ((๐ด mod 8) = 1 โˆจ (๐ด mod 8) = 7)))
4236, 40, 41sylc 62 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ DECID ((๐ด mod 8) = 1 โˆจ (๐ด mod 8) = 7))
43 elprg 3612 . . . . . . . . . . 11 ((๐ด mod 8) โˆˆ โ„•0 โ†’ ((๐ด mod 8) โˆˆ {1, 7} โ†” ((๐ด mod 8) = 1 โˆจ (๐ด mod 8) = 7)))
4433, 43syl 14 . . . . . . . . . 10 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ ((๐ด mod 8) โˆˆ {1, 7} โ†” ((๐ด mod 8) = 1 โˆจ (๐ด mod 8) = 7)))
4544dcbid 838 . . . . . . . . 9 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ (DECID (๐ด mod 8) โˆˆ {1, 7} โ†” DECID ((๐ด mod 8) = 1 โˆจ (๐ด mod 8) = 7)))
4642, 45mpbird 167 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ DECID (๐ด mod 8) โˆˆ {1, 7})
4719, 29, 46ifcldcd 3570 . . . . . . 7 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ if((๐ด mod 8) โˆˆ {1, 7}, 1, -1) โˆˆ ๐‘)
48 2nn 9079 . . . . . . . . 9 2 โˆˆ โ„•
4948a1i 9 . . . . . . . 8 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ 2 โˆˆ โ„•)
50 dvdsdc 11804 . . . . . . . 8 ((2 โˆˆ โ„• โˆง ๐ด โˆˆ โ„ค) โ†’ DECID 2 โˆฅ ๐ด)
5149, 30, 50syl2anc 411 . . . . . . 7 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ DECID 2 โˆฅ ๐ด)
5210, 47, 51ifcldcd 3570 . . . . . 6 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ if(2 โˆฅ ๐ด, 0, if((๐ด mod 8) โˆˆ {1, 7}, 1, -1)) โˆˆ ๐‘)
5352ad3antrrr 492 . . . . 5 (((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โˆง ๐‘› = 2) โ†’ if(2 โˆฅ ๐ด, 0, if((๐ด mod 8) โˆˆ {1, 7}, 1, -1)) โˆˆ ๐‘)
54 simpl1 1000 . . . . . . 7 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โ†’ ๐ด โˆˆ โ„ค)
5554ad2antrr 488 . . . . . 6 (((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โˆง ยฌ ๐‘› = 2) โ†’ ๐ด โˆˆ โ„ค)
56 simplr 528 . . . . . . 7 (((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โˆง ยฌ ๐‘› = 2) โ†’ ๐‘› โˆˆ โ„™)
57 simpr 110 . . . . . . . 8 (((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โˆง ยฌ ๐‘› = 2) โ†’ ยฌ ๐‘› = 2)
5857neqned 2354 . . . . . . 7 (((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โˆง ยฌ ๐‘› = 2) โ†’ ๐‘› โ‰  2)
59 eldifsn 3719 . . . . . . 7 (๐‘› โˆˆ (โ„™ โˆ– {2}) โ†” (๐‘› โˆˆ โ„™ โˆง ๐‘› โ‰  2))
6056, 58, 59sylanbrc 417 . . . . . 6 (((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โˆง ยฌ ๐‘› = 2) โ†’ ๐‘› โˆˆ (โ„™ โˆ– {2}))
617lgslem4 14374 . . . . . 6 ((๐ด โˆˆ โ„ค โˆง ๐‘› โˆˆ (โ„™ โˆ– {2})) โ†’ ((((๐ดโ†‘((๐‘› โˆ’ 1) / 2)) + 1) mod ๐‘›) โˆ’ 1) โˆˆ ๐‘)
6255, 60, 61syl2anc 411 . . . . 5 (((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โˆง ยฌ ๐‘› = 2) โ†’ ((((๐ดโ†‘((๐‘› โˆ’ 1) / 2)) + 1) mod ๐‘›) โˆ’ 1) โˆˆ ๐‘)
63 simplr 528 . . . . . . 7 ((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โ†’ ๐‘› โˆˆ โ„•)
6463nnzd 9373 . . . . . 6 ((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โ†’ ๐‘› โˆˆ โ„ค)
65 2z 9280 . . . . . 6 2 โˆˆ โ„ค
66 zdceq 9327 . . . . . 6 ((๐‘› โˆˆ โ„ค โˆง 2 โˆˆ โ„ค) โ†’ DECID ๐‘› = 2)
6764, 65, 66sylancl 413 . . . . 5 ((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โ†’ DECID ๐‘› = 2)
6853, 62, 67ifcldadc 3563 . . . 4 ((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โ†’ if(๐‘› = 2, if(2 โˆฅ ๐ด, 0, if((๐ด mod 8) โˆˆ {1, 7}, 1, -1)), ((((๐ดโ†‘((๐‘› โˆ’ 1) / 2)) + 1) mod ๐‘›) โˆ’ 1)) โˆˆ ๐‘)
69 simpr 110 . . . . 5 ((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โ†’ ๐‘› โˆˆ โ„™)
70 simpll2 1037 . . . . 5 ((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โ†’ ๐‘ โˆˆ โ„ค)
71 simpll3 1038 . . . . 5 ((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โ†’ ๐‘ โ‰  0)
72 pczcl 12297 . . . . 5 ((๐‘› โˆˆ โ„™ โˆง (๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0)) โ†’ (๐‘› pCnt ๐‘) โˆˆ โ„•0)
7369, 70, 71, 72syl12anc 1236 . . . 4 ((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โ†’ (๐‘› pCnt ๐‘) โˆˆ โ„•0)
747ssrab3 3241 . . . . . 6 ๐‘ โŠ† โ„ค
75 zsscn 9260 . . . . . 6 โ„ค โŠ† โ„‚
7674, 75sstri 3164 . . . . 5 ๐‘ โŠ† โ„‚
777lgslem3 14373 . . . . 5 ((๐‘Ž โˆˆ ๐‘ โˆง ๐‘ โˆˆ ๐‘) โ†’ (๐‘Ž ยท ๐‘) โˆˆ ๐‘)
7876, 77, 18expcllem 10530 . . . 4 ((if(๐‘› = 2, if(2 โˆฅ ๐ด, 0, if((๐ด mod 8) โˆˆ {1, 7}, 1, -1)), ((((๐ดโ†‘((๐‘› โˆ’ 1) / 2)) + 1) mod ๐‘›) โˆ’ 1)) โˆˆ ๐‘ โˆง (๐‘› pCnt ๐‘) โˆˆ โ„•0) โ†’ (if(๐‘› = 2, if(2 โˆฅ ๐ด, 0, if((๐ด mod 8) โˆˆ {1, 7}, 1, -1)), ((((๐ดโ†‘((๐‘› โˆ’ 1) / 2)) + 1) mod ๐‘›) โˆ’ 1))โ†‘(๐‘› pCnt ๐‘)) โˆˆ ๐‘)
7968, 73, 78syl2anc 411 . . 3 ((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ๐‘› โˆˆ โ„™) โ†’ (if(๐‘› = 2, if(2 โˆฅ ๐ด, 0, if((๐ด mod 8) โˆˆ {1, 7}, 1, -1)), ((((๐ดโ†‘((๐‘› โˆ’ 1) / 2)) + 1) mod ๐‘›) โˆ’ 1))โ†‘(๐‘› pCnt ๐‘)) โˆˆ ๐‘)
8018a1i 9 . . 3 ((((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘› โˆˆ โ„™) โ†’ 1 โˆˆ ๐‘)
81 simpr 110 . . . 4 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โ†’ ๐‘› โˆˆ โ„•)
82 prmdc 12129 . . . 4 (๐‘› โˆˆ โ„• โ†’ DECID ๐‘› โˆˆ โ„™)
8381, 82syl 14 . . 3 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โ†’ DECID ๐‘› โˆˆ โ„™)
8479, 80, 83ifcldadc 3563 . 2 (((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โˆง ๐‘› โˆˆ โ„•) โ†’ if(๐‘› โˆˆ โ„™, (if(๐‘› = 2, if(2 โˆฅ ๐ด, 0, if((๐ด mod 8) โˆˆ {1, 7}, 1, -1)), ((((๐ดโ†‘((๐‘› โˆ’ 1) / 2)) + 1) mod ๐‘›) โˆ’ 1))โ†‘(๐‘› pCnt ๐‘)), 1) โˆˆ ๐‘)
85 lgsval.1 . 2 ๐น = (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โˆˆ โ„™, (if(๐‘› = 2, if(2 โˆฅ ๐ด, 0, if((๐ด mod 8) โˆˆ {1, 7}, 1, -1)), ((((๐ดโ†‘((๐‘› โˆ’ 1) / 2)) + 1) mod ๐‘›) โˆ’ 1))โ†‘(๐‘› pCnt ๐‘)), 1))
8684, 85fmptd 5670 1 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โ‰  0) โ†’ ๐น:โ„•โŸถ๐‘)
Colors of variables: wff set class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โˆง wa 104   โ†” wb 105   โˆจ wo 708  DECID wdc 834   โˆง w3a 978   = wceq 1353   โˆˆ wcel 2148   โ‰  wne 2347  {crab 2459   โˆ– cdif 3126  ifcif 3534  {csn 3592  {cpr 3593   class class class wbr 4003   โ†ฆ cmpt 4064  โŸถwf 5212  โ€˜cfv 5216  (class class class)co 5874  โ„‚cc 7808  0cc0 7810  1c1 7811   + caddc 7813   โ‰ค cle 7992   โˆ’ cmin 8127  -cneg 8128   / cdiv 8628  โ„•cn 8918  2c2 8969  7c7 8974  8c8 8975  โ„•0cn0 9175  โ„คcz 9252   mod cmo 10321  โ†‘cexp 10518  abscabs 11005   โˆฅ cdvds 11793  โ„™cprime 12106   pCnt cpc 12283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4118  ax-sep 4121  ax-nul 4129  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536  ax-iinf 4587  ax-cnex 7901  ax-resscn 7902  ax-1cn 7903  ax-1re 7904  ax-icn 7905  ax-addcl 7906  ax-addrcl 7907  ax-mulcl 7908  ax-mulrcl 7909  ax-addcom 7910  ax-mulcom 7911  ax-addass 7912  ax-mulass 7913  ax-distr 7914  ax-i2m1 7915  ax-0lt1 7916  ax-1rid 7917  ax-0id 7918  ax-rnegex 7919  ax-precex 7920  ax-cnre 7921  ax-pre-ltirr 7922  ax-pre-ltwlin 7923  ax-pre-lttrn 7924  ax-pre-apti 7925  ax-pre-ltadd 7926  ax-pre-mulgt0 7927  ax-pre-mulext 7928  ax-arch 7929  ax-caucvg 7930
This theorem depends on definitions:  df-bi 117  df-stab 831  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-xor 1376  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-iun 3888  df-br 4004  df-opab 4065  df-mpt 4066  df-tr 4102  df-id 4293  df-po 4296  df-iso 4297  df-iord 4366  df-on 4368  df-ilim 4369  df-suc 4371  df-iom 4590  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-res 4638  df-ima 4639  df-iota 5178  df-fun 5218  df-fn 5219  df-f 5220  df-f1 5221  df-fo 5222  df-f1o 5223  df-fv 5224  df-isom 5225  df-riota 5830  df-ov 5877  df-oprab 5878  df-mpo 5879  df-1st 6140  df-2nd 6141  df-recs 6305  df-irdg 6370  df-frec 6391  df-1o 6416  df-2o 6417  df-oadd 6420  df-er 6534  df-en 6740  df-dom 6741  df-fin 6742  df-sup 6982  df-inf 6983  df-pnf 7993  df-mnf 7994  df-xr 7995  df-ltxr 7996  df-le 7997  df-sub 8129  df-neg 8130  df-reap 8531  df-ap 8538  df-div 8629  df-inn 8919  df-2 8977  df-3 8978  df-4 8979  df-5 8980  df-6 8981  df-7 8982  df-8 8983  df-n0 9176  df-z 9253  df-uz 9528  df-q 9619  df-rp 9653  df-fz 10008  df-fzo 10142  df-fl 10269  df-mod 10322  df-seqfrec 10445  df-exp 10519  df-ihash 10755  df-cj 10850  df-re 10851  df-im 10852  df-rsqrt 11006  df-abs 11007  df-clim 11286  df-proddc 11558  df-dvds 11794  df-gcd 11943  df-prm 12107  df-phi 12210  df-pc 12284
This theorem is referenced by:  lgscllem  14378  lgsfcl  14379  lgsfle1  14380
  Copyright terms: Public domain W3C validator