Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  perfectALTVlem2 Structured version   Visualization version   GIF version

Theorem perfectALTVlem2 45590
Description: Lemma for perfectALTV 45591. (Contributed by Mario Carneiro, 17-May-2016.) (Revised by AV, 1-Jul-2020.)
Hypotheses
Ref Expression
perfectALTVlem.1 (𝜑𝐴 ∈ ℕ)
perfectALTVlem.2 (𝜑𝐵 ∈ ℕ)
perfectALTVlem.3 (𝜑𝐵 ∈ Odd )
perfectALTVlem.4 (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵)))
Assertion
Ref Expression
perfectALTVlem2 (𝜑 → (𝐵 ∈ ℙ ∧ 𝐵 = ((2↑(𝐴 + 1)) − 1)))

Proof of Theorem perfectALTVlem2
Dummy variables 𝑘 𝑛 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 perfectALTVlem.2 . . . 4 (𝜑𝐵 ∈ ℕ)
2 1re 11081 . . . . . 6 1 ∈ ℝ
32a1i 11 . . . . 5 (𝜑 → 1 ∈ ℝ)
4 perfectALTVlem.1 . . . . . . . 8 (𝜑𝐴 ∈ ℕ)
5 perfectALTVlem.3 . . . . . . . 8 (𝜑𝐵 ∈ Odd )
6 perfectALTVlem.4 . . . . . . . 8 (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵)))
74, 1, 5, 6perfectALTVlem1 45589 . . . . . . 7 (𝜑 → ((2↑(𝐴 + 1)) ∈ ℕ ∧ ((2↑(𝐴 + 1)) − 1) ∈ ℕ ∧ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ))
87simp3d 1144 . . . . . 6 (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ)
98nnred 12094 . . . . 5 (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℝ)
101nnred 12094 . . . . 5 (𝜑𝐵 ∈ ℝ)
118nnge1d 12127 . . . . 5 (𝜑 → 1 ≤ (𝐵 / ((2↑(𝐴 + 1)) − 1)))
12 2cn 12154 . . . . . . . . . . 11 2 ∈ ℂ
13 exp1 13894 . . . . . . . . . . 11 (2 ∈ ℂ → (2↑1) = 2)
1412, 13ax-mp 5 . . . . . . . . . 10 (2↑1) = 2
15 df-2 12142 . . . . . . . . . 10 2 = (1 + 1)
1614, 15eqtri 2765 . . . . . . . . 9 (2↑1) = (1 + 1)
17 2re 12153 . . . . . . . . . . 11 2 ∈ ℝ
1817a1i 11 . . . . . . . . . 10 (𝜑 → 2 ∈ ℝ)
19 1zzd 12457 . . . . . . . . . 10 (𝜑 → 1 ∈ ℤ)
204peano2nnd 12096 . . . . . . . . . . 11 (𝜑 → (𝐴 + 1) ∈ ℕ)
2120nnzd 12531 . . . . . . . . . 10 (𝜑 → (𝐴 + 1) ∈ ℤ)
22 1lt2 12250 . . . . . . . . . . 11 1 < 2
2322a1i 11 . . . . . . . . . 10 (𝜑 → 1 < 2)
244nnrpd 12876 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℝ+)
25 ltaddrp 12873 . . . . . . . . . . . 12 ((1 ∈ ℝ ∧ 𝐴 ∈ ℝ+) → 1 < (1 + 𝐴))
262, 24, 25sylancr 588 . . . . . . . . . . 11 (𝜑 → 1 < (1 + 𝐴))
27 ax-1cn 11035 . . . . . . . . . . . 12 1 ∈ ℂ
284nncnd 12095 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℂ)
29 addcom 11267 . . . . . . . . . . . 12 ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 + 𝐴) = (𝐴 + 1))
3027, 28, 29sylancr 588 . . . . . . . . . . 11 (𝜑 → (1 + 𝐴) = (𝐴 + 1))
3126, 30breqtrd 5123 . . . . . . . . . 10 (𝜑 → 1 < (𝐴 + 1))
32 ltexp2a 13990 . . . . . . . . . 10 (((2 ∈ ℝ ∧ 1 ∈ ℤ ∧ (𝐴 + 1) ∈ ℤ) ∧ (1 < 2 ∧ 1 < (𝐴 + 1))) → (2↑1) < (2↑(𝐴 + 1)))
3318, 19, 21, 23, 31, 32syl32anc 1378 . . . . . . . . 9 (𝜑 → (2↑1) < (2↑(𝐴 + 1)))
3416, 33eqbrtrrid 5133 . . . . . . . 8 (𝜑 → (1 + 1) < (2↑(𝐴 + 1)))
357simp1d 1142 . . . . . . . . . 10 (𝜑 → (2↑(𝐴 + 1)) ∈ ℕ)
3635nnred 12094 . . . . . . . . 9 (𝜑 → (2↑(𝐴 + 1)) ∈ ℝ)
373, 3, 36ltaddsubd 11681 . . . . . . . 8 (𝜑 → ((1 + 1) < (2↑(𝐴 + 1)) ↔ 1 < ((2↑(𝐴 + 1)) − 1)))
3834, 37mpbid 231 . . . . . . 7 (𝜑 → 1 < ((2↑(𝐴 + 1)) − 1))
39 1rp 12840 . . . . . . . . 9 1 ∈ ℝ+
4039a1i 11 . . . . . . . 8 (𝜑 → 1 ∈ ℝ+)
41 peano2rem 11394 . . . . . . . . . . 11 ((2↑(𝐴 + 1)) ∈ ℝ → ((2↑(𝐴 + 1)) − 1) ∈ ℝ)
4236, 41syl 17 . . . . . . . . . 10 (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈ ℝ)
43 expgt1 13927 . . . . . . . . . . . 12 ((2 ∈ ℝ ∧ (𝐴 + 1) ∈ ℕ ∧ 1 < 2) → 1 < (2↑(𝐴 + 1)))
4418, 20, 23, 43syl3anc 1371 . . . . . . . . . . 11 (𝜑 → 1 < (2↑(𝐴 + 1)))
45 posdif 11574 . . . . . . . . . . . 12 ((1 ∈ ℝ ∧ (2↑(𝐴 + 1)) ∈ ℝ) → (1 < (2↑(𝐴 + 1)) ↔ 0 < ((2↑(𝐴 + 1)) − 1)))
462, 36, 45sylancr 588 . . . . . . . . . . 11 (𝜑 → (1 < (2↑(𝐴 + 1)) ↔ 0 < ((2↑(𝐴 + 1)) − 1)))
4744, 46mpbid 231 . . . . . . . . . 10 (𝜑 → 0 < ((2↑(𝐴 + 1)) − 1))
4842, 47jca 513 . . . . . . . . 9 (𝜑 → (((2↑(𝐴 + 1)) − 1) ∈ ℝ ∧ 0 < ((2↑(𝐴 + 1)) − 1)))
49 elrp 12838 . . . . . . . . 9 (((2↑(𝐴 + 1)) − 1) ∈ ℝ+ ↔ (((2↑(𝐴 + 1)) − 1) ∈ ℝ ∧ 0 < ((2↑(𝐴 + 1)) − 1)))
5048, 49sylibr 233 . . . . . . . 8 (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈ ℝ+)
51 nnrp 12847 . . . . . . . . 9 (𝐵 ∈ ℕ → 𝐵 ∈ ℝ+)
521, 51syl 17 . . . . . . . 8 (𝜑𝐵 ∈ ℝ+)
5340, 50, 52ltdiv2d 12901 . . . . . . 7 (𝜑 → (1 < ((2↑(𝐴 + 1)) − 1) ↔ (𝐵 / ((2↑(𝐴 + 1)) − 1)) < (𝐵 / 1)))
5438, 53mpbid 231 . . . . . 6 (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) < (𝐵 / 1))
551nncnd 12095 . . . . . . 7 (𝜑𝐵 ∈ ℂ)
5655div1d 11849 . . . . . 6 (𝜑 → (𝐵 / 1) = 𝐵)
5754, 56breqtrd 5123 . . . . 5 (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) < 𝐵)
583, 9, 10, 11, 57lelttrd 11239 . . . 4 (𝜑 → 1 < 𝐵)
59 eluz2b2 12767 . . . 4 (𝐵 ∈ (ℤ‘2) ↔ (𝐵 ∈ ℕ ∧ 1 < 𝐵))
601, 58, 59sylanbrc 584 . . 3 (𝜑𝐵 ∈ (ℤ‘2))
61 fzfid 13799 . . . . . . . . . . . 12 (𝜑 → (1...𝐵) ∈ Fin)
62 dvdsssfz1 16127 . . . . . . . . . . . . 13 (𝐵 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥𝐵} ⊆ (1...𝐵))
631, 62syl 17 . . . . . . . . . . . 12 (𝜑 → {𝑥 ∈ ℕ ∣ 𝑥𝐵} ⊆ (1...𝐵))
64 ssfi 9043 . . . . . . . . . . . 12 (((1...𝐵) ∈ Fin ∧ {𝑥 ∈ ℕ ∣ 𝑥𝐵} ⊆ (1...𝐵)) → {𝑥 ∈ ℕ ∣ 𝑥𝐵} ∈ Fin)
6561, 63, 64syl2anc 585 . . . . . . . . . . 11 (𝜑 → {𝑥 ∈ ℕ ∣ 𝑥𝐵} ∈ Fin)
6665ad2antrr 724 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {𝑥 ∈ ℕ ∣ 𝑥𝐵} ∈ Fin)
67 ssrab2 4029 . . . . . . . . . . . . 13 {𝑥 ∈ ℕ ∣ 𝑥𝐵} ⊆ ℕ
6867a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {𝑥 ∈ ℕ ∣ 𝑥𝐵} ⊆ ℕ)
6968sselda 3936 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 𝑘 ∈ ℕ)
7069nnred 12094 . . . . . . . . . 10 ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 𝑘 ∈ ℝ)
7169nnnn0d 12399 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 𝑘 ∈ ℕ0)
7271nn0ge0d 12402 . . . . . . . . . 10 ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 0 ≤ 𝑘)
73 df-tp 4583 . . . . . . . . . . . 12 {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {𝑛})
74 prssi 4773 . . . . . . . . . . . . . . 15 (((𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ ∧ 𝐵 ∈ ℕ) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ⊆ ℕ)
758, 1, 74syl2anc 585 . . . . . . . . . . . . . 14 (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ⊆ ℕ)
7675ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ⊆ ℕ)
77 simplrl 775 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℕ)
7877snssd 4761 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {𝑛} ⊆ ℕ)
7976, 78unssd 4138 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {𝑛}) ⊆ ℕ)
8073, 79eqsstrid 3984 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ⊆ ℕ)
81 eltpi 4640 . . . . . . . . . . . . 13 (𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵𝑥 = 𝑛))
827simp2d 1143 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈ ℕ)
8382nnzd 12531 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈ ℤ)
848nnzd 12531 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℤ)
85 dvdsmul2 16088 . . . . . . . . . . . . . . . . . 18 ((((2↑(𝐴 + 1)) − 1) ∈ ℤ ∧ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℤ) → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ (((2↑(𝐴 + 1)) − 1) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
8683, 84, 85syl2anc 585 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ (((2↑(𝐴 + 1)) − 1) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
8782nncnd 12095 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈ ℂ)
8882nnne0d 12129 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((2↑(𝐴 + 1)) − 1) ≠ 0)
8955, 87, 88divcan2d 11859 . . . . . . . . . . . . . . . . 17 (𝜑 → (((2↑(𝐴 + 1)) − 1) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) = 𝐵)
9086, 89breqtrd 5123 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ 𝐵)
91 breq1 5100 . . . . . . . . . . . . . . . 16 (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → (𝑥𝐵 ↔ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ 𝐵))
9290, 91syl5ibrcom 247 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 𝑥𝐵))
9392ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 𝑥𝐵))
941nnzd 12531 . . . . . . . . . . . . . . . . 17 (𝜑𝐵 ∈ ℤ)
95 iddvds 16079 . . . . . . . . . . . . . . . . 17 (𝐵 ∈ ℤ → 𝐵𝐵)
9694, 95syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐵𝐵)
97 breq1 5100 . . . . . . . . . . . . . . . 16 (𝑥 = 𝐵 → (𝑥𝐵𝐵𝐵))
9896, 97syl5ibrcom 247 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥 = 𝐵𝑥𝐵))
9998ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 = 𝐵𝑥𝐵))
100 simplrr 776 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛𝐵)
101 breq1 5100 . . . . . . . . . . . . . . 15 (𝑥 = 𝑛 → (𝑥𝐵𝑛𝐵))
102100, 101syl5ibrcom 247 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 = 𝑛𝑥𝐵))
10393, 99, 1023jaod 1428 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ((𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵𝑥 = 𝑛) → 𝑥𝐵))
10481, 103syl5 34 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} → 𝑥𝐵))
105104imp 408 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}) → 𝑥𝐵)
10680, 105ssrabdv 4023 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ⊆ {𝑥 ∈ ℕ ∣ 𝑥𝐵})
10766, 70, 72, 106fsumless 15608 . . . . . . . . 9 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}𝑘 ≤ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}𝑘)
108 simpr 486 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
109 disjsn 4664 . . . . . . . . . . . 12 (({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {𝑛}) = ∅ ↔ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
110108, 109sylibr 233 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {𝑛}) = ∅)
11173a1i 11 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {𝑛}))
112 tpfi 9193 . . . . . . . . . . . 12 {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ∈ Fin
113112a1i 11 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ∈ Fin)
11480sselda 3936 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}) → 𝑘 ∈ ℕ)
115114nncnd 12095 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}) → 𝑘 ∈ ℂ)
116110, 111, 113, 115fsumsplit 15553 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}𝑘 = (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {𝑛}𝑘))
1178nncnd 12095 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℂ)
118 id 22 . . . . . . . . . . . . . . . 16 (𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))
119118sumsn 15558 . . . . . . . . . . . . . . 15 (((𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ ∧ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℂ) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))
1208, 117, 119syl2anc 585 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))
121 id 22 . . . . . . . . . . . . . . . 16 (𝑘 = 𝐵𝑘 = 𝐵)
122121sumsn 15558 . . . . . . . . . . . . . . 15 ((𝐵 ∈ ℕ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ {𝐵}𝑘 = 𝐵)
1231, 55, 122syl2anc 585 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑘 ∈ {𝐵}𝑘 = 𝐵)
124120, 123oveq12d 7360 . . . . . . . . . . . . 13 (𝜑 → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 + Σ𝑘 ∈ {𝐵}𝑘) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + 𝐵))
125 incom 4153 . . . . . . . . . . . . . . 15 ({𝐵} ∩ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}) = ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∩ {𝐵})
1269, 57gtned 11216 . . . . . . . . . . . . . . . 16 (𝜑𝐵 ≠ (𝐵 / ((2↑(𝐴 + 1)) − 1)))
127 disjsn2 4665 . . . . . . . . . . . . . . . 16 (𝐵 ≠ (𝐵 / ((2↑(𝐴 + 1)) − 1)) → ({𝐵} ∩ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}) = ∅)
128126, 127syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ({𝐵} ∩ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}) = ∅)
129125, 128eqtr3id 2791 . . . . . . . . . . . . . 14 (𝜑 → ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∩ {𝐵}) = ∅)
130 df-pr 4581 . . . . . . . . . . . . . . 15 {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∪ {𝐵})
131130a1i 11 . . . . . . . . . . . . . 14 (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∪ {𝐵}))
132 prfi 9192 . . . . . . . . . . . . . . 15 {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∈ Fin
133132a1i 11 . . . . . . . . . . . . . 14 (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∈ Fin)
13475sselda 3936 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑘 ∈ ℕ)
135134nncnd 12095 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑘 ∈ ℂ)
136129, 131, 133, 135fsumsplit 15553 . . . . . . . . . . . . 13 (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 = (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 + Σ𝑘 ∈ {𝐵}𝑘))
13787, 55mulcld 11101 . . . . . . . . . . . . . . 15 (𝜑 → (((2↑(𝐴 + 1)) − 1) · 𝐵) ∈ ℂ)
13855, 137, 87, 88divdird 11895 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + ((((2↑(𝐴 + 1)) − 1) · 𝐵) / ((2↑(𝐴 + 1)) − 1))))
13935nncnd 12095 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (2↑(𝐴 + 1)) ∈ ℂ)
14027a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 1 ∈ ℂ)
141139, 140, 55subdird 11538 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((2↑(𝐴 + 1)) − 1) · 𝐵) = (((2↑(𝐴 + 1)) · 𝐵) − (1 · 𝐵)))
14255mulid2d 11099 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 · 𝐵) = 𝐵)
143142oveq2d 7358 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((2↑(𝐴 + 1)) · 𝐵) − (1 · 𝐵)) = (((2↑(𝐴 + 1)) · 𝐵) − 𝐵))
144141, 143eqtrd 2777 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((2↑(𝐴 + 1)) − 1) · 𝐵) = (((2↑(𝐴 + 1)) · 𝐵) − 𝐵))
145144oveq2d 7358 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) = (𝐵 + (((2↑(𝐴 + 1)) · 𝐵) − 𝐵)))
146139, 55mulcld 11101 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((2↑(𝐴 + 1)) · 𝐵) ∈ ℂ)
14755, 146pncan3d 11441 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵 + (((2↑(𝐴 + 1)) · 𝐵) − 𝐵)) = ((2↑(𝐴 + 1)) · 𝐵))
148145, 147eqtrd 2777 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) = ((2↑(𝐴 + 1)) · 𝐵))
149148oveq1d 7357 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = (((2↑(𝐴 + 1)) · 𝐵) / ((2↑(𝐴 + 1)) − 1)))
150139, 55, 87, 88divassd 11892 . . . . . . . . . . . . . . 15 (𝜑 → (((2↑(𝐴 + 1)) · 𝐵) / ((2↑(𝐴 + 1)) − 1)) = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
151149, 150eqtrd 2777 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
15255, 87, 88divcan3d 11862 . . . . . . . . . . . . . . 15 (𝜑 → ((((2↑(𝐴 + 1)) − 1) · 𝐵) / ((2↑(𝐴 + 1)) − 1)) = 𝐵)
153152oveq2d 7358 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + ((((2↑(𝐴 + 1)) − 1) · 𝐵) / ((2↑(𝐴 + 1)) − 1))) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + 𝐵))
154138, 151, 1533eqtr3d 2785 . . . . . . . . . . . . 13 (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + 𝐵))
155124, 136, 1543eqtr4d 2787 . . . . . . . . . . . 12 (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
156155ad2antrr 724 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
15777nncnd 12095 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℂ)
158 id 22 . . . . . . . . . . . . 13 (𝑘 = 𝑛𝑘 = 𝑛)
159158sumsn 15558 . . . . . . . . . . . 12 ((𝑛 ∈ ℂ ∧ 𝑛 ∈ ℂ) → Σ𝑘 ∈ {𝑛}𝑘 = 𝑛)
160157, 157, 159syl2anc 585 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {𝑛}𝑘 = 𝑛)
161156, 160oveq12d 7360 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {𝑛}𝑘) = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛))
162116, 161eqtrd 2777 . . . . . . . . 9 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}𝑘 = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛))
1634nnnn0d 12399 . . . . . . . . . . . . . . . . 17 (𝜑𝐴 ∈ ℕ0)
164 expp1 13895 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℂ ∧ 𝐴 ∈ ℕ0) → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2))
16512, 163, 164sylancr 588 . . . . . . . . . . . . . . . 16 (𝜑 → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2))
166 2nn 12152 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℕ
167 nnexpcl 13901 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℕ ∧ 𝐴 ∈ ℕ0) → (2↑𝐴) ∈ ℕ)
168166, 163, 167sylancr 588 . . . . . . . . . . . . . . . . . 18 (𝜑 → (2↑𝐴) ∈ ℕ)
169168nncnd 12095 . . . . . . . . . . . . . . . . 17 (𝜑 → (2↑𝐴) ∈ ℂ)
170 mulcom 11063 . . . . . . . . . . . . . . . . 17 (((2↑𝐴) ∈ ℂ ∧ 2 ∈ ℂ) → ((2↑𝐴) · 2) = (2 · (2↑𝐴)))
171169, 12, 170sylancl 587 . . . . . . . . . . . . . . . 16 (𝜑 → ((2↑𝐴) · 2) = (2 · (2↑𝐴)))
172165, 171eqtrd 2777 . . . . . . . . . . . . . . 15 (𝜑 → (2↑(𝐴 + 1)) = (2 · (2↑𝐴)))
173172oveq1d 7357 . . . . . . . . . . . . . 14 (𝜑 → ((2↑(𝐴 + 1)) · 𝐵) = ((2 · (2↑𝐴)) · 𝐵))
17412a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 2 ∈ ℂ)
175174, 169, 55mulassd 11104 . . . . . . . . . . . . . 14 (𝜑 → ((2 · (2↑𝐴)) · 𝐵) = (2 · ((2↑𝐴) · 𝐵)))
176 isodd7 45533 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ Odd ↔ (𝐵 ∈ ℤ ∧ (2 gcd 𝐵) = 1))
177 simpr 486 . . . . . . . . . . . . . . . . . . 19 ((𝐵 ∈ ℤ ∧ (2 gcd 𝐵) = 1) → (2 gcd 𝐵) = 1)
178176, 177sylbi 216 . . . . . . . . . . . . . . . . . 18 (𝐵 ∈ Odd → (2 gcd 𝐵) = 1)
1795, 178syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (2 gcd 𝐵) = 1)
180 2z 12458 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℤ
181180a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → 2 ∈ ℤ)
182 rpexp1i 16526 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℕ0) → ((2 gcd 𝐵) = 1 → ((2↑𝐴) gcd 𝐵) = 1))
183181, 94, 163, 182syl3anc 1371 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2 gcd 𝐵) = 1 → ((2↑𝐴) gcd 𝐵) = 1))
184179, 183mpd 15 . . . . . . . . . . . . . . . 16 (𝜑 → ((2↑𝐴) gcd 𝐵) = 1)
185 sgmmul 26455 . . . . . . . . . . . . . . . 16 ((1 ∈ ℂ ∧ ((2↑𝐴) ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ((2↑𝐴) gcd 𝐵) = 1)) → (1 σ ((2↑𝐴) · 𝐵)) = ((1 σ (2↑𝐴)) · (1 σ 𝐵)))
186140, 168, 1, 184, 185syl13anc 1372 . . . . . . . . . . . . . . 15 (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = ((1 σ (2↑𝐴)) · (1 σ 𝐵)))
187 pncan 11333 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐴 + 1) − 1) = 𝐴)
18828, 27, 187sylancl 587 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐴 + 1) − 1) = 𝐴)
189188oveq2d 7358 . . . . . . . . . . . . . . . . . 18 (𝜑 → (2↑((𝐴 + 1) − 1)) = (2↑𝐴))
190189oveq2d 7358 . . . . . . . . . . . . . . . . 17 (𝜑 → (1 σ (2↑((𝐴 + 1) − 1))) = (1 σ (2↑𝐴)))
191 1sgm2ppw 26454 . . . . . . . . . . . . . . . . . 18 ((𝐴 + 1) ∈ ℕ → (1 σ (2↑((𝐴 + 1) − 1))) = ((2↑(𝐴 + 1)) − 1))
19220, 191syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (1 σ (2↑((𝐴 + 1) − 1))) = ((2↑(𝐴 + 1)) − 1))
193190, 192eqtr3d 2779 . . . . . . . . . . . . . . . 16 (𝜑 → (1 σ (2↑𝐴)) = ((2↑(𝐴 + 1)) − 1))
194193oveq1d 7357 . . . . . . . . . . . . . . 15 (𝜑 → ((1 σ (2↑𝐴)) · (1 σ 𝐵)) = (((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)))
195186, 6, 1943eqtr3d 2785 . . . . . . . . . . . . . 14 (𝜑 → (2 · ((2↑𝐴) · 𝐵)) = (((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)))
196173, 175, 1953eqtrd 2781 . . . . . . . . . . . . 13 (𝜑 → ((2↑(𝐴 + 1)) · 𝐵) = (((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)))
197196oveq1d 7357 . . . . . . . . . . . 12 (𝜑 → (((2↑(𝐴 + 1)) · 𝐵) / ((2↑(𝐴 + 1)) − 1)) = ((((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)) / ((2↑(𝐴 + 1)) − 1)))
198 1nn0 12355 . . . . . . . . . . . . . . 15 1 ∈ ℕ0
199 sgmnncl 26402 . . . . . . . . . . . . . . 15 ((1 ∈ ℕ0𝐵 ∈ ℕ) → (1 σ 𝐵) ∈ ℕ)
200198, 1, 199sylancr 588 . . . . . . . . . . . . . 14 (𝜑 → (1 σ 𝐵) ∈ ℕ)
201200nncnd 12095 . . . . . . . . . . . . 13 (𝜑 → (1 σ 𝐵) ∈ ℂ)
202201, 87, 88divcan3d 11862 . . . . . . . . . . . 12 (𝜑 → ((((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = (1 σ 𝐵))
203197, 150, 2023eqtr3d 2785 . . . . . . . . . . 11 (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) = (1 σ 𝐵))
204 sgmval 26397 . . . . . . . . . . . 12 ((1 ∈ ℂ ∧ 𝐵 ∈ ℕ) → (1 σ 𝐵) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵} (𝑘𝑐1))
20527, 1, 204sylancr 588 . . . . . . . . . . 11 (𝜑 → (1 σ 𝐵) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵} (𝑘𝑐1))
206 simpr 486 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵})
20767, 206sselid 3934 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 𝑘 ∈ ℕ)
208207nncnd 12095 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 𝑘 ∈ ℂ)
209208cxp1d 25967 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → (𝑘𝑐1) = 𝑘)
210209sumeq2dv 15515 . . . . . . . . . . 11 (𝜑 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵} (𝑘𝑐1) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}𝑘)
211203, 205, 2103eqtrrd 2782 . . . . . . . . . 10 (𝜑 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
212211ad2antrr 724 . . . . . . . . 9 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
213107, 162, 2123brtr3d 5128 . . . . . . . 8 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
21436, 9remulcld 11111 . . . . . . . . . . 11 (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) ∈ ℝ)
215214ad2antrr 724 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) ∈ ℝ)
21677nnrpd 12876 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℝ+)
217215, 216ltaddrpd 12911 . . . . . . . . 9 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛))
21877nnred 12094 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℝ)
219215, 218readdcld 11110 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ∈ ℝ)
220215, 219ltnled 11228 . . . . . . . . 9 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ↔ ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))))
221217, 220mpbid 231 . . . . . . . 8 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
222213, 221condan 816 . . . . . . 7 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) → 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
223 elpri 4600 . . . . . . 7 (𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))
224222, 223syl 17 . . . . . 6 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))
225224expr 458 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (𝑛𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)))
226225ralrimiva 3140 . . . 4 (𝜑 → ∀𝑛 ∈ ℕ (𝑛𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)))
2273, 58gtned 11216 . . . . . . . . . 10 (𝜑𝐵 ≠ 1)
228227necomd 2997 . . . . . . . . 9 (𝜑 → 1 ≠ 𝐵)
229 1nn 12090 . . . . . . . . . . . . 13 1 ∈ ℕ
230229a1i 11 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℕ)
231 1dvds 16080 . . . . . . . . . . . . 13 (𝐵 ∈ ℤ → 1 ∥ 𝐵)
23294, 231syl 17 . . . . . . . . . . . 12 (𝜑 → 1 ∥ 𝐵)
233 breq1 5100 . . . . . . . . . . . . . 14 (𝑛 = 1 → (𝑛𝐵 ↔ 1 ∥ 𝐵))
234 eqeq1 2741 . . . . . . . . . . . . . . 15 (𝑛 = 1 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ↔ 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1))))
235 eqeq1 2741 . . . . . . . . . . . . . . 15 (𝑛 = 1 → (𝑛 = 𝐵 ↔ 1 = 𝐵))
236234, 235orbi12d 917 . . . . . . . . . . . . . 14 (𝑛 = 1 → ((𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵) ↔ (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵)))
237233, 236imbi12d 345 . . . . . . . . . . . . 13 (𝑛 = 1 → ((𝑛𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)) ↔ (1 ∥ 𝐵 → (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵))))
238237rspcv 3570 . . . . . . . . . . . 12 (1 ∈ ℕ → (∀𝑛 ∈ ℕ (𝑛𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)) → (1 ∥ 𝐵 → (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵))))
239230, 226, 232, 238syl3c 66 . . . . . . . . . . 11 (𝜑 → (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵))
240239ord 862 . . . . . . . . . 10 (𝜑 → (¬ 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 1 = 𝐵))
241240necon1ad 2958 . . . . . . . . 9 (𝜑 → (1 ≠ 𝐵 → 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1))))
242228, 241mpd 15 . . . . . . . 8 (𝜑 → 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))
243242eqeq2d 2748 . . . . . . 7 (𝜑 → (𝑛 = 1 ↔ 𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1))))
244243orbi1d 915 . . . . . 6 (𝜑 → ((𝑛 = 1 ∨ 𝑛 = 𝐵) ↔ (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)))
245244imbi2d 341 . . . . 5 (𝜑 → ((𝑛𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵)) ↔ (𝑛𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))))
246245ralbidv 3171 . . . 4 (𝜑 → (∀𝑛 ∈ ℕ (𝑛𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵)) ↔ ∀𝑛 ∈ ℕ (𝑛𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))))
247226, 246mpbird 257 . . 3 (𝜑 → ∀𝑛 ∈ ℕ (𝑛𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵)))
248 isprm2 16485 . . 3 (𝐵 ∈ ℙ ↔ (𝐵 ∈ (ℤ‘2) ∧ ∀𝑛 ∈ ℕ (𝑛𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵))))
24960, 247, 248sylanbrc 584 . 2 (𝜑𝐵 ∈ ℙ)
250214ltp1d 12011 . . . 4 (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1))
251 peano2re 11254 . . . . . 6 (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) ∈ ℝ → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ∈ ℝ)
252214, 251syl 17 . . . . 5 (𝜑 → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ∈ ℝ)
253214, 252ltnled 11228 . . . 4 (𝜑 → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ↔ ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))))
254250, 253mpbid 231 . . 3 (𝜑 → ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
255207nnred 12094 . . . . . . . 8 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 𝑘 ∈ ℝ)
256207nnnn0d 12399 . . . . . . . . 9 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 𝑘 ∈ ℕ0)
257256nn0ge0d 12402 . . . . . . . 8 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 0 ≤ 𝑘)
258 df-tp 4583 . . . . . . . . . 10 {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {1})
259 snssi 4760 . . . . . . . . . . . 12 (1 ∈ ℕ → {1} ⊆ ℕ)
260229, 259mp1i 13 . . . . . . . . . . 11 (𝜑 → {1} ⊆ ℕ)
26175, 260unssd 4138 . . . . . . . . . 10 (𝜑 → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {1}) ⊆ ℕ)
262258, 261eqsstrid 3984 . . . . . . . . 9 (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ⊆ ℕ)
263 eltpi 4640 . . . . . . . . . . 11 (𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵𝑥 = 1))
264 breq1 5100 . . . . . . . . . . . . 13 (𝑥 = 1 → (𝑥𝐵 ↔ 1 ∥ 𝐵))
265232, 264syl5ibrcom 247 . . . . . . . . . . . 12 (𝜑 → (𝑥 = 1 → 𝑥𝐵))
26692, 98, 2653jaod 1428 . . . . . . . . . . 11 (𝜑 → ((𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵𝑥 = 1) → 𝑥𝐵))
267263, 266syl5 34 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} → 𝑥𝐵))
268267imp 408 . . . . . . . . 9 ((𝜑𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}) → 𝑥𝐵)
269262, 268ssrabdv 4023 . . . . . . . 8 (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ⊆ {𝑥 ∈ ℕ ∣ 𝑥𝐵})
27065, 255, 257, 269fsumless 15608 . . . . . . 7 (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 ≤ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}𝑘)
271270adantr 482 . . . . . 6 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 ≤ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}𝑘)
27255, 87, 88diveq1ad 11866 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 / ((2↑(𝐴 + 1)) − 1)) = 1 ↔ 𝐵 = ((2↑(𝐴 + 1)) − 1)))
273272necon3bid 2986 . . . . . . . . . . . 12 (𝜑 → ((𝐵 / ((2↑(𝐴 + 1)) − 1)) ≠ 1 ↔ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)))
274273biimpar 479 . . . . . . . . . . 11 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ≠ 1)
275274necomd 2997 . . . . . . . . . 10 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → 1 ≠ (𝐵 / ((2↑(𝐴 + 1)) − 1)))
276228adantr 482 . . . . . . . . . 10 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → 1 ≠ 𝐵)
277275, 276nelprd 4609 . . . . . . . . 9 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → ¬ 1 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
278 disjsn 4664 . . . . . . . . 9 (({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {1}) = ∅ ↔ ¬ 1 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
279277, 278sylibr 233 . . . . . . . 8 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {1}) = ∅)
280258a1i 11 . . . . . . . 8 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {1}))
281 tpfi 9193 . . . . . . . . 9 {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ∈ Fin
282281a1i 11 . . . . . . . 8 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ∈ Fin)
283262adantr 482 . . . . . . . . . 10 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ⊆ ℕ)
284283sselda 3936 . . . . . . . . 9 (((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}) → 𝑘 ∈ ℕ)
285284nncnd 12095 . . . . . . . 8 (((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}) → 𝑘 ∈ ℂ)
286279, 280, 282, 285fsumsplit 15553 . . . . . . 7 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 = (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {1}𝑘))
287 id 22 . . . . . . . . . . 11 (𝑘 = 1 → 𝑘 = 1)
288287sumsn 15558 . . . . . . . . . 10 ((1 ∈ ℂ ∧ 1 ∈ ℂ) → Σ𝑘 ∈ {1}𝑘 = 1)
289140, 27, 288sylancl 587 . . . . . . . . 9 (𝜑 → Σ𝑘 ∈ {1}𝑘 = 1)
290155, 289oveq12d 7360 . . . . . . . 8 (𝜑 → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {1}𝑘) = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1))
291290adantr 482 . . . . . . 7 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {1}𝑘) = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1))
292286, 291eqtrd 2777 . . . . . 6 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1))
293211adantr 482 . . . . . 6 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
294271, 292, 2933brtr3d 5128 . . . . 5 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
295294ex 414 . . . 4 (𝜑 → (𝐵 ≠ ((2↑(𝐴 + 1)) − 1) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))))
296295necon1bd 2959 . . 3 (𝜑 → (¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) → 𝐵 = ((2↑(𝐴 + 1)) − 1)))
297254, 296mpd 15 . 2 (𝜑𝐵 = ((2↑(𝐴 + 1)) − 1))
298249, 297jca 513 1 (𝜑 → (𝐵 ∈ ℙ ∧ 𝐵 = ((2↑(𝐴 + 1)) − 1)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wo 845  w3o 1086   = wceq 1541  wcel 2106  wne 2941  wral 3062  {crab 3404  cun 3900  cin 3901  wss 3902  c0 4274  {csn 4578  {cpr 4580  {ctp 4582   class class class wbr 5097  cfv 6484  (class class class)co 7342  Fincfn 8809  cc 10975  cr 10976  0cc0 10977  1c1 10978   + caddc 10980   · cmul 10982   < clt 11115  cle 11116  cmin 11311   / cdiv 11738  cn 12079  2c2 12134  0cn0 12339  cz 12425  cuz 12688  +crp 12836  ...cfz 13345  cexp 13888  Σcsu 15497  cdvds 16063   gcd cgcd 16301  cprime 16474  𝑐ccxp 25817   σ csgm 26351   Odd codd 45493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5234  ax-sep 5248  ax-nul 5255  ax-pow 5313  ax-pr 5377  ax-un 7655  ax-inf2 9503  ax-cnex 11033  ax-resscn 11034  ax-1cn 11035  ax-icn 11036  ax-addcl 11037  ax-addrcl 11038  ax-mulcl 11039  ax-mulrcl 11040  ax-mulcom 11041  ax-addass 11042  ax-mulass 11043  ax-distr 11044  ax-i2m1 11045  ax-1ne0 11046  ax-1rid 11047  ax-rnegex 11048  ax-rrecex 11049  ax-cnre 11050  ax-pre-lttri 11051  ax-pre-lttrn 11052  ax-pre-ltadd 11053  ax-pre-mulgt0 11054  ax-pre-sup 11055  ax-addf 11056  ax-mulf 11057
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3444  df-sbc 3732  df-csb 3848  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3921  df-nul 4275  df-if 4479  df-pw 4554  df-sn 4579  df-pr 4581  df-tp 4583  df-op 4585  df-uni 4858  df-int 4900  df-iun 4948  df-iin 4949  df-br 5098  df-opab 5160  df-mpt 5181  df-tr 5215  df-id 5523  df-eprel 5529  df-po 5537  df-so 5538  df-fr 5580  df-se 5581  df-we 5582  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6243  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6436  df-fun 6486  df-fn 6487  df-f 6488  df-f1 6489  df-fo 6490  df-f1o 6491  df-fv 6492  df-isom 6493  df-riota 7298  df-ov 7345  df-oprab 7346  df-mpo 7347  df-of 7600  df-om 7786  df-1st 7904  df-2nd 7905  df-supp 8053  df-frecs 8172  df-wrecs 8203  df-recs 8277  df-rdg 8316  df-1o 8372  df-2o 8373  df-er 8574  df-map 8693  df-pm 8694  df-ixp 8762  df-en 8810  df-dom 8811  df-sdom 8812  df-fin 8813  df-fsupp 9232  df-fi 9273  df-sup 9304  df-inf 9305  df-oi 9372  df-card 9801  df-pnf 11117  df-mnf 11118  df-xr 11119  df-ltxr 11120  df-le 11121  df-sub 11313  df-neg 11314  df-div 11739  df-nn 12080  df-2 12142  df-3 12143  df-4 12144  df-5 12145  df-6 12146  df-7 12147  df-8 12148  df-9 12149  df-n0 12340  df-z 12426  df-dec 12544  df-uz 12689  df-q 12795  df-rp 12837  df-xneg 12954  df-xadd 12955  df-xmul 12956  df-ioo 13189  df-ioc 13190  df-ico 13191  df-icc 13192  df-fz 13346  df-fzo 13489  df-fl 13618  df-mod 13696  df-seq 13828  df-exp 13889  df-fac 14094  df-bc 14123  df-hash 14151  df-shft 14878  df-cj 14910  df-re 14911  df-im 14912  df-sqrt 15046  df-abs 15047  df-limsup 15280  df-clim 15297  df-rlim 15298  df-sum 15498  df-ef 15877  df-sin 15879  df-cos 15880  df-pi 15882  df-dvds 16064  df-gcd 16302  df-prm 16475  df-pc 16636  df-struct 16946  df-sets 16963  df-slot 16981  df-ndx 16993  df-base 17011  df-ress 17040  df-plusg 17073  df-mulr 17074  df-starv 17075  df-sca 17076  df-vsca 17077  df-ip 17078  df-tset 17079  df-ple 17080  df-ds 17082  df-unif 17083  df-hom 17084  df-cco 17085  df-rest 17231  df-topn 17232  df-0g 17250  df-gsum 17251  df-topgen 17252  df-pt 17253  df-prds 17256  df-xrs 17311  df-qtop 17316  df-imas 17317  df-xps 17319  df-mre 17393  df-mrc 17394  df-acs 17396  df-mgm 18424  df-sgrp 18473  df-mnd 18484  df-submnd 18529  df-mulg 18798  df-cntz 19020  df-cmn 19484  df-psmet 20695  df-xmet 20696  df-met 20697  df-bl 20698  df-mopn 20699  df-fbas 20700  df-fg 20701  df-cnfld 20704  df-top 22149  df-topon 22166  df-topsp 22188  df-bases 22202  df-cld 22276  df-ntr 22277  df-cls 22278  df-nei 22355  df-lp 22393  df-perf 22394  df-cn 22484  df-cnp 22485  df-haus 22572  df-tx 22819  df-hmeo 23012  df-fil 23103  df-fm 23195  df-flim 23196  df-flf 23197  df-xms 23579  df-ms 23580  df-tms 23581  df-cncf 24147  df-limc 25136  df-dv 25137  df-log 25818  df-cxp 25819  df-sgm 26357  df-even 45494  df-odd 45495
This theorem is referenced by:  perfectALTV  45591
  Copyright terms: Public domain W3C validator