Theorem itg10a 22411
2 itg1val 22384 . . 3
4 i1ff 22377 . . . . . . . . . . . . . . . 16
5 1, 4 syl 17 . . . . . . . . . . . . . . 15
6 ffn 5716 . . . . . . . . . . . . . . 15
7 5, 6 syl 17 . . . . . . . . . . . . . 14
8 7 adantr 465 . . . . . . . . . . . . 13
9 fniniseg 5988 . . . . . . . . . . . . 13
10 8, 9 syl 17 . . . . . . . . . . . 12
11 eldifsni 4100 . . . . . . . . . . . . . . 15
12 11 ad2antlr 727 . . . . . . . . . . . . . 14
13 simprl 758 . . . . . . . . . . . . . . . 16
14 eldif 3426 . . . . . . . . . . . . . . . . 17
15 simplrr 765 . . . . . . . . . . . . . . . . . . 19
16 simpll 754 . . . . . . . . . . . . . . . . . . . 20
18 16, 17 sylan 471 . . . . . . . . . . . . . . . . . . 19
19 15, 18 eqtr3d 2447 . . . . . . . . . . . . . . . . . 18
20 19 ex 434 . . . . . . . . . . . . . . . . 17
21 14, 20 syl5bir 220 . . . . . . . . . . . . . . . 16
22 13, 21 mpand 675 . . . . . . . . . . . . . . 15
23 22 necon1ad 2621 . . . . . . . . . . . . . 14
25 24 ex 434 . . . . . . . . . . . 12
26 10, 25 sylbid 217 . . . . . . . . . . 11
27 26 ssrdv 3450 . . . . . . . . . 10
30 27, 29 sstrd 3454 . . . . . . . . 9
33 ovolssnul 22192 . . . . . . . . . 10
34 27, 29, 32, 33 syl3anc 1232 . . . . . . . . 9
35 nulmbl 22240 . . . . . . . . 9
36 30, 34, 35 syl2anc 661 . . . . . . . 8
37 mblvol 22235 . . . . . . . 8
38 36, 37 syl 17 . . . . . . 7
39 38, 34 eqtrd 2445 . . . . . 6
40 39 oveq2d 6296 . . . . 5
41 frn 5722 . . . . . . . . . 10
42 5, 41 syl 17 . . . . . . . . 9
43 42 ssdifssd 3583 . . . . . . . 8
44 43 sselda 3444 . . . . . . 7
45 44 recnd 9654 . . . . . 6
46 45 mul01d 9815 . . . . 5
47 40, 46 eqtrd 2445 . . . 4
48 47 sumeq2dv 13676 . . 3
49 i1frn 22378 . . . . . . 7
50 1, 49 syl 17 . . . . . 6
51 difss 3572 . . . . . 6
52 ssfi 7777 . . . . . 6
53 50, 51, 52 sylancl 662 . . . . 5
54 53 olcd 393 . . . 4
55 sumz 13695 . . . 4
56 54, 55 syl 17 . . 3
57 48, 56 eqtrd 2445 . 2
58 3, 57 eqtrd 2445 1
Syntax hints: wn 3 wi 4 wb 186 wo 368 wa 369 wceq 1407 wcel 1844 wne 2600 cdif 3413 wss 3416 csn 3974 ccnv 4824 cdm 4825 crn 4826 cima 4828 wfn 5566 wf 5567 cfv 5571 (class class class)co 6280 cfn 7556 cr 9523 cc0 9524 cmul 9529 cuz 11129 csu 13659 covol 22168 cvol 22169 citg1 22318
This theorem depends on definitions: df-bi 187 df-or 370 df-an 371 df-3or 977 df-3an 978 df-tru 1410 df-fal 1413 df-ex 1636 df-nf 1640 df-sb 1766 df-eu 2244 df-mo 2245 df-clab 2390 df-cleq 2396 df-clel 2399 df-nfc 2554 df-ne 2602 df-nel 2603 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3063 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-pss 3432 df-nul 3741 df-if 3888 df-pw 3959 df-sn 3975 df-pr 3977 df-tp 3979 df-op 3981 df-uni 4194 df-int 4230 df-iun 4275 df-br 4398 df-opab 4456 df-mpt 4457 df-tr 4492 df-eprel 4736 df-id 4740 df-po 4746 df-so 4747 df-fr 4784 df-se 4785 df-we 4786 df-xp 4831 df-rel 4832 df-cnv 4833 df-co 4834 df-dm 4835 df-rn 4836 df-res 4837 df-ima 4838 df-pred 5369 df-ord 5415 df-on 5416 df-lim 5417 df-suc 5418 df-iota 5535 df-fun 5573 df-fn 5574 df-f 5575 df-f1 5576 df-fo 5577 df-f1o 5578 df-fv 5579 df-isom 5580 df-riota 6242 df-ov 6283 df-oprab 6284 df-mpt2 6285 df-om 6686 df-1st 6786 df-2nd 6787 df-wrecs 7015 df-recs 7077 df-rdg 7115 df-1o 7169 df-oadd 7173 df-er 7350 df-map 7461 df-en 7557 df-dom 7558 df-sdom 7559 df-fin 7560 df-sup 7937 df-oi 7971 df-card 8354 df-pnf 9662 df-mnf 9663 df-xr 9664 df-ltxr 9665 df-le 9666 df-sub 9845 df-neg 9846 df-div 10250 df-nn 10579 df-2 10637 df-3 10638 df-n0 10839 df-z 10908 df-uz 11130 df-q 11230 df-rp 11268 df-ioo 11588 df-ico 11590 df-icc 11591 df-fz 11729 df-fzo 11857 df-fl 11968 df-seq 12154 df-exp 12213 df-hash 12455 df-cj 13083 df-re 13084 df-im 13085 df-sqrt 13219 df-abs 13220 df-clim 13462 df-sum 13660 df-ovol 22170 df-vol 22171 df-itg1 22323
This theorem is referenced by: itg2addnclem 31452