Metamath Proof Explorer

Theorem aks6d1c2

Description: Claim 2 of Theorem 6.1 of https://www3.nd.edu/%7eandyp/notes/AKS.pdf (Contributed by metakunt, 2-May-2025)

Ref Expression
Hypotheses aks6d1c2a.1 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) }
aks6d1c2a.2 ⊢ 𝑃 = ( chr ‘ 𝐾 )
aks6d1c2a.3 ⊢ ( 𝜑 → 𝐾 ∈ Field )
aks6d1c2a.4 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
aks6d1c2a.5 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
aks6d1c2a.6 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
aks6d1c2a.7 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
aks6d1c2a.8 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
aks6d1c2a.10 ⊢ 𝐺 = ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
aks6d1c2a.11 ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
aks6d1c2a.12 ⊢ 𝐸 = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
aks6d1c2a.13 ⊢ 𝐿 = ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) )
aks6d1c2a.14 ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )
aks6d1c2a.15 ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
aks6d1c2a.16 ⊢ ( 𝜑 → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
aks6d1c2a.17 ⊢ 𝐻 = ( ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ ℎ ) ) ‘ 𝑀 ) )
aks6d1c2a.18 ⊢ 𝐵 = ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) )
aks6d1c2a.19 ⊢ 𝐶 = ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) )
aks6d1c2a.20 ⊢ ( 𝜑 → ( 𝑄 ∈ ℙ ∧ 𝑄 ∥ 𝑁 ∧ 𝑃 ≠ 𝑄 ) )
Assertion aks6d1c2 ( 𝜑 → ( ♯ ‘ ( 𝐻 “ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ) ≤ ( 𝑁 ↑ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 aks6d1c2a.1 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) }
2 aks6d1c2a.2 ⊢ 𝑃 = ( chr ‘ 𝐾 )
3 aks6d1c2a.3 ⊢ ( 𝜑 → 𝐾 ∈ Field )
4 aks6d1c2a.4 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5 aks6d1c2a.5 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
6 aks6d1c2a.6 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
7 aks6d1c2a.7 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
8 aks6d1c2a.8 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
9 aks6d1c2a.10 ⊢ 𝐺 = ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
10 aks6d1c2a.11 ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
11 aks6d1c2a.12 ⊢ 𝐸 = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
12 aks6d1c2a.13 ⊢ 𝐿 = ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) )
13 aks6d1c2a.14 ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )
14 aks6d1c2a.15 ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
15 aks6d1c2a.16 ⊢ ( 𝜑 → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
16 aks6d1c2a.17 ⊢ 𝐻 = ( ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ ℎ ) ) ‘ 𝑀 ) )
17 aks6d1c2a.18 ⊢ 𝐵 = ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) )
18 aks6d1c2a.19 ⊢ 𝐶 = ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) )
19 aks6d1c2a.20 ⊢ ( 𝜑 → ( 𝑄 ∈ ℙ ∧ 𝑄 ∥ 𝑁 ∧ 𝑃 ≠ 𝑄 ) )
20 simpl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑏 < 𝑐 ∧ ∃ 𝑑 ∈ ℕ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) ) → ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) )
21 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑏 < 𝑐 ∧ ∃ 𝑑 ∈ ℕ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) ) → 𝑏 < 𝑐 )
22 20 21 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑏 < 𝑐 ∧ ∃ 𝑑 ∈ ℕ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) ) → ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑏 < 𝑐 ) )
23 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑏 < 𝑐 ∧ ∃ 𝑑 ∈ ℕ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) ) → ∃ 𝑑 ∈ ℕ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) )
24 22 23 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑏 < 𝑐 ∧ ∃ 𝑑 ∈ ℕ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) ) → ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑏 < 𝑐 ) ∧ ∃ 𝑑 ∈ ℕ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) )
25 3 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑏 < 𝑐 ) ∧ 𝑑 ∈ ℕ ) ∧ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) → 𝐾 ∈ Field )
26 4 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑏 < 𝑐 ) ∧ 𝑑 ∈ ℕ ) ∧ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) → 𝑃 ∈ ℙ )
27 5 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑏 < 𝑐 ) ∧ 𝑑 ∈ ℕ ) ∧ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) → 𝑅 ∈ ℕ )
28 6 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑏 < 𝑐 ) ∧ 𝑑 ∈ ℕ ) ∧ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) → 𝑁 ∈ ℕ )
29 7 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑏 < 𝑐 ) ∧ 𝑑 ∈ ℕ ) ∧ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) → 𝑃 ∥ 𝑁 )
30 8 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑏 < 𝑐 ) ∧ 𝑑 ∈ ℕ ) ∧ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) → ( 𝑁 gcd 𝑅 ) = 1 )
31 0nn0 ⊢ 0 ∈ ℕ0
32 31 a1i ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑏 < 𝑐 ) ∧ 𝑑 ∈ ℕ ) ∧ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝐴 ) ) → 0 ∈ ℕ0 )
33 eqid ⊢ ( 𝑗 ∈ ( 0 ... 𝐴 ) ↦ 0 ) = ( 𝑗 ∈ ( 0 ... 𝐴 ) ↦ 0 )
34 32 33 fmptd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑏 < 𝑐 ) ∧ 𝑑 ∈ ℕ ) ∧ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) → ( 𝑗 ∈ ( 0 ... 𝐴 ) ↦ 0 ) : ( 0 ... 𝐴 ) ⟶ ℕ0 )
35 10 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑏 < 𝑐 ) ∧ 𝑑 ∈ ℕ ) ∧ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) → 𝐴 ∈ ℕ0 )
36 13 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑏 < 𝑐 ) ∧ 𝑑 ∈ ℕ ) ∧ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )
37 14 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑏 < 𝑐 ) ∧ 𝑑 ∈ ℕ ) ∧ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
38 15 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑏 < 𝑐 ) ∧ 𝑑 ∈ ℕ ) ∧ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
39 simp-5r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑏 < 𝑐 ) ∧ 𝑑 ∈ ℕ ) ∧ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) → 𝑏 ∈ 𝐶 )
40 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑏 < 𝑐 ) ∧ 𝑑 ∈ ℕ ) ∧ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) → 𝑐 ∈ 𝐶 )
41 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑏 < 𝑐 ) ∧ 𝑑 ∈ ℕ ) ∧ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) → 𝑏 < 𝑐 )
42 eqid ⊢ ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
43 eqid ⊢ ( var1 ‘ 𝐾 ) = ( var1 ‘ 𝐾 )
44 eqid ⊢ ( ( 𝑐 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( var1 ‘ 𝐾 ) ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑏 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( var1 ‘ 𝐾 ) ) ) = ( ( 𝑐 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( var1 ‘ 𝐾 ) ) ( -g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝑏 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( var1 ‘ 𝐾 ) ) )
45 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑏 < 𝑐 ) ∧ 𝑑 ∈ ℕ ) ∧ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) → 𝑑 ∈ ℕ )
46 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑏 < 𝑐 ) ∧ 𝑑 ∈ ℕ ) ∧ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) → 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) )
47 1 2 25 26 27 28 29 30 34 9 35 11 12 36 37 38 16 17 18 39 40 41 42 43 44 45 46 aks6d1c2lem4 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑏 < 𝑐 ) ∧ 𝑑 ∈ ℕ ) ∧ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) → ( ♯ ‘ ( 𝐻 “ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ) ≤ ( 𝑁 ↑ 𝐵 ) )
48 47 ex ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑏 < 𝑐 ) ∧ 𝑑 ∈ ℕ ) → ( 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) → ( ♯ ‘ ( 𝐻 “ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ) ≤ ( 𝑁 ↑ 𝐵 ) ) )
49 48 rexlimdva ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑏 < 𝑐 ) → ( ∃ 𝑑 ∈ ℕ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) → ( ♯ ‘ ( 𝐻 “ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ) ≤ ( 𝑁 ↑ 𝐵 ) ) )
50 49 imp ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ 𝑏 < 𝑐 ) ∧ ∃ 𝑑 ∈ ℕ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) → ( ♯ ‘ ( 𝐻 “ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ) ≤ ( 𝑁 ↑ 𝐵 ) )
51 24 50 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑏 < 𝑐 ∧ ∃ 𝑑 ∈ ℕ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) ) → ( ♯ ‘ ( 𝐻 “ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ) ≤ ( 𝑁 ↑ 𝐵 ) )
52 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) → 𝑏 < 𝑐 )
53 nfcv ⊢ Ⅎ 𝑠 ( 𝐿 ‘ 𝑡 )
54 nfcv ⊢ Ⅎ 𝑡 ( 𝐿 ‘ 𝑠 )
55 fveq2 ⊢ ( 𝑡 = 𝑠 → ( 𝐿 ‘ 𝑡 ) = ( 𝐿 ‘ 𝑠 ) )
56 53 54 55 cbvmpt ⊢ ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) = ( 𝑠 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑠 ) )
57 56 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) → ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) = ( 𝑠 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑠 ) ) )
58 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ 𝑠 = 𝑏 ) → 𝑠 = 𝑏 )
59 58 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ 𝑠 = 𝑏 ) → ( 𝐿 ‘ 𝑠 ) = ( 𝐿 ‘ 𝑏 ) )
60 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) → 𝑏 ∈ 𝐶 )
61 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) → ( 𝐿 ‘ 𝑏 ) ∈ V )
62 57 59 60 61 fvmptd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) → ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( 𝐿 ‘ 𝑏 ) )
63 62 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) → ( 𝐿 ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) )
64 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) → ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) )
65 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ 𝑠 = 𝑐 ) → 𝑠 = 𝑐 )
66 65 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ 𝑠 = 𝑐 ) → ( 𝐿 ‘ 𝑠 ) = ( 𝐿 ‘ 𝑐 ) )
67 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) → 𝑐 ∈ 𝐶 )
68 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) → ( 𝐿 ‘ 𝑐 ) ∈ V )
69 57 66 67 68 fvmptd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) → ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) = ( 𝐿 ‘ 𝑐 ) )
70 64 69 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) → ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( 𝐿 ‘ 𝑐 ) )
71 63 70 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) → ( 𝐿 ‘ 𝑏 ) = ( 𝐿 ‘ 𝑐 ) )
72 71 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) → ( 𝐿 ‘ 𝑐 ) = ( 𝐿 ‘ 𝑏 ) )
73 5 nnnn0d ⊢ ( 𝜑 → 𝑅 ∈ ℕ0 )
74 73 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) → 𝑅 ∈ ℕ0 )
75 74 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) → 𝑅 ∈ ℕ0 )
76 75 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) → 𝑅 ∈ ℕ0 )
77 fz0ssnn0 ⊢ ( 0 ... 𝐵 ) ⊆ ℕ0
78 77 a1i ⊢ ( 𝜑 → ( 0 ... 𝐵 ) ⊆ ℕ0 )
79 78 78 jca ⊢ ( 𝜑 → ( ( 0 ... 𝐵 ) ⊆ ℕ0 ∧ ( 0 ... 𝐵 ) ⊆ ℕ0 ) )
80 eqid ⊢ ( ℤ/nℤ ‘ 𝑅 ) = ( ℤ/nℤ ‘ 𝑅 )
81 6 4 7 5 8 11 12 80 hashscontpowcl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℕ0 )
82 81 nn0red ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℝ )
83 81 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) )
84 82 83 resqrtcld ⊢ ( 𝜑 → ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ∈ ℝ )
85 84 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ∈ ℤ )
86 82 83 sqrtge0d ⊢ ( 𝜑 → 0 ≤ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) )
87 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
88 flge ⊢ ( ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ∈ ℝ ∧ 0 ∈ ℤ ) → ( 0 ≤ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ↔ 0 ≤ ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) )
89 84 87 88 syl2anc ⊢ ( 𝜑 → ( 0 ≤ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ↔ 0 ≤ ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) )
90 86 89 mpbid ⊢ ( 𝜑 → 0 ≤ ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) )
91 85 90 jca ⊢ ( 𝜑 → ( ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) )
92 elnn0z ⊢ ( ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ∈ ℕ0 ↔ ( ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) )
93 91 92 sylibr ⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ∈ ℕ0 )
94 17 a1i ⊢ ( 𝜑 → 𝐵 = ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) )
95 94 eleq1d ⊢ ( 𝜑 → ( 𝐵 ∈ ℕ0 ↔ ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ∈ ℕ0 ) )
96 93 95 mpbird ⊢ ( 𝜑 → 𝐵 ∈ ℕ0 )
97 96 nn0ge0d ⊢ ( 𝜑 → 0 ≤ 𝐵 )
98 96 nn0zd ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
99 eluz ⊢ ( ( 0 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐵 ∈ ( ℤ≥ ‘ 0 ) ↔ 0 ≤ 𝐵 ) )
100 87 98 99 syl2anc ⊢ ( 𝜑 → ( 𝐵 ∈ ( ℤ≥ ‘ 0 ) ↔ 0 ≤ 𝐵 ) )
101 97 100 mpbird ⊢ ( 𝜑 → 𝐵 ∈ ( ℤ≥ ‘ 0 ) )
102 fzn0 ⊢ ( ( 0 ... 𝐵 ) ≠ ∅ ↔ 𝐵 ∈ ( ℤ≥ ‘ 0 ) )
103 101 102 sylibr ⊢ ( 𝜑 → ( 0 ... 𝐵 ) ≠ ∅ )
104 103 103 jca ⊢ ( 𝜑 → ( ( 0 ... 𝐵 ) ≠ ∅ ∧ ( 0 ... 𝐵 ) ≠ ∅ ) )
105 xpnz ⊢ ( ( ( 0 ... 𝐵 ) ≠ ∅ ∧ ( 0 ... 𝐵 ) ≠ ∅ ) ↔ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ≠ ∅ )
106 105 biimpi ⊢ ( ( ( 0 ... 𝐵 ) ≠ ∅ ∧ ( 0 ... 𝐵 ) ≠ ∅ ) → ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ≠ ∅ )
107 104 106 syl ⊢ ( 𝜑 → ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ≠ ∅ )
108 ssxpb ⊢ ( ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ≠ ∅ → ( ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ⊆ ( ℕ0 × ℕ0 ) ↔ ( ( 0 ... 𝐵 ) ⊆ ℕ0 ∧ ( 0 ... 𝐵 ) ⊆ ℕ0 ) ) )
109 107 108 syl ⊢ ( 𝜑 → ( ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ⊆ ( ℕ0 × ℕ0 ) ↔ ( ( 0 ... 𝐵 ) ⊆ ℕ0 ∧ ( 0 ... 𝐵 ) ⊆ ℕ0 ) ) )
110 79 109 mpbird ⊢ ( 𝜑 → ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ⊆ ( ℕ0 × ℕ0 ) )
111 imass2 ⊢ ( ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ⊆ ( ℕ0 × ℕ0 ) → ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) ⊆ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) )
112 110 111 syl ⊢ ( 𝜑 → ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) ⊆ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) )
113 nfv ⊢ Ⅎ 𝑜 𝜑
114 19 simp1d ⊢ ( 𝜑 → 𝑄 ∈ ℙ )
115 19 simp2d ⊢ ( 𝜑 → 𝑄 ∥ 𝑁 )
116 19 simp3d ⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
117 6 4 7 11 114 115 116 aks6d1c2p2 ⊢ ( 𝜑 → 𝐸 : ( ℕ0 × ℕ0 ) –1-1→ ℕ )
118 f1f ⊢ ( 𝐸 : ( ℕ0 × ℕ0 ) –1-1→ ℕ → 𝐸 : ( ℕ0 × ℕ0 ) ⟶ ℕ )
119 117 118 syl ⊢ ( 𝜑 → 𝐸 : ( ℕ0 × ℕ0 ) ⟶ ℕ )
120 119 ffnd ⊢ ( 𝜑 → 𝐸 Fn ( ℕ0 × ℕ0 ) )
121 120 fnfund ⊢ ( 𝜑 → Fun 𝐸 )
122 119 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑜 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝐸 ‘ 𝑜 ) ∈ ℕ )
123 113 121 122 funimassd ⊢ ( 𝜑 → ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ⊆ ℕ )
124 112 123 sstrd ⊢ ( 𝜑 → ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) ⊆ ℕ )
125 18 a1i ⊢ ( 𝜑 → 𝐶 = ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) )
126 125 sseq1d ⊢ ( 𝜑 → ( 𝐶 ⊆ ℕ ↔ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) ⊆ ℕ ) )
127 124 126 mpbird ⊢ ( 𝜑 → 𝐶 ⊆ ℕ )
128 127 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) → 𝐶 ⊆ ℕ )
129 simpr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) → 𝑐 ∈ 𝐶 )
130 128 129 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) → 𝑐 ∈ ℕ )
131 130 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) → 𝑐 ∈ ℤ )
132 131 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) → 𝑐 ∈ ℤ )
133 simplr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) → 𝑏 ∈ 𝐶 )
134 128 133 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) → 𝑏 ∈ ℕ )
135 134 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) → 𝑏 ∈ ℤ )
136 135 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) → 𝑏 ∈ ℤ )
137 80 12 zndvds ⊢ ( ( 𝑅 ∈ ℕ0 ∧ 𝑐 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( ( 𝐿 ‘ 𝑐 ) = ( 𝐿 ‘ 𝑏 ) ↔ 𝑅 ∥ ( 𝑐 − 𝑏 ) ) )
138 76 132 136 137 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) → ( ( 𝐿 ‘ 𝑐 ) = ( 𝐿 ‘ 𝑏 ) ↔ 𝑅 ∥ ( 𝑐 − 𝑏 ) ) )
139 72 138 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) → 𝑅 ∥ ( 𝑐 − 𝑏 ) )
140 76 nn0zd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) → 𝑅 ∈ ℤ )
141 132 136 zsubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) → ( 𝑐 − 𝑏 ) ∈ ℤ )
142 divides ⊢ ( ( 𝑅 ∈ ℤ ∧ ( 𝑐 − 𝑏 ) ∈ ℤ ) → ( 𝑅 ∥ ( 𝑐 − 𝑏 ) ↔ ∃ 𝑑 ∈ ℤ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) )
143 140 141 142 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) → ( 𝑅 ∥ ( 𝑐 − 𝑏 ) ↔ ∃ 𝑑 ∈ ℤ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) )
144 143 biimpd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) → ( 𝑅 ∥ ( 𝑐 − 𝑏 ) → ∃ 𝑑 ∈ ℤ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) )
145 139 144 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) → ∃ 𝑑 ∈ ℤ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) )
146 simprl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → 𝑑 ∈ ℤ )
147 130 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → 𝑐 ∈ ℕ )
148 147 nnred ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → 𝑐 ∈ ℝ )
149 134 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → 𝑏 ∈ ℕ )
150 149 nnred ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → 𝑏 ∈ ℝ )
151 148 150 resubcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → ( 𝑐 − 𝑏 ) ∈ ℝ )
152 5 nnrpd ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
153 152 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) → 𝑅 ∈ ℝ+ )
154 153 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) → 𝑅 ∈ ℝ+ )
155 154 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) → 𝑅 ∈ ℝ+ )
156 155 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → 𝑅 ∈ ℝ+ )
157 156 rpred ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → 𝑅 ∈ ℝ )
158 52 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → 𝑏 < 𝑐 )
159 150 148 posdifd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → ( 𝑏 < 𝑐 ↔ 0 < ( 𝑐 − 𝑏 ) ) )
160 158 159 mpbid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → 0 < ( 𝑐 − 𝑏 ) )
161 156 rpgt0d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → 0 < 𝑅 )
162 151 157 160 161 divgt0d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → 0 < ( ( 𝑐 − 𝑏 ) / 𝑅 ) )
163 157 recnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → 𝑅 ∈ ℂ )
164 146 zred ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → 𝑑 ∈ ℝ )
165 164 recnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → 𝑑 ∈ ℂ )
166 163 165 mulcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → ( 𝑅 · 𝑑 ) = ( 𝑑 · 𝑅 ) )
167 simprr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) )
168 166 167 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → ( 𝑅 · 𝑑 ) = ( 𝑐 − 𝑏 ) )
169 151 recnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → ( 𝑐 − 𝑏 ) ∈ ℂ )
170 161 gt0ne0d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → 𝑅 ≠ 0 )
171 169 163 165 170 divmuld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → ( ( ( 𝑐 − 𝑏 ) / 𝑅 ) = 𝑑 ↔ ( 𝑅 · 𝑑 ) = ( 𝑐 − 𝑏 ) ) )
172 168 171 mpbird ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → ( ( 𝑐 − 𝑏 ) / 𝑅 ) = 𝑑 )
173 162 172 breqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → 0 < 𝑑 )
174 146 173 jca ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → ( 𝑑 ∈ ℤ ∧ 0 < 𝑑 ) )
175 elnnz ⊢ ( 𝑑 ∈ ℕ ↔ ( 𝑑 ∈ ℤ ∧ 0 < 𝑑 ) )
176 174 175 sylibr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → 𝑑 ∈ ℕ )
177 167 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → ( 𝑐 − 𝑏 ) = ( 𝑑 · 𝑅 ) )
178 148 recnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → 𝑐 ∈ ℂ )
179 150 recnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → 𝑏 ∈ ℂ )
180 167 169 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → ( 𝑑 · 𝑅 ) ∈ ℂ )
181 178 179 180 subaddd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → ( ( 𝑐 − 𝑏 ) = ( 𝑑 · 𝑅 ) ↔ ( 𝑏 + ( 𝑑 · 𝑅 ) ) = 𝑐 ) )
182 177 181 mpbid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → ( 𝑏 + ( 𝑑 · 𝑅 ) ) = 𝑐 )
183 182 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) ∧ ( 𝑑 ∈ ℤ ∧ ( 𝑑 · 𝑅 ) = ( 𝑐 − 𝑏 ) ) ) → 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) )
184 145 176 183 reximssdv ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) → ∃ 𝑑 ∈ ℕ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) )
185 52 184 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐶 ) ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) ) → ( 𝑏 < 𝑐 ∧ ∃ 𝑑 ∈ ℕ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) )
186 fzfid ⊢ ( 𝜑 → ( 0 ... 𝐵 ) ∈ Fin )
187 xpfi ⊢ ( ( ( 0 ... 𝐵 ) ∈ Fin ∧ ( 0 ... 𝐵 ) ∈ Fin ) → ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ∈ Fin )
188 186 186 187 syl2anc ⊢ ( 𝜑 → ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ∈ Fin )
189 imafi ⊢ ( ( Fun 𝐸 ∧ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ∈ Fin ) → ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) ∈ Fin )
190 121 188 189 syl2anc ⊢ ( 𝜑 → ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) ∈ Fin )
191 125 eleq1d ⊢ ( 𝜑 → ( 𝐶 ∈ Fin ↔ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) ∈ Fin ) )
192 190 191 mpbird ⊢ ( 𝜑 → 𝐶 ∈ Fin )
193 80 zncrng ⊢ ( 𝑅 ∈ ℕ0 → ( ℤ/nℤ ‘ 𝑅 ) ∈ CRing )
194 73 193 syl ⊢ ( 𝜑 → ( ℤ/nℤ ‘ 𝑅 ) ∈ CRing )
195 crngring ⊢ ( ( ℤ/nℤ ‘ 𝑅 ) ∈ CRing → ( ℤ/nℤ ‘ 𝑅 ) ∈ Ring )
196 194 195 syl ⊢ ( 𝜑 → ( ℤ/nℤ ‘ 𝑅 ) ∈ Ring )
197 12 zrhrhm ⊢ ( ( ℤ/nℤ ‘ 𝑅 ) ∈ Ring → 𝐿 ∈ ( ℤring RingHom ( ℤ/nℤ ‘ 𝑅 ) ) )
198 196 197 syl ⊢ ( 𝜑 → 𝐿 ∈ ( ℤring RingHom ( ℤ/nℤ ‘ 𝑅 ) ) )
199 198 imaexd ⊢ ( 𝜑 → ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∈ V )
200 hashclb ⊢ ( ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∈ V → ( ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∈ Fin ↔ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℕ0 ) )
201 199 200 syl ⊢ ( 𝜑 → ( ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∈ Fin ↔ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℕ0 ) )
202 81 201 mpbird ⊢ ( 𝜑 → ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∈ Fin )
203 hashcl ⊢ ( ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∈ Fin → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℕ0 )
204 202 203 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℕ0 )
205 204 nn0red ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℝ )
206 204 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) )
207 sqrtmsq ⊢ ( ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℝ ∧ 0 ≤ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) → ( √ ‘ ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) · ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) = ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) )
208 205 206 207 syl2anc ⊢ ( 𝜑 → ( √ ‘ ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) · ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) = ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) )
209 208 eqcomd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) = ( √ ‘ ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) · ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) )
210 205 206 jca ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℝ ∧ 0 ≤ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) )
211 sqrtmul ⊢ ( ( ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℝ ∧ 0 ≤ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ∧ ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℝ ∧ 0 ≤ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) → ( √ ‘ ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) · ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) = ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) )
212 210 210 211 syl2anc ⊢ ( 𝜑 → ( √ ‘ ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) · ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) = ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) )
213 205 206 resqrtcld ⊢ ( 𝜑 → ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ∈ ℝ )
214 213 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ∈ ℤ )
215 205 206 sqrtge0d ⊢ ( 𝜑 → 0 ≤ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) )
216 213 87 88 syl2anc ⊢ ( 𝜑 → ( 0 ≤ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ↔ 0 ≤ ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) )
217 215 216 mpbid ⊢ ( 𝜑 → 0 ≤ ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) )
218 214 217 jca ⊢ ( 𝜑 → ( ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ) )
219 218 92 sylibr ⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) ∈ ℕ0 )
220 219 95 mpbird ⊢ ( 𝜑 → 𝐵 ∈ ℕ0 )
221 220 nn0red ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
222 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
223 221 222 readdcld ⊢ ( 𝜑 → ( 𝐵 + 1 ) ∈ ℝ )
224 flltp1 ⊢ ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ∈ ℝ → ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) < ( ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) + 1 ) )
225 213 224 syl ⊢ ( 𝜑 → ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) < ( ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) + 1 ) )
226 94 oveq1d ⊢ ( 𝜑 → ( 𝐵 + 1 ) = ( ( ⌊ ‘ ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) + 1 ) )
227 225 226 breqtrrd ⊢ ( 𝜑 → ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) < ( 𝐵 + 1 ) )
228 213 223 213 223 215 227 215 227 ltmul12ad ⊢ ( 𝜑 → ( ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) · ( √ ‘ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) < ( ( 𝐵 + 1 ) · ( 𝐵 + 1 ) ) )
229 212 228 eqbrtrd ⊢ ( 𝜑 → ( √ ‘ ( ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) · ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ) < ( ( 𝐵 + 1 ) · ( 𝐵 + 1 ) ) )
230 209 229 eqbrtrd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) < ( ( 𝐵 + 1 ) · ( 𝐵 + 1 ) ) )
231 hashfz0 ⊢ ( 𝐵 ∈ ℕ0 → ( ♯ ‘ ( 0 ... 𝐵 ) ) = ( 𝐵 + 1 ) )
232 220 231 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ... 𝐵 ) ) = ( 𝐵 + 1 ) )
233 232 232 oveq12d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 0 ... 𝐵 ) ) · ( ♯ ‘ ( 0 ... 𝐵 ) ) ) = ( ( 𝐵 + 1 ) · ( 𝐵 + 1 ) ) )
234 230 233 breqtrrd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) < ( ( ♯ ‘ ( 0 ... 𝐵 ) ) · ( ♯ ‘ ( 0 ... 𝐵 ) ) ) )
235 186 186 jca ⊢ ( 𝜑 → ( ( 0 ... 𝐵 ) ∈ Fin ∧ ( 0 ... 𝐵 ) ∈ Fin ) )
236 hashxp ⊢ ( ( ( 0 ... 𝐵 ) ∈ Fin ∧ ( 0 ... 𝐵 ) ∈ Fin ) → ( ♯ ‘ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) = ( ( ♯ ‘ ( 0 ... 𝐵 ) ) · ( ♯ ‘ ( 0 ... 𝐵 ) ) ) )
237 235 236 syl ⊢ ( 𝜑 → ( ♯ ‘ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) = ( ( ♯ ‘ ( 0 ... 𝐵 ) ) · ( ♯ ‘ ( 0 ... 𝐵 ) ) ) )
238 234 237 breqtrrd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) < ( ♯ ‘ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) )
239 ovexd ⊢ ( 𝜑 → ( 0 ... 𝐵 ) ∈ V )
240 239 239 jca ⊢ ( 𝜑 → ( ( 0 ... 𝐵 ) ∈ V ∧ ( 0 ... 𝐵 ) ∈ V ) )
241 xpexg ⊢ ( ( ( 0 ... 𝐵 ) ∈ V ∧ ( 0 ... 𝐵 ) ∈ V ) → ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ∈ V )
242 240 241 syl ⊢ ( 𝜑 → ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ∈ V )
243 242 mptexd ⊢ ( 𝜑 → ( 𝑤 ∈ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ↦ ( 𝐸 ‘ 𝑤 ) ) ∈ V )
244 120 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) → 𝐸 Fn ( ℕ0 × ℕ0 ) )
245 110 sselda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) → 𝑤 ∈ ( ℕ0 × ℕ0 ) )
246 simpr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) → 𝑤 ∈ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) )
247 244 245 246 fnfvimad ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) → ( 𝐸 ‘ 𝑤 ) ∈ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) )
248 eqid ⊢ ( 𝑤 ∈ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ↦ ( 𝐸 ‘ 𝑤 ) ) = ( 𝑤 ∈ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ↦ ( 𝐸 ‘ 𝑤 ) )
249 247 248 fmptd ⊢ ( 𝜑 → ( 𝑤 ∈ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ↦ ( 𝐸 ‘ 𝑤 ) ) : ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ⟶ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) )
250 119 110 feqresmpt ⊢ ( 𝜑 → ( 𝐸 ↾ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) = ( 𝑤 ∈ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ↦ ( 𝐸 ‘ 𝑤 ) ) )
251 250 feq1d ⊢ ( 𝜑 → ( ( 𝐸 ↾ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) : ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ⟶ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) ↔ ( 𝑤 ∈ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ↦ ( 𝐸 ‘ 𝑤 ) ) : ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ⟶ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) ) )
252 249 251 mpbird ⊢ ( 𝜑 → ( 𝐸 ↾ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) : ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ⟶ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) )
253 f1resf1 ⊢ ( ( 𝐸 : ( ℕ0 × ℕ0 ) –1-1→ ℕ ∧ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ⊆ ( ℕ0 × ℕ0 ) ∧ ( 𝐸 ↾ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) : ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ⟶ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) ) → ( 𝐸 ↾ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) : ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) –1-1→ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) )
254 117 110 252 253 syl3anc ⊢ ( 𝜑 → ( 𝐸 ↾ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) : ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) –1-1→ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) )
255 eqidd ⊢ ( 𝜑 → ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) = ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) )
256 eqidd ⊢ ( 𝜑 → ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) = ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) )
257 250 255 256 f1eq123d ⊢ ( 𝜑 → ( ( 𝐸 ↾ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) : ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) –1-1→ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) ↔ ( 𝑤 ∈ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ↦ ( 𝐸 ‘ 𝑤 ) ) : ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) –1-1→ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) ) )
258 254 257 mpbid ⊢ ( 𝜑 → ( 𝑤 ∈ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ↦ ( 𝐸 ‘ 𝑤 ) ) : ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) –1-1→ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) )
259 df-ima ⊢ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) = ran ( 𝐸 ↾ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) )
260 259 a1i ⊢ ( 𝜑 → ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) = ran ( 𝐸 ↾ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) )
261 250 rneqd ⊢ ( 𝜑 → ran ( 𝐸 ↾ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) = ran ( 𝑤 ∈ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ↦ ( 𝐸 ‘ 𝑤 ) ) )
262 260 261 eqtr2d ⊢ ( 𝜑 → ran ( 𝑤 ∈ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ↦ ( 𝐸 ‘ 𝑤 ) ) = ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) )
263 258 262 jca ⊢ ( 𝜑 → ( ( 𝑤 ∈ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ↦ ( 𝐸 ‘ 𝑤 ) ) : ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) –1-1→ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) ∧ ran ( 𝑤 ∈ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ↦ ( 𝐸 ‘ 𝑤 ) ) = ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) ) )
264 dff1o5 ⊢ ( ( 𝑤 ∈ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ↦ ( 𝐸 ‘ 𝑤 ) ) : ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) –1-1-onto→ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) ↔ ( ( 𝑤 ∈ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ↦ ( 𝐸 ‘ 𝑤 ) ) : ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) –1-1→ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) ∧ ran ( 𝑤 ∈ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ↦ ( 𝐸 ‘ 𝑤 ) ) = ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) ) )
265 263 264 sylibr ⊢ ( 𝜑 → ( 𝑤 ∈ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ↦ ( 𝐸 ‘ 𝑤 ) ) : ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) –1-1-onto→ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) )
266 f1oeq1 ⊢ ( 𝑢 = ( 𝑤 ∈ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ↦ ( 𝐸 ‘ 𝑤 ) ) → ( 𝑢 : ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) –1-1-onto→ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) ↔ ( 𝑤 ∈ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ↦ ( 𝐸 ‘ 𝑤 ) ) : ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) –1-1-onto→ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) ) )
267 243 265 266 spcedv ⊢ ( 𝜑 → ∃ 𝑢 𝑢 : ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) –1-1-onto→ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) )
268 hasheqf1oi ⊢ ( ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ∈ V → ( ∃ 𝑢 𝑢 : ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) –1-1-onto→ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) → ( ♯ ‘ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) = ( ♯ ‘ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) ) ) )
269 242 268 syl ⊢ ( 𝜑 → ( ∃ 𝑢 𝑢 : ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) –1-1-onto→ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) → ( ♯ ‘ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) = ( ♯ ‘ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) ) ) )
270 267 269 mpd ⊢ ( 𝜑 → ( ♯ ‘ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) = ( ♯ ‘ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) ) )
271 238 270 breqtrd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) < ( ♯ ‘ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) ) )
272 125 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ 𝐶 ) = ( ♯ ‘ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) ) )
273 271 272 breqtrrd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) < ( ♯ ‘ 𝐶 ) )
274 zringbas ⊢ ℤ = ( Base ‘ ℤring )
275 eqid ⊢ ( Base ‘ ( ℤ/nℤ ‘ 𝑅 ) ) = ( Base ‘ ( ℤ/nℤ ‘ 𝑅 ) )
276 274 275 rhmf ⊢ ( 𝐿 ∈ ( ℤring RingHom ( ℤ/nℤ ‘ 𝑅 ) ) → 𝐿 : ℤ ⟶ ( Base ‘ ( ℤ/nℤ ‘ 𝑅 ) ) )
277 198 276 syl ⊢ ( 𝜑 → 𝐿 : ℤ ⟶ ( Base ‘ ( ℤ/nℤ ‘ 𝑅 ) ) )
278 277 ffnd ⊢ ( 𝜑 → 𝐿 Fn ℤ )
279 278 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐶 ) → 𝐿 Fn ℤ )
280 resss ⊢ ( 𝐸 ↾ ( ℕ0 × ℕ0 ) ) ⊆ 𝐸
281 280 a1i ⊢ ( 𝜑 → ( 𝐸 ↾ ( ℕ0 × ℕ0 ) ) ⊆ 𝐸 )
282 rnss ⊢ ( ( 𝐸 ↾ ( ℕ0 × ℕ0 ) ) ⊆ 𝐸 → ran ( 𝐸 ↾ ( ℕ0 × ℕ0 ) ) ⊆ ran 𝐸 )
283 281 282 syl ⊢ ( 𝜑 → ran ( 𝐸 ↾ ( ℕ0 × ℕ0 ) ) ⊆ ran 𝐸 )
284 df-ima ⊢ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) = ran ( 𝐸 ↾ ( ℕ0 × ℕ0 ) )
285 284 a1i ⊢ ( 𝜑 → ( 𝐸 “ ( ℕ0 × ℕ0 ) ) = ran ( 𝐸 ↾ ( ℕ0 × ℕ0 ) ) )
286 285 sseq1d ⊢ ( 𝜑 → ( ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ⊆ ran 𝐸 ↔ ran ( 𝐸 ↾ ( ℕ0 × ℕ0 ) ) ⊆ ran 𝐸 ) )
287 283 286 mpbird ⊢ ( 𝜑 → ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ⊆ ran 𝐸 )
288 frn ⊢ ( 𝐸 : ( ℕ0 × ℕ0 ) ⟶ ℕ → ran 𝐸 ⊆ ℕ )
289 119 288 syl ⊢ ( 𝜑 → ran 𝐸 ⊆ ℕ )
290 287 289 sstrd ⊢ ( 𝜑 → ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ⊆ ℕ )
291 nnssz ⊢ ℕ ⊆ ℤ
292 291 a1i ⊢ ( 𝜑 → ℕ ⊆ ℤ )
293 290 292 sstrd ⊢ ( 𝜑 → ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ⊆ ℤ )
294 293 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐶 ) → ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ⊆ ℤ )
295 125 sseq1d ⊢ ( 𝜑 → ( 𝐶 ⊆ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ↔ ( 𝐸 “ ( ( 0 ... 𝐵 ) × ( 0 ... 𝐵 ) ) ) ⊆ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) )
296 112 295 mpbird ⊢ ( 𝜑 → 𝐶 ⊆ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) )
297 296 sseld ⊢ ( 𝜑 → ( 𝑡 ∈ 𝐶 → 𝑡 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) )
298 297 imp ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐶 ) → 𝑡 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) )
299 fnfvima ⊢ ( ( 𝐿 Fn ℤ ∧ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ⊆ ℤ ∧ 𝑡 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) → ( 𝐿 ‘ 𝑡 ) ∈ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) )
300 279 294 298 299 syl3anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐶 ) → ( 𝐿 ‘ 𝑡 ) ∈ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) )
301 eqid ⊢ ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) = ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) )
302 300 301 fmptd ⊢ ( 𝜑 → ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) : 𝐶 ⟶ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) )
303 nnssre ⊢ ℕ ⊆ ℝ
304 303 a1i ⊢ ( 𝜑 → ℕ ⊆ ℝ )
305 127 304 sstrd ⊢ ( 𝜑 → 𝐶 ⊆ ℝ )
306 192 202 273 302 305 hashnexinjle ⊢ ( 𝜑 → ∃ 𝑏 ∈ 𝐶 ∃ 𝑐 ∈ 𝐶 ( ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑏 ) = ( ( 𝑡 ∈ 𝐶 ↦ ( 𝐿 ‘ 𝑡 ) ) ‘ 𝑐 ) ∧ 𝑏 < 𝑐 ) )
307 185 306 reximddv2 ⊢ ( 𝜑 → ∃ 𝑏 ∈ 𝐶 ∃ 𝑐 ∈ 𝐶 ( 𝑏 < 𝑐 ∧ ∃ 𝑑 ∈ ℕ 𝑐 = ( 𝑏 + ( 𝑑 · 𝑅 ) ) ) )
308 51 307 r19.29vva ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐻 “ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ) ≤ ( 𝑁 ↑ 𝐵 ) )