MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dchrisum0flblem2 Structured version   Visualization version   GIF version

Theorem dchrisum0flblem2 27246
Description: Lemma for dchrisum0flb 27247. Induction over relatively prime factors, with the prime power case handled in dchrisum0flblem1 . (Contributed by Mario Carneiro, 5-May-2016.) Replace reference to OLD theorem. (Revised by Wolf Lammen, 8-Sep-2020.)
Hypotheses
Ref Expression
rpvmasum.z 𝑍 = (β„€/nβ„€β€˜π‘)
rpvmasum.l 𝐿 = (β„€RHomβ€˜π‘)
rpvmasum.a (πœ‘ β†’ 𝑁 ∈ β„•)
rpvmasum2.g 𝐺 = (DChrβ€˜π‘)
rpvmasum2.d 𝐷 = (Baseβ€˜πΊ)
rpvmasum2.1 1 = (0gβ€˜πΊ)
dchrisum0f.f 𝐹 = (𝑏 ∈ β„• ↦ Σ𝑣 ∈ {π‘ž ∈ β„• ∣ π‘ž βˆ₯ 𝑏} (π‘‹β€˜(πΏβ€˜π‘£)))
dchrisum0f.x (πœ‘ β†’ 𝑋 ∈ 𝐷)
dchrisum0flb.r (πœ‘ β†’ 𝑋:(Baseβ€˜π‘)βŸΆβ„)
dchrisum0flb.1 (πœ‘ β†’ 𝐴 ∈ (β„€β‰₯β€˜2))
dchrisum0flb.2 (πœ‘ β†’ 𝑃 ∈ β„™)
dchrisum0flb.3 (πœ‘ β†’ 𝑃 βˆ₯ 𝐴)
dchrisum0flb.4 (πœ‘ β†’ βˆ€π‘¦ ∈ (1..^𝐴)if((βˆšβ€˜π‘¦) ∈ β„•, 1, 0) ≀ (πΉβ€˜π‘¦))
Assertion
Ref Expression
dchrisum0flblem2 (πœ‘ β†’ if((βˆšβ€˜π΄) ∈ β„•, 1, 0) ≀ (πΉβ€˜π΄))
Distinct variable groups:   𝑦, 1   𝑦,𝐹   π‘ž,𝑏,𝑣,𝑦,𝐴   𝑁,π‘ž,𝑦   𝑃,𝑏,π‘ž,𝑣,𝑦   𝑦,𝑍   𝑦,𝐷   𝐿,𝑏,𝑣,𝑦   𝑋,𝑏,𝑣,𝑦
Allowed substitution hints:   πœ‘(𝑦,𝑣,π‘ž,𝑏)   𝐷(𝑣,π‘ž,𝑏)   1 (𝑣,π‘ž,𝑏)   𝐹(𝑣,π‘ž,𝑏)   𝐺(𝑦,𝑣,π‘ž,𝑏)   𝐿(π‘ž)   𝑁(𝑣,𝑏)   𝑋(π‘ž)   𝑍(𝑣,π‘ž,𝑏)

