Users' Mathboxes Mathbox for metakunt < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  aks4d1p3 Structured version   Visualization version   GIF version

Theorem aks4d1p3 39849
Description: There exists a small enough number such that it does not divide 𝐴. (Contributed by metakunt, 27-Oct-2024.)
Hypotheses
Ref Expression
aks4d1p3.1 (𝜑𝑁 ∈ (ℤ‘3))
aks4d1p3.2 𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))
aks4d1p3.3 𝐵 = (⌈‘((2 logb 𝑁)↑5))
Assertion
Ref Expression
aks4d1p3 (𝜑 → ∃𝑟 ∈ (1...𝐵) ¬ 𝑟𝐴)
Distinct variable groups:   𝐴,𝑟   𝐵,𝑟   𝑘,𝑁   𝜑,𝑘
Allowed substitution hints:   𝜑(𝑟)   𝐴(𝑘)   𝐵(𝑘)   𝑁(𝑟)

Proof of Theorem aks4d1p3
Dummy variable 𝑞 is distinct from all other variables.
StepHypRef Expression
1 aks4d1p3.1 . . . . . 6 (𝜑𝑁 ∈ (ℤ‘3))
2 aks4d1p3.2 . . . . . 6 𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))
3 aks4d1p3.3 . . . . . 6 𝐵 = (⌈‘((2 logb 𝑁)↑5))
41, 2, 3aks4d1p1 39847 . . . . 5 (𝜑𝐴 < (2↑𝐵))
54adantr 484 . . . 4 ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟𝐴) → 𝐴 < (2↑𝐵))
6 2re 11929 . . . . . . . . 9 2 ∈ ℝ
76a1i 11 . . . . . . . 8 (𝜑 → 2 ∈ ℝ)
83a1i 11 . . . . . . . . . . 11 (𝜑𝐵 = (⌈‘((2 logb 𝑁)↑5)))
9 2pos 11958 . . . . . . . . . . . . . . 15 0 < 2
109a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 0 < 2)
11 eluzelz 12473 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ ℤ)
121, 11syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℤ)
1312zred 12307 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℝ)
14 0red 10861 . . . . . . . . . . . . . . 15 (𝜑 → 0 ∈ ℝ)
15 3re 11935 . . . . . . . . . . . . . . . 16 3 ∈ ℝ
1615a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 3 ∈ ℝ)
17 3pos 11960 . . . . . . . . . . . . . . . 16 0 < 3
1817a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 0 < 3)
19 eluzle 12476 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ‘3) → 3 ≤ 𝑁)
201, 19syl 17 . . . . . . . . . . . . . . 15 (𝜑 → 3 ≤ 𝑁)
2114, 16, 13, 18, 20ltletrd 11017 . . . . . . . . . . . . . 14 (𝜑 → 0 < 𝑁)
22 1red 10859 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ∈ ℝ)
23 1lt2 12026 . . . . . . . . . . . . . . . . 17 1 < 2
2423a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 1 < 2)
2522, 24ltned 10993 . . . . . . . . . . . . . . 15 (𝜑 → 1 ≠ 2)
2625necomd 2997 . . . . . . . . . . . . . 14 (𝜑 → 2 ≠ 1)
277, 10, 13, 21, 26relogbcld 39744 . . . . . . . . . . . . 13 (𝜑 → (2 logb 𝑁) ∈ ℝ)
28 5nn0 12135 . . . . . . . . . . . . . 14 5 ∈ ℕ0
2928a1i 11 . . . . . . . . . . . . 13 (𝜑 → 5 ∈ ℕ0)
3027, 29reexpcld 13761 . . . . . . . . . . . 12 (𝜑 → ((2 logb 𝑁)↑5) ∈ ℝ)
31 ceilcl 13442 . . . . . . . . . . . 12 (((2 logb 𝑁)↑5) ∈ ℝ → (⌈‘((2 logb 𝑁)↑5)) ∈ ℤ)
3230, 31syl 17 . . . . . . . . . . 11 (𝜑 → (⌈‘((2 logb 𝑁)↑5)) ∈ ℤ)
338, 32eqeltrd 2839 . . . . . . . . . 10 (𝜑𝐵 ∈ ℤ)
3432zred 12307 . . . . . . . . . . . 12 (𝜑 → (⌈‘((2 logb 𝑁)↑5)) ∈ ℝ)
358, 34eqeltrd 2839 . . . . . . . . . . 11 (𝜑𝐵 ∈ ℝ)
36 7re 11948 . . . . . . . . . . . . . . 15 7 ∈ ℝ
3736a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 7 ∈ ℝ)
38 7pos 11966 . . . . . . . . . . . . . . 15 0 < 7
3938a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 0 < 7)
4013, 203lexlogpow5ineq3 39829 . . . . . . . . . . . . . 14 (𝜑 → 7 < ((2 logb 𝑁)↑5))
4114, 37, 30, 39, 40lttrd 11018 . . . . . . . . . . . . 13 (𝜑 → 0 < ((2 logb 𝑁)↑5))
42 ceilge 13445 . . . . . . . . . . . . . 14 (((2 logb 𝑁)↑5) ∈ ℝ → ((2 logb 𝑁)↑5) ≤ (⌈‘((2 logb 𝑁)↑5)))
4330, 42syl 17 . . . . . . . . . . . . 13 (𝜑 → ((2 logb 𝑁)↑5) ≤ (⌈‘((2 logb 𝑁)↑5)))
4414, 30, 34, 41, 43ltletrd 11017 . . . . . . . . . . . 12 (𝜑 → 0 < (⌈‘((2 logb 𝑁)↑5)))
4544, 8breqtrrd 5096 . . . . . . . . . . 11 (𝜑 → 0 < 𝐵)
4614, 35, 45ltled 11005 . . . . . . . . . 10 (𝜑 → 0 ≤ 𝐵)
4733, 46jca 515 . . . . . . . . 9 (𝜑 → (𝐵 ∈ ℤ ∧ 0 ≤ 𝐵))
48 elnn0z 12214 . . . . . . . . 9 (𝐵 ∈ ℕ0 ↔ (𝐵 ∈ ℤ ∧ 0 ≤ 𝐵))
4947, 48sylibr 237 . . . . . . . 8 (𝜑𝐵 ∈ ℕ0)
507, 49reexpcld 13761 . . . . . . 7 (𝜑 → (2↑𝐵) ∈ ℝ)
5150adantr 484 . . . . . 6 ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟𝐴) → (2↑𝐵) ∈ ℝ)
52 elfznn 13166 . . . . . . . . . . . . 13 (𝑞 ∈ (1...𝐵) → 𝑞 ∈ ℕ)
5352adantl 485 . . . . . . . . . . . 12 ((𝜑𝑞 ∈ (1...𝐵)) → 𝑞 ∈ ℕ)
5453nnzd 12306 . . . . . . . . . . 11 ((𝜑𝑞 ∈ (1...𝐵)) → 𝑞 ∈ ℤ)
5554ex 416 . . . . . . . . . 10 (𝜑 → (𝑞 ∈ (1...𝐵) → 𝑞 ∈ ℤ))
5655ssrdv 3922 . . . . . . . . 9 (𝜑 → (1...𝐵) ⊆ ℤ)
57 fzfid 13573 . . . . . . . . 9 (𝜑 → (1...𝐵) ∈ Fin)
58 lcmfcl 16213 . . . . . . . . 9 (((1...𝐵) ⊆ ℤ ∧ (1...𝐵) ∈ Fin) → (lcm‘(1...𝐵)) ∈ ℕ0)
5956, 57, 58syl2anc 587 . . . . . . . 8 (𝜑 → (lcm‘(1...𝐵)) ∈ ℕ0)
6059nn0red 12176 . . . . . . 7 (𝜑 → (lcm‘(1...𝐵)) ∈ ℝ)
6160adantr 484 . . . . . 6 ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟𝐴) → (lcm‘(1...𝐵)) ∈ ℝ)
622a1i 11 . . . . . . . . 9 (𝜑𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1)))
63 elnnz 12211 . . . . . . . . . . . 12 (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁))
6412, 21, 63sylanbrc 586 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℕ)
657, 10, 35, 45, 26relogbcld 39744 . . . . . . . . . . . . . 14 (𝜑 → (2 logb 𝐵) ∈ ℝ)
6665flcld 13398 . . . . . . . . . . . . 13 (𝜑 → (⌊‘(2 logb 𝐵)) ∈ ℤ)
677, 10, 7, 10, 26relogbcld 39744 . . . . . . . . . . . . . . 15 (𝜑 → (2 logb 2) ∈ ℝ)
68 0le1 11380 . . . . . . . . . . . . . . . . 17 0 ≤ 1
6968a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ 1)
707recnd 10886 . . . . . . . . . . . . . . . . . 18 (𝜑 → 2 ∈ ℂ)
7114, 10gtned 10992 . . . . . . . . . . . . . . . . . 18 (𝜑 → 2 ≠ 0)
72 logbid1 25678 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1) → (2 logb 2) = 1)
7370, 71, 26, 72syl3anc 1373 . . . . . . . . . . . . . . . . 17 (𝜑 → (2 logb 2) = 1)
7473eqcomd 2744 . . . . . . . . . . . . . . . 16 (𝜑 → 1 = (2 logb 2))
7569, 74breqtrd 5094 . . . . . . . . . . . . . . 15 (𝜑 → 0 ≤ (2 logb 2))
76 2z 12234 . . . . . . . . . . . . . . . . 17 2 ∈ ℤ
7776a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 2 ∈ ℤ)
787leidd 11423 . . . . . . . . . . . . . . . 16 (𝜑 → 2 ≤ 2)
79 2lt7 12045 . . . . . . . . . . . . . . . . . . 19 2 < 7
8079a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → 2 < 7)
817, 37, 80ltled 11005 . . . . . . . . . . . . . . . . 17 (𝜑 → 2 ≤ 7)
8237, 30, 34, 40, 43ltletrd 11017 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 7 < (⌈‘((2 logb 𝑁)↑5)))
8382, 8breqtrrd 5096 . . . . . . . . . . . . . . . . . 18 (𝜑 → 7 < 𝐵)
8437, 35, 83ltled 11005 . . . . . . . . . . . . . . . . 17 (𝜑 → 7 ≤ 𝐵)
857, 37, 35, 81, 84letrd 11014 . . . . . . . . . . . . . . . 16 (𝜑 → 2 ≤ 𝐵)
8677, 78, 7, 10, 35, 45, 85logblebd 39747 . . . . . . . . . . . . . . 15 (𝜑 → (2 logb 2) ≤ (2 logb 𝐵))
8714, 67, 65, 75, 86letrd 11014 . . . . . . . . . . . . . 14 (𝜑 → 0 ≤ (2 logb 𝐵))
88 0zd 12213 . . . . . . . . . . . . . . 15 (𝜑 → 0 ∈ ℤ)
89 flge 13405 . . . . . . . . . . . . . . 15 (((2 logb 𝐵) ∈ ℝ ∧ 0 ∈ ℤ) → (0 ≤ (2 logb 𝐵) ↔ 0 ≤ (⌊‘(2 logb 𝐵))))
9065, 88, 89syl2anc 587 . . . . . . . . . . . . . 14 (𝜑 → (0 ≤ (2 logb 𝐵) ↔ 0 ≤ (⌊‘(2 logb 𝐵))))
9187, 90mpbid 235 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ (⌊‘(2 logb 𝐵)))
9266, 91jca 515 . . . . . . . . . . . 12 (𝜑 → ((⌊‘(2 logb 𝐵)) ∈ ℤ ∧ 0 ≤ (⌊‘(2 logb 𝐵))))
93 elnn0z 12214 . . . . . . . . . . . 12 ((⌊‘(2 logb 𝐵)) ∈ ℕ0 ↔ ((⌊‘(2 logb 𝐵)) ∈ ℤ ∧ 0 ≤ (⌊‘(2 logb 𝐵))))
9492, 93sylibr 237 . . . . . . . . . . 11 (𝜑 → (⌊‘(2 logb 𝐵)) ∈ ℕ0)
9564, 94nnexpcld 13840 . . . . . . . . . 10 (𝜑 → (𝑁↑(⌊‘(2 logb 𝐵))) ∈ ℕ)
96 fzfid 13573 . . . . . . . . . . 11 (𝜑 → (1...(⌊‘((2 logb 𝑁)↑2))) ∈ Fin)
9712adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 𝑁 ∈ ℤ)
98 elfznn 13166 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2))) → 𝑘 ∈ ℕ)
9998adantl 485 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 𝑘 ∈ ℕ)
10099nnnn0d 12175 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 𝑘 ∈ ℕ0)
101 zexpcl 13677 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℤ ∧ 𝑘 ∈ ℕ0) → (𝑁𝑘) ∈ ℤ)
10297, 100, 101syl2anc 587 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → (𝑁𝑘) ∈ ℤ)
103 1zzd 12233 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 1 ∈ ℤ)
104102, 103zsubcld 12312 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → ((𝑁𝑘) − 1) ∈ ℤ)
105 1cnd 10853 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 1 ∈ ℂ)
106105addid1d 11057 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → (1 + 0) = 1)
10722adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 1 ∈ ℝ)
108 1nn0 12131 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℕ0
109108a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → 1 ∈ ℕ0)
11013, 109reexpcld 13761 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑁↑1) ∈ ℝ)
111110adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → (𝑁↑1) ∈ ℝ)
112102zred 12307 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → (𝑁𝑘) ∈ ℝ)
113 1lt3 12028 . . . . . . . . . . . . . . . . . . . 20 1 < 3
114113a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 1 < 3)
11522, 16, 13, 114, 20ltletrd 11017 . . . . . . . . . . . . . . . . . 18 (𝜑 → 1 < 𝑁)
11613recnd 10886 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑁 ∈ ℂ)
117116exp1d 13739 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑁↑1) = 𝑁)
118117eqcomd 2744 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 = (𝑁↑1))
119115, 118breqtrd 5094 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 < (𝑁↑1))
120119adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 1 < (𝑁↑1))
12113adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 𝑁 ∈ ℝ)
12264nnge1d 11903 . . . . . . . . . . . . . . . . . 18 (𝜑 → 1 ≤ 𝑁)
123122adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 1 ≤ 𝑁)
124 elfzuz 13133 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2))) → 𝑘 ∈ (ℤ‘1))
125124adantl 485 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 𝑘 ∈ (ℤ‘1))
126121, 123, 125leexp2ad 13851 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → (𝑁↑1) ≤ (𝑁𝑘))
127107, 111, 112, 120, 126ltletrd 11017 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 1 < (𝑁𝑘))
128106, 127eqbrtrd 5090 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → (1 + 0) < (𝑁𝑘))
12914adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 0 ∈ ℝ)
130107, 129, 112ltaddsub2d 11458 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → ((1 + 0) < (𝑁𝑘) ↔ 0 < ((𝑁𝑘) − 1)))
131128, 130mpbid 235 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 0 < ((𝑁𝑘) − 1))
132104, 131jca 515 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → (((𝑁𝑘) − 1) ∈ ℤ ∧ 0 < ((𝑁𝑘) − 1)))
133 elnnz 12211 . . . . . . . . . . . 12 (((𝑁𝑘) − 1) ∈ ℕ ↔ (((𝑁𝑘) − 1) ∈ ℤ ∧ 0 < ((𝑁𝑘) − 1)))
134132, 133sylibr 237 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → ((𝑁𝑘) − 1) ∈ ℕ)
13596, 134fprodnncl 15545 . . . . . . . . . 10 (𝜑 → ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1) ∈ ℕ)
13695, 135nnmulcld 11908 . . . . . . . . 9 (𝜑 → ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1)) ∈ ℕ)
13762, 136eqeltrd 2839 . . . . . . . 8 (𝜑𝐴 ∈ ℕ)
138137nnred 11870 . . . . . . 7 (𝜑𝐴 ∈ ℝ)
139138adantr 484 . . . . . 6 ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟𝐴) → 𝐴 ∈ ℝ)
1401, 2, 3aks4d1p2 39848 . . . . . . 7 (𝜑 → (2↑𝐵) ≤ (lcm‘(1...𝐵)))
141140adantr 484 . . . . . 6 ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟𝐴) → (2↑𝐵) ≤ (lcm‘(1...𝐵)))
142137nnzd 12306 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℤ)
143142adantr 484 . . . . . . . . . 10 ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟𝐴) → 𝐴 ∈ ℤ)
14456adantr 484 . . . . . . . . . 10 ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟𝐴) → (1...𝐵) ⊆ ℤ)
145 fzfid 13573 . . . . . . . . . 10 ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟𝐴) → (1...𝐵) ∈ Fin)
146 lcmfdvdsb 16228 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ (1...𝐵) ⊆ ℤ ∧ (1...𝐵) ∈ Fin) → (∀𝑟 ∈ (1...𝐵)𝑟𝐴 ↔ (lcm‘(1...𝐵)) ∥ 𝐴))
147143, 144, 145, 146syl3anc 1373 . . . . . . . . 9 ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟𝐴) → (∀𝑟 ∈ (1...𝐵)𝑟𝐴 ↔ (lcm‘(1...𝐵)) ∥ 𝐴))
148147biimpd 232 . . . . . . . 8 ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟𝐴) → (∀𝑟 ∈ (1...𝐵)𝑟𝐴 → (lcm‘(1...𝐵)) ∥ 𝐴))
149148syldbl2 841 . . . . . . 7 ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟𝐴) → (lcm‘(1...𝐵)) ∥ 𝐴)
15059nn0zd 12305 . . . . . . . . 9 (𝜑 → (lcm‘(1...𝐵)) ∈ ℤ)
151150adantr 484 . . . . . . . 8 ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟𝐴) → (lcm‘(1...𝐵)) ∈ ℤ)
152137adantr 484 . . . . . . . 8 ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟𝐴) → 𝐴 ∈ ℕ)
153 dvdsle 15899 . . . . . . . 8 (((lcm‘(1...𝐵)) ∈ ℤ ∧ 𝐴 ∈ ℕ) → ((lcm‘(1...𝐵)) ∥ 𝐴 → (lcm‘(1...𝐵)) ≤ 𝐴))
154151, 152, 153syl2anc 587 . . . . . . 7 ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟𝐴) → ((lcm‘(1...𝐵)) ∥ 𝐴 → (lcm‘(1...𝐵)) ≤ 𝐴))
155149, 154mpd 15 . . . . . 6 ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟𝐴) → (lcm‘(1...𝐵)) ≤ 𝐴)
15651, 61, 139, 141, 155letrd 11014 . . . . 5 ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟𝐴) → (2↑𝐵) ≤ 𝐴)
15751, 139lenltd 11003 . . . . 5 ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟𝐴) → ((2↑𝐵) ≤ 𝐴 ↔ ¬ 𝐴 < (2↑𝐵)))
158156, 157mpbid 235 . . . 4 ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟𝐴) → ¬ 𝐴 < (2↑𝐵))
1595, 158pm2.21dd 198 . . 3 ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟𝐴) → ¬ ∀𝑟 ∈ (1...𝐵)𝑟𝐴)
160 simpr 488 . . 3 ((𝜑 ∧ ¬ ∀𝑟 ∈ (1...𝐵)𝑟𝐴) → ¬ ∀𝑟 ∈ (1...𝐵)𝑟𝐴)
161159, 160pm2.61dan 813 . 2 (𝜑 → ¬ ∀𝑟 ∈ (1...𝐵)𝑟𝐴)
162 rexnal 3164 . 2 (∃𝑟 ∈ (1...𝐵) ¬ 𝑟𝐴 ↔ ¬ ∀𝑟 ∈ (1...𝐵)𝑟𝐴)
163161, 162sylibr 237 1 (𝜑 → ∃𝑟 ∈ (1...𝐵) ¬ 𝑟𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399   = wceq 1543  wcel 2111  wne 2941  wral 3062  wrex 3063  wss 3881   class class class wbr 5068  cfv 6398  (class class class)co 7232  Fincfn 8647  cc 10752  cr 10753  0cc0 10754  1c1 10755   + caddc 10757   · cmul 10759   < clt 10892  cle 10893  cmin 11087  cn 11855  2c2 11910  3c3 11911  5c5 11913  7c7 11915  0cn0 12115  cz 12201  cuz 12463  ...cfz 13120  cfl 13390  cceil 13391  cexp 13662  cprod 15495  cdvds 15843  lcmclcmf 16174   logb clogb 25674
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-rep 5194  ax-sep 5207  ax-nul 5214  ax-pow 5273  ax-pr 5337  ax-un 7542  ax-inf2 9281  ax-cc 10074  ax-cnex 10810  ax-resscn 10811  ax-1cn 10812  ax-icn 10813  ax-addcl 10814  ax-addrcl 10815  ax-mulcl 10816  ax-mulrcl 10817  ax-mulcom 10818  ax-addass 10819  ax-mulass 10820  ax-distr 10821  ax-i2m1 10822  ax-1ne0 10823  ax-1rid 10824  ax-rnegex 10825  ax-rrecex 10826  ax-cnre 10827  ax-pre-lttri 10828  ax-pre-lttrn 10829  ax-pre-ltadd 10830  ax-pre-mulgt0 10831  ax-pre-sup 10832  ax-addf 10833  ax-mulf 10834
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-reu 3069  df-rmo 3070  df-rab 3071  df-v 3423  df-sbc 3710  df-csb 3827  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-symdif 4172  df-nul 4253  df-if 4455  df-pw 4530  df-sn 4557  df-pr 4559  df-tp 4561  df-op 4563  df-uni 4835  df-int 4875  df-iun 4921  df-iin 4922  df-disj 5034  df-br 5069  df-opab 5131  df-mpt 5151  df-tr 5177  df-id 5470  df-eprel 5475  df-po 5483  df-so 5484  df-fr 5524  df-se 5525  df-we 5526  df-xp 5572  df-rel 5573  df-cnv 5574  df-co 5575  df-dm 5576  df-rn 5577  df-res 5578  df-ima 5579  df-pred 6176  df-ord 6234  df-on 6235  df-lim 6236  df-suc 6237  df-iota 6356  df-fun 6400  df-fn 6401  df-f 6402  df-f1 6403  df-fo 6404  df-f1o 6405  df-fv 6406  df-isom 6407  df-riota 7189  df-ov 7235  df-oprab 7236  df-mpo 7237  df-of 7488  df-ofr 7489  df-om 7664  df-1st 7780  df-2nd 7781  df-supp 7925  df-wrecs 8068  df-recs 8129  df-rdg 8167  df-1o 8223  df-2o 8224  df-oadd 8227  df-omul 8228  df-er 8412  df-map 8531  df-pm 8532  df-ixp 8600  df-en 8648  df-dom 8649  df-sdom 8650  df-fin 8651  df-fsupp 9011  df-fi 9052  df-sup 9083  df-inf 9084  df-oi 9151  df-dju 9542  df-card 9580  df-acn 9583  df-pnf 10894  df-mnf 10895  df-xr 10896  df-ltxr 10897  df-le 10898  df-sub 11089  df-neg 11090  df-div 11515  df-nn 11856  df-2 11918  df-3 11919  df-4 11920  df-5 11921  df-6 11922  df-7 11923  df-8 11924  df-9 11925  df-n0 12116  df-z 12202  df-dec 12319  df-uz 12464  df-q 12570  df-rp 12612  df-xneg 12729  df-xadd 12730  df-xmul 12731  df-ioo 12964  df-ioc 12965  df-ico 12966  df-icc 12967  df-fz 13121  df-fzo 13264  df-fl 13392  df-ceil 13393  df-mod 13470  df-seq 13602  df-exp 13663  df-fac 13868  df-bc 13897  df-hash 13925  df-shft 14658  df-cj 14690  df-re 14691  df-im 14692  df-sqrt 14826  df-abs 14827  df-limsup 15060  df-clim 15077  df-rlim 15078  df-sum 15278  df-prod 15496  df-ef 15657  df-e 15658  df-sin 15659  df-cos 15660  df-pi 15662  df-dvds 15844  df-gcd 16082  df-lcm 16175  df-lcmf 16176  df-prm 16257  df-struct 16728  df-sets 16745  df-slot 16763  df-ndx 16773  df-base 16789  df-ress 16813  df-plusg 16843  df-mulr 16844  df-starv 16845  df-sca 16846  df-vsca 16847  df-ip 16848  df-tset 16849  df-ple 16850  df-ds 16852  df-unif 16853  df-hom 16854  df-cco 16855  df-rest 16955  df-topn 16956  df-0g 16974  df-gsum 16975  df-topgen 16976  df-pt 16977  df-prds 16980  df-xrs 17035  df-qtop 17040  df-imas 17041  df-xps 17043  df-mre 17117  df-mrc 17118  df-acs 17120  df-mgm 18142  df-sgrp 18191  df-mnd 18202  df-submnd 18247  df-mulg 18517  df-cntz 18739  df-cmn 19200  df-psmet 20383  df-xmet 20384  df-met 20385  df-bl 20386  df-mopn 20387  df-fbas 20388  df-fg 20389  df-cnfld 20392  df-top 21818  df-topon 21835  df-topsp 21857  df-bases 21870  df-cld 21943  df-ntr 21944  df-cls 21945  df-nei 22022  df-lp 22060  df-perf 22061  df-cn 22151  df-cnp 22152  df-haus 22239  df-cmp 22311  df-tx 22486  df-hmeo 22679  df-fil 22770  df-fm 22862  df-flim 22863  df-flf 22864  df-xms 23245  df-ms 23246  df-tms 23247  df-cncf 23802  df-ovol 24388  df-vol 24389  df-mbf 24543  df-itg1 24544  df-itg2 24545  df-ibl 24546  df-itg 24547  df-0p 24594  df-limc 24790  df-dv 24791  df-log 25472  df-cxp 25473  df-logb 25675
This theorem is referenced by:  aks4d1p4  39850  aks4d1p5  39851  aks4d1p7  39854
  Copyright terms: Public domain W3C validator