Proof of Theorem dchrisum0flblem2
StepHypRef Expression
1 breq1 5152 . . 3 (1 = if((βˆšβ€˜π΄) ∈ β„•, 1, 0) β†’ (1 ≀ ((πΉβ€˜(𝑃↑(𝑃 pCnt 𝐴))) Β· (πΉβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) ↔ if((βˆšβ€˜π΄) ∈ β„•, 1, 0) ≀ ((πΉβ€˜(𝑃↑(𝑃 pCnt 𝐴))) Β· (πΉβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))))
2 breq1 5152 . . 3 (0 = if((βˆšβ€˜π΄) ∈ β„•, 1, 0) β†’ (0 ≀ ((πΉβ€˜(𝑃↑(𝑃 pCnt 𝐴))) Β· (πΉβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) ↔ if((βˆšβ€˜π΄) ∈ β„•, 1, 0) ≀ ((πΉβ€˜(𝑃↑(𝑃 pCnt 𝐴))) Β· (πΉβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))))
3 1t1e1 12380 . . . 4 (1 Β· 1) = 1
4 dchrisum0flb.2 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑃 ∈ β„™)
54adantr 479 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ 𝑃 ∈ β„™)
6 nnq 12952 . . . . . . . . . . . . . . 15 ((βˆšβ€˜π΄) ∈ β„• β†’ (βˆšβ€˜π΄) ∈ β„š)
76adantl 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (βˆšβ€˜π΄) ∈ β„š)
8 nnne0 12252 . . . . . . . . . . . . . . 15 ((βˆšβ€˜π΄) ∈ β„• β†’ (βˆšβ€˜π΄) β‰  0)
98adantl 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (βˆšβ€˜π΄) β‰  0)
10 2z 12600 . . . . . . . . . . . . . . 15 2 ∈ β„€
1110a1i 11 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ 2 ∈ β„€)
12 pcexp 16798 . . . . . . . . . . . . . 14 ((𝑃 ∈ β„™ ∧ ((βˆšβ€˜π΄) ∈ β„š ∧ (βˆšβ€˜π΄) β‰  0) ∧ 2 ∈ β„€) β†’ (𝑃 pCnt ((βˆšβ€˜π΄)↑2)) = (2 Β· (𝑃 pCnt (βˆšβ€˜π΄))))
135, 7, 9, 11, 12syl121anc 1373 . . . . . . . . . . . . 13 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (𝑃 pCnt ((βˆšβ€˜π΄)↑2)) = (2 Β· (𝑃 pCnt (βˆšβ€˜π΄))))
14 dchrisum0flb.1 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐴 ∈ (β„€β‰₯β€˜2))
15 eluz2nn 12874 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ (β„€β‰₯β€˜2) β†’ 𝐴 ∈ β„•)
1614, 15syl 17 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐴 ∈ β„•)
1716nncnd 12234 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐴 ∈ β„‚)
1817adantr 479 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ 𝐴 ∈ β„‚)
1918sqsqrtd 15392 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ ((βˆšβ€˜π΄)↑2) = 𝐴)
2019oveq2d 7429 . . . . . . . . . . . . 13 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (𝑃 pCnt ((βˆšβ€˜π΄)↑2)) = (𝑃 pCnt 𝐴))
21 2cnd 12296 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ 2 ∈ β„‚)
22 simpr 483 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (βˆšβ€˜π΄) ∈ β„•)
235, 22pccld 16789 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (𝑃 pCnt (βˆšβ€˜π΄)) ∈ β„•0)
2423nn0cnd 12540 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (𝑃 pCnt (βˆšβ€˜π΄)) ∈ β„‚)
2521, 24mulcomd 11241 . . . . . . . . . . . . 13 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (2 Β· (𝑃 pCnt (βˆšβ€˜π΄))) = ((𝑃 pCnt (βˆšβ€˜π΄)) Β· 2))
2613, 20, 253eqtr3rd 2779 . . . . . . . . . . . 12 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ ((𝑃 pCnt (βˆšβ€˜π΄)) Β· 2) = (𝑃 pCnt 𝐴))
2726oveq2d 7429 . . . . . . . . . . 11 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (𝑃↑((𝑃 pCnt (βˆšβ€˜π΄)) Β· 2)) = (𝑃↑(𝑃 pCnt 𝐴)))
28 prmnn 16617 . . . . . . . . . . . . . 14 (𝑃 ∈ β„™ β†’ 𝑃 ∈ β„•)
295, 28syl 17 . . . . . . . . . . . . 13 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ 𝑃 ∈ β„•)
3029nncnd 12234 . . . . . . . . . . . 12 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ 𝑃 ∈ β„‚)
31 2nn0 12495 . . . . . . . . . . . . 13 2 ∈ β„•0
3231a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ 2 ∈ β„•0)
3330, 32, 23expmuld 14120 . . . . . . . . . . 11 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (𝑃↑((𝑃 pCnt (βˆšβ€˜π΄)) Β· 2)) = ((𝑃↑(𝑃 pCnt (βˆšβ€˜π΄)))↑2))
3427, 33eqtr3d 2772 . . . . . . . . . 10 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (𝑃↑(𝑃 pCnt 𝐴)) = ((𝑃↑(𝑃 pCnt (βˆšβ€˜π΄)))↑2))
3534fveq2d 6896 . . . . . . . . 9 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (βˆšβ€˜(𝑃↑(𝑃 pCnt 𝐴))) = (βˆšβ€˜((𝑃↑(𝑃 pCnt (βˆšβ€˜π΄)))↑2)))
3629, 23nnexpcld 14214 . . . . . . . . . . . 12 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (𝑃↑(𝑃 pCnt (βˆšβ€˜π΄))) ∈ β„•)
3736nnrpd 13020 . . . . . . . . . . 11 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (𝑃↑(𝑃 pCnt (βˆšβ€˜π΄))) ∈ ℝ+)
3837rprege0d 13029 . . . . . . . . . 10 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ ((𝑃↑(𝑃 pCnt (βˆšβ€˜π΄))) ∈ ℝ ∧ 0 ≀ (𝑃↑(𝑃 pCnt (βˆšβ€˜π΄)))))
39 sqrtsq 15222 . . . . . . . . . 10 (((𝑃↑(𝑃 pCnt (βˆšβ€˜π΄))) ∈ ℝ ∧ 0 ≀ (𝑃↑(𝑃 pCnt (βˆšβ€˜π΄)))) β†’ (βˆšβ€˜((𝑃↑(𝑃 pCnt (βˆšβ€˜π΄)))↑2)) = (𝑃↑(𝑃 pCnt (βˆšβ€˜π΄))))
4038, 39syl 17 . . . . . . . . 9 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (βˆšβ€˜((𝑃↑(𝑃 pCnt (βˆšβ€˜π΄)))↑2)) = (𝑃↑(𝑃 pCnt (βˆšβ€˜π΄))))
4135, 40eqtrd 2770 . . . . . . . 8 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (βˆšβ€˜(𝑃↑(𝑃 pCnt 𝐴))) = (𝑃↑(𝑃 pCnt (βˆšβ€˜π΄))))
4241, 36eqeltrd 2831 . . . . . . 7 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (βˆšβ€˜(𝑃↑(𝑃 pCnt 𝐴))) ∈ β„•)
4342iftrued 4537 . . . . . 6 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ if((βˆšβ€˜(𝑃↑(𝑃 pCnt 𝐴))) ∈ β„•, 1, 0) = 1)
44 rpvmasum.z . . . . . . . 8 𝑍 = (β„€/nβ„€β€˜π‘)
45 rpvmasum.l . . . . . . . 8 𝐿 = (β„€RHomβ€˜π‘)
46 rpvmasum.a . . . . . . . 8 (πœ‘ β†’ 𝑁 ∈ β„•)
47 rpvmasum2.g . . . . . . . 8 𝐺 = (DChrβ€˜π‘)
48 rpvmasum2.d . . . . . . . 8 𝐷 = (Baseβ€˜πΊ)
49 rpvmasum2.1 . . . . . . . 8 1 = (0gβ€˜πΊ)
50 dchrisum0f.f . . . . . . . 8 𝐹 = (𝑏 ∈ β„• ↦ Σ𝑣 ∈ {π‘ž ∈ β„• ∣ π‘ž βˆ₯ 𝑏} (π‘‹β€˜(πΏβ€˜π‘£)))
51 dchrisum0f.x . . . . . . . 8 (πœ‘ β†’ 𝑋 ∈ 𝐷)
52 dchrisum0flb.r . . . . . . . 8 (πœ‘ β†’ 𝑋:(Baseβ€˜π‘)βŸΆβ„)
534, 16pccld 16789 . . . . . . . 8 (πœ‘ β†’ (𝑃 pCnt 𝐴) ∈ β„•0)
5444, 45, 46, 47, 48, 49, 50, 51, 52, 4, 53dchrisum0flblem1 27245 . . . . . . 7 (πœ‘ β†’ if((βˆšβ€˜(𝑃↑(𝑃 pCnt 𝐴))) ∈ β„•, 1, 0) ≀ (πΉβ€˜(𝑃↑(𝑃 pCnt 𝐴))))
5554adantr 479 . . . . . 6 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ if((βˆšβ€˜(𝑃↑(𝑃 pCnt 𝐴))) ∈ β„•, 1, 0) ≀ (πΉβ€˜(𝑃↑(𝑃 pCnt 𝐴))))
5643, 55eqbrtrrd 5173 . . . . 5 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ 1 ≀ (πΉβ€˜(𝑃↑(𝑃 pCnt 𝐴))))
57 pcdvds 16803 . . . . . . . . . . . . 13 ((𝑃 ∈ β„™ ∧ 𝐴 ∈ β„•) β†’ (𝑃↑(𝑃 pCnt 𝐴)) βˆ₯ 𝐴)
584, 16, 57syl2anc 582 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑃↑(𝑃 pCnt 𝐴)) βˆ₯ 𝐴)
594, 28syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑃 ∈ β„•)
6059, 53nnexpcld 14214 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑃↑(𝑃 pCnt 𝐴)) ∈ β„•)
61 nndivdvds 16212 . . . . . . . . . . . . 13 ((𝐴 ∈ β„• ∧ (𝑃↑(𝑃 pCnt 𝐴)) ∈ β„•) β†’ ((𝑃↑(𝑃 pCnt 𝐴)) βˆ₯ 𝐴 ↔ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ β„•))
6216, 60, 61syl2anc 582 . . . . . . . . . . . 12 (πœ‘ β†’ ((𝑃↑(𝑃 pCnt 𝐴)) βˆ₯ 𝐴 ↔ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ β„•))
6358, 62mpbid 231 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ β„•)
6463nnzd 12591 . . . . . . . . . 10 (πœ‘ β†’ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ β„€)
6564adantr 479 . . . . . . . . 9 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ β„€)
6616adantr 479 . . . . . . . . . . . . 13 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ 𝐴 ∈ β„•)
6766nnrpd 13020 . . . . . . . . . . . 12 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ 𝐴 ∈ ℝ+)
6867rprege0d 13029 . . . . . . . . . . 11 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (𝐴 ∈ ℝ ∧ 0 ≀ 𝐴))
6960adantr 479 . . . . . . . . . . . 12 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (𝑃↑(𝑃 pCnt 𝐴)) ∈ β„•)
7069nnrpd 13020 . . . . . . . . . . 11 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℝ+)
71 sqrtdiv 15218 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 0 ≀ 𝐴) ∧ (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℝ+) β†’ (βˆšβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = ((βˆšβ€˜π΄) / (βˆšβ€˜(𝑃↑(𝑃 pCnt 𝐴)))))
7268, 70, 71syl2anc 582 . . . . . . . . . 10 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (βˆšβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = ((βˆšβ€˜π΄) / (βˆšβ€˜(𝑃↑(𝑃 pCnt 𝐴)))))
73 nnz 12585 . . . . . . . . . . 11 ((βˆšβ€˜π΄) ∈ β„• β†’ (βˆšβ€˜π΄) ∈ β„€)
74 znq 12942 . . . . . . . . . . 11 (((βˆšβ€˜π΄) ∈ β„€ ∧ (βˆšβ€˜(𝑃↑(𝑃 pCnt 𝐴))) ∈ β„•) β†’ ((βˆšβ€˜π΄) / (βˆšβ€˜(𝑃↑(𝑃 pCnt 𝐴)))) ∈ β„š)
7573, 42, 74syl2an2 682 . . . . . . . . . 10 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ ((βˆšβ€˜π΄) / (βˆšβ€˜(𝑃↑(𝑃 pCnt 𝐴)))) ∈ β„š)
7672, 75eqeltrd 2831 . . . . . . . . 9 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (βˆšβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ β„š)
77 zsqrtelqelz 16700 . . . . . . . . 9 (((𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ β„€ ∧ (βˆšβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ β„š) β†’ (βˆšβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ β„€)
7865, 76, 77syl2anc 582 . . . . . . . 8 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (βˆšβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ β„€)
7963adantr 479 . . . . . . . . . 10 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ β„•)
8079nnrpd 13020 . . . . . . . . 9 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ ℝ+)
8180sqrtgt0d 15365 . . . . . . . 8 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ 0 < (βˆšβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))
82 elnnz 12574 . . . . . . . 8 ((βˆšβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ β„• ↔ ((βˆšβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ β„€ ∧ 0 < (βˆšβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))))
8378, 81, 82sylanbrc 581 . . . . . . 7 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (βˆšβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ β„•)
8483iftrued 4537 . . . . . 6 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ if((βˆšβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ β„•, 1, 0) = 1)
85 fveq2 6892 . . . . . . . . . . 11 (𝑦 = (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) β†’ (βˆšβ€˜π‘¦) = (βˆšβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))
8685eleq1d 2816 . . . . . . . . . 10 (𝑦 = (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) β†’ ((βˆšβ€˜π‘¦) ∈ β„• ↔ (βˆšβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ β„•))
8786ifbid 4552 . . . . . . . . 9 (𝑦 = (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) β†’ if((βˆšβ€˜π‘¦) ∈ β„•, 1, 0) = if((βˆšβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ β„•, 1, 0))
88 fveq2 6892 . . . . . . . . 9 (𝑦 = (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) β†’ (πΉβ€˜π‘¦) = (πΉβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))
8987, 88breq12d 5162 . . . . . . . 8 (𝑦 = (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) β†’ (if((βˆšβ€˜π‘¦) ∈ β„•, 1, 0) ≀ (πΉβ€˜π‘¦) ↔ if((βˆšβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ β„•, 1, 0) ≀ (πΉβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))))
90 dchrisum0flb.4 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘¦ ∈ (1..^𝐴)if((βˆšβ€˜π‘¦) ∈ β„•, 1, 0) ≀ (πΉβ€˜π‘¦))
91 nnuz 12871 . . . . . . . . . 10 β„• = (β„€β‰₯β€˜1)
9263, 91eleqtrdi 2841 . . . . . . . . 9 (πœ‘ β†’ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ (β„€β‰₯β€˜1))
9316nnzd 12591 . . . . . . . . 9 (πœ‘ β†’ 𝐴 ∈ β„€)
9459nnred 12233 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑃 ∈ ℝ)
95 dchrisum0flb.3 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑃 βˆ₯ 𝐴)
96 pcelnn 16809 . . . . . . . . . . . . . 14 ((𝑃 ∈ β„™ ∧ 𝐴 ∈ β„•) β†’ ((𝑃 pCnt 𝐴) ∈ β„• ↔ 𝑃 βˆ₯ 𝐴))
974, 16, 96syl2anc 582 . . . . . . . . . . . . 13 (πœ‘ β†’ ((𝑃 pCnt 𝐴) ∈ β„• ↔ 𝑃 βˆ₯ 𝐴))
9895, 97mpbird 256 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑃 pCnt 𝐴) ∈ β„•)
99 prmuz2 16639 . . . . . . . . . . . . 13 (𝑃 ∈ β„™ β†’ 𝑃 ∈ (β„€β‰₯β€˜2))
100 eluz2gt1 12910 . . . . . . . . . . . . 13 (𝑃 ∈ (β„€β‰₯β€˜2) β†’ 1 < 𝑃)
1014, 99, 1003syl 18 . . . . . . . . . . . 12 (πœ‘ β†’ 1 < 𝑃)
102 expgt1 14072 . . . . . . . . . . . 12 ((𝑃 ∈ ℝ ∧ (𝑃 pCnt 𝐴) ∈ β„• ∧ 1 < 𝑃) β†’ 1 < (𝑃↑(𝑃 pCnt 𝐴)))
10394, 98, 101, 102syl3anc 1369 . . . . . . . . . . 11 (πœ‘ β†’ 1 < (𝑃↑(𝑃 pCnt 𝐴)))
104 1red 11221 . . . . . . . . . . . 12 (πœ‘ β†’ 1 ∈ ℝ)
105 0lt1 11742 . . . . . . . . . . . . 13 0 < 1
106105a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ 0 < 1)
10760nnred 12233 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑃↑(𝑃 pCnt 𝐴)) ∈ ℝ)
10860nngt0d 12267 . . . . . . . . . . . 12 (πœ‘ β†’ 0 < (𝑃↑(𝑃 pCnt 𝐴)))
10916nnred 12233 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐴 ∈ ℝ)
11016nngt0d 12267 . . . . . . . . . . . 12 (πœ‘ β†’ 0 < 𝐴)
111 ltdiv2 12106 . . . . . . . . . . . 12 (((1 ∈ ℝ ∧ 0 < 1) ∧ ((𝑃↑(𝑃 pCnt 𝐴)) ∈ ℝ ∧ 0 < (𝑃↑(𝑃 pCnt 𝐴))) ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) β†’ (1 < (𝑃↑(𝑃 pCnt 𝐴)) ↔ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) < (𝐴 / 1)))
112104, 106, 107, 108, 109, 110, 111syl222anc 1384 . . . . . . . . . . 11 (πœ‘ β†’ (1 < (𝑃↑(𝑃 pCnt 𝐴)) ↔ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) < (𝐴 / 1)))
113103, 112mpbid 231 . . . . . . . . . 10 (πœ‘ β†’ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) < (𝐴 / 1))
11417div1d 11988 . . . . . . . . . 10 (πœ‘ β†’ (𝐴 / 1) = 𝐴)
115113, 114breqtrd 5175 . . . . . . . . 9 (πœ‘ β†’ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) < 𝐴)
116 elfzo2 13641 . . . . . . . . 9 ((𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ (1..^𝐴) ↔ ((𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ (β„€β‰₯β€˜1) ∧ 𝐴 ∈ β„€ ∧ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) < 𝐴))
11792, 93, 115, 116syl3anbrc 1341 . . . . . . . 8 (πœ‘ β†’ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ (1..^𝐴))
11889, 90, 117rspcdva 3614 . . . . . . 7 (πœ‘ β†’ if((βˆšβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ β„•, 1, 0) ≀ (πΉβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))
119118adantr 479 . . . . . 6 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ if((βˆšβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ β„•, 1, 0) ≀ (πΉβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))
12084, 119eqbrtrrd 5173 . . . . 5 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ 1 ≀ (πΉβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))
121 1re 11220 . . . . . . . 8 1 ∈ ℝ
122 0le1 11743 . . . . . . . 8 0 ≀ 1
123121, 122pm3.2i 469 . . . . . . 7 (1 ∈ ℝ ∧ 0 ≀ 1)
124123a1i 11 . . . . . 6 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (1 ∈ ℝ ∧ 0 ≀ 1))
12544, 45, 46, 47, 48, 49, 50, 51, 52dchrisum0ff 27244 . . . . . . . 8 (πœ‘ β†’ 𝐹:β„•βŸΆβ„)
126125, 60ffvelcdmd 7088 . . . . . . 7 (πœ‘ β†’ (πΉβ€˜(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℝ)
127126adantr 479 . . . . . 6 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (πΉβ€˜(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℝ)
128125, 63ffvelcdmd 7088 . . . . . . 7 (πœ‘ β†’ (πΉβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℝ)
129128adantr 479 . . . . . 6 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (πΉβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℝ)
130 lemul12a 12078 . . . . . 6 ((((1 ∈ ℝ ∧ 0 ≀ 1) ∧ (πΉβ€˜(𝑃↑(𝑃 pCnt 𝐴))) ∈ ℝ) ∧ ((1 ∈ ℝ ∧ 0 ≀ 1) ∧ (πΉβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ ℝ)) β†’ ((1 ≀ (πΉβ€˜(𝑃↑(𝑃 pCnt 𝐴))) ∧ 1 ≀ (πΉβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) β†’ (1 Β· 1) ≀ ((πΉβ€˜(𝑃↑(𝑃 pCnt 𝐴))) Β· (πΉβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))))
131124, 127, 124, 129, 130syl22anc 835 . . . . 5 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ ((1 ≀ (πΉβ€˜(𝑃↑(𝑃 pCnt 𝐴))) ∧ 1 ≀ (πΉβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) β†’ (1 Β· 1) ≀ ((πΉβ€˜(𝑃↑(𝑃 pCnt 𝐴))) Β· (πΉβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))))
13256, 120, 131mp2and 695 . . . 4 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ (1 Β· 1) ≀ ((πΉβ€˜(𝑃↑(𝑃 pCnt 𝐴))) Β· (πΉβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))))
1333, 132eqbrtrrid 5185 . . 3 ((πœ‘ ∧ (βˆšβ€˜π΄) ∈ β„•) β†’ 1 ≀ ((πΉβ€˜(𝑃↑(𝑃 pCnt 𝐴))) Β· (πΉβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))))
134 0red 11223 . . . . . 6 (πœ‘ β†’ 0 ∈ ℝ)
135 0re 11222 . . . . . . . 8 0 ∈ ℝ
136121, 135ifcli 4576 . . . . . . 7 if((βˆšβ€˜(𝑃↑(𝑃 pCnt 𝐴))) ∈ β„•, 1, 0) ∈ ℝ
137136a1i 11 . . . . . 6 (πœ‘ β†’ if((βˆšβ€˜(𝑃↑(𝑃 pCnt 𝐴))) ∈ β„•, 1, 0) ∈ ℝ)
138 breq2 5153 . . . . . . . 8 (1 = if((βˆšβ€˜(𝑃↑(𝑃 pCnt 𝐴))) ∈ β„•, 1, 0) β†’ (0 ≀ 1 ↔ 0 ≀ if((βˆšβ€˜(𝑃↑(𝑃 pCnt 𝐴))) ∈ β„•, 1, 0)))
139 breq2 5153 . . . . . . . 8 (0 = if((βˆšβ€˜(𝑃↑(𝑃 pCnt 𝐴))) ∈ β„•, 1, 0) β†’ (0 ≀ 0 ↔ 0 ≀ if((βˆšβ€˜(𝑃↑(𝑃 pCnt 𝐴))) ∈ β„•, 1, 0)))
140 0le0 12319 . . . . . . . 8 0 ≀ 0
141138, 139, 122, 140keephyp 4600 . . . . . . 7 0 ≀ if((βˆšβ€˜(𝑃↑(𝑃 pCnt 𝐴))) ∈ β„•, 1, 0)
142141a1i 11 . . . . . 6 (πœ‘ β†’ 0 ≀ if((βˆšβ€˜(𝑃↑(𝑃 pCnt 𝐴))) ∈ β„•, 1, 0))
143134, 137, 126, 142, 54letrd 11377 . . . . 5 (πœ‘ β†’ 0 ≀ (πΉβ€˜(𝑃↑(𝑃 pCnt 𝐴))))
144121, 135ifcli 4576 . . . . . . 7 if((βˆšβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ β„•, 1, 0) ∈ ℝ
145144a1i 11 . . . . . 6 (πœ‘ β†’ if((βˆšβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ β„•, 1, 0) ∈ ℝ)
146 breq2 5153 . . . . . . . 8 (1 = if((βˆšβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ β„•, 1, 0) β†’ (0 ≀ 1 ↔ 0 ≀ if((βˆšβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ β„•, 1, 0)))
147 breq2 5153 . . . . . . . 8 (0 = if((βˆšβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ β„•, 1, 0) β†’ (0 ≀ 0 ↔ 0 ≀ if((βˆšβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ β„•, 1, 0)))
148146, 147, 122, 140keephyp 4600 . . . . . . 7 0 ≀ if((βˆšβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ β„•, 1, 0)
149148a1i 11 . . . . . 6 (πœ‘ β†’ 0 ≀ if((βˆšβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) ∈ β„•, 1, 0))
150134, 145, 128, 149, 118letrd 11377 . . . . 5 (πœ‘ β†’ 0 ≀ (πΉβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))))
151126, 128, 143, 150mulge0d 11797 . . . 4 (πœ‘ β†’ 0 ≀ ((πΉβ€˜(𝑃↑(𝑃 pCnt 𝐴))) Β· (πΉβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))))
152151adantr 479 . . 3 ((πœ‘ ∧ Β¬ (βˆšβ€˜π΄) ∈ β„•) β†’ 0 ≀ ((πΉβ€˜(𝑃↑(𝑃 pCnt 𝐴))) Β· (πΉβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))))
1531, 2, 133, 152ifbothda 4567 . 2 (πœ‘ β†’ if((βˆšβ€˜π΄) ∈ β„•, 1, 0) ≀ ((πΉβ€˜(𝑃↑(𝑃 pCnt 𝐴))) Β· (πΉβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))))
15460nncnd 12234 . . . . 5 (πœ‘ β†’ (𝑃↑(𝑃 pCnt 𝐴)) ∈ β„‚)
15560nnne0d 12268 . . . . 5 (πœ‘ β†’ (𝑃↑(𝑃 pCnt 𝐴)) β‰  0)
15617, 154, 155divcan2d 11998 . . . 4 (πœ‘ β†’ ((𝑃↑(𝑃 pCnt 𝐴)) Β· (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 𝐴)
157156fveq2d 6896 . . 3 (πœ‘ β†’ (πΉβ€˜((𝑃↑(𝑃 pCnt 𝐴)) Β· (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) = (πΉβ€˜π΄))
158 pcndvds2 16807 . . . . . . 7 ((𝑃 ∈ β„™ ∧ 𝐴 ∈ β„•) β†’ Β¬ 𝑃 βˆ₯ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))
1594, 16, 158syl2anc 582 . . . . . 6 (πœ‘ β†’ Β¬ 𝑃 βˆ₯ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))
160 coprm 16654 . . . . . . 7 ((𝑃 ∈ β„™ ∧ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ β„€) β†’ (Β¬ 𝑃 βˆ₯ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ↔ (𝑃 gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1))
1614, 64, 160syl2anc 582 . . . . . 6 (πœ‘ β†’ (Β¬ 𝑃 βˆ₯ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ↔ (𝑃 gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1))
162159, 161mpbid 231 . . . . 5 (πœ‘ β†’ (𝑃 gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1)
163 prmz 16618 . . . . . . 7 (𝑃 ∈ β„™ β†’ 𝑃 ∈ β„€)
1644, 163syl 17 . . . . . 6 (πœ‘ β†’ 𝑃 ∈ β„€)
165 rpexp1i 16666 . . . . . 6 ((𝑃 ∈ β„€ ∧ (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))) ∈ β„€ ∧ (𝑃 pCnt 𝐴) ∈ β„•0) β†’ ((𝑃 gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1 β†’ ((𝑃↑(𝑃 pCnt 𝐴)) gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1))
166164, 64, 53, 165syl3anc 1369 . . . . 5 (πœ‘ β†’ ((𝑃 gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1 β†’ ((𝑃↑(𝑃 pCnt 𝐴)) gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1))
167162, 166mpd 15 . . . 4 (πœ‘ β†’ ((𝑃↑(𝑃 pCnt 𝐴)) gcd (𝐴 / (𝑃↑(𝑃 pCnt 𝐴)))) = 1)
16844, 45, 46, 47, 48, 49, 50, 51, 60, 63, 167dchrisum0fmul 27243 . . 3 (πœ‘ β†’ (πΉβ€˜((𝑃↑(𝑃 pCnt 𝐴)) Β· (𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))) = ((πΉβ€˜(𝑃↑(𝑃 pCnt 𝐴))) Β· (πΉβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))))
169157, 168eqtr3d 2772 . 2 (πœ‘ β†’ (πΉβ€˜π΄) = ((πΉβ€˜(𝑃↑(𝑃 pCnt 𝐴))) Β· (πΉβ€˜(𝐴 / (𝑃↑(𝑃 pCnt 𝐴))))))
170153, 169breqtrrd 5177 1 (πœ‘ β†’ if((βˆšβ€˜π΄) ∈ β„•, 1, 0) ≀ (πΉβ€˜π΄))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539   ∈ wcel 2104   β‰  wne 2938  βˆ€wral 3059  {crab 3430  ifcif 4529   class class class wbr 5149   ↦ cmpt 5232  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7413  β„‚cc 11112  β„cr 11113  0cc0 11114  1c1 11115   Β· cmul 11119   < clt 11254   ≀ cle 11255   / cdiv 11877  β„•cn 12218  2c2 12273  β„•0cn0 12478  β„€cz 12564  β„€β‰₯cuz 12828  β„šcq 12938  β„+crp 12980  ..^cfzo 13633  β†‘cexp 14033  βˆšcsqrt 15186  Ξ£csu 15638   βˆ₯ cdvds 16203   gcd cgcd 16441  β„™cprime 16614   pCnt cpc 16775  Basecbs 17150  0gc0g 17391  β„€RHomczrh 21270  β„€/nβ„€czn 21273  DChrcdchr 26969
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7729  ax-inf2 9640  ax-cnex 11170  ax-resscn 11171  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-addrcl 11175  ax-mulcl 11176  ax-mulrcl 11177  ax-mulcom 11178  ax-addass 11179  ax-mulass 11180  ax-distr 11181  ax-i2m1 11182  ax-1ne0 11183  ax-1rid 11184  ax-rnegex 11185  ax-rrecex 11186  ax-cnre 11187  ax-pre-lttri 11188  ax-pre-lttrn 11189  ax-pre-ltadd 11190  ax-pre-mulgt0 11191  ax-pre-sup 11192  ax-addf 11193  ax-mulf 11194
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-disj 5115  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-of 7674  df-om 7860  df-1st 7979  df-2nd 7980  df-supp 8151  df-tpos 8215  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-1o 8470  df-2o 8471  df-oadd 8474  df-omul 8475  df-er 8707  df-ec 8709  df-qs 8713  df-map 8826  df-pm 8827  df-ixp 8896  df-en 8944  df-dom 8945  df-sdom 8946  df-fin 8947  df-fsupp 9366  df-fi 9410  df-sup 9441  df-inf 9442  df-oi 9509  df-card 9938  df-acn 9941  df-pnf 11256  df-mnf 11257  df-xr 11258  df-ltxr 11259  df-le 11260  df-sub 11452  df-neg 11453  df-div 11878  df-nn 12219  df-2 12281  df-3 12282  df-4 12283  df-5 12284  df-6 12285  df-7 12286  df-8 12287  df-9 12288  df-n0 12479  df-z 12565  df-dec 12684  df-uz 12829  df-q 12939  df-rp 12981  df-xneg 13098  df-xadd 13099  df-xmul 13100  df-ioo 13334  df-ioc 13335  df-ico 13336  df-icc 13337  df-fz 13491  df-fzo 13634  df-fl 13763  df-mod 13841  df-seq 13973  df-exp 14034  df-fac 14240  df-bc 14269  df-hash 14297  df-shft 15020  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-limsup 15421  df-clim 15438  df-rlim 15439  df-sum 15639  df-ef 16017  df-sin 16019  df-cos 16020  df-pi 16022  df-dvds 16204  df-gcd 16442  df-prm 16615  df-numer 16677  df-denom 16678  df-pc 16776  df-struct 17086  df-sets 17103  df-slot 17121  df-ndx 17133  df-base 17151  df-ress 17180  df-plusg 17216  df-mulr 17217  df-starv 17218  df-sca 17219  df-vsca 17220  df-ip 17221  df-tset 17222  df-ple 17223  df-ds 17225  df-unif 17226  df-hom 17227  df-cco 17228  df-rest 17374  df-topn 17375  df-0g 17393  df-gsum 17394  df-topgen 17395  df-pt 17396  df-prds 17399  df-xrs 17454  df-qtop 17459  df-imas 17460  df-qus 17461  df-xps 17462  df-mre 17536  df-mrc 17537  df-acs 17539  df-mgm 18567  df-sgrp 18646  df-mnd 18662  df-mhm 18707  df-submnd 18708  df-grp 18860  df-minusg 18861  df-sbg 18862  df-mulg 18989  df-subg 19041  df-nsg 19042  df-eqg 19043  df-ghm 19130  df-cntz 19224  df-od 19439  df-cmn 19693  df-abl 19694  df-mgp 20031  df-rng 20049  df-ur 20078  df-ring 20131  df-cring 20132  df-oppr 20227  df-dvdsr 20250  df-unit 20251  df-invr 20281  df-dvr 20294  df-rhm 20365  df-subrng 20436  df-subrg 20461  df-drng 20504  df-lmod 20618  df-lss 20689  df-lsp 20729  df-sra 20932  df-rgmod 20933  df-lidl 20934  df-rsp 20935  df-2idl 21008  df-psmet 21138  df-xmet 21139  df-met 21140  df-bl 21141  df-mopn 21142  df-fbas 21143  df-fg 21144  df-cnfld 21147  df-zring 21220  df-zrh 21274  df-zn 21277  df-top 22618  df-topon 22635  df-topsp 22657  df-bases 22671  df-cld 22745  df-ntr 22746  df-cls 22747  df-nei 22824  df-lp 22862  df-perf 22863  df-cn 22953  df-cnp 22954  df-haus 23041  df-tx 23288  df-hmeo 23481  df-fil 23572  df-fm 23664  df-flim 23665  df-flf 23666  df-xms 24048  df-ms 24049  df-tms 24050  df-cncf 24620  df-limc 25617  df-dv 25618  df-log 26299  df-cxp 26300  df-dchr 26970
This theorem is referenced by:  dchrisum0flb  27247
  Copyright terms: Public domain W3C validator